diff options
27 files changed, 1366 insertions, 396 deletions
diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java index 943ac3aa0..81e7a1f64 100644 --- a/examples/SimpleVC.java +++ b/examples/SimpleVC.java @@ -52,8 +52,7 @@ public class SimpleVC { Expr twox_plus_y_geq_3 = em.mkExpr(Kind.GEQ, twox_plus_y, three); Expr formula = - new Expr(em.mkExpr(Kind.AND, x_positive, y_positive)). - impExpr(new Expr(twox_plus_y_geq_3)); + em.mkExpr(Kind.AND, x_positive, y_positive).impExpr(twox_plus_y_geq_3); System.out.println( "Checking entailment of formula " + formula + " with CVC4."); diff --git a/examples/api/java/BitVectorsAndArrays.java b/examples/api/java/BitVectorsAndArrays.java index 8283794a5..6adb2a61d 100644 --- a/examples/api/java/BitVectorsAndArrays.java +++ b/examples/api/java/BitVectorsAndArrays.java @@ -69,7 +69,7 @@ public class BitVectorsAndArrays { Expr old_current = em.mkExpr(Kind.SELECT, current_array, index); Expr two = em.mkConst(new BitVector(32, 2)); - vectorExpr assertions = new vectorExpr(); + vectorExpr assertions = new vectorExpr(em); for (int i = 1; i < k; ++i) { index = em.mkConst(new BitVector(index_size, new edu.stanford.CVC4.Integer(i))); Expr new_current = em.mkExpr(Kind.BITVECTOR_MULT, two, old_current); diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java index 7ef05f7e1..5c9b0ef72 100644 --- a/examples/api/java/Datatypes.java +++ b/examples/api/java/Datatypes.java @@ -32,11 +32,11 @@ public class Datatypes { // symbols are assigned to its constructors, selectors, and testers. Datatype consListSpec = new Datatype(em, "list"); // give a name - DatatypeConstructor cons = new DatatypeConstructor("cons"); + DatatypeConstructor cons = new DatatypeConstructor(em, "cons"); cons.addArg("head", em.integerType()); cons.addArg("tail", new DatatypeSelfType()); // a list consListSpec.addConstructor(cons); - DatatypeConstructor nil = new DatatypeConstructor("nil"); + DatatypeConstructor nil = new DatatypeConstructor(em, "nil"); consListSpec.addConstructor(nil); System.out.println("spec is:"); diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java index 20e27d33b..f5c5db8a7 100644 --- a/examples/api/java/Relations.java +++ b/examples/api/java/Relations.java @@ -82,7 +82,7 @@ public class Relations { // (declare-sort Person 0) Type personType = manager.mkSort("Person", 0); - vectorType vector1 = new vectorType(); + vectorType vector1 = new vectorType(manager); vector1.add(personType); // (Tuple Person) @@ -90,7 +90,7 @@ public class Relations { // (Set (Tuple Person)) SetType relationArity1 = manager.mkSetType(tupleArity1); - vectorType vector2 = new vectorType(); + vectorType vector2 = new vectorType(manager); vector2.add(personType); vector2.add(personType); // (Tuple Person Person) @@ -99,11 +99,11 @@ public class Relations { SetType relationArity2 = manager.mkSetType(tupleArity2); // empty set - EmptySet emptySet = new EmptySet(relationArity1); + EmptySet emptySet = new EmptySet(manager, relationArity1); Expr emptySetExpr = manager.mkConst(emptySet); // empty relation - EmptySet emptyRelation = new EmptySet(relationArity2); + EmptySet emptyRelation = new EmptySet(manager, relationArity2); Expr emptyRelationExpr = manager.mkConst(emptyRelation); // universe set @@ -174,7 +174,7 @@ public class Relations { Expr xxTuple = manager.mkExpr(Kind.APPLY_CONSTRUCTOR, constructor, x, x); Expr member = manager.mkExpr(Kind.MEMBER, xxTuple, ancestor); Expr notMember = manager.mkExpr(Kind.NOT, member); - vectorExpr vectorExpr = new vectorExpr(); + vectorExpr vectorExpr = new vectorExpr(manager); vectorExpr.add(x); Expr quantifiedVariables = manager.mkExpr(Kind.BOUND_VAR_LIST, x); Expr noSelfAncestor = diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt index 4e1b96af9..8e919db86 100644 --- a/src/bindings/java/CMakeLists.txt +++ b/src/bindings/java/CMakeLists.txt @@ -97,7 +97,6 @@ set(gen_java_files ${CMAKE_CURRENT_BINARY_DIR}/LastExceptionBuffer.java ${CMAKE_CURRENT_BINARY_DIR}/LogicException.java ${CMAKE_CURRENT_BINARY_DIR}/LogicInfo.java - ${CMAKE_CURRENT_BINARY_DIR}/Map_ExprExpr.java ${CMAKE_CURRENT_BINARY_DIR}/ModalException.java ${CMAKE_CURRENT_BINARY_DIR}/OptionException.java ${CMAKE_CURRENT_BINARY_DIR}/Options.java @@ -107,10 +106,6 @@ set(gen_java_files ${CMAKE_CURRENT_BINARY_DIR}/Rational.java ${CMAKE_CURRENT_BINARY_DIR}/RationalHashFunction.java ${CMAKE_CURRENT_BINARY_DIR}/RealType.java - ${CMAKE_CURRENT_BINARY_DIR}/Record.java - ${CMAKE_CURRENT_BINARY_DIR}/RecordHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/RecordUpdate.java - ${CMAKE_CURRENT_BINARY_DIR}/RecordUpdateHashFunction.java ${CMAKE_CURRENT_BINARY_DIR}/RecoverableModalException.java ${CMAKE_CURRENT_BINARY_DIR}/RegExpLoop.java ${CMAKE_CURRENT_BINARY_DIR}/RegExpRepeat.java @@ -122,19 +117,14 @@ set(gen_java_files ${CMAKE_CURRENT_BINARY_DIR}/SExprKeyword.java ${CMAKE_CURRENT_BINARY_DIR}/SExprType.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Model.java - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Printer.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__options__InstFormatMode.java - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_Listener.java - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_ListenerCollection__Registration.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_MaybeT_CVC4__Rational_t.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_Type.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__istream.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__ostream.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__shared_ptrT_CVC4__SygusPrintCallback_t.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__string.java - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__unordered_mapT_CVC4__Expr_CVC4__ProofLetCount_CVC4__ExprHashFunction_t.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_CVC4__DatatypeConstructorArg_t.java - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_CVC4__DatatypeConstructor_t.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_std__pairT_CVC4__Expr_CVC4__Expr_t_t.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_std__vectorT_std__string_t_t.java ${CMAKE_CURRENT_BINARY_DIR}/SelectorType.java @@ -147,7 +137,6 @@ set(gen_java_files ${CMAKE_CURRENT_BINARY_DIR}/Statistics.java ${CMAKE_CURRENT_BINARY_DIR}/StatisticsBase.java ${CMAKE_CURRENT_BINARY_DIR}/StringType.java - ${CMAKE_CURRENT_BINARY_DIR}/SygusPrintCallback.java ${CMAKE_CURRENT_BINARY_DIR}/TesterType.java ${CMAKE_CURRENT_BINARY_DIR}/TheoryId.java ${CMAKE_CURRENT_BINARY_DIR}/TupleUpdate.java @@ -163,13 +152,10 @@ set(gen_java_files ${CMAKE_CURRENT_BINARY_DIR}/UnsafeInterruptException.java ${CMAKE_CURRENT_BINARY_DIR}/UnsatCore.java ${CMAKE_CURRENT_BINARY_DIR}/VariableTypeMap.java - ${CMAKE_CURRENT_BINARY_DIR}/hashmapExpr.java - ${CMAKE_CURRENT_BINARY_DIR}/pairStringType.java ${CMAKE_CURRENT_BINARY_DIR}/setOfType.java ${CMAKE_CURRENT_BINARY_DIR}/vectorDatatype.java ${CMAKE_CURRENT_BINARY_DIR}/vectorDatatypeType.java ${CMAKE_CURRENT_BINARY_DIR}/vectorExpr.java - ${CMAKE_CURRENT_BINARY_DIR}/vectorPairStringType.java ${CMAKE_CURRENT_BINARY_DIR}/vectorSExpr.java ${CMAKE_CURRENT_BINARY_DIR}/vectorString.java ${CMAKE_CURRENT_BINARY_DIR}/vectorType.java diff --git a/src/bindings/java/cvc4_std_vector.i b/src/bindings/java/cvc4_std_vector.i new file mode 100644 index 000000000..e032426a0 --- /dev/null +++ b/src/bindings/java/cvc4_std_vector.i @@ -0,0 +1,206 @@ +/** + * The following file is based on + * https://github.com/swig/swig/blob/master/Lib/java/std_vector.i + * + * Note: The SWIG library is under a different license than SWIG itself. See + * https://github.com/swig/swig/blob/master/LICENSE for details. + * + * This file defines the macro SWIG_STD_VECTOR_EM to wrap a C++ std::vector for + * Java, similar to the SWIG library. The core difference is that the utilities + * in this file add a reference to an ExprManager to keep it alive as long as + * the vector lives. + */ + +%include <std_common.i> + +%{ +#include <vector> +#include <stdexcept> +%} + +%fragment("SWIG_VectorSize", "header", fragment="SWIG_JavaIntFromSize_t") { +SWIGINTERN jint SWIG_VectorSize(size_t size) { + static const jint JINT_MAX = 0x7FFFFFFF; + if (size > static_cast<size_t>(JINT_MAX)) + { + throw std::out_of_range("vector size is too large to fit into a Java int"); + } + return static_cast<jint>(size); +} +} + +%define SWIG_STD_VECTOR_EM(CTYPE, CONST_REFERENCE) + +namespace std { + template<> class vector<CTYPE> { + +%typemap(javabase) std::vector< CTYPE > "java.util.AbstractList<$typemap(jstype, CTYPE)>" +%typemap(javainterfaces) std::vector< CTYPE > "java.util.RandomAccess" + +%typemap(javabody) std::vector< CTYPE > %{ + private long swigCPtr; + protected boolean swigCMemOwn; + private ExprManager em; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + swigCMemOwn = cMemoryOwn; + swigCPtr = cPtr; + this.em = em; + } + + public $javaclassname(ExprManager em) { + this(); + this.em = em; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javaconstruct) std::vector<CTYPE> { + this(null, $imcall, true); +} + +%javamethodmodifiers vector() "private"; + +%proxycode %{ + public $javaclassname(ExprManager em, $typemap(jstype, CTYPE)[] initialElements) { + this(em); + reserve(initialElements.length); + + for ($typemap(jstype, CTYPE) element : initialElements) { + add(element); + } + } + + public $javaclassname(ExprManager em, Iterable<$typemap(jstype, CTYPE)> initialElements) { + this(em); + for ($typemap(jstype, CTYPE) element : initialElements) { + add(element); + } + } + + public $typemap(jstype, CTYPE) get(int index) { + return doGet(index); + } + + public $typemap(jstype, CTYPE) set(int index, $typemap(jstype, CTYPE) e) { + return doSet(index, e); + } + + public boolean add($typemap(jstype, CTYPE) e) { + modCount++; + doAdd(e); + return true; + } + + public void add(int index, $typemap(jstype, CTYPE) e) { + modCount++; + doAdd(index, e); + } + + public $typemap(jstype, CTYPE) remove(int index) { + modCount++; + return doRemove(index); + } + + protected void removeRange(int fromIndex, int toIndex) { + modCount++; + doRemoveRange(fromIndex, toIndex); + } + + public int size() { + return doSize(); + } +%} + + public: + typedef size_t size_type; + typedef ptrdiff_t difference_type; + typedef CTYPE value_type; + typedef CTYPE *pointer; + typedef CTYPE const *const_pointer; + typedef CTYPE &reference; + typedef CONST_REFERENCE const_reference; + + vector(); + size_type capacity() const; + void reserve(size_type n) throw (std::length_error); + %rename(isEmpty) empty; + bool empty() const; + void clear(); + %extend { + %fragment("SWIG_VectorSize"); + + vector(jint count, const CTYPE &value) throw (std::out_of_range) { + if (count < 0) + throw std::out_of_range("vector count must be positive"); + return new std::vector< CTYPE >(static_cast<std::vector< CTYPE >::size_type>(count), value); + } + + jint doSize() const throw (std::out_of_range) { + return SWIG_VectorSize(self->size()); + } + + void doAdd(const value_type& x) { + self->push_back(x); + } + + void doAdd(jint index, const value_type& x) throw (std::out_of_range) { + jint size = static_cast<jint>(self->size()); + if (0 <= index && index <= size) { + self->insert(self->begin() + index, x); + } else { + throw std::out_of_range("vector index out of range"); + } + } + + value_type doRemove(jint index) throw (std::out_of_range) { + jint size = static_cast<jint>(self->size()); + if (0 <= index && index < size) { + CTYPE const old_value = (*self)[index]; + self->erase(self->begin() + index); + return old_value; + } else { + throw std::out_of_range("vector index out of range"); + } + } + + CONST_REFERENCE doGet(jint index) throw (std::out_of_range) { + jint size = static_cast<jint>(self->size()); + if (index >= 0 && index < size) + return (*self)[index]; + else + throw std::out_of_range("vector index out of range"); + } + + value_type doSet(jint index, const value_type& val) throw (std::out_of_range) { + jint size = static_cast<jint>(self->size()); + if (index >= 0 && index < size) { + CTYPE const old_value = (*self)[index]; + (*self)[index] = val; + return old_value; + } + else + throw std::out_of_range("vector index out of range"); + } + + void doRemoveRange(jint fromIndex, jint toIndex) throw (std::out_of_range) { + jint size = static_cast<jint>(self->size()); + if (0 <= fromIndex && fromIndex <= toIndex && toIndex <= size) { + self->erase(self->begin() + fromIndex, self->begin() + toIndex); + } else { + throw std::out_of_range("vector index out of range"); + } + } + } + }; +} + +// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea +%typemap(javaconstruct) vector<CTYPE> { + this(null, $imcall, true); +} + +%enddef diff --git a/src/bindings/java_iterator_adapter.h b/src/bindings/java_iterator_adapter.h index a4966debf..864619004 100644 --- a/src/bindings/java_iterator_adapter.h +++ b/src/bindings/java_iterator_adapter.h @@ -46,6 +46,8 @@ class JavaIteratorAdapter "value_type must be convertible from T::const_iterator::value_type"); } + JavaIteratorAdapter() = delete; + bool hasNext() { return d_it != d_t.end(); } value_type getNext() diff --git a/src/bindings/java_iterator_adapter.i b/src/bindings/java_iterator_adapter.i new file mode 100644 index 000000000..5f814edd7 --- /dev/null +++ b/src/bindings/java_iterator_adapter.i @@ -0,0 +1,75 @@ +%{ +#include "bindings/java_iterator_adapter.h" +%} + +#ifdef SWIGJAVA + +%define SWIG_JAVA_ITERATOR_ADAPTER(TTYPE, VTYPE) + +%typemap(javabody) CVC4::JavaIteratorAdapter %{ + private long swigCPtr; + protected boolean swigCMemOwn; + private ExprManager em; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + swigCMemOwn = cMemoryOwn; + swigCPtr = cPtr; + this.em = em; + } + + public $javaclassname(ExprManager em, $typemap(jstype, TTYPE) t) { + this(t); + this.em = em; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea +%typemap(javaconstruct) JavaIteratorAdapter<TTYPE, VTYPE> { + this(null, $imcall, true); +} + +%typemap(javaconstruct) CVC4::JavaIteratorAdapter<TTYPE, VTYPE> { + this(null, $imcall, true); +} + +%feature("valuewrapper") CVC4::JavaIteratorAdapter<TTYPE, VTYPE>; + +// the JavaIteratorAdapter should not be public, and implements Iterator +%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<TTYPE, VTYPE> "class"; +%typemap(javainterfaces) CVC4::JavaIteratorAdapter< TTYPE, VTYPE > "java.util.Iterator<$typemap(jstype, VTYPE)>"; + +// add some functions to the Java side (do it here because there's no way to do these in C++) +%typemap(javacode) CVC4::JavaIteratorAdapter<TTYPE, VTYPE> " + public void remove() { + throw new java.lang.UnsupportedOperationException(); + } + + public $typemap(jstype, VTYPE) 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<TTYPE, VTYPE>::getNext() "private"; + +%javamethodmodifiers CVC4::JavaIteratorAdapter<TTYPE, VTYPE>::JavaIteratorAdapter(const TTYPE& t) "private"; + +%enddef + +%include "bindings/java_iterator_adapter.h" + +namespace CVC4 { + template<class T, class V> class JavaIteratorAdapter { + SWIG_JAVA_ITERATOR_ADAPTER(T, V) + }; +} + +#endif diff --git a/src/cvc4.i b/src/cvc4.i index 32bdd0887..f62611e8f 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -58,17 +58,10 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; %} #endif /* SWIGPYTHON */ -%template(vectorType) std::vector< CVC4::Type >; -%template(vectorExpr) std::vector< CVC4::Expr >; %template(vectorUnsignedInt) std::vector< unsigned int >; -%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 >; -%template(vectorPairStringType) std::vector< std::pair< std::string, CVC4::Type > >; -%template(pairStringType) std::pair< std::string, CVC4::Type >; %template(setOfType) std::set< CVC4::Type >; -%template(hashmapExpr) std::unordered_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >; // This is unfortunate, but seems to be necessary; if we leave NULL // defined, swig will expand it to "(void*) 0", and some of swig's @@ -77,9 +70,6 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; #ifdef SWIGJAVA -#include "bindings/java_iterator_adapter.h" -#include "bindings/java_stream_adapters.h" - // Map C++ exceptions of type CVC4::Exception to Java exceptions of type // edu.stanford.CVC4.Exception // @@ -92,6 +82,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; return $null; } +%include "bindings/java_iterator_adapter.i" %include "java/typemaps.i" // primitive pointers and references %include "java/std_string.i" // map std::string to java.lang.String %include "java/arrays_java.i" // C arrays to Java arrays @@ -197,6 +188,8 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; JCALL3(ReleaseByteArrayElements, jenv, ba, bae, 0); } +%include "bindings/java_stream_adapters.h" + #endif /* SWIGJAVA */ // TIM: @@ -232,8 +225,6 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; %include "expr/ascription_type.i" %include "expr/emptyset.i" %include "expr/expr_sequence.i" -%include "expr/datatype.i" -%include "expr/record.i" %include "proof/unsat_core.i" // TIM: @@ -245,6 +236,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; // TIM: // The remainder of the includes: +%include "expr/datatype.i" %include "expr/expr.i" %include "expr/expr_manager.i" %include "expr/variable_type_map.i" @@ -254,5 +246,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; %include "theory/logic_info.i" %include "theory/theory_id.i" +%include "expr/array_store_all.i" + // Tim: This should come after "theory/logic_info.i". %include "smt/smt_engine.i" diff --git a/src/expr/array_store_all.i b/src/expr/array_store_all.i index b66e4a178..5158a21d9 100644 --- a/src/expr/array_store_all.i +++ b/src/expr/array_store_all.i @@ -2,15 +2,63 @@ #include "expr/array_store_all.h" %} +#ifdef SWIGJAVA + +%typemap(javabody) CVC4::ArrayStoreAll %{ + private long swigCPtr; + protected boolean swigCMemOwn; + private ExprManager em; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + swigCMemOwn = cMemoryOwn; + swigCPtr = cPtr; + this.em = em; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } + + public $javaclassname(ExprManager em, ArrayType type, Expr expr) { + this(type, expr); + this.em = em; + } +%} + +// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea +%typemap(javaconstruct) ArrayStoreAll { + this(null, $imcall, true); +} + +%typemap(javaconstruct) CVC4::ArrayStoreAll { + this(null, $imcall, true); +} + +%typemap(javaout) const CVC4::Expr& { + return new Expr(this.em, $jnicall, false); +} + +%typemap(javaout) const CVC4::ArrayType& { + return new ArrayType(this.em, $jnicall, false); +} + +%typemap(javaout) const CVC4::ArrayStoreAll& { + return new ArrayStoreAll(this.em, $jnicall, false); +} + +%javamethodmodifiers CVC4::ArrayStoreAll::ArrayStoreAll(const ArrayType& type, const Expr& expr) "private"; + +#endif /* SWIGJAVA */ + +%ignore CVC4::ArrayStoreAll::ArrayStoreAll(const ArrayStoreAll& other); %rename(equals) CVC4::ArrayStoreAll::operator==(const ArrayStoreAll&) const; %ignore CVC4::ArrayStoreAll::operator!=(const ArrayStoreAll&) const; +%ignore CVC4::ArrayStoreAll::operator=(const ArrayStoreAll&); %rename(less) CVC4::ArrayStoreAll::operator<(const ArrayStoreAll&) const; %rename(lessEqual) CVC4::ArrayStoreAll::operator<=(const ArrayStoreAll&) const; %rename(greater) CVC4::ArrayStoreAll::operator>(const ArrayStoreAll&) const; %rename(greaterEqual) CVC4::ArrayStoreAll::operator>=(const ArrayStoreAll&) const; - %rename(apply) CVC4::ArrayStoreAllHashFunction::operator()(const ArrayStoreAll&) const; - %ignore CVC4::operator<<(std::ostream&, const ArrayStoreAll&); %include "expr/type.i" diff --git a/src/expr/ascription_type.i b/src/expr/ascription_type.i index 57d8f97fe..c2499c00e 100644 --- a/src/expr/ascription_type.i +++ b/src/expr/ascription_type.i @@ -2,6 +2,42 @@ #include "expr/ascription_type.h" %} +#ifdef SWIGJAVA + +%typemap(javabody) CVC4::AscriptionType %{ + private long swigCPtr; + protected boolean swigCMemOwn; + private ExprManager em; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + swigCMemOwn = cMemoryOwn; + swigCPtr = cPtr; + this.em = em; // keep ref to em in SWIG proxy class + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } + + public $javaclassname(ExprManager em, Type t) { + this(t); + this.em = em; + } +%} + +// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea +%typemap(javaconstruct) AscriptionType { + this(null, $imcall, true); +} + +%typemap(javaconstruct) CVC4::AscriptionType { + this(null, $imcall, true); +} + +%javamethodmodifiers CVC4::AscriptionType::AscriptionType(Type t) "private"; + +#endif + %rename(equals) CVC4::AscriptionType::operator==(const AscriptionType&) const; %ignore CVC4::AscriptionType::operator!=(const AscriptionType&) const; diff --git a/src/expr/datatype.i b/src/expr/datatype.i index 1ac89efcb..56dd6dad4 100644 --- a/src/expr/datatype.i +++ b/src/expr/datatype.i @@ -1,93 +1,183 @@ %{ #include "expr/datatype.h" - -#ifdef SWIGJAVA - -#include "bindings/java_iterator_adapter.h" -#include "bindings/java_stream_adapters.h" - -#endif /* SWIGJAVA */ %} -%include "expr/kind.i" - -%extend std::vector< CVC4::Datatype > { - %ignore vector(size_type);// java/python/perl/others? - %ignore resize(size_type);// java/python/perl/others? - %ignore set(int i, const CVC4::Datatype& x); - %ignore to_array(); -}; -%template(vectorDatatype) std::vector< CVC4::Datatype >; - -%extend std::vector< CVC4::DatatypeConstructor > { - %ignore vector(size_type);// java/python/perl/others? - %ignore resize(size_type);// java/python/perl/others? - %ignore set(int i, const CVC4::Datatype::Constructor& x); - %ignore to_array(); -}; -//%template(vectorDatatypeConstructor) std::vector< CVC4::DatatypeConstructor >; - -%rename(equals) CVC4::Datatype::operator==(const Datatype&) const; +%ignore CVC4::Datatype::setRecord(); +%ignore CVC4::Datatype::isRecord() const; +%ignore CVC4::Datatype::getRecord() const; %ignore CVC4::Datatype::operator!=(const Datatype&) const; - %ignore CVC4::Datatype::begin(); %ignore CVC4::Datatype::end(); %ignore CVC4::Datatype::begin() const; %ignore CVC4::Datatype::end() const; - +%ignore CVC4::Datatype::getConstructors() const; +%rename(equals) CVC4::Datatype::operator==(const Datatype&) const; %rename(get) CVC4::Datatype::operator[](size_t) const; %rename(get) CVC4::Datatype::operator[](std::string) const; +%ignore CVC4::SygusPrintCallback; + %rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype&) const; %ignore CVC4::DatatypeHashFunction::operator()(const Datatype*) const; %rename(apply) CVC4::DatatypeHashFunction::operator()(const DatatypeConstructor&) const; %ignore CVC4::DatatypeHashFunction::operator()(const DatatypeConstructor*) const; +%ignore CVC4::DatatypeConstructor::DatatypeConstructor(); %ignore CVC4::DatatypeConstructor::begin(); %ignore CVC4::DatatypeConstructor::end(); %ignore CVC4::DatatypeConstructor::begin() const; %ignore CVC4::DatatypeConstructor::end() const; - %rename(get) CVC4::DatatypeConstructor::operator[](size_t) const; %rename(get) CVC4::DatatypeConstructor::operator[](std::string) const; %ignore CVC4::operator<<(std::ostream&, const Datatype&); %ignore CVC4::operator<<(std::ostream&, const DatatypeConstructor&); %ignore CVC4::operator<<(std::ostream&, const DatatypeConstructorArg&); +%ignore CVC4::operator<<(std::ostream& out, const DatatypeIndexConstant& es); %ignore CVC4::DatatypeConstructorIterator; %ignore CVC4::DatatypeConstructorArgIterator; -%feature("valuewrapper") CVC4::DatatypeUnresolvedType; -%feature("valuewrapper") CVC4::DatatypeConstructor; - - -%rename(equals) CVC4::DatatypeIndexConstant::operator==(const DatatypeIndexConstant&) const; %ignore CVC4::DatatypeIndexConstant::operator!=(const DatatypeIndexConstant&) const; - +%rename(equals) CVC4::DatatypeIndexConstant::operator==(const DatatypeIndexConstant&) const; %rename(less) CVC4::DatatypeIndexConstant::operator<(const DatatypeIndexConstant&) const; %rename(lessEqual) CVC4::DatatypeIndexConstant::operator<=(const DatatypeIndexConstant&) const; %rename(greater) CVC4::DatatypeIndexConstant::operator>(const DatatypeIndexConstant&) const; %rename(greaterEqual) CVC4::DatatypeIndexConstant::operator>=(const DatatypeIndexConstant&) const; - %rename(apply) CVC4::DatatypeIndexConstantFunction::operator()(const DatatypeIndexConstant&) const; -%ignore CVC4::operator<<(std::ostream& out, const DatatypeIndexConstant& es); +#ifdef SWIGJAVA +%typemap(javaout) CVC4::Expr { + return new Expr(this.em, $jnicall, true); +} -#ifdef SWIGJAVA +%typemap(javaout) CVC4::DatatypeType { + return new DatatypeType(this.em, $jnicall, true); +} + +%typemap(javabody) CVC4::Datatype %{ + private long swigCPtr; + protected boolean swigCMemOwn; + private ExprManager em; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + swigCMemOwn = cMemoryOwn; + swigCPtr = cPtr; + this.em = em; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } + + public static $javaclassname datatypeOf(Expr item) throws edu.stanford.CVC4.Exception { + $javaclassname result = datatypeOfInternal(item); + result.em = item.getExprManager(); + return result; + } + + public JavaIteratorAdapter_Datatype iterator() { + return new JavaIteratorAdapter_Datatype(this.em, this); + } +%} + +%javamethodmodifiers CVC4::Datatype::datatypeOf(Expr item) "private"; +%rename(datatypeOfInternal) CVC4::Datatype::datatypeOf(Expr item); + +%include "bindings/java/cvc4_std_vector.i" + +SWIG_STD_VECTOR_EM(CVC4::Datatype, const CVC4::Datatype&) -// Instead of Datatype::begin() and end(), create an -// iterator() method on the Java side that returns a Java-style -// Iterator. %extend CVC4::Datatype { - CVC4::JavaIteratorAdapter<CVC4::Datatype, CVC4::DatatypeConstructor> - iterator() - { - return CVC4::JavaIteratorAdapter<CVC4::Datatype, CVC4::DatatypeConstructor>( - *$self); +%typemap(javaout) const CVC4::Datatype& { + return new Datatype(null, $jnicall, false); +} +} + +%typemap(javaout) CVC4::Datatype { + return new Datatype(this.em, $jnicall, true); +} +%typemap(javaout) const CVC4::Datatype& { + return new Datatype(this.em, $jnicall, false); +} +%template(vectorDatatype) std::vector<CVC4::Datatype>; + +%typemap(javaout) typeVector { + return new typeVector(this.em, $jnicall, true); +} + +%typemap(javaout) const CVC4::DatatypeConstructor& { + return new DatatypeConstructor(this.em, $jnicall, false); +} + +%typemap(javabody) CVC4::DatatypeConstructor %{ + private long swigCPtr; + protected boolean swigCMemOwn; + private ExprManager em; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + swigCMemOwn = cMemoryOwn; + swigCPtr = cPtr; + this.em = em; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } + + public DatatypeConstructor(ExprManager em, String name) { + this(name); + this.em = em; + } + + public DatatypeConstructor(ExprManager em, String name, long weight) { + this(name, weight); + this.em = em; + } + + public JavaIteratorAdapter_DatatypeConstructor iterator() { + return new JavaIteratorAdapter_DatatypeConstructor(this.em, this); + } +%} + +// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea +%typemap(javaconstruct) DatatypeConstructor { + this(null, $imcall, true); +} + +%typemap(javaconstruct) CVC4::DatatypeConstructor { + this(null, $imcall, true); +} + +%javamethodmodifiers CVC4::DatatypeConstructor::DatatypeConstructor(std::string) "private"; +%javamethodmodifiers CVC4::DatatypeConstructor::DatatypeConstructor(std::string, unsigned weight) "private"; + +%typemap(javaout) const CVC4::DatatypeConstructorArg& { + return new DatatypeConstructorArg(this.em, $jnicall, false); +} + +%typemap(javabody) CVC4::DatatypeConstructorArg %{ + private long swigCPtr; + protected boolean swigCMemOwn; + private ExprManager em; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + swigCMemOwn = cMemoryOwn; + swigCPtr = cPtr; + this.em = em; } + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javaout) CVC4::SelectorType { + return new SelectorType(this.em, $jnicall, true); +} + +%extend CVC4::Datatype { std::string toString() const { std::stringstream ss; ss << *$self; @@ -95,14 +185,6 @@ } } %extend CVC4::DatatypeConstructor { - CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor, - CVC4::DatatypeConstructorArg> - iterator() - { - return CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor, - CVC4::DatatypeConstructorArg>(*$self); - } - std::string toString() const { std::stringstream ss; ss << *$self; @@ -117,56 +199,28 @@ } } -// Datatype is "iterable" on the Java side -%typemap(javainterfaces) CVC4::Datatype "java.lang.Iterable<DatatypeConstructor>"; -%typemap(javainterfaces) CVC4::DatatypeConstructor "java.lang.Iterable<DatatypeConstructorArg>"; - -// the JavaIteratorAdapter should not be public, and implements Iterator -%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::Datatype, CVC4::DatatypeConstructor> "class"; -%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor, CVC4::DatatypeConstructorArg> "class"; -%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::Datatype, CVC4::DatatypeConstructor> "java.util.Iterator<DatatypeConstructor>"; -%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor, CVC4::DatatypeConstructorArg> "java.util.Iterator<DatatypeConstructorArg>"; -// 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::Datatype, CVC4::DatatypeConstructor> " - public void remove() { - throw new java.lang.UnsupportedOperationException(); - } - - public DatatypeConstructor next() { - if(hasNext()) { - return getNext(); - } else { - throw new java.util.NoSuchElementException(); - } - } -" -%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor, CVC4::DatatypeConstructorArg> " - public void remove() { - throw new java.lang.UnsupportedOperationException(); - } - - public DatatypeConstructorArg 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::Datatype, CVC4::DatatypeConstructor>::getNext() "private"; -%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor, CVC4::DatatypeConstructorArg>::getNext() "private"; - -#endif /* SWIGJAVA */ +// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea +%typemap(javaconstruct) Datatype { + this(null, $imcall, true); +} -%include "expr/datatype.h" +%typemap(javaconstruct) CVC4::Datatype { + this(em, $imcall, true); +} -#ifdef SWIGJAVA +%typemap(javaout) CVC4::DatatypeConstructor { + return new DatatypeConstructor(this.em, $jnicall, true); +} -%include "bindings/java_iterator_adapter.h" -%include "bindings/java_stream_adapters.h" +%typemap(javaout) CVC4::DatatypeConstructorArg { + return new DatatypeConstructorArg(this.em, $jnicall, true); +} +SWIG_JAVA_ITERATOR_ADAPTER(CVC4::Datatype, CVC4::DatatypeConstructor) %template(JavaIteratorAdapter_Datatype) CVC4::JavaIteratorAdapter<CVC4::Datatype, CVC4::DatatypeConstructor>; +SWIG_JAVA_ITERATOR_ADAPTER(CVC4::DatatypeConstructor, CVC4::DatatypeConstructorArg) %template(JavaIteratorAdapter_DatatypeConstructor) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor, CVC4::DatatypeConstructorArg>; #endif /* SWIGJAVA */ + +%include "expr/datatype.h" diff --git a/src/expr/emptyset.i b/src/expr/emptyset.i index ada3dd583..bcd3a0a92 100644 --- a/src/expr/emptyset.i +++ b/src/expr/emptyset.i @@ -2,6 +2,48 @@ #include "expr/emptyset.h" %} +#ifdef SWIGJAVA + +%typemap(javabody) CVC4::EmptySet %{ + private long swigCPtr; + protected boolean swigCMemOwn; + private ExprManager em; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + swigCMemOwn = cMemoryOwn; + swigCPtr = cPtr; + this.em = em; // keep ref to em in SWIG proxy class + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } + + public $javaclassname(ExprManager em, SetType t) { + this(t); + this.em = em; + } +%} + +// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea +%typemap(javaconstruct) EmptySet { + this(null, $imcall, true); +} + +%typemap(javaconstruct) CVC4::EmptySet { + this(null, $imcall, true); +} + +%javamethodmodifiers CVC4::EmptySet::EmptySet(Type t) "private"; + +%typemap(javaout) const CVC4::SetType& { + return new SetType(this.em, $jnicall, false); +} + +#endif + +%ignore CVC4::EmptySet::EmptySet(const CVC4::EmptySet& other); + %rename(equals) CVC4::EmptySet::operator==(const EmptySet&) const; %ignore CVC4::EmptySet::operator!=(const EmptySet&) const; diff --git a/src/expr/expr.i b/src/expr/expr.i index 14228d7c5..7e79d4c1d 100644 --- a/src/expr/expr.i +++ b/src/expr/expr.i @@ -1,102 +1,108 @@ %{ #include "expr/expr.h" +%} -#ifdef SWIGJAVA +%ignore CVC4::Expr::Expr(const Expr&); +// This is currently the only function that would require bindings for +// `std::unordered_map<Expr, Expr, ExprHashFunction>` and is better implemented +// at the Java/Python level if needed. Thus, we ignore it here. +%ignore CVC4::Expr::substitute(const std::unordered_map<Expr, Expr, ExprHashFunction> map) const; +%ignore CVC4::operator<<(std::ostream&, const Expr&); +%ignore CVC4::operator<<(std::ostream&, const TypeCheckingException&); +// Ignore because we would not know which ExprManager the Expr belongs to +%ignore CVC4::TypeCheckingException::getExpression() const; +%ignore CVC4::expr::operator<<(std::ostream&, ExprSetDepth); +%ignore CVC4::expr::operator<<(std::ostream&, ExprPrintTypes); +%ignore CVC4::expr::operator<<(std::ostream&, ExprDag); +%ignore CVC4::expr::operator<<(std::ostream&, ExprSetLanguage); +%ignore CVC4::Expr::operator=(const Expr&); +%ignore CVC4::Expr::operator!=(const Expr&) const; +%ignore CVC4::Expr::operator bool() const;// can just use isNull() -#include "bindings/java_iterator_adapter.h" -#include "bindings/java_stream_adapters.h" +%rename(equals) CVC4::Expr::operator==(const Expr&) const; +%rename(less) CVC4::Expr::operator<(const Expr&) const; +%rename(lessEqual) CVC4::Expr::operator<=(const Expr&) const; +%rename(greater) CVC4::Expr::operator>(const Expr&) const; +%rename(greaterEqual) CVC4::Expr::operator>=(const Expr&) const; -#endif /* SWIGJAVA */ -%} +%rename(getChild) CVC4::Expr::operator[](unsigned i) const; -#ifdef SWIGPYTHON -%rename(doApply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const; -#else /* SWIGPYTHON */ +#ifdef SWIGJAVA + +// For the Java bindings, we implement `getExprManager()` at the Java level +// because we can't map back the C++ point to the Java object +%ignore CVC4::Expr::getExprManager() const; %rename(apply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const; -#endif /* SWIGPYTHON */ -#ifdef SWIGJAVA %typemap(javabody) CVC4::Expr %{ private long swigCPtr; protected boolean swigCMemOwn; + private ExprManager em; - protected $javaclassname(long cPtr, boolean cMemoryOwn) { + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { swigCMemOwn = cMemoryOwn; swigCPtr = cPtr; - this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class + this.em = em; // keep ref to em in SWIG proxy class } protected static long getCPtr($javaclassname obj) { return (obj == null) ? 0 : obj.swigCPtr; } -%} -%javamethodmodifiers CVC4::Expr::operator=(const Expr&) "protected"; -%typemap(javacode) CVC4::Expr %{ - // a ref is kept here to keep Java GC from collecting the ExprManager - // before the Expr - private Object em; - - public Expr assign(Expr e) { - Expr r = assignInternal(e); - this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class - return r; + + public ExprManager getExprManager() throws edu.stanford.CVC4.Exception { + return this.em; + } + + public JavaIteratorAdapter_Expr iterator() { + return new JavaIteratorAdapter_Expr(this.em, this); } %} + +// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea %typemap(javaconstruct) Expr { - this($imcall, true); - this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class - } -%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::Expr { - SmtEngine.dlRef(em); - em = null; - if (swigCPtr != 0) { - if (swigCMemOwn) { - swigCMemOwn = false; - CVC4JNI.delete_Expr(swigCPtr); - } - swigCPtr = 0; - } - } -#endif /* SWIGJAVA */ + this(null, $imcall, true); +} -%ignore CVC4::operator<<(std::ostream&, const Expr&); -%ignore CVC4::operator<<(std::ostream&, const TypeCheckingException&); +%typemap(javaconstruct) CVC4::Expr { + this(null, $imcall, true); +} -%ignore CVC4::expr::operator<<(std::ostream&, ExprSetDepth); -%ignore CVC4::expr::operator<<(std::ostream&, ExprPrintTypes); -%ignore CVC4::expr::operator<<(std::ostream&, ExprDag); -%ignore CVC4::expr::operator<<(std::ostream&, ExprSetLanguage); +%typemap(javaout) CVC4::Expr { + return new Expr(this.em, $jnicall, true); +} -%rename(assignInternal) CVC4::Expr::operator=(const Expr&); -%rename(equals) CVC4::Expr::operator==(const Expr&) const; -%ignore CVC4::Expr::operator!=(const Expr&) const; -%rename(less) CVC4::Expr::operator<(const Expr&) const; -%rename(lessEqual) CVC4::Expr::operator<=(const Expr&) const; -%rename(greater) CVC4::Expr::operator>(const Expr&) const; -%rename(greaterEqual) CVC4::Expr::operator>=(const Expr&) const; +SWIG_STD_VECTOR_EM(CVC4::Expr, const CVC4::Expr&) +SWIG_STD_VECTOR_EM(std::vector<CVC4::Expr>, const std::vector<CVC4::Expr>&) -%rename(getChild) CVC4::Expr::operator[](unsigned i) const; -%ignore CVC4::Expr::operator bool() const;// can just use isNull() +%template(vectorExpr) std::vector<CVC4::Expr>; +%typemap(javaout) std::vector<CVC4::Expr> { + return new vectorExpr(this.em, $jnicall, true); +} +%typemap(javaout) const std::vector<CVC4::Expr>& { + return new vectorExpr(this.em, $jnicall, false); +} +%template(vectorVectorExpr) std::vector<std::vector<CVC4::Expr>>; -namespace CVC4 { - namespace expr { - %ignore exportInternal; - }/* CVC4::expr namespace */ -}/* CVC4 namespace */ +%javamethodmodifiers CVC4::Expr::operator=(const Expr&) "protected"; -#ifdef SWIGJAVA +%typemap(javaout) const CVC4::AscriptionType& { + return new AscriptionType(this.em, $jnicall, $owner); +} + +%typemap(javaout) const CVC4::EmptySet& { + return new EmptySet(this.em, $jnicall, $owner); +} + +%typemap(javaout) const CVC4::ExprSequence& { + return new ExprSequence(this.em, $jnicall, $owner); +} // 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, CVC4::Expr> iterator() - { - return CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr>(*$self); - } -} +%ignore CVC4::Expr::const_iterator; // Expr is "iterable" on the Java side %typemap(javainterfaces) CVC4::Expr "java.lang.Iterable<edu.stanford.CVC4.Expr>"; @@ -123,6 +129,10 @@ namespace CVC4 { #endif /* SWIGJAVA */ +#ifdef SWIGPYTHON +%rename(doApply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const; +#endif /* SWIGPYTHON */ + %include "expr/expr.h" #ifdef SWIGPYTHON @@ -156,11 +166,7 @@ namespace CVC4 { #ifdef SWIGJAVA -%include "bindings/java_iterator_adapter.h" -%include "bindings/java_stream_adapters.h" - +SWIG_JAVA_ITERATOR_ADAPTER(CVC4::Expr, CVC4::Expr) %template(JavaIteratorAdapter_Expr) CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr>; #endif /* SWIGJAVA */ - -%include "expr/expr.h" diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i index 5a5e7a9d4..d8ed7f6a6 100644 --- a/src/expr/expr_manager.i +++ b/src/expr/expr_manager.i @@ -2,29 +2,105 @@ #include "expr/expr_manager.h" %} -%typemap(javacode) CVC4::ExprManager %{ - // a ref is kept here to keep Java GC from collecting the Options - // before the ExprManager - private Object options; -%} -%typemap(javaconstruct) ExprManager { - this($imcall, true); - this.options = SmtEngine.mkRef(options); // keep ref to options in SWIG proxy class - } -%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::ExprManager { - SmtEngine.dlRef(options); - options = null; - if (swigCPtr != 0) { - if (swigCMemOwn) { - swigCMemOwn = false; - CVC4JNI.delete_ExprManager(swigCPtr); - } - swigCPtr = 0; - } - } - +%ignore CVC4::ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap); %ignore CVC4::stats::getStatisticsRegistry(ExprManager*); %ignore CVC4::ExprManager::getResourceManager(); +%ignore CVC4::ExprManager::mkRecordType(const Record& rec); +%ignore CVC4::ExprManager::safeFlushStatistics(int fd) const; + +#ifdef SWIGJAVA + +%typemap(javaout) CVC4::Expr { + return new Expr(this, $jnicall, true); +} + +%typemap(javaout) CVC4::Type { + return new Type(this, $jnicall, true); +} + +%typemap(javaout) CVC4::ArrayType { + return new ArrayType(this, $jnicall, true); +} + +%typemap(javaout) CVC4::BitVectorType { + return new BitVectorType(this, $jnicall, true); +} + +%typemap(javaout) CVC4::BooleanType { + return new BooleanType(this, $jnicall, true); +} + +%typemap(javaout) CVC4::ConstructorType { + return new ConstructorType(this, $jnicall, true); +} + +%typemap(javaout) const CVC4::Datatype& { + return new Datatype(this, $jnicall, false); +} + +%typemap(javaout) CVC4::DatatypeType { + return new DatatypeType(this, $jnicall, true); +} + +%typemap(javaout) std::vector<CVC4::DatatypeType> { + return new vectorDatatypeType(this, $jnicall, true); +} + +%typemap(javaout) CVC4::FloatingPointType { + return new FloatingPointType(this, $jnicall, true); +} + +%typemap(javaout) CVC4::FunctionType { + return new FunctionType(this, $jnicall, true); +} + +%typemap(javaout) CVC4::SelectorType { + return new SelectorType(this, $jnicall, true); +} + +%typemap(javaout) CVC4::StringType { + return new StringType(this, $jnicall, true); +} + +%typemap(javaout) CVC4::RegExpType { + return new RegExpType(this, $jnicall, true); +} + +%typemap(javaout) CVC4::RealType { + return new RealType(this, $jnicall, true); +} + +%typemap(javaout) CVC4::SetType { + return new SetType(this, $jnicall, true); +} + +%typemap(javaout) CVC4::SExprType { + return new SExprType(this, $jnicall, true); +} + +%typemap(javaout) CVC4::SortType { + return new SortType(this, $jnicall, true); +} + +%typemap(javaout) CVC4::SortConstructorType { + return new SortConstructorType(this, $jnicall, true); +} + +%typemap(javaout) CVC4::TesterType { + return new TesterType(this, $jnicall, true); +} + +%typemap(javaout) CVC4::IntegerType { + return new IntegerType(this, $jnicall, true); +} + +%typemap(javaout) CVC4::RoundingModeType { + return new RoundingModeType(this, $jnicall, true); +} + +%javamethodmodifiers CVC4::ExprManager::exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap) "public"; + +#endif /* SWIGJAVA */ %include "expr/expr_manager.h" @@ -53,7 +129,6 @@ %template(mkConst) CVC4::ExprManager::mkConst<CVC4::kind::Kind_t>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::DatatypeIndexConstant>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleUpdate>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordUpdate>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::Rational>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVector>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::EmptySet>; @@ -74,5 +149,3 @@ %template(mkConst) CVC4::ExprManager::mkConst<bool>; %template(mkConst) CVC4::ExprManager::mkConst<CVC4::RoundingMode>; #endif - -%include "expr/expr_manager.h" diff --git a/src/expr/expr_sequence.i b/src/expr/expr_sequence.i index 42e130466..294937024 100644 --- a/src/expr/expr_sequence.i +++ b/src/expr/expr_sequence.i @@ -2,6 +2,42 @@ #include "expr/expr_sequence.h" %} +#ifdef SWIGJAVA + +%typemap(javabody) CVC4::ExprSequence %{ + private long swigCPtr; + protected boolean swigCMemOwn; + private ExprManager em; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + swigCMemOwn = cMemoryOwn; + swigCPtr = cPtr; + this.em = em; // keep ref to em in SWIG proxy class + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } + + public $javaclassname(ExprManager em, Type type, vectorExpr seq) { + this(type, seq); + this.em = em; + } +%} + +// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea +%typemap(javaconstruct) ExprSequence { + this(null, $imcall, true); +} + +%typemap(javaconstruct) CVC4::ExprSequence { + this(null, $imcall, true); +} + +%javamethodmodifiers CVC4::ExprSequence::ExprSequence(Type type, vectorExpr seq) "private"; + +#endif + %rename(equals) CVC4::ExprSequence::operator==(const ExprSequence&) const; %ignore CVC4::ExprSequence::operator!=(const ExprSequence&) const; %ignore CVC4::ExprSequence::getSequence() const; diff --git a/src/expr/record.i b/src/expr/record.i deleted file mode 100644 index dce785ea3..000000000 --- a/src/expr/record.i +++ /dev/null @@ -1,55 +0,0 @@ -%{ -#include "expr/record.h" - -#ifdef SWIGJAVA - -#include "bindings/java_iterator_adapter.h" -#include "bindings/java_stream_adapters.h" - -#endif /* SWIGJAVA */ -%} - -%include "stdint.i" - -%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; - -%rename(apply) CVC4::RecordHashFunction::operator()(const Record&) const; -%rename(apply) CVC4::RecordUpdateHashFunction::operator()(const RecordUpdate&) const; - -%ignore CVC4::operator<<(std::ostream&, const Record&); -%ignore CVC4::operator<<(std::ostream&, const RecordUpdate&); - -#ifdef SWIGJAVA - -// 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/stanford/CVC4/Type"); - jmethodID methodid = jenv->GetMethodID(clazz, "<init>", "(JZ)V"); - jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast<uintptr_t>(new CVC4::Type($1.second)), true)); - }; - - - -#endif /* SWIGJAVA */ - -%include "expr/record.h" - -#ifdef SWIGJAVA - -%include "bindings/java_iterator_adapter.h" -%include "bindings/java_stream_adapters.h" - - -#endif /* SWIGJAVA */ diff --git a/src/expr/type.i b/src/expr/type.i index 16d059eac..8262c4cea 100644 --- a/src/expr/type.i +++ b/src/expr/type.i @@ -2,6 +2,77 @@ #include "expr/type.h" %} +%ignore CVC4::expr::exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* nm, ExprManagerMapCollection& vmap); + +%ignore CVC4::Type::Type(const Type&); +%ignore CVC4::Type::operator=(const Type&); +%ignore CVC4::Type::operator!=(const Type&) const; +%rename(equals) CVC4::Type::operator==(const Type&) const; +%rename(less) CVC4::Type::operator<(const Type&) const; +%rename(lessEqual) CVC4::Type::operator<=(const Type&) const; +%rename(greater) CVC4::Type::operator>(const Type&) const; +%rename(greaterEqual) CVC4::Type::operator>=(const Type&) const; + +%ignore CVC4::BitVectorType::BitVectorType(); +%ignore CVC4::BitVectorType::BitVectorType(const Type&); + +%ignore CVC4::BooleanType::BooleanType(); +%ignore CVC4::BooleanType::BooleanType(const Type&); + +%ignore CVC4::ConstructorType::ConstructorType(); +%ignore CVC4::ConstructorType::ConstructorType(const Type&); + +%ignore CVC4::FloatingPointType::FloatingPointType(); +%ignore CVC4::FloatingPointType::FloatingPointType(const Type&); + +%ignore CVC4::DatatypeType::DatatypeType(); +%ignore CVC4::DatatypeType::DatatypeType(const Type&); +%ignore CVC4::DatatypeType::getRecord() const; + +%ignore CVC4::FunctionType::FunctionType(); +%ignore CVC4::FunctionType::FunctionType(const Type&); + +%ignore CVC4::IntegerType::IntegerType(); +%ignore CVC4::IntegerType::IntegerType(const Type&); + +%ignore CVC4::RealType::RealType(); +%ignore CVC4::RealType::RealType(const Type&); + +%ignore CVC4::RegExpType::RegExpType(); +%ignore CVC4::RegExpType::RegExpType(const Type&); + +%ignore CVC4::RoundingModeType::RoundingModeType(); +%ignore CVC4::RoundingModeType::RoundingModeType(const Type&); + +%ignore CVC4::SelectorType::SelectorType(); +%ignore CVC4::SelectorType::SelectorType(const Type&); + +%ignore CVC4::SequenceType::SequenceType(); +%ignore CVC4::SequenceType::SequenceType(const Type&); + +%ignore CVC4::SExprType::SExprType(); +%ignore CVC4::SExprType::SExprType(const Type&); + +%ignore CVC4::SortType::SortType(); +%ignore CVC4::SortType::SortType(const Type&); + +%ignore CVC4::SortConstructorType::SortConstructorType(); +%ignore CVC4::SortConstructorType::SortConstructorType(const Type&); + +%ignore CVC4::StringType::StringType(); +%ignore CVC4::StringType::StringType(const Type&); + +%ignore CVC4::TesterType::TesterType(); +%ignore CVC4::TesterType::TesterType(const Type&); + +%ignore CVC4::ArrayType::ArrayType(); +%ignore CVC4::ArrayType::ArrayType(const Type&); + +%ignore CVC4::SetType::SetType(); +%ignore CVC4::SetType::SetType(const Type&); + +%ignore CVC4::operator<<(std::ostream&, const Type&); + #ifdef SWIGPYTHON %rename(doApply) CVC4::TypeHashFunction::operator()(const CVC4::Type&) const; #else /* SWIGPYTHON */ @@ -9,62 +80,358 @@ #endif /* SWIGPYTHON */ #ifdef SWIGJAVA + +%include "bindings/java/cvc4_std_vector.i" + +%typemap(javaout) CVC4::Expr { + return new Expr(this.em, $jnicall, true); +} + +%typemap(javaout) std::vector<CVC4::Type> { + return new vectorType(this.em, $jnicall, true); +} + %typemap(javabody) CVC4::Type %{ private long swigCPtr; protected boolean swigCMemOwn; + // Prevent ExprManager from being garbage collected before this instance + protected ExprManager em; - protected $javaclassname(long cPtr, boolean cMemoryOwn) { + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { swigCMemOwn = cMemoryOwn; swigCPtr = cPtr; - this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class + this.em = em; } protected static long getCPtr($javaclassname obj) { return (obj == null) ? 0 : obj.swigCPtr; } %} -%javamethodmodifiers CVC4::Type::operator=(const Type&) "protected"; -%typemap(javacode) CVC4::Type %{ - // a ref is kept here to keep Java GC from collecting the ExprManager - // before the Type - private Object em; - public Type assign(Type t) { - Type r = assignInternal(t); - this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class - return r; +// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea +%typemap(javaconstruct) Type { + this(null, $imcall, true); +} + +%typemap(javaconstruct) CVC4::Type { + this(null, $imcall, true); +} + + +%typemap(javaout) CVC4::Type { + return new Type(this.em, $jnicall, true); +} + +SWIG_STD_VECTOR_EM(CVC4::Type, const CVC4::Type&) + +%typemap(javaout) CVC4::Type { + return new Type(this.em, $jnicall, true); +} +%typemap(javaout) const CVC4::Type& { + return new Type(this.em, $jnicall, false); +} +%template(vectorType) std::vector<CVC4::Type>; + +%typemap(javabody_derived) CVC4::BitVectorType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCPtr = cPtr; + swigCMemOwn = cMemoryOwn; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; } %} -%typemap(javaconstruct) Type { - this($imcall, true); - this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class - } -%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::Type { - SmtEngine.dlRef(em); - em = null; - if (swigCPtr != 0) { - if (swigCMemOwn) { - swigCMemOwn = false; - CVC4JNI.delete_Type(swigCPtr); - } - swigCPtr = 0; - } + +%typemap(javabody_derived) CVC4::BooleanType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCPtr = cPtr; + swigCMemOwn = cMemoryOwn; } -#endif /* SWIGJAVA */ -%ignore CVC4::operator<<(std::ostream&, const Type&); -%rename(assignInternal) CVC4::Type::operator=(const Type&); -%rename(equals) CVC4::Type::operator==(const Type&) const; -%ignore CVC4::Type::operator!=(const Type&) const; -%rename(less) CVC4::Type::operator<(const Type&) const; -%rename(lessEqual) CVC4::Type::operator<=(const Type&) const; -%rename(greater) CVC4::Type::operator>(const Type&) const; -%rename(greaterEqual) CVC4::Type::operator>=(const Type&) const; + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javabody_derived) CVC4::ConstructorType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCPtr = cPtr; + swigCMemOwn = cMemoryOwn; + } -namespace CVC4 { - namespace expr { - %ignore exportTypeInternal; - }/* CVC4::expr namespace */ -}/* CVC4 namespace */ + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javabody_derived) CVC4::FloatingPointType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCPtr = cPtr; + swigCMemOwn = cMemoryOwn; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javabody_derived) CVC4::DatatypeType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCPtr = cPtr; + swigCMemOwn = cMemoryOwn; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +SWIG_STD_VECTOR_EM(CVC4::DatatypeType, const CVC4::DatatypeType&) + +%typemap(javaout) CVC4::DatatypeType { + return new DatatypeType(this.em, $jnicall, true); +} +%typemap(javaout) const CVC4::DatatypeType& { + return new DatatypeType(this.em, $jnicall, false); +} +%template(vectorDatatypeType) std::vector<CVC4::DatatypeType>; + +%typemap(javabody_derived) CVC4::FunctionType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCPtr = cPtr; + swigCMemOwn = cMemoryOwn; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javabody_derived) CVC4::IntegerType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCPtr = cPtr; + swigCMemOwn = cMemoryOwn; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javabody_derived) CVC4::RealType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCPtr = cPtr; + swigCMemOwn = cMemoryOwn; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javabody_derived) CVC4::RegExpType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCPtr = cPtr; + swigCMemOwn = cMemoryOwn; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javabody_derived) CVC4::RoundingModeType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCPtr = cPtr; + swigCMemOwn = cMemoryOwn; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javabody_derived) CVC4::SelectorType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCPtr = cPtr; + swigCMemOwn = cMemoryOwn; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javabody_derived) CVC4::SequenceType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCPtr = cPtr; + swigCMemOwn = cMemoryOwn; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javabody_derived) CVC4::SExprType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCPtr = cPtr; + swigCMemOwn = cMemoryOwn; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javabody_derived) CVC4::SortType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCPtr = cPtr; + swigCMemOwn = cMemoryOwn; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javabody_derived) CVC4::SortConstructorType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCPtr = cPtr; + swigCMemOwn = cMemoryOwn; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javabody_derived) CVC4::StringType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCPtr = cPtr; + swigCMemOwn = cMemoryOwn; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javabody_derived) CVC4::TesterType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCPtr = cPtr; + swigCMemOwn = cMemoryOwn; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javabody_derived) CVC4::ArrayType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCPtr = cPtr; + swigCMemOwn = cMemoryOwn; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javabody_derived) CVC4::SetType %{ + private transient long swigCPtr; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + super(em, CVC4JNI.$javaclassname_SWIGUpcast(cPtr), cMemoryOwn); + swigCMemOwn = cMemoryOwn; + swigCPtr = cPtr; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +%typemap(javaout) CVC4::SetType { + return new SetType(this.em, $jnicall, true); +} + +%typemap(javaout) CVC4::BooleanType { + return new BooleanType(this.em, $jnicall, true); +} + +%typemap(javaout) const CVC4::Datatype& { + return new Datatype(this.em, $jnicall, true); +} + +%typemap(javaout) CVC4::DatatypeType { + return new DatatypeType(this.em, $jnicall, true); +} + +%typemap(javaout) CVC4::SortType { + return new SortType(this.em, $jnicall, true); +} + +%typemap(javaout) typeVector { + return new typeVector(this.em, $jnicall, true); +} + +#endif /* SWIGJAVA */ %include "expr/type.h" diff --git a/src/expr/variable_type_map.i b/src/expr/variable_type_map.i index 95c705c1e..17ca6a110 100644 --- a/src/expr/variable_type_map.i +++ b/src/expr/variable_type_map.i @@ -2,6 +2,50 @@ #include "expr/variable_type_map.h" %} +#if SWIGJAVA + +%typemap(javabody) CVC4::VariableTypeMap %{ + private long swigCPtr; + protected boolean swigCMemOwn; + private ExprManager em; + + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + swigCMemOwn = cMemoryOwn; + swigCPtr = cPtr; + this.em = em; + } + + public VariableTypeMap(ExprManager em) { + this(); + this.em = em; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } +%} + +// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea +%typemap(javaconstruct) VariableTypeMap { + this(null, $imcall, true); +} + +%typemap(javaconstruct) CVC4::VariableTypeMap { + this(null, $imcall, true); +} + +%typemap(javaout) CVC4::Expr& { + return new Expr(this.em, $jnicall, false); +} + +%typemap(javaout) CVC4::Type& { + return new Type(this.em, $jnicall, false); +} + +%javamethodmodifiers CVC4::VariableTypeMap::VariableTypeMap() "private"; + +#endif /* SWIGJAVA */ + %rename(get) CVC4::VariableTypeMap::operator[](Expr); %rename(get) CVC4::VariableTypeMap::operator[](Type); diff --git a/src/options/options.i b/src/options/options.i index ba98c4fc4..319b4addb 100644 --- a/src/options/options.i +++ b/src/options/options.i @@ -2,6 +2,21 @@ #include "options/options.h" %} +%ignore CVC4::Options::registerAndNotify(ListenerCollection& collection, Listener* listener, bool notify); +%ignore CVC4::Options::registerBeforeSearchListener(Listener* listener); +%ignore CVC4::Options::registerTlimitListener(Listener* listener, bool notifyIfSet); +%ignore CVC4::Options::registerTlimitPerListener(Listener* listener, bool notifyIfSet); +%ignore CVC4::Options::registerRlimitListener(Listener* listener, bool notifyIfSet); +%ignore CVC4::Options::registerRlimitPerListener(Listener* listener, bool notifyIfSet); +%ignore CVC4::Options::registerSetDefaultExprDepthListener(Listener* listener, bool notifyIfSet); +%ignore CVC4::Options::registerSetDefaultExprDagListener(Listener* listener, bool notifyIfSet); +%ignore CVC4::Options::registerSetPrintExprTypesListener(Listener* listener, bool notifyIfSet); +%ignore CVC4::Options::registerSetDumpModeListener(Listener* listener, bool notifyIfSet); +%ignore CVC4::Options::registerSetPrintSuccessListener(Listener* listener, bool notifyIfSet); +%ignore CVC4::Options::registerDumpToFileNameListener(Listener* listener, bool notifyIfSet); +%ignore CVC4::Options::registerSetRegularOutputChannelListener(Listener* listener, bool notifyIfSet); +%ignore CVC4::Options::registerSetDiagnosticOutputChannelListener(Listener* listener, bool notifyIfSet); + %apply char** STRING_ARRAY { char* argv[] } %include "options/options.h" %clear char* argv[]; diff --git a/src/proof/unsat_core.i b/src/proof/unsat_core.i index c37c8551d..780a75996 100644 --- a/src/proof/unsat_core.i +++ b/src/proof/unsat_core.i @@ -1,17 +1,37 @@ %{ #include "proof/unsat_core.h" +%} + +%ignore CVC4::operator<<(std::ostream&, const UnsatCore&); #ifdef SWIGJAVA -#include "bindings/java_iterator_adapter.h" -#include "bindings/java_stream_adapters.h" +%typemap(javabody) CVC4::UnsatCore %{ + private long swigCPtr; + protected boolean swigCMemOwn; + private ExprManager em; -#endif /* SWIGJAVA */ + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + swigCMemOwn = cMemoryOwn; + swigCPtr = cPtr; + this.em = em; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } + + public JavaIteratorAdapter_UnsatCore iterator() { + return new JavaIteratorAdapter_UnsatCore(this.em, this); + } %} -%ignore CVC4::operator<<(std::ostream&, const UnsatCore&); +%typemap(javaout) CVC4::Expr { + return new Expr(this.em, $jnicall, true); +} -#ifdef SWIGJAVA +%ignore CVC4::UnsatCore::UnsatCore(); +%ignore CVC4::UnsatCore::UnsatCore(SmtEngine* smt, std::vector<Expr> core); // Instead of UnsatCore::begin() and end(), create an // iterator() method on the Java side that returns a Java-style @@ -20,12 +40,8 @@ %ignore CVC4::UnsatCore::end(); %ignore CVC4::UnsatCore::begin() const; %ignore CVC4::UnsatCore::end() const; -%extend CVC4::UnsatCore { - CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr> iterator() - { - return CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr>(*$self); - } +%extend CVC4::UnsatCore { std::string toString() { std::stringstream ss; @@ -37,36 +53,13 @@ // UnsatCore is "iterable" on the Java side %typemap(javainterfaces) CVC4::UnsatCore "java.lang.Iterable<edu.stanford.CVC4.Expr>"; -// the JavaIteratorAdapter should not be public, and implements Iterator -%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr> "class"; -%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr> "java.util.Iterator<edu.stanford.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::UnsatCore, CVC4::Expr> " - public void remove() { - throw new java.lang.UnsupportedOperationException(); - } - - public edu.stanford.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::UnsatCore, CVC4::Expr>::getNext() "private"; - #endif /* SWIGJAVA */ %include "proof/unsat_core.h" #ifdef SWIGJAVA -%include <std_vector.i> - -%include "bindings/java_iterator_adapter.h" - +SWIG_JAVA_ITERATOR_ADAPTER(CVC4::UnsatCore, CVC4::Expr) %template(JavaIteratorAdapter_UnsatCore) CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr>; #endif /* SWIGJAVA */ diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i index 635e593bb..95a5f4f3b 100644 --- a/src/smt/smt_engine.i +++ b/src/smt/smt_engine.i @@ -3,51 +3,33 @@ %} #ifdef SWIGJAVA + %typemap(javacode) CVC4::SmtEngine %{ // a ref is kept here to keep Java GC from collecting the EM // before the SmtEngine - private Object emRef; - static final native Object mkRef(Object obj); - static final native void dlRef(Object obj); + private ExprManager em; %} -%native (mkRef) jobject SmtEngine::mkRef(jobject); -%native (dlRef) void SmtEngine::dlRef(jobject); -%{ -extern "C" { -SWIGEXPORT jobject JNICALL Java_edu_stanford_CVC4_SmtEngine_mkRef(JNIEnv* jenv, jclass jcls, jobject o) { - if(o == NULL) { - return NULL; - } - return jenv->NewGlobalRef(o); + +%typemap(javaconstruct) SmtEngine { + this($imcall, true); + this.em = em; // keep ref to expr manager in SWIG proxy class } -SWIGEXPORT void JNICALL Java_edu_stanford_CVC4_SmtEngine_dlRef(JNIEnv* jenv, jclass jcls, jobject o) { - if(o != NULL) { - jenv->DeleteGlobalRef(o); - } + +%typemap(javaout) CVC4::Expr { + return new Expr(this.em, $jnicall, true); } + +%typemap(javaout) CVC4::UnsatCore { + return new UnsatCore(this.em, $jnicall, true); } -%} -%typemap(javaconstruct) SmtEngine { - this($imcall, true); - emRef = mkRef(em); // keep ref to expr manager in SWIG proxy class - } -%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::SmtEngine { - dlRef(emRef); - emRef = null; - if (swigCPtr != 0) { - if (swigCMemOwn) { - swigCMemOwn = false; - CVC4JNI.delete_SmtEngine(swigCPtr); - } - swigCPtr = 0; - } - } - -%template(Map_ExprExpr) std::map<CVC4::Expr, CVC4::Expr>; + +// %template(Map_ExprExpr) std::map<CVC4::Expr, CVC4::Expr>; +%ignore CVC4::SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map); #endif // SWIGJAVA %ignore CVC4::SmtEngine::setLogic(const char*); +%ignore CVC4::SmtEngine::setReplayStream(ExprStream* exprStream); %ignore CVC4::smt::currentProofManager(); %include "smt/smt_engine.h" diff --git a/src/util/proof.i b/src/util/proof.i index 22dff1043..59a524a0f 100644 --- a/src/util/proof.i +++ b/src/util/proof.i @@ -2,4 +2,6 @@ #include "util/proof.h" %} +%ignore CVC4::Proof::toStream(std::ostream& out, const ProofLetMap& map) const; + %include "util/proof.h" diff --git a/src/util/statistics.i b/src/util/statistics.i index 8d1086dcc..7dfc7ec39 100644 --- a/src/util/statistics.i +++ b/src/util/statistics.i @@ -64,12 +64,12 @@ %include <std_pair.i> %include <std_string.i> -%include <std_vector.i> -%include "bindings/java_iterator_adapter.h" %include "util/sexpr.h" %template(Statistic) std::pair<std::string, CVC4::SExpr>; + +%feature("valuewrapper") CVC4::JavaIteratorAdapter<CVC4::StatisticsBase, std::pair<std::string, CVC4::SExpr> >; %template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase, std::pair<std::string, CVC4::SExpr> >; #endif /* SWIGJAVA */ diff --git a/test/java/BitVectorsAndArrays.java b/test/java/BitVectorsAndArrays.java index dc78f89c2..c60c49696 100644 --- a/test/java/BitVectorsAndArrays.java +++ b/test/java/BitVectorsAndArrays.java @@ -76,7 +76,7 @@ public class BitVectorsAndArrays { Expr old_current = em.mkExpr(Kind.SELECT, current_array, index); Expr two = em.mkConst(new BitVector(32, 2)); - vectorExpr assertions = new vectorExpr(); + vectorExpr assertions = new vectorExpr(em); for (int i = 1; i < k; ++i) { index = em.mkConst( new BitVector(index_size, new edu.stanford.CVC4.Integer(i))); diff --git a/test/java/CMakeLists.txt b/test/java/CMakeLists.txt index 169013b84..213c6ab8e 100644 --- a/test/java/CMakeLists.txt +++ b/test/java/CMakeLists.txt @@ -7,6 +7,7 @@ set(java_test_src_files BitVectorsAndArrays.java Combination.java HelloWorld.java + Issue2846.java LinearArith.java ) diff --git a/test/java/Issue2846.java b/test/java/Issue2846.java new file mode 100644 index 000000000..b41258c29 --- /dev/null +++ b/test/java/Issue2846.java @@ -0,0 +1,64 @@ +/********************* */ +/*! \file BitVectorsAndArrays.java + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Test case for issue #2846 + ** + ** This test case tests whether the dependency information for keeping the + ** ExprManager alive is maintained correctly. + **/ + +import edu.stanford.CVC4.*; +import org.junit.Test; + +public class Issue2846 { + static { + System.loadLibrary("cvc4jni"); + } + + @Test + public void test() throws InterruptedException { + testInternal(); + gc("h"); + } + + private static void testInternal() throws InterruptedException { + ExprManager em = new ExprManager(); + SmtEngine smt = new SmtEngine(em); + smt.setOption("produce-models", new SExpr(true)); + Expr x = em.mkVar("x", em.integerType()); + Expr y = em.mkVar("y", em.integerType()); + Expr z = em.mkVar("z", em.integerType()); + gc("a"); + Expr a1 = em.mkExpr(Kind.GT, x, em.mkExpr(Kind.PLUS, y, z)); + gc("b"); + smt.assertFormula(a1); + gc("c"); + Expr a2 = em.mkExpr(Kind.LT, y, z); + gc("d"); + smt.assertFormula(a2); + gc("e"); + System.out.println(a1); + System.out.println(a2); + gc("f"); + Result res = smt.checkSat(); + gc("g"); + System.out.println("Res = " + res); + System.out.println("x = " + smt.getValue(x)); + System.out.println("y = " + smt.getValue(y)); + System.out.println("z = " + smt.getValue(z)); + } + + private static void gc(String msg) throws InterruptedException { + System.out.println("calling gc " + msg); + Thread.sleep(100); + System.gc(); + } +} |