11 files changed, 75 insertions, 82 deletions
diff --git a/src/proof/clause_id.h b/src/proof/clause_id.h
index 721da20e4..6f3caaf19 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 CVC4 {
+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);
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__PROOF__CLAUSE_ID_H */
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index a0f80ccd6..dc1a6dd61 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 CVC4 {
+namespace CVC5 {
 
 CnfProof::CnfProof(prop::CnfStream* stream,
                    context::Context* ctx,
@@ -113,4 +113,4 @@ bool CnfProof::getCurrentAssertionKind()
   return d_currentAssertionStack.back().second;
 }
 
-} /* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index abea75d50..1319b83d6 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -28,10 +28,10 @@
 #include "proof/clause_id.h"
 #include "proof/proof_manager.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace prop {
   class CnfStream;
-}/* CVC4::prop namespace */
+  }  // namespace prop
 
 class CnfProof;
 
@@ -46,55 +46,55 @@ typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
 
 class CnfProof {
 protected:
-  CVC4::prop::CnfStream* d_cnfStream;
+ CVC5::prop::CnfStream* d_cnfStream;
 
-  /** Map from ClauseId to the assertion that lead to adding this clause **/
-  ClauseIdToNode d_clauseToAssertion;
+ /** Map from ClauseId to the assertion that lead to adding this clause **/
+ ClauseIdToNode d_clauseToAssertion;
 
-  /** Top of stack is assertion currently being converted to CNF. Also saves
-   * whether it is input (rather than a lemma). **/
-  std::vector<std::pair<Node, bool>> d_currentAssertionStack;
+ /** Top of stack is assertion currently being converted to CNF. Also saves
+  * whether it is input (rather than a lemma). **/
+ std::vector<std::pair<Node, bool>> d_currentAssertionStack;
 
-  /** Map from top-level fact to facts/assertion that it follows from **/
-  NodeToNode d_cnfDeps;
+ /** Map from top-level fact to facts/assertion that it follows from **/
+ NodeToNode d_cnfDeps;
 
-  ClauseIdSet d_explanations;
+ ClauseIdSet d_explanations;
 
-  // The clause ID of the unit clause defining the true SAT literal.
-  ClauseId d_trueUnitClause;
-  // The clause ID of the unit clause defining the false SAT literal.
-  ClauseId d_falseUnitClause;
+ // The clause ID of the unit clause defining the true SAT literal.
+ ClauseId d_trueUnitClause;
+ // The clause ID of the unit clause defining the false SAT literal.
+ ClauseId d_falseUnitClause;
 
-  std::string d_name;
+ std::string d_name;
 public:
-  CnfProof(CVC4::prop::CnfStream* cnfStream,
-           context::Context* ctx,
-           const std::string& name);
-  ~CnfProof();
-
-  /** Methods for logging what the CnfStream does **/
-  // map the clause back to the current assertion where it came from
-  void registerConvertedClause(ClauseId clause);
-
-  /** Clause is one of the clauses defining top-level assertion node*/
-  void setClauseAssertion(ClauseId clause, Node node);
-
-  /** Current assertion being converted and whether it is an input (rather than
-   * a lemma) */
-  void pushCurrentAssertion(Node assertion, bool isInput = false);
-  void popCurrentAssertion();
-  Node getCurrentAssertion();
-  bool getCurrentAssertionKind();
-
-  /**
-   * Checks whether the assertion stack is empty.
-   */
-  bool isAssertionStackEmpty() const { return d_currentAssertionStack.empty(); }
-
-  // accessors for the leaf assertions that are being converted to CNF
-  Node getAssertionForClause(ClauseId clause);
+ CnfProof(CVC5::prop::CnfStream* cnfStream,
+          context::Context* ctx,
+          const std::string& name);
+ ~CnfProof();
+
+ /** Methods for logging what the CnfStream does **/
+ // map the clause back to the current assertion where it came from
+ void registerConvertedClause(ClauseId clause);
+
+ /** Clause is one of the clauses defining top-level assertion node*/
+ void setClauseAssertion(ClauseId clause, Node node);
+
+ /** Current assertion being converted and whether it is an input (rather than
+  * a lemma) */
+ void pushCurrentAssertion(Node assertion, bool isInput = false);
+ void popCurrentAssertion();
+ Node getCurrentAssertion();
+ bool getCurrentAssertionKind();
+
+ /**
+  * Checks whether the assertion stack is empty.
+  */
+ bool isAssertionStackEmpty() const { return d_currentAssertionStack.empty(); }
+
+ // accessors for the leaf assertions that are being converted to CNF
+ Node getAssertionForClause(ClauseId clause);
 };/* class CnfProof */
 
