Theory of Finite Fields
examples/api/cpp/finite_field.cpp
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-2022 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 Solver solver;
27 solver.setOption("produce-models", "true");
28
29 Sort f5 = solver.mkFiniteFieldSort("5");
30 Term a = solver.mkConst(f5, "a");
31 Term b = solver.mkConst(f5, "b");
32 Term z = solver.mkFiniteFieldElem("0", f5);
33
34 Term inv = solver.mkTerm(
35 Kind::EQUAL,
36 {solver.mkTerm(Kind::FINITE_FIELD_ADD,
37 {solver.mkTerm(Kind::FINITE_FIELD_MULT, {a, b}),
38 solver.mkFiniteFieldElem("-1", f5)}),
39 z});
40 Term aIsTwo =
41 solver.mkTerm(Kind::EQUAL,
42 {solver.mkTerm(Kind::FINITE_FIELD_ADD,
43 {a, solver.mkFiniteFieldElem("-2", f5)}),
44 z});
45 // ab - 1 = 0
46 solver.assertFormula(inv);
47 // a = 2
48 solver.assertFormula(aIsTwo);
49
50 // should be SAT, with b = 2^(-1)
51 Result r = solver.checkSat();
52 assert(r.isSat());
53
54 cout << "a = " << solver.getValue(a) << endl;
55 cout << "b = " << solver.getValue(b) << endl;
56
57 // b = 2
58 Term bIsTwo =
59 solver.mkTerm(Kind::EQUAL,
60 {solver.mkTerm(Kind::FINITE_FIELD_ADD,
61 {b, solver.mkFiniteFieldElem("-2", f5)}),
62 z});
63
64 // should be UNSAT, 2*2 - 1 != 0
65 solver.assertFormula(bIsTwo);
66
67 r = solver.checkSat();
68 assert(!r.isSat());
69}
examples/api/java/FiniteField.java
1/******************************************************************************
2 * Top contributors (to current version):
3 * Alex Ozdemir, Mudathir Mohamed, Liana Hadarean, Morgan Deters
4 *
5 * This file is part of the cvc5 project.
6 *
7 * Copyright (c) 2009-2022 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
1from cvc5.pythonic import *
2
3if __name__ == '__main__':
4 F = FiniteFieldSort(5)
5 a, b = FiniteFieldElems("a b", F)
6 s = Solver()
7
8 # a = 2, b = -2 (or 3) is a solution.
9 r = s.check(a * b == 1, a == 2)
10 assert r == sat
11 print(s.model()[a])
12 assert s.model()[b] == -2
13
14 # no solution
15 r = s.check(a * b == 1, a == 2, b == 2)
16 assert r == unsat
examples/api/python/finite_field.py
1###############################################################################
2# Top contributors (to current version):
3# Andrew Reynolds, Alex Ozdemir
4#
5# This file is part of the cvc5 project.
6#
7# Copyright (c) 2009-2022 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 slv = cvc5.Solver()
22 slv.setOption("produce-models", "true")
23 F = slv.mkFiniteFieldSort("5")
24 a = slv.mkConst(F, "a")
25 b = slv.mkConst(F, "b")
26
27 inv = slv.mkTerm(
28 Kind.EQUAL,
29 slv.mkTerm(Kind.FINITE_FIELD_MULT, a, b),
30 slv.mkFiniteFieldElem("1", F),
31 )
32 aIsTwo = slv.mkTerm(
33 Kind.EQUAL,
34 a,
35 slv.mkFiniteFieldElem("2", F),
36 )
37 # ab - 1 = 0
38 slv.assertFormula(inv)
39 # a = 2
40 slv.assertFormula(aIsTwo)
41 r = slv.checkSat()
42
43 # should be SAT, with b = 2^(-1)
44 assert r.isSat()
45 print(slv.getValue(a).toPythonObj())
46 assert slv.getValue(b).toPythonObj() == -2
47
48 bIsTwo = slv.mkTerm(
49 Kind.EQUAL,
50 b,
51 slv.mkFiniteFieldElem("2", F),
52 )
53
54 # b = 2
55 slv.assertFormula(bIsTwo)
56 r = slv.checkSat()
57
58 # should be UNSAT, since 2*2 - 1 != 0
59 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)