user push/pop support in minisat and simplification; also bindings work

13 files changed, 438 insertions, 62 deletions

diff --git a/config/bindings.m4 b/config/bindings.m4
index f47490fec..e328810fb 100644
--- a/config/bindings.m4
+++ b/config/bindings.m4
@@ -21,8 +21,8 @@ AC_ARG_WITH([swig],
   [AS_HELP_STRING([--with-swig=BINARY], [path to swig binary])],
   [if test "$withval" = no; then noswig=yes; else SWIG="$withval"; fi])
 AC_ARG_ENABLE([language-bindings],
-  [AS_HELP_STRING([--enable-language-bindings=][CVC4_SUPPORTED_BINDINGS], [specify language bindings to build])],
-  [cvc4_check_for_bindings=no; if test "$enableval" = no; then try_bindings=; else try_bindings="$enableval"; fi],
+  [AS_HELP_STRING([--enable-language-bindings=][CVC4_SUPPORTED_BINDINGS][ | all], [specify language bindings to build])],
+  [if test "$enableval" = yes; then cvc4_check_for_bindings=yes; try_bindings='$1'; else cvc4_check_for_bindings=no; if test "$enableval" = no; then try_bindings=; else try_bindings="$enableval"; fi; fi],
   [cvc4_check_for_bindings=yes; try_bindings=])
 CVC4_LANGUAGE_BINDINGS=
 if test "$noswig" = yes; then
@@ -44,12 +44,18 @@ else
     fi
   else
     AC_MSG_CHECKING([for requested user language bindings])
-    if test "$cvc4_check_for_bindings" = yes; then
-      try_bindings='$1'
+    if test "$try_bindings" = all; then
+      try_bindings='CVC4_SUPPORTED_BINDINGS'
+    fi
+    try_bindings=$(echo "$try_bindings" | sed 's/,/ /g')
+    if test -z "$try_bindings"; then
+      AC_MSG_RESULT([none])
     else
-      try_bindings=$(echo "$try_bindings" | sed 's/,/ /g')
+      AC_MSG_RESULT([$try_bindings])
     fi
-    AC_MSG_RESULT([$try_bindings])
+    cvc4_save_CPPFLAGS="$CPPFLAGS"
+    cvc4_save_CXXFLAGS="$CXXFLAGS"
+    AC_LANG_PUSH([C++])
     for binding in $try_bindings; do
       binding_error=no
       AC_MSG_CHECKING([for availability of $binding binding])
@@ -60,35 +66,58 @@ else
           cvc4_build_c_bindings=yes
           AC_MSG_RESULT([C support will be built]);;
         java)
-          cvc4_build_java_bindings=yes
-          AC_MSG_RESULT([Java support will be built]);;
+          AC_MSG_RESULT([Java support will be built])
+          AC_ARG_VAR(JAVA_CPPFLAGS, [flags to pass to compiler when building Java bindings])
+          CPPFLAGS="$CPPFLAGS $JAVA_CPPFLAGS"
+          AC_CHECK_HEADER([jni.h], [cvc4_build_java_bindings=yes], [binding_error=yes])
+          ;;
         csharp)
-          binding_error=yes
-          AC_MSG_RESULT([$binding not supported yet]);;
+          cvc4_build_csharp_bindings=yes
+          AC_MSG_RESULT([[C# support will be built]]);;
         perl)
-          binding_error=yes
-          AC_MSG_RESULT([$binding not supported yet]);;
+          AC_MSG_RESULT([perl support will be built])
+          AC_ARG_VAR(PERL_CPPFLAGS, [flags to pass to compiler when building perl bindings])
+          CPPFLAGS="$CPPFLAGS $PERL_CPPFLAGS"
+          AC_CHECK_HEADER([EXTERN.h], [cvc4_build_perl_bindings=yes], [binding_error=yes])
+          ;;
         php)
-          binding_error=yes
-          AC_MSG_RESULT([$binding not supported yet]);;
+          AC_MSG_RESULT([php support will be built])
+          AC_ARG_VAR(PHP_CPPFLAGS, [flags to pass to compiler when building PHP bindings])
+          CPPFLAGS="$CPPFLAGS $PHP_CPPFLAGS"
+          AC_CHECK_HEADER([zend.h], [cvc4_build_php_bindings=yes], [binding_error=yes])
+          ;;
         python)
