From 78af7dfd469b43c17c3ad582a094068484955037 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 15 Nov 2011 22:34:18 +0000 Subject: [PATCH] Bindings work (ocaml bindings are now sort of working); also minor cleanup --- config/bindings.m4 | 43 +++++++++++++-- examples/Makefile.am | 1 + examples/SimpleVC.ml | 91 +++++++++++++++++++++++++++++++ examples/simple_vc_compat_c.c | 6 +- examples/simple_vc_compat_cxx.cpp | 2 +- examples/simple_vc_cxx.cpp | 2 +- src/Makefile.am | 4 +- src/bindings/Makefile.am | 24 +++++++- src/cvc4.i | 14 +++++ src/expr/expr_manager.i | 13 +++++ src/prop/cnf_stream.cpp | 2 +- src/prop/prop_engine.cpp | 8 +-- src/prop/prop_engine.h | 8 +-- src/prop/sat.h | 8 +-- src/util/datatype.i | 20 +++++-- test/unit/prop/cnf_stream_black.h | 2 +- 16 files changed, 219 insertions(+), 29 deletions(-) create mode 100644 examples/SimpleVC.ml 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 #include -// #include +/* #include /* 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 -// #include +// #include // 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 -//#include +//#include // 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 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&); + %ignore CVC4::ExprManager::mkExpr(Kind, Expr, const std::vector&); + %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&); +#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, mkConst, 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; } -- 2.30.2