diff options
Diffstat (limited to 'src')
89 files changed, 584 insertions, 563 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 554739b98..ebe52a2db 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -13,8 +13,8 @@ # The build system configuration. ## -# Collect libcvc4 source files -libcvc4_add_sources( +# Collect libcvc5 source files +libcvc5_add_sources( api/cpp/cvc5.cpp api/cpp/cvc5.h api/cpp/cvc5_checks.h @@ -1107,76 +1107,76 @@ add_subdirectory(theory) add_subdirectory(util) #-----------------------------------------------------------------------------# -# All sources for libcvc4 are now collected in LIBCVC4_SRCS and (if generated) -# LIBCVC4_GEN_SRCS (via libcvc4_add_sources). We can now build libcvc4. +# All sources for libcvc5 are now collected in LIBCVC5_SRCS and (if generated) +# LIBCVC5_GEN_SRCS (via libcvc5_add_sources). We can now build libcvc5. -set_source_files_properties(${LIBCVC4_GEN_SRCS} PROPERTIES GENERATED TRUE) -add_library(cvc4 ${LIBCVC4_SRCS} ${LIBCVC4_GEN_SRCS} - $<TARGET_OBJECTS:cvc4base> $<TARGET_OBJECTS:cvc4context>) -target_include_directories(cvc4 +set_source_files_properties(${LIBCVC5_GEN_SRCS} PROPERTIES GENERATED TRUE) +add_library(cvc5 ${LIBCVC5_SRCS} ${LIBCVC5_GEN_SRCS} + $<TARGET_OBJECTS:cvc5base> $<TARGET_OBJECTS:cvc5context>) +target_include_directories(cvc5 PUBLIC $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}> $<INSTALL_INTERFACE:include> ) include(GenerateExportHeader) -generate_export_header(cvc4) +generate_export_header(cvc5) -install(TARGETS cvc4 - EXPORT cvc4-targets +install(TARGETS cvc5 + EXPORT cvc5-targets LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR} ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR}) -set_target_properties(cvc4 PROPERTIES SOVERSION ${CVC5_SOVERSION}) -target_compile_definitions(cvc4 PRIVATE -D__BUILDING_CVC4LIB) -# Add libcvc4 dependencies for generated sources. -add_dependencies(cvc4 gen-expr gen-gitinfo gen-options gen-tags gen-theory) +set_target_properties(cvc5 PROPERTIES SOVERSION ${CVC5_SOVERSION}) +target_compile_definitions(cvc5 PRIVATE -D__BUILDING_CVC5LIB) +# Add libcvc5 dependencies for generated sources. +add_dependencies(cvc5 gen-expr gen-gitinfo gen-options gen-tags gen-theory) # Add library/include dependencies if(ENABLE_VALGRIND) - target_include_directories(cvc4 PRIVATE ${Valgrind_INCLUDE_DIR}) + target_include_directories(cvc5 PRIVATE ${Valgrind_INCLUDE_DIR}) endif() if(USE_ABC) - target_link_libraries(cvc4 PRIVATE ${ABC_LIBRARIES}) - target_include_directories(cvc4 PRIVATE ${ABC_INCLUDE_DIR}) + target_link_libraries(cvc5 PRIVATE ${ABC_LIBRARIES}) + target_include_directories(cvc5 PRIVATE ${ABC_INCLUDE_DIR}) endif() if(USE_CADICAL) - target_link_libraries(cvc4 PRIVATE CaDiCaL) + target_link_libraries(cvc5 PRIVATE CaDiCaL) endif() if(USE_CLN) - target_link_libraries(cvc4 PRIVATE CLN) + target_link_libraries(cvc5 PRIVATE CLN) endif() if(USE_CRYPTOMINISAT) - target_link_libraries(cvc4 PRIVATE CryptoMiniSat) + target_link_libraries(cvc5 PRIVATE CryptoMiniSat) endif() if(USE_KISSAT) - target_link_libraries(cvc4 PRIVATE Kissat) + target_link_libraries(cvc5 PRIVATE Kissat) endif() if(USE_GLPK) - target_link_libraries(cvc4 PRIVATE ${GLPK_LIBRARIES}) - target_include_directories(cvc4 PRIVATE ${GLPK_INCLUDE_DIR}) + target_link_libraries(cvc5 PRIVATE ${GLPK_LIBRARIES}) + target_include_directories(cvc5 PRIVATE ${GLPK_INCLUDE_DIR}) endif() if(USE_POLY) - target_link_libraries(cvc4 PRIVATE Polyxx) + target_link_libraries(cvc5 PRIVATE Polyxx) endif() if(USE_SYMFPU) - target_link_libraries(cvc4 PRIVATE SymFPU) + target_link_libraries(cvc5 PRIVATE SymFPU) endif() # Note: When linked statically GMP needs to be linked after CLN since CLN # depends on GMP. -target_link_libraries(cvc4 PRIVATE GMP) +target_link_libraries(cvc5 PRIVATE GMP) # Add rt library # Note: For glibc < 2.17 we have to additionally link against rt (man clock_gettime). # RT_LIBRARIES should be empty for glibc >= 2.17 -target_link_libraries(cvc4 PRIVATE ${RT_LIBRARIES}) +target_link_libraries(cvc5 PRIVATE ${RT_LIBRARIES}) #-----------------------------------------------------------------------------# -# Visit main subdirectory after creating target cvc4. For target main, we have +# Visit main subdirectory after creating target cvc5. For target main, we have # to manually add library dependencies since we can't use # target_link_libraries(...) with object libraries for cmake versions <= 3.12. -# Thus, we can only visit main as soon as all dependencies for cvc4 are set up. +# Thus, we can only visit main as soon as all dependencies for cvc5 are set up. if (NOT BUILD_LIB_ONLY) add_subdirectory(main) @@ -1191,7 +1191,7 @@ install(FILES DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}/cvc5/) install(FILES - ${CMAKE_CURRENT_BINARY_DIR}/cvc4_export.h + ${CMAKE_CURRENT_BINARY_DIR}/cvc5_export.h DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}/cvc5/) 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}) diff --git a/src/base/CMakeLists.txt b/src/base/CMakeLists.txt index 5da1216d0..cb4ba64a8 100644 --- a/src/base/CMakeLists.txt +++ b/src/base/CMakeLists.txt @@ -21,6 +21,10 @@ add_custom_target(gen-gitinfo BYPRODUCTS ${CMAKE_CURRENT_BINARY_DIR}/git_versioninfo.cpp COMMAND ${CMAKE_COMMAND} -DGIT_FOUND=${GIT_FOUND} -P GitInfo.cmake) + +# Generate cvc5config.h header +configure_file(cvc5config.h.in cvc5config.h) + #-----------------------------------------------------------------------------# set(LIBBASE_SOURCES @@ -79,8 +83,8 @@ set_source_files_properties( PROPERTIES GENERATED TRUE ) -add_library(cvc4base OBJECT ${LIBBASE_SOURCES}) +add_library(cvc5base OBJECT ${LIBBASE_SOURCES}) if(ENABLE_SHARED) - set_target_properties(cvc4base PROPERTIES POSITION_INDEPENDENT_CODE ON) + set_target_properties(cvc5base PROPERTIES POSITION_INDEPENDENT_CODE ON) endif() -target_compile_definitions(cvc4base PRIVATE -D__BUILDING_CVC4LIB) +target_compile_definitions(cvc5base PRIVATE -D__BUILDING_CVC5LIB) diff --git a/src/base/check.h b/src/base/check.h index 5c7b7c9ed..be9de7d29 100644 --- a/src/base/check.h +++ b/src/base/check.h @@ -37,18 +37,7 @@ #include <ostream> #include "base/exception.h" -#include "cvc4_export.h" - -// Define CVC5_NO_RETURN macro replacement for [[noreturn]]. -#if defined(SWIG) -#define CVC5_NO_RETURN -// SWIG does not yet support [[noreturn]] so emit nothing instead. -#else -#define CVC5_NO_RETURN [[noreturn]] -// Not checking for whether the compiler supports [[noreturn]] using -// __has_cpp_attribute as GCC 4.8 is too widespread and does not support this. -// We instead assume this is C++11 (or later) and [[noreturn]] is available. -#endif // defined(SWIG) +#include "cvc5_export.h" // Define CVC5_PREDICT_FALSE(x) that helps the compiler predict that x will be // false (if there is compiler support). @@ -91,11 +80,11 @@ namespace cvc5 { // Class that provides an ostream and whose destructor aborts! Direct usage of // this class is discouraged. -class CVC4_EXPORT FatalStream +class CVC5_EXPORT FatalStream { public: FatalStream(const char* function, const char* file, int line); - CVC5_NO_RETURN ~FatalStream(); + [[noreturn]] ~FatalStream(); std::ostream& stream(); diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp index c78edbb9b..80d5bac57 100644 --- a/src/base/configuration.cpp +++ b/src/base/configuration.cpp @@ -21,8 +21,8 @@ #include <sstream> #include <string> -#include "cvc4autoconfig.h" #include "base/configuration_private.h" +#include "base/cvc5config.h" #if defined(CVC5_DEBUG) && defined(CVC5_TRACING) # include "base/Debug_tags.h" diff --git a/src/base/configuration.h b/src/base/configuration.h index 5a5109ab2..78e86f920 100644 --- a/src/base/configuration.h +++ b/src/base/configuration.h @@ -21,14 +21,14 @@ #include <string> -#include "cvc4_export.h" +#include "cvc5_export.h" namespace cvc5 { /** * Represents the (static) configuration of cvc5. */ -class CVC4_EXPORT Configuration +class CVC5_EXPORT Configuration { private: /** Private default ctor: Disallow construction of this class */ diff --git a/src/base/cvc5config.h.in b/src/base/cvc5config.h.in new file mode 100644 index 000000000..a824a9c1f --- /dev/null +++ b/src/base/cvc5config.h.in @@ -0,0 +1,75 @@ +#ifndef CVC5__BASE__CVC5CONFIG_H +#define CVC5__BASE__CVC5CONFIG_H + +/* Major component of the version of cvc5. */ +#define CVC5_MAJOR @CVC5_MAJOR@ + +/* Minor component of the version of cvc5. */ +#define CVC5_MINOR @CVC5_MINOR@ + +/* Release component of the version of cvc5. */ +#define CVC5_RELEASE @CVC5_RELEASE@ + +/* Extraversion component of the version of cvc5. */ +#define CVC5_EXTRAVERSION "@CVC5_EXTRAVERSION@" + +/* Full release string for cvc5. */ +#define CVC5_RELEASE_STRING "@CVC5_RELEASE_STRING@" + +/* Full name of this package. */ +#define CVC5_PACKAGE_NAME "@CVC5_PACKAGE_NAME@" + +/* Define to 1 if cvc5 is built with (optional) GPLed library dependencies. */ +#cmakedefine01 CVC5_GPL_DEPS + +/* Define to use the CLN multi-precision arithmetic library. */ +#cmakedefine CVC5_CLN_IMP + +/* Define to use the GMP multi-precision arithmetic library. */ +#cmakedefine CVC5_GMP_IMP + +/* Define to use the libpoly polynomial library. */ +#cmakedefine CVC5_POLY_IMP + +/* Define to 1 if Boost threading library has support for thread attributes. */ +#cmakedefine01 BOOST_HAS_THREAD_ATTR + +/* Define if `clock_gettime' is supported by the platform. */ +#cmakedefine HAVE_CLOCK_GETTIME + +/* Define to 1 if the declaration of `optreset' is available. */ +#cmakedefine01 HAVE_DECL_OPTRESET + +/* Define to 1 if the <ext/stdio_filebuf.h> header file is available. */ +#cmakedefine01 HAVE_EXT_STDIO_FILEBUF_H + +/* Define if `ffs' is supported by the platform. */ +#cmakedefine HAVE_FFS + +/* Define to 1 to use libedit. */ +#cmakedefine01 HAVE_LIBEDITLINE + +/* Define to 1 if `rl_completion_entry_function' returns (char *). */ +#cmakedefine01 EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP + +/* Define if `sigaltstack' is supported by the platform. */ +#cmakedefine HAVE_SIGALTSTACK + +/* Define to 1 if `strerror_r' is supported by the platform. */ +#cmakedefine01 HAVE_STRERROR_R + +/* Define if `strtok_r' is supported by the platform. */ +#cmakedefine HAVE_STRTOK_R + +/* Define if `setitimer` is supported by the platform. */ +#cmakedefine01 HAVE_SETITIMER + +/* Define to 1 if the <unistd.h> header file is available. */ +#cmakedefine01 HAVE_UNISTD_H + +/* Define to 1 if `strerror_r' returns (char *). */ +#cmakedefine01 STRERROR_R_CHAR_P + +#cmakedefine01 CVC5_STATIC_BUILD + +#endif /* __CVC5__CVC5AUTOCONFIG_H */ diff --git a/src/base/exception.h b/src/base/exception.h index ac97bdb2d..6b692abd9 100644 --- a/src/base/exception.h +++ b/src/base/exception.h @@ -22,7 +22,7 @@ #include <iosfwd> #include <string> -#include "cvc4_export.h" +#include "cvc5_export.h" namespace cvc5 { @@ -70,7 +70,7 @@ class Exception : public std::exception }; /* class Exception */ -class CVC4_EXPORT IllegalArgumentException : public Exception +class CVC5_EXPORT IllegalArgumentException : public Exception { protected: IllegalArgumentException() : Exception() {} @@ -137,7 +137,7 @@ inline void CheckArgument(bool cond, const T& arg CVC5_UNUSED) } } -class CVC4_EXPORT LastExceptionBuffer +class CVC5_EXPORT LastExceptionBuffer { public: LastExceptionBuffer(); diff --git a/src/base/output.cpp b/src/base/output.cpp index d894add40..a4003efd0 100644 --- a/src/base/output.cpp +++ b/src/base/output.cpp @@ -26,10 +26,10 @@ namespace cvc5 { null_streambuf null_sb; ostream null_os(&null_sb); -NullC nullCvc4Stream; +NullC nullStream; -const std::string CVC5ostream::s_tab = " "; -const int CVC5ostream::s_indentIosIndex = ios_base::xalloc(); +const std::string Cvc5ostream::s_tab = " "; +const int Cvc5ostream::s_indentIosIndex = ios_base::xalloc(); DebugC DebugChannel(&cout); WarningC WarningChannel(&cerr); diff --git a/src/base/output.h b/src/base/output.h index 9d4b4389f..c0dbb3d7c 100644 --- a/src/base/output.h +++ b/src/base/output.h @@ -25,13 +25,13 @@ #include <string> #include <utility> -#include "cvc4_export.h" +#include "cvc5_export.h" namespace cvc5 { template <class T, class U> std::ostream& operator<<(std::ostream& out, - const std::pair<T, U>& p) CVC4_EXPORT; + const std::pair<T, U>& p) CVC5_EXPORT; template <class T, class U> std::ostream& operator<<(std::ostream& out, const std::pair<T, U>& p) { @@ -58,9 +58,9 @@ class null_streambuf : public std::streambuf /** A null stream-buffer singleton */ extern null_streambuf null_sb; /** A null output stream singleton */ -extern std::ostream null_os CVC4_EXPORT; +extern std::ostream null_os CVC5_EXPORT; -class CVC4_EXPORT CVC5ostream +class CVC5_EXPORT Cvc5ostream { static const std::string s_tab; static const int s_indentIosIndex; @@ -74,11 +74,11 @@ class CVC4_EXPORT CVC5ostream std::ostream& (*const d_endl)(std::ostream&); // do not allow use - CVC5ostream& operator=(const CVC5ostream&); + Cvc5ostream& operator=(const Cvc5ostream&); public: - CVC5ostream() : d_os(NULL), d_firstColumn(false), d_endl(&std::endl) {} - explicit CVC5ostream(std::ostream* os) + Cvc5ostream() : d_os(NULL), d_firstColumn(false), d_endl(&std::endl) {} + explicit Cvc5ostream(std::ostream* os) : d_os(os), d_firstColumn(true), d_endl(&std::endl) { } @@ -97,7 +97,7 @@ class CVC4_EXPORT CVC5ostream } } - CVC5ostream& flush() + Cvc5ostream& flush() { if(d_os != NULL) { d_os->flush(); @@ -111,10 +111,10 @@ class CVC4_EXPORT CVC5ostream std::ostream* getStreamPointer() const { return d_os; } template <class T> - CVC5ostream& operator<<(T const& t) CVC4_EXPORT; + Cvc5ostream& operator<<(T const& t) CVC5_EXPORT; // support manipulators, endl, etc.. - CVC5ostream& operator<<(std::ostream& (*pf)(std::ostream&)) + Cvc5ostream& operator<<(std::ostream& (*pf)(std::ostream&)) { if(d_os != NULL) { d_os = &(*d_os << pf); @@ -125,40 +125,40 @@ class CVC4_EXPORT CVC5ostream } return *this; } - CVC5ostream& operator<<(std::ios& (*pf)(std::ios&)) + Cvc5ostream& operator<<(std::ios& (*pf)(std::ios&)) { if(d_os != NULL) { d_os = &(*d_os << pf); } return *this; } - CVC5ostream& operator<<(std::ios_base& (*pf)(std::ios_base&)) + Cvc5ostream& operator<<(std::ios_base& (*pf)(std::ios_base&)) { if(d_os != NULL) { d_os = &(*d_os << pf); } return *this; } - CVC5ostream& operator<<(CVC5ostream& (*pf)(CVC5ostream&)) + Cvc5ostream& operator<<(Cvc5ostream& (*pf)(Cvc5ostream&)) { return pf(*this); } -}; /* class CVC5ostream */ +}; /* class Cvc5ostream */ -inline CVC5ostream& push(CVC5ostream& stream) +inline Cvc5ostream& push(Cvc5ostream& stream) { stream.pushIndent(); return stream; } -inline CVC5ostream& pop(CVC5ostream& stream) +inline Cvc5ostream& pop(Cvc5ostream& stream) { stream.popIndent(); return stream; } template <class T> -CVC5ostream& CVC5ostream::operator<<(T const& t) +Cvc5ostream& Cvc5ostream::operator<<(T const& t) { if(d_os != NULL) { if(d_firstColumn) { @@ -182,11 +182,11 @@ class NullC { public: operator bool() const { return false; } - operator CVC5ostream() const { return CVC5ostream(); } + operator Cvc5ostream() const { return Cvc5ostream(); } operator std::ostream&() const { return null_os; } }; /* class NullC */ -extern NullC nullCvc4Stream CVC4_EXPORT; +extern NullC nullStream CVC5_EXPORT; /** The debug output class */ class DebugC @@ -197,12 +197,12 @@ class DebugC public: explicit DebugC(std::ostream* os) : d_os(os) {} - CVC5ostream operator()(const std::string& tag) const + Cvc5ostream operator()(const std::string& tag) const { if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { - return CVC5ostream(d_os); + return Cvc5ostream(d_os); } else { - return CVC5ostream(); + return Cvc5ostream(); } } @@ -237,7 +237,7 @@ class WarningC public: explicit WarningC(std::ostream* os) : d_os(os) {} - CVC5ostream operator()() const { return CVC5ostream(d_os); } + Cvc5ostream operator()() const { return Cvc5ostream(d_os); } std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; } std::ostream& getStream() const { return *d_os; } @@ -271,7 +271,7 @@ class MessageC public: explicit MessageC(std::ostream* os) : d_os(os) {} - CVC5ostream operator()() const { return CVC5ostream(d_os); } + Cvc5ostream operator()() const { return Cvc5ostream(d_os); } std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; } std::ostream& getStream() const { return *d_os; } @@ -288,7 +288,7 @@ class NoticeC public: explicit NoticeC(std::ostream* os) : d_os(os) {} - CVC5ostream operator()() const { return CVC5ostream(d_os); } + Cvc5ostream operator()() const { return Cvc5ostream(d_os); } std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; } std::ostream& getStream() const { return *d_os; } @@ -305,7 +305,7 @@ class ChatC public: explicit ChatC(std::ostream* os) : d_os(os) {} - CVC5ostream operator()() const { return CVC5ostream(d_os); } + Cvc5ostream operator()() const { return Cvc5ostream(d_os); } std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; } std::ostream& getStream() const { return *d_os; } @@ -323,12 +323,12 @@ class TraceC public: explicit TraceC(std::ostream* os) : d_os(os) {} - CVC5ostream operator()(std::string tag) const + Cvc5ostream operator()(std::string tag) const { if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { - return CVC5ostream(d_os); + return Cvc5ostream(d_os); } else { - return CVC5ostream(); + return Cvc5ostream(); } } @@ -370,12 +370,12 @@ public: explicit DumpOutC(std::ostream* os) : d_os(os) {} - CVC5ostream operator()(std::string tag) + Cvc5ostream operator()(std::string tag) { if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) { - return CVC5ostream(d_os); + return Cvc5ostream(d_os); } else { - return CVC5ostream(); + return Cvc5ostream(); } } @@ -399,74 +399,66 @@ public: }; /* class DumpOutC */ /** The debug output singleton */ -extern DebugC DebugChannel CVC4_EXPORT; +extern DebugC DebugChannel CVC5_EXPORT; /** The warning output singleton */ -extern WarningC WarningChannel CVC4_EXPORT; +extern WarningC WarningChannel CVC5_EXPORT; /** The message output singleton */ -extern MessageC MessageChannel CVC4_EXPORT; +extern MessageC MessageChannel CVC5_EXPORT; /** The notice output singleton */ -extern NoticeC NoticeChannel CVC4_EXPORT; +extern NoticeC NoticeChannel CVC5_EXPORT; /** The chat output singleton */ -extern ChatC ChatChannel CVC4_EXPORT; +extern ChatC ChatChannel CVC5_EXPORT; /** The trace output singleton */ -extern TraceC TraceChannel CVC4_EXPORT; +extern TraceC TraceChannel CVC5_EXPORT; /** The dump output singleton */ -extern DumpOutC DumpOutChannel CVC4_EXPORT; +extern DumpOutC DumpOutChannel CVC5_EXPORT; #ifdef CVC5_MUZZLE -#define Debug \ - ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::DebugChannel +#define Debug ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DebugChannel #define Warning \ - ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::WarningChannel + ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::WarningChannel #define WarningOnce \ - ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::WarningChannel + ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::WarningChannel #define CVC5Message \ - ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::MessageChannel + ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::MessageChannel #define Notice \ - ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::NoticeChannel -#define Chat \ - ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::ChatChannel -#define Trace \ - ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::TraceChannel + ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::NoticeChannel +#define Chat ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::ChatChannel +#define Trace ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::TraceChannel #define DumpOut \ - ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::DumpOutChannel + ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DumpOutChannel #else /* CVC5_MUZZLE */ #if defined(CVC5_DEBUG) && defined(CVC5_TRACING) #define Debug ::cvc5::DebugChannel #else /* CVC5_DEBUG && CVC5_TRACING */ -#define Debug \ - ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::DebugChannel +#define Debug ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DebugChannel #endif /* CVC5_DEBUG && CVC5_TRACING */ -#define Warning \ - (!::cvc5::WarningChannel.isOn()) ? ::cvc5::nullCvc4Stream \ - : ::cvc5::WarningChannel +#define Warning \ + (!::cvc5::WarningChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::WarningChannel #define WarningOnce \ (!::cvc5::WarningChannel.isOn() \ || !::cvc5::WarningChannel.warnOnce(__FILE__, __LINE__)) \ - ? ::cvc5::nullCvc4Stream \ + ? ::cvc5::nullStream \ : ::cvc5::WarningChannel -#define CVC5Message \ - (!::cvc5::MessageChannel.isOn()) ? ::cvc5::nullCvc4Stream \ - : ::cvc5::MessageChannel -#define Notice \ - (!::cvc5::NoticeChannel.isOn()) ? ::cvc5::nullCvc4Stream \ - : ::cvc5::NoticeChannel +#define CVC5Message \ + (!::cvc5::MessageChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::MessageChannel +#define Notice \ + (!::cvc5::NoticeChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::NoticeChannel #define Chat \ - (!::cvc5::ChatChannel.isOn()) ? ::cvc5::nullCvc4Stream : ::cvc5::ChatChannel + (!::cvc5::ChatChannel.isOn()) ? ::cvc5::nullStream : ::cvc5::ChatChannel #ifdef CVC5_TRACING #define Trace ::cvc5::TraceChannel #else /* CVC5_TRACING */ -#define Trace \ - ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::TraceChannel +#define Trace ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::TraceChannel #endif /* CVC5_TRACING */ #ifdef CVC5_DUMPING #define DumpOut ::cvc5::DumpOutChannel #else /* CVC5_DUMPING */ #define DumpOut \ - ::cvc5::__cvc4_true() ? ::cvc5::nullCvc4Stream : ::cvc5::DumpOutChannel + ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DumpOutChannel #endif /* CVC5_DUMPING */ #endif /* CVC5_MUZZLE */ @@ -475,7 +467,8 @@ extern DumpOutC DumpOutChannel CVC4_EXPORT; // because the ! will apply before the ? . // If a compiler error has directed you here, // just parenthesize it e.g. !(Debug("foo").isOn()) -class __cvc4_true { +class __cvc5_true +{ void operator!() CVC5_UNUSED; void operator~() CVC5_UNUSED; void operator-() CVC5_UNUSED; @@ -483,7 +476,7 @@ class __cvc4_true { public: inline operator bool() { return true; } -};/* __cvc4_true */ +}; /* __cvc5_true */ #if defined(CVC5_DEBUG) && defined(CVC5_TRACING) @@ -569,21 +562,21 @@ class ScopedTrace */ class IndentedScope { - CVC5ostream d_out; + Cvc5ostream d_out; public: - inline IndentedScope(CVC5ostream out); + inline IndentedScope(Cvc5ostream out); inline ~IndentedScope(); }; /* class IndentedScope */ #if defined(CVC5_DEBUG) && defined(CVC5_TRACING) -inline IndentedScope::IndentedScope(CVC5ostream out) : d_out(out) +inline IndentedScope::IndentedScope(Cvc5ostream out) : d_out(out) { d_out << push; } inline IndentedScope::~IndentedScope() { d_out << pop; } #else /* CVC5_DEBUG && CVC5_TRACING */ -inline IndentedScope::IndentedScope(CVC5ostream out) {} +inline IndentedScope::IndentedScope(Cvc5ostream out) {} inline IndentedScope::~IndentedScope() {} #endif /* CVC5_DEBUG && CVC5_TRACING */ diff --git a/src/context/CMakeLists.txt b/src/context/CMakeLists.txt index fb1d25111..73166462c 100644 --- a/src/context/CMakeLists.txt +++ b/src/context/CMakeLists.txt @@ -34,8 +34,8 @@ set(LIBCONTEXT_SOURCES context_mm.h ) -add_library(cvc4context OBJECT ${LIBCONTEXT_SOURCES}) +add_library(cvc5context OBJECT ${LIBCONTEXT_SOURCES}) if(ENABLE_SHARED) - set_target_properties(cvc4context PROPERTIES POSITION_INDEPENDENT_CODE ON) + set_target_properties(cvc5context PROPERTIES POSITION_INDEPENDENT_CODE ON) endif() -target_compile_definitions(cvc4context PRIVATE -D__BUILDING_CVC4LIB) +target_compile_definitions(cvc5context PRIVATE -D__BUILDING_CVC5LIB) diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 17bd49ea7..28cf23f57 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -13,7 +13,7 @@ # The build system configuration. ## -libcvc4_add_sources( +libcvc5_add_sources( array_store_all.cpp array_store_all.h ascription_type.cpp @@ -124,7 +124,7 @@ libcvc4_add_sources( uninterpreted_constant.h ) -libcvc4_add_sources(GENERATED +libcvc5_add_sources(GENERATED kind.cpp kind.h metakind.cpp diff --git a/src/expr/node.h b/src/expr/node.h index 9014016b9..5480b38ae 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -126,7 +126,7 @@ typedef NodeTemplate<true> Node; * * More guidelines on when to use TNodes is available in the cvc5 * Developer's Guide: - * http://cvc4.cs.stanford.edu/wiki/Developer%27s_Guide#Dealing_with_expressions_.28Nodes_and_TNodes.29 + * https://github.com/CVC4/CVC4/wiki/Developer-Guide#dealing-with-expressions-nodes-and-tnodes */ typedef NodeTemplate<false> TNode; @@ -389,20 +389,6 @@ public: return NodeTemplate(d_nv->getChild(i)); } - /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance).. - * - * It has been decided for now to hold off on implementations of - * these functions, as they may only be needed in CNF conversion, - * where it's pointless to do a lazy isAtomic determination by - * searching through the DAG, and storing it, since the result will - * only be used once. For more details see the 4/27/2010 cvc5 - * developer's meeting notes at: - * - * http://cvc4.cs.stanford.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29 - */ - // bool containsDecision(); // is "atomic" - // bool properlyContainsDecision(); // maybe not atomic but all children are - /** * Returns true if this node represents a constant * @return true if const diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 42be16742..70f221091 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -708,7 +708,7 @@ TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vecto if( index==types.size() ){ if( d_data.isNull() ){ std::stringstream sst; - sst << "__cvc4_tuple"; + sst << "__cvc5_tuple"; for (unsigned i = 0; i < types.size(); ++ i) { sst << "_" << types[i]; } @@ -738,7 +738,7 @@ TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Recor { if( d_data.isNull() ){ std::stringstream sst; - sst << "__cvc4_record"; + sst << "__cvc5_record"; for (const std::pair<std::string, TypeNode>& i : rec) { sst << "_" << i.first << "_" << i.second; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 528cdcfc7..6cda50075 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -338,20 +338,6 @@ class NodeManager expr::NodeValue* child[N]; };/* struct NodeManager::NVStorage<N> */ - /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance).. - * - * It has been decided for now to hold off on implementations of - * these functions, as they may only be needed in CNF conversion, - * where it's pointless to do a lazy isAtomic determination by - * searching through the DAG, and storing it, since the result will - * only be used once. For more details see the 4/27/2010 cvc5 - * developer's meeting notes at: - * - * http://cvc4.cs.stanford.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29 - */ - // bool containsDecision(TNode); // is "atomic" - // bool properlyContainsDecision(TNode); // all children are atomic - // undefined private copy constructor (disallow copy) NodeManager(const NodeManager&) = delete; @@ -1079,7 +1065,7 @@ class NodeManager /** * This function gives developers a hook into the NodeManager. - * This can be changed in node_manager.cpp without recompiling most of cvc4. + * This can be changed in node_manager.cpp without recompiling most of cvc5. * * debugHook is a debugging only function, and should not be present in * any published code! diff --git a/src/expr/node_value.h b/src/expr/node_value.h index c45fadb5c..5f5ac7d86 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -330,7 +330,7 @@ class NodeValue /** The ID (0 is reserved for the null value) */ uint64_t d_id : NBITS_ID; - /** The expression's reference count. @see cvc4::Node. */ + /** The expression's reference count. */ uint32_t d_rc : NBITS_REFCOUNT; /** Kind of the expression */ diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h index 53057d0b1..6cd0a1467 100644 --- a/src/expr/symbol_manager.h +++ b/src/expr/symbol_manager.h @@ -23,7 +23,7 @@ #include <string> #include "api/cpp/cvc5.h" -#include "cvc4_export.h" +#include "cvc5_export.h" #include "expr/symbol_table.h" namespace cvc5 { @@ -36,7 +36,7 @@ namespace cvc5 { * Like SymbolTable, this class currently lives in src/expr/ since it uses * context-dependent data structures. */ -class CVC4_EXPORT SymbolManager +class CVC5_EXPORT SymbolManager { public: SymbolManager(api::Solver* s); diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index cd80c0eba..ddf26f9da 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -23,7 +23,7 @@ #include <vector> #include "base/exception.h" -#include "cvc4_export.h" +#include "cvc5_export.h" namespace cvc5 { @@ -33,7 +33,7 @@ class Sort; class Term; } // namespace api -class CVC4_EXPORT ScopeException : public Exception +class CVC5_EXPORT ScopeException : public Exception { }; @@ -42,7 +42,7 @@ class CVC4_EXPORT ScopeException : public Exception * nested scoping rules for declarations, with separate bindings for expressions * and types. */ -class CVC4_EXPORT SymbolTable +class CVC5_EXPORT SymbolTable { public: /** Create a symbol table. */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 318d59613..32a1befbd 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -695,8 +695,6 @@ public: * Returns the leastUpperBound in the extended type lattice of the two types. * If this is \top, i.e. there is no inhabited type that contains both, * a TypeNode such that isNull() is true is returned. - * - * For more information see: http://cvc4.cs.nyu.edu/wiki/Cvc4_Type_Lattice */ static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1); static TypeNode mostCommonTypeNode(TypeNode t0, TypeNode t1); diff --git a/src/fix-install-headers.sh b/src/fix-install-headers.sh index 49bade416..083cec852 100755 --- a/src/fix-install-headers.sh +++ b/src/fix-install-headers.sh @@ -8,4 +8,4 @@ find "$dir/include/cvc5/" -type f \ -exec sed -i'' -e 's/include.*"api\/cpp\/\(.*\)"/include <cvc5\/\1>/' {} + find "$dir/include/cvc5/" -type f \ - -exec sed -i'' -e 's/"cvc4_export.h"/<cvc5\/cvc4_export.h>/' {} + + -exec sed -i'' -e 's/"cvc5_export.h"/<cvc5\/cvc5_export.h>/' {} + diff --git a/src/include/cvc5_private.h b/src/include/cvc5_private.h index 6377997ef..101d7e4f2 100644 --- a/src/include/cvc5_private.h +++ b/src/include/cvc5_private.h @@ -17,11 +17,11 @@ #ifndef CVC5_PRIVATE_H #define CVC5_PRIVATE_H -#if !(defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) +#if !(defined(__BUILDING_CVC5LIB) || defined(__BUILDING_CVC5LIB_UNIT_TEST)) # error A private cvc5 header was included when not building the library or private unit test code. #endif -#include "cvc4autoconfig.h" +#include "base/cvc5config.h" #include "cvc5_public.h" #endif /* CVC5_PRIVATE_H */ diff --git a/src/include/cvc5_private_library.h b/src/include/cvc5_private_library.h index 36b2bbd04..b57292aa4 100644 --- a/src/include/cvc5_private_library.h +++ b/src/include/cvc5_private_library.h @@ -17,14 +17,14 @@ #ifndef CVC5_PRIVATE_LIBRARY_H #define CVC5_PRIVATE_LIBRARY_H -#if !(defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) \ - || defined(__BUILDING_CVC4PARSERLIB) \ - || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST) \ - || defined(__BUILDING_CVC4DRIVER)) +#if !(defined(__BUILDING_CVC5LIB) || defined(__BUILDING_CVC5LIB_UNIT_TEST) \ + || defined(__BUILDING_CVC5PARSERLIB) \ + || defined(__BUILDING_CVC5PARSERLIB_UNIT_TEST) \ + || defined(__BUILDING_CVC5DRIVER)) # error A "private library" cvc5 header was included when not building the library, driver, or private unit test code. #endif -#include "cvc4autoconfig.h" +#include "base/cvc5config.h" #include "cvc5_public.h" #endif /* CVC5_PRIVATE_LIBRARY_H */ diff --git a/src/include/cvc5parser_private.h b/src/include/cvc5parser_private.h index 8f6142cbb..fe9508283 100644 --- a/src/include/cvc5parser_private.h +++ b/src/include/cvc5parser_private.h @@ -17,15 +17,15 @@ #ifndef CVC5PARSER_PRIVATE_H #define CVC5PARSER_PRIVATE_H -#if !(defined(__BUILDING_CVC4PARSERLIB) \ - || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST)) +#if !(defined(__BUILDING_CVC5PARSERLIB) \ + || defined(__BUILDING_CVC5PARSERLIB_UNIT_TEST)) # error A private cvc5 parser header was included when not building the parser library or private unit test code. #endif #include "cvc5parser_public.h" -// It would be nice to #include "cvc4autoconfig.h" here, but there are conflicts -// with antlr3's autoheader stuff, which they export :( +// It would be nice to #include "base/cvc5config.h" here, but there are +// conflicts with antlr3's autoheader stuff, which they export :( // -// #include "cvc4autoconfig.h" +// #include "base/cvc5config.h" #endif /* CVC5PARSER_PRIVATE_H */ diff --git a/src/lib/ffs.h b/src/lib/ffs.h index c9ad5422e..eb66e4172 100644 --- a/src/lib/ffs.h +++ b/src/lib/ffs.h @@ -19,7 +19,7 @@ #define CVC5__LIB__FFS_H //We include this for HAVE_FFS -#include "cvc4autoconfig.h" +#include "base/cvc5config.h" #ifdef HAVE_FFS diff --git a/src/lib/replacements.h b/src/lib/replacements.h index ad868d7c6..26749daf6 100644 --- a/src/lib/replacements.h +++ b/src/lib/replacements.h @@ -16,17 +16,19 @@ #ifndef CVC5__LIB__REPLACEMENTS_H #define CVC5__LIB__REPLACEMENTS_H -#if (defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST)) && !defined(__BUILDING_STATISTICS_FOR_EXPORT) +#if (defined(__BUILDING_CVC5LIB) || defined(__BUILDING_CVC5LIB_UNIT_TEST)) \ + && !defined(__BUILDING_STATISTICS_FOR_EXPORT) #include "cvc5_private.h" #else -# if defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST) +#if defined(__BUILDING_CVC5PARSERLIB) \ + || defined(__BUILDING_CVC5PARSERLIB_UNIT_TEST) #include "cvc5parser_private.h" # else -#if defined(__BUILDING_CVC4DRIVER) || defined(__BUILDING_CVC5_SYSTEM_TEST) \ +#if defined(__BUILDING_CVC5DRIVER) || defined(__BUILDING_CVC5_SYSTEM_TEST) \ || defined(__BUILDING_STATISTICS_FOR_EXPORT) -# include "cvc4autoconfig.h" +#include "base/cvc5config.h" # else -# error Must be building libcvc4 or libcvc4parser to use replacement functions. This is because replacement function headers should never be publicly-depended upon, as they should not be installed on user machines with 'make install'. +# error Must be building libcvc5 or libcvc5parser to use replacement functions. This is because replacement function headers should never be publicly-depended upon, as they should not be installed on user machines with 'make install'. # endif # endif #endif diff --git a/src/main/CMakeLists.txt b/src/main/CMakeLists.txt index 868b7f97d..029397832 100644 --- a/src/main/CMakeLists.txt +++ b/src/main/CMakeLists.txt @@ -26,11 +26,11 @@ set(libmain_src_files ) #-----------------------------------------------------------------------------# -# Build object library since we will use the object files for cvc4-bin and +# Build object library since we will use the object files for cvc5-bin and # main-test library. add_library(main OBJECT ${libmain_src_files}) -target_compile_definitions(main PRIVATE -D__BUILDING_CVC4DRIVER) +target_compile_definitions(main PRIVATE -D__BUILDING_CVC5DRIVER) if(ENABLE_SHARED) set_target_properties(main PROPERTIES POSITION_INDEPENDENT_CODE ON) endif() @@ -39,8 +39,8 @@ endif() # supported for cmake version >= 3.12. Hence, we have to manually add the # library dependencies for main. As a consequence, include directories from # dependencies are not propagated and we need to manually add the include -# directories of libcvc4 to main. -add_dependencies(main cvc4 cvc4parser gen-tokens) +# directories of libcvc5 to main. +add_dependencies(main cvc5 cvc5parser gen-tokens) # Note: This should not be required anymore as soon as we get rid of the # smt_engine.h include in src/main. smt_engine.h has transitive includes @@ -56,35 +56,35 @@ target_include_directories(main PRIVATE ${GMP_INCLUDES}) # that we don't have to include all object files of main into each api/unit # test. Do not link against main-test in any other case. add_library(main-test driver_unified.cpp $<TARGET_OBJECTS:main>) -target_compile_definitions(main-test PRIVATE -D__BUILDING_CVC4DRIVER) -target_link_libraries(main-test PUBLIC cvc4 cvc4parser) +target_compile_definitions(main-test PRIVATE -D__BUILDING_CVC5DRIVER) +target_link_libraries(main-test PUBLIC cvc5 cvc5parser) if(USE_CLN) target_link_libraries(main-test PUBLIC CLN) endif() target_link_libraries(main-test PUBLIC GMP) #-----------------------------------------------------------------------------# -# cvc4 binary configuration +# cvc5 binary configuration -add_executable(cvc4-bin driver_unified.cpp main.cpp $<TARGET_OBJECTS:main>) -target_compile_definitions(cvc4-bin PRIVATE -D__BUILDING_CVC4DRIVER) -set_target_properties(cvc4-bin +add_executable(cvc5-bin driver_unified.cpp main.cpp $<TARGET_OBJECTS:main>) +target_compile_definitions(cvc5-bin PRIVATE -D__BUILDING_CVC5DRIVER) +set_target_properties(cvc5-bin PROPERTIES - OUTPUT_NAME cvc4 + OUTPUT_NAME cvc5 RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin) -target_link_libraries(cvc4-bin PUBLIC cvc4 cvc4parser) +target_link_libraries(cvc5-bin PUBLIC cvc5 cvc5parser) if(USE_CLN) - target_link_libraries(cvc4-bin PUBLIC CLN) + target_link_libraries(cvc5-bin PUBLIC CLN) endif() -target_link_libraries(cvc4-bin PUBLIC GMP) +target_link_libraries(cvc5-bin PUBLIC GMP) if(PROGRAM_PREFIX) install(PROGRAMS - $<TARGET_FILE:cvc4-bin> + $<TARGET_FILE:cvc5-bin> DESTINATION ${CMAKE_INSTALL_BINDIR} - RENAME ${PROGRAM_PREFIX}cvc4) + RENAME ${PROGRAM_PREFIX}cvc5) else() - install(TARGETS cvc4-bin + install(TARGETS cvc5-bin DESTINATION ${CMAKE_INSTALL_BINDIR}) endif() @@ -93,13 +93,13 @@ endif() # https://cmake.org/cmake/help/v3.0/prop_tgt/LINK_SEARCH_START_STATIC.html # https://cmake.org/cmake/help/v3.0/prop_tgt/LINK_SEARCH_END_STATIC.html if(ENABLE_STATIC_BINARY) - set_target_properties(cvc4-bin PROPERTIES LINK_FLAGS -static) - set_target_properties(cvc4-bin PROPERTIES LINK_SEARCH_START_STATIC ON) - set_target_properties(cvc4-bin PROPERTIES LINK_SEARCH_END_STATIC ON) + set_target_properties(cvc5-bin PROPERTIES LINK_FLAGS -static) + set_target_properties(cvc5-bin PROPERTIES LINK_SEARCH_START_STATIC ON) + set_target_properties(cvc5-bin PROPERTIES LINK_SEARCH_END_STATIC ON) endif() if(USE_EDITLINE) - target_link_libraries(cvc4-bin PUBLIC ${Editline_LIBRARIES}) + target_link_libraries(cvc5-bin PUBLIC ${Editline_LIBRARIES}) target_link_libraries(main-test PUBLIC ${Editline_LIBRARIES}) target_include_directories(main PUBLIC ${Editline_INCLUDE_DIRS}) endif() diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 2481eda10..9b0ea4759 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -10,7 +10,7 @@ * directory for licensing information. * **************************************************************************** * - * Driver for cvc5 executable (cvc4). + * Driver for cvc5 executable (cvc5). */ #include <stdio.h> @@ -26,8 +26,8 @@ #include "api/cpp/cvc5.h" #include "base/configuration.h" +#include "base/cvc5config.h" #include "base/output.h" -#include "cvc4autoconfig.h" #include "main/command_executor.h" #include "main/interactive_shell.h" #include "main/main.h" @@ -91,7 +91,8 @@ void printUsage(Options& opts, bool full) { } } -int runCvc4(int argc, char* argv[], Options& opts) { +int runCvc5(int argc, char* argv[], Options& opts) +{ main::totalTime = std::make_unique<TotalTimer>(); // For the signal handlers' benefit pOptions = &opts; diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 127b2c14d..516f9e621 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -27,7 +27,7 @@ #include <vector> // This must go before HAVE_LIBEDITLINE. -#include "cvc4autoconfig.h" +#include "base/cvc5config.h" #if HAVE_LIBEDITLINE #include <editline/readline.h> @@ -112,13 +112,13 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) OutputLanguage lang = toOutputLanguage(d_options.getInputLanguage()); switch(lang) { case output::LANG_CVC: - d_historyFilename = string(getenv("HOME")) + "/.cvc4_history"; + d_historyFilename = string(getenv("HOME")) + "/.cvc5_history"; commandsBegin = cvc_commands; commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands); break; case output::LANG_TPTP: - d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_tptp"; + d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_tptp"; commandsBegin = tptp_commands; commandsEnd = tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands); @@ -126,7 +126,7 @@ InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm) default: if (language::isOutputLang_smt2(lang)) { - d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2"; + d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_smtlib2"; commandsBegin = smt2_commands; commandsEnd = smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands); diff --git a/src/main/main.cpp b/src/main/main.cpp index a4e70be89..6a7baebb3 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -41,13 +41,13 @@ using namespace cvc5::language; * cvc5's main() routine is just an exception-safe wrapper around cvc5. * Please don't construct anything here. Even if the constructor is * inside the try { }, an exception during destruction can cause - * problems. That's why main() wraps runCvc4() in the first place. - * Put everything in runCvc4(). + * problems. That's why main() wraps runCvc5() in the first place. + * Put everything in runCvc5(). */ int main(int argc, char* argv[]) { Options opts; try { - return runCvc4(argc, argv, opts); + return runCvc5(argc, argv, opts); } catch(OptionException& e) { #ifdef CVC5_COMPETITION_MODE *opts.getOut() << "unknown" << endl; diff --git a/src/main/main.h b/src/main/main.h index 121f9d951..54abbdbe9 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -18,8 +18,8 @@ #include <memory> #include <string> +#include "base/cvc5config.h" #include "base/exception.h" -#include "cvc4autoconfig.h" #include "options/options.h" #ifndef CVC5__MAIN__MAIN_H @@ -62,19 +62,11 @@ extern bool segvSpin; /** A pointer to the options in play */ extern thread_local Options* pOptions; -/** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. - * This can throw a cvc5::Exception. - */ -void cvc4_init(); - -/** Shutdown the driver. Frees memory for the signal handlers. */ -void cvc4_shutdown() noexcept; - } // namespace main } // namespace cvc5 -/** Actual Cvc4 driver functions **/ -int runCvc4(int argc, char* argv[], cvc5::Options&); +/** Actual cvc5 driver functions **/ +int runCvc5(int argc, char* argv[], cvc5::Options&); void printUsage(cvc5::Options&, bool full = false); #endif /* CVC5__MAIN__MAIN_H */ diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp index 9a6e34075..503bbc198 100644 --- a/src/main/signal_handlers.cpp +++ b/src/main/signal_handlers.cpp @@ -32,8 +32,8 @@ #endif /* __WIN32__ */ +#include "base/cvc5config.h" #include "base/exception.h" -#include "cvc4autoconfig.h" #include "main/command_executor.h" #include "main/main.h" #include "options/options.h" @@ -73,8 +73,8 @@ void timeout_handler() #ifndef __WIN32__ #ifdef HAVE_SIGALTSTACK -size_t cvc4StackSize; -void* cvc4StackBase; +size_t stackSize; +void* stackBase; #endif /* HAVE_SIGALTSTACK */ /** Handler for SIGXCPU and SIGALRM, i.e., timeout. */ @@ -100,15 +100,15 @@ void sigint_handler(int sig, siginfo_t* info, void*) /** Handler for SIGSEGV (segfault). */ void segv_handler(int sig, siginfo_t* info, void* c) { - uintptr_t extent = reinterpret_cast<uintptr_t>(cvc4StackBase) - cvc4StackSize; + uintptr_t extent = reinterpret_cast<uintptr_t>(stackBase) - stackSize; uintptr_t addr = reinterpret_cast<uintptr_t>(info->si_addr); #ifdef CVC5_DEBUG safe_print(STDERR_FILENO, "cvc5 suffered a segfault in DEBUG mode.\n"); safe_print(STDERR_FILENO, "Offending address is "); safe_print(STDERR_FILENO, info->si_addr); safe_print(STDERR_FILENO, "\n"); - // cerr << "base is " << (void*)cvc4StackBase << endl; - // cerr << "size is " << cvc4StackSize << endl; + // cerr << "base is " << (void*)stackBase << endl; + // cerr << "size is " << stackSize << endl; // cerr << "extent is " << (void*)extent << endl; if (addr >= extent && addr <= extent + 10 * 1024) { @@ -211,7 +211,7 @@ void ill_handler(int sig, siginfo_t* info, void*) static terminate_handler default_terminator; -void cvc4terminate() +void cvc5terminate() { set_terminate(default_terminator); #ifdef CVC5_DEBUG @@ -301,8 +301,8 @@ void install() throw Exception(string("sigaltstack() failure: ") + strerror(errno)); } - cvc4StackSize = limit.rlim_cur; - cvc4StackBase = ss.ss_sp; + stackSize = limit.rlim_cur; + stackBase = ss.ss_sp; struct sigaction act4; act4.sa_sigaction = segv_handler; @@ -325,16 +325,16 @@ void install() #endif /* __WIN32__ */ - default_terminator = set_terminate(cvc4terminate); + default_terminator = set_terminate(cvc5terminate); } void cleanup() noexcept { #ifndef __WIN32__ #ifdef HAVE_SIGALTSTACK - free(cvc4StackBase); - cvc4StackBase = NULL; - cvc4StackSize = 0; + free(stackBase); + stackBase = nullptr; + stackSize = 0; #endif /* HAVE_SIGALTSTACK */ #endif /* __WIN32__ */ } diff --git a/src/main/time_limit.cpp b/src/main/time_limit.cpp index bd41ed7ed..82cfda017 100644 --- a/src/main/time_limit.cpp +++ b/src/main/time_limit.cpp @@ -41,7 +41,7 @@ #include "time_limit.h" -#include "cvc4autoconfig.h" +#include "base/cvc5config.h" #if HAVE_SETITIMER #include <signal.h> diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt index 77c4d5a09..424f5e0df 100644 --- a/src/options/CMakeLists.txt +++ b/src/options/CMakeLists.txt @@ -16,7 +16,7 @@ # Check if the toml Python module is installed. check_python_module("toml") -libcvc4_add_sources( +libcvc5_add_sources( base_handlers.h decision_weight.h didyoumean.cpp @@ -66,7 +66,7 @@ set(options_toml_files string(REPLACE "toml" "cpp;" options_gen_cpp_files ${options_toml_files}) string(REPLACE "toml" "h;" options_gen_h_files ${options_toml_files}) -libcvc4_add_sources(GENERATED options.cpp ${options_gen_cpp_files}) +libcvc5_add_sources(GENERATED options.cpp ${options_gen_cpp_files}) list_prepend(options_toml_files "${CMAKE_CURRENT_LIST_DIR}/" abs_toml_files) @@ -88,7 +88,7 @@ add_custom_command( module_template.cpp options_holder_template.h options_template.cpp - ${CMAKE_CURRENT_BINARY_DIR}/../../doc/cvc4.1_template + ${CMAKE_CURRENT_BINARY_DIR}/../../doc/cvc5.1_template ${CMAKE_CURRENT_BINARY_DIR}/../../doc/SmtEngine.3cvc_template ${CMAKE_CURRENT_BINARY_DIR}/../../doc/options.3cvc_template ) diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml index a43641c73..164dd736b 100644 --- a/src/options/datatypes_options.toml +++ b/src/options/datatypes_options.toml @@ -4,7 +4,7 @@ header = "options/datatypes_options.h" # How to handle selectors applied to incorrect constructors. If this option is set, # then we do not rewrite such a selector term to an arbitrary ground term. -# For example, by default cvc4 considers cdr( nil ) = nil. If this option is set, then +# For example, by default cvc5 considers cdr( nil ) = nil. If this option is set, then # cdr( nil ) has no set value. [[option]] name = "dtRewriteErrorSel" diff --git a/src/options/language.h b/src/options/language.h index 54e0e9dfa..04182cdd9 100644 --- a/src/options/language.h +++ b/src/options/language.h @@ -21,14 +21,14 @@ #include <ostream> #include <string> -#include "cvc4_export.h" +#include "cvc5_export.h" namespace cvc5 { namespace language { namespace input { -enum CVC4_EXPORT Language +enum CVC5_EXPORT Language { // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 @@ -60,7 +60,7 @@ enum CVC4_EXPORT Language LANG_MAX }; /* enum Language */ -inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_EXPORT; +inline std::ostream& operator<<(std::ostream& out, Language lang) CVC5_EXPORT; inline std::ostream& operator<<(std::ostream& out, Language lang) { switch(lang) { case LANG_AUTO: @@ -84,7 +84,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { namespace output { -enum CVC4_EXPORT Language +enum CVC5_EXPORT Language { // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0 @@ -119,7 +119,7 @@ enum CVC4_EXPORT Language LANG_MAX }; /* enum Language */ -inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_EXPORT; +inline std::ostream& operator<<(std::ostream& out, Language lang) CVC5_EXPORT; inline std::ostream& operator<<(std::ostream& out, Language lang) { switch(lang) { case LANG_SMTLIB_V2_6: out << "LANG_SMTLIB_V2_6"; break; @@ -147,24 +147,24 @@ typedef language::output::Language OutputLanguage; namespace language { /** Is the language a variant of the smtlib version 2 language? */ -bool isInputLang_smt2(InputLanguage lang) CVC4_EXPORT; -bool isOutputLang_smt2(OutputLanguage lang) CVC4_EXPORT; +bool isInputLang_smt2(InputLanguage lang) CVC5_EXPORT; +bool isOutputLang_smt2(OutputLanguage lang) CVC5_EXPORT; /** * Is the language smtlib 2.6 or above? If exact=true, then this method returns * false if the input language is not exactly SMT-LIB 2.6. */ -bool isInputLang_smt2_6(InputLanguage lang, bool exact = false) CVC4_EXPORT; -bool isOutputLang_smt2_6(OutputLanguage lang, bool exact = false) CVC4_EXPORT; +bool isInputLang_smt2_6(InputLanguage lang, bool exact = false) CVC5_EXPORT; +bool isOutputLang_smt2_6(OutputLanguage lang, bool exact = false) CVC5_EXPORT; /** Is the language a variant of the SyGuS input language? */ -bool isInputLangSygus(InputLanguage lang) CVC4_EXPORT; -bool isOutputLangSygus(OutputLanguage lang) CVC4_EXPORT; +bool isInputLangSygus(InputLanguage lang) CVC5_EXPORT; +bool isOutputLangSygus(OutputLanguage lang) CVC5_EXPORT; -InputLanguage toInputLanguage(OutputLanguage language) CVC4_EXPORT; -OutputLanguage toOutputLanguage(InputLanguage language) CVC4_EXPORT; -InputLanguage toInputLanguage(std::string language) CVC4_EXPORT; -OutputLanguage toOutputLanguage(std::string language) CVC4_EXPORT; +InputLanguage toInputLanguage(OutputLanguage language) CVC5_EXPORT; +OutputLanguage toOutputLanguage(InputLanguage language) CVC5_EXPORT; +InputLanguage toInputLanguage(std::string language) CVC5_EXPORT; +OutputLanguage toOutputLanguage(std::string language) CVC5_EXPORT; } // namespace language } // namespace cvc5 diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 4fe93c129..c28a6f0cf 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -33,7 +33,7 @@ - module_template.h Directory <tpl-doc> must contain: - - cvc4.1_template + - cvc5.1_template - options.3cvc_template - SmtEngine.3cvc_template These files get generated during autogen.sh from the corresponding *.in @@ -49,7 +49,7 @@ - <dst>/MODULE_options.cpp - <dst>/options_holder.h - <dst>/options.cpp - - <tpl-doc>/cvc4.1 + - <tpl-doc>/cvc5.1 - <tpl-doc>/options.3 - <tpl-doc>/SmtEngine.3 """ @@ -1133,7 +1133,7 @@ def codegen_all_modules(modules, dst_dir, tpl_options, tpl_options_holder, getoption_handlers='\n'.join(getoption_handlers) )) - write_file(doc_dir, 'cvc4.1', tpl_man_cvc.format( + write_file(doc_dir, 'cvc5.1', tpl_man_cvc.format( man_common='\n'.join(man_common), man_others='\n'.join(man_others) )) @@ -1330,7 +1330,7 @@ def mkoptions_main(): tpl_options_holder = read_tpl(src_dir, 'options_holder_template.h') # Read documentation template files from documentation directory. - tpl_man_cvc = read_tpl(doc_dir, 'cvc4.1_template') + tpl_man_cvc = read_tpl(doc_dir, 'cvc5.1_template') tpl_man_smt = read_tpl(doc_dir, 'SmtEngine.3cvc_template') tpl_man_int = read_tpl(doc_dir, 'options.3cvc_template') diff --git a/src/options/open_ostream.cpp b/src/options/open_ostream.cpp index fa36738d9..3b13c42e2 100644 --- a/src/options/open_ostream.cpp +++ b/src/options/open_ostream.cpp @@ -60,15 +60,16 @@ std::pair< bool, std::ostream* > OstreamOpener::open(const std::string& optarg) std::ofstream::out | std::ofstream::trunc); if(outStream == NULL || !*outStream) { std::stringstream ss; - ss << "Cannot open " << d_channelName << " file: `" - << optarg << "': " << cvc4_errno_failreason(); + ss << "Cannot open " << d_channelName << " file: `" << optarg + << "': " << cvc5_errno_failreason(); throw OptionException(ss.str()); } return make_pair(true, outStream); } } -std::string cvc4_errno_failreason() { +std::string cvc5_errno_failreason() +{ #if HAVE_STRERROR_R #if STRERROR_R_CHAR_P if(errno != 0) { diff --git a/src/options/open_ostream.h b/src/options/open_ostream.h index b135ef7ce..162bf3f11 100644 --- a/src/options/open_ostream.h +++ b/src/options/open_ostream.h @@ -54,7 +54,7 @@ class OstreamOpener { }; /* class OstreamOpener */ -std::string cvc4_errno_failreason(); +std::string cvc5_errno_failreason(); } // namespace cvc5 diff --git a/src/options/option_exception.h b/src/options/option_exception.h index 4cfe55a31..f5590709e 100644 --- a/src/options/option_exception.h +++ b/src/options/option_exception.h @@ -19,7 +19,7 @@ #define CVC5__OPTION_EXCEPTION_H #include "base/exception.h" -#include "cvc4_export.h" +#include "cvc5_export.h" namespace cvc5 { @@ -29,7 +29,7 @@ namespace cvc5 { * name is itself unrecognized, a UnrecognizedOptionException (a derived * class, below) should be used instead. */ -class CVC4_EXPORT OptionException : public cvc5::Exception +class CVC5_EXPORT OptionException : public cvc5::Exception { public: OptionException(const std::string& s) : cvc5::Exception(s_errPrefix + s) {} diff --git a/src/options/options.h b/src/options/options.h index 79b00de30..67707c990 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -25,7 +25,7 @@ #include "base/listener.h" #include "base/modal_exception.h" -#include "cvc4_export.h" +#include "cvc5_export.h" #include "options/language.h" #include "options/option_exception.h" #include "options/printer_modes.h" @@ -42,7 +42,7 @@ namespace options { class OptionsListener; -class CVC4_EXPORT Options +class CVC5_EXPORT Options { friend api::Solver; /** The struct that holds all option values. */ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 3c5616c73..0e2315aa0 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -15,15 +15,14 @@ #include "options/options_handler.h" +#include <cerrno> #include <ostream> #include <string> -#include <cerrno> - -#include "cvc4autoconfig.h" #include "base/check.h" #include "base/configuration.h" #include "base/configuration_private.h" +#include "base/cvc5config.h" #include "base/exception.h" #include "base/modal_exception.h" #include "base/output.h" diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 91d06dec2..f24f83b2b 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -15,7 +15,7 @@ #if !defined(_BSD_SOURCE) && defined(__MINGW32__) && !defined(__MINGW64__) // force use of optreset; mingw32 croaks on argv-switching otherwise -#include "cvc4autoconfig.h" +#include "base/cvc5config.h" #define _BSD_SOURCE #undef HAVE_DECL_OPTRESET #define HAVE_DECL_OPTRESET 1 @@ -58,7 +58,7 @@ extern int optreset; ${headers_module}$ #include "options/options_holder.h" -#include "cvc4autoconfig.h" +#include "base/cvc5config.h" #include "options/base_handlers.h" ${headers_handler}$ diff --git a/src/options/set_language.h b/src/options/set_language.h index 5ff7cdb7b..45add38ac 100644 --- a/src/options/set_language.h +++ b/src/options/set_language.h @@ -20,7 +20,7 @@ #include <iostream> -#include "cvc4_export.h" +#include "cvc5_export.h" #include "options/language.h" namespace cvc5 { @@ -29,7 +29,7 @@ namespace language { /** * IOStream manipulator to set the output language for Exprs. */ -class CVC4_EXPORT SetLanguage +class CVC5_EXPORT SetLanguage { public: /** @@ -87,7 +87,7 @@ private: * * The setting stays permanently (until set again) with the stream. */ -std::ostream& operator<<(std::ostream& out, SetLanguage l) CVC4_EXPORT; +std::ostream& operator<<(std::ostream& out, SetLanguage l) CVC5_EXPORT; } // namespace language } // namespace cvc5 diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index da6b1bd58..f2596ceeb 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -19,9 +19,9 @@ find_package(ANTLR3 3.4 REQUIRED) find_package(Java COMPONENTS Runtime REQUIRED) #-----------------------------------------------------------------------------# -# libcvc4parser source files +# libcvc5parser source files -set(libcvc4parser_src_files +set(libcvc5parser_src_files antlr_input.cpp antlr_input.h antlr_input_imports.cpp @@ -96,28 +96,28 @@ foreach(lang Cvc Smt2 Tptp) ${gen_src_files} PROPERTIES COMPILE_FLAGS "-Wno-all -Wno-error") # Add generated source files to the parser source files - list(APPEND libcvc4parser_src_files ${gen_src_files}) + list(APPEND libcvc5parser_src_files ${gen_src_files}) endforeach() #-----------------------------------------------------------------------------# -# libcvc4parser configuration +# libcvc5parser configuration -add_library(cvc4parser ${libcvc4parser_src_files}) -set_target_properties(cvc4parser PROPERTIES SOVERSION ${CVC5_SOVERSION}) -target_compile_definitions(cvc4parser PRIVATE -D__BUILDING_CVC4PARSERLIB) -target_link_libraries(cvc4parser PUBLIC cvc4) -target_link_libraries(cvc4parser PRIVATE ANTLR3) +add_library(cvc5parser ${libcvc5parser_src_files}) +set_target_properties(cvc5parser PROPERTIES SOVERSION ${CVC5_SOVERSION}) +target_compile_definitions(cvc5parser PRIVATE -D__BUILDING_CVC5PARSERLIB) +target_link_libraries(cvc5parser PUBLIC cvc5) +target_link_libraries(cvc5parser PRIVATE ANTLR3) -install(TARGETS cvc4parser - EXPORT cvc4-targets +install(TARGETS cvc5parser + EXPORT cvc5-targets DESTINATION ${CMAKE_INSTALL_LIBDIR}) # The generated lexer/parser files define some functions as # __declspec(dllexport) via the ANTLR3_API macro, which leads to lots of -# unresolved symbols when linking against libcvc4parser. +# unresolved symbols when linking against libcvc5parser. # -Wl,--export-all-symbols makes sure that all symbols are exported when # building a DLL. if(CVC5_WINDOWS_BUILD) - set_target_properties(cvc4parser + set_target_properties(cvc5parser PROPERTIES LINK_FLAGS "-Wl,--export-all-symbols") endif() diff --git a/src/parser/antlr_tracing.h b/src/parser/antlr_tracing.h index 595a2d784..e9d1d0758 100644 --- a/src/parser/antlr_tracing.h +++ b/src/parser/antlr_tracing.h @@ -44,7 +44,8 @@ */ /** A "System" object, just like in Java! */ -static struct __Cvc4System { +static struct __Cvc5System +{ /** * Helper class just to handle arbitrary string concatenation * with Java syntax. In C++ you cannot do "char*" + "char*", @@ -76,7 +77,11 @@ static struct __Cvc4System { // These are highly dependent on the bugs in a particular ANTLR release. // These seem to work with ANTLR 3.3 as of 4/23/2011. A different trick // works with ANTLR 3.2. EXPECT LOTS OF COMPILER WARNINGS. -#define println(x) println(({int failed=0;__Cvc4System::JavaPrinter()+x;})) +#define println(x) \ + println(({ \ + int failed = 0; \ + __Cvc5System::JavaPrinter() + x; \ + })) #undef ANTLR3_FPRINTF #define ANTLR3_FPRINTF(args...) {int failed=0;fprintf(args);} #undef ANTLR3_PRINTF diff --git a/src/parser/input.h b/src/parser/input.h index fb7ce2b40..47453e367 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -25,7 +25,7 @@ #include <vector> #include "api/cpp/cvc5.h" -#include "cvc4_export.h" +#include "cvc5_export.h" #include "options/language.h" #include "parser/parser_exception.h" @@ -78,7 +78,7 @@ class Parser; * for the given input language and attach it to an input source of the * appropriate type. */ -class CVC4_EXPORT Input +class CVC5_EXPORT Input { friend class Parser; // for parseError, parseCommand, parseExpr friend class ParserBuilder; diff --git a/src/parser/parser.h b/src/parser/parser.h index da35606c1..42baf98cd 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -23,7 +23,7 @@ #include <string> #include "api/cpp/cvc5.h" -#include "cvc4_export.h" +#include "cvc5_export.h" #include "expr/kind.h" #include "expr/symbol_manager.h" #include "expr/symbol_table.h" @@ -101,7 +101,7 @@ inline std::ostream& operator<<(std::ostream& out, SymbolType type) { * name of the file, line number and column information, and in-scope * declarations. */ -class CVC4_EXPORT Parser +class CVC5_EXPORT Parser { friend class ParserBuilder; private: diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index b0f9e35e6..5d73fedfa 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -20,7 +20,7 @@ #include <string> -#include "cvc4_export.h" +#include "cvc5_export.h" #include "options/language.h" #include "parser/input.h" @@ -42,7 +42,7 @@ class Parser; * called any number of times on an instance and will generate a fresh * parser each time. */ -class CVC4_EXPORT ParserBuilder +class CVC5_EXPORT ParserBuilder { enum InputType { FILE_INPUT, diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index 0372661a2..124013183 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -19,16 +19,16 @@ #define CVC5__PARSER__PARSER_EXCEPTION_H #include <iostream> -#include <string> #include <sstream> +#include <string> #include "base/exception.h" -#include "cvc4_export.h" +#include "cvc5_export.h" namespace cvc5 { namespace parser { -class CVC4_EXPORT ParserException : public Exception +class CVC5_EXPORT ParserException : public Exception { public: // Constructors diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 7c7196822..1d8bf8f17 100644 --- a/src/prop/bvminisat/bvminisat.cpp +++ b/src/prop/bvminisat/bvminisat.cpp @@ -12,7 +12,7 @@ * * SAT Solver. * - * Implementation of the minisat for cvc4 (bit-vectors). + * Implementation of the minisat for cvc5 (bit-vectors). */ #include "prop/bvminisat/bvminisat.h" diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h index 9d363224f..ea509ece6 100644 --- a/src/prop/bvminisat/bvminisat.h +++ b/src/prop/bvminisat/bvminisat.h @@ -12,7 +12,7 @@ * * SAT Solver. * - * Implementation of the minisat for cvc4 (bit-vectors). + * Implementation of the minisat for cvc5 (bit-vectors). */ #include "cvc5_private.h" diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h index 3826eb9f9..d2423a71a 100644 --- a/src/prop/bvminisat/core/Solver.h +++ b/src/prop/bvminisat/core/Solver.h @@ -79,7 +79,7 @@ private: /** To notify */ Notify* d_notify; - /** Cvc4 context */ + /** cvc5 context */ cvc5::context::Context* c; /** True constant */ diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp index eee0842de..ef13a0b46 100644 --- a/src/prop/cryptominisat.cpp +++ b/src/prop/cryptominisat.cpp @@ -12,7 +12,7 @@ * * SAT Solver. * - * Implementation of the cryptominisat for cvc4 (bit-vectors). + * Implementation of the cryptominisat for cvc5 (bit-vectors). */ #include "prop/cryptominisat.h" diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h index f19821067..58ce33bcf 100644 --- a/src/prop/cryptominisat.h +++ b/src/prop/cryptominisat.h @@ -12,7 +12,7 @@ * * SAT Solver. * - * Implementation of the cryptominisat sat solver for cvc4 (bit-vectors). + * Implementation of the cryptominisat sat solver for cvc5 (bit-vectors). */ #include "cvc5_private.h" diff --git a/src/smt/command.h b/src/smt/command.h index 07dfa2b30..41a3639c9 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -28,7 +28,7 @@ #include <vector> #include "api/cpp/cvc5.h" -#include "cvc4_export.h" +#include "cvc5_export.h" #include "options/language.h" namespace cvc5 { @@ -53,12 +53,12 @@ class Model; * @param sexpr the symbolic expression to convert * @return the symbolic expression as string */ -std::string sexprToString(api::Term sexpr) CVC4_EXPORT; +std::string sexprToString(api::Term sexpr) CVC5_EXPORT; -std::ostream& operator<<(std::ostream&, const Command&) CVC4_EXPORT; -std::ostream& operator<<(std::ostream&, const Command*) CVC4_EXPORT; -std::ostream& operator<<(std::ostream&, const CommandStatus&) CVC4_EXPORT; -std::ostream& operator<<(std::ostream&, const CommandStatus*) CVC4_EXPORT; +std::ostream& operator<<(std::ostream&, const Command&) CVC5_EXPORT; +std::ostream& operator<<(std::ostream&, const Command*) CVC5_EXPORT; +std::ostream& operator<<(std::ostream&, const CommandStatus&) CVC5_EXPORT; +std::ostream& operator<<(std::ostream&, const CommandStatus*) CVC5_EXPORT; /** The status an SMT benchmark can have */ enum BenchmarkStatus @@ -71,7 +71,7 @@ enum BenchmarkStatus SMT_UNKNOWN }; /* enum BenchmarkStatus */ -std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) CVC4_EXPORT; +std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) CVC5_EXPORT; /** * IOStream manipulator to print success messages or not. @@ -85,7 +85,7 @@ std::ostream& operator<<(std::ostream& out, BenchmarkStatus status) CVC4_EXPORT; * prints a success message (in a manner appropriate for the current * output language). */ -class CVC4_EXPORT CommandPrintSuccess +class CVC5_EXPORT CommandPrintSuccess { public: /** Construct a CommandPrintSuccess with the given setting. */ @@ -119,9 +119,9 @@ class CVC4_EXPORT CommandPrintSuccess * The depth stays permanently (until set again) with the stream. */ std::ostream& operator<<(std::ostream& out, - CommandPrintSuccess cps) CVC4_EXPORT; + CommandPrintSuccess cps) CVC5_EXPORT; -class CVC4_EXPORT CommandStatus +class CVC5_EXPORT CommandStatus { protected: // shouldn't construct a CommandStatus (use a derived class) @@ -134,7 +134,7 @@ class CVC4_EXPORT CommandStatus virtual CommandStatus& clone() const = 0; }; /* class CommandStatus */ -class CVC4_EXPORT CommandSuccess : public CommandStatus +class CVC5_EXPORT CommandSuccess : public CommandStatus { static const CommandSuccess* s_instance; @@ -146,7 +146,7 @@ class CVC4_EXPORT CommandSuccess : public CommandStatus } }; /* class CommandSuccess */ -class CVC4_EXPORT CommandInterrupted : public CommandStatus +class CVC5_EXPORT CommandInterrupted : public CommandStatus { static const CommandInterrupted* s_instance; @@ -158,7 +158,7 @@ class CVC4_EXPORT CommandInterrupted : public CommandStatus } }; /* class CommandInterrupted */ -class CVC4_EXPORT CommandUnsupported : public CommandStatus +class CVC5_EXPORT CommandUnsupported : public CommandStatus { public: CommandStatus& clone() const override @@ -167,7 +167,7 @@ class CVC4_EXPORT CommandUnsupported : public CommandStatus } }; /* class CommandSuccess */ -class CVC4_EXPORT CommandFailure : public CommandStatus +class CVC5_EXPORT CommandFailure : public CommandStatus { std::string d_message; @@ -183,7 +183,7 @@ class CVC4_EXPORT CommandFailure : public CommandStatus * for an unsat core in a place that is not immediately preceded by an * unsat/valid response. */ -class CVC4_EXPORT CommandRecoverableFailure : public CommandStatus +class CVC5_EXPORT CommandRecoverableFailure : public CommandStatus { std::string d_message; @@ -196,7 +196,7 @@ class CVC4_EXPORT CommandRecoverableFailure : public CommandStatus std::string getMessage() const { return d_message; } }; /* class CommandRecoverableFailure */ -class CVC4_EXPORT Command +class CVC5_EXPORT Command { public: typedef CommandPrintSuccess printsuccess; @@ -302,7 +302,7 @@ class CVC4_EXPORT Command * EmptyCommands are the residue of a command after the parser handles * them (and there's nothing left to do). */ -class CVC4_EXPORT EmptyCommand : public Command +class CVC5_EXPORT EmptyCommand : public Command { public: EmptyCommand(std::string name = ""); @@ -320,7 +320,7 @@ class CVC4_EXPORT EmptyCommand : public Command std::string d_name; }; /* class EmptyCommand */ -class CVC4_EXPORT EchoCommand : public Command +class CVC5_EXPORT EchoCommand : public Command { public: EchoCommand(std::string output = ""); @@ -344,7 +344,7 @@ class CVC4_EXPORT EchoCommand : public Command std::string d_output; }; /* class EchoCommand */ -class CVC4_EXPORT AssertCommand : public Command +class CVC5_EXPORT AssertCommand : public Command { protected: api::Term d_term; @@ -366,7 +366,7 @@ class CVC4_EXPORT AssertCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class AssertCommand */ -class CVC4_EXPORT PushCommand : public Command +class CVC5_EXPORT PushCommand : public Command { public: void invoke(api::Solver* solver, SymbolManager* sm) override; @@ -379,7 +379,7 @@ class CVC4_EXPORT PushCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class PushCommand */ -class CVC4_EXPORT PopCommand : public Command +class CVC5_EXPORT PopCommand : public Command { public: void invoke(api::Solver* solver, SymbolManager* sm) override; @@ -392,7 +392,7 @@ class CVC4_EXPORT PopCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class PopCommand */ -class CVC4_EXPORT DeclarationDefinitionCommand : public Command +class CVC5_EXPORT DeclarationDefinitionCommand : public Command { protected: std::string d_symbol; @@ -404,7 +404,7 @@ class CVC4_EXPORT DeclarationDefinitionCommand : public Command std::string getSymbol() const; }; /* class DeclarationDefinitionCommand */ -class CVC4_EXPORT DeclareFunctionCommand : public DeclarationDefinitionCommand +class CVC5_EXPORT DeclareFunctionCommand : public DeclarationDefinitionCommand { protected: api::Term d_func; @@ -425,7 +425,7 @@ class CVC4_EXPORT DeclareFunctionCommand : public DeclarationDefinitionCommand OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DeclareFunctionCommand */ -class CVC4_EXPORT DeclarePoolCommand : public DeclarationDefinitionCommand +class CVC5_EXPORT DeclarePoolCommand : public DeclarationDefinitionCommand { protected: api::Term d_func; @@ -451,7 +451,7 @@ class CVC4_EXPORT DeclarePoolCommand : public DeclarationDefinitionCommand OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DeclarePoolCommand */ -class CVC4_EXPORT DeclareSortCommand : public DeclarationDefinitionCommand +class CVC5_EXPORT DeclareSortCommand : public DeclarationDefinitionCommand { protected: size_t d_arity; @@ -473,7 +473,7 @@ class CVC4_EXPORT DeclareSortCommand : public DeclarationDefinitionCommand OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DeclareSortCommand */ -class CVC4_EXPORT DefineSortCommand : public DeclarationDefinitionCommand +class CVC5_EXPORT DefineSortCommand : public DeclarationDefinitionCommand { protected: std::vector<api::Sort> d_params; @@ -498,7 +498,7 @@ class CVC4_EXPORT DefineSortCommand : public DeclarationDefinitionCommand OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DefineSortCommand */ -class CVC4_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand +class CVC5_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand { public: DefineFunctionCommand(const std::string& id, @@ -543,7 +543,7 @@ class CVC4_EXPORT DefineFunctionCommand : public DeclarationDefinitionCommand * This command will assert a set of quantified formulas that specify * the (mutually recursive) function definitions provided to it. */ -class CVC4_EXPORT DefineFunctionRecCommand : public Command +class CVC5_EXPORT DefineFunctionRecCommand : public Command { public: DefineFunctionRecCommand(api::Term func, @@ -588,7 +588,7 @@ class CVC4_EXPORT DefineFunctionRecCommand : public Command * (declare-heap (T U)) * where T is the location sort and U is the data sort. */ -class CVC4_EXPORT DeclareHeapCommand : public Command +class CVC5_EXPORT DeclareHeapCommand : public Command { public: DeclareHeapCommand(api::Sort locSort, api::Sort dataSort); @@ -614,7 +614,7 @@ class CVC4_EXPORT DeclareHeapCommand : public Command * The command when an attribute is set by a user. In SMT-LIBv2 this is done * via the syntax (! expr :attr) */ -class CVC4_EXPORT SetUserAttributeCommand : public Command +class CVC5_EXPORT SetUserAttributeCommand : public Command { public: SetUserAttributeCommand(const std::string& attr, api::Term term); @@ -650,7 +650,7 @@ class CVC4_EXPORT SetUserAttributeCommand : public Command * The command when parsing check-sat. * This command will check satisfiability of the input formula. */ -class CVC4_EXPORT CheckSatCommand : public Command +class CVC5_EXPORT CheckSatCommand : public Command { public: CheckSatCommand(); @@ -678,7 +678,7 @@ class CVC4_EXPORT CheckSatCommand : public Command * This command will assume a set of formulas and check satisfiability of the * input formula under these assumptions. */ -class CVC4_EXPORT CheckSatAssumingCommand : public Command +class CVC5_EXPORT CheckSatAssumingCommand : public Command { public: CheckSatAssumingCommand(api::Term term); @@ -701,7 +701,7 @@ class CVC4_EXPORT CheckSatAssumingCommand : public Command api::Result d_result; }; /* class CheckSatAssumingCommand */ -class CVC4_EXPORT QueryCommand : public Command +class CVC5_EXPORT QueryCommand : public Command { protected: api::Term d_term; @@ -727,7 +727,7 @@ class CVC4_EXPORT QueryCommand : public Command /* ------------------- sygus commands ------------------ */ /** Declares a sygus universal variable */ -class CVC4_EXPORT DeclareSygusVarCommand : public DeclarationDefinitionCommand +class CVC5_EXPORT DeclareSygusVarCommand : public DeclarationDefinitionCommand { public: DeclareSygusVarCommand(const std::string& id, api::Term var, api::Sort sort); @@ -764,7 +764,7 @@ class CVC4_EXPORT DeclareSygusVarCommand : public DeclarationDefinitionCommand * This command is also used for the special case in which we are declaring an * invariant-to-synthesize */ -class CVC4_EXPORT SynthFunCommand : public DeclarationDefinitionCommand +class CVC5_EXPORT SynthFunCommand : public DeclarationDefinitionCommand { public: SynthFunCommand(const std::string& id, @@ -815,7 +815,7 @@ class CVC4_EXPORT SynthFunCommand : public DeclarationDefinitionCommand }; /** Declares a sygus constraint */ -class CVC4_EXPORT SygusConstraintCommand : public Command +class CVC5_EXPORT SygusConstraintCommand : public Command { public: SygusConstraintCommand(const api::Term& t); @@ -853,7 +853,7 @@ class CVC4_EXPORT SygusConstraintCommand : public Command * than the precondition, not weaker than the postcondition and inductive * w.r.t. the transition relation. */ -class CVC4_EXPORT SygusInvConstraintCommand : public Command +class CVC5_EXPORT SygusInvConstraintCommand : public Command { public: SygusInvConstraintCommand(const std::vector<api::Term>& predicates); @@ -889,7 +889,7 @@ class CVC4_EXPORT SygusInvConstraintCommand : public Command }; /** Declares a synthesis conjecture */ -class CVC4_EXPORT CheckSynthCommand : public Command +class CVC5_EXPORT CheckSynthCommand : public Command { public: CheckSynthCommand(){}; @@ -927,7 +927,7 @@ class CVC4_EXPORT CheckSynthCommand : public Command /* ------------------- sygus commands ------------------ */ // this is TRANSFORM in the CVC presentation language -class CVC4_EXPORT SimplifyCommand : public Command +class CVC5_EXPORT SimplifyCommand : public Command { protected: api::Term d_term; @@ -949,7 +949,7 @@ class CVC4_EXPORT SimplifyCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SimplifyCommand */ -class CVC4_EXPORT GetValueCommand : public Command +class CVC5_EXPORT GetValueCommand : public Command { protected: std::vector<api::Term> d_terms; @@ -972,7 +972,7 @@ class CVC4_EXPORT GetValueCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetValueCommand */ -class CVC4_EXPORT GetAssignmentCommand : public Command +class CVC5_EXPORT GetAssignmentCommand : public Command { protected: api::Term d_result; @@ -992,7 +992,7 @@ class CVC4_EXPORT GetAssignmentCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetAssignmentCommand */ -class CVC4_EXPORT GetModelCommand : public Command +class CVC5_EXPORT GetModelCommand : public Command { public: GetModelCommand(); @@ -1014,7 +1014,7 @@ class CVC4_EXPORT GetModelCommand : public Command }; /* class GetModelCommand */ /** The command to block models. */ -class CVC4_EXPORT BlockModelCommand : public Command +class CVC5_EXPORT BlockModelCommand : public Command { public: BlockModelCommand(); @@ -1030,7 +1030,7 @@ class CVC4_EXPORT BlockModelCommand : public Command }; /* class BlockModelCommand */ /** The command to block model values. */ -class CVC4_EXPORT BlockModelValuesCommand : public Command +class CVC5_EXPORT BlockModelValuesCommand : public Command { public: BlockModelValuesCommand(const std::vector<api::Term>& terms); @@ -1050,7 +1050,7 @@ class CVC4_EXPORT BlockModelValuesCommand : public Command std::vector<api::Term> d_terms; }; /* class BlockModelValuesCommand */ -class CVC4_EXPORT GetProofCommand : public Command +class CVC5_EXPORT GetProofCommand : public Command { public: GetProofCommand(); @@ -1072,7 +1072,7 @@ class CVC4_EXPORT GetProofCommand : public Command std::string d_result; }; /* class GetProofCommand */ -class CVC4_EXPORT GetInstantiationsCommand : public Command +class CVC5_EXPORT GetInstantiationsCommand : public Command { public: GetInstantiationsCommand(); @@ -1091,7 +1091,7 @@ class CVC4_EXPORT GetInstantiationsCommand : public Command api::Solver* d_solver; }; /* class GetInstantiationsCommand */ -class CVC4_EXPORT GetSynthSolutionCommand : public Command +class CVC5_EXPORT GetSynthSolutionCommand : public Command { public: GetSynthSolutionCommand(); @@ -1119,7 +1119,7 @@ class CVC4_EXPORT GetSynthSolutionCommand : public Command * find a predicate P, then the output response of this command is: (define-fun * s () Bool P) */ -class CVC4_EXPORT GetInterpolCommand : public Command +class CVC5_EXPORT GetInterpolCommand : public Command { public: GetInterpolCommand(const std::string& name, api::Term conj); @@ -1169,7 +1169,7 @@ class CVC4_EXPORT GetInterpolCommand : public Command * A grammar G can be optionally provided to indicate the syntactic restrictions * on the possible solutions returned. */ -class CVC4_EXPORT GetAbductCommand : public Command +class CVC5_EXPORT GetAbductCommand : public Command { public: GetAbductCommand(const std::string& name, api::Term conj); @@ -1208,7 +1208,7 @@ class CVC4_EXPORT GetAbductCommand : public Command api::Term d_result; }; /* class GetAbductCommand */ -class CVC4_EXPORT GetQuantifierEliminationCommand : public Command +class CVC5_EXPORT GetQuantifierEliminationCommand : public Command { protected: api::Term d_term; @@ -1234,7 +1234,7 @@ class CVC4_EXPORT GetQuantifierEliminationCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetQuantifierEliminationCommand */ -class CVC4_EXPORT GetUnsatAssumptionsCommand : public Command +class CVC5_EXPORT GetUnsatAssumptionsCommand : public Command { public: GetUnsatAssumptionsCommand(); @@ -1253,7 +1253,7 @@ class CVC4_EXPORT GetUnsatAssumptionsCommand : public Command std::vector<api::Term> d_result; }; /* class GetUnsatAssumptionsCommand */ -class CVC4_EXPORT GetUnsatCoreCommand : public Command +class CVC5_EXPORT GetUnsatCoreCommand : public Command { public: GetUnsatCoreCommand(); @@ -1277,7 +1277,7 @@ class CVC4_EXPORT GetUnsatCoreCommand : public Command std::vector<api::Term> d_result; }; /* class GetUnsatCoreCommand */ -class CVC4_EXPORT GetAssertionsCommand : public Command +class CVC5_EXPORT GetAssertionsCommand : public Command { protected: std::string d_result; @@ -1297,7 +1297,7 @@ class CVC4_EXPORT GetAssertionsCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetAssertionsCommand */ -class CVC4_EXPORT SetBenchmarkStatusCommand : public Command +class CVC5_EXPORT SetBenchmarkStatusCommand : public Command { protected: BenchmarkStatus d_status; @@ -1317,7 +1317,7 @@ class CVC4_EXPORT SetBenchmarkStatusCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SetBenchmarkStatusCommand */ -class CVC4_EXPORT SetBenchmarkLogicCommand : public Command +class CVC5_EXPORT SetBenchmarkLogicCommand : public Command { protected: std::string d_logic; @@ -1336,7 +1336,7 @@ class CVC4_EXPORT SetBenchmarkLogicCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SetBenchmarkLogicCommand */ -class CVC4_EXPORT SetInfoCommand : public Command +class CVC5_EXPORT SetInfoCommand : public Command { protected: std::string d_flag; @@ -1358,7 +1358,7 @@ class CVC4_EXPORT SetInfoCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SetInfoCommand */ -class CVC4_EXPORT GetInfoCommand : public Command +class CVC5_EXPORT GetInfoCommand : public Command { protected: std::string d_flag; @@ -1381,7 +1381,7 @@ class CVC4_EXPORT GetInfoCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetInfoCommand */ -class CVC4_EXPORT SetOptionCommand : public Command +class CVC5_EXPORT SetOptionCommand : public Command { protected: std::string d_flag; @@ -1403,7 +1403,7 @@ class CVC4_EXPORT SetOptionCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class SetOptionCommand */ -class CVC4_EXPORT GetOptionCommand : public Command +class CVC5_EXPORT GetOptionCommand : public Command { protected: std::string d_flag; @@ -1426,7 +1426,7 @@ class CVC4_EXPORT GetOptionCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class GetOptionCommand */ -class CVC4_EXPORT DatatypeDeclarationCommand : public Command +class CVC5_EXPORT DatatypeDeclarationCommand : public Command { private: std::vector<api::Sort> d_datatypes; @@ -1446,7 +1446,7 @@ class CVC4_EXPORT DatatypeDeclarationCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class DatatypeDeclarationCommand */ -class CVC4_EXPORT ResetCommand : public Command +class CVC5_EXPORT ResetCommand : public Command { public: ResetCommand() {} @@ -1460,7 +1460,7 @@ class CVC4_EXPORT ResetCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class ResetCommand */ -class CVC4_EXPORT ResetAssertionsCommand : public Command +class CVC5_EXPORT ResetAssertionsCommand : public Command { public: ResetAssertionsCommand() {} @@ -1474,7 +1474,7 @@ class CVC4_EXPORT ResetAssertionsCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class ResetAssertionsCommand */ -class CVC4_EXPORT QuitCommand : public Command +class CVC5_EXPORT QuitCommand : public Command { public: QuitCommand() {} @@ -1488,7 +1488,7 @@ class CVC4_EXPORT QuitCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class QuitCommand */ -class CVC4_EXPORT CommentCommand : public Command +class CVC5_EXPORT CommentCommand : public Command { std::string d_comment; @@ -1507,7 +1507,7 @@ class CVC4_EXPORT CommentCommand : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class CommentCommand */ -class CVC4_EXPORT CommandSequence : public Command +class CVC5_EXPORT CommandSequence : public Command { protected: /** All the commands to be executed (in sequence) */ @@ -1545,7 +1545,7 @@ class CVC4_EXPORT CommandSequence : public Command OutputLanguage language = language::output::LANG_AUTO) const override; }; /* class CommandSequence */ -class CVC4_EXPORT DeclarationSequence : public CommandSequence +class CVC5_EXPORT DeclarationSequence : public CommandSequence { void toStream( std::ostream& out, diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 59081f63e..860caffa8 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -24,7 +24,7 @@ #include <vector> #include "context/cdhashmap_forward.h" -#include "cvc4_export.h" +#include "cvc5_export.h" #include "options/options.h" #include "smt/output_manager.h" #include "smt/smt_mode.h" @@ -119,7 +119,7 @@ namespace theory { /* -------------------------------------------------------------------------- */ -class CVC4_EXPORT SmtEngine +class CVC5_EXPORT SmtEngine { friend class ::cvc5::api::Solver; friend class ::cvc5::smt::SmtEngineState; @@ -243,18 +243,18 @@ class CVC4_EXPORT SmtEngine * to a state where its options were prior to parsing but after e.g. * reading command line options. */ - void notifyStartParsing(const std::string& filename) CVC4_EXPORT; + void notifyStartParsing(const std::string& filename) CVC5_EXPORT; /** return the input name (if any) */ const std::string& getFilename() const; /** * Helper method for the API to put the last check result into the statistics. */ - void setResultStatistic(const std::string& result) CVC4_EXPORT; + void setResultStatistic(const std::string& result) CVC5_EXPORT; /** * Helper method for the API to put the total runtime into the statistics. */ - void setTotalTimeStatistic(double seconds) CVC4_EXPORT; + void setTotalTimeStatistic(double seconds) CVC5_EXPORT; /** * Get the model (only if immediately preceded by a SAT or NOT_ENTAILED diff --git a/src/theory/CMakeLists.txt b/src/theory/CMakeLists.txt index a476592ce..8cc6b9f15 100644 --- a/src/theory/CMakeLists.txt +++ b/src/theory/CMakeLists.txt @@ -13,7 +13,7 @@ # The build system configuration. ## -libcvc4_add_sources(GENERATED +libcvc5_add_sources(GENERATED rewriter_tables.h theory_traits.h type_enumerator.cpp diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp index 536a38739..f343ce56a 100644 --- a/src/theory/arith/approx_simplex.cpp +++ b/src/theory/arith/approx_simplex.cpp @@ -18,12 +18,13 @@ #include "theory/arith/approx_simplex.h" #include <math.h> + #include <cfloat> #include <cmath> #include <unordered_set> +#include "base/cvc5config.h" #include "base/output.h" -#include "cvc4autoconfig.h" #include "smt/smt_statistics_registry.h" #include "theory/arith/constraint.h" #include "theory/arith/cut_log.h" diff --git a/src/theory/arith/cut_log.cpp b/src/theory/arith/cut_log.cpp index 4cdd242db..28fd80acc 100644 --- a/src/theory/arith/cut_log.cpp +++ b/src/theory/arith/cut_log.cpp @@ -16,17 +16,19 @@ * \todo document this file */ +#include "theory/arith/cut_log.h" + +#include <limits.h> +#include <math.h> + #include <cmath> #include <iomanip> -#include <limits.h> #include <map> -#include <math.h> +#include "base/cvc5config.h" #include "base/output.h" -#include "cvc4autoconfig.h" #include "theory/arith/approx_simplex.h" #include "theory/arith/constraint.h" -#include "theory/arith/cut_log.h" #include "theory/arith/normal_form.h" #include "util/ostream_util.h" diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h index 5929bbd5a..7f0e2e586 100644 --- a/src/theory/arith/cut_log.h +++ b/src/theory/arith/cut_log.h @@ -20,9 +20,10 @@ #pragma once -#include <unordered_map> #include <map> +#include <memory> #include <set> +#include <unordered_map> #include "expr/kind.h" #include "theory/arith/arithvar.h" diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp index 4c050b3f0..90276f8b1 100644 --- a/src/theory/bv/bv_subtheory_algebraic.cpp +++ b/src/theory/bv/bv_subtheory_algebraic.cpp @@ -979,5 +979,5 @@ Node mergeExplanations(TNode expl1, TNode expl2) { } } // namespace bv -} /* namespace CVc4::theory */ +} // namespace theory } // namespace cvc5 diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h index 9d18d5145..107093a5c 100644 --- a/src/theory/logic_info.h +++ b/src/theory/logic_info.h @@ -22,7 +22,7 @@ #include <string> #include <vector> -#include "cvc4_export.h" +#include "cvc5_export.h" #include "theory/theory_id.h" namespace cvc5 { @@ -42,7 +42,7 @@ namespace cvc5 { * (e.g., for communicating to the SmtEngine which theories should be used, * rather than having to provide an SMT-LIB string). */ -class CVC4_EXPORT LogicInfo +class CVC5_EXPORT LogicInfo { mutable std::string d_logicString; /**< an SMT-LIB-like logic string */ std::vector<bool> d_theories; /**< set of active theories */ diff --git a/src/theory/quantifiers/term_tuple_enumerator.cpp b/src/theory/quantifiers/term_tuple_enumerator.cpp index 431156c03..b75ebe288 100644 --- a/src/theory/quantifiers/term_tuple_enumerator.cpp +++ b/src/theory/quantifiers/term_tuple_enumerator.cpp @@ -36,7 +36,7 @@ namespace cvc5 { template <typename T> -static CVC5ostream& operator<<(CVC5ostream& out, const std::vector<T>& v) +static Cvc5ostream& operator<<(Cvc5ostream& out, const std::vector<T>& v) { out << "[ "; std::copy(v.begin(), v.end(), std::ostream_iterator<T>(out, " ")); diff --git a/src/theory/sets/cardinality_extension.cpp b/src/theory/sets/cardinality_extension.cpp index a9a7429b4..ec5abfacc 100644 --- a/src/theory/sets/cardinality_extension.cpp +++ b/src/theory/sets/cardinality_extension.cpp @@ -115,7 +115,7 @@ void CardinalityExtension::checkCardinalityExtended(TypeNode& t) if (it == d_univProxy.end()) { - // Force cvc4 to build the cardinality graph for the universe set + // Force cvc5 to build the cardinality graph for the universe set proxy = d_treg.getProxy(univ); d_univProxy[univ] = proxy; } diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index e495fd4d6..79a44f426 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -20,7 +20,7 @@ configure_file(rational.h.in rational.h) configure_file(integer.h.in integer.h) configure_file(real_algebraic_number.h.in real_algebraic_number.h) -libcvc4_add_sources( +libcvc5_add_sources( abstract_value.cpp abstract_value.h bin_heap.h @@ -84,13 +84,13 @@ libcvc4_add_sources( ) if(CVC5_USE_CLN_IMP) - libcvc4_add_sources(rational_cln_imp.cpp integer_cln_imp.cpp) + libcvc5_add_sources(rational_cln_imp.cpp integer_cln_imp.cpp) endif() if(CVC5_USE_GMP_IMP) - libcvc4_add_sources(rational_gmp_imp.cpp integer_gmp_imp.cpp) + libcvc5_add_sources(rational_gmp_imp.cpp integer_gmp_imp.cpp) endif() if(CVC5_USE_POLY_IMP) - libcvc4_add_sources(real_algebraic_number_poly_imp.cpp real_algebraic_number_poly_imp.h) + libcvc5_add_sources(real_algebraic_number_poly_imp.cpp real_algebraic_number_poly_imp.h) endif() diff --git a/src/util/integer.h.in b/src/util/integer.h.in index cfcef4ae2..3fb53a835 100644 --- a/src/util/integer.h.in +++ b/src/util/integer.h.in @@ -13,7 +13,7 @@ * A multi-precision integer constant. */ -// these gestures are used to avoid a public header dependence on cvc4autoconfig.h +// these gestures are used to avoid a public header dependence on base/cvc5config.h #if @CVC5_NEED_INT64_T_OVERLOADS@ # define CVC5_NEED_INT64_T_OVERLOADS @@ -28,14 +28,8 @@ #ifdef CVC5_CLN_IMP # include "util/integer_cln_imp.h" -# if SWIG - %include "util/integer_cln_imp.h" -# endif /* SWIG */ #endif /* CVC5_CLN_IMP */ #ifdef CVC5_GMP_IMP # include "util/integer_gmp_imp.h" -# if SWIG - %include "util/integer_gmp_imp.h" -# endif /* SWIG */ #endif /* CVC5_GMP_IMP */ diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp index f54630d23..a9e4f6f0a 100644 --- a/src/util/integer_cln_imp.cpp +++ b/src/util/integer_cln_imp.cpp @@ -15,7 +15,7 @@ #include <sstream> #include <string> -#include "cvc4autoconfig.h" +#include "base/cvc5config.h" #include "util/integer.h" #ifndef CVC5_CLN_IMP diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 303567dc6..80bc406ee 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -29,13 +29,13 @@ #include <string> #include "base/exception.h" -#include "cvc4_export.h" // remove when Cvc language support is removed +#include "cvc5_export.h" // remove when Cvc language support is removed namespace cvc5 { class Rational; -class CVC4_EXPORT Integer +class CVC5_EXPORT Integer { friend class cvc5::Rational; diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp index 52e408a37..f33a90408 100644 --- a/src/util/integer_gmp_imp.cpp +++ b/src/util/integer_gmp_imp.cpp @@ -13,15 +13,13 @@ * A multi-precision rational constant. */ -#include "util/integer.h" - #include <cmath> #include <sstream> #include <string> -#include "cvc4autoconfig.h" - #include "base/check.h" +#include "base/cvc5config.h" +#include "util/integer.h" #include "util/rational.h" #ifndef CVC5_GMP_IMP diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index f2d568d13..ff2ea9815 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -23,13 +23,13 @@ #include <iosfwd> #include <string> -#include "cvc4_export.h" // remove when Cvc language support is removed +#include "cvc5_export.h" // remove when Cvc language support is removed namespace cvc5 { class Rational; -class CVC4_EXPORT Integer +class CVC5_EXPORT Integer { friend class cvc5::Rational; diff --git a/src/util/rational.h.in b/src/util/rational.h.in index c8b673d7e..981fceab2 100644 --- a/src/util/rational.h.in +++ b/src/util/rational.h.in @@ -13,7 +13,7 @@ * A multi-precision rational constant. */ -// these gestures are used to avoid a public header dependence on cvc4autoconfig.h +// these gestures are used to avoid a public header dependence on base/cvc5config.h #if @CVC5_NEED_INT64_T_OVERLOADS@ # define CVC5_NEED_INT64_T_OVERLOADS @@ -28,14 +28,8 @@ #ifdef CVC5_CLN_IMP # include "util/rational_cln_imp.h" -# if SWIG - %include "util/rational_cln_imp.h" -# endif /* SWIG */ #endif /* CVC5_CLN_IMP */ #ifdef CVC5_GMP_IMP # include "util/rational_gmp_imp.h" -# if SWIG - %include "util/rational_gmp_imp.h" -# endif /* SWIG */ #endif /* CVC5_GMP_IMP */ diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp index 93816bd20..728b2d97e 100644 --- a/src/util/rational_cln_imp.cpp +++ b/src/util/rational_cln_imp.cpp @@ -12,12 +12,11 @@ * * A multi-precision rational constant. */ -#include "util/rational.h" - #include <sstream> #include <string> -#include "cvc4autoconfig.h" +#include "base/cvc5config.h" +#include "util/rational.h" #ifndef CVC5_CLN_IMP #error "This source should only ever be built if CVC5_CLN_IMP is on !" diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index 9745bbdad..67e73f7e9 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -31,7 +31,7 @@ #include <string> #include "base/exception.h" -#include "cvc4_export.h" // remove when Cvc language support is removed +#include "cvc5_export.h" // remove when Cvc language support is removed #include "util/integer.h" #include "util/maybe.h" @@ -52,7 +52,7 @@ namespace cvc5 { * in danger of invoking the char* constructor, from whence you will segfault. */ -class CVC4_EXPORT Rational +class CVC5_EXPORT Rational { public: /** @@ -337,7 +337,7 @@ struct RationalHashFunction inline size_t operator()(const cvc5::Rational& r) const { return r.hash(); } }; /* struct RationalHashFunction */ -std::ostream& operator<<(std::ostream& os, const Rational& n) CVC4_EXPORT; +std::ostream& operator<<(std::ostream& os, const Rational& n) CVC5_EXPORT; } // namespace cvc5 diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp index 24e6e96d7..0997b8b09 100644 --- a/src/util/rational_gmp_imp.cpp +++ b/src/util/rational_gmp_imp.cpp @@ -12,15 +12,14 @@ * * A multi-precision rational constant. */ -#include "util/rational.h" - #include <cmath> #include <sstream> #include <string> -#include "cvc4autoconfig.h" +#include "base/cvc5config.h" +#include "util/rational.h" -#ifndef CVC5_GMP_IMP // Make sure this comes after cvc4autoconfig.h +#ifndef CVC5_GMP_IMP // Make sure this comes after base/cvc5config.h #error "This source should only ever be built if CVC5_GMP_IMP is on !" #endif /* CVC5_GMP_IMP */ diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index 0961adc73..fd7492a87 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -22,7 +22,7 @@ #include <string> -#include "cvc4_export.h" // remove when Cvc language support is removed +#include "cvc5_export.h" // remove when Cvc language support is removed #include "util/gmp_util.h" #include "util/integer.h" #include "util/maybe.h" @@ -44,7 +44,7 @@ namespace cvc5 { * in danger of invoking the char* constructor, from whence you will segfault. */ -class CVC4_EXPORT Rational +class CVC5_EXPORT Rational { public: /** @@ -327,7 +327,7 @@ struct RationalHashFunction inline size_t operator()(const cvc5::Rational& r) const { return r.hash(); } }; /* struct RationalHashFunction */ -std::ostream& operator<<(std::ostream& os, const Rational& n) CVC4_EXPORT; +std::ostream& operator<<(std::ostream& os, const Rational& n) CVC5_EXPORT; } // namespace cvc5 diff --git a/src/util/real_algebraic_number.h.in b/src/util/real_algebraic_number.h.in index 8eb8b35fb..077c260f6 100644 --- a/src/util/real_algebraic_number.h.in +++ b/src/util/real_algebraic_number.h.in @@ -13,7 +13,7 @@ * A real algebraic number constant. */ -// these gestures are used to avoid a public header dependence on cvc4autoconfig.h +// these gestures are used to avoid a public header dependence on base/cvc5config.h #if /* use libpoly */ @CVC5_USE_POLY_IMP@ # define CVC5_POLY_IMP diff --git a/src/util/real_algebraic_number_poly_imp.cpp b/src/util/real_algebraic_number_poly_imp.cpp index 736970129..58af26193 100644 --- a/src/util/real_algebraic_number_poly_imp.cpp +++ b/src/util/real_algebraic_number_poly_imp.cpp @@ -13,10 +13,10 @@ * Implementation of RealAlgebraicNumber based on libpoly. */ -#include "cvc4autoconfig.h" +#include "base/cvc5config.h" #include "util/real_algebraic_number.h" -#ifndef CVC5_POLY_IMP // Make sure this comes after cvc4autoconfig.h +#ifndef CVC5_POLY_IMP // Make sure this comes after base/cvc5config.h #error "This source should only ever be built if CVC5_POLY_IMP is on!" #endif /* CVC5_POLY_IMP */ diff --git a/src/util/safe_print.h b/src/util/safe_print.h index ba0704d9c..e3280bb55 100644 --- a/src/util/safe_print.h +++ b/src/util/safe_print.h @@ -43,7 +43,7 @@ #include <cstring> #include <string> -#include "cvc4_export.h" +#include "cvc5_export.h" namespace cvc5 { @@ -52,7 +52,7 @@ namespace cvc5 { * signal handler. */ template <size_t N> -void CVC4_EXPORT safe_print(int fd, const char (&msg)[N]) +void CVC5_EXPORT safe_print(int fd, const char (&msg)[N]) { ssize_t nb = N - 1; if (write(fd, msg, nb) != nb) { @@ -96,7 +96,7 @@ auto toStringImpl(const T& obj, int) -> decltype(toString(obj)) * @param obj The object to print */ template <typename T> -void CVC4_EXPORT safe_print(int fd, const T& obj) +void CVC5_EXPORT safe_print(int fd, const T& obj) { const char* s = toStringImpl(obj, /* prefer the method that uses `toString()` */ 0); @@ -108,25 +108,25 @@ void CVC4_EXPORT safe_print(int fd, const T& obj) } template <> -void CVC4_EXPORT safe_print(int fd, const std::string& msg); +void CVC5_EXPORT safe_print(int fd, const std::string& msg); template <> -void CVC4_EXPORT safe_print(int fd, const int64_t& _i); +void CVC5_EXPORT safe_print(int fd, const int64_t& _i); template <> -void CVC4_EXPORT safe_print(int fd, const int32_t& i); +void CVC5_EXPORT safe_print(int fd, const int32_t& i); template <> -void CVC4_EXPORT safe_print(int fd, const uint64_t& _i); +void CVC5_EXPORT safe_print(int fd, const uint64_t& _i); template <> -void CVC4_EXPORT safe_print(int fd, const uint32_t& i); +void CVC5_EXPORT safe_print(int fd, const uint32_t& i); template <> -void CVC4_EXPORT safe_print(int fd, const double& _d); +void CVC5_EXPORT safe_print(int fd, const double& _d); template <> -void CVC4_EXPORT safe_print(int fd, const float& f); +void CVC5_EXPORT safe_print(int fd, const float& f); template <> -void CVC4_EXPORT safe_print(int fd, const bool& b); +void CVC5_EXPORT safe_print(int fd, const bool& b); template <> -void CVC4_EXPORT safe_print(int fd, void* const& addr); +void CVC5_EXPORT safe_print(int fd, void* const& addr); template <> -void CVC4_EXPORT safe_print(int fd, const timespec& t); +void CVC5_EXPORT safe_print(int fd, const timespec& t); /** Prints an integer in hexadecimal. Safe to use in a signal handler. */ void safe_print_hex(int fd, uint64_t i); diff --git a/src/util/unsafe_interrupt_exception.h b/src/util/unsafe_interrupt_exception.h index 72c67d24a..16364cba2 100644 --- a/src/util/unsafe_interrupt_exception.h +++ b/src/util/unsafe_interrupt_exception.h @@ -20,11 +20,11 @@ #define CVC5__UNSAFE_INTERRUPT_EXCEPTION_H #include "base/exception.h" -#include "cvc4_export.h" +#include "cvc5_export.h" namespace cvc5 { -class CVC4_EXPORT UnsafeInterruptException : public cvc5::Exception +class CVC5_EXPORT UnsafeInterruptException : public cvc5::Exception { public: UnsafeInterruptException() : |