diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-26 17:58:39 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-26 19:43:25 -0400 |
commit | ad5e31e2031349c9b9d0bf5d9fcaa1ea7950db58 (patch) | |
tree | dd3e7e943628f1410f4a8d2f260c994d62be308d /src | |
parent | a9912269ab2b47b783a66f381b14148c0ac73e93 (diff) |
Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac
Diffstat (limited to 'src')
31 files changed, 281 insertions, 36 deletions
diff --git a/src/bindings/compat/c/c_interface.cpp b/src/bindings/compat/c/c_interface.cpp index 6540f428c..8219d5169 100644 --- a/src/bindings/compat/c/c_interface.cpp +++ b/src/bindings/compat/c/c_interface.cpp @@ -31,6 +31,7 @@ //#include "fdstream.h" #include <string> #include <cassert> +#include <cerrno> #include <unistd.h> #ifdef CVC4_DEBUG @@ -862,7 +863,12 @@ extern "C" void vc_printExprFile(VC vc, Expr e, int fd) CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc; cvc->printExpr(fromExpr(e), ss); string s = ss.str(); - write(fd, s.c_str(), s.size()); + ssize_t e = write(fd, s.c_str(), s.size()); + if(e < 0) { + IF_DEBUG(cerr << "write() failed, errno == " << errno << endl;) + c_interface_error_string = "write() failed"; + c_interface_error_flag = errno; + } } catch(CVC3::Exception ex) { signal_error("vc_printExpr",error_int,ex); } diff --git a/src/bindings/compat/java/Makefile.am b/src/bindings/compat/java/Makefile.am index 3b0df308a..e465195d9 100644 --- a/src/bindings/compat/java/Makefile.am +++ b/src/bindings/compat/java/Makefile.am @@ -16,7 +16,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4BINDINGSLIB \ -I@builddir@/../../.. -I@srcdir@/../../../include -I@srcdir@/../../.. \ -I@builddir@/cvc3 -I@srcdir@/include/cvc3 -AM_CXXFLAGS = -Wall +AM_CXXFLAGS = -Wall -Wno-unused-variable javadatadir = $(datadir)/java javalibdir = $(libdir)/jni diff --git a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp index af588a4ff..fa608a785 100644 --- a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp +++ b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp @@ -87,10 +87,12 @@ return toJavaVCopy(env, result); DEFINITION: Java_cvc3_ValidityChecker_jniAnyType jobject m ValidityChecker vc assert(false);// Unimplemented +return NULL; DEFINITION: Java_cvc3_ValidityChecker_jniArrayLiteral jobject m ValidityChecker vc c Expr indexVar c Expr bodyExpr assert(false);// Unimplemented +return NULL; 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 0cd35ce0d..9fbdeb8d0 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -1261,6 +1261,7 @@ Type ValidityChecker::createType(const std::string& typeName) { Type ValidityChecker::createType(const std::string& typeName, const Type& def) { d_parserContext->defineType(typeName, def); + return def; } Type ValidityChecker::lookupType(const std::string& typeName) { @@ -1279,6 +1280,7 @@ Expr ValidityChecker::varExpr(const std::string& name, const Type& type, const Expr& def) { CVC4::CheckArgument(def.getType() == type, def, "expected types to match"); d_parserContext->defineVar(name, def); + return def; } Expr ValidityChecker::lookupVar(const std::string& name, Type* type) { diff --git a/src/cvc4.i b/src/cvc4.i index 925152248..ebb8cbd63 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -62,6 +62,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; %template(vectorCommandPtr) std::vector< CVC4::Command* >; %template(vectorType) std::vector< CVC4::Type >; %template(vectorExpr) std::vector< CVC4::Expr >; +%template(vectorVectorExpr) std::vector< std::vector< CVC4::Expr > >; %template(vectorDatatypeType) std::vector< CVC4::DatatypeType >; %template(vectorSExpr) std::vector< CVC4::SExpr >; %template(vectorString) std::vector< std::string >; @@ -177,7 +178,8 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; *(CVC4::JavaInputStreamAdapter **)&$result = $1; %} %typemap(javacode) CVC4::JavaInputStreamAdapter %{ - private static java.util.HashMap streams = new java.util.HashMap(); + private static java.util.HashMap<java.io.InputStream, JavaInputStreamAdapter> streams = + new java.util.HashMap<java.io.InputStream, JavaInputStreamAdapter>(); public static JavaInputStreamAdapter get(java.io.InputStream is) { if(streams.containsKey(is)) { return (JavaInputStreamAdapter) streams.get(is); @@ -195,6 +197,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; %} %ignore CVC4::JavaInputStreamAdapter::init(JNIEnv*); %ignore CVC4::JavaInputStreamAdapter::pullAdapters(JNIEnv*); +%ignore CVC4::JavaInputStreamAdapter::pull(JNIEnv*); %javamethodmodifiers CVC4::JavaInputStreamAdapter::getInputStream() const "private"; %javamethodmodifiers CVC4::JavaInputStreamAdapter::JavaInputStreamAdapter(jobject) "private"; @@ -256,6 +259,8 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; %include "expr/type.i" %include "util/ascription_type.i" %include "util/datatype.i" +%include "util/tuple.i" +%include "util/record.i" %include "util/uninterpreted_constant.i" %include "expr/kind.i" diff --git a/src/expr/command.i b/src/expr/command.i index 09e54fec0..6085a444f 100644 --- a/src/expr/command.i +++ b/src/expr/command.i @@ -1,5 +1,12 @@ %{ #include "expr/command.h" + +#ifdef SWIGJAVA + +#include "bindings/java_iterator_adapter.h" +#include "bindings/java_stream_adapters.h" + +#endif /* SWIGJAVA */ %} %ignore CVC4::operator<<(std::ostream&, const Command&) throw(); @@ -7,8 +14,55 @@ %ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status) throw(); %ignore CVC4::GetProofCommand; +%ignore CVC4::CommandPrintSuccess::Scope; + +#ifdef SWIGJAVA + +// Instead of CommandSequence::begin() and end(), create an +// iterator() method on the Java side that returns a Java-style +// Iterator. +%ignore CVC4::CommandSequence::begin(); +%ignore CVC4::CommandSequence::end(); +%ignore CVC4::CommandSequence::begin() const; +%ignore CVC4::CommandSequence::end() const; +%extend CVC4::CommandSequence { + CVC4::JavaIteratorAdapter<CVC4::CommandSequence> iterator() { + return CVC4::JavaIteratorAdapter<CVC4::CommandSequence>(*$self); + } +} + +// CommandSequence is "iterable" on the Java side +%typemap(javainterfaces) CVC4::CommandSequence "java.lang.Iterable<edu.nyu.acsys.CVC4.Command>"; -%rename(beginConst) CVC4::CommandSequence::begin() const throw(); -%rename(endConst) CVC4::CommandSequence::end() const throw(); +// the JavaIteratorAdapter should not be public, and implements Iterator +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "class"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "java.util.Iterator<edu.nyu.acsys.CVC4.Command>"; +// add some functions to the Java side (do it here because there's no way to do these in C++) +%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> " + public void remove() { + throw new java.lang.UnsupportedOperationException(); + } + + public edu.nyu.acsys.CVC4.Command next() { + if(hasNext()) { + return getNext(); + } else { + throw new java.util.NoSuchElementException(); + } + } +" +// getNext() just allows C++ iterator access from Java-side next(), make it private +%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::CommandSequence>::getNext() "private"; + +#endif /* SWIGJAVA */ %include "expr/command.h" + +#ifdef SWIGJAVA + +%include "bindings/java_iterator_adapter.h" +%include "bindings/java_stream_adapters.h" + +%template(JavaIteratorAdapter_CommandSequence) CVC4::JavaIteratorAdapter<CVC4::CommandSequence>; + +#endif /* SWIGJAVA */ diff --git a/src/expr/expr.i b/src/expr/expr.i index 34f074a6d..92ab517b1 100644 --- a/src/expr/expr.i +++ b/src/expr/expr.i @@ -1,5 +1,12 @@ %{ #include "expr/expr.h" + +#ifdef SWIGJAVA + +#include "bindings/java_iterator_adapter.h" +#include "bindings/java_stream_adapters.h" + +#endif /* SWIGJAVA */ %} %rename(apply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const; @@ -29,6 +36,44 @@ namespace CVC4 { }/* CVC4::expr namespace */ }/* CVC4 namespace */ +#ifdef SWIGJAVA + +// Instead of Expr::begin() and end(), create an +// iterator() method on the Java side that returns a Java-style +// Iterator. +%ignore CVC4::Expr::begin() const; +%ignore CVC4::Expr::end() const; +%extend CVC4::Expr { + CVC4::JavaIteratorAdapter<CVC4::Expr> iterator() { + return CVC4::JavaIteratorAdapter<CVC4::Expr>(*$self); + } +} + +// Expr is "iterable" on the Java side +%typemap(javainterfaces) CVC4::Expr "java.lang.Iterable<edu.nyu.acsys.CVC4.Expr>"; + +// the JavaIteratorAdapter should not be public, and implements Iterator +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::Expr> "class"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::Expr> "java.util.Iterator<edu.nyu.acsys.CVC4.Expr>"; +// add some functions to the Java side (do it here because there's no way to do these in C++) +%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::Expr> " + public void remove() { + throw new java.lang.UnsupportedOperationException(); + } + + public edu.nyu.acsys.CVC4.Expr next() { + if(hasNext()) { + return getNext(); + } else { + throw new java.util.NoSuchElementException(); + } + } +" +// getNext() just allows C++ iterator access from Java-side next(), make it private +%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::Expr>::getNext() "private"; + +#endif /* SWIGJAVA */ + %include "expr/expr.h" %template(getConstTypeConstant) CVC4::Expr::getConst<CVC4::TypeConstant>; @@ -52,4 +97,13 @@ namespace CVC4 { %template(getConstString) CVC4::Expr::getConst<std::string>; %template(getConstBoolean) CVC4::Expr::getConst<bool>; +#ifdef SWIGJAVA + +%include "bindings/java_iterator_adapter.h" +%include "bindings/java_stream_adapters.h" + +%template(JavaIteratorAdapter_Expr) CVC4::JavaIteratorAdapter<CVC4::Expr>; + +#endif /* SWIGJAVA */ + %include "expr/expr.h" diff --git a/src/expr/variable_type_map.i b/src/expr/variable_type_map.i index a5d50361f..95c705c1e 100644 --- a/src/expr/variable_type_map.i +++ b/src/expr/variable_type_map.i @@ -5,4 +5,8 @@ %rename(get) CVC4::VariableTypeMap::operator[](Expr); %rename(get) CVC4::VariableTypeMap::operator[](Type); +%ignore CVC4::ExprManagerMapCollection::d_typeMap; +%ignore CVC4::ExprManagerMapCollection::d_to; +%ignore CVC4::ExprManagerMapCollection::d_from; + %include "expr/variable_type_map.h" diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am index b1cfe7bd8..7c5d48c1c 100644 --- a/src/parser/cvc/Makefile.am +++ b/src/parser/cvc/Makefile.am @@ -1,7 +1,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable $(WNO_CONVERSION_NULL) +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTHESES) $(WNO_TAUTOLOGICAL_COMPARE) -Wno-unused-function -Wno-unused-variable $(WNO_CONVERSION_NULL) # Compile generated C files using C++ compiler CC=$(CXX) diff --git a/src/parser/parser.i b/src/parser/parser.i index 5b23555ea..37aefb901 100644 --- a/src/parser/parser.i +++ b/src/parser/parser.i @@ -19,6 +19,8 @@ namespace CVC4 { }/* namespace CVC4::parser */ }/* namespace CVC4 */ +%ignore CVC4::parser::Parser::ExprStream; + %include "parser/parser.h" %{ diff --git a/src/parser/parser_exception.i b/src/parser/parser_exception.i index 5be81034d..39f67e6f5 100644 --- a/src/parser/parser_exception.i +++ b/src/parser/parser_exception.i @@ -3,5 +3,6 @@ %} %ignore CVC4::parser::ParserException::ParserException(const char*); +%ignore CVC4::parser::ParserEndOfFileException::ParserEndOfFileException(const char*); %include "parser/parser_exception.h" diff --git a/src/parser/smt1/Makefile.am b/src/parser/smt1/Makefile.am index 578fae272..90ee7eb31 100644 --- a/src/parser/smt1/Makefile.am +++ b/src/parser/smt1/Makefile.am @@ -1,7 +1,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTHESES) $(WNO_TAUTOLOGICAL_COMPARE) -Wno-unused-function -Wno-unused-variable # Compile generated C files using C++ compiler AM_CFLAGS = $(AM_CXXFLAGS) diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am index ec445427a..bf42e9288 100644 --- a/src/parser/smt2/Makefile.am +++ b/src/parser/smt2/Makefile.am @@ -1,7 +1,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTHESES) $(WNO_TAUTOLOGICAL_COMPARE) -Wno-unused-function -Wno-unused-variable # Compile generated C files using C++ compiler AM_CFLAGS = $(AM_CXXFLAGS) diff --git a/src/parser/tptp/Makefile.am b/src/parser/tptp/Makefile.am index 0db7773b2..b5ac965e8 100644 --- a/src/parser/tptp/Makefile.am +++ b/src/parser/tptp/Makefile.am @@ -1,7 +1,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTHESES) $(WNO_TAUTOLOGICAL_COMPARE) -Wno-unused-function -Wno-unused-variable # Compile generated C files using C++ compiler AM_CFLAGS = $(AM_CXXFLAGS) diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index 0923848e9..c3cd488d8 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -31,6 +31,7 @@ class AstPrinter : public CVC4::Printer { void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw(); void toStream(std::ostream& out, Model& m, const Command* c) const throw(); public: + using CVC4::Printer::toStream; void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 524344612..bad05b5c8 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -24,6 +24,8 @@ #include "smt/options.h" #include "theory/model.h" #include "theory/arrays/theory_arrays_rewriter.h" +#include "printer/dagification_visitor.h" +#include "util/node_visitor.h" #include <iostream> #include <vector> diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index 77d770bb2..71ad947bf 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -22,9 +22,6 @@ #include <iostream> #include "printer/printer.h" -#include "printer/dagification_visitor.h" -#include "theory/substitutions.h" -#include "util/node_visitor.h" namespace CVC4 { namespace printer { @@ -34,6 +31,7 @@ class CvcPrinter : public CVC4::Printer { void toStream(std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const throw(); void toStream(std::ostream& out, Model& m, const Command* c) const throw(); public: + using CVC4::Printer::toStream; void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); diff --git a/src/printer/smt1/smt1_printer.h b/src/printer/smt1/smt1_printer.h index ca19c19c2..118f6b028 100644 --- a/src/printer/smt1/smt1_printer.h +++ b/src/printer/smt1/smt1_printer.h @@ -30,6 +30,7 @@ namespace smt1 { class Smt1Printer : public CVC4::Printer { void toStream(std::ostream& out, Model& m, const Command* c) const throw(); public: + using CVC4::Printer::toStream; void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 32a0c94ba..cf0d06e6c 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -32,6 +32,7 @@ class Smt2Printer : public CVC4::Printer { void toStream(std::ostream& out, Model& m, const Command* c) const throw(); void toStream(std::ostream& out, Model& m) const throw(); public: + using CVC4::Printer::toStream; void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw(); void toStream(std::ostream& out, const CommandStatus* s) const throw(); diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 09d8fcbd4..2eabdbea3 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -304,7 +304,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa } } - BooleanTermCache::iterator i = d_termCache.find(make_pair<Node, theory::TheoryId>(top, parentTheory)); + BooleanTermCache::iterator i = d_termCache.find(pair<Node, theory::TheoryId>(top, parentTheory)); if(i != d_termCache.end()) { return (*i).second.isNull() ? Node(top) : (*i).second; } diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i index c53bb8ce5..c326d95d3 100644 --- a/src/smt/smt_engine.i +++ b/src/smt/smt_engine.i @@ -2,6 +2,7 @@ #include "smt/smt_engine.h" %} +%ignore CVC4::SmtEngine::setLogic(const char*); %ignore CVC4::SmtEngine::getProof; %ignore CVC4::stats::getStatisticsRegistry(SmtEngine*); %ignore CVC4::smt::beforeSearch(std::string, bool, SmtEngine*); diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 1952108f6..f95382cb1 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -119,11 +119,12 @@ EXTRA_DIST = \ bool.i \ sexpr.i \ datatype.i \ + tuple.i \ + record.i \ output.i \ cardinality.i \ result.i \ configuration.i \ - cvc4_assert.i \ bitvector.i \ subrange_bound.i \ exception.i \ diff --git a/src/util/cvc4_assert.i b/src/util/cvc4_assert.i deleted file mode 100644 index 45d76312d..000000000 --- a/src/util/cvc4_assert.i +++ /dev/null @@ -1,8 +0,0 @@ -%{ -#include "util/cvc4_assert.h" -%} - -%rename(CVC4IllegalArgumentException) CVC4::IllegalArgumentException; -%ignore CVC4::InternalErrorException::InternalErrorException(const char*, const char*, unsigned, const char*, ...); - -%include "util/cvc4_assert.h" diff --git a/src/util/output.h b/src/util/output.h index 477035a16..0b89980f2 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -570,7 +570,7 @@ public: * used for clearly separating different phases of an algorithm, * or iterations of a loop, or... etc. */ -class IndentedScope { +class CVC4_PUBLIC IndentedScope { CVC4ostream d_out; public: inline IndentedScope(CVC4ostream out); diff --git a/src/util/output.i b/src/util/output.i index dc524e185..74953ba53 100644 --- a/src/util/output.i +++ b/src/util/output.i @@ -3,6 +3,7 @@ %} %ignore CVC4::null_streambuf; +%ignore std::streambuf; %feature("valuewrapper") std::ostream; // There are issues with SWIG's attempted wrapping of these variables when @@ -10,13 +11,17 @@ %ignore CVC4::null_sb; %ignore CVC4::null_os; %ignore CVC4::DumpOutC::dump_cout; +%ignore CVC4::CVC4ostream; %ignore operator<<; %ignore on(std::string); %ignore isOn(std::string); %ignore off(std::string); %ignore printf(std::string, const char*, ...); -%ignore operator()(std::string); + +%ignore CVC4::IndentedScope; +%ignore CVC4::push(CVC4ostream&); +%ignore CVC4::pop(CVC4ostream&); %ignore CVC4::ScopedDebug::ScopedDebug(std::string); %ignore CVC4::ScopedDebug::ScopedDebug(std::string, bool); @@ -24,6 +29,22 @@ %ignore CVC4::ScopedTrace::ScopedTrace(std::string); %ignore CVC4::ScopedTrace::ScopedTrace(std::string, bool); +%ignore CVC4::WarningC::WarningC(std::ostream*); +%ignore CVC4::MessageC::MessageC(std::ostream*); +%ignore CVC4::NoticeC::NoticeC(std::ostream*); +%ignore CVC4::ChatC::ChatC(std::ostream*); +%ignore CVC4::TraceC::TraceC(std::ostream*); +%ignore CVC4::DebugC::DebugC(std::ostream*); +%ignore CVC4::DumpOutC::DumpOutC(std::ostream*); + +%ignore CVC4::WarningC::operator(); +%ignore CVC4::MessageC::operator(); +%ignore CVC4::NoticeC::operator(); +%ignore CVC4::ChatC::operator(); +%ignore CVC4::TraceC::operator(); +%ignore CVC4::DebugC::operator(); +%ignore CVC4::DumpOutC::operator(); + %ignore CVC4::WarningC::getStream(); %ignore CVC4::MessageC::getStream(); %ignore CVC4::NoticeC::getStream(); @@ -43,7 +64,7 @@ %ignore operator std::ostream&; %ignore operator CVC4ostream; -%rename(get) operator(); +%rename(get) operator (); %rename(ok) operator bool; %include "util/output.h" diff --git a/src/util/record.i b/src/util/record.i index f662178c2..2805d2fdf 100644 --- a/src/util/record.i +++ b/src/util/record.i @@ -1,5 +1,93 @@ %{ #include "util/record.h" + +#ifdef SWIGJAVA + +#include "bindings/java_iterator_adapter.h" +#include "bindings/java_stream_adapters.h" + +#endif /* SWIGJAVA */ %} +%rename(equals) CVC4::RecordSelect::operator==(const RecordSelect&) const; +%ignore CVC4::RecordSelect::operator!=(const RecordSelect&) const; + +%rename(equals) CVC4::RecordUpdate::operator==(const RecordUpdate&) const; +%ignore CVC4::RecordUpdate::operator!=(const RecordUpdate&) const; + +%rename(equals) CVC4::Record::operator==(const Record&) const; +%ignore CVC4::Record::operator!=(const Record&) const; +%rename(getField) CVC4::Record::operator[](size_t) const; + +// These Object arrays are always of two elements, the first is a String and the second a +// Type. (On the C++ side, it is a std::pair<std::string, Type>.) +%typemap(jni) std::pair<std::string, CVC4::Type> "jobjectArray"; +%typemap(jtype) std::pair<std::string, CVC4::Type> "java.lang.Object[]"; +%typemap(jstype) std::pair<std::string, CVC4::Type> "java.lang.Object[]"; +%typemap(javaout) std::pair<std::string, CVC4::Type> { return $jnicall; } +%typemap(out) std::pair<std::string, CVC4::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/Type"); + jmethodID methodid = jenv->GetMethodID(clazz, "<init>", "(JZ)V"); + jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast<long>(new CVC4::Type($1.second)), true)); + }; + +#ifdef SWIGJAVA + +// Instead of Record::begin() and end(), create an +// iterator() method on the Java side that returns a Java-style +// Iterator. +%ignore CVC4::Record::begin() const; +%ignore CVC4::Record::end() const; +%extend CVC4::Record { + CVC4::Type find(std::string name) const { + CVC4::Record::const_iterator i; + for(i = $self->begin(); i != $self->end(); ++i) { + if((*i).first == name) { + return (*i).second; + } + } + return CVC4::Type(); + } + + CVC4::JavaIteratorAdapter<CVC4::Record> iterator() { + return CVC4::JavaIteratorAdapter<CVC4::Record>(*$self); + } +} + +// Record is "iterable" on the Java side +%typemap(javainterfaces) CVC4::Record "java.lang.Iterable<Object[]>"; + +// the JavaIteratorAdapter should not be public, and implements Iterator +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::Record> "class"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::Record> "java.util.Iterator<Object[]>"; +// add some functions to the Java side (do it here because there's no way to do these in C++) +%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::Record> " + public void remove() { + throw new java.lang.UnsupportedOperationException(); + } + + public Object[] next() { + if(hasNext()) { + return getNext(); + } else { + throw new java.util.NoSuchElementException(); + } + } +" +// getNext() just allows C++ iterator access from Java-side next(), make it private +%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::Record>::getNext() "private"; + +#endif /* SWIGJAVA */ + %include "util/record.h" + +#ifdef SWIGJAVA + +%include "bindings/java_iterator_adapter.h" +%include "bindings/java_stream_adapters.h" + +%template(JavaIteratorAdapter_Record) CVC4::JavaIteratorAdapter<CVC4::Record>; + +#endif /* SWIGJAVA */ diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 135a83c7e..e9ea83aa1 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -37,6 +37,13 @@ namespace CVC4 { +class CVC4_PUBLIC SExprKeyword { + std::string d_str; +public: + SExprKeyword(const std::string& s) : d_str(s) {} + const std::string& getString() const { return d_str; } +};/* class SExpr::Keyword */ + /** * A simple S-expression. An S-expression is either an atom with a * string value, or a list of other S-expressions. @@ -65,11 +72,7 @@ class CVC4_PUBLIC SExpr { public: - class CVC4_PUBLIC Keyword : protected std::string { - public: - Keyword(const std::string& s) : std::string(s) {} - const std::string& getString() const { return *this; } - };/* class SExpr::Keyword */ + typedef SExprKeyword Keyword; SExpr() : d_sexprType(SEXPR_STRING), diff --git a/src/util/sexpr.i b/src/util/sexpr.i index 5d78142f3..4c89c5019 100644 --- a/src/util/sexpr.i +++ b/src/util/sexpr.i @@ -10,6 +10,11 @@ std::string toString() const { return self->getValue(); } };/* CVC4::SExpr */ +%ignore CVC4::SExpr::SExpr(int); +%ignore CVC4::SExpr::SExpr(unsigned int); +%ignore CVC4::SExpr::SExpr(unsigned long); +%ignore CVC4::SExpr::SExpr(const char*); + %rename(equals) CVC4::SExpr::operator==(const SExpr&) const; %ignore CVC4::SExpr::operator!=(const SExpr&) const; diff --git a/src/util/statistics.i b/src/util/statistics.i index 7f3bbe526..bd3a4eeb9 100644 --- a/src/util/statistics.i +++ b/src/util/statistics.i @@ -62,7 +62,7 @@ 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)); + jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast<long>(new CVC4::SExpr($1.second)), true)); }; #endif /* SWIGJAVA */ diff --git a/src/util/tuple.i b/src/util/tuple.i index d7301d201..f3de7b51b 100644 --- a/src/util/tuple.i +++ b/src/util/tuple.i @@ -2,4 +2,10 @@ #include "util/tuple.h" %} +%rename(equals) CVC4::TupleSelect::operator==(const TupleSelect&) const; +%ignore CVC4::TupleSelect::operator!=(const TupleSelect&) const; + +%rename(equals) CVC4::TupleUpdate::operator==(const TupleUpdate&) const; +%ignore CVC4::TupleUpdate::operator!=(const TupleUpdate&) const; + %include "util/tuple.h" diff --git a/src/util/util_model.i b/src/util/util_model.i deleted file mode 100644 index 0d1b3bc81..000000000 --- a/src/util/util_model.i +++ /dev/null @@ -1,5 +0,0 @@ -%{ -#include "util/util_model.h" -%} - -%include "util/util_model.h" |