* 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.)

diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index a747a38128f75a4ce2266ccfdcb8928a4bd8e3e3..bd0bad6ba874002e86bb2c1800e370b8bfe004b3 100644 (file)
--- 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 (file)
index 0000000..16c968a
--- /dev/null
+++ b/src/bindings/java_iterator_adapter.h
@@ -0,0 +1,25 @@
+namespace CVC4 {
+
+template <class T>
+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<T> */
+
+}/* CVC4 namespace */

diff --git a/src/bindings/java_output_stream_adapter.h b/src/bindings/java_output_stream_adapter.h
new file mode 100644 (file)
index 0000000..e6f7d67
--- /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 53444539a3d5d5201c522e097b630e7fd627c394..5264ff6066ef4aecc841e27503d8d4c6e869f689 100644 (file)
--- 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 b581e89197162bcc65343987a15e49630c6b2d6a..0f3a95cdc21958ccb9f9be762b954cd7fd242e02 100644 (file)
--- 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 a4bf5473e730391d2ecc3f46862c59daae24141a..09e54fec0fd6445af28a29d9f5e90fb1f8297778 100644 (file)
--- 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 0d82c7aa8fa8b1cae9c9fa7bb5cf5dcb2ee26db6..a386af5eecb860c2e170fcb7bd405bce59016b6a 100644 (file)
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -15,6 +15,8 @@
   %ignore CVC4::ExprManager::mkExpr(Expr, const std::vector<Expr>&);
 #endif /* SWIGOCAML */
 
+%ignore CVC4::stats::getStatisticsRegistry(ExprManager*);
+
 %include "expr/expr_manager.h"
 
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>;

diff --git a/src/expr/variable_type_map.i b/src/expr/variable_type_map.i
new file mode 100644 (file)
index 0000000..a5d5036
--- /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 8476b6239bf311abdf36dc227ed73a9ef9441751..f190b81bfa920fd1da65479324ae83470131f80a 100644 (file)
--- 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 bf222d189494b863c26beae0d7d5e4afd2a3007c..c3fb3b78223b1d2c368aa90a6da24bfd43cfe853 100644 (file)
--- 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 6058c66d70405352ba9a830b274f42036dbdebbf..e4d21c72e98d6b23be22bb834321a5b556454566 100644 (file)
--- 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 b2ac0b88626fcd22d29ff1a60b7562f22afeea77..3a7fbe389d70e6b9b83dd2358154e04c08eb773d 100644 (file)
--- 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 <string>
 #include <vector>
 
 #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 64a4f93e2e9c5c66fbbd71067db5cf239d66d79d..7fdb594673babcfa8c0de2ceaa35c9ef59c61289 100644 (file)
--- 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 8dcd149954da67306ea9f76a458f196641a76c6a..1f0108581f27cc3032856d74066dfaef8ae5c16b 100644 (file)
--- 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 d2cf576438583cb44f3ff280ead6fe1fcc2cd105..e76e2ace91ae41b52b07720adbdf829435fe3410 100644 (file)
--- 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 (file)
index 0000000..67eea4e
--- /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 72206afb8906118fef87cbe736cd332d61e26cfc..95fe03c829a9f6430acbc25ced15d6a5e0becdcf 100644 (file)
--- 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 0f9cb5e8e669382e0979ece6c3b60d826e1158b7..4b4316db131d29c13fcfe70ba2592d47f572b55c 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1329,25 +1329,23 @@ void TheoryEngine::ppUnconstrainedSimp(vector<Node>& 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; i<d_attr_handle[attr].size(); i++ ){
-      d_attr_handle[attr][i]->setUserAttribute( 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 67830390c06e71cde4917ecbc643116c74520528..d6e984f8f672286814c04a2387e1f13ea90b62c4 100644 (file)
--- 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 f3ae43b05ffe9414aa019e59e164fc65d1d940a0..e72706ea3104d77d2d1425a0d431fe3f18a3c921 100644 (file)
--- 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 e9f674240ecb58946847b65051e0c5bedd33c4e4..dc524e1855bc971bb693b2f0e000b61bfb437eff 100644 (file)
--- 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 (file)
index 0000000..233da01
--- /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 c0d86b30a1a31227bd79a8e1cd29dd2ec0a28914..029a3618ad5e197efb067857a54a1f174efeb710 100644 (file)
--- 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 a14fc29dd9e851799c2e5cf90237207029a7fc3d..1f5cab2e15298223674337f8bd274ceaf9e8f674 100644 (file)
--- 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<CVC4::StatisticsBase> iterator() {
+    return CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>(*$self);
+  }
+}
+
+%typemap(javainterfaces) CVC4::StatisticsBase "java.lang.Iterable<Object>";
+
+%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "class";
+%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "java.util.Iterator";
+%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase> "
+  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, "<init>", "(JZ)V");
+      jenv->SetObjectArrayElement($result, 1, jenv->NewObject(jenv->FindClass("edu/nyu/acsys/CVC4/SExpr"), methodid, reinterpret_cast<long>(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<CVC4::StatisticsBase>;

diff --git a/src/util/uninterpreted_constant.i b/src/util/uninterpreted_constant.i
new file mode 100644 (file)
index 0000000..c0bdc53
--- /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 430a2a164f00b9290dd2f9926dacc641a9df5d52..a6b64c5471ce74a4e1d6ac3d5eea7dfe4f9e7dc8 100644 (file)
--- 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 ) );