fix some Java compatibility-layer interface problems; also fix some Mac OS X build...

diff --git a/src/bindings/compat/java/Makefile.am b/src/bindings/compat/java/Makefile.am
index 7c22e6231cc81c00f6ceebf3cbb5b14784b1748d..d268d4d7698ab918fc773ef4bea1579ae670700a 100644 (file)
--- a/src/bindings/compat/java/Makefile.am
+++ b/src/bindings/compat/java/Makefile.am
@@ -14,7 +14,8 @@ LIBCVC4BINDINGS_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@
 
 AM_CPPFLAGS = \
        -D__BUILDING_CVC4BINDINGSLIB \
-       -I@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../.. -I@builddir@/cvc3
+       -I@srcdir@/../../../include -I@srcdir@/../../.. \
+       -I@srcdir@/include/cvc3 -I@builddir@/../../.. -I@builddir@/cvc3
 AM_CXXFLAGS = -Wall
 
 javadatadir = $(datadir)/java
@@ -25,10 +26,12 @@ BUILT_SOURCES =
 if CVC4_LANGUAGE_BINDING_JAVA
 
 lib_LTLIBRARIES += libcvc4bindings_java_compat.la
-javadata_DATA += cvc4compat.jar
+javadata_DATA += CVC4compat.jar
 libcvc4bindings_java_compat_la_LDFLAGS = \
        -version-info $(LIBCVC4BINDINGS_VERSION)
 libcvc4bindings_java_compat_la_LIBADD = \
+       -L@builddir@/../../.. -lcvc4 \
+       -L@builddir@/../../../parser -lcvc4parser \
        -L@builddir@/../../../compat -lcvc4compat
 BUILT_SOURCES += $(JNI_CPP_FILES)
 
@@ -37,7 +40,6 @@ endif
 # source files
 # java files of the library wrapper
 LIB_FILES = \
-       JniUtils \
        Cvc3Exception \
        TypecheckException \
        SoundException \
@@ -80,48 +82,44 @@ TEST_FILES = Test
 # java files of the stand alone program
 PROG_FILES = TimeoutHandler Cvc3
 # all java files, library and stand alone
-JAVA_FILES = $(LIB_FILES) $(TEST_FILES) $(PROG_FILES)
-# jni files of the library wrapper
-JNI_FILES = \
-       EmbeddedManager \
-       Expr \
-       ExprMut \
-       ExprManager \
-       Type \
-       TypeMut \
-       Op \
-       OpMut \
-       Rational \
-       RationalMut \
-       Theorem \
-       TheoremMut \
-       Proof \
-       ProofMut \
-       Context \
-       ContextMut \
-       Flag \
-       Flags \
-       FlagsMut \
-       Statistics \
-       StatisticsMut \
-       ValidityChecker
-
-# stub files
-IMPL_FILES = $(patsubst %,src/cvc3/%_impl.cpp,$(JNI_FILES))
+JAVA_FILES = JniUtils $(LIB_FILES) $(TEST_FILES) $(PROG_FILES)
 # generated files
-JNI_CPP_FILES = $(patsubst %,%.cpp,$(JNI_FILES))
+JNI_CPP_FILES = \
+       EmbeddedManager.cpp \
+       Expr.cpp \
+       ExprMut.cpp \
+       ExprManager.cpp \
+       ValidityChecker.cpp
+#      Type.cpp \
+#      TypeMut.cpp \
+#      Op.cpp \
+#      OpMut.cpp \
+#      Rational.cpp \
+#      RationalMut.cpp \
+#      Theorem.cpp \
+#      TheoremMut.cpp \
+#      Proof.cpp \
+#      ProofMut.cpp \
+#      Context.cpp \
+#      ContextMut.cpp \
+#      Flag.cpp \
+#      Flags.cpp \
+#      FlagsMut.cpp \
+#      Statistics.cpp \
+#      StatisticsMut.cpp \
 # non-generated files
 SRC_CPP_FILES = src/cvc3/JniUtils.cpp
 # all cpp files (to compile)
 CPP_FILES = $(SRC_CPP_FILES) $(JNI_CPP_FILES)
 
