Arithmetic 

Basic Arithmetic Term Builders 

cvc5.pythonic. Int ( name , ctx = None ) 

Return an integer constant named name . If ctx=None , then the global context is used.

>>> x = Int('x')
>>> is_int(x)
True
>>> is_int(x + 1)
True

cvc5.pythonic. Real ( name , ctx = None ) 

Return a real constant named name . If ctx=None , then the global context is used.

>>> x = Real('x')
>>> is_real(x)
True
>>> is_real(x + 1)
True

cvc5.pythonic. IntVal ( val , ctx = None ) 

Return an SMT integer value. If ctx=None , then the global context is used.

>>> IntVal(1)
1
>>> IntVal("100")
100

cvc5.pythonic. RealVal ( val , ctx = None ) 

Return an SMT real value.

val may be a Python int, long, float or string representing a number in decimal or rational notation. If ctx=None , then the global context is used.

>>> RealVal(1)
1
>>> RealVal(1).sort()
Real
>>> RealVal("3/5")
3/5
>>> RealVal("1.5")
3/2

cvc5.pythonic. RatVal ( a , b , ctx = None ) 

Return an SMT rational a/b.

If ctx=None , then the global context is used.

>>> RatVal(3,5)
3/5
>>> RatVal(3,5).sort()
Real

cvc5.pythonic. Q ( a , b , ctx = None ) 

Return an SMT rational a/b.

If ctx=None , then the global context is used.

>>> Q(3,5)
3/5
>>> Q(3,5).sort()
Real
>>> Q(4,8)
1/2

cvc5.pythonic. IntSort ( ctx = None ) 

Return the integer sort in the given context. If ctx=None , then the global context is used.

>>> IntSort()
Int
>>> x = Const('x', IntSort())
>>> is_int(x)
True
>>> x.sort() == IntSort()
True
>>> x.sort() == BoolSort()
False

cvc5.pythonic. RealSort ( ctx = None ) 

Return the real sort in the given context. If ctx=None , then the global context is used.

>>> RealSort()
Real
>>> x = Const('x', RealSort())
>>> is_real(x)
True
>>> is_int(x)
False
>>> x.sort() == RealSort()
True

cvc5.pythonic. FreshInt ( prefix = 'x' , ctx = None ) 

Return a fresh integer constant in the given context using the given prefix.

>>> x = FreshInt()
>>> y = FreshInt()
>>> eq(x, y)
False
>>> x.sort()
Int

cvc5.pythonic. Ints ( names , ctx = None ) 

Return a tuple of Integer constants.

>>> x, y, z = Ints('x y z')
>>> Sum(x, y, z)
x + y + z

cvc5.pythonic. IntVector ( prefix , sz , ctx = None ) 

Return a list of integer constants of size sz .

>>> X = IntVector('x', 3)
>>> X
[x__0, x__1, x__2]
>>> Sum(X)
x__0 + x__1 + x__2

cvc5.pythonic. FreshReal ( prefix = 'b' , ctx = None ) 

Return a fresh real constant in the given context using the given prefix.

>>> x = FreshReal()
>>> y = FreshReal()
>>> eq(x, y)
False
>>> x.sort()
Real

cvc5.pythonic. Reals ( names , ctx = None ) 

Return a tuple of real constants.

>>> x, y, z = Reals('x y z')
>>> Sum(x, y, z)
x + y + z
>>> Sum(x, y, z).sort()
Real

cvc5.pythonic. RealVector ( prefix , sz , ctx = None ) 

Return a list of real constants of size sz .

>>> X = RealVector('x', 3)
>>> X
[x__0, x__1, x__2]
>>> Sum(X)
x__0 + x__1 + x__2
>>> Sum(X).sort()
Real

Arithmetic Overloads 

See the following operator overloads for building arithmetic terms. These terms can also be built with builder functions listed below.

addition ( + )

cvc5.pythonic.ArithRef.__add__()

subtraction ( - )

cvc5.pythonic.ArithRef.__sub__()

multiplication ( * )

cvc5.pythonic.ArithRef.__mul__()

division ( / )

cvc5.pythonic.ArithRef.__div__()

power ( ** )

