Rename namespace CVC4 to CVC5. (#6249)

1 files changed, 43 insertions, 43 deletions

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 */