diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/bindings/compat/java/Makefile.am | 70 | ||||
| -rw-r--r-- | src/bindings/compat/java/include/cvc3/JniUtils.h | 4 | ||||
| -rw-r--r-- | src/bindings/compat/java/src/cvc3/Embedded.java | 2 | ||||
| -rw-r--r-- | src/bindings/compat/java/src/cvc3/Expr_impl.cpp | 10 | ||||
| -rw-r--r-- | src/bindings/compat/java/src/cvc3/JniUtils.cpp | 4 | ||||
| -rw-r--r-- | src/bindings/compat/java/src/cvc3/Type_impl.cpp | 10 | ||||
| -rw-r--r-- | src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp | 12 | ||||
| -rw-r--r-- | src/compat/cvc3_compat.cpp | 26 | ||||
| -rw-r--r-- | src/compat/cvc3_compat.h | 66 | ||||
| -rw-r--r-- | src/expr/expr_manager_template.cpp | 10 | ||||
| -rw-r--r-- | src/expr/expr_manager_template.h | 13 | ||||
| -rw-r--r-- | src/util/Assert.cpp | 2 |
12 files changed, 166 insertions, 63 deletions
diff --git a/src/bindings/compat/java/Makefile.am b/src/bindings/compat/java/Makefile.am index 7c22e6231..d268d4d76 100644 --- 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 c6bcc04f8..d4688fc25 100644 --- 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 c645f2655..fdeeef058 100644 --- 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 58c26eb03..f002109c5 100644 --- 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 f291b221b..9ae2023f6 100644 --- 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 ce201fa15..769ce984a 100644 --- 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 e27e44913..34feaacbb 100644 --- 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 83c33c7ab..16169c10a 100644 --- 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 beef53006..eae8412cf 100644 --- 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 533a4dd7f..8819684fc 100644 --- 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 bf9bfbb38..9d0b8d34a 100644 --- 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 54d95ced0..11745ad26 100644 --- 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, |