New C++ Api: Rename and move headers. (#6292)

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"