-dist_libcvc4bindings_java_compat_la_SOURCES = $(SRC_CPP_FILES) $(IMPL_FILES) include/cvc3/JniUtils.h
+dist_libcvc4bindings_java_compat_la_SOURCES = $(SRC_CPP_FILES) include/cvc3/JniUtils.h
 nodist_libcvc4bindings_java_compat_la_SOURCES = $(JNI_CPP_FILES)
 
 EXTRA_DIST = \
        formula_value.h \
        create_impl.py \
        Cvc3_manifest \
+       $(SRC_CPP_FILES:%=src/cvc3/%_impl.cpp) \
        $(JAVA_FILES:%=src/cvc3/%.java)
 
 # compile each cpp file
@@ -134,7 +132,7 @@ $(JNI_CPP_FILES): %.cpp: src/cvc3/%_impl.cpp $(builddir)/cvc3/%.h include/cvc3/J
 JniUtils.lo: src/cvc3/JniUtils.cpp .headers
        $(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_INCLUDES) $(JAVA_CPPFLAGS) -I . -o $@ $<
 
-$(LIB_FILES:%=classes/cvc3/%.class): .classes
+$(LIB_FILES:%=classes/cvc3/%.class) classes/cvc3/JniUtils.class: .classes
 .classes:
        $(AM_V_GEN)mkdir -p classes && $(JAVAC) -source 1.4 -sourcepath $(srcdir)/src -d classes $(LIB_FILES:%=$(srcdir)/src/cvc3/%.java)
        @touch .classes
@@ -144,9 +142,9 @@ $(LIB_FILES:%=cvc3/%.h): %.h: classes/%.class .cvc3dir
        $(AM_V_GEN)$(JAVAH) -jni -force -classpath classes -o $@ cvc3.$(@:cvc3/%.h=%)
 .cvc3dir:
        @mkdir -p cvc3 && touch $@
-cvc4compat.jar: $(LIB_FILES:%=classes/cvc3/%.class)
+CVC4compat.jar: $(LIB_FILES:%=classes/cvc3/%.class) classes/cvc3/JniUtils.class
        $(AM_V_GEN)$(JAR) cf $@ -C classes .
 
 clean-local:
        rm -fr classes cvc3
-MOSTLYCLEANFILES = .cvc3dir .classes .headers cvc4compat.jar $(JNI_CPP_FILES)
+MOSTLYCLEANFILES = .cvc3dir .classes .headers CVC4compat.jar $(JNI_CPP_FILES)

