diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
commit | de0dd1dc966b05467f1a5443ff33094262f5076a (patch) | |
tree | 46a8539229fc31226b416755e6a88c18476ecffc /src/proof/cnf_proof.h | |
parent | 89ba584531115b7f6d47088d7614368ea05ab9d8 (diff) |
Revert "Merging proof branch"
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
Diffstat (limited to 'src/proof/cnf_proof.h')
-rw-r--r-- | src/proof/cnf_proof.h | 34 |
1 files changed, 15 insertions, 19 deletions
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index 62036ced0..a21cb1c0e 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -27,7 +27,6 @@ #include "context/cdhashmap.h" #include "proof/clause_id.h" -#include "proof/lemma_proof.h" #include "proof/sat_proof.h" #include "util/proof.h" @@ -44,9 +43,7 @@ typedef __gnu_cxx::hash_set<ClauseId> ClauseIdSet; typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode; typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> NodeToProofRule; -typedef std::map<std::set<Node>, LemmaProofRecipe> LemmaToRecipe; -typedef std::pair<Node, Node> NodePair; -typedef std::set<NodePair> NodePairSet; +typedef context::CDHashMap<ClauseId, theory::TheoryId> ClauseIdToTheory; class CnfProof { protected: @@ -58,8 +55,11 @@ protected: /** Map from assertion to reason for adding assertion **/ NodeToProofRule d_assertionToProofRule; - /** Map from lemma to the recipe for proving it **/ - LemmaToRecipe d_lemmaToProofRecipe; + /** 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; @@ -91,16 +91,10 @@ public: Node getAtom(prop::SatVariable var); prop::SatLiteral getLiteral(TNode node); - bool hasLiteral(TNode node); - void ensureLiteral(TNode node, bool noPreregistration = false); - void collectAtoms(const prop::SatClause* clause, - std::set<Node>& atoms); + NodeSet& atoms); void collectAtomsForClauses(const IdToSatClause& clauses, - std::set<Node>& atoms); - void collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses, - std::set<Node>& atoms, - NodePairSet& rewrites); + NodeSet& atoms); void collectAssertionsForClauses(const IdToSatClause& clauses, NodeSet& assertions); @@ -127,9 +121,11 @@ public: void popCurrentDefinition(); Node getCurrentDefinition(); - void setProofRecipe(LemmaProofRecipe* proofRecipe); - LemmaProofRecipe getProofRecipe(const std::set<Node> &lemma); - bool haveProofRecipe(const std::set<Node> &lemma); + 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); @@ -138,7 +134,7 @@ public: Node getAssertionForClause(ClauseId clause); /** Virtual methods for printing things **/ - virtual void printAtomMapping(const std::set<Node>& atoms, + virtual void printAtomMapping(const NodeSet& atoms, std::ostream& os, std::ostream& paren) = 0; @@ -165,7 +161,7 @@ public: {} ~LFSCCnfProof() {} - void printAtomMapping(const std::set<Node>& atoms, + void printAtomMapping(const NodeSet& atoms, std::ostream& os, std::ostream& paren); |