From 643a673c6206f158297a4d7b63a2f2f61e61deb8 Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 30 Nov 2012 18:30:37 +0000 Subject: [PATCH] Changes to SExpr to accept autoconversion from bool and const char*. Adding an example for combination. --- examples/api/Makefile.am | 8 +++- examples/api/combination.cpp | 85 +++++++++++++++++++++++++++++++++++ examples/api/linear_arith.cpp | 13 +++--- src/util/sexpr.h | 65 +++++++++++++++++++++++++++ 4 files changed, 164 insertions(+), 7 deletions(-) create mode 100644 examples/api/combination.cpp 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 + +//#include // 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 @@ -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; diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 7f56319fa..135a83c7e 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -12,6 +12,13 @@ ** \brief Simple representation of S-expressions ** ** Simple representation of S-expressions. + ** These are used when a simple, and obvious interface for basic + ** expressions is appropraite. + ** + ** These are quite ineffecient. + ** These are totally disconnected from any ExprManager. + ** These keep unique copies of all of their children. + ** These are VERY overly verbose and keep much more data than is needed. **/ #include "cvc4_public.h" @@ -80,6 +87,38 @@ public: d_children() { } + SExpr(int value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children() { + } + + SExpr(long int value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children() { + } + + SExpr(unsigned int value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children() { + } + + SExpr(unsigned long int value) : + d_sexprType(SEXPR_INTEGER), + d_integerValue(value), + d_rationalValue(0), + d_stringValue(""), + d_children() { + } + SExpr(const CVC4::Rational& value) : d_sexprType(SEXPR_RATIONAL), d_integerValue(0), @@ -96,6 +135,32 @@ public: d_children() { } + /** + * This constructs a string expression from a const char* value. + * This cannot be removed in order to support SExpr("foo"). + * Given the other constructors this SExpr("foo") converts to bool. + * instead of SExpr(string("foo")). + */ + SExpr(const char* value) : + d_sexprType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value), + d_children() { + } + + /** + * This adds a convenience wrapper to SExpr to cast from bools. + * This is internally handled as the strings "true" and "false" + */ + SExpr(bool value) : + d_sexprType(SEXPR_STRING), + d_integerValue(0), + d_rationalValue(0), + d_stringValue(value ? "true" : "false"), + d_children() { + } + SExpr(const Keyword& value) : d_sexprType(SEXPR_KEYWORD), d_integerValue(0), -- 2.30.2