Theory of Finite Fields
examples/api/cpp/finite_field.cpp
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * An example of solving finite field problems with cvc5's cpp API.
11 */
12
13#include <cvc5/cvc5.h>
14
15#include <cassert>
16#include <iostream>
17
18using namespace std;
19using namespace cvc5;
20
21int main()
22{
23 TermManager tm;
24 Solver solver(tm);
25 solver.setOption("produce-models", "true");
26
27 Sort f5 = tm.mkFiniteFieldSort("5");
28 Term a = tm.mkConst(f5, "a");
29 Term b = tm.mkConst(f5, "b");
30 Term z = tm.mkFiniteFieldElem("0", f5);
31
32 Term inv = tm.mkTerm(Kind::EQUAL,
33 {tm.mkTerm(Kind::FINITE_FIELD_ADD,
34 {tm.mkTerm(Kind::FINITE_FIELD_MULT, {a, b}),
35 tm.mkFiniteFieldElem("-1", f5)}),
36 z});
37 Term aIsTwo = tm.mkTerm(
38 Kind::EQUAL,
39 {tm.mkTerm(Kind::FINITE_FIELD_ADD, {a, tm.mkFiniteFieldElem("-2", f5)}),
40 z});
41 // ab - 1 = 0
42 solver.assertFormula(inv);
43 // a = 2
44 solver.assertFormula(aIsTwo);
45
46 // should be SAT, with b = 2^(-1)
47 Result r = solver.checkSat();
48 assert(r.isSat());
49
50 cout << "a = " << solver.getValue(a) << endl;
51 cout << "b = " << solver.getValue(b) << endl;
52
53 // b = 2
54 Term bIsTwo = tm.mkTerm(
55 Kind::EQUAL,
56 {tm.mkTerm(Kind::FINITE_FIELD_ADD, {b, tm.mkFiniteFieldElem("-2", f5)}),
57 z});
58
59 // should be UNSAT, 2*2 - 1 != 0
60 solver.assertFormula(bIsTwo);
61
62 r = solver.checkSat();
63 assert(r.isUnsat());
64}
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * An example of solving finite field problems with cvc5's cpp API.
11 */
12
13#include <assert.h>
14#include <cvc5/c/cvc5.h>
15#include <stdio.h>
16
17int main()
18{
19 Cvc5TermManager* tm = cvc5_term_manager_new();
20 Cvc5* slv = cvc5_new(tm);
21 cvc5_set_option(slv, "produce-models", "true");
22
23 Cvc5Sort f5 = cvc5_mk_ff_sort(tm, "5", 10);
24 Cvc5Term a = cvc5_mk_const(tm, f5, "a");
25 Cvc5Term b = cvc5_mk_const(tm, f5, "b");
26 Cvc5Term z = cvc5_mk_ff_elem(tm, "0", f5, 10);
27
28 Cvc5Term args2[2] = {a, b};
29 Cvc5Term ff_mul = cvc5_mk_term(tm, CVC5_KIND_FINITE_FIELD_MULT, 2, args2);
30 args2[0] = ff_mul;
31 args2[1] = cvc5_mk_ff_elem(tm, "-1", f5, 10);
32 Cvc5Term ff_add = cvc5_mk_term(tm, CVC5_KIND_FINITE_FIELD_ADD, 2, args2);
33 args2[0] = ff_add;
34 args2[1] = z;
35 Cvc5Term inv = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
36
37 args2[0] = a;
38 args2[1] = cvc5_mk_ff_elem(tm, "-2", f5, 10);
39 cvc5_term_release(ff_add); // optional, not needed anymore so we can release
40 ff_add = cvc5_mk_term(tm, CVC5_KIND_FINITE_FIELD_ADD, 2, args2);
41 args2[0] = ff_add;
42 args2[1] = z;
43 Cvc5Term a_is_two = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
44
45 // ab - 1 = 0
46 cvc5_assert_formula(slv, inv);
47 // a = 2
48 cvc5_assert_formula(slv, a_is_two);
49
50 // should be SAT, with b = 2^(-1)
51 Cvc5Result r = cvc5_check_sat(slv);
52 assert(cvc5_result_is_sat(r));
53
54 printf("a = %s\n", cvc5_term_to_string(cvc5_get_value(slv, a)));
55 printf("b = %s\n", cvc5_term_to_string(cvc5_get_value(slv, b)));
56
57 // b = 2
58 args2[0] = b;
59 args2[1] = cvc5_mk_ff_elem(tm, "-2", f5, 10);
60 cvc5_term_release(ff_add); // optional, not needed anymore so we can release
61 ff_add = cvc5_mk_term(tm, CVC5_KIND_FINITE_FIELD_ADD, 2, args2);
62 args2[0] = ff_add;
63 args2[1] = z;
64 Cvc5Term b_is_two = cvc5_mk_term(tm, CVC5_KIND_EQUAL, 2, args2);
65
66 // should be UNSAT, 2*2 - 1 != 0
67 cvc5_assert_formula(slv, b_is_two);
68
69 cvc5_result_release(r); // optional, not needed anymore so we can release
70 r = cvc5_check_sat(slv);
71 assert(cvc5_result_is_unsat(r));
72
73 cvc5_delete(slv);
74 cvc5_term_manager_delete(tm);
75}
examples/api/java/FiniteField.java
1/******************************************************************************
2 * This file is part of the cvc5 project.
3 *
4 * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 * in the top-level source directory and their institutional affiliations.
6 * All rights reserved. See the file COPYING in the top-level source
7 * directory for licensing information.
8 * ****************************************************************************
9 *
10 * An example of solving finite field problems with cvc5's Java API
11 *
12 */
13
14import io.github.cvc5.*;
15import java.util.*;
16
17public class FiniteField
18{
19 public static void main(String args[]) throws CVC5ApiException
20 {
21 TermManager tm = new TermManager();
22 Solver slv = new Solver(tm);
23 {
24 slv.setLogic("QF_FF"); // Set the logic
25
26 Sort f5 = tm.mkFiniteFieldSort("5", 10);
27 Term a = tm.mkConst(f5, "a");
28 Term b = tm.mkConst(f5, "b");
29 Term z = tm.mkFiniteFieldElem("0", f5, 10);
30
31 System.out.println("is ff: " + f5.isFiniteField());
32 System.out.println("ff size: " + f5.getFiniteFieldSize());
33 System.out.println("is ff value: " + z.isFiniteFieldValue());
34 System.out.println("ff value: " + z.getFiniteFieldValue());
35
36 Term inv = tm.mkTerm(Kind.EQUAL,
37 tm.mkTerm(Kind.FINITE_FIELD_ADD,
38 tm.mkTerm(Kind.FINITE_FIELD_MULT, a, b),
39 tm.mkFiniteFieldElem("-1", f5, 10)),
40 z);
41
42 Term aIsTwo = tm.mkTerm(
43 Kind.EQUAL, tm.mkTerm(Kind.FINITE_FIELD_ADD, a, tm.mkFiniteFieldElem("-2", f5, 10)), z);
44
45 slv.assertFormula(inv);
46 slv.assertFormula(aIsTwo);
47
48 Result r = slv.checkSat();
49 System.out.println("is sat: " + r.isSat());
50
51 Term bIsTwo = tm.mkTerm(
52 Kind.EQUAL, tm.mkTerm(Kind.FINITE_FIELD_ADD, b, tm.mkFiniteFieldElem("-2", f5, 10)), z);
53
54 slv.assertFormula(bIsTwo);
55 r = slv.checkSat();
56 System.out.println("is sat: " + r.isSat());
57 }
58 Context.deletePointers();
59 }
60}
examples/api/python/pythonic/finite_field.py
1###############################################################################
2# This file is part of the cvc5 project.
3#
4# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5# in the top-level source directory and their institutional affiliations.
6# All rights reserved. See the file COPYING in the top-level source
7# directory for licensing information.
8# #############################################################################
9#
10# An example of solving finite field problems with cvc5's Python API.
11##
12from cvc5.pythonic import *
13
14if __name__ == '__main__':
15 F = FiniteFieldSort(5)
16 a, b = FiniteFieldElems("a b", F)
17 s = Solver()
18
19 # a = 2, b = -2 (or 3) is a solution.
20 r = s.check(a * b == 1, a == 2)
21 assert r == sat
22 print(s.model()[a])
23 assert s.model()[b] == -2
24
25 # no solution
26 r = s.check(a * b == 1, a == 2, b == 2)
27 assert r == unsat
examples/api/python/finite_field.py
1###############################################################################
2# This file is part of the cvc5 project.
3#
4# Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5# in the top-level source directory and their institutional affiliations.
6# All rights reserved. See the file COPYING in the top-level source
7# directory for licensing information.
8# #############################################################################
9#
10# A simple test for cvc5's finite field solver.
11#
12##
13
14import cvc5
15from cvc5 import Kind
16
17if __name__ == "__main__":
18 tm = cvc5.TermManager()
19 slv = cvc5.Solver(tm)
20 slv.setOption("produce-models", "true")
21 F = tm.mkFiniteFieldSort("5")
22 a = tm.mkConst(F, "a")
23 b = tm.mkConst(F, "b")
24
25 inv = tm.mkTerm(
26 Kind.EQUAL,
27 tm.mkTerm(Kind.FINITE_FIELD_MULT, a, b),
28 tm.mkFiniteFieldElem("1", F),
29 )
30 aIsTwo = tm.mkTerm(
31 Kind.EQUAL,
32 a,
33 tm.mkFiniteFieldElem("2", F),
34 )
35 # ab - 1 = 0
36 slv.assertFormula(inv)
37 # a = 2
38 slv.assertFormula(aIsTwo)
39 r = slv.checkSat()
40
41 # should be SAT, with b = 2^(-1)
42 assert r.isSat()
43 print(slv.getValue(a).toPythonObj())
44 assert slv.getValue(b).toPythonObj() == -2
45
46 bIsTwo = tm.mkTerm(
47 Kind.EQUAL,
48 b,
49 tm.mkFiniteFieldElem("2", F),
50 )
51
52 # b = 2
53 slv.assertFormula(bIsTwo)
54 r = slv.checkSat()
55
56 # should be UNSAT, since 2*2 - 1 != 0
57 assert not r.isSat()
examples/api/smtlib/finite_field.smt2
1(set-logic QF_FF)
2(set-option :incremental true)
3
4(define-sort F () (_ FiniteField 5))
5
6(declare-fun a () F)
7(declare-fun b () F)
8
9; ab = 1
10(assert (= (ff.mul a b) (as ff1 F)))
11
12; a = 2
13(assert (= a (as ff2 F)))
14
15; SAT
16(check-sat)
17
18; b = 2
19(assert (= b (as ff2 F)))
20
21; UNSAT
22(check-sat)