diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Makefile.am | 4 | ||||
| -rw-r--r-- | src/bindings/Makefile.am | 24 | ||||
| -rw-r--r-- | src/cvc4.i | 14 | ||||
| -rw-r--r-- | src/expr/expr_manager.i | 13 | ||||
| -rw-r--r-- | src/prop/cnf_stream.cpp | 2 | ||||
| -rw-r--r-- | src/prop/prop_engine.cpp | 8 | ||||
| -rw-r--r-- | src/prop/prop_engine.h | 8 | ||||
| -rw-r--r-- | src/prop/sat.h | 8 | ||||
| -rw-r--r-- | src/util/datatype.i | 20 |
9 files changed, 82 insertions, 19 deletions
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 >; |