cvc5.pythonic.ArithRef.__pow__()

negation ( - )

cvc5.pythonic.ArithRef.__neg__()

greater than ( > )

cvc5.pythonic.ArithRef.__gt__()

less than ( < )

cvc5.pythonic.ArithRef.__lt__()

greater than or equal to ( >= )

cvc5.pythonic.ArithRef.__ge__()

less than or equal to ( <= )

cvc5.pythonic.ArithRef.__le__()

equal ( == )

cvc5.pythonic.ExprRef.__eq__()

not equal ( != )

cvc5.pythonic.ExprRef.__ne__()

cvc5.pythonic. Add ( * args ) 

Create an SMT addition.

See also the __add__ overload (+ operator) for arithmetic SMT expressions.

>>> x, y = Ints('x y')
>>> Add(x, x, y)
x + x + y
>>> Add(x, x, y, main_ctx())
x + x + y

cvc5.pythonic. Mult ( * args ) 

Create an SMT multiplication.

See also the __mul__ overload (* operator) for arithmetic SMT expressions.

>>> x, y = Ints('x y')
>>> Mult(x, x, y)
x*x*y
>>> Mult(x, x, y, main_ctx())
x*x*y

cvc5.pythonic. Sub ( a , b ) 

Create an SMT subtraction.

See also the __sub__ overload (- operator) for arithmetic SMT expressions.

>>> x, y = Ints('x y')
>>> Sub(x, y)
x - y

cvc5.pythonic. UMinus ( a ) 

Create an SMT unary negation.

Deprecated. Kept for compatiblity with Z3. See “Neg”.

See also the __neg__ overload (unary - operator) for arithmetic SMT expressions.

>>> x = Int('x')
>>> UMinus(x)
-x

cvc5.pythonic. Div ( a , b ) 

Create an SMT division.

See also the __div__ overload (/ operator) for arithmetic SMT expressions.

>>> x, y = Ints('x y')
>>> a, b = Reals('x y')
>>> Div(x, y).sexpr()
'(div x y)'
>>> Div(a, y).sexpr()
'(/ x (to_real y))'
>>> Div(a, b).sexpr()
'(/ x y)'

cvc5.pythonic. Pow ( a , b ) 

Create an SMT power.

See also the __pow__ overload for arithmetic SMT expressions.

>>> x = Int('x')
>>> Pow(x, 3)
x**3

cvc5.pythonic. IntsModulus ( a , b ) 

Create an SMT integer modulus.

See also the __mod__ overload (% operator) for arithmetic SMT expressions.

>>> x, y = Ints('x y')
>>> IntsModulus(x, y)
x%y

cvc5.pythonic. Leq ( a , b ) 

Create an SMT less-than-or-equal-to.

See also the __le__ overload (<= operator) for arithmetic SMT expressions.

>>> x, y = Ints('x y')
>>> Leq(x, y)
x <= y

cvc5.pythonic. Geq ( a , b ) 

Create an SMT greater-than-or-equal-to.

See also the __ge__ overload (>= operator) for arithmetic SMT expressions.

>>> x, y = Ints('x y')
>>> Geq(x, y)
x >= y

cvc5.pythonic. Lt ( a , b ) 

Create an SMT less-than.

See also the __lt__ overload (< operator) for arithmetic SMT expressions.

>>> x, y = Ints('x y')
>>> Lt(x, y)
x < y

cvc5.pythonic. Gt ( a , b ) 

Create an SMT greater-than.

See also the __gt__ overload (> operator) for arithmetic SMT expressions.

>>> x, y = Ints('x y')
>>> Gt(x, y)
x > y

Other Arithmetic Operators 

cvc5.pythonic. ToReal ( a ) 

Return the SMT expression ToReal(a).

>>> x = Int('x')
>>> x.sort()
Int
>>> n = ToReal(x)
>>> n
ToReal(x)
>>> n.sort()
Real

cvc5.pythonic. ToInt ( a ) 

Return the SMT expression ToInt(a).

>>> x = Real('x')
>>> x.sort()
Real
>>> n = ToInt(x)
>>> n
ToInt(x)
>>> n.sort()
Int