-          binding_error=yes
-          AC_MSG_RESULT([$binding not supported yet]);;
+          AC_MSG_RESULT([python support will be built])
+          AC_ARG_VAR(PYTHON_CPPFLAGS, [flags to pass to compiler when building Python bindings])
+          CPPFLAGS="$CPPFLAGS $PYTHON_CPPFLAGS"
+          AC_CHECK_HEADER([Python.h], [cvc4_build_python_bindings=yes], [binding_error=yes])
+          ;;
         ruby)
-          binding_error=yes
-          AC_MSG_RESULT([$binding not supported yet]);;
+          AC_MSG_RESULT([ruby support will be built])
+          AC_ARG_VAR(RUBY_CPPFLAGS, [flags to pass to compiler when building ruby bindings])
+          CPPFLAGS="$CPPFLAGS $RUBY_CPPFLAGS"
+          AC_CHECK_HEADER([ruby.h], [cvc4_build_ruby_bindings=yes], [binding_error=yes])
+          ;;
         tcl)
-          binding_error=yes
-          AC_MSG_RESULT([$binding not supported yet]);;
+          cvc4_build_tcl_bindings=yes
+          AC_MSG_RESULT([tcl support will be built]);;
         ocaml)
-          binding_error=yes
-          AC_MSG_RESULT([$binding not supported yet]);;
+          cvc4_build_ocaml_bindings=yes
+          AC_MSG_RESULT([OCaml support will be built]);;
         *) AC_MSG_RESULT([unknown binding]); binding_error=yes;;
       esac
