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}