Bindings work (ocaml bindings are now sort of working); also minor cleanup

16 files changed, 219 insertions, 29 deletions

diff --git a/config/bindings.m4 b/config/bindings.m4
index c478b6da3..416a338da 100644
--- a/config/bindings.m4
+++ b/config/bindings.m4
@@ -72,8 +72,11 @@ else
           AC_CHECK_HEADER([jni.h], [cvc4_build_java_bindings=yes], [binding_error=yes])
           ;;
         csharp)
+          AC_MSG_RESULT([[C# support will be built]])
+          AC_ARG_VAR(CSHARP_CPPFLAGS, [flags to pass to compiler when building C# bindings])
+          CPPFLAGS="$CPPFLAGS $CSHARP_CPPFLAGS"
           cvc4_build_csharp_bindings=yes
-          AC_MSG_RESULT([[C# support will be built]]);;
+          ;;
         perl)
           AC_MSG_RESULT([perl support will be built])
           AC_ARG_VAR(PERL_CPPFLAGS, [flags to pass to compiler when building perl bindings])
@@ -99,11 +102,43 @@ else
           AC_CHECK_HEADER([ruby.h], [cvc4_build_ruby_bindings=yes], [binding_error=yes])
           ;;
         tcl)
+          AC_MSG_RESULT([tcl support will be built])
+          AC_ARG_VAR(TCL_CPPFLAGS, [flags to pass to compiler when building tcl bindings])
+          CPPFLAGS="$CPPFLAGS $TCL_CPPFLAGS"
           cvc4_build_tcl_bindings=yes
-          AC_MSG_RESULT([tcl support will be built]);;
+          ;;
         ocaml)
-          cvc4_build_ocaml_bindings=yes
-          AC_MSG_RESULT([OCaml support will be built]);;
+          AC_MSG_RESULT([OCaml support will be built])
+          AC_ARG_VAR(TCL_CPPFLAGS, [flags to pass to compiler when building OCaml bindings])
+          CPPFLAGS="$CPPFLAGS $OCAML_CPPFLAGS"
+          AC_CHECK_HEADER([caml/misc.h], [cvc4_build_ocaml_bindings=yes], [binding_error=yes])
+          if test "$binding_error" = no; then
+            AC_ARG_VAR(OCAMLC, [OCaml compiler])
+            if test -z "$OCAMLC"; then
+              AC_CHECK_PROGS(OCAMLC, ocamlc, ocamlc, [])
+            else
+              AC_CHECK_PROG(OCAMLC, "$OCAMLC", "$OCAMLC", [])
+            fi
+            AC_ARG_VAR(OCAMLMKTOP, [OCaml runtime-maker])
+            if test -z "$OCAMLMKTOP"; then
+              AC_CHECK_PROGS(OCAMLMKTOP, ocamlmktop, ocamlmktop, [])
+            else
+              AC_CHECK_PROG(OCAMLMKTOP, "$OCAMLMKTOP", "$OCAMLMKTOP", [])
+            fi
+            AC_ARG_VAR(OCAMLFIND, [OCaml-find binary])
+            if test -z "$OCAMLFIND"; then
+              AC_CHECK_PROGS(OCAMLFIND, ocamlfind, ocamlfind, [])
+            else
+              AC_CHECK_PROG(OCAMLFIND, "$OCAMLFIND", "$OCAMLFIND", [])
+            fi
+            AC_ARG_VAR(CAMLP4O, [camlp4o binary])
+            if test -z "$CAMLP4O"; then
+              AC_CHECK_PROGS(CAMLP4O, camlp4o, camlp4o, [])
+            else
+              AC_CHECK_PROG(CAMLP4O, "$CAMLP4O", "$CAMLP4O", [])
+            fi
+          fi
+          ;;
         *) AC_MSG_RESULT([unknown binding]); binding_error=yes;;
       esac
       if test "$binding_error" = yes; then
diff --git a/examples/Makefile.am b/examples/Makefile.am
index f72c20d02..46de3689b 100644
--- a/examples/Makefile.am
+++ b/examples/Makefile.am
@@ -52,6 +52,7 @@ SimpleVCCompat.class: SimpleVCCompat.java
 EXTRA_DIST = \
 	SimpleVC.java \
 	SimpleVC.py \
+	SimpleVC.ml \
 	SimpleVCCompat.java \
 	README
 
diff --git a/examples/SimpleVC.ml b/examples/SimpleVC.ml
new file mode 100644
index 000000000..f7caa9e3d
--- /dev/null
+++ b/examples/SimpleVC.ml
@@ -0,0 +1,91 @@
+(*********************                                                        **
+**! \file SimpleVC.ml
+*** \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 OCaml interface
+***
+*** A simple demonstration of the OCaml interface.  Compare to the
+*** C++ interface in simple_vc_cxx.cpp; they are quite similar.
+***
+*** To run, use something like:
+***
+***   LD_LIBRARY_PATH=../builds/src/bindings/.libs \
+***     ../builds/src/bindings/cvc4_ocaml_top -I ../builds/src/bindings/ocaml \
+***     SimpleVC.ml
+***
+*** After you "make install" CVC4, it's much easier; the cvc4_ocaml_top goes in
+*** $prefix/bin, and it's automatically set up the load the .cmo and .cmi files
+*** from $prefix/lib/ocaml/cvc4, in which they get installed.  Then you just
+*** have to: cvc4_ocaml_top -I $prefix/lib/ocaml/cvc4
+***)
+
+open Swig
+open CVC4
+
+let em = new_ExprManager '()
+let smt = new_SmtEngine(em)
+
+(* Prove that for integers x and y:
+ *   x > 0 AND y > 0  =>  2x + y >= 3 *)
+
+let integer = em->integerType()
+
+let x = em->mkVar(integer) (* em->mkVar("x", integer) *)
+let y = em->mkVar(integer) (* em->mkVar("y", integer) *)
+let integerZero = new_Integer '("0", 10)
+let zero = em->mkConst(integerZero)
+
+(* OK, this is really strange.  We can call mkExpr(36, ...) for
+ * example, with the int value of the operator Kind we want,
+ * or we can compute it.  But if we compute it, we have to rip
+ * it out of its C_int, then wrap it again a C_int, in order
+ * for the parser to make it go through. *)
+let geq = C_int (get_int (enum_to_int `Kind_t (``GEQ)))
+let gt = C_int (get_int (enum_to_int `Kind_t (``GT)))
+let mult = C_int (get_int (enum_to_int `Kind_t (``MULT)))
+let plus = C_int (get_int (enum_to_int `Kind_t (``PLUS)))
+let and_kind = C_int (get_int (enum_to_int `Kind_t (``AND)))
+let implies = C_int (get_int (enum_to_int `Kind_t (``IMPLIES)))
+
+(* gt = 35, but the parser screws up if we put "geq" what follows *)
+let x_positive = em->mkExpr(gt, x, zero)
+let y_positive = em->mkExpr(gt, y, zero)
+
+let integerTwo = new_Integer '("2", 10)
+let two = em->mkConst(integerTwo)
+let twox = em->mkExpr(mult, two, x)
+let twox_plus_y = em->mkExpr(plus, twox, y)
+
+let integerThree = new_Integer '("3", 10)
+let three = em->mkConst(integerThree)
+let twox_plus_y_geq_3 = em->mkExpr(geq, twox_plus_y, three)
+
+let lhs = em->mkExpr(and_kind, x_positive, y_positive)
+
+(* This fails for some reason. *)
+(* let rhs = new_BoolExpr(twox_plus_y_geq_3)
+   let formula = new_BoolExpr(lhs)->impExpr(rhs) *)
+
+let formula = em->mkExpr(implies, lhs, twox_plus_y_geq_3)
+
+let bformula = new_BoolExpr(formula) in
+
+print_string "Checking validity of formula " ;
+print_string (get_string (formula->toString ())) ;
+print_string " with CVC4." ;
+print_newline () ;
+print_string "CVC4 should report VALID." ;
+print_newline () ;
+print_string "Result from CVC4 is: " ;
+print_string (get_string (smt->query(bformula)->toString ())) ;
+print_newline ()
+;;
diff --git a/examples/simple_vc_compat_c.c b/examples/simple_vc_compat_c.c
index 9bcb52280..f45df65f5 100644
--- a/examples/simple_vc_compat_c.c
+++ b/examples/simple_vc_compat_c.c
@@ -21,14 +21,14 @@
 #include <stdio.h>
 #include <stdlib.h>
 
-// #include <cvc4/compat/c_interface.h>
+/* #include <cvc4/compat/c_interface.h> /* use this after CVC4 is properly installed */
 #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
+  /* Prove that for integers x and y:
+   *   x > 0 AND y > 0  =>  2x + y >= 3 */
 
   Type integer = vc_intType(vc);
 
diff --git a/examples/simple_vc_compat_cxx.cpp b/examples/simple_vc_compat_cxx.cpp
index c178d1aba..0cb99f4be 100644
--- a/examples/simple_vc_compat_cxx.cpp
+++ b/examples/simple_vc_compat_cxx.cpp
@@ -25,7 +25,7 @@
 
 #include <iostream>
 
-// #include <cvc4/compat/cvc3_compat.h>
+// #include <cvc4/compat/cvc3_compat.h> // use this after CVC4 is properly installed
 #include "compat/cvc3_compat.h"
 
 using namespace std;
diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp
index 3b5db7c02..819b1fc97 100644
--- a/examples/simple_vc_cxx.cpp
+++ b/examples/simple_vc_cxx.cpp
@@ -20,7 +20,7 @@
 
 #include <iostream>
 
-//#include <cvc4.h>
+//#include <cvc4.h> // use this after CVC4 is properly installed
 #include "smt/smt_engine.h"
 
 using namespace std;
diff --git a/src/Makefile.am b/src/Makefile.am
index 627a89a67..7112d5a55 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -137,6 +137,8 @@ uninstall-local:
 		fi; \
 		d="$$(echo "$$f" | sed 's,^include/,,')"; \
 		rm -f "$(DESTDIR)$(includedir)/cvc4/$$d"; \
-		rmdir -p "$$(dirname "$(DESTDIR)$(includedir)/cvc4/$$d")" 2>/dev/null; \
 	done
+	-rmdir "$(DESTDIR)$(includedir)/cvc4/bindings/compat"
+	-rmdir "$(DESTDIR)$(includedir)/cvc4/bindings"
 	-rmdir "$(DESTDIR)$(includedir)/cvc4"
+	-rmdir "$(DESTDIR)$(libdir)/ocaml/cvc4"
diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index 53c29ff02..35b3a6e07 100644
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -19,9 +19,12 @@ AM_CXXFLAGS = -Wall
 
 SUBDIRS = . compat
 
-javadatadir = $(datadir)/java
 lib_LTLIBRARIES =
+bin_PROGRAMS =
+javadatadir = $(datadir)/java
+ocamldatadir = $(libdir)/ocaml/cvc4
 javadata_DATA =
+ocamldata_DATA =
 if CVC4_LANGUAGE_BINDING_JAVA
 lib_LTLIBRARIES += libcvc4bindings_java.la
 javadata_DATA += cvc4.jar
@@ -65,6 +68,8 @@ libcvc4bindings_python_la_LIBADD = \
 endif
 if CVC4_LANGUAGE_BINDING_OCAML
 lib_LTLIBRARIES += libcvc4bindings_ocaml.la
+bin_PROGRAMS += cvc4_ocaml_top
+ocamldata_DATA += ocaml/swig.cmo ocaml/swig.cmi ocaml/swigp4.cmo ocaml/swigp4.cmi ocaml/CVC4.cmo ocaml/CVC4.cmi
 libcvc4bindings_ocaml_la_LDFLAGS = \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
 libcvc4bindings_ocaml_la_LIBADD = \
@@ -126,6 +131,8 @@ cvc4.jar: java.cpp
 	cd classes); \
 	$(JAR) cf $@ -C java/classes .
 java.cpp:
+perl.lo: csharp.cpp
+	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(CSHARP_CPPFLAGS) -o $@ $<
 csharp.cpp:
 perl.lo: perl.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(PERL_CPPFLAGS) -o $@ $<
@@ -136,10 +143,25 @@ php.cpp:
 python.lo: python.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(PYTHON_CPPFLAGS) -o $@ $<
 python.cpp:
+ocaml.lo: ocaml.cpp
+	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(OCAML_CPPFLAGS) -o $@ $<
+ocaml/swig.cmo: ocaml/swig.ml ocaml/swig.cmi; $(AM_V_GEN)$(OCAMLC) -I ocaml -c -o $@ $<
+ocaml/swig.cmi: ocaml/swig.mli; $(AM_V_GEN)$(OCAMLC) -I ocaml -c -o $@ $<
+ocaml/CVC4.cmo: ocaml/CVC4.ml ocaml/CVC4.cmi; $(AM_V_GEN)$(OCAMLC) -I ocaml -c -o $@ $<
+ocaml/CVC4.cmi: ocaml/CVC4.mli; $(AM_V_GEN)$(OCAMLC) -I ocaml -c -o $@ $<
+ocaml/swigp4.cmo: ocaml/swigp4.ml; $(AM_V_GEN)$(OCAMLFIND) ocamlc -package camlp4 -pp "$(CAMLP4O) pa_extend.cmo q_MLast.cmo" -o $@ -c $<
+ocaml/swig.ml:; $(AM_V_GEN)cd ocaml && $(SWIG) -ocaml -co swig.ml
+ocaml/swig.mli:; $(AM_V_GEN)cd ocaml && $(SWIG) -ocaml -co swig.mli
+ocaml/swigp4.ml:; $(AM_V_GEN)cd ocaml && $(SWIG) -ocaml -co swigp4.ml
 ocaml.cpp:
+cvc4_ocaml_top: libcvc4bindings_ocaml.la ocaml/swig.cmo ocaml/swig.cmi ocaml/swigp4.cmo ocaml/CVC4.cmo ocaml/CVC4.cmi
+	$(AM_V_GEN)\
+	$(OCAMLFIND) ocamlmktop -I $(ocamldatadir) -custom -o cvc4_ocaml_top -package camlp4 dynlink.cma camlp4o.cma ocaml/swig.cmo ocaml/swigp4.cmo ocaml/CVC4.cmo -cclib -L.libs -cclib -L. -cclib -lcvc4bindings_ocaml -cclib -lstdc++
 ruby.lo: ruby.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(RUBY_CPPFLAGS) -o $@ $<
 ruby.cpp:
+tcl.lo: tcl.cpp
+	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(TCL_CPPFLAGS) -o $@ $<
 tcl.cpp:
 java.cpp: @srcdir@/../cvc4.i
 	$(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@)
diff --git a/src/cvc4.i b/src/cvc4.i
index 8a8157699..7723aee6e 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -1,4 +1,5 @@
 %import "bindings/swig.h"
+
 %include "stdint.i"
 %include "stl.i"
 
@@ -20,6 +21,19 @@ namespace std {
 #  undef seed
 #endif /* SWIGPERL */
 
+// OCaml's headers define "invalid_argument" and "flush" to
+// caml_invalid_argument and caml_flush, which breaks C++
+// standard headers; undo this damage
+//
+// Unfortunately, this doesn't happen early enough.  swig puts an
+// include <stdexcept> very early, which breaks linking due to a
+// nonexistent std::caml_invalid_argument symbol.. ridiculous!
+//
+#ifdef SWIGOCAML
+#  undef flush
+#  undef invalid_argument
+#endif /* SWIGOCAML */
+
 namespace CVC4 {}
 using namespace CVC4;
 
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index b4d2051e3..375976330 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -2,6 +2,19 @@
 #include "expr/expr_manager.h"
 %}
 
+#ifdef SWIGOCAML
+  /* OCaml bindings cannot deal with this degree of overloading */
+  %ignore CVC4::ExprManager::mkExpr(Kind, const std::vector<Expr>&);
+  %ignore CVC4::ExprManager::mkExpr(Kind, Expr, const std::vector<Expr>&);
+  %ignore CVC4::ExprManager::mkExpr(Expr);
+  %ignore CVC4::ExprManager::mkExpr(Expr, Expr);
+  %ignore CVC4::ExprManager::mkExpr(Expr, Expr, Expr);
+  %ignore CVC4::ExprManager::mkExpr(Expr, Expr, Expr, Expr);
+  %ignore CVC4::ExprManager::mkExpr(Expr, Expr, Expr, Expr, Expr);
+  %ignore CVC4::ExprManager::mkExpr(Expr, Expr, Expr, Expr, Expr, Expr);
+  %ignore CVC4::ExprManager::mkExpr(Expr, const std::vector<Expr>&);
+#endif /* SWIGOCAML */
+
 %include "expr/expr_manager.h"
 
 %template(mkConst) CVC4::ExprManager::mkConst< CVC4::Integer >;
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 6810d3a94..09e072370 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -173,7 +173,7 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
   }
 
   // We will translate clauses, so remember the level
-  int level = d_satSolver->getLevel();
+  int level = d_satSolver->getAssertionLevel();
   d_translationCache[node].level = level;
   d_translationCache[node.notNode()].level = level;
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 3d5a27d00..8663a2f68 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -171,7 +171,7 @@ Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) {
   return Result(result == l_True ? Result::SAT : Result::UNSAT);
 }
 
-Node PropEngine::getValue(TNode node) {
+Node PropEngine::getValue(TNode node) const {
   Assert(node.getType().isBoolean());
   SatLiteral lit = d_cnfStream->getLiteral(node);
 
@@ -186,15 +186,15 @@ Node PropEngine::getValue(TNode node) {
   }
 }
 
-bool PropEngine::isSatLiteral(TNode node) {
+bool PropEngine::isSatLiteral(TNode node) const {
   return d_cnfStream->hasLiteral(node);
 }
 
-bool PropEngine::isTranslatedSatLiteral(TNode node) {
+bool PropEngine::isTranslatedSatLiteral(TNode node) const {
   return d_cnfStream->isTranslated(node);
 }
 
-bool PropEngine::hasValue(TNode node, bool& value) {
+bool PropEngine::hasValue(TNode node, bool& value) const {
   Assert(node.getType().isBoolean());
   SatLiteral lit = d_cnfStream->getLiteral(node);
 
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 25697b856..0b5be4647 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -206,24 +206,24 @@ public:
    * @return mkConst<true>, mkConst<false>, or Node::null() if
    * unassigned.
    */
-  Node getValue(TNode node);
+  Node getValue(TNode node) const;
 
   /**
    * Return true if node has an associated SAT literal.
    */
-  bool isSatLiteral(TNode node);
+  bool isSatLiteral(TNode node) const;
 
   /**
    * Return true if node has an associated SAT literal that is
    * currently translated (i.e., it's relevant to the current
    * user push/pop level).
    */
-  bool isTranslatedSatLiteral(TNode node);
+  bool isTranslatedSatLiteral(TNode node) const;
 
   /**
    * Check if the node has a value and return it if yes.
    */
-  bool hasValue(TNode node, bool& value);
+  bool hasValue(TNode node, bool& value) const;
 
   /**
    * Ensure that the given node will have a designated SAT literal
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 13b32f18d..be3ed244b 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -108,8 +108,8 @@ public:
   virtual void addClause(SatClause& clause, bool removable) = 0;
   /** Create a new boolean variable in the solver. */
   virtual SatVariable newVar(bool theoryAtom = false) = 0;
-  /** Get the current decision level of the solver */
-  virtual int getLevel() const = 0;
+  /** Get the current user assertion level of the solver */
+  virtual int getAssertionLevel() const = 0;
   /** Unregister the variable (of the literal) from solving */
   virtual void unregisterVar(SatLiteral lit) = 0;
   /** Register the variable (of the literal) for solving */
@@ -240,7 +240,7 @@ public:
   /** Call modelValue() when the search is done.*/
   SatLiteralValue modelValue(SatLiteral l);
 
-  int getLevel() const;
+  int getAssertionLevel() const;
 
   void push();
 
@@ -341,7 +341,7 @@ inline void SatSolver::pop() {
   d_minisat->pop();
 }
 
-inline int SatSolver::getLevel() const {
+inline int SatSolver::getAssertionLevel() const {
   return d_minisat->getAssertionLevel();
 }
 
diff --git a/src/util/datatype.i b/src/util/datatype.i
index 23782aa28..34e890214 100644
--- a/src/util/datatype.i
+++ b/src/util/datatype.i
@@ -8,14 +8,26 @@ namespace CVC4 {
 }
 
 %extend std::vector< CVC4::Datatype > {
-  %ignore vector(size_type);
-  %ignore resize(size_type);
+  /* These member functions have slightly different signatures in
+   * different swig language packages.  The underlying issue is that
+   * Datatype::Constructor doesn't have a default constructor */
+  %ignore vector(unsigned int size = 0);// ocaml
+  %ignore set( int i, const CVC4::Datatype &x );// ocaml
+  %ignore to_array();// ocaml
+  %ignore vector(size_type);// java/python
+  %ignore resize(size_type);// java/python
 };
 %template(vectorDatatype) std::vector< CVC4::Datatype >;
 
 %extend std::vector< CVC4::Datatype::Constructor > {
-  %ignore vector(size_type);
-  %ignore resize(size_type);
+  /* These member functions have slightly different signatures in
+   * different swig language packages.  The underlying issue is that
+   * Datatype::Constructor doesn't have a default constructor */
+  %ignore vector(unsigned int size = 0);// ocaml
+  %ignore set( int i, const CVC4::Datatype::Constructor &x );// ocaml
+  %ignore to_array();// ocaml
+  %ignore vector(size_type);// java/python
+  %ignore resize(size_type);// java/python
 };
 %template(vectorDatatypeConstructor) std::vector< CVC4::Datatype::Constructor >;
 
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index 2fe6c0210..8520dacd8 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -71,7 +71,7 @@ public:
     return d_addClauseCalled;
   }
 
-  int getLevel() const {
+  int getAssertionLevel() const {
     return 0;
   }