From: Tim King Date: Wed, 28 Nov 2012 22:59:58 +0000 (+0000) Subject: Adding the helloworld.cpp example. X-Git-Tag: cvc5-1.0.0~7535 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=91673d6cefa63bc0f706101946e0c01fcd429071;p=cvc5.git Adding the helloworld.cpp example. --- diff --git a/examples/Makefile.am b/examples/Makefile.am index a36480af7..d5d8534f4 100644 --- a/examples/Makefile.am +++ b/examples/Makefile.am @@ -1,4 +1,4 @@ -SUBDIRS = nra-translate hashsmt . +SUBDIRS = nra-translate hashsmt api . AM_CPPFLAGS = \ -I@srcdir@/../src/include -I@srcdir@/../src -I@builddir@/../src $(ANTLR_INCLUDES) @@ -6,8 +6,7 @@ AM_CXXFLAGS = -Wall AM_CFLAGS = -Wall noinst_PROGRAMS = \ - simple_vc_cxx \ - linear_arith + simple_vc_cxx if CVC4_BUILD_LIBCOMPAT noinst_PROGRAMS += \ @@ -29,11 +28,6 @@ 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 @@ -70,12 +64,10 @@ 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) diff --git a/examples/api/Makefile.am b/examples/api/Makefile.am new file mode 100644 index 000000000..937a76d36 --- /dev/null +++ b/examples/api/Makefile.am @@ -0,0 +1,26 @@ +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) diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp new file mode 100644 index 000000000..26b081a79 --- /dev/null +++ b/examples/api/helloworld.cpp @@ -0,0 +1,30 @@ +/********************* */ +/*! \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 +#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 // 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; +} diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp new file mode 100644 index 000000000..27e7592ac --- /dev/null +++ b/examples/api/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 + +//#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("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; +} diff --git a/examples/linear_arith.cpp b/examples/linear_arith.cpp deleted file mode 100644 index 27e7592ac..000000000 --- a/examples/linear_arith.cpp +++ /dev/null @@ -1,85 +0,0 @@ -/********************* */ -/*! \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 - -//#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("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; -}