Quantifiers 

Builders 

cvc5.pythonic. ForAll ( vs , body ) 

Create a forall formula.

>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> x = Int('x')
>>> y = Int('y')
>>> ForAll([x, y], f(x, y) >= x)
ForAll([x, y], f(x, y) >= x)

cvc5.pythonic. Exists ( vs , body ) 

Create a exists formula.

>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> x = Int('x')
>>> y = Int('y')
>>> q = Exists([x, y], f(x, y) >= x)
>>> q
Exists([x, y], f(x, y) >= x)

cvc5.pythonic. Lambda ( vs , body ) 

Create a lambda expression.

>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> mem0 = Array('mem0', IntSort(), IntSort())
>>> lo, hi, e, i = Ints('lo hi e i')
>>> mem1 = Lambda([i], If(And(lo <= i, i <= hi), e, mem0[i]))
>>> mem1
Lambda(i, If(And(lo <= i, i <= hi), e, mem0[i]))

Testers 

cvc5.pythonic. is_var ( a ) 

Return True if a is bound variable.

>>> x = Int('x')
>>> is_var(x)
False
>>> is_const(x)
True
>>> is_var(BoolSort())
False

cvc5.pythonic. is_quantifier ( a ) 

Return True if a is an SMT quantifier, including lambda expressions.

>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0)
>>> p = Lambda(x, f(x) == 0)
>>> is_quantifier(q)
True
>>> is_quantifier(p)
True
>>> is_quantifier(f(x))
False

Classes 

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

Universally and Existentially quantified formulas.

__getitem__ ( arg ) 

Apply the lambda expression self to arg .

Z3Py gives a lambda an array sort and applies it with [] ; the same spelling works here, even though the sort is a function sort. Note that Select stays an array operation, so Z3Py code written as Select(L, i) should be rewritten as L[i] , which Z3Py accepts too.

>>> x, y = Ints('x y')
>>> i = Int('i')
>>> Lambda([x], x + 1)[i]
Lambda(x, x + 1)(i)
>>> simplify(Lambda([x], x + 1)[3])
4
>>> simplify(Lambda([x, y], x + y)[3, 4])
7

as_ast ( ) 

Return a pointer to the underlying Term object.

body ( ) 

Return the expression being quantified.

>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0)
>>> q.body()
f(x) == 0

children ( ) 

Return a list containing a single element self.body()

>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0)
>>> q.children()
[f(x) == 0]

is_exists ( ) 

Return True if self is an existential quantifier.

>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0)
>>> q.is_exists()
False
>>> q = Exists(x, f(x) != 0)
>>> q.is_exists()
True

is_forall ( ) 

Return True if self is a universal quantifier.

>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = ForAll(x, f(x) == 0)
>>> q.is_forall()
True
>>> q = Exists(x, f(x) != 0)
>>> q.is_forall()
False

is_lambda ( ) 

Return True if self is a lambda expression.

>>> f = Function('f', IntSort(), IntSort())
>>> x = Int('x')
>>> q = Lambda(x, f(x))
>>> q.is_lambda()
True
>>> q = Exists(x, f(x) != 0)
>>> q.is_lambda()
False

num_vars ( ) 

Return the number of variables bounded by this quantifier.

>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> x = Int('x')
>>> y = Int('y')
>>> q = ForAll([x, y], f(x, y) >= x)
>>> q.num_vars()
2

sort ( ) 

Return the Boolean sort, or the function sort of a lambda.

>>> f = Function('f', IntSort(), IntSort())
>>> x, y = Ints('x y')
>>> ForAll(x, f(x) == 0).sort()
Bool
>>> Lambda(x, f(x)).sort()
(-> Int Int)
>>> Lambda(x, f(x)).sort().domain()
Int
>>> Lambda([x, y], f(x) + y).sort().range()
Int

var_name ( idx ) 

Return a string representing a name used when displaying the quantifier.

>>> f = Function('f', IntSort(), IntSort(), IntSort())
>>> x = Int('x')
>>> y = Int('y')
>>> q = ForAll([x, y], f(x, y) >= x)
>>> q.var_name(0)
'x'
>>> q.var_name(1)
'y'

var_sort ( idx ) 

Return the sort of a bound variable.

>>> f = Function('f', IntSort(), RealSort(), IntSort())
>>> x = Int('x')
>>> y = Real('y')
>>> q = ForAll([x, y], f(x, y) >= x)
>>> q.var_sort(0)
Int
>>> q.var_sort(1)
Real