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)