-      if test "$binding_error" = yes -a "$cvc4_check_for_bindings" = no; then
-        AC_MSG_ERROR([Language binding \`$binding' requested by user, but it cannot be built.])
+      if test "$binding_error" = yes; then
+        if test "$cvc4_check_for_bindings" = no; then
+          AC_MSG_ERROR([Language binding \`$binding' requested by user, but it cannot be built.])
+        else
+          AC_MSG_WARN([Language binding \`$binding' cannot be built.])
+        fi
+      else
+        CVC4_LANGUAGE_BINDINGS="${CVC4_LANGUAGE_BINDINGS:+$CVC4_LANGUAGE_BINDINGS }$binding"
       fi
-      CVC4_LANGUAGE_BINDINGS="${CVC4_LANGUAGE_BINDINGS:+$CVC4_LANGUAGE_BINDINGS }$binding"
+      AC_LANG_POP([C++])
+      CXXFLAGS="$cvc4_save_CXXFLAGS"
+      CPPFLAGS="$cvc4_save_CPPFLAGS"
     done
   fi
 fi
diff --git a/configure.ac b/configure.ac
index b2badafbb..930a5685c 100644
--- a/configure.ac
+++ b/configure.ac
@@ -784,7 +784,7 @@ AC_LIB_ANTLR
 # build support.  The arg list is the default set if unspecified by
 # the user (the actual built set is the subset that appears to be
 # supported by the build host).
-CVC4_CHECK_BINDINGS dnl ([java csharp perl php python ruby tcl ocaml])
+CVC4_CHECK_BINDINGS([c java])dnl csharp perl php python ruby tcl ocaml])
 
 # Checks for header files.
 AC_CHECK_HEADERS([getopt.h unistd.h])
@@ -857,7 +857,6 @@ AC_ARG_VAR(JAVA, [Java interpreter (used when testing Java interface)])
 AC_ARG_VAR(JAVAC, [Java compiler (used when building and testing Java interface)])
 AC_ARG_VAR(JAVAH, [Java compiler (used when building and testing Java interface)])
 AC_ARG_VAR(JAR, [Jar archiver (used when building Java interface)])
-AC_ARG_VAR(JAVA_INCLUDES, [flags to pass to C compiler when building JNI libraries])
 if test "$cvc4_build_java_bindings"; then
   dnl AM_PROG_GCJ
   if test -z "$JAVA"; then
diff --git a/examples/SimpleVCCompat.java b/examples/SimpleVCCompat.java
index 107b5504e..aa28a423b 100644
--- a/examples/SimpleVCCompat.java
+++ b/examples/SimpleVCCompat.java
@@ -39,6 +39,8 @@ import cvc3.*;
 
 public class SimpleVCCompat {
   public static void main(String[] args) {
+    //System.loadLibrary("cvc4bindings_java_compat");
+
     ValidityChecker vc = ValidityChecker.create();
 
     // Prove that for integers x and y:
diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index f9420dbdb..e35ec5e67 100644
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -30,13 +30,62 @@ libcvc4bindings_java_la_LIBADD = \
 	-L@builddir@/.. -lcvc4 \
 	-L@builddir@/../parser -lcvc4parser
 endif
-#	cvc4bindings_csharp.so \
-#	cvc4bindings_perl.so \
-#	cvc4bindings_php.so \
-#	cvc4bindings_python.so \
-#	cvc4bindings_ocaml.so \
-#	cvc4bindings_ruby.so \
-#	cvc4bindings_tcl.so
+if CVC4_LANGUAGE_BINDING_CSHARP
+lib_LTLIBRARIES += libcvc4bindings_csharp.la
+libcvc4bindings_csharp_la_LDFLAGS = \
+	-version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_csharp_la_LIBADD = \
+	-L@builddir@/.. -lcvc4 \
+	-L@builddir@/../parser -lcvc4parser
+endif
+if CVC4_LANGUAGE_BINDING_PERL
+lib_LTLIBRARIES += libcvc4bindings_perl.la
+libcvc4bindings_perl_la_LDFLAGS = \
+	-version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_perl_la_LIBADD = \
+	-L@builddir@/.. -lcvc4 \
+	-L@builddir@/../parser -lcvc4parser
+endif
+if CVC4_LANGUAGE_BINDING_PHP
+lib_LTLIBRARIES += libcvc4bindings_php.la
+libcvc4bindings_php_la_LDFLAGS = \
+	-version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_php_la_LIBADD = \
+	-L@builddir@/.. -lcvc4 \
+	-L@builddir@/../parser -lcvc4parser
+endif
+if CVC4_LANGUAGE_BINDING_PYTHON
+lib_LTLIBRARIES += libcvc4bindings_python.la
+libcvc4bindings_python_la_LDFLAGS = \
+	-version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_python_la_LIBADD = \
+	-L@builddir@/.. -lcvc4 \
+	-L@builddir@/../parser -lcvc4parser
+endif
+if CVC4_LANGUAGE_BINDING_OCAML
+lib_LTLIBRARIES += libcvc4bindings_ocaml.la
+libcvc4bindings_ocaml_la_LDFLAGS = \
+	-version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_ocaml_la_LIBADD = \
+	-L@builddir@/.. -lcvc4 \
+	-L@builddir@/../parser -lcvc4parser
+endif
+if CVC4_LANGUAGE_BINDING_RUBY
+lib_LTLIBRARIES += libcvc4bindings_ruby.la
+libcvc4bindings_ruby_la_LDFLAGS = \
+	-version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_ruby_la_LIBADD = \
+	-L@builddir@/.. -lcvc4 \
+	-L@builddir@/../parser -lcvc4parser
+endif
+if CVC4_LANGUAGE_BINDING_TCL
+lib_LTLIBRARIES += libcvc4bindings_tcl.la
+libcvc4bindings_tcl_la_LDFLAGS = \
+	-version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_tcl_la_LIBADD = \
+	-L@builddir@/.. -lcvc4 \
+	-L@builddir@/../parser -lcvc4parser
+endif
 
 nodist_libcvc4bindings_java_la_SOURCES = java.cpp
 libcvc4bindings_java_la_CXXFLAGS = -fno-strict-aliasing
@@ -66,7 +115,7 @@ MOSTLYCLEANFILES = \
 	cvc4.jar
 
 java.lo: java.cpp
-	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_INCLUDES) -o $@ $<
+	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_CPPFLAGS) -o $@ $<
 cvc4.jar: java.cpp
 	$(AM_V_GEN) \
 	(cd java; \
@@ -77,15 +126,26 @@ cvc4.jar: java.cpp
 	$(JAR) cf $@ -C java/classes .
 java.cpp:
 csharp.cpp:
+perl.lo: perl.cpp
+	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(PERL_CPPFLAGS) -o $@ $<
 perl.cpp:
+php.lo: php.cpp
+	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(PHP_CPPFLAGS) -Iphp -o $@ $<
 php.cpp:
+python.lo: python.cpp
+	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(PYTHON_CPPFLAGS) -o $@ $<
 python.cpp:
 ocaml.cpp:
+python.lo: ruby.cpp
+	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(RUBY_CPPFLAGS) -o $@ $<
 ruby.cpp:
 tcl.cpp:
-$(patsubst %,%.cpp,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.cpp: @srcdir@/../cvc4.i
+java.cpp: @srcdir@/../cvc4.i
 	$(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@)
 	$(AM_V_GEN)$(SWIG) -Wall -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -package edu.nyu.acsys.CVC4 -o $@ $<
+$(patsubst %,%.cpp,$(filter-out c c++ java,$(CVC4_LANGUAGE_BINDINGS))): %.cpp: @srcdir@/../cvc4.i
+	$(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@)
+	$(AM_V_GEN)$(SWIG) -Wall -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -o $@ $<
 
 $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.d: @srcdir@/../cvc4.i
 	$(AM_V_GEN)$(SWIG) -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -MM -o $(patsubst %.d,%.cpp,$@) $<
diff --git a/src/cvc4.i b/src/cvc4.i
index 7f7926bfd..0e2f48dba 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -40,6 +40,13 @@ using namespace CVC4;
 %template(setType) std::set< CVC4::Type >;
 %template(hashmapExpr) std::hash_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >;
 
+// This is unfortunate, but seems to be necessary; if we leave NULL
+// defined, swig will expand it to "(void*) 0", and some of swig's
+// helper functions won't compile properly.
+#undef NULL
+
+#ifdef SWIGJAVA
+
 %exception {
   try {
     $action
@@ -50,16 +57,13 @@ using namespace CVC4;
   }
 }
 
-// This is unfortunate, but seems to be necessary; if we leave NULL
-// defined, swig will expand it to "(void*) 0", and some of swig's
-// helper functions won't compile properly.
-#undef NULL
-
 %include "java/typemaps.i" // primitive pointers and references
 %include "java/std_string.i" // map std::string to java.lang.String
 %include "java/arrays_java.i" // C arrays to Java arrays
 %include "java/various.i" // map char** to java.lang.String[]
 
+#endif /* SWIGJAVA */
+
 %include "util/integer.i"
 %include "util/rational.i"
 %include "util/stats.i"
diff --git a/src/parser/parser.i b/src/parser/parser.i
index 55119be9a..dd52bfcda 100644
--- a/src/parser/parser.i
+++ b/src/parser/parser.i
@@ -8,7 +8,24 @@ namespace CVC4 {
     enum SymbolType;
     %ignore operator<<(std::ostream&, DeclarationCheck);
     %ignore operator<<(std::ostream&, SymbolType);
+
+  class ParserExprStream : public CVC4::ExprStream {
+    Parser* d_parser;
+  public:
+    ExprStream(Parser* parser) : d_parser(parser) {}
+    ~ExprStream() { delete d_parser; }
+    Expr nextExpr() { return d_parser->nextExpression(); }
+  };/* class Parser::ExprStream */
+
   }/* namespace CVC4::parser */
 }/* namespace CVC4 */
 
 %include "parser/parser.h"
+
+%{
+namespace CVC4 {
+  namespace parser {
+    typedef CVC4::parser::Parser::ExprStream ParserExprStream;
+  }
+}
+%}
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 7b5ba9286..c1795a12c 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -221,7 +221,6 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
     // Fit to size
     ps.shrink(i - j);
 
-
     // If we are in solve or decision level > 0
     if (minisat_busy || decisionLevel() > 0) {
       lemmas.push();
@@ -232,8 +231,15 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
       if (ps.size() == 0) {
           return ok = false;
       } else if (ps.size() == 1) {
-        uncheckedEnqueue(ps[0]);
-        return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef);
+        if(assigns[var(ps[0])] == l_Undef) {
+          uncheckedEnqueue(ps[0]);
+          if(assertionLevel > 0) {
+            // remember to unset it on user pop
+            Debug("minisat") << "got new unit " << ps[0] << " at assertion level " << assertionLevel << std::endl;
+            trail_user.push(ps[0]);
+          }
+          return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef);
+        } else return ok;
       } else {
         CRef cr = ca.alloc(assertionLevel, ps, false);
         clauses_persistent.push(cr);
@@ -307,10 +313,13 @@ void Solver::cancelUntil(int level) {
         }
         for (int c = trail.size()-1; c >= trail_lim[level]; c--){
             Var      x  = var(trail[c]);
-            assigns [x] = l_Undef;
-            if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
+            if(intro_level(x) != -1) {// might be unregistered
+              assigns [x] = l_Undef;
+              vardata[x].trail_index = -1;
+              if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
                 polarity[x] = sign(trail[c]);
-            insertVarOrder(x);
+              insertVarOrder(x);
+            }
         }
         qhead = trail_lim[level];
         trail.shrink(trail.size() - trail_lim[level]);
@@ -581,8 +590,16 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
     Debug("minisat") << "unchecked enqueue of " << p << " (" << trail_index(var(p)) << ") trail size is " << trail.size() << " cap is " << trail.capacity() << std::endl;
     assert(value(p) == l_Undef);
     assigns[var(p)] = lbool(!sign(p));
-    vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail.size());
-    trail.push_(p);
+    if(trail_index(var(p)) != -1) {
+      // This var is already represented in the trail, presumably from
+      // an earlier incarnation as a unit clause (it has been
+      // unregistered and renewed since then)
+      vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail_index(var(p)));
+      trail[trail_index(var(p))] = p;
+    } else {
+      vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail.size());
+      trail.push_(p);
+    }
     if (theory[var(p)]) {
       // Enqueue to the theory
       proxy->enqueueTheoryLiteral(p);
@@ -1050,6 +1067,8 @@ lbool Solver::solve_()
 
     ScopedBool scoped_bool(minisat_busy, true);
 
+    popTrail();
+
     model.clear();
     conflict.clear();
     if (!ok){
@@ -1231,14 +1250,19 @@ void Solver::push()
 {
   assert(enable_incremental);
 
-  Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl;
+  popTrail();
   ++assertionLevel;
+  Debug("minisat") << "in user push, increasing assertion level to " << assertionLevel << std::endl;
+  trail_user.push(lit_Undef);
+  trail_ok.push(ok);
 }
 
 void Solver::pop()
 {
   assert(enable_incremental);
 
+  popTrail();
+
   --assertionLevel;
 
   Debug("minisat") << "in user pop, reducing assertion level to " << assertionLevel << " and removing clauses above this from db" << std::endl;
@@ -1247,8 +1271,26 @@ void Solver::pop()
   removeClausesAboveLevel(clauses_removable, assertionLevel);
   removeClausesAboveLevel(clauses_persistent, assertionLevel);
 
-  // Pop the user trail size
-  popTrail();
+  Debug("minisat") << "in user pop, at " << trail_lim.size() << " : " << assertionLevel << std::endl;
+
+  // Unset any units learned or added at this level
+  Debug("minisat") << "in user pop, unsetting level units for level " << assertionLevel << std::endl;
+  while(trail_user.last() != lit_Undef) {
+    Lit l = trail_user.last();
+    Debug("minisat") << "== unassigning " << l << std::endl;
+    Var      x  = var(l);
+    assigns [x] = l_Undef;
+    if (phase_saving >= 1)
+      polarity[x] = sign(l);
+    insertVarOrder(x);
+    trail_user.pop();
+  }
+  trail_user.pop();
+  ok = trail_ok.last();
+  trail_ok.pop();
+  Debug("minisat") << "in user pop, done unsetting level units" << std::endl;
+
+  Debug("minisat") << "about to removeClausesAboveLevel(" << assertionLevel << ") in CNF" << std::endl;
 
   // Notify the cnf
   proxy->removeClausesAboveLevel(assertionLevel);
@@ -1357,9 +1399,11 @@ CRef Solver::updateLemmas() {
 //          }
           Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;
           uncheckedEnqueue(lemma[0], lemma_ref);
-          if(assertionLevel > 0) {
+          if(lemma.size() == 1 && assertionLevel > 0) {
+            assert(decisionLevel() == 0);
             // remember to unset it on user pop
             Debug("minisat") << "got new unit (survived downward during updateLemmas()) " << lemma[0] << " at assertion level " << assertionLevel << std::endl;
+            trail_user.push(lemma[0]);
           }
         }
       }
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 345a00e52..c5220997b 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -278,6 +278,8 @@ protected:
     vec<char>           decision;           // Declares if a variable is eligible for selection in the decision heuristic.
     vec<Lit>            trail;              // Assignment stack; stores all assigments made in the order they were made.
     vec<int>            trail_lim;          // Separator indices for different decision levels in 'trail'.
+    vec<Lit>            trail_user;         // Stack of assignments to UNdo on user pop.
+    vec<bool>           trail_ok;           // Stack of "whether we're in conflict" flags.
     vec<VarData>        vardata;            // Stores reason and level for each variable.
     int                 qhead;              // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
     int                 simpDB_assigns;     // Number of top-level assignments since last execution of 'simplify()'.
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index f8292c072..8c31dd377 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -57,7 +57,7 @@ SimpSolver::SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* con
   , asymm_lits         (0)
   , eliminated_vars    (0)
   , elimorder          (1)
-  , use_simplification (true)
+  , use_simplification (!enableIncremental)
   , occurs             (ClauseDeleted(ca))
   , elim_heap          (ElimLt(n_occ))
   , bwdsub_assigns     (0)
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 42b21b79a..f80d9a135 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -574,14 +574,17 @@ void SmtEnginePrivate::nonClausalSimplify() {
   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                     << "applying substitutions" << endl;
   for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
+    Trace("simplify") << "applying to " << d_assertionsToPreprocess[i] << std::endl;
     d_assertionsToPreprocess[i] =
       theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i]));
+    Trace("simplify") << "  got " << d_assertionsToPreprocess[i] << std::endl;
   }
 
   // Assert all the assertions to the propagator
   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                     << "asserting to propagator" << endl;
   for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
+    Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertionsToPreprocess[i] << std::endl;
     d_propagator.assert(d_assertionsToPreprocess[i]);
   }
 
@@ -591,6 +594,7 @@ void SmtEnginePrivate::nonClausalSimplify() {
     // If in conflict, just return false
     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                       << "conflict in non-clausal propagation" << endl;
+    d_assertionsToPreprocess.clear();
     d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
     return;
   } else {
@@ -610,6 +614,7 @@ void SmtEnginePrivate::nonClausalSimplify() {
           Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                             << "conflict with "
                             << d_nonClausalLearnedLiterals[i] << endl;
+          d_assertionsToPreprocess.clear();
           d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
           return;
         }
@@ -625,6 +630,7 @@ void SmtEnginePrivate::nonClausalSimplify() {
         Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                           << "conflict while solving "
                           << learnedLiteral << endl;
+        d_assertionsToPreprocess.clear();
         d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
         return;
       case Theory::SOLVE_STATUS_SOLVED:
diff --git a/src/util/datatype.i b/src/util/datatype.i
index f306d7682..b62033e17 100644
--- a/src/util/datatype.i
+++ b/src/util/datatype.i
@@ -7,7 +7,7 @@ namespace CVC4 {
 
 namespace CVC4 {
 %rename(DatatypeConstructor) CVC4::Datatype::Constructor;
-//%rename(DatatypeConstructor) CVC4::Constructor;
+%rename(DatatypeConstructor) CVC4::Constructor;
 }
 
 %extend std::vector< CVC4::Datatype > {
@@ -37,5 +37,221 @@ namespace CVC4 {
 %ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor&);
 %ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor::Arg&);
 
+%feature("valuewrapper") CVC4::Datatype::UnresolvedType;
 
 %include "util/datatype.h"
+
+namespace CVC4 {
+    class CVC4_PUBLIC Arg {
+
+      std::string d_name;
+      Expr d_selector;
+      /** the constructor associated with this selector */
+      Expr d_constructor;
+      bool d_resolved;
+
+      explicit Arg(std::string name, Expr selector);
+      friend class Constructor;
+      friend class Datatype;
+
+      bool isUnresolvedSelf() const throw();
+
+    public:
+
+      /** Get the name of this constructor argument. */
+      std::string getName() const throw();
+
+      /**
+       * Get the selector for this constructor argument; this call is
+       * only permitted after resolution.
+       */
+      Expr getSelector() const;
+
+      /**
+       * Get the associated constructor for this constructor argument;
+       * this call is only permitted after resolution.
+       */
+      Expr getConstructor() const;
+
+      /**
+       * Get the selector for this constructor argument; this call is
+       * only permitted after resolution.
+       */
+      Type getSelectorType() const;
+
+      /**
+       * Get the name of the type of this constructor argument
+       * (Datatype field).  Can be used for not-yet-resolved Datatypes
+       * (in which case the name of the unresolved type, or "[self]"
+       * for a self-referential type is returned).
+       */
+      std::string getSelectorTypeName() const;
+
+      /**
+       * Returns true iff this constructor argument has been resolved.
+       */
+      bool isResolved() const throw();
+
+    };/* class Datatype::Constructor::Arg */
+
+  class Constructor {
+  public:
+
+    /** The type for iterators over constructor arguments. */
+    typedef std::vector<Arg>::iterator iterator;
+    /** The (const) type for iterators over constructor arguments. */
+    typedef std::vector<Arg>::const_iterator const_iterator;
+
+  private:
+
+    std::string d_name;
+    Expr d_constructor;
+    Expr d_tester;
+    std::vector<Arg> d_args;
+
+    void resolve(ExprManager* em, DatatypeType self,
+                 const std::map<std::string, DatatypeType>& resolutions,
+                 const std::vector<Type>& placeholders,
+                 const std::vector<Type>& replacements,
+                 const std::vector< SortConstructorType >& paramTypes,
+                 const std::vector< DatatypeType >& paramReplacements)
+      throw(AssertionException, DatatypeResolutionException);
+    friend class Datatype;
+
+    /** @FIXME document this! */
+    Type doParametricSubstitution(Type range,
+                                  const std::vector< SortConstructorType >& paramTypes,
+                                  const std::vector< DatatypeType >& paramReplacements);
+  public:
+    /**
+     * Create a new Datatype constructor with the given name for the
+     * constructor and the given name for the tester.  The actual
+     * constructor and tester aren't created until resolution time.
+     */
+    explicit Constructor(std::string name, std::string tester);
+
+    /**
+     * Add an argument (i.e., a data field) of the given name and type
+     * to this Datatype constructor.
+     */
+    void addArg(std::string selectorName, Type selectorType);
+
+    /**
+     * Add an argument (i.e., a data field) of the given name to this
+     * Datatype constructor that refers to an as-yet-unresolved
+     * Datatype (which may be mutually-recursive).
+     */
+    void addArg(std::string selectorName, Datatype::UnresolvedType selectorType);
+
+    /**
+     * Add a self-referential (i.e., a data field) of the given name
+     * to this Datatype constructor that refers to the enclosing
+     * Datatype.  For example, using the familiar "nat" Datatype, to
+     * create the "pred" field for "succ" constructor, one uses
+     * succ::addArg("pred", Datatype::SelfType())---the actual Type
+     * cannot be passed because the Datatype is still under
+     * construction.
+     *
+     * This is a special case of
+     * Constructor::addArg(std::string, Datatype::UnresolvedType).
+     */
+    void addArg(std::string selectorName, Datatype::SelfType);
+
+    /** Get the name of this Datatype constructor. */
+    std::string getName() const throw();
+    /**
+     * Get the constructor operator of this Datatype constructor.  The
+     * Datatype must be resolved.
+     */
+    Expr getConstructor() const;
+    /**
+     * Get the tester operator of this Datatype constructor.  The
+     * Datatype must be resolved.
+     */
+    Expr getTester() const;
+    /**
+     * Get the number of arguments (so far) of this Datatype constructor.
+     */
+    inline size_t getNumArgs() const throw();
+
+    /**
+     * Get the specialized constructor type for a parametric
+     * constructor; this call is only permitted after resolution.
+     */
+    Type getSpecializedConstructorType(Type returnType) const;
+
+    /**
+     * Return the cardinality of this constructor (the product of the
+     * cardinalities of its arguments).
+     */
+    Cardinality getCardinality() const throw(AssertionException);
+
+    /**
+     * Return true iff this constructor is finite (it is nullary or
+     * each of its argument types are finite).  This function can
+     * only be called for resolved constructors.
+     */
+    bool isFinite() const throw(AssertionException);
+
+    /**
+     * Return true iff this constructor is well-founded (there exist
+     * ground terms).  The constructor must be resolved or an
+     * exception is thrown.
+     */
+    bool isWellFounded() const throw(AssertionException);
+
+    /**
+     * Construct and return a ground term of this constructor.  The
+     * constructor must be both resolved and well-founded, or else an
+     * exception is thrown.
+     */
+    Expr mkGroundTerm( Type t ) const throw(AssertionException);
+
+    /**
+     * Returns true iff this Datatype constructor has already been
+     * resolved.
+     */
+    inline bool isResolved() const throw();
+
+    /** Get the beginning iterator over Constructor args. */
+    inline iterator begin() throw();
+    /** Get the ending iterator over Constructor args. */
+    inline iterator end() throw();
+    /** Get the beginning const_iterator over Constructor args. */
+    inline const_iterator begin() const throw();
+    /** Get the ending const_iterator over Constructor args. */
+    inline const_iterator end() const throw();
+
+    /** Get the ith Constructor arg. */
+    const Arg& operator[](size_t index) const;
+
+  };/* class Datatype::Constructor */
+}
+
+  class SelfType {
+  };/* class Datatype::SelfType */
+
+  /**
+   * An unresolved type (used in calls to
+   * Datatype::Constructor::addArg()) to allow a Datatype to refer to
+   * itself or to other mutually-recursive Datatypes.  Unresolved-type
+   * fields of Datatypes will be properly typed when a Type is created
+   * for the Datatype by the ExprManager (which calls
+   * Datatype::resolve()).
+   */
+  class UnresolvedType {
+    std::string d_name;
+  public:
+    inline UnresolvedType(std::string name);
+    inline std::string getName() const throw();
+  };/* class Datatype::UnresolvedType */
+
+%{
+namespace CVC4 {
+typedef Datatype::Constructor Constructor;
+typedef Datatype::Constructor::Arg Arg;
+typedef Datatype::SelfType SelfType;
+typedef Datatype::UnresolvedType UnresolvedType;
+}
+%}
+
diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am
index 85c3cb9c9..86eeae902 100644
--- a/test/regress/regress0/push-pop/Makefile.am
+++ b/test/regress/regress0/push-pop/Makefile.am
@@ -8,7 +8,10 @@ MAKEFLAGS = -k
 # put it below in "TESTS +="
 
 # Regression tests for SMT inputs
-CVC_TESTS = 
+CVC_TESTS = \
+	test.00.cvc \
+	test.01.cvc \
+	units.cvc
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
 
diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index cc0d63aee..6f8094410 100644
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -71,12 +71,6 @@ cvc3_main: cvc3_george.lo $(LIBADD)
 	$(AM_V_CXXLD)$(system_LINK) $(LIBADD) $(AM_LDFLAGS) $+
 CVC4JavaTest.class: CVC4JavaTest.java @abs_top_builddir@/src/bindings/cvc4.jar @abs_top_builddir@/src/bindings/libcvc4bindings_java.la
 	$(AM_V_JAVAC)$(JAVAC) -classpath @abs_top_builddir@/src/bindings/cvc4.jar -d $(builddir) $<
-#CVC4JavaTest: CVC4JavaTest.class
-#	$(AM_V_GEN)( \
-#	echo "#!/bin/bash"; \
-#	echo "exec $(JAVA) -classpath @abs_top_builddir@/src/bindings/cvc4.jar -Djava.library.path=@abs_top_builddir@/src/bindings/.libs CVC4JavaTest"; \
-#	) >$@; \
-#	chmod +x $@
 
 # for silent automake rules
 AM_V_JAVAC = $(am__v_JAVAC_$(V))