diff options
Diffstat (limited to 'src/proof/cnf_proof.h')
| -rw-r--r-- | src/proof/cnf_proof.h | 43 |
1 files changed, 28 insertions, 15 deletions
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index a21cb1c0e..788526b80 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,9 +138,13 @@ 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; + virtual void printAtomMapping(const std::set<Node>& atoms, + std::ostream& os, + std::ostream& paren, + ProofLetMap &letMap) = 0; virtual void printClause(const prop::SatClause& clause, std::ostream& os, @@ -161,10 +169,15 @@ public: {} ~LFSCCnfProof() {} - void printAtomMapping(const NodeSet& atoms, + void printAtomMapping(const std::set<Node>& atoms, std::ostream& os, std::ostream& paren); + void printAtomMapping(const std::set<Node>& atoms, + std::ostream& os, + std::ostream& paren, + ProofLetMap &letMap); + void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren); |