diff --git a/src/bindings/compat/java/include/cvc3/JniUtils.h b/src/bindings/compat/java/include/cvc3/JniUtils.h
index c6bcc04f854833cbeb3dd213d5c67a4e945ecc2e..d4688fc25dfe3deec7867aad1dc5095a02881485 100644 (file)
--- a/src/bindings/compat/java/include/cvc3/JniUtils.h
+++ b/src/bindings/compat/java/include/cvc3/JniUtils.h
@@ -244,7 +244,7 @@ namespace Java_cvc3_JniUtils {
 
 
   // hash map
-  template <class K, class V> jobjectArray toJavaHCopy(JNIEnv* env, const Hash::hash_map<K, V>& hm) {
+  /*template <class K, class V> jobjectArray toJavaHCopy(JNIEnv* env, const Hash::hash_map<K, V>& hm) {
     jobjectArray jarray = (jobjectArray)
       env->NewObjectArray(
        hm.size() * 2,
@@ -262,7 +262,7 @@ namespace Java_cvc3_JniUtils {
       ++i;
     }
     return jarray;
-  }
+  }*/
 
   template <class V> jobjectArray toJavaHCopy(JNIEnv* env, const CVC3::ExprMap<V>& hm) {
     jobjectArray jarray = (jobjectArray)

diff --git a/src/bindings/compat/java/src/cvc3/Embedded.java b/src/bindings/compat/java/src/cvc3/Embedded.java
index c645f265508a11b3d616524f9bb8ed74b4a846eb..fdeeef058517e9f99fe4591676f2a580b87520b5 100644 (file)
--- a/src/bindings/compat/java/src/cvc3/Embedded.java
+++ b/src/bindings/compat/java/src/cvc3/Embedded.java
@@ -12,6 +12,8 @@ public abstract class Embedded {
 
     // load jni c++ library
     static {
+        System.loadLibrary("cvc4");
+        System.loadLibrary("cvc4parser");
         System.loadLibrary("cvc4bindings_java_compat");
 
        /*

diff --git a/src/bindings/compat/java/src/cvc3/Expr_impl.cpp b/src/bindings/compat/java/src/cvc3/Expr_impl.cpp
index 58c26eb038e7286dd55342f6ebccb9018ea3fcfa..f002109c54a8e084267d3b5f96a971fe3c843dfa 100644 (file)
--- a/src/bindings/compat/java/src/cvc3/Expr_impl.cpp
+++ b/src/bindings/compat/java/src/cvc3/Expr_impl.cpp
@@ -1,7 +1,7 @@
-INCLUDE: <expr.h>
-INCLUDE: <theory_array.h>
-INCLUDE: <theory_arith.h>
-INCLUDE: <theory_bitvector.h>
+//INCLUDE: <expr.h>
+//INCLUDE: <theory_array.h>
+//INCLUDE: <theory_arith.h>
+//INCLUDE: <theory_bitvector.h>
 
 DEFINITION: Java_cvc3_Expr_jniEquals
 jboolean c Expr expr1 c Expr expr2
@@ -282,7 +282,7 @@ return expr->arity();
 
 DEFINITION: Java_cvc3_Expr_jniGetKid
 jobject c Expr expr n int i
-return embed_const_ref<Expr>(env, &((*expr)[ji]));
+return embed_copy<Expr>(env, (*expr)[ji]);
 
 DEFINITION: Java_cvc3_Expr_jniGetKids
 jobjectArray c Expr expr

diff --git a/src/bindings/compat/java/src/cvc3/JniUtils.cpp b/src/bindings/compat/java/src/cvc3/JniUtils.cpp
index f291b221b5ccde3d23527c8e5acdd0e2bf6af9dc..9ae2023f61b1100535586a4edbaf91b3e6fe2ab7 100644 (file)
--- a/src/bindings/compat/java/src/cvc3/JniUtils.cpp
+++ b/src/bindings/compat/java/src/cvc3/JniUtils.cpp
@@ -19,7 +19,7 @@ namespace Java_cvc3_JniUtils {
 
   /// Embedding of c++ objects in java objects
 
-  /*Embedded* unembed(JNIEnv* env, jobject jobj) {
+  Embedded* unembed(JNIEnv* env, jobject jobj) {
     Embedded* embedded = (Embedded*) env->GetDirectBufferAddress(jobj);
     DebugAssert(embedded != NULL, "JniUtils::unembed: embedded object is NULL");
     return embedded;
@@ -29,7 +29,7 @@ namespace Java_cvc3_JniUtils {
     Embedded* embedded = unembed(env, jobj);
     DebugAssert(embedded != NULL, "JniUtils::deleteEmbedded: embedded object is NULL");
     delete embedded;
-  }*/
+  }
 
 
 

diff --git a/src/bindings/compat/java/src/cvc3/Type_impl.cpp b/src/bindings/compat/java/src/cvc3/Type_impl.cpp
index ce201fa1582a51ffd024223aa8ca66dfb99914e7..769ce984a65a26eae039b46f8eccdc46e3714730 100644 (file)
--- a/src/bindings/compat/java/src/cvc3/Type_impl.cpp
+++ b/src/bindings/compat/java/src/cvc3/Type_impl.cpp
@@ -1,8 +1,8 @@
-INCLUDE: "kinds.h"
-INCLUDE: "type.h"
-INCLUDE: "theory_array.h"
-INCLUDE: "theory_bitvector.h"
-INCLUDE: "theory_datatype.h"
+//INCLUDE: "kinds.h"
+//INCLUDE: "type.h"
+//INCLUDE: "theory_array.h"
+//INCLUDE: "theory_bitvector.h"
+//INCLUDE: "theory_datatype.h"
 
 DEFINITION: Java_cvc3_Type_jniConstr
 jobject c Expr expr

diff --git a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
index e27e44913ef90097dca6eac991383ef1df8c1364..34feaacbb25e107403564738dc5e6b51bb2cfc08 100644 (file)
--- a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
+++ b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
@@ -1,14 +1,14 @@
 INCLUDE: <sstream>
-INCLUDE: <theory_arith.h>
-INCLUDE: <theory_array.h>
+//INCLUDE: <theory_arith.h>
+//INCLUDE: <theory_array.h>
 
 DEFINITION: Java_cvc3_ValidityChecker_jniCreate1
 jobject
-return embed_own<ValidityChecker>(env, VCL::create());
+return embed_own<ValidityChecker>(env, ValidityChecker::create());
 
 DEFINITION: Java_cvc3_ValidityChecker_jniCreate2
 jobject c CLFlags flags
-return embed_own<ValidityChecker>(env, VCL::create(*flags));
+return embed_own<ValidityChecker>(env, ValidityChecker::create(*flags));
 
 
 
@@ -86,11 +86,11 @@ return toJavaVCopy(env, result);
 
 DEFINITION: Java_cvc3_ValidityChecker_jniAnyType
 jobject m ValidityChecker vc
-return embed_copy(env, Type::anyType(vc->getEM()));
+Unimplemented();
 
 DEFINITION: Java_cvc3_ValidityChecker_jniArrayLiteral
 jobject m ValidityChecker vc c Expr indexVar c Expr bodyExpr
-return embed_copy(env, CVC3::arrayLiteral(*indexVar, *bodyExpr));
+Unimplemented();
 
 DEFINITION: Java_cvc3_ValidityChecker_jniArrayType
 jobject m ValidityChecker vc c Type typeIndex c Type typeData

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 83c33c7ab098ce475c402f5c0955e0396237af2f..16169c10a4b141edf195c32f92c20fa01c0a4f87 100644 (file)
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -225,6 +225,10 @@ Expr::Expr(const Expr& e) : CVC4::Expr(e) {
 Expr::Expr(const CVC4::Expr& e) : CVC4::Expr(e) {
 }
 
+Expr::Expr(const CVC4::Kind k) : CVC4::Expr() {
+  *this = getEM()->operatorOf(k);
+}
+
 Expr Expr::eqExpr(const Expr& right) const {
   return getEM()->mkExpr(CVC4::kind::EQUAL, *this, right);
 }
@@ -321,6 +325,22 @@ bool Expr::isString() const {
   return false;
 }
 
+bool Expr::isBoundVar() const {
+  Unimplemented();
+}
+
+bool Expr::isLambda() const {
+  Unimplemented();
+}
+
+bool Expr::isClosure() const {
+  Unimplemented();
+}
+
+bool Expr::isQuantifier() const {
+  Unimplemented();
+}
+
 bool Expr::isApply() const {
   return hasOperator();
 }
@@ -404,7 +424,7 @@ std::vector< std::vector<Expr> > Expr::getTriggers() const {
 }
 
 ExprManager* Expr::getEM() const {
-  return getExprManager();
+  return reinterpret_cast<ExprManager*>(getExprManager());
 }
 
 std::vector<Expr> Expr::getKids() const {
@@ -709,7 +729,7 @@ ValidityChecker::ValidityChecker() :
   d_clflags(new CLFlags()),
   d_options() {
   setUpOptions(d_options, *d_clflags);
-  d_em = new CVC4::ExprManager(d_options);
+  d_em = reinterpret_cast<ExprManager*>(new CVC4::ExprManager(d_options));
   d_smt = new CVC4::SmtEngine(d_em);
   d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build();
 }
@@ -718,7 +738,7 @@ ValidityChecker::ValidityChecker(const CLFlags& clflags) :
   d_clflags(new CLFlags(clflags)),
   d_options() {
   setUpOptions(d_options, *d_clflags);
-  d_em = new CVC4::ExprManager(d_options);
+  d_em = reinterpret_cast<ExprManager*>(new CVC4::ExprManager(d_options));
   d_smt = new CVC4::SmtEngine(d_em);
   d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build();
 }

diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h
index beef53006d3b0abd9c7d91f7ce788f008ff6cc23..eae8412cf4101488230bf0020e8ac259f9910223 100644 (file)
--- a/src/compat/cvc3_compat.h
+++ b/src/compat/cvc3_compat.h
@@ -82,6 +82,20 @@
 
 namespace CVC3 {
 
+const CVC4::Kind EQ = CVC4::kind::EQUAL;
+const CVC4::Kind LE = CVC4::kind::LEQ;
+const CVC4::Kind GE = CVC4::kind::GEQ;
+const CVC4::Kind DIVIDE = CVC4::kind::DIVISION;
+const CVC4::Kind BVLT = CVC4::kind::BITVECTOR_ULT;
+const CVC4::Kind BVLE = CVC4::kind::BITVECTOR_ULE;
+const CVC4::Kind BVGT = CVC4::kind::BITVECTOR_UGT;
+const CVC4::Kind BVGE = CVC4::kind::BITVECTOR_UGE;
+const CVC4::Kind BVPLUS = CVC4::kind::BITVECTOR_PLUS;
+const CVC4::Kind BVSUB = CVC4::kind::BITVECTOR_SUB;
+const CVC4::Kind BVCONST = CVC4::kind::CONST_BITVECTOR;
+const CVC4::Kind EXTRACT = CVC4::kind::BITVECTOR_EXTRACT;
+const CVC4::Kind CONCAT = CVC4::kind::BITVECTOR_CONCAT;
+
 std::string int2string(int n);
 
 //! Different types of command line flags
@@ -227,10 +241,11 @@ public:
 
 };/* class CLFlags */
 
+class ExprManager;
 class Context;
 class Proof {};
+class Theorem {};
 
-using CVC4::ExprManager;
 using CVC4::InputLanguage;
 using CVC4::Integer;
 using CVC4::Rational;
@@ -318,6 +333,7 @@ public:
   Expr();
   Expr(const Expr& e);
   Expr(const CVC4::Expr& e);
+  Expr(CVC4::Kind k);
 
   // Compound expression constructors
   Expr eqExpr(const Expr& right) const;
@@ -348,12 +364,40 @@ public:
   bool isTrue() const;
   bool isBoolConst() const;
   bool isVar() const;
+  bool isBoundVar() const;
   bool isString() const;
+  bool isSymbol() const;
+  bool isTerm() const;
+  bool isType() const;
+  bool isClosure() const;
+  bool isQuantifier() const;
+  bool isForall() const;
+  bool isExists() const;
+  bool isLambda() const;
   bool isApply() const;
   bool isTheorem() const;
   bool isConstant() const;
   bool isRawList() const;
 
+  bool isAtomic() const;
+  bool isAtomicFormula() const;
+  bool isAbsAtomicFormula() const;
+  bool isLiteral() const;
+  bool isAbsLiteral() const;
+  bool isBoolConnective() const;
+  bool isPropLiteral() const;
+  bool isPropAtom() const;
+
+  const std::string& getName() const;
+  const std::string& getUid() const;
+
+  const std::string& getString() const;
+  const std::vector<Expr>& getVars() const;
+  const Expr& getExistential() const;
+  int getBoundIndex() const;
+  const Expr& getBody() const;
+  const Theorem& getTheorem() const;
+
   bool isEq() const;
   bool isNot() const;
   bool isAnd() const;
@@ -366,7 +410,7 @@ public:
   bool isRational() const;
   bool isSkolem() const;
 
-  Rational getRational() const;
+  const Rational& getRational() const;
 
   Op mkOp() const;
   Op getOp() const;
@@ -407,8 +451,24 @@ public:
   //! Look up the current type. Do not recursively compute (i.e. may be NULL)
   Type lookupType() const;
 
+  //! Pretty-print the expression
+  void pprint() const;
+  //! Pretty-print without dagifying
+  void pprintnodag() const;
+
 };/* class CVC3::Expr */
 
+bool isArrayLiteral(const Expr&);
+
+class ExprManager : public CVC4::ExprManager {
+public:
+  const std::string& getKindName(int kind);
+  //! Get the input language for printing
+  InputLanguage getInputLang() const;
+  //! Get the output language for printing
+  InputLanguage getOutputLang() const;
+};/* class CVC3::ExprManager */
+
 typedef CVC4::StatisticsRegistry Statistics;
 
 #define PRESENTATION_LANG ::CVC4::language::input::LANG_CVC4
@@ -464,7 +524,7 @@ class CVC4_PUBLIC ValidityChecker {
 
   CLFlags* d_clflags;
   CVC4::Options d_options;
-  CVC4::ExprManager* d_em;
+  CVC3::ExprManager* d_em;
   CVC4::SmtEngine* d_smt;
   CVC4::parser::Parser* d_parserContext;
 

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 533a4dd7f54a98b7a275d63526bfada5e0ddda3a..8819684fc4c9d075545e83ea830ff02e32877578 100644 (file)
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -463,6 +463,16 @@ Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) {
   }
 }
 
+bool ExprManager::hasOperator(Kind k) {
+  return NodeManager::hasOperator(k);
+}
+
+Expr ExprManager::operatorOf(Kind k) {
+  NodeManagerScope nms(d_nodeManager);
+
+  return d_nodeManager->operatorOf(k).toExpr();
+}
+
 /** Make a function type from domain to range. */
 FunctionType ExprManager::mkFunctionType(Type domain, Type range) {
   NodeManagerScope nms(d_nodeManager);

diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index bf9bfbb3888e384efaff462be4321afe9089a982..9d0b8d34a6a4550bd27d0ab85304802ca7f838d6 100644 (file)
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -305,6 +305,19 @@ public:
    */
   Expr mkAssociative(Kind kind, const std::vector<Expr>& children);
 
+  /**
+   * Determine whether Exprs of a particular Kind have operators.
+   * @returns true if Exprs of Kind k have operators.
+   */
+  static bool hasOperator(Kind k);
+
+  /**
+   * Get the (singleton) operator of an OPERATOR-kinded kind.  The
+   * returned Expr e will have kind BUILTIN, and calling
+   * e.getConst<CVC4::Kind>() will yield k.
+   */
+  Expr operatorOf(Kind k);
+
   /** Make a function type from domain to range. */
   FunctionType mkFunctionType(Type domain, Type range);
 

diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp
index 54d95ced08bce387759a8a19691b459d174ffa4d..11745ad265b8d50ed45cf018829399d8b89d765c 100644 (file)
--- a/src/util/Assert.cpp
+++ b/src/util/Assert.cpp
@@ -27,7 +27,7 @@ using namespace std;
 namespace CVC4 {
 
 #ifdef CVC4_DEBUG
-CVC4_PUBLIC CVC4_THREADLOCAL(const char*) s_debugLastException = NULL;
+CVC4_THREADLOCAL_PUBLIC(const char*) s_debugLastException = NULL;
 #endif /* CVC4_DEBUG */
 
 void AssertionException::construct(const char* header, const char* extra,