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