From: Mathias Preiner Date: Fri, 24 Aug 2018 19:52:49 +0000 (-0700) Subject: cmake: Add SWIG support + Python and Java bindings. X-Git-Tag: cvc5-1.0.0~4585 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f0260ef80ee8020e6f5ee7cace54be0a568236f0;p=cvc5.git cmake: Add SWIG support + Python and Java bindings. --- diff --git a/CMakeLists.txt b/CMakeLists.txt index 74f223e22..81bbaf533 100644 --- 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 2d8d20962..0a8db038f 100644 --- 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 910b62766..a9032b0d9 100644 --- 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 index 000000000..c3fee67a5 --- /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 index 000000000..2c2c50126 --- /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})