diff options
Diffstat (limited to 'src/bindings/java')
-rw-r--r-- | src/bindings/java/CMakeLists.txt | 14 | ||||
-rw-r--r-- | src/bindings/java/cvc4_std_vector.i | 206 |
2 files changed, 206 insertions, 14 deletions
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 |