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 =
35 solver.mkTerm(EQUAL,
36 {solver.mkTerm(FINITE_FIELD_ADD,
37 {solver.mkTerm(FINITE_FIELD_MULT, {a, b}),
38 solver.mkFiniteFieldElem("-1", f5)}),
39 z});
40 Term aIsTwo = solver.mkTerm(
41 EQUAL,
42 {solver.mkTerm(FINITE_FIELD_ADD, {a, solver.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 = solver.mkTerm(
58 EQUAL,
59 {solver.mkTerm(FINITE_FIELD_ADD, {b, solver.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.isSat());
67}
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");
29 Term a = slv.mkConst(f5, "a");
30 Term b = slv.mkConst(f5, "b");
31 Term z = slv.mkFiniteFieldElem("0", f5);
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 =
39 slv.mkTerm(Kind.EQUAL,
40 slv.mkTerm(Kind.FINITE_FIELD_ADD,
41 slv.mkTerm(Kind.FINITE_FIELD_MULT, a, b),
42 slv.mkFiniteFieldElem("-1", f5)),
43 z);
44
45 Term aIsTwo =
46 slv.mkTerm(Kind.EQUAL,
47 slv.mkTerm(Kind.FINITE_FIELD_ADD,
48 a,
49 slv.mkFiniteFieldElem("-2", f5)),
50 z);
51
52 slv.assertFormula(inv);
53 slv.assertFormula(aIsTwo);
54
55 Result r = slv.checkSat();
56 System.out.println("is sat: " + r.isSat());
57
58 Term bIsTwo =
59 slv.mkTerm(Kind.EQUAL,
60 slv.mkTerm(Kind.FINITE_FIELD_ADD,
61 b,
62 slv.mkFiniteFieldElem("-2", f5)),
63 z);
64
65 slv.assertFormula(bIsTwo);
66 r = slv.checkSat();
67 System.out.println("is sat: " + r.isSat());
68 }
69 }
70}
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)