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

               