cvc5.pythonic. IsInt ( a ) 

Return the SMT predicate IsInt(a).

>>> x = Real('x')
>>> IsInt(x + "1/2")
IsInt(x + 1/2)
>>> solve(IsInt(x + "1/2"), x > 0, x < 1)
[x = 1/2]
>>> solve(IsInt(x + "1/2"), x > 0, x < 1, x != "1/2")
no solution

cvc5.pythonic. Sqrt ( a , ctx = None ) 

Return an SMT expression which represents the square root of a.

Can also operate on python builtins of arithemtic type.

>>> x = Real('x')
>>> Sqrt(x)
x**(1/2)
>>> Sqrt(4)
4**(1/2)

cvc5.pythonic. Cbrt ( a , ctx = None ) 

Return an SMT expression which represents the cubic root of a.

Can also operate on python builtins of arithemtic type.

>>> x = Real('x')
>>> Cbrt(x)
x**(1/3)
>>> Cbrt(4)
4**(1/3)

Transcendentals 

cvc5.pythonic. Pi ( ctx = None ) 

Create the constant pi

>>> Pi()
Pi

cvc5.pythonic. Exponential ( x ) 

Create an exponential function

>>> x = Real('x')
>>> solve(Exponential(x) == 1)
[x = 0]

cvc5.pythonic. Sine ( x ) 

Create a sine function

>>> x = Real('x')
>>> i = Int('i')
>>> prove(Sine(x) < 2)
proved
>>> prove(Sine(i) < 2)
proved

cvc5.pythonic. Cosine ( x ) 

Create a cosine function

>>> x = Real('x')
>>> i = Int('i')
>>> prove(Cosine(x) < 2)
proved
>>> prove(Cosine(i) < 2)
proved

cvc5.pythonic. Tangent ( x ) 

Create a tangent function

>>> Tangent(Real('x'))
Tangent(x)

cvc5.pythonic. Arcsine ( x ) 

Create an arcsine function

>>> Arcsine(Real('x'))
Arcsine(x)

cvc5.pythonic. Arccosine ( x ) 

Create an arccosine function

>>> Arccosine(Real('x'))
Arccosine(x)

cvc5.pythonic. Arctangent ( x ) 

Create an arctangent function

>>> Arctangent(Real('x'))
Arctangent(x)

cvc5.pythonic. Secant ( x ) 

Create a secant function

>>> Secant(Real('x'))
Secant(x)

cvc5.pythonic. Cosecant ( x ) 

Create a cosecant function

>>> Cosecant(Real('x'))
Cosecant(x)

cvc5.pythonic. Cotangent ( x ) 

Create a cotangent function

>>> Cotangent(Real('x'))
Cotangent(x)

cvc5.pythonic. Arcsecant ( x ) 

Create an arcsecant function

>>> Arcsecant(Real('x'))
Arcsecant(x)

cvc5.pythonic. Arccosecant ( x ) 

Create an arccosecant function

>>> Arccosecant(Real('x'))
Arccosecant(x)

cvc5.pythonic. Arccotangent ( x ) 

Create an arccotangent function

>>> Arccotangent(Real('x'))
Arccotangent(x)

Testers 

cvc5.pythonic. is_arith ( a ) 

Return True if a is an arithmetical expression.

>>> x = Int('x')
>>> is_arith(x)
True
>>> is_arith(x + 1)
True
>>> is_arith(1)
False
>>> is_arith(IntVal(1))
True
>>> y = Real('y')
>>> is_arith(y)
True
>>> is_arith(y + 1)
True

cvc5.pythonic. is_int ( a ) 

Return True if a is an integer expression.

>>> x = Int('x')
>>> is_int(x + 1)
True
>>> is_int(1)
False
>>> is_int(IntVal(1))
True
>>> y = Real('y')
>>> is_int(y)
False
>>> is_int(y + 1)
False

cvc5.pythonic. is_real ( a ) 

Return True if a is a real expression.

>>> x = Int('x')
>>> is_real(x + 1)
False
>>> y = Real('y')
>>> is_real(y)
True
>>> is_real(y + 1)
True
>>> is_real(1)
False
>>> is_real(RealVal(1))
True

