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

9 files changed, 31 insertions, 35 deletions

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 = \