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

23 files changed, 497 insertions, 35 deletions

diff --git a/Makefile b/Makefile
index 6f7356ad7..7f272b668 100644
--- a/Makefile
+++ b/Makefile
@@ -27,6 +27,10 @@ test: check
 .PHONY: doc
 doc: doc-builds
 
+.PHONY: examples
+examples: all
+	(cd examples && $(MAKE) $(AM_MAKEFLAGS))
+
 YEAR := $(shell date +%Y)
 submission:
 	if [ ! -e configure ]; then ./autogen.sh; fi
diff --git a/Makefile.am b/Makefile.am
index d2b11fe9c..db74bd378 100644
--- a/Makefile.am
+++ b/Makefile.am
@@ -6,6 +6,11 @@ AUTOMAKE_OPTIONS = foreign
 ACLOCAL_AMFLAGS = -I config
 
 SUBDIRS = src test contrib
+DIST_SUBDIRS = $(SUBDIRS) examples
+
+.PHONY: examples
+examples: all
+	(cd examples && $(MAKE) $(AM_MAKEFLAGS))
 
 .PHONY: units systemtests regress regress0 regress1 regress2 regress3
 systemtests regress regress0 regress1 regress2 regress3: all
@@ -32,8 +37,8 @@ if COVERAGE_ENABLED
 # work...)
 lcov: all
 	$(LCOV) -z -d .
-	$(MAKE) check -C src
-	+$(MAKE) check -C test/unit
+	(cd src && $(MAKE) $(AM_MAKEFLAGS) check)
+	+(cd test/unit && $(MAKE) $(AM_MAKEFLAGS) check)
 	$(LCOV) -c -d . -t cvc4_units -o cvc4-coverage-full.info
 	$(LCOV) -o cvc4-coverage.info -r cvc4-coverage-full.info $(LCOV_EXCLUDES)
 	mkdir -p "@top_srcdir@/html"
@@ -44,8 +49,8 @@ lcov: all
 
 lcov-all: all
 	$(LCOV) -z -d .
-	$(MAKE) check -C src
-	+$(MAKE) check -C test
+	(cd src && $(MAKE) $(AM_MAKEFLAGS) check)
+	+(cd test && $(MAKE) $(AM_MAKEFLAGS) check)
 	$(LCOV) -c -d . -t cvc4_units -o cvc4-coverage-full.info
 	$(LCOV) -o cvc4-coverage.info -r cvc4-coverage-full.info $(LCOV_EXCLUDES)
 	mkdir -p "@top_srcdir@/html"
@@ -62,10 +67,10 @@ lcov18: all
 		echo; echo "=== Collecting coverage data from $$testtype unit tests ==="; \
 		echo $(LCOV) -z -d .; \
 		$(LCOV) -z -d . || exit 1; \
-		echo $(MAKE) check -C src || exit 1; \
-		$(MAKE) check -C src || exit 1; \
-		echo $(MAKE) check -C test/unit TEST_SUFFIX=_$$testtype || exit 1; \
-		$(MAKE) check -C test/unit TEST_SUFFIX=_$$testtype || exit 1; \
+		echo "(cd src && $(MAKE) $(AM_MAKEFLAGS) check) || exit 1"; \
+		(cd src && $(MAKE) $(AM_MAKEFLAGS) check) || exit 1; \
+		echo "(cd test/unit && $(MAKE) $(AM_MAKEFLAGS) check TEST_SUFFIX=_$$testtype) || exit 1"; \
+		(cd test/unit && $(MAKE) $(AM_MAKEFLAGS) check TEST_SUFFIX=_$$testtype) || exit 1; \
 		echo $(LCOV) -c -d . -t $$testtype -o cvc4-coverage-$$testtype-full.info || exit 1; \
 		$(LCOV) -c -d . -t $$testtype -o cvc4-coverage-$$testtype-full.info || exit 1; \
 		echo $(LCOV) -o cvc4-coverage-$$testtype.info -r cvc4-coverage-$$testtype-full.info $(LCOV_EXCLUDES); \
diff --git a/Makefile.builds.in b/Makefile.builds.in
index 7d2e8586b..21d172623 100644
--- a/Makefile.builds.in
+++ b/Makefile.builds.in
@@ -121,6 +121,7 @@ endif
 #	set up builds/bin and builds/lib
 	test -e lib || ln -sfv ".$(libdir)" lib
 	test -e bin || ln -sfv ".$(bindir)" bin