cvc5.pythonic. is_int_value ( a ) 

Return True if a is an integer value of sort Int.

>>> is_int_value(IntVal(1))
True
>>> is_int_value(1)
False
>>> is_int_value(Int('x'))
False
>>> n = Int('x') + 1
>>> n
x + 1
>>> n.arg(1)
1
>>> is_int_value(n.arg(1))
True
>>> is_int_value(RealVal("1/3"))
False
>>> is_int_value(RealVal(1))
False

cvc5.pythonic. is_rational_value ( a ) 

Return True if a is rational value of sort Real.

>>> is_rational_value(RealVal(1))
True
>>> is_rational_value(RealVal("3/5"))
True
>>> is_rational_value(IntVal(1))
False
>>> is_rational_value(1)
False
>>> n = Real('x') + 1
>>> n.arg(1)
1
>>> is_rational_value(n.arg(1))
True
>>> is_rational_value(Real('x'))
False

cvc5.pythonic. is_arith_sort ( s ) 

Return True if s is an arithmetical sort (type).

>>> is_arith_sort(IntSort())
True
>>> is_arith_sort(RealSort())
True
>>> is_arith_sort(BoolSort())
False
>>> n = Int('x') + 1
>>> is_arith_sort(n.sort())
True

cvc5.pythonic. is_add ( a ) 

Return True if a is an expression of the form b + c.

>>> x, y = Ints('x y')
>>> is_add(x + y)
True
>>> is_add(x - y)
False

cvc5.pythonic. is_mul ( a ) 

Return True if a is an expression of the form b * c.

>>> x, y = Ints('x y')
>>> is_mul(x * y)
True
>>> is_mul(x - y)
False

cvc5.pythonic. is_sub ( a ) 

Return True if a is an expression of the form b - c.

>>> x, y = Ints('x y')
>>> is_sub(x - y)
True
>>> is_sub(x + y)
False

cvc5.pythonic. is_div ( a ) 

Return True if a is a rational division term (i.e. b / c).

Note: this returns false for integer division. See is_idiv .

>>> x, y = Reals('x y')
>>> is_div(x / y)
True
>>> is_div(x + y)
False
>>> x, y = Ints('x y')
>>> is_div(x / y)
False
>>> is_idiv(x / y)
True

cvc5.pythonic. is_idiv ( a ) 

Return True if a is an expression of the form b div c.

>>> x, y = Ints('x y')
>>> is_idiv(x / y)
True
>>> is_idiv(x + y)
False

cvc5.pythonic. is_mod ( a ) 

Return True if a is an expression of the form b % c.

>>> x, y = Ints('x y')
>>> is_mod(x % y)
True
>>> is_mod(x + y)
False

cvc5.pythonic. is_le ( a ) 

Return True if a is an expression of the form b <= c.

>>> x, y = Ints('x y')
>>> is_le(x <= y)
True
>>> is_le(x < y)
False

cvc5.pythonic. is_lt ( a ) 

Return True if a is an expression of the form b < c.

>>> x, y = Ints('x y')
>>> is_lt(x < y)
True
>>> is_lt(x == y)
False

cvc5.pythonic. is_ge ( a ) 

Return True if a is an expression of the form b >= c.

>>> x, y = Ints('x y')
>>> is_ge(x >= y)
True
>>> is_ge(x == y)
False

cvc5.pythonic. is_gt ( a ) 

Return True if a is an expression of the form b > c.

>>> x, y = Ints('x y')
>>> is_gt(x > y)
True
>>> is_gt(x == y)
False

cvc5.pythonic. is_is_int ( a ) 

Return True if a is an expression of the form IsInt(b).

>>> x = Real('x')
>>> is_is_int(IsInt(x))
True
>>> is_is_int(x)
False

cvc5.pythonic. is_to_real ( a ) 

Return True if a is an expression of the form ToReal(b).

>>> x = Int('x')
>>> n = ToReal(x)
>>> n
ToReal(x)
>>> is_to_real(n)
True
>>> is_to_real(x)
False

cvc5.pythonic. is_to_int ( a ) 

Return True if a is an expression of the form ToInt(b).

