interfaces fixes and cleanups...and examples of each interface!

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