diff options
author | Tim King <taking@cs.nyu.edu> | 2012-11-27 01:39:58 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-11-27 01:39:58 +0000 |
commit | 3da16da97df7cd2efd4b113db3bfef8b9c138ebe (patch) | |
tree | cd88a2861329bdd7888684e5d2775c0c8f47b67f /examples | |
parent | 1e4c37a3ef7b1c16914b181c189716aa4a3df6b8 (diff) |
Adding an example to show how to use arithmetic.
Diffstat (limited to 'examples')
-rw-r--r-- | examples/Makefile.am | 12 | ||||
-rw-r--r-- | examples/linear_arith.cpp | 85 |
2 files changed, 96 insertions, 1 deletions
diff --git a/examples/Makefile.am b/examples/Makefile.am index 19c460c92..a36480af7 100644 --- a/examples/Makefile.am +++ b/examples/Makefile.am @@ -6,7 +6,8 @@ AM_CXXFLAGS = -Wall AM_CFLAGS = -Wall noinst_PROGRAMS = \ - simple_vc_cxx + simple_vc_cxx \ + linear_arith if CVC4_BUILD_LIBCOMPAT noinst_PROGRAMS += \ @@ -28,6 +29,12 @@ noinst_DATA += \ endif endif +linear_arith_SOURCES = \ + linear_arith.cpp +linear_arith_LDADD = \ + @builddir@/../src/parser/libcvc4parser.la \ + @builddir@/../src/libcvc4.la + simple_vc_cxx_SOURCES = \ simple_vc_cxx.cpp simple_vc_cxx_LDADD = \ @@ -63,10 +70,12 @@ EXTRA_DIST = \ README if STATIC_BINARY +linear_arith_LINK = $(CXXLINK) -all-static simple_vc_cxx_LINK = $(CXXLINK) -all-static simple_vc_compat_cxx_LINK = $(CXXLINK) -all-static simple_vc_compat_c_LINK = $(LINK) -all-static else +linear_arith_LINK = $(CXXLINK) simple_vc_cxx_LINK = $(CXXLINK) simple_vc_compat_cxx_LINK = $(CXXLINK) simple_vc_compat_c_LINK = $(LINK) @@ -82,3 +91,4 @@ MOSTLYCLEANFILES = $(noinst_DATA) AM_V_JAVAC = $(am__v_JAVAC_$(V)) am__v_JAVAC_ = $(am__v_JAVAC_$(AM_DEFAULT_VERBOSITY)) am__v_JAVAC_0 = @echo " JAVAC " $@; + diff --git a/examples/linear_arith.cpp b/examples/linear_arith.cpp new file mode 100644 index 000000000..27e7592ac --- /dev/null +++ b/examples/linear_arith.cpp @@ -0,0 +1,85 @@ +/********************* */ +/*! \file linear_arith.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 linear arithmetic capabilities of CVC4 + ** + ** A simple demonstration of the linear real, integer and mixed real integer + ** solving capabilities of CVC4. + **/ + +#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("incremental", SExpr("true")); // Enable incremental solving + + // Prove that if given x (Integer) and y (Real) then + // the maximum value of y - x is 2/3 + + // Types + Type real = em.realType(); + Type integer = em.integerType(); + + // Variables + Expr x = em.mkVar("x", integer); + Expr y = em.mkVar("y", real); + + // Constants + Expr three = em.mkConst(Rational(3)); + Expr neg2 = em.mkConst(Rational(-2)); + Expr two_thirds = em.mkConst(Rational(2,3)); + + // Terms + Expr three_y = em.mkExpr(kind::MULT, three, y); + Expr diff = em.mkExpr(kind::MINUS, y, x); + + // Formulas + Expr x_geq_3y = em.mkExpr(kind::GEQ, x, three_y); + Expr x_leq_y = em.mkExpr(kind::LEQ, x, y); + Expr neg2_lt_x = em.mkExpr(kind::LT, neg2, x); + + Expr assumptions = + em.mkExpr(kind::AND, x_geq_3y, x_leq_y, neg2_lt_x); + + cout << "Given the assumptions " << assumptions << endl; + smt.assertFormula(assumptions); + + + Expr diff_leq_two_thirds = em.mkExpr(kind::LEQ, diff, two_thirds); + smt.push(); + 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; + smt.pop(); + + cout << endl; + + Expr diff_is_two_thirds = em.mkExpr(kind::EQUAL, diff, two_thirds); + smt.push(); + 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; + smt.pop(); + + cout << "Thus the maximum value of (y - x) is 2/3."<< endl; + + return 0; +} |