Rename namespace CVC4 to CVC5. (#6249)

28 files changed, 63 insertions, 63 deletions

diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp
index 6c0a1e875..1cbfdb031 100644
--- a/examples/api/bitvectors.cpp
+++ b/examples/api/bitvectors.cpp
@@ -19,7 +19,7 @@
 #include <cvc4/api/cvc4cpp.h>
 
 using namespace std;
-using namespace CVC4::api;
+using namespace CVC5::api;
 
 int main()
 {
diff --git a/examples/api/bitvectors_and_arrays.cpp b/examples/api/bitvectors_and_arrays.cpp
index ebc1da9fe..5c243e1d1 100644
--- a/examples/api/bitvectors_and_arrays.cpp
+++ b/examples/api/bitvectors_and_arrays.cpp
@@ -20,7 +20,7 @@
 #include <cvc4/api/cvc4cpp.h>
 
 using namespace std;
-using namespace CVC4::api;
+using namespace CVC5::api;
 
 int main()
 {
diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp
index 9e0b47f33..2651bf80f 100644
--- a/examples/api/combination.cpp
+++ b/examples/api/combination.cpp
@@ -21,7 +21,7 @@
 #include <cvc4/api/cvc4cpp.h>
 
 using namespace std;
-using namespace CVC4::api;
+using namespace CVC5::api;
 
 void prefixPrintGetValue(Solver& slv, Term t, int level = 0)
 {
diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp
index fcd2757d7..c2b3bc4c4 100644
--- a/examples/api/datatypes.cpp
+++ b/examples/api/datatypes.cpp
@@ -18,7 +18,7 @@
 
 #include <cvc4/api/cvc4cpp.h>
 
-using namespace CVC4::api;
+using namespace CVC5::api;
 
 void test(Solver& slv, Sort& consListSort)
 {
diff --git a/examples/api/extract.cpp b/examples/api/extract.cpp
index cbb1468b2..a6a43a7c2 100644
--- a/examples/api/extract.cpp
+++ b/examples/api/extract.cpp
@@ -19,7 +19,7 @@
 #include <cvc4/api/cvc4cpp.h>
 
 using namespace std;
-using namespace CVC4::api;
+using namespace CVC5::api;
 
 int main()
 {
diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp
index 79477c9b8..89b0e212d 100644
--- a/examples/api/helloworld.cpp
+++ b/examples/api/helloworld.cpp
@@ -18,7 +18,7 @@
 
 #include <cvc4/api/cvc4cpp.h>
 
-using namespace CVC4::api;
+using namespace CVC5::api;
 
 int main()
 {
diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp
index 039ae586f..ca3e8a2b9 100644
--- a/examples/api/linear_arith.cpp
+++ b/examples/api/linear_arith.cpp
@@ -20,7 +20,7 @@
 #include "cvc4/api/cvc4cpp.h"
 
 using namespace std;
-using namespace CVC4::api;
+using namespace CVC5::api;
 
 int main()
 {
diff --git a/examples/api/sequences.cpp b/examples/api/sequences.cpp
index ef479cbd3..6272b423b 100644
--- a/examples/api/sequences.cpp
+++ b/examples/api/sequences.cpp
@@ -18,7 +18,7 @@
 
 #include <iostream>
 
-using namespace CVC4::api;
+using namespace CVC5::api;
 
 int main()
 {
diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp
index b1090d19b..cac705415 100644
--- a/examples/api/sets.cpp
+++ b/examples/api/sets.cpp
@@ -19,7 +19,7 @@
 #include <cvc4/api/cvc4cpp.h>
 
 using namespace std;
-using namespace CVC4::api;
+using namespace CVC5::api;
 
 int main()
 {
diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp
index bae9c9ec2..b926395de 100644
--- a/examples/api/strings.cpp
+++ b/examples/api/strings.cpp
@@ -18,7 +18,7 @@
 
 #include <cvc4/api/cvc4cpp.h>
 
-using namespace CVC4::api;
+using namespace CVC5::api;
 
 int main()
 {
diff --git a/examples/api/sygus-fun.cpp b/examples/api/sygus-fun.cpp
index dc6f4df0f..a29cdb132 100644
--- a/examples/api/sygus-fun.cpp
+++ b/examples/api/sygus-fun.cpp
@@ -49,7 +49,7 @@
 
 #include <iostream>
 
-using namespace CVC4::api;
+using namespace CVC5::api;
 
 int main()
 {
diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp
index 9dc801e66..6491dc0a5 100644
--- a/examples/api/sygus-grammar.cpp
+++ b/examples/api/sygus-grammar.cpp
@@ -46,7 +46,7 @@
 
 #include <iostream>
 
-using namespace CVC4::api;
+using namespace CVC5::api;
 
 int main()
 {
diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp
index 8435eea44..206803eb6 100644
--- a/examples/api/sygus-inv.cpp
+++ b/examples/api/sygus-inv.cpp
@@ -37,7 +37,7 @@
 
 #include <iostream>
 
-using namespace CVC4::api;
+using namespace CVC5::api;
 
 int main()
 {
diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp
index 7887cb3e9..6fa7954ea 100644
--- a/examples/hashsmt/sha1_collision.cpp
+++ b/examples/hashsmt/sha1_collision.cpp
@@ -34,7 +34,7 @@
 #include "word.h"
 
 using namespace std;
-using namespace CVC4;
+using namespace CVC5;
 
 hashsmt::cvc4_uchar8 *createInput(unsigned size, std::string prefix, std::ostream& output) {
   hashsmt::cvc4_uchar8 *input = new hashsmt::cvc4_uchar8[size];
@@ -101,8 +101,9 @@ int main(int argc, char* argv[]) {
 
     delete[] cvc4input1;
     delete[] cvc4input2;
-
-  } catch (CVC4::Exception& e) {
+  }
+  catch (CVC5::Exception& e)
+  {
     cerr << e << endl;
   }
 }
diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp
index e555486d2..957f9225e 100644
--- a/examples/hashsmt/sha1_inversion.cpp
+++ b/examples/hashsmt/sha1_inversion.cpp
@@ -43,7 +43,7 @@
 #include "word.h"
 
 using namespace std;
-using namespace CVC4;
+using namespace CVC5;
 
 int main(int argc, char* argv[]) {
 
@@ -104,7 +104,9 @@ int main(int argc, char* argv[]) {
 
     // Checksat command
     output << CheckSatCommand() << endl;
-  } catch (CVC4::Exception& e) {
+  }
+  catch (CVC5::Exception& e)
+  {
     cerr << e << endl;
   }
 }
diff --git a/examples/hashsmt/word.cpp b/examples/hashsmt/word.cpp
index 4d86d062e..5fd5b7979 100644
--- a/examples/hashsmt/word.cpp
+++ b/examples/hashsmt/word.cpp
@@ -33,8 +33,8 @@
 
 using namespace std;
 using namespace hashsmt;
-using namespace CVC4;
-using namespace CVC4::options;
+using namespace CVC5;
+using namespace CVC5::options;
 
 Expr Word::extendToSize(unsigned newSize) const {
   if (newSize <= size()) {
@@ -50,10 +50,10 @@ ExprManager* Word::s_manager = 0;
 
 ExprManager* Word::em() {
   if (s_manager == 0) {
-    CVC4::Options options;
+    CVC5::Options options;
     options.setInputLanguage(language::input::LANG_SMTLIB_V2);
     options.setOutputLanguage(language::output::LANG_SMTLIB_V2);
-    s_manager = new CVC4::ExprManager(options);
+    s_manager = new CVC5::ExprManager(options);
   }
   return s_manager;
 }
@@ -71,7 +71,7 @@ Word Word::concat(const Word words[], unsigned size) {
 }
 
 void Word::print(ostream& out) const {
-  out << CVC4::expr::ExprSetDepth(-1) << d_expr;
+  out << CVC5::expr::ExprSetDepth(-1) << d_expr;
 }
 
 Word::Word(unsigned newSize, unsigned value) {
diff --git a/examples/hashsmt/word.h b/examples/hashsmt/word.h
index 11871e951..4a1d142f4 100644
--- a/examples/hashsmt/word.h
+++ b/examples/hashsmt/word.h
@@ -35,23 +35,22 @@ namespace hashsmt {
 class Word {
 
   /** Expression managaer we're using for all word expressions */
-  static CVC4::ExprManager* s_manager;
+  static CVC5::ExprManager* s_manager;
 
-protected:
+ protected:
 
   /** The expression of this word */
-  CVC4::Expr d_expr;
+  CVC5::Expr d_expr;
 
   /** Get the expression manager words are using */
-  static CVC4::ExprManager* em();
+  static CVC5::ExprManager* em();
 
-  Word(CVC4::Expr expr = CVC4::Expr())
-  : d_expr(expr) {}
+  Word(CVC5::Expr expr = CVC5::Expr()) : d_expr(expr) {}
 
   /** Extend the representing expression to the given size >= size() */
-  CVC4::Expr extendToSize(unsigned size) const;
+  CVC5::Expr extendToSize(unsigned size) const;
 
-public:
+ public:
 
   Word(unsigned size, unsigned value = 0);
   Word(unsigned size, std::string name);
@@ -71,12 +70,10 @@ public:
 
   void print(std::ostream& out) const;
 
-  CVC4::Expr getExpr() const {
-    return d_expr;
-  }
+  CVC5::Expr getExpr() const { return d_expr; }
 
-  /** Returns the comparison expression */  
-  CVC4::Expr operator == (const Word& b) const;
+  /** Returns the comparison expression */
+  CVC5::Expr operator==(const Word& b) const;
 
   /** Concatenate the given words */
   static Word concat(const Word words[], unsigned size);
diff --git a/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp
index 43e120f08..daa7d920d 100644
--- a/examples/nra-translate/normalize.cpp
+++ b/examples/nra-translate/normalize.cpp
@@ -28,9 +28,9 @@
 #include <cvc4/options/set_language.h>
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::parser;
-using namespace CVC4::theory;
+using namespace CVC5;
+using namespace CVC5::parser;
+using namespace CVC5::theory;
 
 int main(int argc, char* argv[])
 {
diff --git a/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp
index b73b0d28f..661747ab0 100644
--- a/examples/nra-translate/smt2info.cpp
+++ b/examples/nra-translate/smt2info.cpp
@@ -25,9 +25,9 @@
 #include <cvc4/cvc4.h>
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::parser;
-using namespace CVC4::options;
+using namespace CVC5;
+using namespace CVC5::parser;
+using namespace CVC5::options;
 
 unsigned compute_degree(ExprManager& exprManager, const Expr& term) {
   unsigned n = term.getNumChildren();    
diff --git a/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp
index fe27b01bd..2a12b828e 100644
--- a/examples/nra-translate/smt2todreal.cpp
+++ b/examples/nra-translate/smt2todreal.cpp
@@ -28,9 +28,9 @@
 #include <cvc4/options/set_language.h>
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::parser;
-using namespace CVC4::options;
+using namespace CVC5;
+using namespace CVC5::parser;
+using namespace CVC5::options;
 
 int main(int argc, char* argv[])
 {
diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp
index 33efcbbfe..aecdf5ba2 100644
--- a/examples/nra-translate/smt2toisat.cpp
+++ b/examples/nra-translate/smt2toisat.cpp
@@ -26,9 +26,9 @@
 #include <cvc4/cvc4.h>
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::parser;
-using namespace CVC4::options;
+using namespace CVC5;
+using namespace CVC5::parser;
+using namespace CVC5::options;
 
 void translate_to_isat(
         string input,
diff --git a/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp
index 0c7a4f275..02795dc1f 100644
--- a/examples/nra-translate/smt2tomathematica.cpp
+++ b/examples/nra-translate/smt2tomathematica.cpp
@@ -26,8 +26,8 @@
 #include <cvc4/cvc4.h>
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::parser;
+using namespace CVC5;
+using namespace CVC5::parser;
 
 void translate_to_mathematica(
         string input,
diff --git a/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp
index 6164f437c..1bfe9424b 100644
--- a/examples/nra-translate/smt2toqepcad.cpp
+++ b/examples/nra-translate/smt2toqepcad.cpp
@@ -26,8 +26,8 @@
 #include <cvc4/cvc4.h>
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::parser;
+using namespace CVC5;
+using namespace CVC5::parser;
 
 void translate_to_qepcad(
         string input,
diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp
index 97d600797..4238e9f13 100644
--- a/examples/nra-translate/smt2toredlog.cpp
+++ b/examples/nra-translate/smt2toredlog.cpp
@@ -26,9 +26,9 @@
 #include <cvc4/cvc4.h>
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::parser;
-using namespace CVC4::options;
+using namespace CVC5;
+using namespace CVC5::parser;
+using namespace CVC5::options;
 
 void translate_to_redlog(
         string input,
diff --git a/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index 3e59eaa2a..b9ced3d79 100644
--- a/examples/sets-translate/sets_translate.cpp
+++ b/examples/sets-translate/sets_translate.cpp
@@ -28,9 +28,9 @@
 #include <cvc4/options/set_language.h>
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::parser;
-using namespace CVC4::options;
+using namespace CVC5;
+using namespace CVC5::parser;
+using namespace CVC5::options;
 
 bool nonsense(char c) { return !isalnum(c); }
 
diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp
index f99a0170e..b6890e6ef 100644
--- a/examples/simple_vc_cxx.cpp
+++ b/examples/simple_vc_cxx.cpp
@@ -20,7 +20,7 @@
 
 #include <iostream>
 
-using namespace CVC4::api;
+using namespace CVC5::api;
 
 int main() {
   Solver slv;
diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp
index 9fb720652..e6778fa41 100644
--- a/examples/simple_vc_quant_cxx.cpp
+++ b/examples/simple_vc_quant_cxx.cpp
@@ -18,7 +18,7 @@
 
 #include <iostream>
 
-using namespace CVC4::api;
+using namespace CVC5::api;
 
 int main() {
   Solver slv;
diff --git a/examples/translator.cpp b/examples/translator.cpp
index 0783989fc..1a9de7f80 100644
--- a/examples/translator.cpp
+++ b/examples/translator.cpp
@@ -28,9 +28,9 @@
 #include <cvc4/options/set_language.h>
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::language;
-using namespace CVC4::parser;
+using namespace CVC5;
+using namespace CVC5::language;
+using namespace CVC5::parser;
 
 enum {
   INPUT_LANG = 'L',