Adding an example to show how to use arithmetic.

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;
+}