Rename namespace CVC5 to cvc5. (#6258)

28 files changed, 56 insertions, 56 deletions

diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp
index 1cbfdb031..043bbf8aa 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 CVC5::api;
+using namespace cvc5::api;
 
 int main()
 {
diff --git a/examples/api/bitvectors_and_arrays.cpp b/examples/api/bitvectors_and_arrays.cpp
index 5c243e1d1..2bca1eb4c 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 CVC5::api;
+using namespace cvc5::api;
 
 int main()
 {
diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp
index 2651bf80f..9ea2f55ed 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 CVC5::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 c2b3bc4c4..49253e466 100644
--- a/examples/api/datatypes.cpp
+++ b/examples/api/datatypes.cpp
@@ -18,7 +18,7 @@
 
 #include <cvc4/api/cvc4cpp.h>
 
-using namespace CVC5::api;
+using namespace cvc5::api;
 
 void test(Solver& slv, Sort& consListSort)
 {
diff --git a/examples/api/extract.cpp b/examples/api/extract.cpp
index a6a43a7c2..760f5d0fe 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 CVC5::api;
+using namespace cvc5::api;
 
 int main()
 {
diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp
index 89b0e212d..092e2a79a 100644
--- a/examples/api/helloworld.cpp
+++ b/examples/api/helloworld.cpp
@@ -18,7 +18,7 @@
 
 #include <cvc4/api/cvc4cpp.h>
 
-using namespace CVC5::api;
+using namespace cvc5::api;
 
 int main()
 {
diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp
index ca3e8a2b9..b56982daa 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 CVC5::api;
+using namespace cvc5::api;
 
 int main()
 {
diff --git a/examples/api/sequences.cpp b/examples/api/sequences.cpp
index 6272b423b..3498b3275 100644
--- a/examples/api/sequences.cpp
+++ b/examples/api/sequences.cpp
@@ -18,7 +18,7 @@
 
 #include <iostream>
 
-using namespace CVC5::api;
+using namespace cvc5::api;
 
 int main()
 {
diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp
index cac705415..59385896c 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 CVC5::api;
+using namespace cvc5::api;
 
 int main()
 {
diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp
index b926395de..53352d266 100644
--- a/examples/api/strings.cpp
+++ b/examples/api/strings.cpp
@@ -18,7 +18,7 @@
 
 #include <cvc4/api/cvc4cpp.h>
 
-using namespace CVC5::api;
+using namespace cvc5::api;
 
 int main()
 {
diff --git a/examples/api/sygus-fun.cpp b/examples/api/sygus-fun.cpp
index a29cdb132..be4d3e8d5 100644
--- a/examples/api/sygus-fun.cpp
+++ b/examples/api/sygus-fun.cpp
@@ -49,7 +49,7 @@
 
 #include <iostream>
 
-using namespace CVC5::api;
+using namespace cvc5::api;
 
 int main()
 {
diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp
index 6491dc0a5..61b00f6de 100644
--- a/examples/api/sygus-grammar.cpp
+++ b/examples/api/sygus-grammar.cpp
@@ -46,7 +46,7 @@
 
 #include <iostream>
 
-using namespace CVC5::api;
+using namespace cvc5::api;
 
 int main()
 {
diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp
index 206803eb6..56b5a0aaa 100644
--- a/examples/api/sygus-inv.cpp
+++ b/examples/api/sygus-inv.cpp
@@ -37,7 +37,7 @@
 
 #include <iostream>
 
-using namespace CVC5::api;
+using namespace cvc5::api;
 
 int main()
 {
diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp
index 6fa7954ea..0545ce048 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 CVC5;
+using namespace cvc5;
 
 hashsmt::cvc4_uchar8 *createInput(unsigned size, std::string prefix, std::ostream& output) {
   hashsmt::cvc4_uchar8 *input = new hashsmt::cvc4_uchar8[size];
@@ -102,7 +102,7 @@ int main(int argc, char* argv[]) {
     delete[] cvc4input1;
     delete[] cvc4input2;
   }
-  catch (CVC5::Exception& e)
+  catch (cvc5::Exception& e)
   {
     cerr << e << endl;
   }
diff --git a/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp
index 957f9225e..a4acfc3c6 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 CVC5;
+using namespace cvc5;
 
 int main(int argc, char* argv[]) {
 
@@ -105,7 +105,7 @@ int main(int argc, char* argv[]) {
     // Checksat command
     output << CheckSatCommand() << endl;
   }
-  catch (CVC5::Exception& e)
+  catch (cvc5::Exception& e)
   {
     cerr << e << endl;
   }
diff --git a/examples/hashsmt/word.cpp b/examples/hashsmt/word.cpp
index 5fd5b7979..79b868d1c 100644
--- a/examples/hashsmt/word.cpp
+++ b/examples/hashsmt/word.cpp
@@ -33,8 +33,8 @@
 
 using namespace std;
 using namespace hashsmt;
-using namespace CVC5;
-using namespace CVC5::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) {
-    CVC5::Options options;
+    cvc5::Options options;
     options.setInputLanguage(language::input::LANG_SMTLIB_V2);
     options.setOutputLanguage(language::output::LANG_SMTLIB_V2);
-    s_manager = new CVC5::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 << CVC5::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 4a1d142f4..f5b95ba32 100644
--- a/examples/hashsmt/word.h
+++ b/examples/hashsmt/word.h
@@ -35,20 +35,20 @@ namespace hashsmt {
 class Word {
 
   /** Expression managaer we're using for all word expressions */
-  static CVC5::ExprManager* s_manager;
+  static cvc5::ExprManager* s_manager;
 
  protected:
 
   /** The expression of this word */
-  CVC5::Expr d_expr;
+  cvc5::Expr d_expr;
 
   /** Get the expression manager words are using */
-  static CVC5::ExprManager* em();
+  static cvc5::ExprManager* em();
 
-  Word(CVC5::Expr expr = CVC5::Expr()) : d_expr(expr) {}
+  Word(cvc5::Expr expr = cvc5::Expr()) : d_expr(expr) {}
 
   /** Extend the representing expression to the given size >= size() */
-  CVC5::Expr extendToSize(unsigned size) const;
+  cvc5::Expr extendToSize(unsigned size) const;
 
  public:
 
@@ -70,10 +70,10 @@ class Word {
 
   void print(std::ostream& out) const;
 
-  CVC5::Expr getExpr() const { return d_expr; }
+  cvc5::Expr getExpr() const { return d_expr; }
 
   /** Returns the comparison expression */
-  CVC5::Expr operator==(const Word& b) const;
+  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 daa7d920d..ba495e1fd 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 CVC5;
-using namespace CVC5::parser;
-using namespace CVC5::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 661747ab0..1eb4b3d4d 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 CVC5;
-using namespace CVC5::parser;
-using namespace CVC5::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 2a12b828e..8139a4d91 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 CVC5;
-using namespace CVC5::parser;
-using namespace CVC5::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 aecdf5ba2..09b0c69d8 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 CVC5;
-using namespace CVC5::parser;
-using namespace CVC5::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 02795dc1f..6cb51f17c 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 CVC5;
-using namespace CVC5::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 1bfe9424b..afd468d5d 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 CVC5;
-using namespace CVC5::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 4238e9f13..d9bd6012a 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 CVC5;
-using namespace CVC5::parser;
-using namespace CVC5::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 b9ced3d79..ec95b5f70 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 CVC5;
-using namespace CVC5::parser;
-using namespace CVC5::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 b6890e6ef..b97b86bb8 100644
--- a/examples/simple_vc_cxx.cpp
+++ b/examples/simple_vc_cxx.cpp
@@ -20,7 +20,7 @@
 
 #include <iostream>
 
-using namespace CVC5::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 e6778fa41..73dbfe34f 100644
--- a/examples/simple_vc_quant_cxx.cpp
+++ b/examples/simple_vc_quant_cxx.cpp
@@ -18,7 +18,7 @@
 
 #include <iostream>
 
-using namespace CVC5::api;
+using namespace cvc5::api;
 
 int main() {
   Solver slv;
diff --git a/examples/translator.cpp b/examples/translator.cpp
index 1a9de7f80..4838e06fb 100644
--- a/examples/translator.cpp
+++ b/examples/translator.cpp
@@ -28,9 +28,9 @@
 #include <cvc4/options/set_language.h>
 
 using namespace std;
-using namespace CVC5;
-using namespace CVC5::language;
-using namespace CVC5::parser;
+using namespace cvc5;
+using namespace cvc5::language;
+using namespace cvc5::parser;
 
 enum {
   INPUT_LANG = 'L',