mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
368f3c3ed6
Organizing the PR a bit: we hook up the subtheories to TheoryFf we expose FF-related things via the C++/Pytohn API and SMT-LIB2 interface. we add a bunch of tests against these interfaces.
68 lines
1.8 KiB
C++
68 lines
1.8 KiB
C++
/******************************************************************************
|
|
* Top contributors (to current version):
|
|
* Alex Ozdemir
|
|
*
|
|
* This file is part of the cvc5 project.
|
|
*
|
|
* Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
|
|
* in the top-level source directory and their institutional affiliations.
|
|
* All rights reserved. See the file COPYING in the top-level source
|
|
* directory for licensing information.
|
|
* ****************************************************************************
|
|
*
|
|
* An example of solving finite field problems with cvc5's cpp API
|
|
*/
|
|
|
|
#include <cvc5/cvc5.h>
|
|
|
|
#include <cassert>
|
|
#include <iostream>
|
|
|
|
using namespace std;
|
|
using namespace cvc5;
|
|
|
|
int main()
|
|
{
|
|
Solver solver;
|
|
solver.setOption("produce-models", "true");
|
|
|
|
Sort f5 = solver.mkFiniteFieldSort("5");
|
|
Term a = solver.mkConst(f5, "a");
|
|
Term b = solver.mkConst(f5, "b");
|
|
Term z = solver.mkFiniteFieldElem("0", f5);
|
|
|
|
Term inv =
|
|
solver.mkTerm(EQUAL,
|
|
{solver.mkTerm(FINITE_FIELD_ADD,
|
|
{solver.mkTerm(FINITE_FIELD_MULT, {a, b}),
|
|
solver.mkFiniteFieldElem("-1", f5)}),
|
|
z});
|
|
Term aIsTwo = solver.mkTerm(
|
|
EQUAL,
|
|
{solver.mkTerm(FINITE_FIELD_ADD, {a, solver.mkFiniteFieldElem("-2", f5)}),
|
|
z});
|
|
// ab - 1 = 0
|
|
solver.assertFormula(inv);
|
|
// a = 2
|
|
solver.assertFormula(aIsTwo);
|
|
|
|
// should be SAT, with b = 2^(-1)
|
|
Result r = solver.checkSat();
|
|
assert(r.isSat());
|
|
|
|
cout << "a = " << solver.getValue(a) << endl;
|
|
cout << "b = " << solver.getValue(b) << endl;
|
|
|
|
// b = 2
|
|
Term bIsTwo = solver.mkTerm(
|
|
EQUAL,
|
|
{solver.mkTerm(FINITE_FIELD_ADD, {b, solver.mkFiniteFieldElem("-2", f5)}),
|
|
z});
|
|
|
|
// should be UNSAT, 2*2 - 1 != 0
|
|
solver.assertFormula(bIsTwo);
|
|
|
|
r = solver.checkSat();
|
|
assert(!r.isSat());
|
|
}
|