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