diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-31 15:23:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-31 22:23:17 +0000 |
commit | a1466978fbc328507406d4a121dab4d1a1047e1d (patch) | |
tree | 12b40f161bb4d7a6ee40c20c78a15d6cda3c1995 /src/proof/cnf_proof.h | |
parent | f9a9af855fb65804ff0b36e764ccd9d0fa9f87f8 (diff) |
Rename namespace CVC4 to CVC5. (#6249)
Diffstat (limited to 'src/proof/cnf_proof.h')
-rw-r--r-- | src/proof/cnf_proof.h | 86 |
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 */ |