Core & Booleans

Basic Boolean Term Builders

cvc5.pythonic.Bool(name, ctx=None)

Return a Boolean constant named name. If ctx=None, then the global context is used.

>>> p = Bool('p')
>>> q = Bool('q')
>>> And(p, q)
And(p, q)
cvc5.pythonic.BoolVal(val, ctx=None)

Return the Boolean value True or False. If ctx=None, then the global context is used.

>>> BoolVal(True)
True
>>> is_true(BoolVal(True))
True
>>> is_true(True)
False
>>> is_false(BoolVal(False))
True
cvc5.pythonic.BoolSort(ctx=None)

Return the Boolean SMT sort. If ctx=None, then the global context is used.

>>> BoolSort()
Bool
>>> p = Const('p', BoolSort())
>>> is_bool(p)
True
>>> r = Function('r', IntSort(), IntSort(), BoolSort())
>>> r(0, 1)
r(0, 1)
>>> is_bool(r(0, 1))
True
cvc5.pythonic.FreshBool(prefix='b', ctx=None)

Return a fresh Boolean constant in the given context using the given prefix.

If ctx=None, then the global context is used.

>>> b1 = FreshBool()
>>> b2 = FreshBool()
>>> eq(b1, b2)
False
cvc5.pythonic.Bools(names, ctx=None)

Return a tuple of Boolean constants.

names is a single string containing all names separated by blank spaces. If ctx=None, then the global context is used.

>>> p, q, r = Bools('p q r')
>>> And(p, Or(q, r))
And(p, Or(q, r))
cvc5.pythonic.BoolVector(prefix, sz, ctx=None)

Return a list of Boolean constants of size sz.

The constants are named using the given prefix. If ctx=None, then the global context is used.

>>> P = BoolVector('p', 3)
>>> P
[p__0, p__1, p__2]
>>> And(P)
And(p__0, p__1, p__2)

Basic Generic Term Builders

cvc5.pythonic.Const(name, sort)

Create a constant of the given sort.

>>> Const('x', IntSort())
x
cvc5.pythonic.Consts(names, sort)

Create several constants of the given sort.

names is a string containing the names of all constants to be created. Blank spaces separate the names of different constants.

>>> x, y, z = Consts('x y z', IntSort())
>>> x + y + z
x + y + z
cvc5.pythonic.FreshConst(sort, prefix='c')

Create a fresh constant of a specified sort

>>> x = FreshConst(BoolSort(), prefix="test")
>>> y = FreshConst(BoolSort(), prefix="test")
>>> x.eq(y)
False
cvc5.pythonic.Function(name, *sig)

Create a new SMT uninterpreted function with the given sorts.

>>> f = Function('f', IntSort(), IntSort())
>>> f(f(0))
f(f(0))
cvc5.pythonic.FreshFunction(*sig)

Create a new fresh SMT uninterpreted function with the given sorts.

>>> f = FreshFunction(IntSort(), IntSort())
>>> x = Int('x')
>>> solve([f(x) != f(x)])
no solution

Boolean Operators

cvc5.pythonic.And(*args)

Create an SMT and-expression or and-probe.

>>> p, q, r = Bools('p q r')
>>> And(p, q, r)
And(p, q, r)
>>> And(p, q, r, main_ctx())
And(p, q, r)
>>> P = BoolVector('p', 5)
>>> And(P)
And(p__0, p__1, p__2, p__3, p__4)
cvc5.pythonic.Or(*args)

Create an SMT or-expression or or-probe.

>>> p, q, r = Bools('p q r')
>>> Or(p, q, r)
Or(p, q, r)
>>> Or(p, q, r, main_ctx())
Or(p, q, r)
>>> P = BoolVector('p', 5)
>>> Or(P)
Or(p__0, p__1, p__2, p__3, p__4)
cvc5.pythonic.Not(a, ctx=None)

Create an SMT not expression or probe.

>>> p = Bool('p')
>>> Not(Not(p))
Not(Not(p))
cvc5.pythonic.mk_not(a)

Negate a boolean expression. Strips a negation if one is already present

>>> x = Bool('x')
>>> mk_not(x)
Not(x)
>>> mk_not(mk_not(x))
x
cvc5.pythonic.Implies(a, b, ctx=None)

Create an SMT implies expression.

>>> p, q = Bools('p q')
>>> Implies(p, q)
Implies(p, q)
cvc5.pythonic.Xor(a, b, ctx=None)

