diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-30 18:30:37 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-30 18:30:37 +0000 |
commit | 643a673c6206f158297a4d7b63a2f2f61e61deb8 (patch) | |
tree | 8b005ba86e36593b689ea44e464861ba583e910d /examples/api | |
parent | 8ebb053b1c8a43df8b8df21e31ed5a94cf0a53be (diff) |
Changes to SExpr to accept autoconversion from bool and const char*. Adding an example for combination.
Diffstat (limited to 'examples/api')
-rw-r--r-- | examples/api/Makefile.am | 8 | ||||
-rw-r--r-- | examples/api/combination.cpp | 85 | ||||
-rw-r--r-- | examples/api/linear_arith.cpp | 13 |
3 files changed, 99 insertions, 7 deletions
diff --git a/examples/api/Makefile.am b/examples/api/Makefile.am index 937a76d36..9e4e4470e 100644 --- a/examples/api/Makefile.am +++ b/examples/api/Makefile.am @@ -5,7 +5,8 @@ AM_CFLAGS = -Wall noinst_PROGRAMS = \ linear_arith \ - helloworld + helloworld \ + combination noinst_DATA = @@ -16,6 +17,11 @@ linear_arith_LDADD = \ @builddir@/../../src/libcvc4.la +combination_SOURCES = \ + combination.cpp +combination_LDADD = \ + @builddir@/../../src/libcvc4.la + helloworld_SOURCES = \ helloworld.cpp helloworld_LDADD = \ diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp new file mode 100644 index 000000000..f91e78ce6 --- /dev/null +++ b/examples/api/combination.cpp @@ -0,0 +1,85 @@ +/********************* */ +/*! \file combination.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief A simple demonstration of the capabilities of CVC4 + ** + ** A simple demonstration of how to use uninterpreted functions, combining this + ** with arithmetic, and extracting a model at the end of a satisfiable query. + **/ + +#include <iostream> + +//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed +#include "smt/smt_engine.h" + +using namespace std; +using namespace CVC4; + +int main() { + ExprManager em; + SmtEngine smt(&em); + smt.setOption("tlimit", 100); + smt.setOption("produce-models", true); // Produce Models + smt.setOption("incremental", true); // Produce Models + smt.setOption("output-language", "smtlib"); // output-language + + // Sorts + SortType u = em.mkSort("u"); + Type integer = em.integerType(); + Type boolean = em.booleanType(); + Type uToInt = em.mkFunctionType(u, integer); + Type intPred = em.mkFunctionType(integer, boolean); + + // Variables + Expr x = em.mkVar("x", u); + Expr y = em.mkVar("y", u); + + //Functions + Expr f = em.mkVar("f", uToInt); + Expr p = em.mkVar("p", intPred); + + // Constants + Expr zero = em.mkConst(Rational(0)); + Expr one = em.mkConst(Rational(1)); + + // terms + Expr f_x = em.mkExpr(kind::APPLY_UF, f, x); + Expr f_y = em.mkExpr(kind::APPLY_UF, f, y); + Expr sum = em.mkExpr(kind::PLUS, f_x, f_y); + Expr p_0 = em.mkExpr(kind::APPLY_UF, p, zero); + Expr p_f_y = em.mkExpr(kind::APPLY_UF, p, f_y); + + smt.assertFormula(em.mkExpr(kind::LEQ, zero, f_x)); // 0 <= f(x) + smt.assertFormula(em.mkExpr(kind::LEQ, zero, f_y)); // 0 <= f(y) + smt.assertFormula(em.mkExpr(kind::LEQ, sum, one)); // f(x) + f(y) <= 1 + smt.assertFormula(p_0.notExpr()); // not p(0) + smt.assertFormula(p_f_y); // p(f(y)) + + cout << "Under the assumptions, prove x cannot equal y is valid: " + << " CVC4 says " << smt.query(em.mkExpr(kind::DISTINCT, x, y)) << endl; + + cout << "Now we call checksat on a trivial query to show that" << endl + << "the assumptions are satisfiable: " + << smt.checkSat(em.mkConst(true)) << "."<< endl; + cout << smt.getValue(x) << endl; + cout << smt.getValue(y) << endl; + cout << smt.getValue(f_x) << endl; + cout << smt.getValue(f_y) << endl; + cout << smt.getValue(p_f_y) << endl; + cout << smt.getValue(p_0) << endl; + + cout << smt.getValue(f) << endl; + cout << smt.getValue(p) << endl; + + return 0; +} diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp index 27e7592ac..38a78b5ef 100644 --- a/examples/api/linear_arith.cpp +++ b/examples/api/linear_arith.cpp @@ -13,8 +13,8 @@ ** ** \brief A simple demonstration of the linear arithmetic capabilities of CVC4 ** - ** A simple demonstration of the linear real, integer and mixed real integer - ** solving 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> @@ -28,7 +28,7 @@ using namespace CVC4; int main() { ExprManager em; SmtEngine smt(&em); - smt.setOption("incremental", SExpr("true")); // Enable incremental solving + smt.setOption("incremental", true); // Enable incremental solving // Prove that if given x (Integer) and y (Real) then // the maximum value of y - x is 2/3 @@ -62,8 +62,8 @@ int main() { smt.assertFormula(assumptions); - Expr diff_leq_two_thirds = em.mkExpr(kind::LEQ, diff, two_thirds); smt.push(); + Expr diff_leq_two_thirds = em.mkExpr(kind::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: " << smt.query(diff_leq_two_thirds) << endl; @@ -71,12 +71,13 @@ int main() { cout << endl; - Expr diff_is_two_thirds = em.mkExpr(kind::EQUAL, diff, two_thirds); smt.push(); + Expr diff_is_two_thirds = em.mkExpr(kind::EQUAL, diff, two_thirds); + smt.assertFormula(diff_is_two_thirds); cout << "Show that the asserts are consistent with " << endl; cout << diff_is_two_thirds << " with CVC4." << endl; cout << "CVC4 should report SAT." << endl; - cout << "Result from CVC4 is: " << smt.checkSat(diff_is_two_thirds) << endl; + cout << "Result from CVC4 is: " << smt.checkSat(em.mkConst(true)) << endl; smt.pop(); cout << "Thus the maximum value of (y - x) is 2/3."<< endl; |