>>> x = Real('x')
>>> n = ToInt(x)
>>> n
ToInt(x)
>>> is_to_int(n)
True
>>> is_to_int(x)
False

Classes (with overloads) 

class cvc5.pythonic. ArithSortRef ( ast , ctx = None ) 

Real and Integer sorts.

cast ( val ) 

Try to cast val as an Integer or Real.

>>> IntSort().cast(10)
10
>>> is_int(IntSort().cast(10))
True
>>> is_int(10)
False
>>> RealSort().cast(10)
10
>>> is_real(RealSort().cast(10))
True
>>> IntSort().cast(Bool('x'))
If(x, 1, 0)
>>> RealSort().cast(Bool('x'))
ToReal(If(x, 1, 0))
>>> try:
...   IntSort().cast(RealVal("1.1"))
... except SMTException as ex:
...   print("failed")
failed

is_int ( ) 

Return True if self is of the sort Integer.

>>> x = Int('x')
>>> x.is_int()
True
>>> (x + 1).is_int()
True
>>> x = Real('x')
>>> x.is_int()
False

is_real ( ) 

Return True if self is of the sort Real.

>>> x = Real('x')
>>> x.is_real()
True
>>> (x + 1).is_real()
True
>>> x = Int('x')
>>> x.is_real()
False

subsort ( other ) 

Return True if self is a subsort of other .

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

Integer and Real expressions.

__add__ ( other ) 

Create the SMT expression self + other .

>>> x = Int('x')
>>> y = Int('y')
>>> x + y
x + y
>>> (x + y).sort()
Int

__div__ ( other ) 

Create the SMT expression other/self .

>>> x = Int('x')
>>> y = Int('y')
>>> x/y
x/y
>>> (x/y).sort()
Int
>>> (x/y).sexpr()
'(div x y)'
>>> x = Real('x')
>>> y = Real('y')
>>> x/y
x/y
>>> (x/y).sort()
Real
>>> (x/y).sexpr()
'(/ x y)'

__ge__ ( other ) 

Create the SMT expression other >= self .

>>> x, y = Ints('x y')
>>> x >= y
x >= y
>>> y = Real('y')
>>> x >= y
ToReal(x) >= y

__gt__ ( other ) 

Create the SMT expression other > self .

>>> x, y = Ints('x y')
>>> x > y
x > y
>>> y = Real('y')
>>> x > y
ToReal(x) > y

__le__ ( other ) 

Create the SMT expression other <= self .

>>> x, y = Ints('x y')
>>> x <= y
x <= y
>>> y = Real('y')
>>> x <= y
ToReal(x) <= y

__lt__ ( other ) 

Create the SMT expression other < self .

>>> x, y = Ints('x y')
>>> x < y
x < y
>>> y = Real('y')
>>> x < y
ToReal(x) < y

__mod__ ( other ) 

Create the SMT expression other%self .

>>> x = Int('x')
>>> y = Int('y')
>>> x % y
x%y

__mul__ ( other ) 

Create the SMT expression self * other .

>>> x = Real('x')
>>> y = Real('y')
>>> x * y
x*y
>>> (x * y).sort()
Real
>>> x * BoolVal(True)
If(True, x, 0)

__neg__ ( ) 

Return an expression representing -self .

>>> x = Int('x')
>>> -x
-x

__pos__ ( ) 

Return self .

>>> x = Int('x')
>>> +x
x

__pow__ ( other ) 

Create the SMT expression self**other (** is the power operator).

>>> x = Real('x')
>>> x**3
x**3
>>> (x**3).sort()
Real
>>> solve([x ** 2 == x, x > 0])
[x = 1]

__radd__ ( other ) 

Create the SMT expression other + self .

>>> x = Int('x')
>>> 10 + x
10 + x

__rdiv__ ( other ) 

Create the SMT expression other/self .

>>> x = Int('x')
>>> 10/x
10/x
>>> (10/x).sexpr()
'(div 10 x)'
>>> x = Real('x')
>>> 10/x
10/x
>>> (10/x).sexpr()
'(/ 10.0 x)'

__rmod__ ( other ) 