Create an SMT Xor expression.

>>> p, q = Bools('p q')
>>> Xor(p, q)
Xor(p, q)

Generic Operators

cvc5.pythonic.If(a, b, c, ctx=None)

Create an SMT if-then-else expression.

>>> x = Int('x')
>>> y = Int('y')
>>> max = If(x > y, x, y)
>>> max
If(x > y, x, y)
>>> If(True, 1, 0, main_ctx())
If(True, 1, 0)
cvc5.pythonic.Distinct(*args)

Create an SMT distinct expression.

>>> x = Int('x')
>>> y = Int('y')
>>> Distinct(x, y)
x != y
>>> z = Int('z')
>>> Distinct(x, y, z)
Distinct(x, y, z)

Equality

See cvc5.pythonic.ExprRef.__eq__() and cvc5.pythonic.ExprRef.__ne__() for building equality and disequality terms.

Testers

cvc5.pythonic.is_bool(a)

Return True if a is an SMT Boolean expression.

>>> p = Bool('p')
>>> is_bool(p)
True
>>> q = Bool('q')
>>> is_bool(And(p, q))
True
>>> x = Real('x')
>>> is_bool(x)
False
>>> is_bool(x == 0)
True
cvc5.pythonic.is_bool_value(a)

Return True if a is an integer value of sort Int.

>>> is_bool_value(IntVal(1))
False
>>> is_bool_value(Bool('x'))
False
>>> is_bool_value(BoolVal(False))
True
cvc5.pythonic.is_true(a)

Return True if a is the SMT true expression.

>>> p = Bool('p')
>>> is_true(p)
False
>>> x = Real('x')
>>> is_true(x == 0)
False
>>> # True is a Python Boolean expression
>>> is_true(True)
False
cvc5.pythonic.is_false(a)

Return True if a is the SMT false expression.

>>> p = Bool('p')
>>> is_false(p)
False
>>> is_false(False)
False
>>> is_false(BoolVal(False))
True
cvc5.pythonic.is_and(a)

Return True if a is an SMT and expression.

>>> p, q = Bools('p q')
>>> is_and(And(p, q))
True
>>> is_and(Or(p, q))
False
cvc5.pythonic.is_or(a)

Return True if a is an SMT or expression.

>>> p, q = Bools('p q')
>>> is_or(Or(p, q))
True
>>> is_or(And(p, q))
False
cvc5.pythonic.is_implies(a)

Return True if a is an SMT implication expression.

>>> p, q = Bools('p q')
>>> is_implies(Implies(p, q))
True
>>> is_implies(And(p, q))
False
cvc5.pythonic.is_not(a)

Return True if a is an SMT not expression.

>>> p = Bool('p')
>>> is_not(p)
False
>>> is_not(Not(p))
True
cvc5.pythonic.is_eq(a)

Return True if a is an SMT equality expression.

>>> x, y = Ints('x y')
>>> is_eq(x == y)
True
cvc5.pythonic.is_distinct(a)

Return True if a is an SMT distinct expression.

>>> x, y, z = Ints('x y z')
>>> is_distinct(x == y)
False
>>> is_distinct(Distinct(x, y, z))
True
cvc5.pythonic.is_const(a)

Return True if a is SMT constant/variable expression.

These include:
  • concrete (i.e. literal, or non-symbolic) values

  • declared constants

These do not include:
  • bound variables

  • quantified formulae

  • applied operators

>>> a = Int('a')
>>> is_const(a)
True
>>> is_const(a + 1)
False
>>> is_const(1)
False
>>> is_const(IntVal(1))
True
>>> x = Int('x')
cvc5.pythonic.is_func_decl(a)

Return True if a is an SMT function declaration.

>>> f = Function('f', IntSort(), IntSort())
>>> is_func_decl(f)
True
>>> x = Real('x')
>>> is_func_decl(x)
False

Classes (with overloads)

class cvc5.pythonic.ExprRef(ast, ctx=None, reverse_children=False)

Constraints, formulas and terms are expressions.

__bool__()

Convert this expression to a python boolean.

Produces * the appropriate value for a BoolVal. * whether structural equality holds for an EQ-node

