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

24 files changed, 51 insertions, 60 deletions

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;