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