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.