diff options
Diffstat (limited to 'src/proof/cnf_proof.h')
| -rw-r--r-- | src/proof/cnf_proof.h | 136 |
1 files changed, 116 insertions, 20 deletions
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h index d3e59ef93..675bd9b9d 100644 --- a/src/proof/cnf_proof.h +++ b/src/proof/cnf_proof.h @@ -21,11 +21,14 @@ #ifndef __CVC4__CNF_PROOF_H #define __CVC4__CNF_PROOF_H -#include <ext/hash_map> +#include <ext/hash_map> #include <ext/hash_set> #include <iosfwd> +#include "context/cdhashmap.h" #include "proof/sat_proof.h" +#include "proof/sat_proof.h" +#include "util/proof.h" #include "util/proof.h" namespace CVC4 { @@ -35,38 +38,131 @@ namespace prop { class CnfProof; +typedef __gnu_cxx::hash_map<prop::SatVariable, Expr> SatVarToExpr; +typedef __gnu_cxx::hash_map<Node, Node, NodeHashFunction> NodeToNode; +typedef __gnu_cxx::hash_set<ClauseId> ClauseIdSet; + +typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode; +typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> NodeToProofRule; + class CnfProof { protected: CVC4::prop::CnfStream* d_cnfStream; - VarSet d_atomsDeclared; + + /** Map from ClauseId to the assertion that lead to adding this clause **/ + ClauseIdToNode d_clauseToAssertion; + + /** Map from assertion to reason for adding assertion **/ + NodeToProofRule d_assertionToProofRule; + + /** 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); + CnfProof(CVC4::prop::CnfStream* cnfStream, + context::Context* ctx, + const std::string& name); + + + Node getAtom(prop::SatVariable var); + prop::SatLiteral getLiteral(TNode node); + void collectAtoms(const prop::SatClause* clause, + NodeSet& atoms); + void collectAtomsForClauses(const IdToSatClause& clauses, + NodeSet& atoms); + void collectAssertionsForClauses(const IdToSatClause& clauses, + NodeSet& assertions); + + /** Methods for logging what the CnfStream does **/ + // map the clause back to the current assertion where it came from + // if it is an explanation, it does not have a CNF proof since it is + // already in CNF + void registerConvertedClause(ClauseId clause, bool explanation=false); + + /** Clause is one of the clauses defining the node expression*/ + void setClauseDefinition(ClauseId clause, Node node); + + /** 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(); + + void pushCurrentDefinition(Node assertion); // the current Tseitin definition being converted + void popCurrentDefinition(); + Node getCurrentDefinition(); + + + // 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); - Expr getAtom(prop::SatVariable var); - Expr getAssertion(uint64_t id); - prop::SatLiteral getLiteral(TNode atom); + + /** Virtual methods for printing things **/ + virtual void printAtomMapping(const NodeSet& atoms, + std::ostream& os, + std::ostream& paren) = 0; - virtual void printClauses(std::ostream& os, std::ostream& paren) = 0; + virtual void printClause(const prop::SatClause& clause, + std::ostream& os, + std::ostream& paren) = 0; + virtual void printCnfProofForClause(ClauseId id, + const prop::SatClause* clause, + std::ostream& os, + std::ostream& paren) = 0; virtual ~CnfProof(); };/* class CnfProof */ class LFSCCnfProof : public CnfProof { - void printPreprocess(std::ostream& os, std::ostream& paren); - void printInputClauses(std::ostream& os, std::ostream& paren); - void printTheoryLemmas(std::ostream& os, std::ostream& paren); - void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren); - virtual void printAtomMapping(const prop::SatClause* clause, std::ostream& os, std::ostream& paren); - - Expr clauseToExpr( const prop::SatClause& clause, - std::map< Expr, unsigned >& childIndex, - std::map< Expr, bool >& childPol ); - + Node clauseToNode( const prop::SatClause& clause, + std::map<Node, unsigned>& childIndex, + std::map<Node, bool>& childPol ); + bool printProofTopLevel(Node e, std::ostream& out); public: - LFSCCnfProof(CVC4::prop::CnfStream* cnfStream) - : CnfProof(cnfStream) + LFSCCnfProof(CVC4::prop::CnfStream* cnfStream, + context::Context* ctx, + const std::string& name) + : CnfProof(cnfStream, ctx, name) {} + ~LFSCCnfProof() {} - virtual void printClauses(std::ostream& os, std::ostream& paren); + void printAtomMapping(const NodeSet& atoms, + std::ostream& os, + std::ostream& paren); + + void printClause(const prop::SatClause& clause, + std::ostream& os, + std::ostream& paren); + void printCnfProofForClause(ClauseId id, + const prop::SatClause* clause, + std::ostream& os, + std::ostream& paren); };/* class LFSCCnfProof */ } /* CVC4 namespace */ |