+	rm -f examples; ln -sf "$(CURRENT_BUILD)/examples" examples
 
 # The descent into "src" with target "check" is to build check
 # prerequisites (e.g. CHECK_PROGRAMS, CHECK_LTLIBRARIES, ...).
diff --git a/configure.ac b/configure.ac
index ea7d4f7ae..b2badafbb 100644
--- a/configure.ac
+++ b/configure.ac
@@ -954,7 +954,7 @@ AC_SUBST(MAN_DATE)
 AC_CONFIG_FILES([
   Makefile.builds
   Makefile]
-  m4_esyscmd([find contrib src test -name Makefile.am | sort | sed 's,\.am$,,'])
+  m4_esyscmd([find contrib src test examples -name Makefile.am | sort | sed 's,\.am$,,'])
 )
 
 CVC4_CONFIG_FILE_ONLY_IF_CHANGED([src/util/rational.h])
diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl
index 397f1426b..7ad839b1d 100755
--- a/contrib/update-copyright.pl
+++ b/contrib/update-copyright.pl
@@ -33,9 +33,7 @@
 #
 
 my $excluded_directories = '^(minisat|CVS|generated)$';
-# re-include bounded_token_buffer.{h,cpp}
-#my $excluded_paths = '^(src/parser/bounded_token_buffer\.(h|cpp))|(src/parser/antlr_input_imports.cpp)$';
-my $excluded_paths = '^src/parser/antlr_input_imports.cpp$';
+my $excluded_paths = '^(src/parser/antlr_input_imports.cpp|src/bindings/compat/.*)$';
 
 # Years of copyright for the template.  E.g., the string
 # "1985, 1987, 1992, 1997, 2008" or "2006-2009" or whatever.
