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