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.

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

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