Theory Reference: Finite Fields 

Note

Currently, cvc5 only supports finite fields of prime order p.: Such a field is isomorphic to the integers modulo p.

Semantics 

First, for integer \(x\) and positive integer \(y\) , define \((x \bmod y)\) as the unique integer \(r\) such that \(y = qx + r\) (where \(q\) is an integer) and \(0 \le r < q\) . NB: This is the remainder when so-called “floor division” is performed.

We interpret field sorts as prime fields and field terms as integers. In the following, let:

N be an integer numeral and \(N\) be its integer
p be a prime numeral and \(p\) be its prime
F be an SMT field sort (of order \(p\) )
x and y be SMT field terms (of the same sort F ) with interpretations \(x\) and \(y\)

SMT construct	Semantics	Notes
`(_ FiniteField p)`	the field of order \(p\)	represented as the integers modulo \(p\)
`(as ffN F)`	the integer \((N \bmod p)\)
`(ff.add x y)`	the integer \(((x + y) \bmod p)\)	NB: `ff.add` is an n-ary operator
`(ff.mul x y)`	the integer \(((x \times y) \bmod p)\)	NB: `ff.mul` is an n-ary operator
`(= x y)`	the Boolean \(x = y\)

Syntax 

For the C++ API examples in the table below, we assume that we have created a Solver object solver .

	SMT-LIB language	C++ API
Logic String	use FF for finite fields `(set-logic QF_FF)`	use FF for finite fields `solver.setLogic("QF_FF");`
Sort	`(_ FiniteField <Prime Order>)`	`solver.mkFiniteFieldSort(<Prime Order As String>);`
Constants	`(declare-const X (_ FiniteField 7))`	`Sort s = solver.mkFiniteFieldSort("7");` `Term X = solver.mkConst(s, "X");`
Finite Field Value	`(as ff3 (_ FiniteField 7))`	`Sort ffSort = solver.mkFiniteFieldSort("7");` `Term t = solver.mkFiniteFieldElem("3", ffSort);`
Addition	`(ff.add x y)`	`Term t = solver.mkTerm(Kind::FINITE_FIELD_ADD, {x, y});`
Multiplication	`(ff.mul x y)`	`Term t = solver.mkTerm(Kind::FINITE_FIELD_MULT, {x, y});`
Equality	`(= x y)`	`Term t = solver.mkTerm(Kind::EQUAL, {x, y});`

Examples 

            (set-logic QF_FF)
(set-info :status unsat)
(define-sort F () (_ FiniteField 3))
(declare-const x F)
(assert (= (ff.mul x x) (as ff-1 F)))
(check-sat)
; unsat

           

            (set-logic QF_FF)
(set-info :status sat)
(define-sort F () (_ FiniteField 3))
(declare-const x F)
(assert (= (ff.mul x x) (as ff0 F)))
(check-sat)
; sat: (= x (as ff0 F)) is the only model

           

            (set-logic QF_FF)
(set-info :status unsat)
(define-sort F () (_ FiniteField 3))
(declare-const x F)
(declare-const y F)
(declare-const z F)
(assert (= (ff.mul (ff.add x y z) (ff.add x y z)) (as ff-1 F)))
(check-sat)
; unsat

           

Experimental Extensions 

These features of the theory are experimental; they may be removed in the future:

ff.bitsum : an n-ary operator for bitsums: (ff.bitsum x0 x1 x2) is equivalent to \(x_0 + 2x_1 + 4x_2\) .
ff.neg : unary negation

Solvers 

Internally, cvc5 implements two solvers for the theory of finite fields.

The default solver is described in “Satisfiability Modulo Finite Fields” [ OKTB23 ] .
The --ff-solver split flag turns on an alternate solver from “Split Groebner Bases for Satisfiability Modulo Finite Fields” [ OPB+24 ] . This solver may be better on field equations that encode bit-decomposition. See the paper for more information.