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