diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-07-02 17:14:22 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-02 17:14:22 -0700 |
| commit | 2faf908ed88c798a25b4881e3ce3026dc139bca3 (patch) | |
| tree | a0e0977d8c40e4c4e6f9aa36f517335062ee282b | |
| parent | 34661cedac9ea64c4cec5fc71f0d303eb7688723 (diff) | |
Remove SWIG bindings (#4683)
This commit removes support for SWIG bindings for the legacy API. The
bindings were already broken by 19054b3b1d427e662d30d4322df2b2f2361353da
and we are not planning on using SWIG for the Java API for the new API.
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" |