diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:33:41 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:33:41 -0700 |
commit | 89ba584531115b7f6d47088d7614368ea05ab9d8 (patch) | |
tree | aae1792c05c0a67c521160226deb451ca861822c /src/proof/cnf_proof.h | |
parent | 324ca0376c960c75f621f0102eeaa1186589dda7 (diff) |
Merging proof branch
Diffstat (limited to 'src/proof/cnf_proof.h')
-rw-r--r-- | src/proof/cnf_proof.h | 34 |
1 files changed, 19 insertions, 15 deletions
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index a21cb1c0e..62036ced0 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -27,6 +27,7 @@ #include "context/cdhashmap.h" #include "proof/clause_id.h" +#include "proof/lemma_proof.h" #include "proof/sat_proof.h" #include "util/proof.h" @@ -43,7 +44,9 @@ 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; +typedef std::map<std::set<Node>, LemmaProofRecipe> LemmaToRecipe; +typedef std::pair<Node, Node> NodePair; +typedef std::set<NodePair> NodePairSet; class CnfProof { protected: @@ -55,11 +58,8 @@ 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; + /** Map from lemma to the recipe for proving it **/ + LemmaToRecipe d_lemmaToProofRecipe; /** Top of stack is assertion currently being converted to CNF **/ std::vector<Node> d_currentAssertionStack; @@ -91,10 +91,16 @@ 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, - NodeSet& atoms); + std::set<Node>& atoms); void collectAtomsForClauses(const IdToSatClause& clauses, - NodeSet& atoms); + std::set<Node>& atoms); + void collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses, + std::set<Node>& atoms, + NodePairSet& rewrites); void collectAssertionsForClauses(const IdToSatClause& clauses, NodeSet& assertions); @@ -121,11 +127,9 @@ public: void popCurrentDefinition(); Node getCurrentDefinition(); - void setExplainerTheory(theory::TheoryId theory); - theory::TheoryId getExplainerTheory(); - theory::TheoryId getOwnerTheory(ClauseId clause); - - void registerExplanationLemma(ClauseId clauseId); + void setProofRecipe(LemmaProofRecipe* proofRecipe); + LemmaProofRecipe getProofRecipe(const std::set<Node> &lemma); + bool haveProofRecipe(const std::set<Node> &lemma); // accessors for the leaf assertions that are being converted to CNF bool isAssertion(Node node); @@ -134,7 +138,7 @@ public: Node getAssertionForClause(ClauseId clause); /** Virtual methods for printing things **/ - virtual void printAtomMapping(const NodeSet& atoms, + virtual void printAtomMapping(const std::set<Node>& atoms, std::ostream& os, std::ostream& paren) = 0; @@ -161,7 +165,7 @@ public: {} ~LFSCCnfProof() {} - void printAtomMapping(const NodeSet& atoms, + void printAtomMapping(const std::set<Node>& atoms, std::ostream& os, std::ostream& paren); |