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.");
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);
// 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:");
// (declare-sort Person 0)
Type personType = manager.mkSort("Person", 0);
- vectorType vector1 = new vectorType();
+ vectorType vector1 = new vectorType(manager);
vector1.add(personType);
// (Tuple Person)
// (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)
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
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 =
${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
${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
${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
${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
${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
--- /dev/null
+/**
+ * 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
"value_type must be convertible from T::const_iterator::value_type");
}
+ JavaIteratorAdapter() = delete;
+
bool hasNext() { return d_it != d_t.end(); }
value_type getNext()
--- /dev/null
+%{
+#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
%}
#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
#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
//
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
JCALL3(ReleaseByteArrayElements, jenv, ba, bae, 0);
}
+%include "bindings/java_stream_adapters.h"
+
#endif /* SWIGJAVA */
// TIM:
%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:
// 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"
%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"
#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"
#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;
%{
#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;
}
}
%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;
}
}
-// 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"
#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;
%{
#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>";
#endif /* SWIGJAVA */
+#ifdef SWIGPYTHON
+%rename(doApply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const;
+#endif /* SWIGPYTHON */
+
%include "expr/expr.h"
#ifdef SWIGPYTHON
#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"
#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"
%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>;
%template(mkConst) CVC4::ExprManager::mkConst<bool>;
%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RoundingMode>;
#endif
-
-%include "expr/expr_manager.h"
#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;
+++ /dev/null
-%{
-#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 */
#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 */
#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"
#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);
#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[];
%{
#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
%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;
// 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 */
%}
#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"
#include "util/proof.h"
%}
+%ignore CVC4::Proof::toStream(std::ostream& out, const ProofLetMap& map) const;
+
%include "util/proof.h"
%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 */
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)));
BitVectorsAndArrays.java
Combination.java
HelloWorld.java
+ Issue2846.java
LinearArith.java
)
--- /dev/null
+/********************* */
+/*! \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();
+ }
+}
projects / cvc5.git / commitdiff