Internals ¶

Testers ¶

cvc5.pythonic. is_expr ( a ) ¶

Return True if a is an SMT expression.

              >>> a = Int('a')
>>> is_expr(a)
True
>>> is_expr(a + 1)
True
>>> is_expr(IntSort())
False
>>> is_expr(1)
False
>>> is_expr(IntVal(1))
True
>>> x = Int('x')

             

cvc5.pythonic. is_sort ( s ) ¶

Return True if s is an SMT sort.

              >>> is_sort(IntSort())
True
>>> is_sort(Int('x'))
False
>>> is_expr(Int('x'))
True

             

cvc5.pythonic. is_app ( a ) ¶

Return True if a is an SMT function application.

Note that, constants are function applications with 0 arguments.

              >>> a = Int('a')
>>> is_app(a)
True
>>> is_app(a + 1)
True
>>> is_app(IntSort())
False
>>> is_app(1)
False
>>> is_app(IntVal(1))
True
>>> x = Int('x')

             

cvc5.pythonic. is_app_of ( a , k ) ¶

Return True if a is an application of the given kind k .

              >>> x = Int('x')
>>> n = x + 1
>>> is_app_of(n, Kind.ADD)
True
>>> is_app_of(n, Kind.MULT)
False

             

Exceptions ¶

class cvc5.pythonic. SMTException ( value ) ¶

__init__ ( value ) ¶

__str__ ( ) ¶: Return str(self).

__weakref__ ¶: list of weak references to the object (if defined)