diff options
54 files changed, 24 insertions, 2969 deletions
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 35154828f..da97a2cd2 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -16,7 +16,7 @@ jobs: include: - name: production - config: production --language-bindings=java --lfsc --python-bindings + config: production --all-bindings --lfsc cache-key: production python-bindings: true check-examples: true diff --git a/CMakeLists.txt b/CMakeLists.txt index 1b6027b46..688a7c1ea 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -165,12 +165,9 @@ set(SYMFPU_DIR "" CACHE STRING "Set SymFPU install directory") # Prepend binaries with prefix on make install set(PROGRAM_PREFIX "" CACHE STRING "Program prefix on make install") -# Supported SWIG language bindings -option(BUILD_SWIG_BINDINGS_JAVA "Build Java bindings with SWIG") -option(BUILD_SWIG_BINDINGS_PYTHON "Build Python bindings with SWIG") - # Supprted language bindings based on new C++ API option(BUILD_BINDINGS_PYTHON "Build Python bindings based on new C++ API ") +option(BUILD_BINDINGS_JAVA "Build Java bindings based on new C++ API ") #-----------------------------------------------------------------------------# # Internal cmake variables @@ -542,14 +539,15 @@ add_subdirectory(doc) add_subdirectory(src) add_subdirectory(test) -if(BUILD_SWIG_BINDINGS_JAVA OR BUILD_SWIG_BINDINGS_PYTHON) - add_subdirectory(src/bindings) -endif() - if(BUILD_BINDINGS_PYTHON) add_subdirectory(src/api/python) endif() +if(BUILD_BINDINGS_JAVA) + message(FATAL_ERROR + "Java bindings for the new API are not implemented yet.") +endif() + #-----------------------------------------------------------------------------# # Package configuration # @@ -624,9 +622,8 @@ print_config("Valgrind :" ENABLE_VALGRIND) message("") print_config("Shared libs :" ENABLE_SHARED) print_config("Static binary :" ENABLE_STATIC_BINARY) -print_config("Java SWIG bindings :" BUILD_SWIG_BINDINGS_JAVA) -print_config("Python SWIG bindings :" BUILD_SWIG_BINDINGS_PYTHON) print_config("Python bindings :" BUILD_BINDINGS_PYTHON) +print_config("Java bindings :" BUILD_BINDINGS_JAVA) print_config("Python2 :" USE_PYTHON2) print_config("Python3 :" USE_PYTHON3) message("") diff --git a/INSTALL.md b/INSTALL.md index bf3a20ed2..ae22e2d71 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -129,11 +129,6 @@ dependency. with --check-proofs. It can be installed using the `contrib/get-lfsc` script. Configure CVC4 with `configure.sh --lfsc` to build with this dependency. -### SWIG >= 3.0.x (Simplified Wrapper and Interface Generator) - -SWIG 3.0.x (and a JDK) is necessary to build the Java API. -See [Language Bindings](#language-bindings) below for build instructions. - ### CLN >= v1.3 (Class Library for Numbers) [CLN](http://www.ginac.de/CLN) @@ -202,17 +197,13 @@ See [Testing CVC4](#Testing-CVC4) below for more details. ## Language bindings -CVC4 provides a complete and flexible C++ API (see `examples/api` for examples). -It further provides Java (see `examples/SimpleVC.java` and `examples/api/java`) -and Python (see `examples/SimpleVC.py`) API bindings. +CVC4 provides a complete and flexible C++ API (see `examples/api` for +examples). It further provides Java (see `examples/SimpleVC.java` and +`examples/api/java`) and Python (see `examples/api/python`) API bindings. -Configure CVC4 with `configure.sh --language-bindings=[java,python,all]` -to build with language bindings. -Note that this requires SWIG >= 3.0.x. +Configure CVC4 with `configure.sh --<lang>-bindings` to build with language +bindings for `<lang>`. -In principle, since we use SWIG to generate the native Java and PythonAPI, -we could support other languages as well. However, using CVC4 from other -languages is not supported, nor expected to work, at this time. If you're interested in helping to develop, maintain, and test a language binding, please contact one of the project leaders. @@ -328,4 +319,3 @@ available on the system. Override with `ARGS=-jN`. Use `-jN` for parallel **building** with `N` threads. - @@ -13,6 +13,7 @@ Improvements: Changes: * SyGuS: Removed support for SyGuS-IF 1.0. +* Removed Java and Python bindings for the legacy API Changes since 1.7 ================= diff --git a/configure.sh b/configure.sh index 21a444082..988b7a392 100755 --- a/configure.sh +++ b/configure.sh @@ -46,15 +46,12 @@ The following flags enable optional features (disable with --no-<option name>). --python2 prefer using Python 2 (also for Python bindings) --python3 prefer using Python 3 (also for Python bindings) --python-bindings build Python bindings based on new C++ API + --java-bindings build Java bindings based on new C++ API + --all-bindings build bindings for all supported languages --asan build with ASan instrumentation --ubsan build with UBSan instrumentation --tsan build with TSan instrumentation -The following options configure parameterized features. - - --language-bindings[=java,python,all] - specify language bindings to build - Optional Packages: The following flags enable optional packages (disable with --no-<option name>). --cln use CLN instead of GMP @@ -135,6 +132,7 @@ proofs=default python2=default python3=default python_bindings=default +java_bindings=default readline=default shared=default static_binary=default @@ -147,9 +145,6 @@ unit_testing=default valgrind=default win64=default -language_bindings_java=default -language_bindings_python=default - abc_dir=default antlr_dir=default cadical_dir=default @@ -282,6 +277,11 @@ do --python-bindings) python_bindings=ON;; --no-python-bindings) python_bindings=OFF;; + --java-bindings) java_bindings=ON;; + --no-java-bindings) java_bindings=OFF;; + + --all-bindings) python_bindings=ON;; + --valgrind) valgrind=ON;; --no-valgrind) valgrind=OFF;; @@ -291,23 +291,6 @@ do --readline) readline=ON;; --no-readline) readline=OFF;; - --language-bindings) die "missing argument to $1 (try -h)" ;; - --language-bindings=*) - lang="${1##*=}" - IFS=',' - for l in $lang; do - case $l in - java) language_bindings_java=ON ;; - python) language_bindings_python=ON ;; - all) - language_bindings_python=ON - language_bindings_java=ON ;; - *) die "invalid language binding '$l' specified (try -h)" ;; - esac - done - unset IFS - ;; - --abc-dir) die "missing argument to $1 (try -h)" ;; --abc-dir=*) abc_dir=${1##*=} ;; @@ -410,6 +393,8 @@ cmake_opts="" && cmake_opts="$cmake_opts -DUSE_PYTHON3=$python3" [ $python_bindings != default ] \ && cmake_opts="$cmake_opts -DBUILD_BINDINGS_PYTHON=$python_bindings" +[ $java_bindings != default ] \ + && cmake_opts="$cmake_opts -DBUILD_BINDINGS_JAVA=$java_bindings" [ $valgrind != default ] \ && cmake_opts="$cmake_opts -DENABLE_VALGRIND=$valgrind" [ $profiling != default ] \ @@ -434,12 +419,6 @@ cmake_opts="" && cmake_opts="$cmake_opts -DUSE_LFSC=$lfsc" [ $symfpu != default ] \ && cmake_opts="$cmake_opts -DUSE_SYMFPU=$symfpu" - -[ $language_bindings_java != default ] \ - && cmake_opts="$cmake_opts -DBUILD_SWIG_BINDINGS_JAVA=$language_bindings_java" -[ $language_bindings_python != default ] \ - && cmake_opts="$cmake_opts -DBUILD_SWIG_BINDINGS_PYTHON=$language_bindings_python" - [ "$abc_dir" != default ] \ && cmake_opts="$cmake_opts -DABC_DIR=$abc_dir" [ "$antlr_dir" != default ] \ diff --git a/src/base/configuration.i b/src/base/configuration.i deleted file mode 100644 index 3b92e2438..000000000 --- a/src/base/configuration.i +++ /dev/null @@ -1,7 +0,0 @@ -%{ -#include "base/configuration.h" -%} - -%apply char **STRING_ARRAY { char const* const* } -%include "base/configuration.h" -%clear char const* const*; diff --git a/src/base/exception.i b/src/base/exception.i deleted file mode 100644 index 5098dbc6e..000000000 --- a/src/base/exception.i +++ /dev/null @@ -1,15 +0,0 @@ -%{ -#include "base/exception.h" -%} - -%ignore CVC4::operator<<(std::ostream&, const Exception&); -%ignore CVC4::Exception::Exception(const char*); -%typemap(javabase) CVC4::Exception "java.lang.RuntimeException"; - -// Make sure that the CVC4.Exception class of the Python API inherits from -// BaseException and can be caught -%exceptionclass CVC4::Exception; - -%rename(CVC4IllegalArgumentException) CVC4::IllegalArgumentException; - -%include "base/exception.h" diff --git a/src/base/modal_exception.i b/src/base/modal_exception.i deleted file mode 100644 index 7df4c8f83..000000000 --- a/src/base/modal_exception.i +++ /dev/null @@ -1,7 +0,0 @@ -%{ -#include "base/modal_exception.h" -%} - -%ignore CVC4::ModalException::ModalException(const char*); - -%include "base/modal_exception.h" diff --git a/src/bindings/CMakeLists.txt b/src/bindings/CMakeLists.txt deleted file mode 100644 index ac2fadd95..000000000 --- a/src/bindings/CMakeLists.txt +++ /dev/null @@ -1,35 +0,0 @@ -if(NOT ENABLE_SHARED) - message(FATAL_ERROR "Can't build language bindings for static CVC4 build.") -endif() - -find_package(SWIG 3.0.0 REQUIRED) -if(POLICY CMP0078) - cmake_policy(SET CMP0078 OLD) -endif() -if(POLICY CMP0086) - cmake_policy(SET CMP0086 OLD) -endif() - -if(USE_PYTHON3 AND (SWIG_VERSION VERSION_EQUAL 3.0.8)) - message(FATAL_ERROR - "\nSWIG ${SWIG_VERSION} is not supported for python3 bindings because of the following bug: https://github.com/swig/swig/issues/588 -Please downgrade to 3.0.0-3.0.7 or upgrade.") -endif() - -include(${SWIG_USE_FILE}) - -set(CVC4_SWIG_INTERFACE ${PROJECT_SOURCE_DIR}/src/cvc4.i) - -set_property(SOURCE ${CVC4_SWIG_INTERFACE} PROPERTY CPLUSPLUS ON) - -include_directories( - ${PROJECT_SOURCE_DIR}/src - ${PROJECT_SOURCE_DIR}/src/include - ${CMAKE_BINARY_DIR}/src) - -if(BUILD_SWIG_BINDINGS_JAVA) - add_subdirectory(java) -endif() -if(BUILD_SWIG_BINDINGS_PYTHON) - add_subdirectory(python) -endif() diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt deleted file mode 100644 index 8159b8ee0..000000000 --- a/src/bindings/java/CMakeLists.txt +++ /dev/null @@ -1,196 +0,0 @@ -find_package(Java REQUIRED) -find_package(JNI REQUIRED) -include(UseJava) - -include_directories(${JNI_INCLUDE_DIRS}) - -set(SWIG_MODULE_cvc4jni_EXTRA_DEPS cvc4 cvc4parser) -set_property(SOURCE ${CVC4_SWIG_INTERFACE} PROPERTY CPLUSPLUS ON) -set(CMAKE_SWIG_FLAGS -package edu.stanford.CVC4) - -if(${CMAKE_VERSION} VERSION_LESS "3.8.0") - swig_add_module(cvc4jni Java ${CVC4_SWIG_INTERFACE}) -else() - swig_add_library(cvc4jni LANGUAGE Java SOURCES ${CVC4_SWIG_INTERFACE}) -endif() -swig_link_libraries(cvc4jni cvc4 cvc4parser ${JNI_LIBRARIRES}) - -# Create CVC4.jar from all generated *.java files. -set(gen_java_files - ${CMAKE_CURRENT_BINARY_DIR}/ArrayStoreAll.java - ${CMAKE_CURRENT_BINARY_DIR}/ArrayStoreAllHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/ArrayType.java - ${CMAKE_CURRENT_BINARY_DIR}/AscriptionType.java - ${CMAKE_CURRENT_BINARY_DIR}/AscriptionTypeHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/BitVector.java - ${CMAKE_CURRENT_BINARY_DIR}/BitVectorBitOf.java - ${CMAKE_CURRENT_BINARY_DIR}/BitVectorBitOfHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/BitVectorExtract.java - ${CMAKE_CURRENT_BINARY_DIR}/BitVectorExtractHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/BitVectorHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/BitVectorRepeat.java - ${CMAKE_CURRENT_BINARY_DIR}/BitVectorRotateLeft.java - ${CMAKE_CURRENT_BINARY_DIR}/BitVectorRotateRight.java - ${CMAKE_CURRENT_BINARY_DIR}/BitVectorSignExtend.java - ${CMAKE_CURRENT_BINARY_DIR}/BitVectorSize.java - ${CMAKE_CURRENT_BINARY_DIR}/BitVectorType.java - ${CMAKE_CURRENT_BINARY_DIR}/BitVectorZeroExtend.java - ${CMAKE_CURRENT_BINARY_DIR}/BoolHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/BooleanType.java - ${CMAKE_CURRENT_BINARY_DIR}/CVC4.java - ${CMAKE_CURRENT_BINARY_DIR}/CVC4IllegalArgumentException.java - ${CMAKE_CURRENT_BINARY_DIR}/CVC4JNI.java - ${CMAKE_CURRENT_BINARY_DIR}/CVC4String.java - ${CMAKE_CURRENT_BINARY_DIR}/CVC4StringHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/Cardinality.java - ${CMAKE_CURRENT_BINARY_DIR}/CardinalityBeth.java - ${CMAKE_CURRENT_BINARY_DIR}/CardinalityUnknown.java - ${CMAKE_CURRENT_BINARY_DIR}/Configuration.java - ${CMAKE_CURRENT_BINARY_DIR}/ConstructorType.java - ${CMAKE_CURRENT_BINARY_DIR}/Datatype.java - ${CMAKE_CURRENT_BINARY_DIR}/DatatypeConstructor.java - ${CMAKE_CURRENT_BINARY_DIR}/DatatypeConstructorArg.java - ${CMAKE_CURRENT_BINARY_DIR}/DatatypeHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/DatatypeIndexConstant.java - ${CMAKE_CURRENT_BINARY_DIR}/DatatypeIndexConstantHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/DatatypeResolutionException.java - ${CMAKE_CURRENT_BINARY_DIR}/DatatypeSelfType.java - ${CMAKE_CURRENT_BINARY_DIR}/DatatypeType.java - ${CMAKE_CURRENT_BINARY_DIR}/DatatypeUnresolvedType.java - ${CMAKE_CURRENT_BINARY_DIR}/EmptySet.java - ${CMAKE_CURRENT_BINARY_DIR}/EmptySetHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/Exception.java - ${CMAKE_CURRENT_BINARY_DIR}/ExportUnsupportedException.java - ${CMAKE_CURRENT_BINARY_DIR}/Expr.java - ${CMAKE_CURRENT_BINARY_DIR}/ExprHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/ExprManager.java - ${CMAKE_CURRENT_BINARY_DIR}/ExprManagerMapCollection.java - ${CMAKE_CURRENT_BINARY_DIR}/ExprSequence.java - ${CMAKE_CURRENT_BINARY_DIR}/FloatingPoint.java - ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointConvertSort.java - ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointSize.java - ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToBV.java - ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToFPFloatingPoint.java - ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToFPGeneric.java - ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToFPIEEEBitVector.java - ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToFPReal.java - ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToFPSignedBitVector.java - ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToFPUnsignedBitVector.java - ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToSBV.java - ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointToUBV.java - ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointType.java - ${CMAKE_CURRENT_BINARY_DIR}/FunctionType.java - ${CMAKE_CURRENT_BINARY_DIR}/InputLanguage.java - ${CMAKE_CURRENT_BINARY_DIR}/IntAnd.java - ${CMAKE_CURRENT_BINARY_DIR}/IntToBitVector.java - ${CMAKE_CURRENT_BINARY_DIR}/Integer.java - ${CMAKE_CURRENT_BINARY_DIR}/IntegerHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/IntegerType.java - ${CMAKE_CURRENT_BINARY_DIR}/JavaInputStreamAdapter.java - ${CMAKE_CURRENT_BINARY_DIR}/JavaIteratorAdapter_Datatype.java - ${CMAKE_CURRENT_BINARY_DIR}/JavaIteratorAdapter_DatatypeConstructor.java - ${CMAKE_CURRENT_BINARY_DIR}/JavaIteratorAdapter_Expr.java - ${CMAKE_CURRENT_BINARY_DIR}/JavaIteratorAdapter_StatisticsBase.java - ${CMAKE_CURRENT_BINARY_DIR}/JavaIteratorAdapter_UnsatCore.java - ${CMAKE_CURRENT_BINARY_DIR}/JavaOutputStreamAdapter.java - ${CMAKE_CURRENT_BINARY_DIR}/Kind.java - ${CMAKE_CURRENT_BINARY_DIR}/KindHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/LastExceptionBuffer.java - ${CMAKE_CURRENT_BINARY_DIR}/LogicException.java - ${CMAKE_CURRENT_BINARY_DIR}/LogicInfo.java - ${CMAKE_CURRENT_BINARY_DIR}/ModalException.java - ${CMAKE_CURRENT_BINARY_DIR}/OptionException.java - ${CMAKE_CURRENT_BINARY_DIR}/Options.java - ${CMAKE_CURRENT_BINARY_DIR}/OutputLanguage.java - ${CMAKE_CURRENT_BINARY_DIR}/PrettySExprs.java - ${CMAKE_CURRENT_BINARY_DIR}/Proof.java - ${CMAKE_CURRENT_BINARY_DIR}/Rational.java - ${CMAKE_CURRENT_BINARY_DIR}/RationalHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/RealType.java - ${CMAKE_CURRENT_BINARY_DIR}/RecoverableModalException.java - ${CMAKE_CURRENT_BINARY_DIR}/RegExpLoop.java - ${CMAKE_CURRENT_BINARY_DIR}/RegExpRepeat.java - ${CMAKE_CURRENT_BINARY_DIR}/RegExpType.java - ${CMAKE_CURRENT_BINARY_DIR}/Result.java - ${CMAKE_CURRENT_BINARY_DIR}/RoundingMode.java - ${CMAKE_CURRENT_BINARY_DIR}/RoundingModeType.java - ${CMAKE_CURRENT_BINARY_DIR}/SExpr.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__options__InstFormatMode.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__vectorT_CVC4__DatatypeConstructorArg_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}/SequenceType.java - ${CMAKE_CURRENT_BINARY_DIR}/SetType.java - ${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.java - ${CMAKE_CURRENT_BINARY_DIR}/SortConstructorType.java - ${CMAKE_CURRENT_BINARY_DIR}/SortType.java - ${CMAKE_CURRENT_BINARY_DIR}/Statistic.java - ${CMAKE_CURRENT_BINARY_DIR}/Statistics.java - ${CMAKE_CURRENT_BINARY_DIR}/StatisticsBase.java - ${CMAKE_CURRENT_BINARY_DIR}/StringType.java - ${CMAKE_CURRENT_BINARY_DIR}/TesterType.java - ${CMAKE_CURRENT_BINARY_DIR}/TheoryId.java - ${CMAKE_CURRENT_BINARY_DIR}/TupleUpdate.java - ${CMAKE_CURRENT_BINARY_DIR}/TupleUpdateHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/Type.java - ${CMAKE_CURRENT_BINARY_DIR}/TypeCheckingException.java - ${CMAKE_CURRENT_BINARY_DIR}/TypeConstant.java - ${CMAKE_CURRENT_BINARY_DIR}/TypeConstantHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/TypeHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/UninterpretedConstant.java - ${CMAKE_CURRENT_BINARY_DIR}/UninterpretedConstantHashFunction.java - ${CMAKE_CURRENT_BINARY_DIR}/UnrecognizedOptionException.java - ${CMAKE_CURRENT_BINARY_DIR}/UnsafeInterruptException.java - ${CMAKE_CURRENT_BINARY_DIR}/UnsatCore.java - ${CMAKE_CURRENT_BINARY_DIR}/VariableTypeMap.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}/vectorSExpr.java - ${CMAKE_CURRENT_BINARY_DIR}/vectorString.java - ${CMAKE_CURRENT_BINARY_DIR}/vectorType.java - ${CMAKE_CURRENT_BINARY_DIR}/vectorUnsignedInt.java - ${CMAKE_CURRENT_BINARY_DIR}/vectorVectorExpr.java -) - -if(CVC4_USE_CLN_IMP) - list(APPEND gen_java_files - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_cln__cl_I.java - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_cln__cl_RA.java - ) -elseif(CVC4_USE_GMP_IMP) - list(APPEND gen_java_files - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpq_class.java - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpz_class.java - ) -endif() - -set(CMAKE_JNI_TARGET TRUE) -add_jar(cvc4jar - SOURCES ${gen_java_files} - VERSION ${CVC4_MAJOR}.${CVC4_MINOR}.${CVC4_RELEASE} - OUTPUT_NAME CVC4) -add_dependencies(cvc4jar cvc4jni) -install_jar(cvc4jar DESTINATION share/java/cvc4) -install_jni_symlink(cvc4jar DESTINATION share/java/cvc4) -install(TARGETS cvc4jni - EXPORT cvc4-targets - DESTINATION ${LIBRARY_INSTALL_DIR}) - -install_jar_exports( - TARGETS cvc4jar - NAMESPACE CVC4:: - FILE CVC4JavaTargets.cmake - DESTINATION ${LIBRARY_INSTALL_DIR}/cmake/CVC4 -) diff --git a/src/bindings/java/cvc4_std_vector.i b/src/bindings/java/cvc4_std_vector.i deleted file mode 100644 index e032426a0..000000000 --- a/src/bindings/java/cvc4_std_vector.i +++ /dev/null @@ -1,206 +0,0 @@ -/** - * 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 deleted file mode 100644 index 864619004..000000000 --- a/src/bindings/java_iterator_adapter.h +++ /dev/null @@ -1,67 +0,0 @@ -/********************* */ -/*! \file java_iterator_adapter.h - ** \verbatim - ** Top contributors (to current version): - ** Andres Noetzli, Morgan Deters, Mathias Preiner - ** 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 An iterator adapter for the Java bindings, giving Java iterators - ** the ability to access elements from STL iterators. - ** - ** An iterator adapter for the Java bindings, giving Java iterators the - ** ability to access elements from STL iterators. This class is mapped - ** into Java by SWIG, where it implements Iterator (some additional - ** Java-side functions are added by the SWIG layer to implement the full - ** interface). - ** - ** The functionality requires significant assistance from the ".i" SWIG - ** interface files, applying a variety of typemaps. - **/ - -// private to the bindings layer -#ifndef SWIGJAVA -# error This should only be included from the Java bindings layer. -#endif /* SWIGJAVA */ - -#ifndef CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H -#define CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H - -#include <type_traits> - -namespace CVC4 { - -template <class T, class value_type> -class JavaIteratorAdapter -{ - public: - JavaIteratorAdapter(const T& t) : d_t(t), d_it(d_t.begin()) - { - static_assert( - std::is_convertible<typename T::const_iterator::value_type, - value_type>(), - "value_type must be convertible from T::const_iterator::value_type"); - } - - JavaIteratorAdapter() = delete; - - bool hasNext() { return d_it != d_t.end(); } - - value_type getNext() - { - value_type ret = *d_it; - ++d_it; - return ret; - } - - private: - const T& d_t; - typename T::const_iterator d_it; -}; /* class JavaIteratorAdapter<T, value_type> */ - -} // namespace CVC4 - -#endif /* CVC4__BINDINGS__JAVA_ITERATOR_ADAPTER_H */ diff --git a/src/bindings/java_iterator_adapter.i b/src/bindings/java_iterator_adapter.i deleted file mode 100644 index 5f814edd7..000000000 --- a/src/bindings/java_iterator_adapter.i +++ /dev/null @@ -1,75 +0,0 @@ -%{ -#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/bindings/java_stream_adapters.h b/src/bindings/java_stream_adapters.h deleted file mode 100644 index 2f3c8093f..000000000 --- a/src/bindings/java_stream_adapters.h +++ /dev/null @@ -1,108 +0,0 @@ -/********************* */ -/*! \file java_stream_adapters.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Mathias Preiner - ** 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 An OutputStream adapter for the Java bindings - ** - ** An OutputStream adapter for the Java bindings. This works with a lot - ** of help from SWIG, and custom typemaps in the ".i" SWIG interface files - ** for CVC4. The basic idea is that, when a CVC4 function with a - ** std::ostream& parameter is called, a Java-side binding is generated - ** taking a java.io.OutputStream. Now, the problem is that std::ostream - ** has no Java equivalent, and java.io.OutputStream has no C++ equivalent, - ** so we use this class (which exists on both sides) as the go-between. - ** The wrapper connecting the Java function (taking an OutputStream) and - ** the C++ function (taking an ostream) creates a JavaOutputStreamAdapter, - ** and call the C++ function with the stringstream inside. After the call, - ** the generated stream material is collected and output to the Java-side - ** OutputStream. - **/ - -// private to the bindings layer -#ifndef SWIGJAVA -# error This should only be included from the Java bindings layer. -#endif /* SWIGJAVA */ - -#include <sstream> -#include <set> -#include <cassert> -#include <iosfwd> -#include <string> -#include <jni.h> - -#ifndef CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H -#define CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H - -namespace CVC4 { - -class JavaOutputStreamAdapter : public std::ostringstream { -public: - std::string toString() { return str(); } -};/* class JavaOutputStreamAdapter */ - -class JavaInputStreamAdapter : public std::stringstream { - static std::set<JavaInputStreamAdapter*> s_adapters; - jobject inputStream; - - JavaInputStreamAdapter& operator=(const JavaInputStreamAdapter&); - JavaInputStreamAdapter(const JavaInputStreamAdapter&); - -public: - JavaInputStreamAdapter(jobject inputStream) : inputStream(inputStream) { - s_adapters.insert(this); - } - - ~JavaInputStreamAdapter() { - s_adapters.erase(this); - } - - static void pullAdapters(JNIEnv* jenv) { - for(std::set<JavaInputStreamAdapter*>::iterator i = s_adapters.begin(); - i != s_adapters.end(); - ++i) { - (*i)->pull(jenv); - } - } - - jobject getInputStream() const { - return inputStream; - } - - void pull(JNIEnv* jenv) { - if(fail() || eof()) { - clear(); - } - jclass clazz = jenv->FindClass("java/io/InputStream"); - assert(clazz != NULL && jenv->ExceptionOccurred() == NULL); - jmethodID method = jenv->GetMethodID(clazz, "available", "()I"); - assert(method != NULL && jenv->ExceptionOccurred() == NULL); - jint available = jenv->CallIntMethod(inputStream, method); - assert(jenv->ExceptionOccurred() == NULL); - jbyteArray bytes = jenv->NewByteArray(available); - assert(bytes != NULL && jenv->ExceptionOccurred() == NULL); - method = jenv->GetMethodID(clazz, "read", "([B)I"); - assert(method != NULL && jenv->ExceptionOccurred() == NULL); - jint nread = jenv->CallIntMethod(inputStream, method, bytes); - assert(jenv->ExceptionOccurred() == NULL); - jbyte* bptr = jenv->GetByteArrayElements(bytes, NULL); - assert(jenv->ExceptionOccurred() == NULL); - std::copy(bptr, bptr + nread, std::ostream_iterator<char>(*this)); - *this << std::flush; - jenv->ReleaseByteArrayElements(bytes, bptr, 0); - assert(jenv->ExceptionOccurred() == NULL); - assert(good()); - assert(!eof()); - } - -};/* class JavaInputStreamAdapter */ - -}/* CVC4 namespace */ - -#endif /* CVC4__BINDINGS__JAVA_STREAM_ADAPTERS_H */ diff --git a/src/bindings/python/CMakeLists.txt b/src/bindings/python/CMakeLists.txt deleted file mode 100644 index d03924680..000000000 --- a/src/bindings/python/CMakeLists.txt +++ /dev/null @@ -1,43 +0,0 @@ -# Make sure that interpreter and libraries have a compatible version. -# Note: We use the Python interpreter to determine the install path for Python -# modules. If the interpreter and library have different versions, the module -# will be installed for the wrong Python version. Hence, we require the library -# version to match the Python interpreter's version. -find_package(PythonLibs - ${PYTHON_VERSION_MAJOR}.${PYTHON_VERSION_MINOR} REQUIRED) -include_directories(${PYTHON_INCLUDE_DIRS}) - -set(SWIG_MODULE_CVC4_EXTRA_DEPS cvc4 cvc4parser) -set_property(SOURCE ${CVC4_SWIG_INTERFACE} PROPERTY CPLUSPLUS ON) - -# Suppress -Wsuggest-override warnings for generated code -set_property( - SOURCE ${CMAKE_CURRENT_BINARY_DIR}/cvc4PYTHON_wrap.cxx - PROPERTY COMPILE_OPTIONS -Wno-suggest-override) - -# The generated module should have the name _CVC4.so, hence we use CVC4 as -# target name. -if(${CMAKE_VERSION} VERSION_LESS "3.8.0") - swig_add_module(CVC4 Python ${CVC4_SWIG_INTERFACE}) -else() - swig_add_library(CVC4 LANGUAGE Python SOURCES ${CVC4_SWIG_INTERFACE}) -endif() -swig_link_libraries(CVC4 cvc4 cvc4parser ${PYTHON_LIBRARIES}) - - -# Install Python bindings to the corresponding python-*/site-packages -# directory. Lookup Python module directory and store path in -# PYTHON_MODULE_PATH. -execute_process(COMMAND - ${PYTHON_EXECUTABLE} -c - "from distutils.sysconfig import get_python_lib;\ - print(get_python_lib(plat_specific=True,\ - prefix='${CMAKE_INSTALL_PREFIX}'))" - OUTPUT_VARIABLE PYTHON_MODULE_PATH - OUTPUT_STRIP_TRAILING_WHITESPACE) - -# Copy _CVC4.so and CVC4.py to PYTHON_MODULE_PATH -install(TARGETS ${SWIG_MODULE_CVC4_REAL_NAME} - DESTINATION ${PYTHON_MODULE_PATH}) -install(FILES ${CMAKE_CURRENT_BINARY_DIR}/CVC4.py - DESTINATION ${PYTHON_MODULE_PATH}) diff --git a/src/bindings/swig.h b/src/bindings/swig.h deleted file mode 100644 index ed401ad18..000000000 --- a/src/bindings/swig.h +++ /dev/null @@ -1,33 +0,0 @@ -/********************* */ -/*! \file swig.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Mathias Preiner, 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 Common swig checks and definitions - ** - ** Common swig checks and definitions, when generating swig interfaces. - **/ - -#ifndef CVC4__BINDINGS__SWIG_H -#define CVC4__BINDINGS__SWIG_H - -#ifndef SWIG -# error This file should only be included when generating swig interfaces. -#endif /* SWIG */ - -#if !defined(SWIG_VERSION) || SWIG_VERSION < 0x030000 -# error CVC4 bindings require swig version 3.0.0 or later, sorry. -#endif /* SWIG_VERSION */ - -%import "cvc4_public.h" - -// swig doesn't like GCC attributes -#define __attribute__(x) - -#endif /* CVC4__BINDINGS__SWIG_H */ diff --git a/src/cvc4.i b/src/cvc4.i deleted file mode 100644 index 9fc8ed60e..000000000 --- a/src/cvc4.i +++ /dev/null @@ -1,255 +0,0 @@ -// Declare that all functions in the interface can throw exceptions of type -// CVC4::Exception and exceptions in general. SWIG catches those exceptions and -// turns them into target language exceptions via "throws" typemaps. -%catches(CVC4::Exception,...); - -%import "bindings/swig.h" - -%include "stdint.i" -%include "stl.i" - -%module CVC4 -// nspace completely broken with Java packaging -//%nspace; - -namespace std { - class istream; - class ostream; - template <class T> class set {}; - template <class K, class V, class H> class unordered_map {}; -} - -%{ -namespace CVC4 {} -using namespace CVC4; - -#include <cassert> -#include <unordered_map> -#include <iosfwd> -#include <set> -#include <string> -#include <typeinfo> -#include <vector> - -#include "base/exception.h" -#include "base/modal_exception.h" -#include "expr/datatype.h" -#include "expr/expr.h" -#include "expr/type.h" -#include "options/option_exception.h" -#include "smt/command.h" -#include "util/bitvector.h" -#include "util/floatingpoint.h" -#include "util/iand.h" -#include "util/integer.h" -#include "util/sexpr.h" -#include "util/unsafe_interrupt_exception.h" - -#ifdef SWIGJAVA -#include "bindings/java_stream_adapters.h" -std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters; -#endif -%} - -#ifdef SWIGPYTHON -%pythonappend CVC4::SmtEngine::SmtEngine %{ - self.thisown = 0 -%} -%pythonappend CVC4::ExprManager::ExprManager %{ - self.thisown = 0 -%} -#endif /* SWIGPYTHON */ - -%template(vectorUnsignedInt) std::vector< unsigned int >; -%template(vectorSExpr) std::vector< CVC4::SExpr >; -%template(vectorString) std::vector< std::string >; -%template(setOfType) std::set< CVC4::Type >; - -// 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 -// helper functions won't compile properly. -#undef NULL - -#ifdef SWIGJAVA - -// Map C++ exceptions of type CVC4::Exception to Java exceptions of type -// edu.stanford.CVC4.Exception -// -// As suggested in: -// http://www.swig.org/Doc3.0/SWIGDocumentation.html#Java_exception_typemap -%typemap(throws, throws="edu.stanford.CVC4.Exception") CVC4::Exception { - jclass excep = jenv->FindClass("edu/stanford/CVC4/Exception"); - if (excep) - jenv->ThrowNew(excep, $1.what()); - 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 -%include "java/various.i" // map char** to java.lang.String[] - -// Functions on the C++ side taking std::ostream& should on the Java side -// take a java.io.OutputStream. A JavaOutputStreamAdapter is created in -// the wrapper which creates and passes on a std::stringstream to the C++ -// function. Then on exit, the string from the stringstream is dumped to -// the Java-side OutputStream. -%typemap(jni) std::ostream& "jlong" -%typemap(jtype) std::ostream& "long" -%typemap(jstype) std::ostream& "java.io.OutputStream" -%typemap(javain, - pre=" edu.stanford.CVC4.JavaOutputStreamAdapter temp$javainput = new edu.stanford.CVC4.JavaOutputStreamAdapter();", pgcppname="temp$javainput", - post=" new java.io.PrintStream($javainput).print(temp$javainput.toString());") - std::ostream& "edu.stanford.CVC4.JavaOutputStreamAdapter.getCPtr(temp$javainput)" - -%typemap(jni) std::istream& "jlong" -%typemap(jtype) std::istream& "long" -%typemap(jstype) std::istream& "java.io.InputStream" -%typemap(javain, - pre=" edu.stanford.CVC4.JavaInputStreamAdapter temp$javainput = edu.stanford.CVC4.JavaInputStreamAdapter.get($javainput);", pgcppname="temp$javainput", - post="") - std::istream& "edu.stanford.CVC4.JavaInputStreamAdapter.getCPtr(temp$javainput)" -%typemap(in) jobject inputStream %{ - $1 = jenv->NewGlobalRef($input); -%} -%typemap(out) CVC4::JavaInputStreamAdapter* %{ - $1->pull(jenv); - *(CVC4::JavaInputStreamAdapter **)&$result = $1; -%} -%typemap(javacode) CVC4::JavaInputStreamAdapter %{ - private static java.util.HashMap<java.io.InputStream, JavaInputStreamAdapter> streams = - new java.util.HashMap<java.io.InputStream, JavaInputStreamAdapter>(); - public static JavaInputStreamAdapter get(java.io.InputStream is) { - if(streams.containsKey(is)) { - return (JavaInputStreamAdapter) streams.get(is); - } - JavaInputStreamAdapter adapter = new JavaInputStreamAdapter(is); - streams.put(is, adapter); - return adapter; - } -%} -%typemap(javafinalize) CVC4::JavaInputStreamAdapter %{ - protected void finalize() { - streams.remove(getInputStream()); - delete(); - } -%} -%ignore CVC4::JavaInputStreamAdapter::init(JNIEnv*); -%ignore CVC4::JavaInputStreamAdapter::pullAdapters(JNIEnv*); -%ignore CVC4::JavaInputStreamAdapter::pull(JNIEnv*); -%javamethodmodifiers CVC4::JavaInputStreamAdapter::getInputStream() const "private"; -%javamethodmodifiers CVC4::JavaInputStreamAdapter::JavaInputStreamAdapter(jobject) "private"; - -%exception CVC4::JavaInputStreamAdapter::~JavaInputStreamAdapter() %{ - try { - jenv->DeleteGlobalRef(arg1->getInputStream()); - $action - } catch(CVC4::Exception& e) { - std::stringstream ss; - ss << e.what() << ": " << e.getMessage(); - std::string explanation = ss.str(); - SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, explanation.c_str()); - } -%} - -/* Copied (and modified) from java.swg; the standard swig version causes - * negative BigInteger to be interpreted unsigned. Here we throw an - * exception. */ -%typemap(in) unsigned long long { - jclass clazz; - jmethodID mid; - jbyteArray ba; - jbyte* bae; - jsize sz; - int i; - - if (!$input) { - SWIG_JavaThrowException(jenv, SWIG_JavaNullPointerException, "BigInteger null"); - return $null; - } - clazz = JCALL1(GetObjectClass, jenv, $input); - mid = JCALL3(GetMethodID, jenv, clazz, "toByteArray", "()[B"); - ba = (jbyteArray)JCALL2(CallObjectMethod, jenv, $input, mid); - bae = JCALL2(GetByteArrayElements, jenv, ba, 0); - sz = JCALL1(GetArrayLength, jenv, ba); - if((bae[0] & 0x80) != 0) { - SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, "BigInteger argument must be nonnegative."); - } - jsize test_sz = sz; - if(sz > 1 && bae[0] == 0) { - --test_sz; - } - if(test_sz > sizeof(unsigned long long)) { - SWIG_JavaThrowException(jenv, SWIG_JavaRuntimeException, "BigInteger argument out of bounds."); - } - $1 = 0; - for(i=0; i<sz; i++) { - $1 = ($1 << 8) | ($1_type)(unsigned char)bae[i]; - } - JCALL3(ReleaseByteArrayElements, jenv, ba, bae, 0); -} - -%include "bindings/java_stream_adapters.h" - -#endif /* SWIGJAVA */ - -// TIM: -// At the moment, the header includes seem to need to follow a special order. -// I don't know why. I am following the build order -%include "base/configuration.i" -%include "base/exception.i" -%include "base/modal_exception.i" - -%include "options/language.i" - -// Tim: "util/integer.i" must come before util/{rational.i,bitvector.i}. -%include "util/integer.i" -%include "util/rational.i" -%include "util/bitvector.i" -%include "util/iand.i" -%include "util/floatingpoint.i" - -// Tim: The remainder of util/. -%include "util/bool.i" -%include "util/cardinality.i" -%include "util/hash.i" -%include "util/proof.i" -%include "util/regexp.i" -%include "util/result.i" -%include "util/sexpr.i" -%include "util/statistics.i" -%include "util/string.i" -%include "util/tuple.i" -%include "util/unsafe_interrupt_exception.i" - -%include "expr/uninterpreted_constant.i" -%include "expr/array_store_all.i" -%include "expr/ascription_type.i" -%include "expr/emptyset.i" -%include "expr/expr_sequence.i" -%include "proof/unsat_core.i" - -// TIM: -// Have these before the rest of expr/. -// Again, no clue why. -%include "expr/array.i" -%include "expr/kind.i" -%include "expr/type.i" - -// 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 "options/option_exception.i" -%include "options/options.i" -%include "smt/logic_exception.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" diff --git a/src/expr/array.i b/src/expr/array.i deleted file mode 100644 index 4acd7bf0c..000000000 --- a/src/expr/array.i +++ /dev/null @@ -1,5 +0,0 @@ -%{ -#include "expr/array.h" -%} - -%include "expr/array.h" diff --git a/src/expr/array_store_all.i b/src/expr/array_store_all.i deleted file mode 100644 index 5158a21d9..000000000 --- a/src/expr/array_store_all.i +++ /dev/null @@ -1,65 +0,0 @@ -%{ -#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/array_store_all.h" diff --git a/src/expr/ascription_type.i b/src/expr/ascription_type.i deleted file mode 100644 index c2499c00e..000000000 --- a/src/expr/ascription_type.i +++ /dev/null @@ -1,48 +0,0 @@ -%{ -#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; - -%rename(apply) CVC4::AscriptionTypeHashFunction::operator()(const AscriptionType&) const; - -%ignore CVC4::operator<<(std::ostream&, AscriptionType); - -%include "expr/ascription_type.h" diff --git a/src/expr/datatype.i b/src/expr/datatype.i deleted file mode 100644 index 56dd6dad4..000000000 --- a/src/expr/datatype.i +++ /dev/null @@ -1,226 +0,0 @@ -%{ -#include "expr/datatype.h" -%} - -%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; - -%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; - -#ifdef SWIGJAVA - -%typemap(javaout) CVC4::Expr { - return new Expr(this.em, $jnicall, true); -} - -%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&) - -%extend CVC4::Datatype { -%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; - return ss.str(); - } -} -%extend CVC4::DatatypeConstructor { - std::string toString() const { - std::stringstream ss; - ss << *$self; - return ss.str(); - } -} -%extend CVC4::DatatypeConstructorArg { - std::string toString() const { - std::stringstream ss; - ss << *$self; - return ss.str(); - } -} - -// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea -%typemap(javaconstruct) Datatype { - this(null, $imcall, true); -} - -%typemap(javaconstruct) CVC4::Datatype { - this(em, $imcall, true); -} - -%typemap(javaout) CVC4::DatatypeConstructor { - return new DatatypeConstructor(this.em, $jnicall, true); -} - -%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 deleted file mode 100644 index bcd3a0a92..000000000 --- a/src/expr/emptyset.i +++ /dev/null @@ -1,59 +0,0 @@ -%{ -#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; - -%rename(less) CVC4::EmptySet::operator<(const EmptySet&) const; -%rename(lessEqual) CVC4::EmptySet::operator<=(const EmptySet&) const; -%rename(greater) CVC4::EmptySet::operator>(const EmptySet&) const; -%rename(greaterEqual) CVC4::EmptySet::operator>=(const EmptySet&) const; - -%rename(apply) CVC4::EmptySetHashFunction::operator()(const EmptySet&) const; - -%ignore CVC4::operator<<(std::ostream& out, const EmptySet& es); - -%include "expr/emptyset.h" diff --git a/src/expr/expr.i b/src/expr/expr.i deleted file mode 100644 index 7e79d4c1d..000000000 --- a/src/expr/expr.i +++ /dev/null @@ -1,172 +0,0 @@ -%{ -#include "expr/expr.h" -%} - -%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() - -%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; - -%rename(getChild) CVC4::Expr::operator[](unsigned i) const; - -#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; - -%typemap(javabody) CVC4::Expr %{ - 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 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(null, $imcall, true); -} - -%typemap(javaconstruct) CVC4::Expr { - this(null, $imcall, true); -} - -%typemap(javaout) CVC4::Expr { - return new Expr(this.em, $jnicall, true); -} - -SWIG_STD_VECTOR_EM(CVC4::Expr, const CVC4::Expr&) -SWIG_STD_VECTOR_EM(std::vector<CVC4::Expr>, const std::vector<CVC4::Expr>&) - -%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>>; - -%javamethodmodifiers CVC4::Expr::operator=(const Expr&) "protected"; - -%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; -%ignore CVC4::Expr::const_iterator; - -// Expr is "iterable" on the Java side -%typemap(javainterfaces) CVC4::Expr "java.lang.Iterable<edu.stanford.CVC4.Expr>"; - -// the JavaIteratorAdapter should not be public, and implements Iterator -%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr> "class"; -%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::Expr, 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::Expr, 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::Expr, CVC4::Expr>::getNext() "private"; - -#endif /* SWIGJAVA */ - -#ifdef SWIGPYTHON -%rename(doApply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const; -#endif /* SWIGPYTHON */ - -%include "expr/expr.h" - -#ifdef SWIGPYTHON -/* The python bindings on Mac OS X have trouble with this one - leave it - * out for now. */ -//%template(getConstTypeConstant) CVC4::Expr::getConst<CVC4::TypeConstant>; -#else -%template(getConstTypeConstant) CVC4::Expr::getConst<CVC4::TypeConstant>; -#endif -%template(getConstArrayStoreAll) CVC4::Expr::getConst<CVC4::ArrayStoreAll>; -%template(getConstAscriptionType) CVC4::Expr::getConst<CVC4::AscriptionType>; -%template(getConstBitVector) CVC4::Expr::getConst<CVC4::BitVector>; -%template(getConstBitVectorBitOf) CVC4::Expr::getConst<CVC4::BitVectorBitOf>; -%template(getConstBitVectorExtract) CVC4::Expr::getConst<CVC4::BitVectorExtract>; -%template(getConstBitVectorRepeat) CVC4::Expr::getConst<CVC4::BitVectorRepeat>; -%template(getConstBitVectorRotateLeft) CVC4::Expr::getConst<CVC4::BitVectorRotateLeft>; -%template(getConstBitVectorRotateRight) CVC4::Expr::getConst<CVC4::BitVectorRotateRight>; -%template(getConstBitVectorSignExtend) CVC4::Expr::getConst<CVC4::BitVectorSignExtend>; -%template(getConstBitVectorSize) CVC4::Expr::getConst<CVC4::BitVectorSize>; -%template(getConstBitVectorZeroExtend) CVC4::Expr::getConst<CVC4::BitVectorZeroExtend>; -%template(getConstBoolean) CVC4::Expr::getConst<bool>; -%template(getConstDatatypeIndexConstant) CVC4::Expr::getConst<CVC4::DatatypeIndexConstant>; -%template(getConstEmptySet) CVC4::Expr::getConst<CVC4::EmptySet>; -%template(getConstExprSequence) CVC4::Expr::getConst<CVC4::ExprSequence>; -%template(getConstFloatingPoint) CVC4::Expr::getConst<CVC4::FloatingPoint>; -%template(getConstKind) CVC4::Expr::getConst<CVC4::kind::Kind_t>; -%template(getConstRational) CVC4::Expr::getConst<CVC4::Rational>; -%template(getConstRoundingMode) CVC4::Expr::getConst<CVC4::RoundingMode>; -%template(getConstString) CVC4::Expr::getConst<CVC4::String>; -%template(getConstUninterpretedConstant) CVC4::Expr::getConst<CVC4::UninterpretedConstant>; - -#ifdef SWIGJAVA - -SWIG_JAVA_ITERATOR_ADAPTER(CVC4::Expr, CVC4::Expr) -%template(JavaIteratorAdapter_Expr) CVC4::JavaIteratorAdapter<CVC4::Expr, CVC4::Expr>; - -#endif /* SWIGJAVA */ diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i deleted file mode 100644 index d8ed7f6a6..000000000 --- a/src/expr/expr_manager.i +++ /dev/null @@ -1,151 +0,0 @@ -%{ -#include "expr/expr_manager.h" -%} - -%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::ArrayStoreAll>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorSize>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::AscriptionType>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorBitOf>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRepeat>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorExtract>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRotateLeft>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorSignExtend>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorZeroExtend>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVectorRotateRight>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::IntToBitVector>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPoint>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointSize>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPIEEEBitVector>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPFloatingPoint>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPReal>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPSignedBitVector>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPUnsignedBitVector>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToFPGeneric>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToUBV>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::FloatingPointToSBV>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::UninterpretedConstant>; -%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::Rational>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::BitVector>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::EmptySet>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::ExprSequence>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::String>; -#ifdef SWIGPYTHON -/* The python bindings cannot differentiate between bool and other basic - * types like enum and int. Therefore, we rename mkConst for the bool - * case into mkBoolConst. -*/ -%template(mkBoolConst) CVC4::ExprManager::mkConst<bool>; -%template(mkRoundingMode) CVC4::ExprManager::mkConst<RoundingMode>; - -// These cases have trouble too. Remove them for now. -//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>; -#else -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>; -%template(mkConst) CVC4::ExprManager::mkConst<bool>; -%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RoundingMode>; -#endif diff --git a/src/expr/expr_sequence.i b/src/expr/expr_sequence.i deleted file mode 100644 index 294937024..000000000 --- a/src/expr/expr_sequence.i +++ /dev/null @@ -1,54 +0,0 @@ -%{ -#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; - -%rename(less) CVC4::ExprSequence::operator<(const ExprSequence&) const; -%rename(lessEqual) CVC4::ExprSequence::operator<=(const ExprSequence&) const; -%rename(greater) CVC4::ExprSequence::operator>(const ExprSequence&) const; -%rename(greaterEqual) CVC4::ExprSequence::operator>=(const ExprSequence&) const; - -%rename(apply) CVC4::ExprSequenceHashFunction::operator()(const ExprSequence&) const; - -%ignore CVC4::operator<<(std::ostream& out, const ExprSequence& es); - -%include "expr/expr_sequence.h" diff --git a/src/expr/kind.i b/src/expr/kind.i deleted file mode 100644 index 189c94f1f..000000000 --- a/src/expr/kind.i +++ /dev/null @@ -1,16 +0,0 @@ -%{ -#include "expr/kind.h" -%} - -%ignore CVC4::kind::operator<<(std::ostream&, CVC4::Kind); -%ignore CVC4::operator<<(std::ostream&, TypeConstant); -%ignore CVC4::theory::operator<<(std::ostream&, TheoryId); - -%ignore CVC4::theory::operator++(TheoryId&); - -%rename(apply) CVC4::kind::KindHashFunction::operator()(::CVC4::Kind) const; -%rename(apply) CVC4::TypeConstantHashFunction::operator()(TypeConstant) const; - -%rename(Kind) CVC4::kind::Kind_t; - -%include "expr/kind.h" diff --git a/src/expr/type.i b/src/expr/type.i deleted file mode 100644 index 8262c4cea..000000000 --- a/src/expr/type.i +++ /dev/null @@ -1,437 +0,0 @@ -%{ -#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 */ -%rename(apply) CVC4::TypeHashFunction::operator()(const CVC4::Type&) const; -#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(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; - } -%} - -// 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(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; - } - - 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; - } - - 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/uninterpreted_constant.i b/src/expr/uninterpreted_constant.i deleted file mode 100644 index 1636eba5b..000000000 --- a/src/expr/uninterpreted_constant.i +++ /dev/null @@ -1,17 +0,0 @@ -%{ -#include "expr/uninterpreted_constant.h" -%} - -%rename(less) CVC4::UninterpretedConstant::operator<(const UninterpretedConstant&) const; -%rename(lessEqual) CVC4::UninterpretedConstant::operator<=(const UninterpretedConstant&) const; -%rename(greater) CVC4::UninterpretedConstant::operator>(const UninterpretedConstant&) const; -%rename(greaterEqual) CVC4::UninterpretedConstant::operator>=(const UninterpretedConstant&) const; - -%rename(equals) CVC4::UninterpretedConstant::operator==(const UninterpretedConstant&) const; -%ignore CVC4::UninterpretedConstant::operator!=(const UninterpretedConstant&) const; - -%rename(apply) CVC4::UninterpretedConstantHashFunction::operator()(const UninterpretedConstant&) const; - -%ignore CVC4::operator<<(std::ostream&, const UninterpretedConstant&); - -%include "expr/uninterpreted_constant.h" diff --git a/src/expr/variable_type_map.i b/src/expr/variable_type_map.i deleted file mode 100644 index 17ca6a110..000000000 --- a/src/expr/variable_type_map.i +++ /dev/null @@ -1,56 +0,0 @@ -%{ -#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); - -%ignore CVC4::ExprManagerMapCollection::d_typeMap; -%ignore CVC4::ExprManagerMapCollection::d_to; -%ignore CVC4::ExprManagerMapCollection::d_from; - -%include "expr/variable_type_map.h" diff --git a/src/options/language.i b/src/options/language.i deleted file mode 100644 index 7f81ea7c6..000000000 --- a/src/options/language.i +++ /dev/null @@ -1,42 +0,0 @@ -%{ -#include "options/language.h" -%} - -namespace CVC4 { - namespace language { - namespace input { - %ignore operator<<(std::ostream&, Language); - }/* CVC4::language::input namespace */ - - namespace output { - %ignore operator<<(std::ostream&, Language); - }/* CVC4::language::output namespace */ - }/* CVC4::language namespace */ -}/* CVC4 namespace */ - -// These clash in the monolithic Java namespace, so we rename them. -%rename(InputLanguage) CVC4::language::input::Language; -%rename(OutputLanguage) CVC4::language::output::Language; - -%rename(INPUT_LANG_AUTO) CVC4::language::input::LANG_AUTO; -%rename(INPUT_LANG_SMTLIB_V2) CVC4::language::input::LANG_SMTLIB_V2; -%rename(INPUT_LANG_SMTLIB_V2_0) CVC4::language::input::LANG_SMTLIB_V2_0; -%rename(INPUT_LANG_SMTLIB_V2_5) CVC4::language::input::LANG_SMTLIB_V2_5; -%rename(INPUT_LANG_SMTLIB_V2_6) CVC4::language::input::LANG_SMTLIB_V2_6; -%rename(INPUT_LANG_TPTP) CVC4::language::input::LANG_TPTP; -%rename(INPUT_LANG_CVC4) CVC4::language::input::LANG_CVC4; -%rename(INPUT_LANG_MAX) CVC4::language::input::LANG_MAX; -%rename(INPUT_LANG_SYGUS_V2) CVC4::language::input::LANG_SYGUS_V2; - -%rename(OUTPUT_LANG_AUTO) CVC4::language::output::LANG_AUTO; -%rename(OUTPUT_LANG_SMTLIB_V2) CVC4::language::output::LANG_SMTLIB_V2; -%rename(OUTPUT_LANG_SMTLIB_V2_0) CVC4::language::output::LANG_SMTLIB_V2_0; -%rename(OUTPUT_LANG_SMTLIB_V2_5) CVC4::language::output::LANG_SMTLIB_V2_5; -%rename(OUTPUT_LANG_SMTLIB_V2_6) CVC4::language::output::LANG_SMTLIB_V2_6; -%rename(OUTPUT_LANG_TPTP) CVC4::language::output::LANG_TPTP; -%rename(OUTPUT_LANG_CVC4) CVC4::language::output::LANG_CVC4; -%rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST; -%rename(OUTPUT_LANG_MAX) CVC4::language::output::LANG_MAX; -%rename(OUTPUT_LANG_SYGUS_V2) CVC4::language::output::LANG_SYGUS_V2; - -%include "options/language.h" diff --git a/src/options/option_exception.i b/src/options/option_exception.i deleted file mode 100644 index ae68d4e0f..000000000 --- a/src/options/option_exception.i +++ /dev/null @@ -1,5 +0,0 @@ -%{ -#include "options/option_exception.h" -%} - -%include "options/option_exception.h" diff --git a/src/options/options.i b/src/options/options.i deleted file mode 100644 index 319b4addb..000000000 --- a/src/options/options.i +++ /dev/null @@ -1,22 +0,0 @@ -%{ -#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 deleted file mode 100644 index 780a75996..000000000 --- a/src/proof/unsat_core.i +++ /dev/null @@ -1,65 +0,0 @@ -%{ -#include "proof/unsat_core.h" -%} - -%ignore CVC4::operator<<(std::ostream&, const UnsatCore&); - -#ifdef SWIGJAVA - -%typemap(javabody) CVC4::UnsatCore %{ - 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 JavaIteratorAdapter_UnsatCore iterator() { - return new JavaIteratorAdapter_UnsatCore(this.em, this); - } -%} - -%typemap(javaout) CVC4::Expr { - return new Expr(this.em, $jnicall, true); -} - -%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 -// Iterator. -%ignore CVC4::UnsatCore::begin(); -%ignore CVC4::UnsatCore::end(); -%ignore CVC4::UnsatCore::begin() const; -%ignore CVC4::UnsatCore::end() const; - -%extend CVC4::UnsatCore { - std::string toString() - { - std::stringstream ss; - ss << (*$self); - return ss.str(); - } -} - -// UnsatCore is "iterable" on the Java side -%typemap(javainterfaces) CVC4::UnsatCore "java.lang.Iterable<edu.stanford.CVC4.Expr>"; - -#endif /* SWIGJAVA */ - -%include "proof/unsat_core.h" - -#ifdef SWIGJAVA - -SWIG_JAVA_ITERATOR_ADAPTER(CVC4::UnsatCore, CVC4::Expr) -%template(JavaIteratorAdapter_UnsatCore) CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr>; - -#endif /* SWIGJAVA */ diff --git a/src/smt/logic_exception.i b/src/smt/logic_exception.i deleted file mode 100644 index 0c4ab50e0..000000000 --- a/src/smt/logic_exception.i +++ /dev/null @@ -1,7 +0,0 @@ -%{ -#include "smt/logic_exception.h" -%} - -%ignore CVC4::LogicException::LogicException(const char*); - -%include "smt/logic_exception.h" diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i deleted file mode 100644 index 95a5f4f3b..000000000 --- a/src/smt/smt_engine.i +++ /dev/null @@ -1,35 +0,0 @@ -%{ -#include "smt/smt_engine.h" -%} - -#ifdef SWIGJAVA - -%typemap(javacode) CVC4::SmtEngine %{ - // a ref is kept here to keep Java GC from collecting the EM - // before the SmtEngine - private ExprManager em; -%} - -%typemap(javaconstruct) SmtEngine { - this($imcall, true); - this.em = em; // keep ref to expr manager in SWIG proxy class -} - -%typemap(javaout) CVC4::Expr { - return new Expr(this.em, $jnicall, true); -} - -%typemap(javaout) CVC4::UnsatCore { - return new UnsatCore(this.em, $jnicall, true); -} - -// %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/theory/logic_info.i b/src/theory/logic_info.i deleted file mode 100644 index ee3652a1e..000000000 --- a/src/theory/logic_info.i +++ /dev/null @@ -1,17 +0,0 @@ -%{ -#include "theory/logic_info.h" -%} - -%ignore CVC4::LogicInfo::LogicInfo(const char*); - -%rename(less) CVC4::LogicInfo::operator<(const LogicInfo&) const; -%rename(lessEqual) CVC4::LogicInfo::operator<=(const LogicInfo&) const; -%rename(greater) CVC4::LogicInfo::operator>(const LogicInfo&) const; -%rename(greaterEqual) CVC4::LogicInfo::operator>=(const LogicInfo&) const; - -%rename(equals) CVC4::LogicInfo::operator==(const LogicInfo&) const; -%ignore CVC4::LogicInfo::operator!=(const LogicInfo&) const; - -%ignore CVC4::operator<<(std::ostream&, const LogicInfo&); - -%include "theory/logic_info.h" diff --git a/src/theory/theory_id.i b/src/theory/theory_id.i deleted file mode 100644 index afe01d7b2..000000000 --- a/src/theory/theory_id.i +++ /dev/null @@ -1,5 +0,0 @@ -%{ -#include "theory/theory_id.h" -%} - -%include "theory/theory_id.h" diff --git a/src/util/bitvector.i b/src/util/bitvector.i deleted file mode 100644 index 8eb6158ae..000000000 --- a/src/util/bitvector.i +++ /dev/null @@ -1,43 +0,0 @@ -%{ -#include "util/bitvector.h" -%} - -%ignore CVC4::BitVector::BitVector(unsigned, unsigned); - -%rename(assign) CVC4::BitVector::operator=(const BitVector&); -%rename(equals) CVC4::BitVector::operator==(const BitVector&) const; -%ignore CVC4::BitVector::operator!=(const BitVector&) const; -%rename(plus) CVC4::BitVector::operator+(const BitVector&) const; -%rename(minus) CVC4::BitVector::operator-(const BitVector&) const; -%rename(minus) CVC4::BitVector::operator-() const; -%rename(times) CVC4::BitVector::operator*(const BitVector&) const; -%rename(bitXor) CVC4::BitVector::operator^(const BitVector&) const; -%rename(bitOr) CVC4::BitVector::operator|(const BitVector&) const; -%rename(bitAnd) CVC4::BitVector::operator&(const BitVector&) const; -%rename(complement) CVC4::BitVector::operator~() const; -%rename(less) CVC4::BitVector::operator<(const BitVector&) const; -%rename(lessEqual) CVC4::BitVector::operator<=(const BitVector&) const; -%rename(greater) CVC4::BitVector::operator>(const BitVector&) const; -%rename(greaterEqual) CVC4::BitVector::operator>=(const BitVector&) const; - -%rename(equals) CVC4::BitVectorExtract::operator==(const BitVectorExtract&) const; -%rename(equals) CVC4::BitVectorBitOf::operator==(const BitVectorBitOf&) const; - -%rename(toUnsigned) CVC4::BitVectorSize::operator unsigned() const; -%rename(toUnsigned) CVC4::BitVectorRepeat::operator unsigned() const; -%rename(toUnsigned) CVC4::BitVectorZeroExtend::operator unsigned() const; -%rename(toUnsigned) CVC4::BitVectorSignExtend::operator unsigned() const; -%rename(toUnsigned) CVC4::BitVectorRotateLeft::operator unsigned() const; -%rename(toUnsigned) CVC4::BitVectorRotateRight::operator unsigned() const; -%rename(toUnsigned) CVC4::IntToBitVector::operator unsigned() const; - -%rename(apply) CVC4::BitVectorHashFunction::operator()(const BitVector&) const; -%rename(apply) CVC4::BitVectorExtractHashFunction::operator()(const BitVectorExtract&) const; -%rename(apply) CVC4::BitVectorBitOfHashFunction::operator()(const BitVectorBitOf&) const; - -%ignore CVC4::operator<<(std::ostream&, const BitVector&); -%ignore CVC4::operator<<(std::ostream&, const BitVectorExtract&); -%ignore CVC4::operator<<(std::ostream&, const BitVectorBitOf&); -%ignore CVC4::operator<<(std::ostream&, const IntToBitVector&); - -%include "util/bitvector.h" diff --git a/src/util/bool.i b/src/util/bool.i deleted file mode 100644 index 47a0c4217..000000000 --- a/src/util/bool.i +++ /dev/null @@ -1,7 +0,0 @@ -%{ -#include "util/bool.h" -%} - -%rename(apply) CVC4::BoolHashFunction::operator()(bool) const; - -%include "util/bool.h" diff --git a/src/util/cardinality.i b/src/util/cardinality.i deleted file mode 100644 index c88037cfe..000000000 --- a/src/util/cardinality.i +++ /dev/null @@ -1,23 +0,0 @@ -%{ -#include "util/cardinality.h" -%} - -%feature("valuewrapper") CVC4::CardinalityBeth; - -%rename(plusAssign) CVC4::Cardinality::operator+=(const Cardinality&); -%rename(timesAssign) CVC4::Cardinality::operator*=(const Cardinality&); -%rename(powerAssign) CVC4::Cardinality::operator^=(const Cardinality&); -%rename(plus) CVC4::Cardinality::operator+(const Cardinality&) const; -%rename(times) CVC4::Cardinality::operator*(const Cardinality&) const; -%rename(power) CVC4::Cardinality::operator^(const Cardinality&) const; -%rename(equals) CVC4::Cardinality::operator==(const Cardinality&) const; -%ignore CVC4::Cardinality::operator!=(const Cardinality&) const; -%rename(less) CVC4::Cardinality::operator<(const Cardinality&) const; -%rename(lessEqual) CVC4::Cardinality::operator<=(const Cardinality&) const; -%rename(greater) CVC4::Cardinality::operator>(const Cardinality&) const; -%rename(greaterEqual) CVC4::Cardinality::operator>=(const Cardinality&) const; - -%ignore CVC4::operator<<(std::ostream&, const Cardinality&); -%ignore CVC4::operator<<(std::ostream&, CardinalityBeth); - -%include "util/cardinality.h" diff --git a/src/util/divisible.i b/src/util/divisible.i deleted file mode 100644 index 7599360ca..000000000 --- a/src/util/divisible.i +++ /dev/null @@ -1,10 +0,0 @@ -%{ -#include "util/divisible.h" -%} - -%rename(equals) CVC4::Divisible::operator==(const Divisible&) const; -%ignore CVC4::Divisible::operator!=(const Divisible&) const; - -%ignore CVC4::operator<<(std::ostream&, const Divisible&); - -%include "util/divisible.h" diff --git a/src/util/floatingpoint.i b/src/util/floatingpoint.i deleted file mode 100644 index 7a57de057..000000000 --- a/src/util/floatingpoint.i +++ /dev/null @@ -1,18 +0,0 @@ -%{ -#include "util/floatingpoint.h" -%} - -// Ignore the methods related to FloatingPointLiteral (otherwise we have to -// wrap those classes as well) -%ignore CVC4::FloatingPointLiteral; -%ignore CVC4::FloatingPoint::FloatingPoint (const FloatingPointSize &oldt, const FloatingPointLiteral &oldfpl); -%ignore CVC4::FloatingPoint::getLiteral () const; - -// Ignore the partial methods (otherwise we have to provide a template -// instantiation for std::pair<FloatingPoint, bool> which is quite ugly) -%ignore CVC4::FloatingPoint::max(const FloatingPoint &arg) const; -%ignore CVC4::FloatingPoint::min(const FloatingPoint &arg) const; -%ignore CVC4::FloatingPoint::convertToRational() const; -%ignore CVC4::FloatingPoint::convertToBV(BitVectorSize width, const RoundingMode &rm, bool signedBV) const; - -%include "util/floatingpoint.h" diff --git a/src/util/hash.i b/src/util/hash.i deleted file mode 100644 index f2f1e6652..000000000 --- a/src/util/hash.i +++ /dev/null @@ -1,5 +0,0 @@ -%{ -#include "util/hash.h" -%} - -%include "util/hash.h" diff --git a/src/util/iand.i b/src/util/iand.i deleted file mode 100644 index 92c5a1223..000000000 --- a/src/util/iand.i +++ /dev/null @@ -1,9 +0,0 @@ -%{ -#include "util/iand.h" -%} - -%rename(toUnsigned) CVC4::IntAnd::operator unsigned() const; - -%ignore CVC4::operator<<(std::ostream&, const IntAnd&); - -%include "util/iand.h" diff --git a/src/util/integer.i b/src/util/integer.i deleted file mode 100644 index c8d2f7bdf..000000000 --- a/src/util/integer.i +++ /dev/null @@ -1,33 +0,0 @@ -%{ -#include "util/integer.h" -%} - -%ignore CVC4::Integer::Integer(int); -%ignore CVC4::Integer::Integer(unsigned int); -%ignore CVC4::Integer::Integer(const std::string&); -%ignore CVC4::Integer::Integer(const std::string&, unsigned int); - -%rename(assign) CVC4::Integer::operator=(const Integer&); -%rename(equals) CVC4::Integer::operator==(const Integer&) const; -%ignore CVC4::Integer::operator!=(const Integer&) const; -%rename(plus) CVC4::Integer::operator+(const Integer&) const; -%rename(minus) CVC4::Integer::operator-() const; -%rename(minus) CVC4::Integer::operator-(const Integer&) const; -%rename(times) CVC4::Integer::operator*(const Integer&) const; -%rename(dividedBy) CVC4::Integer::operator/(const Integer&) const; -%rename(modulo) CVC4::Integer::operator%(const Integer&) const; -%rename(plusAssign) CVC4::Integer::operator+=(const Integer&); -%rename(minusAssign) CVC4::Integer::operator-=(const Integer&); -%rename(timesAssign) CVC4::Integer::operator*=(const Integer&); -%rename(dividedByAssign) CVC4::Integer::operator/=(const Integer&); -%rename(moduloAssign) CVC4::Integer::operator%=(const Integer&); -%rename(less) CVC4::Integer::operator<(const Integer&) const; -%rename(lessEqual) CVC4::Integer::operator<=(const Integer&) const; -%rename(greater) CVC4::Integer::operator>(const Integer&) const; -%rename(greaterEqual) CVC4::Integer::operator>=(const Integer&) const; - -%rename(apply) CVC4::IntegerHashFunction::operator()(const CVC4::Integer&) const; - -%ignore CVC4::operator<<(std::ostream&, const Integer&); - -%include "util/integer.h" diff --git a/src/util/proof.i b/src/util/proof.i deleted file mode 100644 index 59a524a0f..000000000 --- a/src/util/proof.i +++ /dev/null @@ -1,7 +0,0 @@ -%{ -#include "util/proof.h" -%} - -%ignore CVC4::Proof::toStream(std::ostream& out, const ProofLetMap& map) const; - -%include "util/proof.h" diff --git a/src/util/rational.i b/src/util/rational.i deleted file mode 100644 index a65c78327..000000000 --- a/src/util/rational.i +++ /dev/null @@ -1,33 +0,0 @@ -%{ -#include "util/rational.h" -%} - -%ignore CVC4::Rational::Rational(int); -%ignore CVC4::Rational::Rational(unsigned int); -%ignore CVC4::Rational::Rational(int, int); -%ignore CVC4::Rational::Rational(unsigned int, unsigned int); -%ignore CVC4::Rational::Rational(const std::string&); -%ignore CVC4::Rational::Rational(const std::string&, unsigned int); - -%rename(assign) CVC4::Rational::operator=(const Rational&); -%rename(equals) CVC4::Rational::operator==(const Rational&) const; -%ignore CVC4::Rational::operator!=(const Rational&) const; -%rename(plus) CVC4::Rational::operator+(const Rational&) const; -%rename(minus) CVC4::Rational::operator-() const; -%rename(minus) CVC4::Rational::operator-(const Rational&) const; -%rename(times) CVC4::Rational::operator*(const Rational&) const; -%rename(dividedBy) CVC4::Rational::operator/(const Rational&) const; -%rename(plusAssign) CVC4::Rational::operator+=(const Rational&); -%rename(minusAssign) CVC4::Rational::operator-=(const Rational&); -%rename(timesAssign) CVC4::Rational::operator*=(const Rational&); -%rename(dividedByAssign) CVC4::Rational::operator/=(const Rational&); -%rename(less) CVC4::Rational::operator<(const Rational&) const; -%rename(lessEqual) CVC4::Rational::operator<=(const Rational&) const; -%rename(greater) CVC4::Rational::operator>(const Rational&) const; -%rename(greaterEqual) CVC4::Rational::operator>=(const Rational&) const; - -%rename(apply) CVC4::RationalHashFunction::operator()(const CVC4::Rational&) const; - -%ignore CVC4::operator<<(std::ostream&, const Rational&); - -%include "util/rational.h" diff --git a/src/util/regexp.i b/src/util/regexp.i deleted file mode 100644 index 775e778f7..000000000 --- a/src/util/regexp.i +++ /dev/null @@ -1,12 +0,0 @@ -%{ -#include "util/regexp.h" -%} - -%rename(equals) CVC4::RegExpRepeat::operator==(const RegExpRepeat&) const; - -%rename(equals) CVC4::RegExpLoop::operator==(const RegExpLoop&) const; - -%ignore CVC4::operator<<(std::ostream&, const RegExpRepeat&); -%ignore CVC4::operator<<(std::ostream&, const RegExpLoop&); - -%include "util/regexp.h" diff --git a/src/util/result.i b/src/util/result.i deleted file mode 100644 index cb835fbb0..000000000 --- a/src/util/result.i +++ /dev/null @@ -1,20 +0,0 @@ -%{ -#include "util/result.h" -%} - -%ignore CVC4::operator<<(std::ostream&, const Result& r); - -%rename(equals) CVC4::Result::operator==(const Result& r) const; -%ignore CVC4::Result::operator!=(const Result& r) const; - -%ignore CVC4::operator<<(std::ostream&, enum Result::Sat); -%ignore CVC4::operator<<(std::ostream&, enum Result::Entailment); -%ignore CVC4::operator<<(std::ostream&, enum Result::UnknownExplanation); - -%ignore CVC4::operator==(enum Result::Sat, const Result&); -%ignore CVC4::operator!=(enum Result::Sat, const Result&); - -%ignore CVC4::operator==(enum Result::Entailment, const Result&); -%ignore CVC4::operator!=(enum Result::Entailment, const Result&); - -%include "util/result.h" diff --git a/src/util/sexpr.i b/src/util/sexpr.i deleted file mode 100644 index 3c865c097..000000000 --- a/src/util/sexpr.i +++ /dev/null @@ -1,22 +0,0 @@ -%{ -#include "util/sexpr.h" -%} - -%ignore CVC4::operator<<(std::ostream&, const SExpr&); -%ignore CVC4::operator<<(std::ostream&, SExpr::SexprTypes); -%ignore CVC4::operator<<(std::ostream&, PrettySExprs); - -// for Java and the like -%extend CVC4::SExpr { - std::string toString() const { return self->getValue(); } -};/* CVC4::SExpr */ - -%ignore CVC4::SExpr::SExpr(int); -%ignore CVC4::SExpr::SExpr(unsigned int); -%ignore CVC4::SExpr::SExpr(unsigned long); -%ignore CVC4::SExpr::SExpr(const char*); - -%rename(equals) CVC4::SExpr::operator==(const SExpr&) const; -%ignore CVC4::SExpr::operator!=(const SExpr&) const; - -%include "util/sexpr.h" diff --git a/src/util/statistics.i b/src/util/statistics.i deleted file mode 100644 index 7dfc7ec39..000000000 --- a/src/util/statistics.i +++ /dev/null @@ -1,75 +0,0 @@ -%{ -#include "util/statistics.h" - -#ifdef SWIGJAVA - -#include "bindings/java_iterator_adapter.h" - -#endif /* SWIGJAVA */ -%} - -%include "stdint.i" - -%rename(assign) CVC4::Statistics::operator=(const StatisticsBase&); -%rename(assign) CVC4::Statistics::operator=(const Statistics& stats); - -#ifdef SWIGJAVA - -// Instead of StatisticsBase::begin() and end(), create an -// iterator() method on the Java side that returns a Java-style -// Iterator. -%ignore CVC4::StatisticsBase::begin(); -%ignore CVC4::StatisticsBase::end(); -%ignore CVC4::StatisticsBase::begin() const; -%ignore CVC4::StatisticsBase::end() const; -%extend CVC4::StatisticsBase { - CVC4::JavaIteratorAdapter<CVC4::StatisticsBase, - std::pair<std::string, CVC4::SExpr> > - iterator() - { - return CVC4::JavaIteratorAdapter<CVC4::StatisticsBase, - std::pair<std::string, CVC4::SExpr> >( - *$self); - } -} - -// StatisticsBase is "iterable" on the Java side -%typemap(javainterfaces) CVC4::StatisticsBase "java.lang.Iterable<Statistic>"; - -// the JavaIteratorAdapter should not be public, and implements Iterator -%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase, std::pair<std::string, CVC4::SExpr> > "class"; -%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase, std::pair<std::string, CVC4::SExpr> > "java.util.Iterator<Statistic>"; -// 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::StatisticsBase, std::pair<std::string, CVC4::SExpr> > " - public void remove() { - throw new java.lang.UnsupportedOperationException(); - } - - public Statistic 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::StatisticsBase, std::pair<std::string, CVC4::SExpr> >::getNext() "private"; - -#endif /* SWIGJAVA */ - -%include "util/statistics.h" - -#ifdef SWIGJAVA - -%include <std_pair.i> -%include <std_string.i> - -%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/src/util/string.i b/src/util/string.i deleted file mode 100644 index 1ded901aa..000000000 --- a/src/util/string.i +++ /dev/null @@ -1,25 +0,0 @@ -%{ -#include "util/string.h" -%} - -%rename(CVC4String) String; -%rename(CVC4StringHashFunction) CVC4::strings::StringHashFunction; - -%ignore CVC4::String::String(const std::string&); - -%rename(assign) CVC4::String::operator=(const String&); -%rename(getChar) CVC4::String::operator[](const unsigned int) const; -%rename(equals) CVC4::String::operator==(const String&) const; -%ignore CVC4::String::operator!=(const String&) const; -%rename(less) CVC4::String::operator<(const String&) const; -%rename(lessEqual) CVC4::String::operator<=(const String&) const; -%rename(greater) CVC4::String::operator>(const String&) const; -%rename(greaterEqual) CVC4::String::operator>=(const String&) const; - -%rename(apply) CVC4::strings::StringHashFunction::operator()(const ::CVC4::String&) const; - -%ignore CVC4::operator<<(std::ostream&, const String&); - -%apply int &OUTPUT { int &c }; -%include "util/string.h" -%clear int &c; diff --git a/src/util/tuple.i b/src/util/tuple.i deleted file mode 100644 index d5bf22f30..000000000 --- a/src/util/tuple.i +++ /dev/null @@ -1,12 +0,0 @@ -%{ -#include "util/tuple.h" -%} - -%rename(equals) CVC4::TupleUpdate::operator==(const TupleUpdate&) const; -%ignore CVC4::TupleUpdate::operator!=(const TupleUpdate&) const; - -%rename(apply) CVC4::TupleUpdateHashFunction::operator()(const TupleUpdate&) const; - -%ignore CVC4::operator<<(std::ostream&, const TupleUpdate&); - -%include "util/tuple.h" diff --git a/src/util/unsafe_interrupt_exception.i b/src/util/unsafe_interrupt_exception.i deleted file mode 100644 index 94a552877..000000000 --- a/src/util/unsafe_interrupt_exception.i +++ /dev/null @@ -1,7 +0,0 @@ -%{ -#include "util/unsafe_interrupt_exception.h" -%} - -%ignore CVC4::UnsafeInterruptException::UnsafeInterruptException(const char*); - -%include "util/unsafe_interrupt_exception.h" |