-} /* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__CNF_PROOF_H */
diff --git a/src/proof/dot/dot_printer.cpp b/src/proof/dot/dot_printer.cpp
index f542924b1..8ecec8484 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 CVC4 {
+namespace CVC5 {
 namespace proof {
 
 void DotPrinter::cleanQuotes(std::string& s)
@@ -91,4 +91,4 @@ void DotPrinter::ruleArguments(std::ostringstream& currentArguments,
 }
 
 }  // namespace proof
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/proof/dot/dot_printer.h b/src/proof/dot/dot_printer.h
index 4b7d7660c..173495780 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 CVC4 {
+namespace CVC5 {
 namespace proof {
 
 class DotPrinter
@@ -69,6 +69,6 @@ class DotPrinter
 };
 
 }  // namespace proof
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
 \ No newline at end of file
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 424c667fd..8b3dfd17a 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 CVC4 {
+namespace CVC5 {
 
 ProofManager::ProofManager(context::Context* context)
     : d_context(context),
@@ -217,4 +217,4 @@ void ProofManager::addUnsatCore(Node formula)
   d_outputCoreFormulas.insert(formula);
 }
 
-} /* CVC4  namespace */
+}  // namespace CVC5
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 61470e2b4..b303b996f 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 CVC4 {
+namespace CVC5 {
 
 // forward declarations
 namespace Minisat {
@@ -37,22 +37,22 @@ namespace Minisat {
 
 namespace prop {
   class CnfStream;
-}/* CVC4::prop namespace */
+  }  // namespace prop
 
 class SmtEngine;
 
 template <class Solver> class TSatProof;
-typedef TSatProof< CVC4::Minisat::Solver> CoreSatProof;
+typedef TSatProof<CVC5::Minisat::Solver> CoreSatProof;
 
 class CnfProof;
 
-typedef TSatProof<CVC4::Minisat::Solver> CoreSatProof;
+typedef TSatProof<CVC5::Minisat::Solver> CoreSatProof;
 
 namespace prop {
   typedef uint64_t SatVariable;
   class SatLiteral;
   typedef std::vector<SatLiteral> SatClause;
-}/* CVC4::prop namespace */
+  }  // namespace prop
 
 typedef std::unordered_map<ClauseId, prop::SatClause*> IdToSatClause;
 typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
@@ -81,7 +81,7 @@ public:
 
  // initialization
  void initSatProof(Minisat::Solver* solver);
- void initCnfProof(CVC4::prop::CnfStream* cnfStream, context::Context* ctx);
+ void initCnfProof(CVC5::prop::CnfStream* cnfStream, context::Context* ctx);
 
  // getting various proofs
  static CoreSatProof* getSatProof();
@@ -120,8 +120,6 @@ private:
 
 };/* class ProofManager */
 
-}/* CVC4 namespace */
-
-
+}  // namespace CVC5
 
 #endif /* CVC4__PROOF_MANAGER_H */
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index d16f8259e..298b82624 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 CVC4 {
+namespace CVC5 {
 class CnfProof;
-} /* namespace CVC4 */
+} // namespace CVC5
 
-namespace CVC4 {
+namespace CVC5 {
 /**
  * Helper debugging functions
  */
@@ -369,6 +369,6 @@ template <class Solver>
 void toSatClause(const typename Solver::TClause& minisat_cl,
                  prop::SatClause& sat_cl);
 
-} /* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__SAT__PROOF_H */
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index 06a3cc00e..6049c4876 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 CVC4 {
+namespace CVC5 {
 
 template <class Solver>
 void printLit(typename Solver::TLit l) {
@@ -1040,17 +1040,12 @@ TSatProof<Solver>::Statistics::~Statistics() {
   smtStatisticsRegistry()->unregisterStat(&d_usedClauseGlue);
 }
 
-inline std::ostream& operator<<(std::ostream& out, CVC4::ClauseKind k) {
+inline std::ostream& operator<<(std::ostream& out, CVC5::ClauseKind k)
+{
   switch (k) {
-    case CVC4::INPUT:
-      out << "INPUT";
-      break;
-    case CVC4::THEORY_LEMMA:
-      out << "THEORY_LEMMA";
-      break;
-    case CVC4::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) << "]";
   }
@@ -1058,6 +1053,6 @@ inline std::ostream& operator<<(std::ostream& out, CVC4::ClauseKind k) {
   return out;
 }
 
-} /* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__SAT__PROOF_IMPLEMENTATION_H */
diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp
index 1c7a6a556..2415daf98 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 CVC4 {
+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;
 }
 
-}/* CVC4 namespace */
+}  // namespace CVC5
diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h
index 472661db9..46dd7bf69 100644
--- a/src/proof/unsat_core.h
+++ b/src/proof/unsat_core.h
@@ -22,7 +22,7 @@
 
 #include "expr/node.h"
 
-namespace CVC4 {
+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);
 
-}/* CVC4 namespace */
+}  // namespace CVC5
 
 #endif /* CVC4__UNSAT_CORE_H */