diff options
Diffstat (limited to 'src')
30 files changed, 62 insertions, 63 deletions
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 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 <cstring> #include <sstream> @@ -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<std::int32_t>(getInteger(node)); + return isInteger(node) && checkIntegerBounds<std::int32_t>(getInteger(node)); } bool isUInt32(const Node& node) { - return isInteger(node) - && checkIntegerBounds<std::uint32_t>(getInteger(node)); + return isInteger(node) && checkIntegerBounds<std::uint32_t>(getInteger(node)); } bool isInt64(const Node& node) { - return isInteger(node) - && checkIntegerBounds<std::int64_t>(getInteger(node)); + return isInteger(node) && checkIntegerBounds<std::int64_t>(getInteger(node)); } bool isUInt64(const Node& node) { - return isInteger(node) - && checkIntegerBounds<std::uint64_t>(getInteger(node)); + return isInteger(node) && checkIntegerBounds<std::uint64_t>(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 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 <map> #include <memory> @@ -30,6 +28,8 @@ #include <unordered_set> #include <vector> +#include "api/cpp/cvc5_kind.h" + namespace cvc5 { template <bool ref_count> @@ -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 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 <ostream> 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 "<iostream>" 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 <memory> #include <string> -#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 <unordered_map> #include <utility> -#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 <cvc4\/\1>/' {} + +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>/' {} + 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 <iosfwd> #include <string> -#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 <memory> #include <new> -#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 <string> #include <vector> -#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 <string> -#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 <sstream> #include <unordered_set> -#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 <set> #include <string> -#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 <string> -#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 <unordered_set> #include <vector> -#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 <unordered_map> #include <utility> -#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 <iterator> #include <vector> -#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 <algorithm> #include <set> -#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 <unordered_map> #include <unordered_set> -#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 <typeinfo> #include <vector> -#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 <utility> #include <vector> -#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 <string> #include <vector> -#include "api/cvc4cpp.h" +#include "api/cpp/cvc5.h" #include "cvc4_export.h" #include "options/language.h" |