Rename namespace CVC5 to cvc5. (#6258)

6 files changed, 18 insertions, 18 deletions

diff --git a/src/decision/decision_attributes.h b/src/decision/decision_attributes.h
index be5987e6d..c34abd179 100644
--- a/src/decision/decision_attributes.h
+++ b/src/decision/decision_attributes.h
@@ -22,7 +22,7 @@
 #include "options/decision_weight.h"
 #include "expr/attribute.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace decision {
 namespace attr {
   struct DecisionWeightTag {};
@@ -31,6 +31,6 @@ namespace attr {
 typedef expr::Attribute<attr::DecisionWeightTag, DecisionWeight> DecisionWeightAttr;
 
 }  // namespace decision
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__DECISION__DECISION_ATTRIBUTES_H */
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 3196336aa..f202037b0 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -24,7 +24,7 @@
 
 using namespace std;
 
-namespace CVC5 {
+namespace cvc5 {
 
 DecisionEngine::DecisionEngine(context::Context* sc,
                                context::UserContext* uc,
@@ -101,4 +101,4 @@ void DecisionEngine::addSkolemDefinition(TNode lem, TNode skolem)
   }
 }
 
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 7405498b5..cbb6b897d 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -28,10 +28,10 @@
 #include "prop/sat_solver_types.h"
 #include "util/result.h"
 
-using namespace CVC5::prop;
-using namespace CVC5::decision;
+using namespace cvc5::prop;
+using namespace cvc5::decision;
 
-namespace CVC5 {
+namespace cvc5 {
 
 class DecisionEngine {
 
@@ -160,6 +160,6 @@ class DecisionEngine {
   std::unique_ptr<ITEDecisionStrategy> d_enabledITEStrategy;
 };/* DecisionEngine class */
 
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__DECISION__DECISION_ENGINE_H */
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index 6a9353474..4a1828a8f 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -25,7 +25,7 @@
 #include "prop/sat_solver_types.h"
 #include "smt/term_formula_removal.h"
 
-namespace CVC5 {
+namespace cvc5 {
 
 class DecisionEngine;
 
@@ -66,6 +66,6 @@ public:
 };/* class ITEDecisionStrategy */
 
 }  // namespace decision
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__DECISION__DECISION_STRATEGY_H */
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index f9f9cb7df..abe7a47a7 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -28,10 +28,10 @@
 #include "theory/rewriter.h"
 #include "util/random.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace decision {
 
-JustificationHeuristic::JustificationHeuristic(CVC5::DecisionEngine* de,
+JustificationHeuristic::JustificationHeuristic(cvc5::DecisionEngine* de,
                                                context::UserContext* uc,
                                                context::Context* c)
     : ITEDecisionStrategy(de, c),
@@ -66,7 +66,7 @@ JustificationHeuristic::~JustificationHeuristic()
   smtStatisticsRegistry()->unregisterStat(&d_timestat);
 }
 
-CVC5::prop::SatLiteral JustificationHeuristic::getNext(bool& stopSearch)
+cvc5::prop::SatLiteral JustificationHeuristic::getNext(bool& stopSearch)
 {
   if(options::decisionThreshold() > 0) {
     bool stopSearchTmp = false;
@@ -82,7 +82,7 @@ CVC5::prop::SatLiteral JustificationHeuristic::getNext(bool& stopSearch)
   return getNextThresh(stopSearch, 0);
 }
 
-CVC5::prop::SatLiteral JustificationHeuristic::getNextThresh(
+cvc5::prop::SatLiteral JustificationHeuristic::getNextThresh(
     bool& stopSearch, DecisionWeight threshold)
 {
   Trace("decision") << "JustificationHeuristic::getNextThresh(stopSearch, "<<threshold<<")" << std::endl;
@@ -733,4 +733,4 @@ JustificationHeuristic::handleEmbeddedSkolems(TNode node)
 }
 
 } /* namespace decision */
-} // namespace CVC5
\ No newline at end of file
+}  // namespace cvc5
\ No newline at end of file
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 9ec61d540..06864470e 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -37,7 +37,7 @@
 #include "util/statistics_registry.h"
 #include "util/stats_timer.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace decision {
 
 class JustificationHeuristic : public ITEDecisionStrategy {
@@ -117,7 +117,7 @@ class JustificationHeuristic : public ITEDecisionStrategy {
   };
 
 public:
- JustificationHeuristic(CVC5::DecisionEngine* de,
+ JustificationHeuristic(cvc5::DecisionEngine* de,
                         context::UserContext* uc,
                         context::Context* c);
 
@@ -195,6 +195,6 @@ private:
 };/* class JustificationHeuristic */
 
 }/* namespace decision */
-} // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC4__DECISION__JUSTIFICATION_HEURISTIC */