diff options
Diffstat (limited to 'src/api')
-rw-r--r-- | src/api/cpp/cvc5.h | 81 | ||||
-rw-r--r-- | src/api/cpp/cvc5_checks.h | 4 | ||||
-rw-r--r-- | src/api/cpp/cvc5_kind.h | 25 | ||||
-rw-r--r-- | src/api/parsekinds.py | 2 | ||||
-rw-r--r-- | src/api/python/CMakeLists.txt | 42 | ||||
-rw-r--r-- | src/api/python/cvc5.pxd (renamed from src/api/python/cvc4.pxd) | 2 | ||||
-rw-r--r-- | src/api/python/cvc5.pxi (renamed from src/api/python/cvc4.pxi) | 42 | ||||
-rw-r--r-- | src/api/python/genkinds.py.in | 2 | ||||
-rw-r--r-- | src/api/python/pycvc4.pyx | 2 | ||||
-rw-r--r-- | src/api/python/pycvc5.pyx | 2 | ||||
-rw-r--r-- | src/api/python/setup.py.in | 8 |
11 files changed, 107 insertions, 105 deletions
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index c8f1b8d4a..96e287f84 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -13,7 +13,7 @@ * The cvc5 C++ API. */ -#include "cvc4_export.h" +#include "cvc5_export.h" #ifndef CVC5__API__CVC5_H #define CVC5__API__CVC5_H @@ -63,7 +63,7 @@ struct APIStatistics; * Base class for all API exceptions. * If thrown, all API objects may be in an unsafe state. */ -class CVC4_EXPORT CVC5ApiException : public std::exception +class CVC5_EXPORT CVC5ApiException : public std::exception { public: /** @@ -96,7 +96,7 @@ class CVC4_EXPORT CVC5ApiException : public std::exception * A recoverable API exception. * If thrown, API objects can still be used. */ -class CVC4_EXPORT CVC5ApiRecoverableException : public CVC5ApiException +class CVC5_EXPORT CVC5ApiRecoverableException : public CVC5ApiException { public: /** @@ -121,7 +121,7 @@ class CVC4_EXPORT CVC5ApiRecoverableException : public CVC5ApiException /** * Encapsulation of a three-valued solver result, with explanations. */ -class CVC4_EXPORT Result +class CVC5_EXPORT Result { friend class Solver; @@ -230,7 +230,7 @@ class CVC4_EXPORT Result * @param r the result to be serialized to the given output stream * @return the output stream */ -std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_EXPORT; +std::ostream& operator<<(std::ostream& out, const Result& r) CVC5_EXPORT; /** * Serialize an UnknownExplanation to given stream. @@ -239,7 +239,7 @@ std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_EXPORT; * @return the output stream */ std::ostream& operator<<(std::ostream& out, - enum Result::UnknownExplanation e) CVC4_EXPORT; + enum Result::UnknownExplanation e) CVC5_EXPORT; /* -------------------------------------------------------------------------- */ /* Sort */ @@ -250,7 +250,7 @@ class Datatype; /** * The sort of a cvc5 term. */ -class CVC4_EXPORT Sort +class CVC5_EXPORT Sort { friend class cvc5::Command; friend class DatatypeConstructor; @@ -749,12 +749,12 @@ class CVC4_EXPORT Sort * @param s the sort to be serialized to the given output stream * @return the output stream */ -std::ostream& operator<<(std::ostream& out, const Sort& s) CVC4_EXPORT; +std::ostream& operator<<(std::ostream& out, const Sort& s) CVC5_EXPORT; /** * Hash function for Sorts. */ -struct CVC4_EXPORT SortHashFunction +struct CVC5_EXPORT SortHashFunction { size_t operator()(const Sort& s) const; }; @@ -768,7 +768,7 @@ struct CVC4_EXPORT SortHashFunction * An operator is a term that represents certain operators, instantiated * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT. */ -class CVC4_EXPORT Op +class CVC5_EXPORT Op { friend class Solver; friend class Term; @@ -896,7 +896,7 @@ class CVC4_EXPORT Op /** * A cvc5 Term. */ -class CVC4_EXPORT Term +class CVC5_EXPORT Term { friend class cvc5::Command; friend class Datatype; @@ -1285,7 +1285,7 @@ class CVC4_EXPORT Term /** * Hash function for Terms. */ -struct CVC4_EXPORT TermHashFunction +struct CVC5_EXPORT TermHashFunction { size_t operator()(const Term& t) const; }; @@ -1296,7 +1296,7 @@ struct CVC4_EXPORT TermHashFunction * @param t the term to be serialized to the given output stream * @return the output stream */ -std::ostream& operator<<(std::ostream& out, const Term& t) CVC4_EXPORT; +std::ostream& operator<<(std::ostream& out, const Term& t) CVC5_EXPORT; /** * Serialize a vector of terms to given stream. @@ -1305,7 +1305,7 @@ std::ostream& operator<<(std::ostream& out, const Term& t) CVC4_EXPORT; * @return the output stream */ std::ostream& operator<<(std::ostream& out, - const std::vector<Term>& vector) CVC4_EXPORT; + const std::vector<Term>& vector) CVC5_EXPORT; /** * Serialize a set of terms to the given stream. @@ -1314,7 +1314,7 @@ std::ostream& operator<<(std::ostream& out, * @return the output stream */ std::ostream& operator<<(std::ostream& out, - const std::set<Term>& set) CVC4_EXPORT; + const std::set<Term>& set) CVC5_EXPORT; /** * Serialize an unordered_set of terms to the given stream. @@ -1325,7 +1325,7 @@ std::ostream& operator<<(std::ostream& out, */ std::ostream& operator<<(std::ostream& out, const std::unordered_set<Term, TermHashFunction>& - unordered_set) CVC4_EXPORT; + unordered_set) CVC5_EXPORT; /** * Serialize a map of terms to the given stream. @@ -1336,7 +1336,7 @@ std::ostream& operator<<(std::ostream& out, */ template <typename V> std::ostream& operator<<(std::ostream& out, - const std::map<Term, V>& map) CVC4_EXPORT; + const std::map<Term, V>& map) CVC5_EXPORT; /** * Serialize an unordered_map of terms to the given stream. @@ -1348,7 +1348,7 @@ std::ostream& operator<<(std::ostream& out, template <typename V> std::ostream& operator<<(std::ostream& out, const std::unordered_map<Term, V, TermHashFunction>& - unordered_map) CVC4_EXPORT; + unordered_map) CVC5_EXPORT; /** * Serialize an operator to given stream. @@ -1356,12 +1356,12 @@ std::ostream& operator<<(std::ostream& out, * @param t the operator to be serialized to the given output stream * @return the output stream */ -std::ostream& operator<<(std::ostream& out, const Op& t) CVC4_EXPORT; +std::ostream& operator<<(std::ostream& out, const Op& t) CVC5_EXPORT; /** * Hash function for Ops. */ -struct CVC4_EXPORT OpHashFunction +struct CVC5_EXPORT OpHashFunction { size_t operator()(const Op& t) const; }; @@ -1376,7 +1376,7 @@ class DatatypeIterator; /** * A cvc5 datatype constructor declaration. */ -class CVC4_EXPORT DatatypeConstructorDecl +class CVC5_EXPORT DatatypeConstructorDecl { friend class DatatypeDecl; friend class Solver; @@ -1446,7 +1446,7 @@ class Solver; /** * A cvc5 datatype declaration. */ -class CVC4_EXPORT DatatypeDecl +class CVC5_EXPORT DatatypeDecl { friend class DatatypeConstructorArg; friend class Solver; @@ -1550,7 +1550,7 @@ class CVC4_EXPORT DatatypeDecl /** * A cvc5 datatype selector. */ -class CVC4_EXPORT DatatypeSelector +class CVC5_EXPORT DatatypeSelector { friend class DatatypeConstructor; friend class Solver; @@ -1619,7 +1619,7 @@ class CVC4_EXPORT DatatypeSelector /** * A cvc5 datatype constructor. */ -class CVC4_EXPORT DatatypeConstructor +class CVC5_EXPORT DatatypeConstructor { friend class Datatype; friend class Solver; @@ -1846,7 +1846,7 @@ class CVC4_EXPORT DatatypeConstructor /** * A cvc5 datatype. */ -class CVC4_EXPORT Datatype +class CVC5_EXPORT Datatype { friend class Solver; friend class Sort; @@ -2072,7 +2072,7 @@ class CVC4_EXPORT Datatype * @return the output stream */ std::ostream& operator<<(std::ostream& out, - const DatatypeDecl& dtdecl) CVC4_EXPORT; + const DatatypeDecl& dtdecl) CVC5_EXPORT; /** * Serialize a datatype constructor declaration to given stream. @@ -2081,7 +2081,7 @@ std::ostream& operator<<(std::ostream& out, * @return the output stream */ std::ostream& operator<<(std::ostream& out, - const DatatypeConstructorDecl& ctordecl) CVC4_EXPORT; + const DatatypeConstructorDecl& ctordecl) CVC5_EXPORT; /** * Serialize a vector of datatype constructor declarations to given stream. @@ -2092,7 +2092,7 @@ std::ostream& operator<<(std::ostream& out, */ std::ostream& operator<<(std::ostream& out, const std::vector<DatatypeConstructorDecl>& vector) - CVC4_EXPORT; + CVC5_EXPORT; /** * Serialize a datatype to given stream. @@ -2100,7 +2100,7 @@ std::ostream& operator<<(std::ostream& out, * @param dtype the datatype to be serialized to given stream * @return the output stream */ -std::ostream& operator<<(std::ostream& out, const Datatype& dtype) CVC4_EXPORT; +std::ostream& operator<<(std::ostream& out, const Datatype& dtype) CVC5_EXPORT; /** * Serialize a datatype constructor to given stream. @@ -2109,7 +2109,7 @@ std::ostream& operator<<(std::ostream& out, const Datatype& dtype) CVC4_EXPORT; * @return the output stream */ std::ostream& operator<<(std::ostream& out, - const DatatypeConstructor& ctor) CVC4_EXPORT; + const DatatypeConstructor& ctor) CVC5_EXPORT; /** * Serialize a datatype selector to given stream. @@ -2118,7 +2118,7 @@ std::ostream& operator<<(std::ostream& out, * @return the output stream */ std::ostream& operator<<(std::ostream& out, - const DatatypeSelector& stor) CVC4_EXPORT; + const DatatypeSelector& stor) CVC5_EXPORT; /* -------------------------------------------------------------------------- */ /* Grammar */ @@ -2127,7 +2127,7 @@ std::ostream& operator<<(std::ostream& out, /** * A Sygus Grammar. */ -class CVC4_EXPORT Grammar +class CVC5_EXPORT Grammar { friend class cvc5::Command; friend class Solver; @@ -2272,7 +2272,7 @@ class CVC4_EXPORT Grammar * @param g the grammar to be serialized to the given output stream * @return the output stream */ -std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC4_EXPORT; +std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC5_EXPORT; /* -------------------------------------------------------------------------- */ /* Rounding Mode for Floating-Points */ @@ -2292,7 +2292,7 @@ std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC4_EXPORT; * Standard 754. * \endverbatim */ -enum CVC4_EXPORT RoundingMode +enum CVC5_EXPORT RoundingMode { /** * Round to the nearest even number. @@ -2331,7 +2331,7 @@ enum CVC4_EXPORT RoundingMode /** * Hash function for RoundingModes. */ -struct CVC4_EXPORT RoundingModeHashFunction +struct CVC5_EXPORT RoundingModeHashFunction { inline size_t operator()(const RoundingMode& rm) const; }; @@ -2347,7 +2347,7 @@ struct CVC4_EXPORT RoundingModeHashFunction * The value type can be queried (using `isInt`, `isString`, etc.) and * the stored value can be accessed (using `getInt`, `getString`, etc.). */ -class CVC4_EXPORT Stat +class CVC5_EXPORT Stat { struct StatData; @@ -2392,7 +2392,7 @@ class CVC4_EXPORT Stat std::unique_ptr<StatData> d_data; }; -std::ostream& operator<<(std::ostream& os, const Stat& sv) CVC4_EXPORT; +std::ostream& operator<<(std::ostream& os, const Stat& sv) CVC5_EXPORT; /** * Represents a snapshot of the solver statistics. @@ -2407,7 +2407,7 @@ std::ostream& operator<<(std::ostream& os, const Stat& sv) CVC4_EXPORT; * statistics that are expert, unchanged, or both, can be included as well. * A single statistic value is represented as `Stat`. */ -class CVC4_EXPORT Statistics +class CVC5_EXPORT Statistics { public: friend Solver; @@ -2458,7 +2458,8 @@ class CVC4_EXPORT Statistics /** Internal data */ BaseType d_stats; }; -std::ostream& operator<<(std::ostream& out, const Statistics& stats) CVC4_EXPORT; +std::ostream& operator<<(std::ostream& out, + const Statistics& stats) CVC5_EXPORT; /* -------------------------------------------------------------------------- */ /* Solver */ @@ -2467,7 +2468,7 @@ std::ostream& operator<<(std::ostream& out, const Statistics& stats) CVC4_EXPORT /** * A cvc5 solver. */ -class CVC4_EXPORT Solver +class CVC5_EXPORT Solver { friend class Datatype; friend class DatatypeDecl; diff --git a/src/api/cpp/cvc5_checks.h b/src/api/cpp/cvc5_checks.h index d332652fd..c30237ecd 100644 --- a/src/api/cpp/cvc5_checks.h +++ b/src/api/cpp/cvc5_checks.h @@ -20,7 +20,7 @@ #ifndef CVC5__API__CHECKS_H #define CVC5__API__CHECKS_H -namespace cvc4 { +namespace cvc5 { namespace api { /* -------------------------------------------------------------------------- */ @@ -653,5 +653,5 @@ namespace api { } \ } while (0) } // namespace api -} // namespace cvc4 +} // namespace cvc5 #endif diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 86e6d676d..7d0f7b9b7 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -13,7 +13,7 @@ * The term kinds of the cvc5 C++ API. */ -#include "cvc4_export.h" +#include "cvc5_export.h" #ifndef CVC5__API__CVC5_KIND_H #define CVC5__API__CVC5_KIND_H @@ -35,7 +35,7 @@ namespace api { * checks for validity). The size of this type depends on the size of * cvc5::Kind (NodeValue::NBITS_KIND, currently 10 bits, see expr/node_value.h). */ -enum CVC4_EXPORT Kind : int32_t +enum CVC5_EXPORT Kind : int32_t { /** * Internal kind. @@ -185,9 +185,9 @@ enum CVC4_EXPORT Kind : int32_t * (e.g. for arithmetic terms in non-linear queries). However, it is not * supported by the parser. Moreover, the user of the API should be cautious * when using this operator. In general, all witness terms - * `(witness ((x Int)) F)` should be such that `(exists ((x Int)) F)` is a valid - * formula. If this is not the case, then the semantics in formulas that use - * witness terms may be unintuitive. For example, the following formula is + * `(witness ((x Int)) F)` should be such that `(exists ((x Int)) F)` is a + * valid formula. If this is not the case, then the semantics in formulas that + * use witness terms may be unintuitive. For example, the following formula is * unsatisfiable: * `(or (= (witness ((x Int)) false) 0) (not (= (witness ((x Int)) false) 0))` * whereas notice that `(or (= z 0) (not (= z 0)))` is true for any `z`. @@ -393,7 +393,7 @@ enum CVC4_EXPORT Kind : int32_t * - `Solver::mkOp(Kind kind, uint32_t param) const` * * Apply integer conversion to bit-vector. - + * Parameters: * - 1: Op of kind IAND * - 2: Integer term @@ -2341,11 +2341,12 @@ enum CVC4_EXPORT Kind : int32_t * a predicate P[x1...xn], and a term t[x1...xn]. A comprehension C with the * above form has members given by the following semantics: * @f[ - * \forall y. ( \exists x_1...x_n. P[x_1...x_n] \hat{} t[x_1...x_n] = y ) \Leftrightarrow (member y C) + * \forall y. ( \exists x_1...x_n. P[x_1...x_n] \hat{} t[x_1...x_n] = y ) + * \Leftrightarrow (member y C) * @f] * where y ranges over the element type of the (set) type of the - * comprehension. If @f$ t[x_1..x_n] @f$ is not provided, it is equivalent to y in the - * above formula. + * comprehension. If @f$ t[x_1..x_n] @f$ is not provided, it is equivalent to + * y in the above formula. * * Parameters: * - 1: Term BOUND_VAR_LIST @@ -3430,7 +3431,7 @@ enum CVC4_EXPORT Kind : int32_t * @param k the kind * @return the string representation of kind k */ -std::string kindToString(Kind k) CVC4_EXPORT; +std::string kindToString(Kind k) CVC5_EXPORT; /** * Serialize a kind to given stream. @@ -3438,12 +3439,12 @@ std::string kindToString(Kind k) CVC4_EXPORT; * @param k the kind to be serialized to the given output stream * @return the output stream */ -std::ostream& operator<<(std::ostream& out, Kind k) CVC4_EXPORT; +std::ostream& operator<<(std::ostream& out, Kind k) CVC5_EXPORT; /** * Hash function for Kinds. */ -struct CVC4_EXPORT KindHashFunction +struct CVC5_EXPORT KindHashFunction { /** * Hashes a Kind to a size_t. diff --git a/src/api/parsekinds.py b/src/api/parsekinds.py index cb1586995..30f182b02 100644 --- a/src/api/parsekinds.py +++ b/src/api/parsekinds.py @@ -34,7 +34,7 @@ US = '_' NL = '\n' # Enum Declarations -ENUM_START = 'enum CVC4_EXPORT Kind' +ENUM_START = 'enum CVC5_EXPORT Kind' ENUM_END = CCB + SC # Comments and Macro Tokens diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index 4eca7e442..02405a0cc 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -22,11 +22,11 @@ endif() find_package(PythonExtensions REQUIRED) find_package(Cython 0.29 REQUIRED) -# Generate cvc4kinds.{pxd,pyx} +# Generate cvc5kinds.{pxd,pyx} configure_file(genkinds.py.in genkinds.py) set(GENERATED_FILES - "${CMAKE_CURRENT_BINARY_DIR}/cvc4kinds.pxd" - "${CMAKE_CURRENT_BINARY_DIR}/cvc4kinds.pxi" + "${CMAKE_CURRENT_BINARY_DIR}/cvc5kinds.pxd" + "${CMAKE_CURRENT_BINARY_DIR}/cvc5kinds.pxi" ) add_custom_command( OUTPUT @@ -37,58 +37,58 @@ add_custom_command( "${PYTHON_EXECUTABLE}" "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py" --kinds-header "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h" - --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc4kinds" + --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc5kinds" DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py" "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h" ) -add_custom_target(cvc4kinds DEPENDS ${GENERATED_FILES}) +add_custom_target(cvc5kinds DEPENDS ${GENERATED_FILES}) -include_directories(${CMAKE_CURRENT_BINARY_DIR}) # for cvc4kinds.pxi -add_cython_target(pycvc4 CXX) +include_directories(${CMAKE_CURRENT_BINARY_DIR}) # for cvc5kinds.pxi +add_cython_target(pycvc5 CXX) -add_library(pycvc4 +add_library(pycvc5 MODULE - ${pycvc4}) -add_dependencies(pycvc4 cvc4kinds) + ${pycvc5}) +add_dependencies(pycvc5 cvc5kinds) -target_include_directories(pycvc4 +target_include_directories(pycvc5 PRIVATE ${PYTHON_INCLUDE_DIRS} ${PROJECT_SOURCE_DIR}/src # for API headers in src/api/cpp - ${CMAKE_BINARY_DIR}/src # for cvc4_export.h + ${CMAKE_BINARY_DIR}/src # for cvc5_export.h ) -target_link_libraries(pycvc4 cvc4 ${PYTHON_LIBRARIES}) +target_link_libraries(pycvc5 cvc5 ${PYTHON_LIBRARIES}) # Disable -Werror and other warnings for code generated by Cython. # Note: Visibility is reset to default here since otherwise the PyInit_... # function will not be exported correctly # (https://github.com/cython/cython/issues/3380). -set_target_properties(pycvc4 +set_target_properties(pycvc5 PROPERTIES COMPILE_FLAGS "-Wno-error -Wno-shadow -Wno-implicit-fallthrough" CXX_VISIBILITY_PRESET default VISIBILITY_INLINES_HIDDEN 0) -python_extension_module(pycvc4) +python_extension_module(pycvc5) # Installation based on https://bloerg.net/2012/11/10/cmake-and-distutils.html # Create a wrapper python directory and generate a distutils setup.py file configure_file(setup.py.in setup.py) -set(PYCVC5_MODULE "${CMAKE_CURRENT_BINARY_DIR}/pycvc4") +set(PYCVC5_MODULE "${CMAKE_CURRENT_BINARY_DIR}/pycvc5") file(MAKE_DIRECTORY "${PYCVC5_MODULE}") file(WRITE ${PYCVC5_MODULE}/__init__.py "import sys -from .pycvc4 import * -# fake a submodule for dotted imports, e.g. from pycvc4.kinds import * +from .pycvc5 import * +# fake a submodule for dotted imports, e.g. from pycvc5.kinds import * sys.modules['%s.%s'%(__name__, kinds.__name__)] = kinds") -set(PYCVC5_LOC "${PYCVC5_MODULE}/$<TARGET_FILE_NAME:pycvc4>") -add_custom_command(TARGET pycvc4 POST_BUILD - COMMAND ${CMAKE_COMMAND} -E rename $<TARGET_FILE:pycvc4> ${PYCVC5_LOC} +set(PYCVC5_LOC "${PYCVC5_MODULE}/$<TARGET_FILE_NAME:pycvc5>") +add_custom_command(TARGET pycvc5 POST_BUILD + COMMAND ${CMAKE_COMMAND} -E rename $<TARGET_FILE:pycvc5> ${PYCVC5_LOC} ) # figure out if we're in a virtualenv diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc5.pxd index 336def3dc..83d811a1d 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc5.pxd @@ -5,7 +5,7 @@ from libcpp.set cimport set from libcpp.string cimport string from libcpp.vector cimport vector from libcpp.pair cimport pair -from cvc4kinds cimport Kind +from cvc5kinds cimport Kind cdef extern from "<iostream>" namespace "std": diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc5.pxi index 48921dc87..0ee56cd55 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc5.pxi @@ -9,27 +9,27 @@ from libcpp.set cimport set from libcpp.string cimport string from libcpp.vector cimport vector -from cvc4 cimport cout -from cvc4 cimport Datatype as c_Datatype -from cvc4 cimport DatatypeConstructor as c_DatatypeConstructor -from cvc4 cimport DatatypeConstructorDecl as c_DatatypeConstructorDecl -from cvc4 cimport DatatypeDecl as c_DatatypeDecl -from cvc4 cimport DatatypeSelector as c_DatatypeSelector -from cvc4 cimport Result as c_Result -from cvc4 cimport RoundingMode as c_RoundingMode -from cvc4 cimport Op as c_Op -from cvc4 cimport OpHashFunction as c_OpHashFunction -from cvc4 cimport Solver as c_Solver -from cvc4 cimport Grammar as c_Grammar -from cvc4 cimport Sort as c_Sort -from cvc4 cimport SortHashFunction as c_SortHashFunction -from cvc4 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE -from cvc4 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO -from cvc4 cimport ROUND_NEAREST_TIES_TO_AWAY -from cvc4 cimport Term as c_Term -from cvc4 cimport TermHashFunction as c_TermHashFunction - -from cvc4kinds cimport Kind as c_Kind +from cvc5 cimport cout +from cvc5 cimport Datatype as c_Datatype +from cvc5 cimport DatatypeConstructor as c_DatatypeConstructor +from cvc5 cimport DatatypeConstructorDecl as c_DatatypeConstructorDecl +from cvc5 cimport DatatypeDecl as c_DatatypeDecl +from cvc5 cimport DatatypeSelector as c_DatatypeSelector +from cvc5 cimport Result as c_Result +from cvc5 cimport RoundingMode as c_RoundingMode +from cvc5 cimport Op as c_Op +from cvc5 cimport OpHashFunction as c_OpHashFunction +from cvc5 cimport Solver as c_Solver +from cvc5 cimport Grammar as c_Grammar +from cvc5 cimport Sort as c_Sort +from cvc5 cimport SortHashFunction as c_SortHashFunction +from cvc5 cimport ROUND_NEAREST_TIES_TO_EVEN, ROUND_TOWARD_POSITIVE +from cvc5 cimport ROUND_TOWARD_NEGATIVE, ROUND_TOWARD_ZERO +from cvc5 cimport ROUND_NEAREST_TIES_TO_AWAY +from cvc5 cimport Term as c_Term +from cvc5 cimport TermHashFunction as c_TermHashFunction + +from cvc5kinds cimport Kind as c_Kind ################################## DECORATORS ################################# def expand_list_arg(num_req_args=0): diff --git a/src/api/python/genkinds.py.in b/src/api/python/genkinds.py.in index a78372e71..8c8de35ac 100644 --- a/src/api/python/genkinds.py.in +++ b/src/api/python/genkinds.py.in @@ -56,7 +56,7 @@ KINDS_PXI_TOP = \ r"""# distutils: language = c++ # distutils: extra_compile_args = -std=c++11 -from cvc4kinds cimport * +from cvc5kinds cimport * import sys from types import ModuleType diff --git a/src/api/python/pycvc4.pyx b/src/api/python/pycvc4.pyx deleted file mode 100644 index 40766341a..000000000 --- a/src/api/python/pycvc4.pyx +++ /dev/null @@ -1,2 +0,0 @@ -include "cvc4kinds.pxi" -include "cvc4.pxi" diff --git a/src/api/python/pycvc5.pyx b/src/api/python/pycvc5.pyx new file mode 100644 index 000000000..f09300265 --- /dev/null +++ b/src/api/python/pycvc5.pyx @@ -0,0 +1,2 @@ +include "cvc5kinds.pxi" +include "cvc5.pxi" diff --git a/src/api/python/setup.py.in b/src/api/python/setup.py.in index 8919dd3f1..231f27c2a 100644 --- a/src/api/python/setup.py.in +++ b/src/api/python/setup.py.in @@ -35,9 +35,9 @@ class PyCVC5Install(install): c.finalize_options() c.run() -setup(name='pycvc4', +setup(name='pycvc5', version='${CVC5_MAJOR}.${CVC5_MINOR}.${CVC5_RELEASE}', - packages=['pycvc4'], - package_dir={'pycvc4': '${CMAKE_CURRENT_BINARY_DIR}/pycvc4'}, - package_data={'pycvc4': ['pycvc4.so']}, + packages=['pycvc5'], + package_dir={'pycvc5': '${CMAKE_CURRENT_BINARY_DIR}/pycvc5'}, + package_data={'pycvc5': ['pycvc5.so']}, cmdclass={'install': PyCVC5Install}) |