Finite Fields 

Basic FiniteField Term Builders 

cvc5.pythonic. FiniteFieldElem ( name , ff , ctx = None ) 

Return a finite field constant named name . ff may be the number of bits of a finite field sort. If ctx=None , then the global context is used.

>>> x  = FiniteFieldElem('x', 17)
>>> is_ff(x)
True
>>> x.size()
17
>>> x.sort()
FiniteField(17)
>>> word = FiniteFieldSort(17)
>>> x2 = FiniteFieldElem('x', word)
>>> eq(x, x2)
True

cvc5.pythonic. FiniteFieldVal ( val , ff , ctx = None ) 

Return a finite field value with the given number of bits. If ctx=None , then the global context is used. The second argument can be a number of bits (integer) or a finite field sort.

>>> v = FiniteFieldVal(10, 29)
>>> v
10
>>> print("0x%.8x" % v.as_long())
0x0000000a
>>> s = FiniteFieldSort(3)
>>> u = FiniteFieldVal(10, s)
>>> u
1

cvc5.pythonic. FiniteFieldSort ( sz , ctx = None ) 

Return an SMT finite field sort of the given size. If ctx=None , then the global context is used.

>>> f7 = FiniteFieldSort(7)
>>> f7
FiniteField(7)
>>> x = Const('x', f7)
>>> eq(x, FiniteFieldElem('x', 7))
True

cvc5.pythonic. FiniteFieldElems ( names , ff , ctx = None ) 

Return a tuple of finite field constants of size ff.

>>> x, y, z = FiniteFieldElems('x y z', 17)
>>> x.size()
17
>>> x.sort()
FiniteField(17)
>>> Sum(x, y, z)
x + y + z
>>> Product(x, y, z)
x*y*z

Arithmetic Overloads 

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

addition ( + )

cvc5.pythonic.FiniteFieldRef.__add__()

subtraction ( - )

cvc5.pythonic.FiniteFieldRef.__sub__()

negation ( - )

cvc5.pythonic.FiniteFieldRef.__neg__()

multiplication ( * )

cvc5.pythonic.FiniteFieldRef.__mul__()

equality ( == )

cvc5.pythonic.ExprRef.__eq__()

cvc5.pythonic. FFAdd ( * args ) 

Create a sum of finite fields.

See also the __add__ overload (+ operator) for FiniteFieldRef.

>>> x, y, z = FiniteFieldElems('x y z', 29)
>>> FFAdd(x, y, z)
x + y + z

cvc5.pythonic. FFSub ( a , b ) 

Create a difference of finite fields.

See also the __sub__ overload (- operator) for FiniteFieldRef.

>>> x, y = FiniteFieldElems('x y', 29)
>>> FFSub(x, y)
x + -y

cvc5.pythonic. FFNeg ( a ) 

Create a negation of a finite field elemetn

See also the __neg__ overload (unary - operator) for FiniteFieldRef.

>>> x = FiniteFieldElem('x', 29)
>>> FFNeg(x)
-x

cvc5.pythonic. FFMult ( * args ) 

Create a product of finite fields.

See also the __mul__ overload (* operator) for FiniteFieldRef.

>>> x, y, z = FiniteFieldElems('x y z', 29)
>>> FFMult(x, y, z)
x*y*z

Testers 

cvc5.pythonic. is_ff_sort ( s ) 

Return True if s is an SMT finite field sort.

>>> is_ff_sort(FiniteFieldSort(29))
True
>>> is_ff_sort(IntSort())
False

cvc5.pythonic. is_ff ( a ) 

Return True if a is an SMT finite field expression.

>>> b = FiniteFieldElem('b', 29)
>>> is_ff(b)
True
>>> is_ff(b + 10)
True
>>> is_ff(Int('x'))
False

cvc5.pythonic. is_ff_value ( a ) 

Return True if a is an SMT finite field numeral value.

>>> b = FiniteFieldElem('b', 29)
>>> is_ff_value(b)
False
>>> b = FiniteFieldVal(10, 29)
>>> b
10
>>> is_ff_value(b)
True

Classes (with overloads) 

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

Bit-vector sort.

cast ( val ) 

Try to cast val as a finite field

>>> b = FiniteFieldSort(31)
>>> b.cast(10)
10
>>> b.cast(10).sexpr()
'#f10m31'

size ( ) 

Return the size (number of elements) of the finite field sort self .

>>> b = FiniteFieldSort(17)
>>> b.size()
17

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

Bit-vector expressions.

__add__ ( other ) 

Create the SMT expression self + other .

>>> x = FiniteFieldElem('x', 29)
>>> y = FiniteFieldElem('y', 29)
>>> x + y
x + y
>>> (x + y).sort()
FiniteField(29)

__mul__ ( other ) 

Create the SMT expression self * other .

>>> x = FiniteFieldElem('x', 29)
>>> y = FiniteFieldElem('y', 29)
>>> x * y
x*y
>>> (x * y).sort()
FiniteField(29)

__neg__ ( ) 

Return an expression representing -self .

>>> x = FiniteFieldElem('x', 29)
>>> -x
-x
>>> solve([-(-x) != x])
no solution

__pos__ ( ) 

Return self .

>>> x = FiniteFieldElem('x', 29)
>>> +x
x

__radd__ ( other ) 

Create the SMT expression other + self .

>>> x = FiniteFieldElem('x', 29)
>>> 10 + x
10 + x

__rmul__ ( other ) 

Create the SMT expression other * self .

>>> x = FiniteFieldElem('x', 29)
>>> 10 * x
10*x

__rsub__ ( other ) 

Create the SMT expression other - self .

>>> x = FiniteFieldElem('x', 29)
>>> 10 - x
10 + -x
>>> 10 + -x
10 + -x

__sub__ ( other ) 

Create the SMT expression self - other .

>>> x = FiniteFieldElem('x', 29)
>>> y = FiniteFieldElem('y', 29)
>>> x - y
x + -y
>>> (x - y).sort()
FiniteField(29)

size ( ) 

Return the number of bits of the finite field expression self .

>>> x = FiniteFieldElem('x', 29)
>>> (x + 1).size()
29

sort ( ) 

Return the sort of the finite field expression self .

>>> x = FiniteFieldElem('x', 29)
>>> x.sort()
FiniteField(29)
>>> x.sort() == FiniteFieldSort(29)
True

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

Bit-vector values.

as_long ( ) 

Return an SMT finite field numeral as a positive Python long (bignum) numeral.

>>> v = FiniteFieldVal(28, 29)
>>> v
-1
>>> v.as_long()
28

as_signed_long ( ) 

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

Returns the numeral of minimum absolute value, so the additive inverse of 1 is “-1”.

>>> FiniteFieldVal(4, 3).as_signed_long()
1
>>> FiniteFieldVal(7, 3).as_signed_long()
1
>>> FiniteFieldVal(3, 3).as_signed_long()
0
>>> FiniteFieldVal(28, 29).as_signed_long()
-1