-SUBDIRS = nra-translate hashsmt .
+SUBDIRS = nra-translate hashsmt api .
AM_CPPFLAGS = \
-I@srcdir@/../src/include -I@srcdir@/../src -I@builddir@/../src $(ANTLR_INCLUDES)
AM_CFLAGS = -Wall
noinst_PROGRAMS = \
- simple_vc_cxx \
- linear_arith
+ simple_vc_cxx
if CVC4_BUILD_LIBCOMPAT
noinst_PROGRAMS += \
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
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)
--- /dev/null
+AM_CPPFLAGS = \
+ -I@srcdir@/../../src/include -I@srcdir@/../../src -I@builddir@/../../src $(ANTLR_INCLUDES)
+AM_CXXFLAGS = -Wall
+AM_CFLAGS = -Wall
+
+noinst_PROGRAMS = \
+ linear_arith \
+ helloworld
+
+
+noinst_DATA =
+
+linear_arith_SOURCES = \
+ linear_arith.cpp
+linear_arith_LDADD = \
+ @builddir@/../../src/libcvc4.la
+
+
+helloworld_SOURCES = \
+ helloworld.cpp
+helloworld_LDADD = \
+ @builddir@/../../src/libcvc4.la
+
+# for installation
+examplesdir = $(docdir)/$(subdir)
+examples_DATA = $(DIST_SOURCES) $(EXTRA_DIST)
--- /dev/null
+/********************* */
+/*! \file helloworld.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 very simple CVC4 example
+ **
+ ** A very simple CVC4 tutorial example.
+ **/
+
+#include <iostream>
+#warning "To use helloworld.cpp as given in the wiki, instead of make examples, change the following two includes lines."
+#include "smt/smt_engine.h" // for use with make examples
+//#include <cvc4/cvc4.h> // To follow the wiki
+using namespace CVC4;
+int main() {
+ ExprManager em;
+ Expr helloworld = em.mkVar("Hello World!", em.booleanType());
+ SmtEngine smt(&em);
+ std::cout << helloworld << " is " << smt.query(helloworld) << std::endl;
+ return 0;
+}
--- /dev/null
+/********************* */
+/*! \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;
+}
+++ /dev/null
-/********************* */
-/*! \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;
-}
projects / cvc5.git / commitdiff