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 socalled “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
andy
be SMT field terms (of the same sortF
) with interpretations \(x\) and \(y\)
SMT construct 
Semantics 
Notes 


the field of order \(p\) 
represented as the integers modulo \(p\) 

the integer \((N \bmod p)\) 


the integer \(((x + y) \bmod p)\) 
NB:


the integer \(((x \times y) \bmod p)\) 
NB:


the Boolean \(x = y\) 
Syntax
For the C++ API examples in the table below, we assume that we have created
a
Solver
object
solver
.
SMTLIB language 
C++ API 


Logic String 
use FF for finite fields

use FF for finite fields

Sort 


Constants 


Finite Field Value 


Addition 


Multiplication 


Equality 


Examples
(setlogic QF_FF)
(setinfo :status unsat)
(definesort F () (_ FiniteField 3))
(declareconst x F)
(assert (= (ff.mul x x) (as ff1 F)))
(checksat)
; unsat
(setlogic QF_FF)
(setinfo :status sat)
(definesort F () (_ FiniteField 3))
(declareconst x F)
(assert (= (ff.mul x x) (as ff0 F)))
(checksat)
; sat: (= x (as ff0 F)) is the only model
(setlogic QF_FF)
(setinfo :status unsat)
(definesort F () (_ FiniteField 3))
(declareconst x F)
(declareconst y F)
(declareconst z F)
(assert (= (ff.mul (ff.add x y z) (ff.add x y z)) (as ff1 F)))
(checksat)
; unsat
References
The theory of finite fields was defined in “Satisfiability Modulo Finite Fields” [ OKTB23 ] . See the paper for more information.