@@ -135,7 +133,7 @@ while($#searchdirs >= 0) {
 
 sub handleFile {
   my ($srcdir, $file) = @_;
-  return if !($file =~ /\.(c|cc|cpp|C|h|hh|hpp|H|y|yy|ypp|Y|l|ll|lpp|L|g)$/);
+  return if !($file =~ /\.(c|cc|cpp|C|h|hh|hpp|H|y|yy|ypp|Y|l|ll|lpp|L|g|java)$/);
   return if ($srcdir.'/'.$file) =~ /$excluded_paths/;
   return if $modonly  &&`svn status "$srcdir/$file" 2>/dev/null` !~ /^M/;
   print "$srcdir/$file...";
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;
+}
diff --git a/src/Makefile.am b/src/Makefile.am
index 5b245d303..63fcf590d 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -63,6 +63,7 @@ EXTRA_DIST = \
 	include/cvc4parser_public.h \
 	include/cvc4_private.h \
 	include/cvc4_public.h \
+	include/cvc4.h \
 	cvc4.i
 
 subversion_versioninfo.cpp: svninfo
@@ -94,7 +95,8 @@ svninfo.tmp:
 	$(AM_V_GEN)(cd "$(top_srcdir)" && svn info && echo "Modifications: `test -z \"\`svn status -q\`\" && echo false || echo true`") >"$@" 2>/dev/null || true
 
 install-data-local:
-	(echo include/cvc4_public.h; \
+	(echo include/cvc4.h; \
+	 echo include/cvc4_public.h; \
 	 find * -name '*.h' | \
 		xargs grep -l '^# *include  *"cvc4.*_public\.h"'; \
 	(cd "$(srcdir)" && find * -name '*.h' | \
@@ -115,7 +117,8 @@ install-data-local:
 	done
 
 uninstall-local:
-	-(echo include/cvc4_public.h; \
+	-(echo include/cvc4.h; \
+	  echo include/cvc4_public.h; \
 	  find * -name '*.h' | \
 		xargs grep -l '^# *include  *"cvc4.*_public\.h"'; \
 	(cd "$(srcdir)" && find * -name '*.h' | \
diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index 2552e39d6..f9420dbdb 100644
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -15,7 +15,7 @@ LIBCVC4BINDINGS_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4BINDINGSLIB \
 	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
-AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
+AM_CXXFLAGS = -Wall
 
 SUBDIRS = . compat
 
diff --git a/src/bindings/compat/Makefile.am b/src/bindings/compat/Makefile.am
index e5ea3b399..2aa714458 100644
--- a/src/bindings/compat/Makefile.am
+++ b/src/bindings/compat/Makefile.am
@@ -1,7 +1,7 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4BINDINGSLIB \
 	-I@srcdir@/../../include -I@srcdir@/../.. -I@builddir@/../..
-AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
+AM_CXXFLAGS = -Wall
 
 if CVC4_BUILD_LIBCOMPAT
 SUBDIRS = c java
diff --git a/src/bindings/compat/c/Makefile.am b/src/bindings/compat/c/Makefile.am
index ceabe16db..c7298a927 100644
--- a/src/bindings/compat/c/Makefile.am
+++ b/src/bindings/compat/c/Makefile.am
@@ -15,7 +15,7 @@ LIBCVC4BINDINGS_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4BINDINGSLIB \
 	-I@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../..
-AM_CXXFLAGS = -Wall -Wno-return-type $(FLAG_VISIBILITY_HIDDEN)
+AM_CXXFLAGS = -Wall -Wno-return-type
 
 lib_LTLIBRARIES =
 
diff --git a/src/bindings/compat/java/Makefile.am b/src/bindings/compat/java/Makefile.am
index 25765f0f0..14701ebb3 100644
--- a/src/bindings/compat/java/Makefile.am
+++ b/src/bindings/compat/java/Makefile.am
@@ -15,7 +15,7 @@ LIBCVC4BINDINGS_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4BINDINGSLIB \
 	-I@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../.. -I@builddir@/cvc3
-AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
+AM_CXXFLAGS = -Wall
 
 lib_LTLIBRARIES =
 data_DATA =
diff --git a/src/bindings/compat/java/src/cvc3/Embedded.java b/src/bindings/compat/java/src/cvc3/Embedded.java
index 87d67d743..c645f2655 100644
--- a/src/bindings/compat/java/src/cvc3/Embedded.java
+++ b/src/bindings/compat/java/src/cvc3/Embedded.java
@@ -12,7 +12,7 @@ public abstract class Embedded {
 
     // load jni c++ library
     static {
-    	System.loadLibrary("cvc3jni");
+        System.loadLibrary("cvc4bindings_java_compat");
 
 	/*
 	// for debugging: stop here by waiting for a key press,
diff --git a/src/compat/Makefile.am b/src/compat/Makefile.am
index 936a63559..a79301c18 100644
--- a/src/compat/Makefile.am
+++ b/src/compat/Makefile.am
@@ -15,7 +15,7 @@ LIBCVC4COMPAT_VERSION = @CVC4_COMPAT_LIBRARY_VERSION@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4COMPATLIB \
 	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. $(ANTLR_INCLUDES)
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas
 
 if CVC4_BUILD_LIBCOMPAT
 
@@ -40,10 +40,12 @@ libcvc4compat_noinst_la_LIBADD = \
 libcvc4compat_la_SOURCES = \
 	cvc3_compat.h \
 	cvc3_compat.cpp
+libcvc4compat_la_CXXFLAGS = -fno-strict-aliasing
 
 libcvc4compat_noinst_la_SOURCES = \
 	cvc3_compat.h \
 	cvc3_compat.cpp
+libcvc4compat_noinst_la_CXXFLAGS = -fno-strict-aliasing
 
 else
 
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 739da614a..90d0942b4 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -3,3 +3,8 @@
 %}
 
 %include "expr/expr_manager.h"
+
+%template(mkConst) CVC4::ExprManager::mkConst< CVC4::Integer >;
+%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Rational>;
+
+%include "expr/expr_manager.h"
diff --git a/src/include/cvc4.h b/src/include/cvc4.h
new file mode 100644
index 000000000..cfe11fb82
--- /dev/null
+++ b/src/include/cvc4.h
@@ -0,0 +1,39 @@
+/*********************                                                        */
+/*! \file cvc4.h
+ ** \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 Main header file for CVC4 library functionality
+ **
+ ** Main header file for CVC4 library functionality.  Includes the
+ ** most-commonly used CVC4 public-facing class interfaces.
+ **/
+
+#ifndef __CVC4__CVC4_H
+#define __CVC4__CVC4_H
+
+#include <cvc4/smt/smt_engine.h>
+
+#include <cvc4/expr/expr_manager.h>
+#include <cvc4/expr/expr.h>
+#include <cvc4/expr/command.h>
+
+#include <cvc4/util/datatype.h>
+#include <cvc4/util/integer.h>
+#include <cvc4/util/rational.h>
+#include <cvc4/util/exception.h>
+#include <cvc4/util/options.h>
+#include <cvc4/util/configuration.h>
+
+#include <cvc4/parser/parser.h>
+#include <cvc4/parser/parser_builder.h>
+
+#endif /* __CVC4__CVC4_H */
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 6b79a84bf..38dcf12c9 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -123,7 +123,7 @@ static const string optionsDescription = "\
    --print-expr-types     print types with variables when printing exprs\n\
    --interactive          run interactively\n\
    --no-interactive       do not run interactively\n\
-   --produce-models       support the get-value command\n\
+   --produce-models | -m  support the get-value command\n\
    --produce-assignments  support the get-assignment command\n\
    --lazy-definition-expansion expand define-fun lazily\n\
    --simplification=MODE  choose simplification mode, see --simplification=help\n\
@@ -138,7 +138,7 @@ static const string optionsDescription = "\
    --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\
    --disable-arithmetic-propagation turns on arithmetic propagation\n\
    --disable-symmetry-breaker turns off UF symmetry breaker (Deharbe et al., CADE 2011)\n\
-   --incremental          enable incremental solving\n";
+   --incremental | -i     enable incremental solving\n";
 
 static const string languageDescription = "\
 Languages currently supported as arguments to the -L / --lang option:\n\
@@ -281,12 +281,10 @@ enum OptionValue {
   NO_STATIC_LEARNING,
   INTERACTIVE,
   NO_INTERACTIVE,
-  PRODUCE_MODELS,
   PRODUCE_ASSIGNMENTS,
   NO_TYPE_CHECKING,
   LAZY_TYPE_CHECKING,
   EAGER_TYPE_CHECKING,
-  INCREMENTAL,
   REPLAY,
   REPLAY_LOG,
   PIVOT_RULE,
@@ -355,19 +353,14 @@ static struct option cmdlineOptions[] = {
   { "no-static-learning", no_argument, NULL, NO_STATIC_LEARNING },
   { "interactive", no_argument      , NULL, INTERACTIVE },
   { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
-  { "produce-models", no_argument   , NULL, PRODUCE_MODELS },
+  { "produce-models", no_argument   , NULL, 'm' },
   { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS },
   { "no-type-checking", no_argument , NULL, NO_TYPE_CHECKING },
   { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING },
   { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING },
-  { "incremental", no_argument      , NULL, INCREMENTAL },
+  { "incremental", no_argument      , NULL, 'i' },
   { "replay"     , required_argument, NULL, REPLAY      },
   { "replay-log" , required_argument, NULL, REPLAY_LOG  },
-  { "produce-models", no_argument   , NULL, PRODUCE_MODELS },
-  { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS },
-  { "no-type-checking", no_argument, NULL, NO_TYPE_CHECKING },
-  { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING },
-  { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING },
   { "pivot-rule" , required_argument, NULL, PIVOT_RULE  },
   { "pivot-threshold" , required_argument, NULL, ARITHMETIC_PIVOT_THRESHOLD  },
   { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH  },
@@ -405,7 +398,7 @@ throw(OptionException) {
   // permitted.  cmdlineOptions specifies all the long-options and the
   // return value for getopt_long() should they be encountered.
   while((c = getopt_long(argc, argv,
-                         ":hVvqL:d:t:",
+                         ":himVvqL:d:t:",
                          cmdlineOptions, NULL)) != -1) {
     switch(c) {
 
@@ -614,7 +607,7 @@ throw(OptionException) {
       interactiveSetByUser = true;
       break;
 
-    case PRODUCE_MODELS:
+    case 'm':
       produceModels = true;
       break;
 
@@ -637,7 +630,7 @@ throw(OptionException) {
       earlyTypeChecking = true;
       break;
 
-    case INCREMENTAL:
+    case 'i':
       incrementalSolving = true;
       break;