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

70 files changed, 129 insertions, 139 deletions

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 <cvc4/api/cvc4cpp.h>\nint main() { cvc5::api::Solver s; return 0; }" > /tmp/test.cpp
+        echo -e "#include <cvc5/cvc5.h>\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 <iostream>
+#include <cvc5/cvc5.h>
 
-#include <cvc4/api/cvc4cpp.h>
+#include <iostream>
 
 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 <iostream>
-#include <cmath>
+#include <cvc5/cvc5.h>
 
-#include <cvc4/api/cvc4cpp.h>
+#include <cmath>
+#include <iostream>
 
 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 <iostream>
+#include <cvc5/cvc5.h>
 
-#include <cvc4/api/cvc4cpp.h>
+#include <iostream>
 
 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 <iostream>
+#include <cvc5/cvc5.h>
 
-#include <cvc4/api/cvc4cpp.h>
+#include <iostream>
 
 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 <iostream>
+#include <cvc5/cvc5.h>
 
-#include <cvc4/api/cvc4cpp.h>
+#include <iostream>
 
 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 <iostream>
+#include <cvc5/cvc5.h>
 
-#include <cvc4/api/cvc4cpp.h>
+#include <iostream>
 
 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 <iostream>
 
-#include "cvc4/api/cvc4cpp.h"
+#include <cvc5/cvc5.h>
 
 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 <cvc4/api/cvc4cpp.h>
+#include <cvc5/cvc5.h>
 
 #include <iostream>
 
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 <iostream>
+#include <cvc5/cvc5.h>
 
-#include <cvc4/api/cvc4cpp.h>
+#include <iostream>
 
 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 <iostream>
+#include <cvc5/cvc5.h>
 
-#include <cvc4/api/cvc4cpp.h>
+#include <iostream>
 
 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 <cvc4/api/cvc4cpp.h>
+#include <cvc5/cvc5.h>
 
 #include <iostream>
 
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 <cvc4/api/cvc4cpp.h>
+#include <cvc5/cvc5.h>
 
 #include <iostream>
 
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 <cvc4/api/cvc4cpp.h>
+#include <cvc5/cvc5.h>
 
 #include <iostream>
 
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 <cvc5/cvc5.h>
+#include <cvc4/expr/expr_iomanip.h>
+#include <cvc4/options/set_language.h>
+
 #include <cassert>
 #include <iostream>
 #include <map>
@@ -22,11 +26,6 @@
 #include <typeinfo>
 #include <vector>
 
-#include <cvc4/api/cvc4cpp.h>
-#include <cvc4/cvc4.h>
-#include <cvc4/expr/expr_iomanip.h>
-#include <cvc4/options/set_language.h>
-
 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 <cvc5/cvc5.h>
+
 #include <cassert>
 #include <iostream>
 #include <string>
 #include <typeinfo>
 #include <vector>
 
-#include <cvc4/api/cvc4cpp.h>
-#include <cvc4/cvc4.h>
-
 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 <cvc5/cvc5.h>
+#include <cvc4/expr/expr_iomanip.h>
+#include <cvc4/options/set_language.h>
+
 #include <cassert>
 #include <iostream>
 #include <map>
@@ -22,11 +26,6 @@
 #include <typeinfo>
 #include <vector>
 
-#include <cvc4/api/cvc4cpp.h>
-#include <cvc4/cvc4.h>
-#include <cvc4/expr/expr_iomanip.h>
-#include <cvc4/options/set_language.h>
-
 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 <cvc5/cvc5.h>
+
 #include <cassert>
 #include <iostream>
 #include <map>
@@ -22,9 +24,6 @@
 #include <typeinfo>
 #include <vector>
 
-#include <cvc4/api/cvc4cpp.h>
-#include <cvc4/cvc4.h>
-
 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 <cvc5/cvc5.h>
+
 #include <cassert>
 #include <iostream>
 #include <map>
@@ -22,9 +24,6 @@
 #include <typeinfo>
 #include <vector>
 
-#include <cvc4/api/cvc4cpp.h>
-#include <cvc4/cvc4.h>
-
 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 <cvc5/cvc5.h>
+
 #include <cassert>
 #include <iostream>
 #include <map>
@@ -22,9 +24,6 @@
 #include <typeinfo>
 #include <vector>
 
-#include <cvc4/api/cvc4cpp.h>
-#include <cvc4/cvc4.h>
-
 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 <cvc5/cvc5.h>
+
 #include <cassert>
 #include <iostream>
 #include <map>
@@ -22,9 +24,6 @@
 #include <typeinfo>
 #include <vector>
 
-#include <cvc4/api/cvc4cpp.h>
-#include <cvc4/cvc4.h>
-
 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 <boost/algorithm/string.hpp> // include Boost, a C++ library
+#include <cvc5/cvc5.h>
+#include <cvc4/options/set_language.h>
+
+#include <boost/algorithm/string.hpp>  // include Boost, a C++ library
 #include <cassert>
 #include <iostream>
 #include <string>
@@ -23,10 +26,6 @@
 #include <unordered_map>
 #include <vector>
 
-#include <cvc4/api/cvc4cpp.h>
-#include <cvc4/cvc4.h>
-#include <cvc4/options/set_language.h>
-
 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 <cvc4/api/cvc4cpp.h>
+#include <cvc5/cvc5.h>
 
 #include <iostream>
 
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 <cvc4/api/cvc4cpp.h>
+#include <cvc5/cvc5.h>
 
 #include <iostream>
 
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 <cvc5/cvc5.h>
+#include <cvc4/expr/expr_iomanip.h>
+#include <cvc4/options/set_language.h>
+#include <getopt.h>
+
 #include <cerrno>
 #include <cstdlib>
 #include <cstring>
 #include <fstream>
-#include <getopt.h>
 #include <iostream>
 
-#include <cvc4/api/cvc4cpp.h>
-#include <cvc4/cvc4.h>
-#include <cvc4/expr/expr_iomanip.h>
-#include <cvc4/options/set_language.h>
-
 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
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"
 
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 <iostream>
 #include <sstream>
 
-#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 <iostream>
 #include <string>
 
-#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 <iostream>
 #include <sstream>
 
-#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 <iostream>
 #include <sstream>
 
-#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 <iostream>
 #include <sstream>
 
-#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 <iostream>
 #include <sstream>
 
-#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 <sstream>
 #include <vector>
 
-#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 <string>
 #include <vector>
 
-#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 <sstream>
 
-#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 <fstream>
 #include <iostream>
 
-#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 <iostream>
 
-#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 <memory>
 #include <vector>
 
-#include "api/cvc4cpp.h"
+#include "api/cpp/cvc5.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
 #include "smt/smt_engine_scope.h"