diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-30 23:01:58 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-30 23:01:58 +0000 |
commit | 33e3657c15d6c760206aeaca10b5690af4a78223 (patch) | |
tree | a75475200584ab5e11981827182d979d84f6e1ff /examples | |
parent | 192c5592424e5db0afc72e7316c4698949a2f7e5 (diff) |
interfaces fixes and cleanups...and examples of each interface!
Diffstat (limited to 'examples')
-rw-r--r-- | examples/Makefile | 4 | ||||
-rw-r--r-- | examples/Makefile.am | 67 | ||||
-rw-r--r-- | examples/README | 12 | ||||
-rw-r--r-- | examples/SimpleVC.java | 73 | ||||
-rw-r--r-- | examples/SimpleVCCompat.java | 70 | ||||
-rw-r--r-- | examples/simple_vc_compat_c.c | 61 | ||||
-rw-r--r-- | examples/simple_vc_compat_cxx.cpp | 64 | ||||
-rw-r--r-- | examples/simple_vc_cxx.cpp | 61 |
8 files changed, 412 insertions, 0 deletions
diff --git a/examples/Makefile b/examples/Makefile new file mode 100644 index 000000000..3db5bc0ac --- /dev/null +++ b/examples/Makefile @@ -0,0 +1,4 @@ +topdir = .. +srcdir = examples + +include $(topdir)/Makefile.subdir diff --git a/examples/Makefile.am b/examples/Makefile.am new file mode 100644 index 000000000..8f120e14c --- /dev/null +++ b/examples/Makefile.am @@ -0,0 +1,67 @@ +AM_CPPFLAGS = \ + -I@srcdir@/../src/include -I@srcdir@/../src -I@builddir@/../src $(ANTLR_INCLUDES) +AM_CXXFLAGS = -Wall +AM_CFLAGS = -Wall + +noinst_PROGRAMS = \ + simple_vc_cxx + +if CVC4_BUILD_LIBCOMPAT +noinst_PROGRAMS += \ + simple_vc_compat_cxx +if CVC4_LANGUAGE_BINDING_C +noinst_PROGRAMS += \ + simple_vc_compat_c +endif +endif + +noinst_DATA = + +if CVC4_LANGUAGE_BINDING_JAVA +noinst_DATA += \ + SimpleVC.class +if CVC4_BUILD_LIBCOMPAT +noinst_DATA += \ + SimpleVCCompat.class +endif +endif + +simple_vc_cxx_SOURCES = \ + simple_vc_cxx.cpp +simple_vc_cxx_LDADD = \ + @builddir@/../src/parser/libcvc4parser.la \ + @builddir@/../src/libcvc4.la + +simple_vc_compat_cxx_SOURCES = \ + simple_vc_compat_cxx.cpp +simple_vc_compat_cxx_LDADD = \ + @builddir@/../src/compat/libcvc4compat.la \ + @builddir@/../src/parser/libcvc4parser.la \ + @builddir@/../src/libcvc4.la + +simple_vc_compat_c_SOURCES = \ + simple_vc_compat_c.c +simple_vc_compat_c_LDADD = \ + @builddir@/../src/bindings/compat/c/libcvc4bindings_c_compat.la + +SimpleVC.class: SimpleVC.java + $(AM_V_JAVAC)$(JAVAC) -classpath "@builddir@/../src/bindings/cvc4.jar" -d "@builddir@" $< +SimpleVCCompat.class: SimpleVCCompat.java + $(AM_V_JAVAC)$(JAVAC) -classpath "@builddir@/../src/bindings/compat/java/cvc4compat.jar" -d "@builddir@" $< + +if STATIC_BINARY +simple_vc_cxx_LINK = $(CXXLINK) -all-static +simple_vc_compat_cxx_LINK = $(CXXLINK) -all-static +simple_vc_compat_c_LINK = $(LINK) -all-static +else +simple_vc_cxx_LINK = $(CXXLINK) +simple_vc_compat_cxx_LINK = $(CXXLINK) +simple_vc_compat_c_LINK = $(LINK) +endif + +MOSTLYCLEANFILES = $(noinst_DATA) + +# for silent automake rules +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/README b/examples/README new file mode 100644 index 000000000..1ba0a54e6 --- /dev/null +++ b/examples/README @@ -0,0 +1,12 @@ +These are examples of how to use CVC4 with each of its in-memory, library +interfaces. They are essentially "hello world" examples, and do not +fully demonstrate the interfaces, but function as a starting point to +using simple expressions and solving functionality through each library. + +These examples are built as a separate step. After building CVC4, you +can make the examples by running "make" from inside the examples +directory. With the default configuration, you'll find them in +builds/examples in the top-level source directory (if you configured +your own build directory, you'll find them there). + +-- Morgan Deters <mdeters@cs.nyu.edu> Fri, 30 Sep 2011 16:19:46 -0400 diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java new file mode 100644 index 000000000..e6a667e16 --- /dev/null +++ b/examples/SimpleVC.java @@ -0,0 +1,73 @@ +/********************* */ +/*! \file SimpleVC.java + ** \verbatim + ** Original author: mdeters + ** 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 Java interface + ** + ** A simple demonstration of the Java interface. + ** + ** To run the resulting class file, you need to do something like the + ** following: + ** + ** java \ + ** -classpath path/to/cvc4.jar \ + ** -Djava.library.path=/dir/containing/libcvc4bindings_java.so \ + ** SimpleVC + ** + ** For example, if you are building CVC4 without specifying your own + ** build directory, the build process puts everything in builds/, and + ** you can run this example (after building it with "make") like this: + ** + ** java \ + ** -classpath builds/examples:builds/src/bindings/cvc4.jar \ + ** -Djava.library.path=builds/src/bindings/.libs \ + ** SimpleVC + **/ + +import edu.nyu.acsys.CVC4.*; +import edu.nyu.acsys.CVC4.Integer;// to override java.lang.Integer name lookup + +public class SimpleVC { + public static void main(String[] args) { + System.loadLibrary("cvc4bindings_java"); + + ExprManager em = new ExprManager(); + SmtEngine smt = new SmtEngine(em); + + // Prove that for integers x and y: + // x > 0 AND y > 0 => 2x + y >= 3 + + Type integer = em.integerType(); + + Expr x = em.mkVar("x", integer); + Expr y = em.mkVar("y", integer); + Expr zero = em.mkConst(new Integer(0)); + + Expr x_positive = em.mkExpr(Kind.GT, x, zero); + Expr y_positive = em.mkExpr(Kind.GT, y, zero); + + Expr two = em.mkConst(new Integer(2)); + Expr twox = em.mkExpr(Kind.MULT, two, x); + Expr twox_plus_y = em.mkExpr(Kind.PLUS, twox, y); + + Expr three = em.mkConst(new Integer(3)); + Expr twox_plus_y_geq_3 = em.mkExpr(Kind.GEQ, twox_plus_y, three); + + BoolExpr formula = + new BoolExpr(em.mkExpr(Kind.AND, x_positive, y_positive)). + impExpr(new BoolExpr(twox_plus_y_geq_3)); + + System.out.println("Checking validity of formula " + formula + " with CVC4."); + System.out.println("CVC4 should report VALID."); + System.out.println("Result from CVC4 is: " + smt.query(formula)); + } +} diff --git a/examples/SimpleVCCompat.java b/examples/SimpleVCCompat.java new file mode 100644 index 000000000..107b5504e --- /dev/null +++ b/examples/SimpleVCCompat.java @@ -0,0 +1,70 @@ +/********************* */ +/*! \file SimpleVCCompat.java + ** \verbatim + ** Original author: mdeters + ** 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 Java compatibility interface + ** (quite similar to the old CVC3 Java interface) + ** + ** A simple demonstration of the Java compatibility interface + ** (quite similar to the old CVC3 Java interface). + ** + ** To run the resulting class file, you need to do something like the + ** following: + ** + ** java \ + ** -classpath path/to/cvc4compat.jar \ + ** -Djava.library.path=/dir/containing/libcvc4bindings_java_compat.so \ + ** SimpleVCCompat + ** + ** For example, if you are building CVC4 without specifying your own + ** build directory, the build process puts everything in builds/, and + ** you can run this example (after building it with "make") like this: + ** + ** java \ + ** -classpath builds/examples:builds/src/bindings/compat/java/cvc4compat.jar \ + ** -Djava.library.path=builds/src/bindings/compat/java/.libs \ + ** SimpleVCCompat + **/ + +import cvc3.*; + +public class SimpleVCCompat { + public static void main(String[] args) { + ValidityChecker vc = ValidityChecker.create(); + + // Prove that for integers x and y: + // x > 0 AND y > 0 => 2x + y >= 3 + + Type integer = vc.intType(); + + Expr x = vc.varExpr("x", integer); + Expr y = vc.varExpr("y", integer); + Expr zero = vc.ratExpr(0); + + Expr x_positive = vc.gtExpr(x, zero); + Expr y_positive = vc.gtExpr(y, zero); + + Expr two = vc.ratExpr(2); + Expr twox = vc.multExpr(two, x); + Expr twox_plus_y = vc.plusExpr(twox, y); + + Expr three = vc.ratExpr(3); + Expr twox_plus_y_geq_3 = vc.geExpr(twox_plus_y, three); + + Expr formula = vc.impliesExpr(vc.andExpr(x_positive, y_positive), + twox_plus_y_geq_3); + + System.out.println("Checking validity of formula " + formula + " with CVC4."); + System.out.println("CVC4 should report VALID."); + System.out.println("Result from CVC4 is: " + vc.query(formula)); + } +} diff --git a/examples/simple_vc_compat_c.c b/examples/simple_vc_compat_c.c new file mode 100644 index 000000000..9bcb52280 --- /dev/null +++ b/examples/simple_vc_compat_c.c @@ -0,0 +1,61 @@ +/********************* */ +/*! \file simple_vc_compat_c.c + ** \verbatim + ** Original author: mdeters + ** 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 C compatibility interface + ** (quite similar to the old CVC3 C interface) + ** + ** A simple demonstration of the C compatibility interface + ** (quite similar to the old CVC3 C interface). + **/ + +#include <stdio.h> +#include <stdlib.h> + +// #include <cvc4/compat/c_interface.h> +#include "bindings/compat/c/c_interface.h" + +int main() { + VC vc = vc_createValidityChecker(NULL); + + // Prove that for integers x and y: + // x > 0 AND y > 0 => 2x + y >= 3 + + Type integer = vc_intType(vc); + + Expr x = vc_varExpr(vc, "x", integer); + Expr y = vc_varExpr(vc, "y", integer); + Expr zero = vc_ratExpr(vc, 0, 1); + + Expr x_positive = vc_gtExpr(vc, x, zero); + Expr y_positive = vc_gtExpr(vc, y, zero); + + Expr two = vc_ratExpr(vc, 2, 1); + Expr twox = vc_multExpr(vc, two, x); + Expr twox_plus_y = vc_plusExpr(vc, twox, y); + + Expr three = vc_ratExpr(vc, 3, 1); + Expr twox_plus_y_geq_3 = vc_geExpr(vc, twox_plus_y, three); + + Expr formula = vc_impliesExpr(vc, vc_andExpr(vc, x_positive, y_positive), + twox_plus_y_geq_3); + + char* formulaString = vc_printExprString(vc, formula); + + printf("Checking validity of formula %s with CVC4.\n", formulaString); + printf("CVC4 should return 1 (meaning VALID).\n"); + printf("Result from CVC4 is: %d\n", vc_query(vc, formula)); + + free(formulaString); + + return 0; +} diff --git a/examples/simple_vc_compat_cxx.cpp b/examples/simple_vc_compat_cxx.cpp new file mode 100644 index 000000000..c178d1aba --- /dev/null +++ b/examples/simple_vc_compat_cxx.cpp @@ -0,0 +1,64 @@ +/********************* */ +/*! \file simple_vc_compat_cxx.cpp + ** \verbatim + ** Original author: mdeters + ** 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 C++ compatibility interface + ** (quite similar to the old CVC3 C++ interface) + ** + ** A simple demonstration of the C++ compatibility interface (quite + ** similar to the old CVC3 C++ interface). Note that the library is + ** named "libcvc4compat," to mark it as being part of CVC4, but the + ** header file is "cvc3_compat.h" to indicate the similarity to the + ** CVC3 interface, and the namespace is "CVC3". CVC3::Expr and + ** CVC4::Expr are incompatible; to avoid confusion, it is best to not + ** include both the CVC3 and CVC4 interface headers. + **/ + +#include <iostream> + +// #include <cvc4/compat/cvc3_compat.h> +#include "compat/cvc3_compat.h" + +using namespace std; +using namespace CVC3; + +int main() { + ValidityChecker* vc = ValidityChecker::create(); + + // Prove that for integers x and y: + // x > 0 AND y > 0 => 2x + y >= 3 + + Type integer = vc->intType(); + + Expr x = vc->varExpr("x", integer); + Expr y = vc->varExpr("y", integer); + Expr zero = vc->ratExpr(0); + + Expr x_positive = vc->gtExpr(x, zero); + Expr y_positive = vc->gtExpr(y, zero); + + Expr two = vc->ratExpr(2); + Expr twox = vc->multExpr(two, x); + Expr twox_plus_y = vc->plusExpr(twox, y); + + Expr three = vc->ratExpr(3); + Expr twox_plus_y_geq_3 = vc->geExpr(twox_plus_y, three); + + Expr formula = vc->impliesExpr(vc->andExpr(x_positive, y_positive), + twox_plus_y_geq_3); + + cout << "Checking validity of formula " << formula << " with CVC4." << endl; + cout << "CVC4 should report VALID." << endl; + cout << "Result from CVC4 is: " << vc->query(formula) << endl; + + return 0; +} diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp new file mode 100644 index 000000000..3b5db7c02 --- /dev/null +++ b/examples/simple_vc_cxx.cpp @@ -0,0 +1,61 @@ +/********************* */ +/*! \file simple_vc_cxx.cpp + ** \verbatim + ** Original author: mdeters + ** 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 C++ interface + ** + ** A simple demonstration of the C++ interface. Compare to the Java + ** interface in SimpleVC.java; they are virtually line-by-line + ** identical. + **/ + +#include <iostream> + +//#include <cvc4.h> +#include "smt/smt_engine.h" + +using namespace std; +using namespace CVC4; + +int main() { + ExprManager em; + SmtEngine smt(&em); + + // Prove that for integers x and y: + // x > 0 AND y > 0 => 2x + y >= 3 + + Type integer = em.integerType(); + + Expr x = em.mkVar("x", integer); + Expr y = em.mkVar("y", integer); + Expr zero = em.mkConst(Integer(0)); + + Expr x_positive = em.mkExpr(kind::GT, x, zero); + Expr y_positive = em.mkExpr(kind::GT, y, zero); + + Expr two = em.mkConst(Integer(2)); + Expr twox = em.mkExpr(kind::MULT, two, x); + Expr twox_plus_y = em.mkExpr(kind::PLUS, twox, y); + + Expr three = em.mkConst(Integer(3)); + Expr twox_plus_y_geq_3 = em.mkExpr(kind::GEQ, twox_plus_y, three); + + BoolExpr formula = + BoolExpr(em.mkExpr(kind::AND, x_positive, y_positive)). + impExpr(BoolExpr(twox_plus_y_geq_3)); + + cout << "Checking validity of formula " << formula << " with CVC4." << endl; + cout << "CVC4 should report VALID." << endl; + cout << "Result from CVC4 is: " << smt.query(formula) << endl; + + return 0; +} |