From d2e454e0dfc06e16fe0a4228168b21cf1311fc35 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 5 Apr 2021 19:31:28 -0700 Subject: [PATCH] New C++ Api: Rename and move headers. (#6292) --- .github/workflows/ci.yml | 2 +- examples/api/bitvectors.cpp | 4 ++-- examples/api/bitvectors_and_arrays.cpp | 6 +++--- examples/api/combination.cpp | 4 ++-- examples/api/datatypes.cpp | 4 ++-- examples/api/extract.cpp | 4 ++-- examples/api/helloworld.cpp | 4 ++-- examples/api/linear_arith.cpp | 2 +- examples/api/sequences.cpp | 2 +- examples/api/sets.cpp | 4 ++-- examples/api/strings.cpp | 4 ++-- examples/api/sygus-fun.cpp | 2 +- examples/api/sygus-grammar.cpp | 2 +- examples/api/sygus-inv.cpp | 2 +- examples/nra-translate/normalize.cpp | 9 ++++---- examples/nra-translate/smt2info.cpp | 5 ++--- examples/nra-translate/smt2todreal.cpp | 9 ++++---- examples/nra-translate/smt2toisat.cpp | 5 ++--- examples/nra-translate/smt2tomathematica.cpp | 5 ++--- examples/nra-translate/smt2toqepcad.cpp | 5 ++--- examples/nra-translate/smt2toredlog.cpp | 5 ++--- examples/sets-translate/sets_translate.cpp | 9 ++++---- examples/simple_vc_cxx.cpp | 2 +- examples/simple_vc_quant_cxx.cpp | 2 +- examples/translator.cpp | 11 +++++----- src/CMakeLists.txt | 14 ++++++------- src/api/{cvc4cpp.cpp => cpp/cvc5.cpp} | 22 ++++++++------------ src/api/{cvc4cpp.h => cpp/cvc5.h} | 11 +++++----- src/api/{cvc4cppkind.h => cpp/cvc5_kind.h} | 6 +++--- src/api/java/CMakeLists.txt | 2 +- src/api/java/genkinds.py | 2 +- src/api/parsekinds.py | 3 ++- src/api/python/CMakeLists.txt | 2 +- src/api/python/cvc4.pxd | 10 ++++----- src/api/python/genkinds.py.in | 8 +++---- src/expr/symbol_manager.h | 2 +- src/expr/symbol_table.cpp | 2 +- src/fix-install-headers.sh | 7 +++++-- src/main/command_executor.h | 2 +- src/main/driver_unified.cpp | 2 +- src/main/interactive_shell.cpp | 2 +- src/parser/cvc/cvc.h | 2 +- src/parser/input.h | 2 +- src/parser/parse_op.h | 2 +- src/parser/parser.cpp | 2 +- src/parser/parser.h | 2 +- src/parser/parser_builder.cpp | 2 +- src/parser/smt2/Smt2.g | 2 +- src/parser/smt2/smt2.h | 2 +- src/parser/tptp/Tptp.g | 2 +- src/parser/tptp/tptp.cpp | 2 +- src/parser/tptp/tptp.h | 2 +- src/printer/smt2/smt2_printer.cpp | 2 +- src/smt/command.cpp | 2 +- src/smt/command.h | 2 +- test/api/boilerplate.cpp | 2 +- test/api/issue4889.cpp | 2 +- test/api/issue5074.cpp | 2 +- test/api/ouroborous.cpp | 2 +- test/api/reset_assertions.cpp | 2 +- test/api/sep_log_api.cpp | 2 +- test/api/smt2_compliance.cpp | 2 +- test/api/two_solvers.cpp | 2 +- test/unit/main/interactive_shell_black.cpp | 2 +- test/unit/node/node_black.cpp | 2 +- test/unit/parser/parser_black.cpp | 2 +- test/unit/parser/parser_builder_black.cpp | 2 +- test/unit/printer/smt2_printer_black.cpp | 2 +- test/unit/test_api.h | 2 +- test/unit/theory/regexp_operation_black.cpp | 2 +- 70 files changed, 129 insertions(+), 139 deletions(-) rename src/api/{cvc4cpp.cpp => cpp/cvc5.cpp} (99%) rename src/api/{cvc4cpp.h => cpp/cvc5.h} (99%) rename src/api/{cvc4cppkind.h => cpp/cvc5_kind.h} (99%) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 8d8104385..8925b06d9 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -194,7 +194,7 @@ jobs: - name: Install Check run: | make -j2 install - echo -e "#include \nint main() { cvc5::api::Solver s; return 0; }" > /tmp/test.cpp + echo -e "#include \nint main() { cvc5::api::Solver s; return 0; }" > /tmp/test.cpp g++ -std=c++11 /tmp/test.cpp -I install/include -L install/lib -lcvc4 working-directory: build diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp index 043bbf8aa..be9557c99 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/bitvectors.cpp @@ -14,9 +14,9 @@ ** **/ -#include +#include -#include +#include using namespace std; using namespace cvc5::api; diff --git a/examples/api/bitvectors_and_arrays.cpp b/examples/api/bitvectors_and_arrays.cpp index 2bca1eb4c..ca9869503 100644 --- a/examples/api/bitvectors_and_arrays.cpp +++ b/examples/api/bitvectors_and_arrays.cpp @@ -14,10 +14,10 @@ ** **/ -#include -#include +#include -#include +#include +#include using namespace std; using namespace cvc5::api; diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp index 9ea2f55ed..82c2978e6 100644 --- a/examples/api/combination.cpp +++ b/examples/api/combination.cpp @@ -16,9 +16,9 @@ ** The model is displayed using getValue(). **/ -#include +#include -#include +#include using namespace std; using namespace cvc5::api; diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp index 49253e466..f9a1484da 100644 --- a/examples/api/datatypes.cpp +++ b/examples/api/datatypes.cpp @@ -14,9 +14,9 @@ ** An example of using inductive datatypes in CVC4. **/ -#include +#include -#include +#include using namespace cvc5::api; diff --git a/examples/api/extract.cpp b/examples/api/extract.cpp index 760f5d0fe..d2f631d25 100644 --- a/examples/api/extract.cpp +++ b/examples/api/extract.cpp @@ -14,9 +14,9 @@ ** **/ -#include +#include -#include +#include using namespace std; using namespace cvc5::api; diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp index 092e2a79a..b5881f312 100644 --- a/examples/api/helloworld.cpp +++ b/examples/api/helloworld.cpp @@ -14,9 +14,9 @@ ** A very simple CVC4 tutorial example. **/ -#include +#include -#include +#include using namespace cvc5::api; diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp index b56982daa..ee9663455 100644 --- a/examples/api/linear_arith.cpp +++ b/examples/api/linear_arith.cpp @@ -17,7 +17,7 @@ #include -#include "cvc4/api/cvc4cpp.h" +#include using namespace std; using namespace cvc5::api; diff --git a/examples/api/sequences.cpp b/examples/api/sequences.cpp index 3498b3275..39117c090 100644 --- a/examples/api/sequences.cpp +++ b/examples/api/sequences.cpp @@ -14,7 +14,7 @@ ** A simple demonstration of reasoning about sequences with CVC4 via C++ API. **/ -#include +#include #include diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp index 59385896c..c8b8bcc9e 100644 --- a/examples/api/sets.cpp +++ b/examples/api/sets.cpp @@ -14,9 +14,9 @@ ** A simple demonstration of reasoning about sets with CVC4. **/ -#include +#include -#include +#include using namespace std; using namespace cvc5::api; diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp index 53352d266..548d25b81 100644 --- a/examples/api/strings.cpp +++ b/examples/api/strings.cpp @@ -14,9 +14,9 @@ ** A simple demonstration of reasoning about strings with CVC4 via C++ API. **/ -#include +#include -#include +#include using namespace cvc5::api; diff --git a/examples/api/sygus-fun.cpp b/examples/api/sygus-fun.cpp index be4d3e8d5..44e276ddc 100644 --- a/examples/api/sygus-fun.cpp +++ b/examples/api/sygus-fun.cpp @@ -45,7 +45,7 @@ ** (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y)) **/ -#include +#include #include diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp index 61b00f6de..441cfa30c 100644 --- a/examples/api/sygus-grammar.cpp +++ b/examples/api/sygus-grammar.cpp @@ -42,7 +42,7 @@ ** (define-fun id4 ((x Int)) Int (+ x (+ x (- x)))) **/ -#include +#include #include diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp index 56b5a0aaa..5d6789759 100644 --- a/examples/api/sygus-inv.cpp +++ b/examples/api/sygus-inv.cpp @@ -33,7 +33,7 @@ ** (define-fun inv-f ((x Int)) Bool (not (>= x 11))) **/ -#include +#include #include diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp index ba495e1fd..635c369a0 100644 --- a/examples/nra-translate/normalize.cpp +++ b/examples/nra-translate/normalize.cpp @@ -15,6 +15,10 @@ ** \todo document this file **/ +#include +#include +#include + #include #include #include @@ -22,11 +26,6 @@ #include #include -#include -#include -#include -#include - using namespace std; using namespace cvc5; using namespace cvc5::parser; diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp index 1eb4b3d4d..413601769 100644 --- a/examples/nra-translate/smt2info.cpp +++ b/examples/nra-translate/smt2info.cpp @@ -15,15 +15,14 @@ ** \todo document this file **/ +#include + #include #include #include #include #include -#include -#include - using namespace std; using namespace cvc5; using namespace cvc5::parser; diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp index 8139a4d91..62a1f4b5e 100644 --- a/examples/nra-translate/smt2todreal.cpp +++ b/examples/nra-translate/smt2todreal.cpp @@ -15,6 +15,10 @@ ** \todo document this file **/ +#include +#include +#include + #include #include #include @@ -22,11 +26,6 @@ #include #include -#include -#include -#include -#include - using namespace std; using namespace cvc5; using namespace cvc5::parser; diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp index 09b0c69d8..5898e5cff 100644 --- a/examples/nra-translate/smt2toisat.cpp +++ b/examples/nra-translate/smt2toisat.cpp @@ -15,6 +15,8 @@ ** \todo document this file **/ +#include + #include #include #include @@ -22,9 +24,6 @@ #include #include -#include -#include - using namespace std; using namespace cvc5; using namespace cvc5::parser; diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp index 6cb51f17c..b2c73d48e 100644 --- a/examples/nra-translate/smt2tomathematica.cpp +++ b/examples/nra-translate/smt2tomathematica.cpp @@ -15,6 +15,8 @@ ** \todo document this file **/ +#include + #include #include #include @@ -22,9 +24,6 @@ #include #include -#include -#include - using namespace std; using namespace cvc5; using namespace cvc5::parser; diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp index afd468d5d..760a7024c 100644 --- a/examples/nra-translate/smt2toqepcad.cpp +++ b/examples/nra-translate/smt2toqepcad.cpp @@ -15,6 +15,8 @@ ** \todo document this file **/ +#include + #include #include #include @@ -22,9 +24,6 @@ #include #include -#include -#include - using namespace std; using namespace cvc5; using namespace cvc5::parser; diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp index d9bd6012a..dd6fb9bb6 100644 --- a/examples/nra-translate/smt2toredlog.cpp +++ b/examples/nra-translate/smt2toredlog.cpp @@ -15,6 +15,8 @@ ** \todo document this file **/ +#include + #include #include #include @@ -22,9 +24,6 @@ #include #include -#include -#include - using namespace std; using namespace cvc5; using namespace cvc5::parser; diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp index ec95b5f70..0f924072c 100644 --- a/examples/sets-translate/sets_translate.cpp +++ b/examples/sets-translate/sets_translate.cpp @@ -15,7 +15,10 @@ ** \todo document this file **/ -#include // include Boost, a C++ library +#include +#include + +#include // include Boost, a C++ library #include #include #include @@ -23,10 +26,6 @@ #include #include -#include -#include -#include - using namespace std; using namespace cvc5; using namespace cvc5::parser; diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp index b97b86bb8..4042e15cb 100644 --- a/examples/simple_vc_cxx.cpp +++ b/examples/simple_vc_cxx.cpp @@ -16,7 +16,7 @@ ** identical. **/ -#include +#include #include diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp index 73dbfe34f..3d6a6e103 100644 --- a/examples/simple_vc_quant_cxx.cpp +++ b/examples/simple_vc_quant_cxx.cpp @@ -14,7 +14,7 @@ ** A simple demonstration of the C++ interface for quantifiers. **/ -#include +#include #include diff --git a/examples/translator.cpp b/examples/translator.cpp index 4838e06fb..bcdf2b2d2 100644 --- a/examples/translator.cpp +++ b/examples/translator.cpp @@ -15,18 +15,17 @@ ** CVC4's input languages to one of its output languages. **/ +#include +#include +#include +#include + #include #include #include #include -#include #include -#include -#include -#include -#include - using namespace std; using namespace cvc5; using namespace cvc5::language; diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 6c2af8226..04ad27b5c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -13,9 +13,9 @@ libcvc4_add_sources( api/checks.h - api/cvc4cpp.cpp - api/cvc4cpp.h - api/cvc4cppkind.h + api/cpp/cvc5.cpp + api/cpp/cvc5.h + api/cpp/cvc5_kind.h context/backtrackable.h context/cddense_set.h context/cdhashmap.h @@ -1182,14 +1182,14 @@ endif() # Install public API headers install(FILES - api/cvc4cpp.h - api/cvc4cppkind.h + api/cpp/cvc5.h + api/cpp/cvc5_kind.h DESTINATION - ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/api) + ${CMAKE_INSTALL_INCLUDEDIR}/cvc5/) install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4_export.h DESTINATION - ${CMAKE_INSTALL_INCLUDEDIR}/cvc4/) + ${CMAKE_INSTALL_INCLUDEDIR}/cvc5/) # Fix include paths for all public headers. # Note: This is a temporary fix until the new C++ API is in place. diff --git a/src/api/cvc4cpp.cpp b/src/api/cpp/cvc5.cpp similarity index 99% rename from src/api/cvc4cpp.cpp rename to src/api/cpp/cvc5.cpp index 463fe74df..b965d55a6 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cpp/cvc5.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file cvc4cpp.cpp +/*! \file cvc5.cpp ** \verbatim ** Top contributors (to current version): ** Aina Niemetz, Andrew Reynolds, Andres Noetzli @@ -31,7 +31,7 @@ ** consistent behavior (see Solver::mkRealFromStrHelper for an example). **/ -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include #include @@ -2117,7 +2117,7 @@ size_t Term::getNumChildren() const { return d_node->getNumChildren() + 1; } - if(isCastedReal()) + if (isCastedReal()) { return 0; } @@ -2551,23 +2551,19 @@ bool isInteger(const Node& node) } bool isInt32(const Node& node) { - return isInteger(node) - && checkIntegerBounds(getInteger(node)); + return isInteger(node) && checkIntegerBounds(getInteger(node)); } bool isUInt32(const Node& node) { - return isInteger(node) - && checkIntegerBounds(getInteger(node)); + return isInteger(node) && checkIntegerBounds(getInteger(node)); } bool isInt64(const Node& node) { - return isInteger(node) - && checkIntegerBounds(getInteger(node)); + return isInteger(node) && checkIntegerBounds(getInteger(node)); } bool isUInt64(const Node& node) { - return isInteger(node) - && checkIntegerBounds(getInteger(node)); + return isInteger(node) && checkIntegerBounds(getInteger(node)); } } // namespace detail @@ -6384,8 +6380,8 @@ Term Solver::getQuantifierEliminationDisjunct(const Term& q) const CVC4_API_TRY_CATCH_BEGIN; CVC4_API_SOLVER_CHECK_TERM(q); //////// all checks before this line - return Term( - this, d_smtEngine->getQuantifierElimination(q.getNode(), false, true)); + return Term(this, + d_smtEngine->getQuantifierElimination(q.getNode(), false, true)); //////// CVC4_API_TRY_CATCH_END; } diff --git a/src/api/cvc4cpp.h b/src/api/cpp/cvc5.h similarity index 99% rename from src/api/cvc4cpp.h rename to src/api/cpp/cvc5.h index 8f4977b28..ec2f32c6e 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cpp/cvc5.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file cvc4cpp.h +/*! \file cvc5.h ** \verbatim ** Top contributors (to current version): ** Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed @@ -16,10 +16,8 @@ #include "cvc4_export.h" -#ifndef CVC4__API__CVC4CPP_H -#define CVC4__API__CVC4CPP_H - -#include "api/cvc4cppkind.h" +#ifndef CVC5__API__CVC5_H +#define CVC5__API__CVC5_H #include #include @@ -30,6 +28,8 @@ #include #include +#include "api/cpp/cvc5_kind.h" + namespace cvc5 { template @@ -3542,7 +3542,6 @@ class CVC4_EXPORT Solver */ void printSynthSolution(std::ostream& out) const; - // !!! This is only temporarily available until the parser is fully migrated // to the new API. !!! SmtEngine* getSmtEngine(void) const; diff --git a/src/api/cvc4cppkind.h b/src/api/cpp/cvc5_kind.h similarity index 99% rename from src/api/cvc4cppkind.h rename to src/api/cpp/cvc5_kind.h index eec90147e..188c8d0b6 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cpp/cvc5_kind.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file cvc4cppkind.h +/*! \file cvc5_kind.h ** \verbatim ** Top contributors (to current version): ** Aina Niemetz, Andrew Reynolds, Makai Mann @@ -16,8 +16,8 @@ #include "cvc4_export.h" -#ifndef CVC4__API__CVC4CPPKIND_H -#define CVC4__API__CVC4CPPKIND_H +#ifndef CVC5__API__CVC5_KIND_H +#define CVC5__API__CVC5_KIND_H #include diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index 9c25e7393..38c12aa5c 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -19,7 +19,7 @@ add_custom_target( COMMAND "${PYTHON_EXECUTABLE}" "${CMAKE_CURRENT_LIST_DIR}/genkinds.py" - --kinds-header "${PROJECT_SOURCE_DIR}/src/api/cvc4cppkind.h" + --kinds-header "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h" --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc/Kind" DEPENDS genkinds.py diff --git a/src/api/java/genkinds.py b/src/api/java/genkinds.py index 6b2e0a5af..8dc3c84d8 100644 --- a/src/api/java/genkinds.py +++ b/src/api/java/genkinds.py @@ -11,7 +11,7 @@ # """ -This script reads CVC4/src/api/cvc4cppkind.h and generates +This script reads CVC4/src/api/cpp/cvc5_kind.h and generates cvc/Kind.java file which declare all the CVC4 kinds. """ diff --git a/src/api/parsekinds.py b/src/api/parsekinds.py index 89116ff0e..1ae697a80 100644 --- a/src/api/parsekinds.py +++ b/src/api/parsekinds.py @@ -12,7 +12,7 @@ """ This script implements KindsParser which -parses the header file CVC4/src/api/cvc4cppkind.h +parses the header file CVC4/src/api/cpp/cvc5_kind.h The script is aware of the '#if 0' pattern and will ignore kinds declared between '#if 0' and '#endif'. It can also @@ -21,6 +21,7 @@ handle nested '#if 0' pairs. from collections import OrderedDict + ##################### Useful Constants ################ OCB = '{' CCB = '}' diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index ec156e50e..2311b63f4 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -33,7 +33,7 @@ add_custom_target( COMMAND "${PYTHON_EXECUTABLE}" "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py" - --kinds-header "${PROJECT_SOURCE_DIR}/src/api/cvc4cppkind.h" + --kinds-header "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h" --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc4kinds" DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py" diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index 8bcd618cf..8072dbfa7 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -14,12 +14,12 @@ cdef extern from "" namespace "std": ostream cout -cdef extern from "api/cvc4cpp.h" namespace "CVC4": +cdef extern from "api/cpp/cvc5.h" namespace "CVC4": cdef cppclass Options: pass -cdef extern from "api/cvc4cpp.h" namespace "cvc5::api": +cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": cdef cppclass Datatype: Datatype() except + DatatypeConstructor operator[](size_t idx) except + @@ -199,7 +199,7 @@ cdef extern from "api/cvc4cpp.h" namespace "cvc5::api": Term mkAbstractValue(const string& index) except + Term mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) except + Term mkConst(Sort sort, const string& symbol) except + - # default value for symbol defined in cvc4cpp.h + # default value for symbol defined in cpp/cvc5.h Term mkConst(Sort sort) except + Term mkVar(Sort sort, const string& symbol) except + DatatypeConstructorDecl mkDatatypeConstructorDecl(const string& name) except + @@ -209,7 +209,7 @@ cdef extern from "api/cvc4cpp.h" namespace "cvc5::api": DatatypeDecl mkDatatypeDecl(const string& name, Sort param, bint isCoDatatype) except + DatatypeDecl mkDatatypeDecl(const string& name, vector[Sort]& params) except + DatatypeDecl mkDatatypeDecl(const string& name, vector[Sort]& params, bint isCoDatatype) except + - # default value for symbol defined in cvc4cpp.h + # default value for symbol defined in cpp/cvc5.h Term mkVar(Sort sort) except + Term simplify(const Term& t) except + void assertFormula(Term term) except + @@ -354,7 +354,7 @@ cdef extern from "api/cvc4cpp.h" namespace "cvc5::api": size_t operator()(const Term & t) except + -cdef extern from "api/cvc4cpp.h" namespace "cvc5::api::RoundingMode": +cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api::RoundingMode": cdef RoundingMode ROUND_NEAREST_TIES_TO_EVEN, cdef RoundingMode ROUND_TOWARD_POSITIVE, cdef RoundingMode ROUND_TOWARD_NEGATIVE, diff --git a/src/api/python/genkinds.py.in b/src/api/python/genkinds.py.in index 7fb84b43c..4c5fc818a 100644 --- a/src/api/python/genkinds.py.in +++ b/src/api/python/genkinds.py.in @@ -10,7 +10,7 @@ ## directory for licensing information. ## """ -This script reads CVC4/src/api/cvc4cppkind.h and generates +This script reads CVC4/src/api/cpp/cvc5_kind.h and generates .pxd and .pxi files which declare all the CVC4 kinds and implement a Python wrapper for kinds, respectively. The default names are kinds.pxd / kinds.pxi, but the name is @@ -40,13 +40,13 @@ PYCOMMENT = '#' CDEF_KIND = " cdef Kind " KINDS_PXD_TOP = \ -r"""cdef extern from "api/cvc4cppkind.h" namespace "cvc5::api": +r"""cdef extern from "api/cpp/cvc5_kind.h" namespace "cvc5::api": cdef cppclass Kind: pass -# Kind declarations: See cvc4cppkind.h for additional information -cdef extern from "api/cvc4cppkind.h" namespace "cvc5::api::Kind": +# Kind declarations: See cpp/cvc5_kind.h for additional information +cdef extern from "api/cpp/cvc5_kind.h" namespace "cvc5::api::Kind": """ KINDS_PXI_TOP = \ diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h index 0a9248f78..4ff307bc2 100644 --- a/src/expr/symbol_manager.h +++ b/src/expr/symbol_manager.h @@ -21,7 +21,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "cvc4_export.h" #include "expr/symbol_table.h" diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index 1c513fea4..9e60680c7 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -23,7 +23,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "context/cdhashmap.h" #include "context/cdhashset.h" #include "context/context.h" diff --git a/src/fix-install-headers.sh b/src/fix-install-headers.sh index 7f9fa5d5b..49bade416 100755 --- a/src/fix-install-headers.sh +++ b/src/fix-install-headers.sh @@ -4,5 +4,8 @@ set -e -o pipefail dir="$DESTDIR$1" -find "$dir/include/cvc4/" -type f \ - -exec sed -i'' -e 's/include.*"\(.*\)"/include /' {} + +find "$dir/include/cvc5/" -type f \ + -exec sed -i'' -e 's/include.*"api\/cpp\/\(.*\)"/include /' {} + + +find "$dir/include/cvc5/" -type f \ + -exec sed -i'' -e 's/"cvc4_export.h"//' {} + diff --git a/src/main/command_executor.h b/src/main/command_executor.h index d2117e109..1b68e01e6 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -18,7 +18,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "expr/symbol_manager.h" #include "options/options.h" diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 6f9377a33..ec141d13a 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -23,7 +23,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "base/configuration.h" #include "base/output.h" #include "cvc4autoconfig.h" diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index 44fee3eb5..0ddd8707a 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -35,7 +35,7 @@ # endif /* HAVE_EXT_STDIO_FILEBUF_H */ #endif /* HAVE_LIBEDITLINE */ -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "base/check.h" #include "base/output.h" #include "expr/symbol_manager.h" diff --git a/src/parser/cvc/cvc.h b/src/parser/cvc/cvc.h index acfcc1d17..ad3642e20 100644 --- a/src/parser/cvc/cvc.h +++ b/src/parser/cvc/cvc.h @@ -19,7 +19,7 @@ #ifndef CVC4__PARSER__CVC_H #define CVC4__PARSER__CVC_H -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "parser/parser.h" namespace cvc5 { diff --git a/src/parser/input.h b/src/parser/input.h index fcaa36932..d54cb95ab 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -25,7 +25,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "cvc4_export.h" #include "options/language.h" #include "parser/parser_exception.h" diff --git a/src/parser/parse_op.h b/src/parser/parse_op.h index 1163ab6be..592fce4f7 100644 --- a/src/parser/parse_op.h +++ b/src/parser/parse_op.h @@ -19,7 +19,7 @@ #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" namespace cvc5 { diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 6725b5ec7..b4e4639ba 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -23,7 +23,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "base/check.h" #include "base/output.h" #include "expr/kind.h" diff --git a/src/parser/parser.h b/src/parser/parser.h index 173b98a9c..79b975fc4 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -23,7 +23,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "cvc4_export.h" #include "expr/kind.h" #include "expr/symbol_manager.h" diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index b0b6a03e7..933be7a51 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -19,7 +19,7 @@ #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "base/check.h" #include "cvc/cvc.h" #include "options/options.h" diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 6adc6275a..3302533e6 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -102,7 +102,7 @@ namespace cvc5 { #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "base/output.h" #include "options/set_language.h" #include "parser/antlr_input.h" diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 5ad508868..645209c61 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -25,7 +25,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "parser/parse_op.h" #include "parser/parser.h" #include "theory/logic_info.h" diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 030330748..f6b845212 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -100,7 +100,7 @@ using namespace cvc5::parser; #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "base/output.h" #include "parser/antlr_input.h" #include "parser/parser.h" diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 7a3a47ec9..2f770a58d 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -18,7 +18,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "base/check.h" #include "options/options.h" #include "parser/parser.h" diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index b91418bd0..ab2e0db51 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -22,7 +22,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "parser/parse_op.h" #include "parser/parser.h" #include "util/hash.h" diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index a2a45de81..b0019d272 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -22,7 +22,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/node_manager_attributes.h" diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 4a6efe713..a8d9afdfa 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -23,7 +23,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "base/check.h" #include "base/output.h" #include "expr/expr_iomanip.h" diff --git a/src/smt/command.h b/src/smt/command.h index 6c3b4f0e4..e92594736 100644 --- a/src/smt/command.h +++ b/src/smt/command.h @@ -27,7 +27,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "cvc4_export.h" #include "options/language.h" diff --git a/test/api/boilerplate.cpp b/test/api/boilerplate.cpp index cc71a48ae..73abb3e19 100644 --- a/test/api/boilerplate.cpp +++ b/test/api/boilerplate.cpp @@ -19,7 +19,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" using namespace cvc5::api; using namespace std; diff --git a/test/api/issue4889.cpp b/test/api/issue4889.cpp index 2b57781b6..ed2340c18 100644 --- a/test/api/issue4889.cpp +++ b/test/api/issue4889.cpp @@ -12,7 +12,7 @@ ** \brief Test for issue #4889 **/ -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" using namespace cvc5::api; diff --git a/test/api/issue5074.cpp b/test/api/issue5074.cpp index ab58797ee..d0000c710 100644 --- a/test/api/issue5074.cpp +++ b/test/api/issue5074.cpp @@ -12,7 +12,7 @@ ** \brief Test for issue #5074 **/ -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" using namespace cvc5::api; diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp index 8686cbeb1..96698b4d2 100644 --- a/test/api/ouroborous.cpp +++ b/test/api/ouroborous.cpp @@ -28,7 +28,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "options/set_language.h" #include "parser/parser.h" #include "parser/parser_builder.h" diff --git a/test/api/reset_assertions.cpp b/test/api/reset_assertions.cpp index 46941e36d..5e31b0b5e 100644 --- a/test/api/reset_assertions.cpp +++ b/test/api/reset_assertions.cpp @@ -20,7 +20,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" using namespace cvc5::api; diff --git a/test/api/sep_log_api.cpp b/test/api/sep_log_api.cpp index 8599a36e1..1ce8e9c70 100644 --- a/test/api/sep_log_api.cpp +++ b/test/api/sep_log_api.cpp @@ -22,7 +22,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" using namespace cvc5::api; using namespace std; diff --git a/test/api/smt2_compliance.cpp b/test/api/smt2_compliance.cpp index 0510e59db..a3ae59eda 100644 --- a/test/api/smt2_compliance.cpp +++ b/test/api/smt2_compliance.cpp @@ -18,7 +18,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "options/options.h" #include "options/set_language.h" #include "parser/parser.h" diff --git a/test/api/two_solvers.cpp b/test/api/two_solvers.cpp index d28f0ceb5..b55678b1a 100644 --- a/test/api/two_solvers.cpp +++ b/test/api/two_solvers.cpp @@ -17,7 +17,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" using namespace cvc5::api; using namespace std; diff --git a/test/unit/main/interactive_shell_black.cpp b/test/unit/main/interactive_shell_black.cpp index 7ab337c09..52f07a2f2 100644 --- a/test/unit/main/interactive_shell_black.cpp +++ b/test/unit/main/interactive_shell_black.cpp @@ -17,7 +17,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "expr/symbol_manager.h" #include "main/interactive_shell.h" #include "options/base_options.h" diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 5177ff453..be393039b 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -19,7 +19,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "expr/dtype.h" #include "expr/dtype_cons.h" #include "expr/node.h" diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp index 3c6d8b820..5b695030e 100644 --- a/test/unit/parser/parser_black.cpp +++ b/test/unit/parser/parser_black.cpp @@ -17,7 +17,7 @@ #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "base/output.h" #include "expr/symbol_manager.h" #include "options/base_options.h" diff --git a/test/unit/parser/parser_builder_black.cpp b/test/unit/parser/parser_builder_black.cpp index a83932b2f..113a5abd5 100644 --- a/test/unit/parser/parser_builder_black.cpp +++ b/test/unit/parser/parser_builder_black.cpp @@ -22,7 +22,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "expr/symbol_manager.h" #include "options/language.h" #include "parser/parser.h" diff --git a/test/unit/printer/smt2_printer_black.cpp b/test/unit/printer/smt2_printer_black.cpp index 03ab95083..d89930033 100644 --- a/test/unit/printer/smt2_printer_black.cpp +++ b/test/unit/printer/smt2_printer_black.cpp @@ -16,7 +16,7 @@ #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "expr/node.h" #include "expr/node_manager.h" #include "options/language.h" diff --git a/test/unit/test_api.h b/test/unit/test_api.h index 7ad2e1e5c..b66dd58bc 100644 --- a/test/unit/test_api.h +++ b/test/unit/test_api.h @@ -15,7 +15,7 @@ #ifndef CVC4__TEST__UNIT__TEST_API_H #define CVC4__TEST__UNIT__TEST_API_H -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "gtest/gtest.h" namespace cvc5 { diff --git a/test/unit/theory/regexp_operation_black.cpp b/test/unit/theory/regexp_operation_black.cpp index ed432ca2f..608eeb649 100644 --- a/test/unit/theory/regexp_operation_black.cpp +++ b/test/unit/theory/regexp_operation_black.cpp @@ -18,7 +18,7 @@ #include #include -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "expr/node.h" #include "expr/node_manager.h" #include "smt/smt_engine_scope.h" -- 2.30.2