Rename namespace CVC4 to CVC5. (#6249)

6 files changed, 98 insertions, 96 deletions

diff --git a/src/decision/decision_attributes.h b/src/decision/decision_attributes.h
index 918710dc8..be5987e6d 100644
--- a/src/decision/decision_attributes.h
+++ b/src/decision/decision_attributes.h
@@ -22,15 +22,15 @@
 #include "options/decision_weight.h"
 #include "expr/attribute.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace decision {
 namespace attr {
   struct DecisionWeightTag {};
-}/* CVC4::decision::attr namespace */
+  }  // namespace attr
 
 typedef expr::Attribute<attr::DecisionWeightTag, DecisionWeight> DecisionWeightAttr;
 
-}/* CVC4::decision namespace */
-}/* CVC4 namespace */
+}  // namespace decision
+}  // namespace CVC5
 
 #endif /* CVC4__DECISION__DECISION_ATTRIBUTES_H */
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index e535e5415..3196336aa 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -24,7 +24,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 
 DecisionEngine::DecisionEngine(context::Context* sc,
                                context::UserContext* uc,
@@ -101,4 +101,4 @@ void DecisionEngine::addSkolemDefinition(TNode lem, TNode skolem)
   }
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index 2e7eaaa76..7405498b5 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 CVC4::prop;
-using namespace CVC4::decision;
+using namespace CVC5::prop;
+using namespace CVC5::decision;
 
-namespace CVC4 {
+namespace CVC5 {
 
 class DecisionEngine {
 
@@ -160,6 +160,6 @@ class DecisionEngine {
   std::unique_ptr<ITEDecisionStrategy> d_enabledITEStrategy;
 };/* DecisionEngine class */
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__DECISION__DECISION_ENGINE_H */
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index 829ad18a4..6a9353474 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -25,13 +25,13 @@
 #include "prop/sat_solver_types.h"
 #include "smt/term_formula_removal.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class DecisionEngine;
 
 namespace context {
   class Context;
-}/* CVC4::context namespace */
+  }  // namespace context
 
 namespace decision {
 
@@ -65,7 +65,7 @@ public:
   virtual void addSkolemDefinition(TNode lem, TNode skolem) = 0;
 };/* class ITEDecisionStrategy */
 
-}/* CVC4::decision namespace */
-}/* CVC4 namespace */
+}  // namespace decision
+}  // namespace CVC5
 
 #endif /* CVC4__DECISION__DECISION_STRATEGY_H */
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index a313dcf15..f9f9cb7df 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 CVC4 {
+namespace CVC5 {
 namespace decision {
 
-JustificationHeuristic::JustificationHeuristic(CVC4::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);
 }
 
-CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch)
+CVC5::prop::SatLiteral JustificationHeuristic::getNext(bool& stopSearch)
 {
   if(options::decisionThreshold() > 0) {
     bool stopSearchTmp = false;
@@ -82,7 +82,9 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch)
   return getNextThresh(stopSearch, 0);
 }
 
-CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, DecisionWeight threshold) {
+CVC5::prop::SatLiteral JustificationHeuristic::getNextThresh(
+    bool& stopSearch, DecisionWeight threshold)
+{
   Trace("decision") << "JustificationHeuristic::getNextThresh(stopSearch, "<<threshold<<")" << std::endl;
   TimerStat::CodeTimer codeTimer(d_timestat);
 
@@ -731,4 +733,4 @@ JustificationHeuristic::handleEmbeddedSkolems(TNode node)
 }
 
 } /* namespace decision */
