diff options
Diffstat (limited to 'src/proof/cnf_proof.h')
-rw-r--r-- | src/proof/cnf_proof.h | 30 |
1 files changed, 20 insertions, 10 deletions
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index e5a80b428..b4df850f7 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -21,7 +21,7 @@ #ifndef __CVC4__CNF_PROOF_H #define __CVC4__CNF_PROOF_H -#include <ext/hash_map> +#include <ext/hash_map> #include <ext/hash_set> #include <iosfwd> @@ -43,6 +43,7 @@ typedef __gnu_cxx::hash_set<ClauseId> ClauseIdSet; typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode; typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> NodeToProofRule; +typedef context::CDHashMap<ClauseId, theory::TheoryId> ClauseIdToTheory; class CnfProof { protected: @@ -54,28 +55,33 @@ protected: /** Map from assertion to reason for adding assertion **/ NodeToProofRule d_assertionToProofRule; + /** Map from assertion to the theory that added this assertion **/ + ClauseIdToTheory d_clauseIdToOwnerTheory; + + /** The last theory to explain a lemma **/ + theory::TheoryId d_explainerTheory; + /** Top of stack is assertion currently being converted to CNF **/ std::vector<Node> d_currentAssertionStack; /** Top of stack is top-level fact currently being converted to CNF **/ std::vector<Node> d_currentDefinitionStack; - /** Map from ClauseId to the top-level fact that lead to adding this clause **/ ClauseIdToNode d_clauseToDefinition; /** Top-level facts that follow from assertions during convertAndAssert **/ NodeSet d_definitions; - + /** Map from top-level fact to facts/assertion that it follows from **/ NodeToNode d_cnfDeps; ClauseIdSet d_explanations; - + bool isDefinition(Node node); Node getDefinitionForClause(ClauseId clause); - + std::string d_name; public: CnfProof(CVC4::prop::CnfStream* cnfStream, @@ -103,10 +109,10 @@ public: /** Clause is one of the clauses defining top-level assertion node*/ void setClauseAssertion(ClauseId clause, Node node); - + void registerAssertion(Node assertion, ProofRule reason); void setCnfDependence(Node from, Node to); - + void pushCurrentAssertion(Node assertion); // the current assertion being converted void popCurrentAssertion(); Node getCurrentAssertion(); @@ -115,14 +121,18 @@ public: void popCurrentDefinition(); Node getCurrentDefinition(); - + void setExplainerTheory(theory::TheoryId theory); + theory::TheoryId getExplainerTheory(); + theory::TheoryId getOwnerTheory(ClauseId clause); + + void registerExplanationLemma(ClauseId clauseId); + // accessors for the leaf assertions that are being converted to CNF bool isAssertion(Node node); ProofRule getProofRule(Node assertion); ProofRule getProofRule(ClauseId clause); Node getAssertionForClause(ClauseId clause); - /** Virtual methods for printing things **/ virtual void printAtomMapping(const NodeSet& atoms, std::ostream& os, @@ -154,7 +164,7 @@ public: void printAtomMapping(const NodeSet& atoms, std::ostream& os, std::ostream& paren); - + void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren); |