cmake: Add SWIG support + Python and Java bindings.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 74f223e228598fd5f3d8a1ca2c20a508ef53cf93..81bbaf533120bb7498c0047117c35227b8ab0a32 100644 (file)
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -158,6 +158,12 @@ option(USE_LFSC                  "Use LFSC proof checker")
 option(USE_READLINE              "Use readline for better interactive support" OFF)
 option(USE_SYMFPU                "Use SymFPU for floating point support")
 
+# Supported language bindings
+option(BUILD_BINDINGS_JAVA       "Build Java bindings" OFF)
+option(BUILD_BINDINGS_PYTHON     "Build Python bindings" OFF)
+
+# All bindings: c,java,csharp,perl,php,python,ruby,tcl,ocaml
+
 
 #-----------------------------------------------------------------------------#
 # Internal cmake variables
@@ -239,6 +245,10 @@ enable_testing()
 
 #-----------------------------------------------------------------------------#
 
+if(BUILD_BINDINGS_JAVA OR BUILD_BINDINGS_PYTHON)
+  set(BUILD_BINDINGS TRUE)
+endif()
+
 if(ENABLE_ASAN)
   set(CMAKE_REQUIRED_LIBRARIES -fsanitize=address)
   add_required_c_cxx_flag("-fsanitize=address")
@@ -506,6 +516,9 @@ include_directories(${CMAKE_CURRENT_BINARY_DIR})
 
 add_subdirectory(doc)
 add_subdirectory(src)
+if(BUILD_BINDINGS)
+  add_subdirectory(src/bindings)
+endif()
 add_subdirectory(test/java)
 add_subdirectory(test/regress)
 add_subdirectory(test/system)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 2d8d209626b6369a1a191e15c81710f2e09270e9..0a8db038f9c6750f124576524142427e7b019257 100644 (file)
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -577,7 +577,6 @@ include_directories(include)
 include_directories(. ${CMAKE_CURRENT_BINARY_DIR})
 
 add_subdirectory(base)
-#add_subdirectory(bindings)
 add_subdirectory(compat)
 add_subdirectory(expr)
 add_subdirectory(lib)

diff --git a/src/bindings/CMakeLists.txt b/src/bindings/CMakeLists.txt
index 910b62766ebf6e3dac9d9218b60622b6352a5e44..a9032b0d9953899cd6d024a29e672d84ddb1f9ec 100644 (file)
--- a/src/bindings/CMakeLists.txt
+++ b/src/bindings/CMakeLists.txt
@@ -1 +1,18 @@
-add_subdirectory(compat)
+find_package(SWIG 3.0.0 REQUIRED)
+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_BINDINGS_JAVA)
+  add_subdirectory(java)
+endif()
+if(BUILD_BINDINGS_PYTHON)
+  add_subdirectory(python)
+endif()

diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
new file mode 100644 (file)
index 0000000..c3fee67
--- /dev/null
+++ b/src/bindings/java/CMakeLists.txt
@@ -0,0 +1,239 @@
+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.nyu.acsys.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}/AssertCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/BenchmarkStatus.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}/CheckSatAssumingCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/CheckSatCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/CheckSynthCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/Command.java
+  ${CMAKE_CURRENT_BINARY_DIR}/CommandFailure.java
+  ${CMAKE_CURRENT_BINARY_DIR}/CommandInterrupted.java
+  ${CMAKE_CURRENT_BINARY_DIR}/CommandPrintSuccess.java
+  ${CMAKE_CURRENT_BINARY_DIR}/CommandRecoverableFailure.java
+  ${CMAKE_CURRENT_BINARY_DIR}/CommandSequence.java
+  ${CMAKE_CURRENT_BINARY_DIR}/CommandStatus.java
+  ${CMAKE_CURRENT_BINARY_DIR}/CommandSuccess.java
+  ${CMAKE_CURRENT_BINARY_DIR}/CommandUnsupported.java
+  ${CMAKE_CURRENT_BINARY_DIR}/CommentCommand.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}/DatatypeDeclarationCommand.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}/DeclarationCheck.java
+  ${CMAKE_CURRENT_BINARY_DIR}/DeclarationDefinitionCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/DeclarationSequence.java
+  ${CMAKE_CURRENT_BINARY_DIR}/DeclareFunctionCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/DeclareTypeCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/DefineFunctionCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/DefineFunctionRecCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/DefineNamedFunctionCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/DefineTypeCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/EchoCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/EmptyCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/EmptySet.java
+  ${CMAKE_CURRENT_BINARY_DIR}/EmptySetHashFunction.java
+  ${CMAKE_CURRENT_BINARY_DIR}/Exception.java
+  ${CMAKE_CURRENT_BINARY_DIR}/ExpandDefinitionsCommand.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}/ExprStream.java
+  ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/FunctionType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/GetAssertionsCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/GetAssignmentCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/GetInfoCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/GetInstantiationsCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/GetModelCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/GetOptionCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/GetQuantifierEliminationCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/GetSynthSolutionCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/GetUnsatAssumptionsCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/GetUnsatCoreCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/GetValueCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/Input.java
+  ${CMAKE_CURRENT_BINARY_DIR}/InputLanguage.java
+  ${CMAKE_CURRENT_BINARY_DIR}/InputStream.java
+  ${CMAKE_CURRENT_BINARY_DIR}/InputStreamException.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_CommandSequence.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}/Parser.java
+  ${CMAKE_CURRENT_BINARY_DIR}/ParserBuilder.java
+  ${CMAKE_CURRENT_BINARY_DIR}/ParserEndOfFileException.java
+  ${CMAKE_CURRENT_BINARY_DIR}/ParserException.java
+  ${CMAKE_CURRENT_BINARY_DIR}/ParserExprStream.java
+  ${CMAKE_CURRENT_BINARY_DIR}/PopCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/PrettySExprs.java
+  ${CMAKE_CURRENT_BINARY_DIR}/Proof.java
+  ${CMAKE_CURRENT_BINARY_DIR}/PropagateRuleCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/PushCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/QueryCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/QuitCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/Rational.java
+  ${CMAKE_CURRENT_BINARY_DIR}/RationalHashFunction.java
+  ${CMAKE_CURRENT_BINARY_DIR}/RealType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/Record.java
+  ${CMAKE_CURRENT_BINARY_DIR}/RecordHashFunction.java
+  ${CMAKE_CURRENT_BINARY_DIR}/RecordUpdate.java
+  ${CMAKE_CURRENT_BINARY_DIR}/RecordUpdateHashFunction.java
+  ${CMAKE_CURRENT_BINARY_DIR}/RecoverableModalException.java
+  ${CMAKE_CURRENT_BINARY_DIR}/RegExpType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/ResetAssertionsCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/ResetCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/ResourceManager.java
+  ${CMAKE_CURRENT_BINARY_DIR}/Result.java
+  ${CMAKE_CURRENT_BINARY_DIR}/RewriteRuleCommand.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__Printer.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__api__Solver.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_InstFormatMode.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_LemmaChannels.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_Listener.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_ListenerCollection__Registration.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_MaybeT_CVC4__Rational_t.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_Type.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpq_class.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpz_class.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__istream.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__mapT_CVC4__Expr_CVC4__Expr_t.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__ostream.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__shared_ptrT_CVC4__SygusPrintCallback_t.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__string.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__unordered_mapT_CVC4__Expr_CVC4__ProofLetCount_CVC4__ExprHashFunction_t.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_CVC4__DatatypeConstructorArg_t.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_CVC4__DatatypeConstructor_t.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__vectorT_CVC4__SygusGTerm_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}/ScopeException.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SelectorType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SetBenchmarkLogicCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SetBenchmarkStatusCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SetExpressionNameCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SetInfoCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SetOptionCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SetType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SetUserAttributeCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SimplifyCommand.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SortConstructorType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SortType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/Statistics.java
+  ${CMAKE_CURRENT_BINARY_DIR}/StatisticsBase.java
+  ${CMAKE_CURRENT_BINARY_DIR}/StringType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SygusGTerm.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SygusPrintCallback.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SymbolTable.java
+  ${CMAKE_CURRENT_BINARY_DIR}/SymbolType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/TesterType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/TheoryId.java
+  ${CMAKE_CURRENT_BINARY_DIR}/Timer.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}/hashmapExpr.java
+  ${CMAKE_CURRENT_BINARY_DIR}/pairStringType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/setOfType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/vectorCommandPtr.java
+  ${CMAKE_CURRENT_BINARY_DIR}/vectorDatatype.java
+  ${CMAKE_CURRENT_BINARY_DIR}/vectorDatatypeType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/vectorExpr.java
+  ${CMAKE_CURRENT_BINARY_DIR}/vectorPairStringType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/vectorSExpr.java
+  ${CMAKE_CURRENT_BINARY_DIR}/vectorString.java
+  ${CMAKE_CURRENT_BINARY_DIR}/vectorType.java
+  ${CMAKE_CURRENT_BINARY_DIR}/vectorUnsignedInt.java
+  ${CMAKE_CURRENT_BINARY_DIR}/vectorVectorExpr.java
+)
+
+add_jar(cvc4jar SOURCES ${gen_java_files} OUTPUT_NAME CVC4)
+add_dependencies(cvc4jar cvc4jni)

diff --git a/src/bindings/python/CMakeLists.txt b/src/bindings/python/CMakeLists.txt
new file mode 100644 (file)
index 0000000..2c2c501
--- /dev/null
+++ b/src/bindings/python/CMakeLists.txt
@@ -0,0 +1,19 @@
+find_package(PythonLibs 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})