-} /* namespace CVC4 */
\ 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 6c1ff3378..9ec61d540 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 CVC4 {
+namespace CVC5 {
 namespace decision {
 
 class JustificationHeuristic : public ITEDecisionStrategy {
@@ -117,84 +117,84 @@ class JustificationHeuristic : public ITEDecisionStrategy {
   };
 
 public:
-  JustificationHeuristic(CVC4::DecisionEngine* de,
-                         context::UserContext *uc,
-                         context::Context *c);
-
-  ~JustificationHeuristic();
-
-  prop::SatLiteral getNext(bool &stopSearch) override;
-
-  /**
-   * Notify this class that assertion is an (input) assertion, not corresponding
-   * to a skolem definition.
-   */
-  void addAssertion(TNode assertion) override;
-  /**
-   * Notify this class  that lem is the skolem definition for skolem, which is
-   * a part of the current assertions.
-   */
-  void addSkolemDefinition(TNode lem, TNode skolem) override;
-
- private:
-  /* getNext with an option to specify threshold */
-  prop::SatLiteral getNextThresh(bool &stopSearch, DecisionWeight threshold);
-
-  prop::SatLiteral findSplitter(TNode node, prop::SatValue desiredVal);
-
-  /**
-   * Do all the hard work.
-   */
-  SearchResult findSplitterRec(TNode node, prop::SatValue value);
-
-  /* Helper functions */
-  void setJustified(TNode);
-  bool checkJustified(TNode);
-  DecisionWeight getExploredThreshold(TNode);
-  void setExploredThreshold(TNode);
-  void setPrvsIndex(int);
-  int  getPrvsIndex();
-  DecisionWeight getWeightPolarized(TNode n, bool polarity);
-  DecisionWeight getWeightPolarized(TNode n, prop::SatValue);
-  static DecisionWeight getWeight(TNode);
-  bool compareByWeightFalse(TNode, TNode);
-  bool compareByWeightTrue(TNode, TNode);
-  TNode getChildByWeight(TNode n, int i, bool polarity);
-
-  /* If literal exists corresponding to the node return
-     that. Otherwise an UNKNOWN */
-  prop::SatValue tryGetSatValue(Node n);
-
-  /* Get list of all term-ITEs for the atomic formula v */
-  JustificationHeuristic::SkolemList getSkolems(TNode n);
-
-  /**
-   * For big and/or nodes, a cache to save starting index into children
-   * for efficiently.
-   */
-  typedef context::CDHashMap<Node, int, NodeHashFunction> StartIndexCache;
-  StartIndexCache d_startIndexCache;
-  int getStartIndex(TNode node);
-  void saveStartIndex(TNode node, int val);
-
-  /* Compute all term-removal skolems in a node recursively */
-  void computeSkolems(TNode n, SkolemList& l);
-
-  SearchResult handleAndOrEasy(TNode node, prop::SatValue desiredVal);
-  SearchResult handleAndOrHard(TNode node, prop::SatValue desiredVal);
-  SearchResult handleBinaryEasy(TNode node1,
-                                prop::SatValue desiredVal1,
-                                TNode node2,
-                                prop::SatValue desiredVal2);
-  SearchResult handleBinaryHard(TNode node1,
-                                prop::SatValue desiredVal1,
-                                TNode node2,
-                                prop::SatValue desiredVal2);
-  SearchResult handleITE(TNode node, prop::SatValue desiredVal);
-  SearchResult handleEmbeddedSkolems(TNode node);
+ JustificationHeuristic(CVC5::DecisionEngine* de,
+                        context::UserContext* uc,
+                        context::Context* c);
+
+ ~JustificationHeuristic();
+
+ prop::SatLiteral getNext(bool& stopSearch) override;
+
+ /**
+  * Notify this class that assertion is an (input) assertion, not corresponding
+  * to a skolem definition.
+  */
+ void addAssertion(TNode assertion) override;
+ /**
+  * Notify this class  that lem is the skolem definition for skolem, which is
+  * a part of the current assertions.
+  */
+ void addSkolemDefinition(TNode lem, TNode skolem) override;
+
+private:
+ /* getNext with an option to specify threshold */
+ prop::SatLiteral getNextThresh(bool& stopSearch, DecisionWeight threshold);
+
+ prop::SatLiteral findSplitter(TNode node, prop::SatValue desiredVal);
+
+ /**
+  * Do all the hard work.
+  */
+ SearchResult findSplitterRec(TNode node, prop::SatValue value);
+
+ /* Helper functions */
+ void setJustified(TNode);
+ bool checkJustified(TNode);
+ DecisionWeight getExploredThreshold(TNode);
+ void setExploredThreshold(TNode);
+ void setPrvsIndex(int);
+ int getPrvsIndex();
+ DecisionWeight getWeightPolarized(TNode n, bool polarity);
+ DecisionWeight getWeightPolarized(TNode n, prop::SatValue);
+ static DecisionWeight getWeight(TNode);
+ bool compareByWeightFalse(TNode, TNode);
+ bool compareByWeightTrue(TNode, TNode);
+ TNode getChildByWeight(TNode n, int i, bool polarity);
+
+ /* If literal exists corresponding to the node return
+    that. Otherwise an UNKNOWN */
+ prop::SatValue tryGetSatValue(Node n);
+
+ /* Get list of all term-ITEs for the atomic formula v */
+ JustificationHeuristic::SkolemList getSkolems(TNode n);
+
+ /**
+  * For big and/or nodes, a cache to save starting index into children
+  * for efficiently.
+  */
+ typedef context::CDHashMap<Node, int, NodeHashFunction> StartIndexCache;
+ StartIndexCache d_startIndexCache;
+ int getStartIndex(TNode node);
+ void saveStartIndex(TNode node, int val);
+
+ /* Compute all term-removal skolems in a node recursively */
+ void computeSkolems(TNode n, SkolemList& l);
+
+ SearchResult handleAndOrEasy(TNode node, prop::SatValue desiredVal);
+ SearchResult handleAndOrHard(TNode node, prop::SatValue desiredVal);
+ SearchResult handleBinaryEasy(TNode node1,
+                               prop::SatValue desiredVal1,
+                               TNode node2,
+                               prop::SatValue desiredVal2);
+ SearchResult handleBinaryHard(TNode node1,
+                               prop::SatValue desiredVal1,
+                               TNode node2,
+                               prop::SatValue desiredVal2);
+ SearchResult handleITE(TNode node, prop::SatValue desiredVal);
+ SearchResult handleEmbeddedSkolems(TNode node);
 };/* class JustificationHeuristic */
 
 }/* namespace decision */
-}/* namespace CVC4 */
+} // namespace CVC5
 
 #endif /* CVC4__DECISION__JUSTIFICATION_HEURISTIC */