Rename namespace CVC5 to cvc5. (#6258)

11 files changed, 33 insertions, 33 deletions

diff --git a/src/proof/clause_id.h b/src/proof/clause_id.h
index 6f3caaf19..7ce8a384a 100644
--- a/src/proof/clause_id.h
+++ b/src/proof/clause_id.h
@@ -20,7 +20,7 @@
 #ifndef CVC4__PROOF__CLAUSE_ID_H
 #define CVC4__PROOF__CLAUSE_ID_H
 
-namespace CVC5 {
+namespace cvc5 {
 
 /**
  * A ClauseId is a shared identifier between the proofs module and the sat
@@ -35,6 +35,6 @@ const ClauseId ClauseIdEmpty(-1);
 const ClauseId ClauseIdUndef(-2);
 const ClauseId ClauseIdError(-3);
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__PROOF__CLAUSE_ID_H */
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index dc1a6dd61..fbe87c267 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -23,7 +23,7 @@
 #include "prop/minisat/minisat.h"
 #include "prop/sat_solver_types.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 CnfProof::CnfProof(prop::CnfStream* stream,
                    context::Context* ctx,
@@ -113,4 +113,4 @@ bool CnfProof::getCurrentAssertionKind()
   return d_currentAssertionStack.back().second;
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 1319b83d6..88eb885aa 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -28,7 +28,7 @@
 #include "proof/clause_id.h"
 #include "proof/proof_manager.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace prop {
   class CnfStream;
   }  // namespace prop
@@ -46,7 +46,7 @@ typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
 
 class CnfProof {
 protected:
- CVC5::prop::CnfStream* d_cnfStream;
+ cvc5::prop::CnfStream* d_cnfStream;
 
  /** Map from ClauseId to the assertion that lead to adding this clause **/
  ClauseIdToNode d_clauseToAssertion;
@@ -67,7 +67,7 @@ protected:
 
  std::string d_name;
 public:
- CnfProof(CVC5::prop::CnfStream* cnfStream,
+ CnfProof(cvc5::prop::CnfStream* cnfStream,
           context::Context* ctx,
           const std::string& name);
  ~CnfProof();
@@ -95,6 +95,6 @@ public:
  Node getAssertionForClause(ClauseId clause);
 };/* class CnfProof */
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__CNF_PROOF_H */
diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp
index 8ecec8484..c2e8bd863 100644
--- a/src/proof/dot/dot_printer.cpp
+++ b/src/proof/dot/dot_printer.cpp
@@ -17,7 +17,7 @@
 #include <sstream>
 #include "expr/proof_node_manager.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace proof {
 
 void DotPrinter::cleanQuotes(std::string& s)
@@ -91,4 +91,4 @@ void DotPrinter::ruleArguments(std::ostringstream& currentArguments,
 }
 
 }  // namespace proof
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h
index 173495780..3bcc1cd73 100644
--- a/src/proof/dot/dot_printer.h
+++ b/src/proof/dot/dot_printer.h
@@ -21,7 +21,7 @@
 
 #include "expr/proof_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace proof {
 
 class DotPrinter
@@ -69,6 +69,6 @@ class DotPrinter
 };
 
 }  // namespace proof
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif
\ No newline at end of file
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 8b3dfd17a..d9fd9c37a 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -36,7 +36,7 @@
 #include "theory/valuation.h"
 #include "util/hash.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 ProofManager::ProofManager(context::Context* context)
     : d_context(context),
