mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
01061af730
mkFunctionSort that takes two sorts as arguments is redundant, because the first argument is equivalent to a vector of size one passed to the other overload of mkFunctionSort. This commit removes the method from the C++ API but keeps the existing semantics for the Java and Python bindings for convenience and consistency with, e.g. mkTerm.
137 lines
4.2 KiB
C++
137 lines
4.2 KiB
C++
/******************************************************************************
|
|
* Top contributors (to current version):
|
|
* Aina Niemetz, Tim King, Mudathir Mohamed
|
|
*
|
|
* This file is part of the cvc5 project.
|
|
*
|
|
* Copyright (c) 2009-2021 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.
|
|
* ****************************************************************************
|
|
*
|
|
* A simple demonstration of the capabilities of cvc5
|
|
*
|
|
* A simple demonstration of how to use uninterpreted functions, combining this
|
|
* with arithmetic, and extracting a model at the end of a satisfiable query.
|
|
* The model is displayed using getValue().
|
|
*/
|
|
|
|
#include <cvc5/cvc5.h>
|
|
|
|
#include <iostream>
|
|
|
|
using namespace std;
|
|
using namespace cvc5;
|
|
|
|
void prefixPrintGetValue(Solver& slv, Term t, int level = 0)
|
|
{
|
|
cout << "slv.getValue(" << t << "): " << slv.getValue(t) << endl;
|
|
|
|
for (const Term& c : t)
|
|
{
|
|
prefixPrintGetValue(slv, c, level + 1);
|
|
}
|
|
}
|
|
|
|
int main()
|
|
{
|
|
Solver slv;
|
|
slv.setOption("produce-models", "true"); // Produce Models
|
|
slv.setOption("dag-thresh", "0"); // Disable dagifying the output
|
|
slv.setOption("output-language", "smt2"); // use smt-lib v2 as output language
|
|
slv.setLogic(string("QF_UFLIRA"));
|
|
|
|
// Sorts
|
|
Sort u = slv.mkUninterpretedSort("u");
|
|
Sort integer = slv.getIntegerSort();
|
|
Sort boolean = slv.getBooleanSort();
|
|
Sort uToInt = slv.mkFunctionSort({u}, integer);
|
|
Sort intPred = slv.mkFunctionSort({integer}, boolean);
|
|
|
|
// Variables
|
|
Term x = slv.mkConst(u, "x");
|
|
Term y = slv.mkConst(u, "y");
|
|
|
|
// Functions
|
|
Term f = slv.mkConst(uToInt, "f");
|
|
Term p = slv.mkConst(intPred, "p");
|
|
|
|
// Constants
|
|
Term zero = slv.mkInteger(0);
|
|
Term one = slv.mkInteger(1);
|
|
|
|
// Terms
|
|
Term f_x = slv.mkTerm(APPLY_UF, {f, x});
|
|
Term f_y = slv.mkTerm(APPLY_UF, {f, y});
|
|
Term sum = slv.mkTerm(ADD, {f_x, f_y});
|
|
Term p_0 = slv.mkTerm(APPLY_UF, {p, zero});
|
|
Term p_f_y = slv.mkTerm(APPLY_UF, {p, f_y});
|
|
|
|
// Construct the assertions
|
|
Term assertions =
|
|
slv.mkTerm(AND,
|
|
{
|
|
slv.mkTerm(LEQ, {zero, f_x}), // 0 <= f(x)
|
|
slv.mkTerm(LEQ, {zero, f_y}), // 0 <= f(y)
|
|
slv.mkTerm(LEQ, {sum, one}), // f(x) + f(y) <= 1
|
|
p_0.notTerm(), // not p(0)
|
|
p_f_y // p(f(y))
|
|
});
|
|
slv.assertFormula(assertions);
|
|
|
|
cout << "Given the following assertions:" << endl
|
|
<< assertions << endl << endl;
|
|
|
|
cout << "Prove x /= y is entailed. " << endl
|
|
<< "cvc5: " << slv.checkSatAssuming(slv.mkTerm(EQUAL, {x, y})) << "."
|
|
<< endl
|
|
<< endl;
|
|
|
|
cout << "Call checkSat to show that the assertions are satisfiable. "
|
|
<< endl
|
|
<< "cvc5: "
|
|
<< slv.checkSat() << "."<< endl << endl;
|
|
|
|
cout << "Call slv.getValue(...) on terms of interest."
|
|
<< endl;
|
|
cout << "slv.getValue(" << f_x << "): " << slv.getValue(f_x) << endl;
|
|
cout << "slv.getValue(" << f_y << "): " << slv.getValue(f_y) << endl;
|
|
cout << "slv.getValue(" << sum << "): " << slv.getValue(sum) << endl;
|
|
cout << "slv.getValue(" << p_0 << "): " << slv.getValue(p_0) << endl;
|
|
cout << "slv.getValue(" << p_f_y << "): " << slv.getValue(p_f_y)
|
|
<< endl << endl;
|
|
|
|
cout << "Alternatively, iterate over assertions and call slv.getValue(...) "
|
|
<< "on all terms."
|
|
<< endl;
|
|
prefixPrintGetValue(slv, assertions);
|
|
|
|
cout << endl;
|
|
cout << "You can also use nested loops to iterate over terms." << endl;
|
|
for (Term::const_iterator it = assertions.begin();
|
|
it != assertions.end();
|
|
++it)
|
|
{
|
|
cout << "term: " << *it << endl;
|
|
for (Term::const_iterator it2 = (*it).begin();
|
|
it2 != (*it).end();
|
|
++it2)
|
|
{
|
|
cout << " + child: " << *it2 << std::endl;
|
|
}
|
|
}
|
|
cout << endl;
|
|
cout << "Alternatively, you can also use for-each loops." << endl;
|
|
for (const Term& t : assertions)
|
|
{
|
|
cout << "term: " << t << endl;
|
|
for (const Term& c : t)
|
|
{
|
|
cout << " + child: " << c << endl;
|
|
}
|
|
}
|
|
|
|
return 0;
|
|
}
|