docs/api/python/z3compat/boolean.rst

   1 Core & Booleans
   2 ================
   3
   4 Basic Boolean Term Builders
   5 -------------------
   6 .. autofunction:: cvc5_z3py_compat.Bool
   7 .. autofunction:: cvc5_z3py_compat.Bools
   8 .. autofunction:: cvc5_z3py_compat.BoolVal
   9 .. autofunction:: cvc5_z3py_compat.BoolSort
  10 .. autofunction:: cvc5_z3py_compat.FreshBool
  11 .. autofunction:: cvc5_z3py_compat.BoolVector
  12
  13 Basic Generic Term Builders
  14 -------------------
  15 .. autofunction:: cvc5_z3py_compat.Const
  16 .. autofunction:: cvc5_z3py_compat.Consts
  17 .. autofunction:: cvc5_z3py_compat.FreshConst
  18
  19 Boolean Operators
  20 -------------------
  21 .. autofunction:: cvc5_z3py_compat.And
  22 .. autofunction:: cvc5_z3py_compat.Or
  23 .. autofunction:: cvc5_z3py_compat.Not
  24 .. autofunction:: cvc5_z3py_compat.mk_not
  25 .. autofunction:: cvc5_z3py_compat.Implies
  26 .. autofunction:: cvc5_z3py_compat.Xor
  27
  28 Generic Operators
  29 -------------------
  30 .. autofunction:: cvc5_z3py_compat.If
  31 .. autofunction:: cvc5_z3py_compat.Distinct
  32
  33 Equality
  34 ~~~~~~~~
  35
  36 See
  37 :py:meth:`cvc5_z3py_compat.ExprRef.__eq__`
  38 and
  39 :py:meth:`cvc5_z3py_compat.ExprRef.__ne__`
  40 for building equality and disequality terms.
  41
  42
  43 Testers
  44 -------------------
  45 .. autofunction:: cvc5_z3py_compat.is_bool
  46 .. autofunction:: cvc5_z3py_compat.is_true
  47 .. autofunction:: cvc5_z3py_compat.is_false
  48 .. autofunction:: cvc5_z3py_compat.is_and
  49 .. autofunction:: cvc5_z3py_compat.is_or
  50 .. autofunction:: cvc5_z3py_compat.is_implies
  51 .. autofunction:: cvc5_z3py_compat.is_not
  52 .. autofunction:: cvc5_z3py_compat.is_eq
  53 .. autofunction:: cvc5_z3py_compat.is_distinct
  54 .. autofunction:: cvc5_z3py_compat.is_const
  55
  56
  57 Classes
  58 --------
  59 .. autoclass:: cvc5_z3py_compat.ExprRef
  60    :members:
  61    :special-members:
  62 .. autoclass:: cvc5_z3py_compat.SortRef
  63    :members:
  64    :special-members:
  65 .. autoclass:: cvc5_z3py_compat.BoolRef
  66    :members:
  67    :special-members:
  68 .. autoclass:: cvc5_z3py_compat.BoolSortRef
  69    :members:
  70    :special-members: