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
# 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
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
#
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("")
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)
## 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.
Use `-jN` for parallel **building** with `N` threads.
-
Changes:
* SyGuS: Removed support for SyGuS-IF 1.0.
+* Removed Java and Python bindings for the legacy API
Changes since 1.7
=================
--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
python2=default
python3=default
python_bindings=default
+java_bindings=default
readline=default
shared=default
static_binary=default
valgrind=default
win64=default
-language_bindings_java=default
-language_bindings_python=default
-
abc_dir=default
antlr_dir=default
cadical_dir=default
--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;;
--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##*=} ;;
&& 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 ] \
&& 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 ] \
+++ /dev/null
-%{
-#include "base/configuration.h"
-%}
-
-%apply char **STRING_ARRAY { char const* const* }
-%include "base/configuration.h"
-%clear char const* const*;
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#include "base/modal_exception.h"
-%}
-
-%ignore CVC4::ModalException::ModalException(const char*);
-
-%include "base/modal_exception.h"
+++ /dev/null
-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()
+++ /dev/null
-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
-)
+++ /dev/null
-/**
- * The following file is based on
- * https://github.com/swig/swig/blob/master/Lib/java/std_vector.i
- *
- * Note: The SWIG library is under a different license than SWIG itself. See
- * https://github.com/swig/swig/blob/master/LICENSE for details.
- *
- * This file defines the macro SWIG_STD_VECTOR_EM to wrap a C++ std::vector for
- * Java, similar to the SWIG library. The core difference is that the utilities
- * in this file add a reference to an ExprManager to keep it alive as long as
- * the vector lives.
- */
-
-%include <std_common.i>
-
-%{
-#include <vector>
-#include <stdexcept>
-%}
-
-%fragment("SWIG_VectorSize", "header", fragment="SWIG_JavaIntFromSize_t") {
-SWIGINTERN jint SWIG_VectorSize(size_t size) {
- static const jint JINT_MAX = 0x7FFFFFFF;
- if (size > static_cast<size_t>(JINT_MAX))
- {
- throw std::out_of_range("vector size is too large to fit into a Java int");
- }
- return static_cast<jint>(size);
-}
-}
-
-%define SWIG_STD_VECTOR_EM(CTYPE, CONST_REFERENCE)
-
-namespace std {
- template<> class vector<CTYPE> {
-
-%typemap(javabase) std::vector< CTYPE > "java.util.AbstractList<$typemap(jstype, CTYPE)>"
-%typemap(javainterfaces) std::vector< CTYPE > "java.util.RandomAccess"
-
-%typemap(javabody) std::vector< CTYPE > %{
- private long swigCPtr;
- protected boolean swigCMemOwn;
- private ExprManager em;
-
- protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
- swigCMemOwn = cMemoryOwn;
- swigCPtr = cPtr;
- this.em = em;
- }
-
- public $javaclassname(ExprManager em) {
- this();
- this.em = em;
- }
-
- protected static long getCPtr($javaclassname obj) {
- return (obj == null) ? 0 : obj.swigCPtr;
- }
-%}
-
-%typemap(javaconstruct) std::vector<CTYPE> {
- this(null, $imcall, true);
-}
-
-%javamethodmodifiers vector() "private";
-
-%proxycode %{
- public $javaclassname(ExprManager em, $typemap(jstype, CTYPE)[] initialElements) {
- this(em);
- reserve(initialElements.length);
-
- for ($typemap(jstype, CTYPE) element : initialElements) {
- add(element);
- }
- }
-
- public $javaclassname(ExprManager em, Iterable<$typemap(jstype, CTYPE)> initialElements) {
- this(em);
- for ($typemap(jstype, CTYPE) element : initialElements) {
- add(element);
- }
- }
-
- public $typemap(jstype, CTYPE) get(int index) {
- return doGet(index);
- }
-
- public $typemap(jstype, CTYPE) set(int index, $typemap(jstype, CTYPE) e) {
- return doSet(index, e);
- }
-
- public boolean add($typemap(jstype, CTYPE) e) {
- modCount++;
- doAdd(e);
- return true;
- }
-
- public void add(int index, $typemap(jstype, CTYPE) e) {
- modCount++;
- doAdd(index, e);
- }
-
- public $typemap(jstype, CTYPE) remove(int index) {
- modCount++;
- return doRemove(index);
- }
-
- protected void removeRange(int fromIndex, int toIndex) {
- modCount++;
- doRemoveRange(fromIndex, toIndex);
- }
-
- public int size() {
- return doSize();
- }
-%}
-
- public:
- typedef size_t size_type;
- typedef ptrdiff_t difference_type;
- typedef CTYPE value_type;
- typedef CTYPE *pointer;
- typedef CTYPE const *const_pointer;
- typedef CTYPE &reference;
- typedef CONST_REFERENCE const_reference;
-
- vector();
- size_type capacity() const;
- void reserve(size_type n) throw (std::length_error);
- %rename(isEmpty) empty;
- bool empty() const;
- void clear();
- %extend {
- %fragment("SWIG_VectorSize");
-
- vector(jint count, const CTYPE &value) throw (std::out_of_range) {
- if (count < 0)
- throw std::out_of_range("vector count must be positive");
- return new std::vector< CTYPE >(static_cast<std::vector< CTYPE >::size_type>(count), value);
- }
-
- jint doSize() const throw (std::out_of_range) {
- return SWIG_VectorSize(self->size());
- }
-
- void doAdd(const value_type& x) {
- self->push_back(x);
- }
-
- void doAdd(jint index, const value_type& x) throw (std::out_of_range) {
- jint size = static_cast<jint>(self->size());
- if (0 <= index && index <= size) {
- self->insert(self->begin() + index, x);
- } else {
- throw std::out_of_range("vector index out of range");
- }
- }
-
- value_type doRemove(jint index) throw (std::out_of_range) {
- jint size = static_cast<jint>(self->size());
- if (0 <= index && index < size) {
- CTYPE const old_value = (*self)[index];
- self->erase(self->begin() + index);
- return old_value;
- } else {
- throw std::out_of_range("vector index out of range");
- }
- }
-
- CONST_REFERENCE doGet(jint index) throw (std::out_of_range) {
- jint size = static_cast<jint>(self->size());
- if (index >= 0 && index < size)
- return (*self)[index];
- else
- throw std::out_of_range("vector index out of range");
- }
-
- value_type doSet(jint index, const value_type& val) throw (std::out_of_range) {
- jint size = static_cast<jint>(self->size());
- if (index >= 0 && index < size) {
- CTYPE const old_value = (*self)[index];
- (*self)[index] = val;
- return old_value;
- }
- else
- throw std::out_of_range("vector index out of range");
- }
-
- void doRemoveRange(jint fromIndex, jint toIndex) throw (std::out_of_range) {
- jint size = static_cast<jint>(self->size());
- if (0 <= fromIndex && fromIndex <= toIndex && toIndex <= size) {
- self->erase(self->begin() + fromIndex, self->begin() + toIndex);
- } else {
- throw std::out_of_range("vector index out of range");
- }
- }
- }
- };
-}
-
-// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea
-%typemap(javaconstruct) vector<CTYPE> {
- this(null, $imcall, true);
-}
-
-%enddef
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-%{
-#include "bindings/java_iterator_adapter.h"
-%}
-
-#ifdef SWIGJAVA
-
-%define SWIG_JAVA_ITERATOR_ADAPTER(TTYPE, VTYPE)
-
-%typemap(javabody) CVC4::JavaIteratorAdapter %{
- private long swigCPtr;
- protected boolean swigCMemOwn;
- private ExprManager em;
-
- protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) {
- swigCMemOwn = cMemoryOwn;
- swigCPtr = cPtr;
- this.em = em;
- }
-
- public $javaclassname(ExprManager em, $typemap(jstype, TTYPE) t) {
- this(t);
- this.em = em;
- }
-
- protected static long getCPtr($javaclassname obj) {
- return (obj == null) ? 0 : obj.swigCPtr;
- }
-%}
-
-// Workaround for https://github.com/swig/swig/commit/63a5a8af88271559a7b170794b4c61c30b8934ea
-%typemap(javaconstruct) JavaIteratorAdapter<TTYPE, VTYPE> {
- this(null, $imcall, true);
-}
-
-%typemap(javaconstruct) CVC4::JavaIteratorAdapter<TTYPE, VTYPE> {
- this(null, $imcall, true);
-}
-
-%feature("valuewrapper") CVC4::JavaIteratorAdapter<TTYPE, VTYPE>;
-
-// the JavaIteratorAdapter should not be public, and implements Iterator
-%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<TTYPE, VTYPE> "class";
-%typemap(javainterfaces) CVC4::JavaIteratorAdapter< TTYPE, VTYPE > "java.util.Iterator<$typemap(jstype, VTYPE)>";
-
-// add some functions to the Java side (do it here because there's no way to do these in C++)
-%typemap(javacode) CVC4::JavaIteratorAdapter<TTYPE, VTYPE> "
- public void remove() {
- throw new java.lang.UnsupportedOperationException();
- }
-
- public $typemap(jstype, VTYPE) next() {
- if(hasNext()) {
- return getNext();
- } else {
- throw new java.util.NoSuchElementException();
- }
- }
-"
-
-// getNext() just allows C++ iterator access from Java-side next(), make it private
-%javamethodmodifiers CVC4::JavaIteratorAdapter<TTYPE, VTYPE>::getNext() "private";
-
-%javamethodmodifiers CVC4::JavaIteratorAdapter<TTYPE, VTYPE>::JavaIteratorAdapter(const TTYPE& t) "private";
-
-%enddef
-
-%include "bindings/java_iterator_adapter.h"
-
-namespace CVC4 {
- template<class T, class V> class JavaIteratorAdapter {
- SWIG_JAVA_ITERATOR_ADAPTER(T, V)
- };
-}
-
-#endif
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-# 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})
+++ /dev/null
-/********************* */
-/*! \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 */
+++ /dev/null
-// 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"
+++ /dev/null
-%{
-#include "expr/array.h"
-%}
-
-%include "expr/array.h"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#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 */
+++ /dev/null
-%{
-#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
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#include "options/option_exception.h"
-%}
-
-%include "options/option_exception.h"
+++ /dev/null
-%{
-#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[];
+++ /dev/null
-%{
-#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 */
+++ /dev/null
-%{
-#include "smt/logic_exception.h"
-%}
-
-%ignore CVC4::LogicException::LogicException(const char*);
-
-%include "smt/logic_exception.h"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#include "theory/theory_id.h"
-%}
-
-%include "theory/theory_id.h"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#include "util/bool.h"
-%}
-
-%rename(apply) CVC4::BoolHashFunction::operator()(bool) const;
-
-%include "util/bool.h"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#include "util/hash.h"
-%}
-
-%include "util/hash.h"
+++ /dev/null
-%{
-#include "util/iand.h"
-%}
-
-%rename(toUnsigned) CVC4::IntAnd::operator unsigned() const;
-
-%ignore CVC4::operator<<(std::ostream&, const IntAnd&);
-
-%include "util/iand.h"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#include "util/proof.h"
-%}
-
-%ignore CVC4::Proof::toStream(std::ostream& out, const ProofLetMap& map) const;
-
-%include "util/proof.h"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#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 */
+++ /dev/null
-%{
-#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;
+++ /dev/null
-%{
-#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"
+++ /dev/null
-%{
-#include "util/unsafe_interrupt_exception.h"
-%}
-
-%ignore CVC4::UnsafeInterruptException::UnsafeInterruptException(const char*);
-
-%include "util/unsafe_interrupt_exception.h"
projects / cvc5.git / commitdiff