From 44498017455cce207bf9cb0a1ebbf67c4a4d77cf Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 17 Nov 2012 04:05:17 +0000 Subject: [PATCH] * Fix for bug 445 agreed to in meeting 11/13/2012: always dump in ALL_SUPPORTED logic * Java bindings fixes: fixed access to ostreams, iterators * Make SmtEngine::setUserAttribute() (and others) take a const string& * Also a few compliance fixes (this commit was certified error- and warning-free by the test-and-commit script.) --- src/bindings/Makefile.am | 15 ++-- src/bindings/java_iterator_adapter.h | 25 +++++++ src/bindings/java_output_stream_adapter.h | 13 ++++ src/cvc4.i | 12 ++- src/expr/Makefile.am | 3 +- src/expr/command.i | 2 + src/expr/expr_manager.i | 2 + src/expr/variable_type_map.i | 8 ++ src/printer/cvc/cvc_printer.cpp | 2 +- src/printer/smt2/smt2_printer.cpp | 8 +- src/smt/smt_engine.cpp | 15 ++-- src/smt/smt_engine.h | 3 +- src/smt/smt_engine.i | 3 + src/theory/Makefile.am | 1 + src/theory/logic_info.cpp | 91 +++++++++++++---------- src/theory/logic_info.i | 15 ++++ src/theory/theory.h | 2 +- src/theory/theory_engine.cpp | 10 +-- src/theory/theory_engine.h | 4 +- src/util/Makefile.am | 4 +- src/util/output.i | 23 +++++- src/util/predicate.i | 8 ++ src/util/result.i | 5 ++ src/util/statistics.i | 46 ++++++++++++ src/util/uninterpreted_constant.i | 13 ++++ test/unit/theory/logic_info_white.h | 2 +- 26 files changed, 264 insertions(+), 71 deletions(-) create mode 100644 src/bindings/java_iterator_adapter.h create mode 100644 src/bindings/java_output_stream_adapter.h create mode 100644 src/expr/variable_type_map.i create mode 100644 src/theory/logic_info.i create mode 100644 src/util/predicate.i create mode 100644 src/util/uninterpreted_constant.i diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am index a747a3812..bd0bad6ba 100644 --- a/src/bindings/Makefile.am +++ b/src/bindings/Makefile.am @@ -160,7 +160,10 @@ CLEANFILES = \ ruby.cpp \ tcl.cpp -EXTRA_DIST = swig.h +EXTRA_DIST = \ + swig.h \ + java_iterator_adapter.h \ + java_output_stream_adapter.h MOSTLYCLEANFILES = \ .swig_deps \ @@ -171,11 +174,11 @@ java_libcvc4jni_la-java.lo java.lo: java.cpp $(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_CPPFLAGS) $(java_libcvc4jni_la_CXXFLAGS) -o $@ $< CVC4.jar: java.cpp $(AM_V_GEN) \ - (cd java; \ - rm -fr classes; \ - mkdir -p classes; \ - $(JAVAC) -classpath . -d classes `find . -name '*.java'`; \ - cd classes); \ + (cd java && \ + rm -fr classes && \ + mkdir -p classes && \ + $(JAVAC) -classpath . -d classes `find . -name '*.java'` && \ + cd classes) && \ $(JAR) cf $@ -C java/classes . #java.cpp:; csharp.lo: csharp.cpp diff --git a/src/bindings/java_iterator_adapter.h b/src/bindings/java_iterator_adapter.h new file mode 100644 index 000000000..16c968a47 --- /dev/null +++ b/src/bindings/java_iterator_adapter.h @@ -0,0 +1,25 @@ +namespace CVC4 { + +template +class JavaIteratorAdapter { + const T& d_t; + typename T::const_iterator d_it; + +public: + JavaIteratorAdapter(const T& t) : + d_t(t), + d_it(d_t.begin()) { + } + + bool hasNext() { + return d_it != d_t.end(); + } + + typename T::const_iterator::value_type getNext() { + typename T::const_iterator::value_type ret = *d_it; + ++d_it; + return ret; + } +};/* class JavaIteratorAdapter */ + +}/* CVC4 namespace */ diff --git a/src/bindings/java_output_stream_adapter.h b/src/bindings/java_output_stream_adapter.h new file mode 100644 index 000000000..e6f7d6786 --- /dev/null +++ b/src/bindings/java_output_stream_adapter.h @@ -0,0 +1,13 @@ +namespace CVC4 { + +class JavaOutputStreamAdapter { + std::stringstream d_ss; + +public: + JavaOutputStreamAdapter() { } + + std::string toString() { return d_ss.str(); } + +};/* class JavaOutputStreamAdapter */ + +}/* CVC4 namespace */ diff --git a/src/cvc4.i b/src/cvc4.i index 53444539a..5264ff606 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -133,17 +133,22 @@ using namespace CVC4; %include "java/arrays_java.i" // C arrays to Java arrays %include "java/various.i" // map char** to java.lang.String[] +%typemap(jni) std::ostream& "jlong" +%typemap(jtype) std::ostream& "long" +%typemap(jstype) std::ostream& "java.io.OutputStream" +%typemap(javain, pre=" edu.nyu.acsys.CVC4.JavaOutputStreamAdapter temp$javainput = new edu.nyu.acsys.CVC4.JavaOutputStreamAdapter();", pgcppname="temp$javainput", post=" new java.io.PrintStream($javainput).print(temp$javainput.toString());") std::ostream& "edu.nyu.acsys.CVC4.JavaOutputStreamAdapter.getCPtr(temp$javainput)" + #endif /* SWIGJAVA */ %include "util/integer.i" %include "util/rational.i" -%include "util/statistics.i" %include "util/exception.i" %include "util/language.i" %include "options/options.i" %include "util/cardinality.i" %include "util/bool.i" %include "util/sexpr.i" +%include "util/statistics.i" %include "util/output.i" %include "util/result.i" %include "util/configuration.i" @@ -151,11 +156,13 @@ using namespace CVC4; %include "util/subrange_bound.i" %include "util/array.i" %include "util/array_store_all.i" +%include "util/predicate.i" %include "util/hash.i" %include "expr/type.i" %include "util/ascription_type.i" %include "util/datatype.i" +%include "util/uninterpreted_constant.i" %include "expr/kind.i" %include "expr/expr.i" @@ -163,6 +170,9 @@ using namespace CVC4; %include "expr/symbol_table.i" %include "expr/expr_manager.i" %include "expr/expr_stream.i" +%include "expr/variable_type_map.i" + +%include "theory/logic_info.i" %include "smt/smt_engine.i" %include "smt/modal_exception.i" diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index b581e8919..0f3a95cdc 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -66,7 +66,8 @@ EXTRA_DIST = \ command.i \ type.i \ kind.i \ - expr.i + expr.i \ + variable_type_map.i BUILT_SOURCES = \ kind.h \ diff --git a/src/expr/command.i b/src/expr/command.i index a4bf5473e..09e54fec0 100644 --- a/src/expr/command.i +++ b/src/expr/command.i @@ -6,6 +6,8 @@ %ignore CVC4::operator<<(std::ostream&, const Command*) throw(); %ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status) throw(); +%ignore CVC4::GetProofCommand; + %rename(beginConst) CVC4::CommandSequence::begin() const throw(); %rename(endConst) CVC4::CommandSequence::end() const throw(); diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i index 0d82c7aa8..a386af5ee 100644 --- a/src/expr/expr_manager.i +++ b/src/expr/expr_manager.i @@ -15,6 +15,8 @@ %ignore CVC4::ExprManager::mkExpr(Expr, const std::vector&); #endif /* SWIGOCAML */ +%ignore CVC4::stats::getStatisticsRegistry(ExprManager*); + %include "expr/expr_manager.h" %template(mkConst) CVC4::ExprManager::mkConst; diff --git a/src/expr/variable_type_map.i b/src/expr/variable_type_map.i new file mode 100644 index 000000000..a5d50361f --- /dev/null +++ b/src/expr/variable_type_map.i @@ -0,0 +1,8 @@ +%{ +#include "expr/variable_type_map.h" +%} + +%rename(get) CVC4::VariableTypeMap::operator[](Expr); +%rename(get) CVC4::VariableTypeMap::operator[](Type); + +%include "expr/variable_type_map.h" diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 8476b6239..f190b81bf 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -939,7 +939,7 @@ static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) thro } static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw() { - out << "% (set-logic " << c->getLogic() << ")"; + out << "OPTION \"logic\" \"" << c->getLogic() << "\";"; } static void toStream(std::ostream& out, const SetInfoCommand* c) throw() { diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index bf222d189..c3fb3b782 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -791,7 +791,13 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr } static void toStream(std::ostream& out, const CommentCommand* c) throw() { - out << "(set-info :notes \"" << c->getComment() << "\")"; + string s = c->getComment(); + size_t pos = 0; + while((pos = s.find_first_of('"', pos)) != string::npos) { + s.replace(pos, 1, "\\\""); + pos += 2; + } + out << "(set-info :notes \"" << s << "\")"; } static void toStream(std::ostream& out, const EmptyCommand* c) throw() { diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 6058c66d7..e4d21c72e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -566,6 +566,15 @@ void SmtEngine::finishInit() { d_assertionList = new(true) AssertionList(d_userContext); } + // dump out a set-logic command + if(Dump.isOn("benchmark")) { + // Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString()); + LogicInfo everything; + everything.lock(); + Dump("benchmark") << CommentCommand("CVC4 always dumps the most general, \"all-supported\" logic (above), as some internals might require the use of a logic more general than the input.") + << SetBenchmarkLogicCommand(everything.getLogicString()); + } + // dump out any pending declaration commands for(unsigned i = 0; i < d_dumpCommands.size(); ++i) { Dump("declarations") << *d_dumpCommands[i]; @@ -697,10 +706,6 @@ SmtEngine::~SmtEngine() throw() { void SmtEngine::setLogic(const LogicInfo& logic) throw(ModalException) { SmtScope smts(this); - if(Dump.isOn("benchmark")) { - Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString()); - } - d_logic = logic; setLogicInternal(); } @@ -3016,7 +3021,7 @@ SExpr SmtEngine::getStatistic(std::string name) const throw() { return d_statisticsRegistry->getStatistic(name); } -void SmtEngine::setUserAttribute(std::string& attr, Expr expr) { +void SmtEngine::setUserAttribute(const std::string& attr, Expr expr) { SmtScope smts(this); d_theoryEngine->setUserAttribute(attr, expr.getNode()); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index b2ac0b886..3a7fbe389 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -19,6 +19,7 @@ #ifndef __CVC4__SMT_ENGINE_H #define __CVC4__SMT_ENGINE_H +#include #include #include "context/cdlist_forward.h" @@ -586,7 +587,7 @@ public: * This function is called when an attribute is set by a user. * In SMT-LIBv2 this is done via the syntax (! expr :attr) */ - void setUserAttribute( std::string& attr, Expr expr ); + void setUserAttribute(const std::string& attr, Expr expr); };/* class SmtEngine */ diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i index 64a4f93e2..7fdb59467 100644 --- a/src/smt/smt_engine.i +++ b/src/smt/smt_engine.i @@ -2,4 +2,7 @@ #include "smt/smt_engine.h" %} +%ignore CVC4::SmtEngine::getProof; +%ignore CVC4::stats::getStatisticsRegistry(SmtEngine*); + %include "smt/smt_engine.h" diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 8dcd14995..1f0108581 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -61,6 +61,7 @@ libtheory_la_LIBADD = \ @builddir@/rewriterules/librewriterules.la EXTRA_DIST = \ + logic_info.i \ options_handlers.h \ rewriter_tables_template.h \ instantiator_tables_template.cpp \ diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index d2cf57643..e76e2ace9 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -76,52 +76,61 @@ LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) : std::string LogicInfo::getLogicString() const { CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried"); if(d_logicString == "") { - size_t seen = 0; // make sure we support all the active theories + LogicInfo qf_all_supported; + qf_all_supported.disableQuantifiers(); + qf_all_supported.lock(); + if(hasEverything()) { + d_logicString = "ALL_SUPPORTED"; + } else if(*this == qf_all_supported) { + d_logicString = "QF_ALL_SUPPORTED"; + } else { + size_t seen = 0; // make sure we support all the active theories - stringstream ss; - if(!isQuantified()) { - ss << "QF_"; - } - if(d_theories[THEORY_ARRAY]) { - ss << (d_sharingTheories == 1 ? "AX" : "A"); - ++seen; - } - if(d_theories[THEORY_UF]) { - ss << "UF"; - ++seen; - } - if(d_theories[THEORY_BV]) { - ss << "BV"; - ++seen; - } - if(d_theories[THEORY_DATATYPES]) { - ss << "DT"; - ++seen; - } - if(d_theories[THEORY_ARITH]) { - if(isDifferenceLogic()) { - ss << (areIntegersUsed() ? "I" : ""); - ss << (areRealsUsed() ? "R" : ""); - ss << "DL"; - } else { - ss << (isLinear() ? "L" : "N"); - ss << (areIntegersUsed() ? "I" : ""); - ss << (areRealsUsed() ? "R" : ""); - ss << "A"; + stringstream ss; + if(!isQuantified()) { + ss << "QF_"; + } + if(d_theories[THEORY_ARRAY]) { + ss << (d_sharingTheories == 1 ? "AX" : "A"); + ++seen; + } + if(d_theories[THEORY_UF]) { + ss << "UF"; + ++seen; + } + if(d_theories[THEORY_BV]) { + ss << "BV"; + ++seen; + } + if(d_theories[THEORY_DATATYPES]) { + ss << "DT"; + ++seen; + } + if(d_theories[THEORY_ARITH]) { + if(isDifferenceLogic()) { + ss << (areIntegersUsed() ? "I" : ""); + ss << (areRealsUsed() ? "R" : ""); + ss << "DL"; + } else { + ss << (isLinear() ? "L" : "N"); + ss << (areIntegersUsed() ? "I" : ""); + ss << (areRealsUsed() ? "R" : ""); + ss << "A"; + } + ++seen; } - ++seen; - } - if(seen != d_sharingTheories) { - Unhandled("can't extract a logic string from LogicInfo; at least one " - "active theory is unknown to LogicInfo::getLogicString() !"); - } + if(seen != d_sharingTheories) { + Unhandled("can't extract a logic string from LogicInfo; at least one " + "active theory is unknown to LogicInfo::getLogicString() !"); + } - if(seen == 0) { - ss << "SAT"; - } + if(seen == 0) { + ss << "SAT"; + } - d_logicString = ss.str(); + d_logicString = ss.str(); + } } return d_logicString; } diff --git a/src/theory/logic_info.i b/src/theory/logic_info.i new file mode 100644 index 000000000..67eea4e04 --- /dev/null +++ b/src/theory/logic_info.i @@ -0,0 +1,15 @@ +%{ +#include "theory/logic_info.h" +%} + +%ignore CVC4::LogicInfo::LogicInfo(const char*); + +%rename(less) CVC4::LogicInfo::operator<(const LogicInfo&) const; +%rename(lessEqual) CVC4::LogicInfo::operator<=(const LogicInfo&) const; +%rename(greater) CVC4::LogicInfo::operator>(const LogicInfo&) const; +%rename(greaterEqual) CVC4::LogicInfo::operator>=(const LogicInfo&) const; + +%rename(equals) CVC4::LogicInfo::operator==(const LogicInfo&) const; +%ignore CVC4::LogicInfo::operator!=(const LogicInfo&) const; + +%include "theory/logic_info.h" diff --git a/src/theory/theory.h b/src/theory/theory.h index 72206afb8..95fe03c82 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -669,7 +669,7 @@ public: * This function is called when an attribute is set by a user. In SMT-LIBv2 this is done * via the syntax (! n :attr) */ - virtual void setUserAttribute( std::string& attr, Node n ) { + virtual void setUserAttribute(const std::string& attr, Node n) { Unimplemented("Theory %s doesn't support Theory::setUserAttribute interface", identify().c_str()); } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 0f9cb5e8e..4b4316db1 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1329,25 +1329,23 @@ void TheoryEngine::ppUnconstrainedSimp(vector& assertions) } -void TheoryEngine::setUserAttribute( std::string& attr, Node n ){ +void TheoryEngine::setUserAttribute(const std::string& attr, Node n) { Trace("te-attr") << "set user attribute " << attr << " " << n << std::endl; if( d_attr_handle.find( attr )!=d_attr_handle.end() ){ for( size_t i=0; isetUserAttribute( attr, n ); + d_attr_handle[attr][i]->setUserAttribute(attr, n); } - }else{ + } else { //unhandled exception? } } - -void TheoryEngine::handleUserAttribute( const char* attr, Theory* t ){ +void TheoryEngine::handleUserAttribute(const char* attr, Theory* t) { Trace("te-attr") << "Handle user attribute " << attr << " " << t << std::endl; std::string str( attr ); d_attr_handle[ str ].push_back( t ); } - void TheoryEngine::checkTheoryAssertionsWithModel() { for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 67830390c..d6e984f8f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -703,13 +703,13 @@ public: * This function is called when an attribute is set by a user. In SMT-LIBv2 this is done * via the syntax (! n :attr) */ - void setUserAttribute( std::string& attr, Node n ); + void setUserAttribute(const std::string& attr, Node n); /** Handle user attribute * Associates theory t with the attribute attr. Theory t will be * notifed whenever an attribute of name attr is set. */ - void handleUserAttribute( const char* attr, theory::Theory* t ); + void handleUserAttribute(const char* attr, theory::Theory* t); /** Check that the theory assertions are satisfied in the model * This function is called from the smt engine's checkModel routine diff --git a/src/util/Makefile.am b/src/util/Makefile.am index f3ae43b05..e72706ea3 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -141,7 +141,9 @@ EXTRA_DIST = \ array_store_all.i \ ascription_type.i \ rational.i \ - hash.i + hash.i \ + predicate.i \ + uninterpreted_constant.i DISTCLEANFILES = \ integer.h.tmp \ diff --git a/src/util/output.i b/src/util/output.i index e9f674240..dc524e185 100644 --- a/src/util/output.i +++ b/src/util/output.i @@ -2,7 +2,7 @@ #include "util/output.h" %} -%feature("valuewrapper") CVC4::null_streambuf; +%ignore CVC4::null_streambuf; %feature("valuewrapper") std::ostream; // There are issues with SWIG's attempted wrapping of these variables when @@ -24,8 +24,25 @@ %ignore CVC4::ScopedTrace::ScopedTrace(std::string); %ignore CVC4::ScopedTrace::ScopedTrace(std::string, bool); -%rename(getostream) operator std::ostream&; -%rename(getCVC4ostream) operator CVC4ostream; +%ignore CVC4::WarningC::getStream(); +%ignore CVC4::MessageC::getStream(); +%ignore CVC4::NoticeC::getStream(); +%ignore CVC4::ChatC::getStream(); +%ignore CVC4::TraceC::getStream(); +%ignore CVC4::DebugC::getStream(); +%ignore CVC4::DumpOutC::getStream(); + +%ignore CVC4::WarningC::setStream(std::ostream&); +%ignore CVC4::MessageC::setStream(std::ostream&); +%ignore CVC4::NoticeC::setStream(std::ostream&); +%ignore CVC4::ChatC::setStream(std::ostream&); +%ignore CVC4::TraceC::setStream(std::ostream&); +%ignore CVC4::DebugC::setStream(std::ostream&); +%ignore CVC4::DumpOutC::setStream(std::ostream&); + +%ignore operator std::ostream&; +%ignore operator CVC4ostream; + %rename(get) operator(); %rename(ok) operator bool; diff --git a/src/util/predicate.i b/src/util/predicate.i new file mode 100644 index 000000000..233da01f9 --- /dev/null +++ b/src/util/predicate.i @@ -0,0 +1,8 @@ +%{ +#include "util/predicate.h" +%} + +%rename(equals) CVC4::Predicate::operator==(const Predicate&) const; +%rename(toExpr) CVC4::Predicate::operator Expr() const; + +%include "util/predicate.h" diff --git a/src/util/result.i b/src/util/result.i index c0d86b30a..029a3618a 100644 --- a/src/util/result.i +++ b/src/util/result.i @@ -11,4 +11,9 @@ %ignore CVC4::operator<<(std::ostream&, enum Result::Validity); %ignore CVC4::operator<<(std::ostream&, enum Result::UnknownExplanation); +%ignore CVC4::operator==(enum Result::Sat, const Result&); +%ignore CVC4::operator==(enum Result::Validity, const Result&); +%ignore CVC4::operator!=(enum Result::Sat, const Result&); +%ignore CVC4::operator!=(enum Result::Validity, const Result&); + %include "util/result.h" diff --git a/src/util/statistics.i b/src/util/statistics.i index a14fc29dd..1f5cab2e1 100644 --- a/src/util/statistics.i +++ b/src/util/statistics.i @@ -1,8 +1,54 @@ %{ #include "util/statistics.h" +#include "bindings/java_iterator_adapter.h" +#include "bindings/java_output_stream_adapter.h" %} %rename(assign) CVC4::Statistics::operator=(const StatisticsBase&); %rename(assign) CVC4::Statistics::operator=(const Statistics& stats); +%ignore CVC4::StatisticsBase::begin(); +%ignore CVC4::StatisticsBase::end(); +%ignore CVC4::StatisticsBase::begin() const; +%ignore CVC4::StatisticsBase::end() const; +%extend CVC4::StatisticsBase { + CVC4::JavaIteratorAdapter iterator() { + return CVC4::JavaIteratorAdapter(*$self); + } +} + +%typemap(javainterfaces) CVC4::StatisticsBase "java.lang.Iterable"; + +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter "class"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter "java.util.Iterator"; +%typemap(javacode) CVC4::JavaIteratorAdapter " + public void remove() { + throw new java.lang.UnsupportedOperationException(); + } + + public Object next() { + if(hasNext()) { + return getNext(); + } else { + throw new java.util.NoSuchElementException(); + } + } +" + +%typemap(jni) CVC4::StatisticsBase::const_iterator::value_type "jobjectArray"; +%typemap(jtype) CVC4::StatisticsBase::const_iterator::value_type "java.lang.Object[]"; +%typemap(jstype) CVC4::StatisticsBase::const_iterator::value_type "java.lang.Object[]"; +%typemap(javaout) CVC4::StatisticsBase::const_iterator::value_type { return $jnicall; } +%typemap(out) CVC4::StatisticsBase::const_iterator::value_type { + $result = jenv->NewObjectArray(2, jenv->FindClass("java/lang/Object"), $null); + jenv->SetObjectArrayElement($result, 0, jenv->NewStringUTF($1.first.c_str())); + jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/SExpr"); + jmethodID methodid = jenv->GetMethodID(clazz, "", "(JZ)V"); + jenv->SetObjectArrayElement($result, 1, jenv->NewObject(jenv->FindClass("edu/nyu/acsys/CVC4/SExpr"), methodid, reinterpret_cast(new CVC4::SExpr($1.second)), true)); + }; + %include "util/statistics.h" +%include "bindings/java_iterator_adapter.h" +%include "bindings/java_output_stream_adapter.h" + +%template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter; diff --git a/src/util/uninterpreted_constant.i b/src/util/uninterpreted_constant.i new file mode 100644 index 000000000..c0bdc5390 --- /dev/null +++ b/src/util/uninterpreted_constant.i @@ -0,0 +1,13 @@ +%{ +#include "util/uninterpreted_constant.h" +%} + +%rename(less) CVC4::UninterpretedConstant::operator<(const UninterpretedConstant&) const; +%rename(lessEqual) CVC4::UninterpretedConstant::operator<=(const UninterpretedConstant&) const; +%rename(greater) CVC4::UninterpretedConstant::operator>(const UninterpretedConstant&) const; +%rename(greaterEqual) CVC4::UninterpretedConstant::operator>=(const UninterpretedConstant&) const; + +%rename(equals) CVC4::UninterpretedConstant::operator==(const UninterpretedConstant&) const; +%ignore CVC4::UninterpretedConstant::operator!=(const UninterpretedConstant&) const; + +%include "util/uninterpreted_constant.h" diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index 430a2a164..a6b64c547 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -474,7 +474,7 @@ public: info.lock(); TS_ASSERT( info.isLocked() ); - TS_ASSERT_EQUALS( info.getLogicString(), "AUFBVDTLIRA" );// for now, nonlinear not included in ALL_SUPPORTED + TS_ASSERT_EQUALS( info.getLogicString(), "ALL_SUPPORTED" ); TS_ASSERT( info.isSharingEnabled() ); TS_ASSERT( info.isTheoryEnabled( THEORY_BUILTIN ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_BOOL ) ); -- 2.30.2