diff options
Diffstat (limited to 'examples/api/linear_arith-new.cpp')
-rw-r--r-- | examples/api/linear_arith-new.cpp | 85 |
1 files changed, 85 insertions, 0 deletions
diff --git a/examples/api/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp new file mode 100644 index 000000000..ef8faade9 --- /dev/null +++ b/examples/api/linear_arith-new.cpp @@ -0,0 +1,85 @@ +/********************* */ +/*! \file linear_arith.cpp + ** \verbatim + ** Top contributors (to current version): + ** Tim King, Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 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.\endverbatim + ** + ** \brief A simple demonstration of the linear arithmetic capabilities of CVC4 + ** + ** A simple demonstration of the linear arithmetic solving capabilities and + ** the push pop of CVC4. This also gives an example option. + **/ + +#include <iostream> + +//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "api/cvc4cpp.h" + +using namespace std; +using namespace CVC4::api; + +int main() +{ + Solver slv; + slv.setLogic("QF_LIRA"); // Set the logic + + // Prove that if given x (Integer) and y (Real) then + // the maximum value of y - x is 2/3 + + // Sorts + Sort real = slv.getRealSort(); + Sort integer = slv.getIntegerSort(); + + // Variables + Term x = slv.mkVar("x", integer); + Term y = slv.mkVar("y", real); + + // Constants + Term three = slv.mkInteger(3); + Term neg2 = slv.mkInteger(-2); + Term two_thirds = slv.mkReal(2, 3); + + // Terms + Term three_y = slv.mkTerm(MULT, three, y); + Term diff = slv.mkTerm(MINUS, y, x); + + // Formulas + Term x_geq_3y = slv.mkTerm(GEQ, x, three_y); + Term x_leq_y = slv.mkTerm(LEQ, x, y); + Term neg2_lt_x = slv.mkTerm(LT, neg2, x); + + Term assertions = + slv.mkTerm(AND, x_geq_3y, x_leq_y, neg2_lt_x); + + cout << "Given the assertions " << assertions << endl; + slv.assertFormula(assertions); + + + slv.push(); + Term diff_leq_two_thirds = slv.mkTerm(LEQ, diff, two_thirds); + cout << "Prove that " << diff_leq_two_thirds << " with CVC4." << endl; + cout << "CVC4 should report VALID." << endl; + cout << "Result from CVC4 is: " + << slv.checkValidAssuming(diff_leq_two_thirds) << endl; + slv.pop(); + + cout << endl; + + slv.push(); + Term diff_is_two_thirds = slv.mkTerm(EQUAL, diff, two_thirds); + slv.assertFormula(diff_is_two_thirds); + cout << "Show that the assertions are consistent with " << endl; + cout << diff_is_two_thirds << " with CVC4." << endl; + cout << "CVC4 should report SAT." << endl; + cout << "Result from CVC4 is: " << slv.checkSat() << endl; + slv.pop(); + + cout << "Thus the maximum value of (y - x) is 2/3."<< endl; + + return 0; +} |