@@ -217,4 +217,4 @@ void ProofManager::addUnsatCore(Node formula)
   d_outputCoreFormulas.insert(formula);
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index b303b996f..b6e6c1b2c 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -28,7 +28,7 @@
 #include "expr/node.h"
 #include "proof/clause_id.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 // forward declarations
 namespace Minisat {
@@ -42,11 +42,11 @@ namespace prop {
 class SmtEngine;
 
 template <class Solver> class TSatProof;
-typedef TSatProof<CVC5::Minisat::Solver> CoreSatProof;
+typedef TSatProof<cvc5::Minisat::Solver> CoreSatProof;
 
 class CnfProof;
 
-typedef TSatProof<CVC5::Minisat::Solver> CoreSatProof;
+typedef TSatProof<cvc5::Minisat::Solver> CoreSatProof;
 
 namespace prop {
   typedef uint64_t SatVariable;
@@ -81,7 +81,7 @@ public:
 
  // initialization
  void initSatProof(Minisat::Solver* solver);
- void initCnfProof(CVC5::prop::CnfStream* cnfStream, context::Context* ctx);
+ void initCnfProof(cvc5::prop::CnfStream* cnfStream, context::Context* ctx);
 
  // getting various proofs
  static CoreSatProof* getSatProof();
@@ -120,6 +120,6 @@ private:
 
 };/* class ProofManager */
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__PROOF_MANAGER_H */
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 298b82624..a66ca2d00 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -34,11 +34,11 @@
 #include "util/stats_histogram.h"
 
 // Forward declarations.
-namespace CVC5 {
+namespace cvc5 {
 class CnfProof;
-} // namespace CVC5
+}  // namespace cvc5
 
-namespace CVC5 {
+namespace cvc5 {
 /**
  * Helper debugging functions
  */
@@ -369,6 +369,6 @@ template <class Solver>
 void toSatClause(const typename Solver::TClause& minisat_cl,
                  prop::SatClause& sat_cl);
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__SAT__PROOF_H */
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index 6049c4876..c2bbf6f11 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -26,7 +26,7 @@
 #include "prop/sat_solver_types.h"
 #include "smt/smt_statistics_registry.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 template <class Solver>
 void printLit(typename Solver::TLit l) {
@@ -1040,12 +1040,12 @@ TSatProof<Solver>::Statistics::~Statistics() {
   smtStatisticsRegistry()->unregisterStat(&d_usedClauseGlue);
 }
 
-inline std::ostream& operator<<(std::ostream& out, CVC5::ClauseKind k)
+inline std::ostream& operator<<(std::ostream& out, cvc5::ClauseKind k)
 {
   switch (k) {
-    case CVC5::INPUT: out << "INPUT"; break;
-    case CVC5::THEORY_LEMMA: out << "THEORY_LEMMA"; break;
-    case CVC5::LEARNT: out << "LEARNT"; break;
+    case cvc5::INPUT: out << "INPUT"; break;
+    case cvc5::THEORY_LEMMA: out << "THEORY_LEMMA"; break;
+    case cvc5::LEARNT: out << "LEARNT"; break;
     default:
       out << "ClauseKind Unknown! [" << unsigned(k) << "]";
   }
@@ -1053,6 +1053,6 @@ inline std::ostream& operator<<(std::ostream& out, CVC5::ClauseKind k)
   return out;
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__SAT__PROOF_IMPLEMENTATION_H */
diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp
index 2415daf98..e13db65d0 100644
--- a/src/proof/unsat_core.cpp
+++ b/src/proof/unsat_core.cpp
@@ -20,7 +20,7 @@
 #include "printer/printer.h"
 #include "smt/smt_engine_scope.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 UnsatCore::UnsatCore(const std::vector<Node>& core)
     : d_useNames(false), d_core(core), d_names()
@@ -58,4 +58,4 @@ std::ostream& operator<<(std::ostream& out, const UnsatCore& core) {
   return out;
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h
index 46dd7bf69..7d7688347 100644
--- a/src/proof/unsat_core.h
+++ b/src/proof/unsat_core.h
@@ -22,7 +22,7 @@
 
 #include "expr/node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 /**
  * An unsat core, which can optionally be initialized as a list of names
@@ -68,6 +68,6 @@ class UnsatCore
 /** Print the unsat core to stream out */
 std::ostream& operator<<(std::ostream& out, const UnsatCore& core);
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__UNSAT_CORE_H */