>>> bool(BoolVal(True))
True
>>> bool(BoolVal(False))
False
>>> bool(BoolVal(False) == BoolVal(False))
True
>>> try:
...   bool(Int('y'))
... except SMTException as ex:
...   print("failed: %s" % ex)
failed: Symbolic expressions cannot be cast to concrete Boolean values.
__eq__(other)

Return an SMT expression that represents the constraint self == other.

If other is None, then this method simply returns False.

>>> a = Int('a')
>>> b = Int('b')
>>> a == b
a == b
>>> a is None
False
>>> a == None
False
__hash__()

Hash code.

__init__(ast, ctx=None, reverse_children=False)
__ne__(other)

Return an SMT expression that represents the constraint self != other.

If other is None, then this method simply returns True.

>>> a = Int('a')
>>> b = Int('b')
>>> a != b
a != b
>>> a is not None
True
>>> a != None
True
__nonzero__()

Convert this expression to a python boolean. See __bool__.

>>> (BoolVal(False) == BoolVal(False)).__nonzero__()
True
__repr__()

Return repr(self).

__str__()

Return str(self).

__weakref__

list of weak references to the object (if defined)

arg(idx)

Return argument idx of the application self.

This method assumes that self is a function application with at least idx+1 arguments.

>>> a = Int('a')
>>> b = Int('b')
>>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
>>> t = f(a, b, 0)
>>> t.arg(0)
a
>>> t.arg(1)
b
>>> t.arg(2)
0
as_ast()

Return a pointer to the underlying Term object.

children()

Return a list containing the children of the given expression

>>> a = Int('a')
>>> b = Int('b')
>>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
>>> t = f(a, b, 0)
>>> t.children()
[a, b, 0]
decl()

Return the SMT function declaration associated with an SMT application.

>>> f = Function('f', IntSort(), IntSort())
>>> a = Int('a')
>>> t = f(a)
>>> eq(t.decl(), f)
True
>>> try:
...   Int('y').decl()
... except SMTException as ex:
...   print("failed: %s" % ex)
failed: Declarations for non-function applications
eq(other)

Return True if self and other are structurally identical.

>>> x = Int('x')
>>> n1 = x + 1
>>> n2 = 1 + x
>>> n1.eq(n2)
False
get_id()

Return unique identifier for object. It can be used for hash-tables and maps.

>>> BoolVal(True).get_id() == BoolVal(True).get_id()
True
hash()

Return a hashcode for the self.

>>> n1 = Int('x') + 1
>>> n2 = Int('x') + 1
>>> n1.hash() == n2.hash()
True
is_int()

Return True if self is of the sort Integer.

>>> x = Int('x')
>>> x.is_int()
True
>>> (x + 1).is_int()
True
>>> x = Real('x')
>>> x.is_int()
False
>>> Set('x', IntSort()).is_int()
False
kind()

Return the Kind of this term

>>> f = Function('f', IntSort(), IntSort())
>>> a = Int('a')
>>> t = f(a)
>>> t.kind() == Kind.APPLY_UF
True
num_args()

Return the number of arguments of an SMT application.

>>> a = Int('a')
>>> b = Int('b')
>>> (a + b).num_args()
2
>>> f = Function('f', IntSort(), IntSort(), IntSort(), IntSort())
>>> t = f(a, b, 0)
>>> t.num_args()
3
sexpr()

Return a string representing the AST node in s-expression notation.

>>> x = Int('x')
>>> ((x + 1)*x).sexpr()
'(* (+ x 1) x)'
sort()

Return the sort of expression self.

>>> x = Int('x')
>>> (x + 1).sort()
Int
>>> y = Real('y')
>>> (x + y).sort()
Real
class cvc5.pythonic.SortRef(ast, ctx=None)

A Sort is essentially a type. Every term has a sort

__eq__(other)

Return self==value.

__hash__()

Hash code.

__init__(ast, ctx=None)
__ne__(other)

Return True if self and other are not the same SMT sort.

>>> p = Bool('p')
>>> p.sort() != BoolSort()
False
>>> p.sort() != IntSort()
True
__repr__()

A pretty-printed representation of this sort.

>>> repr(IntSort())
'Int'
__str__()

A pretty-printed representation of this sort.

>>> str(IntSort())
'Int'
__weakref__

list of weak references to the object (if defined)

as_ast()

Return a pointer to the underlying Sort object.

cast(val)

Try to cast val as an element of sort self.

This method is used in SMT to convert Python objects such as integers, floats, longs and strings into SMT expressions.

