# -----------------------
# Supported language bindings for CVC4.
AC_DEFUN([CVC4_SUPPORTED_BINDINGS],
-[c,java])
+[c,c++,java])
# CVC4_ALL_BINDINGS
# -----------------
AC_DEFUN([CVC4_CXX_OPTION], [
AC_MSG_CHECKING([whether $CXX supports $1])
cvc4_save_CXXFLAGS="$CXXFLAGS"
-CXXFLAGS="$CXXFLAGS $1"
+CXXFLAGS="$CXXFLAGS $WERROR $1"
AC_LANG_PUSH([C++])
AC_COMPILE_IFELSE([AC_LANG_SOURCE([int main() { return 0; }])],
[AC_MSG_RESULT([yes]); $2='$1'],
# Check for ANTLR runantlr script (defined in config/antlr.m4)
AC_PROG_ANTLR
+CVC4_CXX_OPTION([-Werror], [WERROR])
CVC4_CXX_OPTION([-Wno-conversion-null], [WNO_CONVERSION_NULL])
+CVC4_CXX_OPTION([-Wno-tautological-compare], [WNO_TAUTOLOGICAL_COMPARE])
+CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES])
CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
+AC_SUBST([WERROR])
AC_SUBST([WNO_CONVERSION_NULL])
+AC_SUBST([WNO_TAUTOLOGICAL_COMPARE])
+AC_SUBST([WNO_PARENTHESES])
AC_SUBST([WNO_UNINITIALIZED])
AC_SUBST([WNO_UNUSED_VARIABLE])
AC_SUBST([FNO_STRICT_ALIASING])
BitVectorsAndArrays.class \
Combination.class \
HelloWorld.class \
- LinearArith.class
+ LinearArith.class \
+ PipedInput.class
endif
%.class: %.java
BitVectorsAndArrays.java \
Combination.java \
HelloWorld.java \
- LinearArith.java
+ LinearArith.java \
+ PipedInput.java
# for installation
examplesdir = $(docdir)/$(subdir)
--- /dev/null
+/********************* */
+/*! \file PipedInput.java
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A simple demonstration of the input parsing capabilities of CVC4
+ ** when used from Java
+ **
+ ** A simple demonstration of the input parsing capabilities of CVC4 when
+ ** used from Java.
+ **/
+
+import edu.nyu.acsys.CVC4.*;
+import java.io.*;
+
+public class PipedInput {
+ public static void main(String[] args) throws IOException {
+ System.loadLibrary("cvc4jni");
+
+ // Boilerplate setup for CVC4
+ ExprManager exprMgr = new ExprManager();
+ SmtEngine smt = new SmtEngine(exprMgr);
+ smt.setOption("incremental", new SExpr(true));
+ smt.setOption("output-language", new SExpr("smt2"));
+
+ // Set up a pair of connected Java streams
+ PipedOutputStream solverPipe = new PipedOutputStream();
+ PrintWriter toSolver = new PrintWriter(solverPipe);
+ PipedInputStream stream = new PipedInputStream(solverPipe);
+
+ // Write some things to CVC4's input stream, making sure to flush()
+ toSolver.println("(set-logic QF_LIA)");
+ toSolver.println("(declare-fun x () Int)");
+ toSolver.println("(assert (= x 5))");
+ toSolver.println("(check-sat)");
+ toSolver.flush();
+
+ // Set up the CVC4 parser
+ ParserBuilder pbuilder =
+ new ParserBuilder(exprMgr, "<string 1>")
+ .withInputLanguage(InputLanguage.INPUT_LANG_SMTLIB_V2)
+ .withLineBufferedStreamInput((java.io.InputStream)stream);
+ Parser parser = pbuilder.build();
+
+ // Read all the commands thus far
+ Command cmd;
+ while((cmd = parser.nextCommand()) != null) {
+ System.out.println(cmd);
+ cmd.invoke(smt, System.out);
+ }
+
+ // Write some more things to CVC4's input stream, making sure to flush()
+ toSolver.println("(assert (= x 10))");
+ toSolver.println("(check-sat)");
+ toSolver.flush();
+
+ // Read all the commands thus far
+ while((cmd = parser.nextCommand()) != null) {
+ System.out.println(cmd);
+ cmd.invoke(smt, System.out);
+ }
+ }
+}
//#include "fdstream.h"
#include <string>
#include <cassert>
+#include <cerrno>
#include <unistd.h>
#ifdef CVC4_DEBUG
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);
}
-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
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
Type ValidityChecker::createType(const std::string& typeName, const Type& def) {
d_parserContext->defineType(typeName, def);
+ return def;
}
Type ValidityChecker::lookupType(const std::string& typeName) {
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) {
%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 >;
*(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);
%}
%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";
%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"
%{
#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();
%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 */
%{
#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;
}/* 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>;
%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"
%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"
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)
}/* namespace CVC4::parser */
}/* namespace CVC4 */
+%ignore CVC4::parser::Parser::ExprStream;
+
%include "parser/parser.h"
%{
%}
%ignore CVC4::parser::ParserException::ParserException(const char*);
+%ignore CVC4::parser::ParserEndOfFileException::ParserEndOfFileException(const char*);
%include "parser/parser_exception.h"
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)
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)
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)
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();
#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>
#include <iostream>
#include "printer/printer.h"
-#include "printer/dagification_visitor.h"
-#include "theory/substitutions.h"
-#include "util/node_visitor.h"
namespace CVC4 {
namespace 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();
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();
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();
}
}
- 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;
}
#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*);
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 \
+++ /dev/null
-%{
-#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"
* 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);
%}
%ignore CVC4::null_streambuf;
+%ignore std::streambuf;
%feature("valuewrapper") std::ostream;
// There are issues with SWIG's attempted wrapping of these variables when
%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);
%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();
%ignore operator std::ostream&;
%ignore operator CVC4ostream;
-%rename(get) operator();
+%rename(get) operator ();
%rename(ok) operator bool;
%include "util/output.h"
%{
#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 */
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.
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),
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;
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 */
#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"
+++ /dev/null
-%{
-#include "util/util_model.h"
-%}
-
-%include "util/util_model.h"
projects / cvc5.git / commitdiff