Create the SMT expression other%self .

>>> x = Int('x')
>>> 10 % x
10%x

__rmul__ ( other ) 

Create the SMT expression other * self .

>>> x = Real('x')
>>> 10 * x
10*x

__rpow__ ( other ) 

Create the SMT expression other**self (** is the power operator).

>>> x = Real('x')
>>> 2**x
2**x
>>> (2**x).sort()
Real

__rsub__ ( other ) 

Create the SMT expression other - self .

>>> x = Int('x')
>>> 10 - x
10 - x

__rtruediv__ ( other ) 

Create the SMT expression other/self .

__sub__ ( other ) 

Create the SMT expression self - other .

>>> x = Int('x')
>>> y = Int('y')
>>> x - y
x - y
>>> (x - y).sort()
Int

__truediv__ ( other ) 

Create the SMT expression other/self .

is_int ( ) 

Return True if self is an integer expression.

>>> x = Int('x')
>>> x.is_int()
True
>>> (x + 1).is_int()
True
>>> y = Real('y')
>>> (x + y).is_int()
False

is_real ( ) 

Return True if self is an real expression.

>>> x = Real('x')
>>> x.is_real()
True
>>> (x + 1).is_real()
True

sort ( ) 

Return the sort (type) of the arithmetical expression self .

>>> Int('x').sort()
Int
>>> (Real('x') + 1).sort()
Real

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

Integer values.

as_binary_string ( ) 

Return an SMT integer numeral as a Python binary string. >>> v = IntVal(10) >>> v.as_binary_string() ‘1010’

as_long ( ) 

Return an SMT integer numeral as a Python long (bignum) numeral.

>>> v = IntVal(1)
>>> v + 1
1 + 1
>>> v.as_long() + 1
2

as_string ( ) 

Return an SMT integer numeral as a Python string. >>> v = IntVal(100) >>> v.as_string() ‘100’

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

Rational values.

as_decimal ( prec ) 

Return an SMT rational value as a string in decimal notation using at most prec decimal places.

>>> v = RealVal("1/5")
>>> v.as_decimal(3)
'0.2'
>>> v = RealVal("1/3")
>>> v.as_decimal(3)
'0.333'

as_fraction ( ) 

Return an SMT rational as a Python Fraction object.

>>> v = RealVal("1/5")
>>> v.as_fraction()
Fraction(1, 5)

as_long ( ) 

Is this arithmetic value an integer? >>> RealVal(“2/1”).as_long() 2 >>> try: … RealVal(“2/3”).as_long() … except SMTException as e: … print(“failed: %s” % e) failed: Expected integer fraction

as_string ( ) 

Return an SMT rational numeral as a Python string.

>>> v = Q(3,6)
>>> v.as_string()
'1/2'

denominator ( ) 

Return the denominator of an SMT rational numeral.

>>> is_rational_value(Q(3,5))
True
>>> n = Q(3,5)
>>> n.denominator()
5

denominator_as_long ( ) 

Return the denominator as a Python long.

>>> v = RealVal("1/3")
>>> v
1/3
>>> v.denominator_as_long()
3

is_int ( ) 

Return True if self is an integer expression.

>>> x = Int('x')
>>> x.is_int()
True
>>> (x + 1).is_int()
True
>>> y = Real('y')
>>> (x + y).is_int()
False

is_int_value ( ) 

Is this arithmetic value an integer? >>> RealVal(“2/1”).is_int_value() True >>> RealVal(“2/3”).is_int_value() False

is_real ( ) 

Return True if self is an real expression.

>>> x = Real('x')
>>> x.is_real()
True
>>> (x + 1).is_real()
True

numerator ( ) 

Return the numerator of an SMT rational numeral.

>>> is_rational_value(RealVal("3/5"))
True
>>> n = RealVal("3/5")
>>> n.numerator()
3
>>> is_rational_value(Q(3,5))
True
>>> Q(3,5).numerator()
3

numerator_as_long ( ) 

Return the numerator as a Python long.

>>> v = RealVal(10000000000)
>>> v
10000000000
>>> v + 1
10000000000 + 1
>>> v.numerator_as_long() + 1 == 10000000001
True