summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--examples/api/Makefile.am8
-rw-r--r--examples/api/combination.cpp85
-rw-r--r--examples/api/linear_arith.cpp13
-rw-r--r--src/util/sexpr.h65
4 files changed, 164 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;
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),
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback