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])
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
EXTRA_DIST = \
SimpleVC.java \
SimpleVC.py \
+ SimpleVC.ml \
SimpleVCCompat.java \
README
--- /dev/null
+(********************* **
+**! \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 ()
+;;
#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);
#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;
#include <iostream>
-//#include <cvc4.h>
+//#include <cvc4.h> // use this after CVC4 is properly installed
#include "smt/smt_engine.h"
using namespace std;
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"
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
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 = \
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 $@ $<
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,%,$@)
%import "bindings/swig.h"
+
%include "stdint.i"
%include "stl.i"
# 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;
#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 >;
}
// 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;
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);
}
}
-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);
* @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
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 */
/** Call modelValue() when the search is done.*/
SatLiteralValue modelValue(SatLiteral l);
- int getLevel() const;
+ int getAssertionLevel() const;
void push();
d_minisat->pop();
}
-inline int SatSolver::getLevel() const {
+inline int SatSolver::getAssertionLevel() const {
return d_minisat->getAssertionLevel();
}
}
%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 >;
return d_addClauseCalled;
}
- int getLevel() const {
+ int getAssertionLevel() const {
return 0;
}
projects / cvc5.git / commitdiff