>>> x = Int('x')
>>> RealSort().cast(x)
ToReal(x)
eq(other)

Return True if self and other are structurally identical.

>>> x = Int('x')
>>> n1 = x + 1
>>> n2 = 1 + x
>>> n1.eq(n2)
False
>>> n1.eq(x + 1)
True
hash()

Return a hashcode for the self.

>>> n1 = IntSort()
>>> n2 = RealSort()
>>> n1.hash() == n2.hash()
False
is_int()

Subclasses override

>>> SetSort(IntSort()).is_int()
False
name()

Return the name (string) of sort self.

>>> BoolSort().name()
'Bool'
>>> ArraySort(IntSort(), IntSort()).name()
'(Array Int Int)'
sexpr()

Return a string representing the AST node in s-expression notation.

>>> IntSort().sexpr()
'Int'
subsort(other)

Return True if self is a subsort of other.

>>> IntSort().subsort(RealSort())
True
>>> BoolSort().subsort(RealSort())
True
>>> SetSort(BitVecSort(2)).subsort(SetSort(IntSort()))
False
class cvc5.pythonic.BoolRef(ast, ctx=None, reverse_children=False)

All Boolean expressions are instances of this class.

__mul__(other)

Create the SMT expression self * other.

>>> x = Real("x")
>>> BoolVal(True) * x
If(True, x, 0)
__rmul__(other)
>>> x = Real("x")
>>> x * BoolVal(True)
If(True, x, 0)
sort()

Return the sort of expression self.

>>> x = Int('x')
>>> (x + 1).sort()
Int
>>> y = Real('y')
>>> (x + y).sort()
Real
class cvc5.pythonic.BoolSortRef(ast, ctx=None)

Boolean sort.

cast(val)

Try to cast val as a Boolean.

>>> x = BoolSort().cast(True)
>>> x
True
>>> is_expr(x)
True
>>> is_expr(True)
False
>>> x.sort()
Bool
>>> try:
...   BoolSort().cast(Int('y'))
... except SMTException as ex:
...   print("failed")
failed
>>> try:
...   BoolSort().cast(1)
... except SMTException as ex:
...   print("failed")
failed
is_bool()

Return True if self is of the sort Boolean.

>>> x = BoolSort()
>>> x.is_bool()
True
is_int()

Return True if self is of the sort Integer.

>>> x = IntSort()
>>> x.is_int()
True
>>> x = RealSort()
>>> x.is_int()
False
>>> x = BoolSort()
>>> x.is_int()
True
subsort(other)

Return True if self is a subsort of other.

>>> IntSort().subsort(RealSort())
True
>>> BoolSort().subsort(RealSort())
True
>>> SetSort(BitVecSort(2)).subsort(SetSort(IntSort()))
False
class cvc5.pythonic.FuncDeclRef(ast, ctx=None, reverse_children=False)

Function declaration. Every constant and function have an associated declaration.

The declaration assigns a name, a sort (i.e., type), and for function the sort (i.e., type) of each of its arguments. Note that, in SMT, a constant is a function with 0 arguments.

__call__(*args)

Create an SMT application expression using the function self, and the given arguments.

The arguments must be SMT expressions. This method assumes that the sorts of the elements in args match the sorts of the domain. Limited coercion is supported. For example, if args[0] is a Python integer, and the function expects a SMT integer, then the argument is automatically converted into a SMT integer.

>>> f = Function('f', IntSort(), RealSort(), BoolSort())
>>> x = Int('x')
>>> y = Real('y')
>>> f(x, y)
f(x, y)
>>> f(x, x)
f(x, ToReal(x))
arity()

Return the number of arguments of a function declaration. If self is a constant, then self.arity() is 0.

>>> f = Function('f', IntSort(), RealSort(), BoolSort())
>>> f.arity()
2
domain(i)

Return the sort of the argument i of a function declaration. This method assumes that 0 <= i < self.arity().

>>> f = Function('f', IntSort(), RealSort(), BoolSort())
>>> f.domain(0)
Int
>>> f.domain(1)
Real
name()

Return the name of the function declaration self.

>>> f = Function('f', IntSort(), IntSort())
>>> f.name()
'f'
>>> isinstance(f.name(), str)
True
range()

Return the sort of the range of a function declaration. For constants, this is the sort of the constant.

>>> f = Function('f', IntSort(), RealSort(), BoolSort())
>>> f.range()
Bool