1 /********************* */ 2 /*! \file cnf_proof.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Liana Hadarean, Guy Katz, Alex Ozdemir 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief A manager for CnfProofs. 13 ** 14 ** A manager for CnfProofs. 15 ** 16 ** 17 **/ 18 19 #include "cvc4_private.h" 20 21 #ifndef __CVC4__CNF_PROOF_H 22 #define __CVC4__CNF_PROOF_H 23 24 #include <iosfwd> 25 #include <unordered_map> 26 #include <unordered_set> 27 28 #include "context/cdhashmap.h" 29 #include "proof/clause_id.h" 30 #include "proof/lemma_proof.h" 31 #include "proof/sat_proof.h" 32 #include "util/maybe.h" 33 #include "util/proof.h" 34 35 namespace CVC4 { 36 namespace prop { 37 class CnfStream; 38 }/* CVC4::prop namespace */ 39 40 class CnfProof; 41 42 typedef std::unordered_map<prop::SatVariable, Expr> SatVarToExpr; 43 typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode; 44 typedef std::unordered_set<ClauseId> ClauseIdSet; 45 46 typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode; 47 typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> NodeToProofRule; 48 typedef std::map<std::set<Node>, LemmaProofRecipe> LemmaToRecipe; 49 typedef std::pair<Node, Node> NodePair; 50 typedef std::set<NodePair> NodePairSet; 51 52 class CnfProof { 53 protected: 54 CVC4::prop::CnfStream* d_cnfStream; 55 56 /** Map from ClauseId to the assertion that lead to adding this clause **/ 57 ClauseIdToNode d_clauseToAssertion; 58 59 /** Map from assertion to reason for adding assertion **/ 60 NodeToProofRule d_assertionToProofRule; 61 62 /** Map from lemma to the recipe for proving it **/ 63 LemmaToRecipe d_lemmaToProofRecipe; 64 65 /** Top of stack is assertion currently being converted to CNF **/ 66 std::vector<Node> d_currentAssertionStack; 67 68 /** Top of stack is top-level fact currently being converted to CNF **/ 69 std::vector<Node> d_currentDefinitionStack; 70 71 /** Map from ClauseId to the top-level fact that lead to adding this clause **/ 72 ClauseIdToNode d_clauseToDefinition; 73 74 /** Top-level facts that follow from assertions during convertAndAssert **/ 75 NodeSet d_definitions; 76 77 /** Map from top-level fact to facts/assertion that it follows from **/ 78 NodeToNode d_cnfDeps; 79 80 ClauseIdSet d_explanations; 81 82 // The clause ID of the unit clause defining the true SAT literal. 83 ClauseId d_trueUnitClause; 84 // The clause ID of the unit clause defining the false SAT literal. 85 ClauseId d_falseUnitClause; 86 87 bool isDefinition(Node node); 88 89 Node getDefinitionForClause(ClauseId clause); 90 91 std::string d_name; 92 public: 93 CnfProof(CVC4::prop::CnfStream* cnfStream, 94 context::Context* ctx, 95 const std::string& name); 96 97 98 Node getAtom(prop::SatVariable var); 99 prop::SatLiteral getLiteral(TNode node); 100 bool hasLiteral(TNode node); 101 void ensureLiteral(TNode node, bool noPreregistration = false); 102 103 void collectAtoms(const prop::SatClause* clause, 104 std::set<Node>& atoms); 105 void collectAtomsForClauses(const IdToSatClause& clauses, 106 std::set<Node>& atoms); 107 void collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses, 108 std::set<Node>& atoms, 109 NodePairSet& rewrites); 110 void collectAssertionsForClauses(const IdToSatClause& clauses, 111 NodeSet& assertions); 112 113 /** Methods for logging what the CnfStream does **/ 114 // map the clause back to the current assertion where it came from 115 // if it is an explanation, it does not have a CNF proof since it is 116 // already in CNF 117 void registerConvertedClause(ClauseId clause, bool explanation=false); 118 119 // The CNF proof has a special relationship to true and false. 120 // In particular, it need to know the identity of clauses defining 121 // canonical true and false literals in the underlying SAT solver. 122 void registerTrueUnitClause(ClauseId clauseId); 123 void registerFalseUnitClause(ClauseId clauseId); getTrueUnitClause()124 inline ClauseId getTrueUnitClause() { return d_trueUnitClause; }; getFalseUnitClause()125 inline ClauseId getFalseUnitClause() { return d_falseUnitClause; }; 126 127 /** Clause is one of the clauses defining the node expression*/ 128 void setClauseDefinition(ClauseId clause, Node node); 129 130 /** Clause is one of the clauses defining top-level assertion node*/ 131 void setClauseAssertion(ClauseId clause, Node node); 132 133 void registerAssertion(Node assertion, ProofRule reason); 134 void setCnfDependence(Node from, Node to); 135 136 void pushCurrentAssertion(Node assertion); // the current assertion being converted 137 void popCurrentAssertion(); 138 Node getCurrentAssertion(); 139 140 void pushCurrentDefinition(Node assertion); // the current Tseitin definition being converted 141 void popCurrentDefinition(); 142 Node getCurrentDefinition(); 143 144 /** 145 * Checks whether the assertion stack is empty. 146 */ isAssertionStackEmpty()147 bool isAssertionStackEmpty() const { return d_currentAssertionStack.empty(); } 148 149 void setProofRecipe(LemmaProofRecipe* proofRecipe); 150 LemmaProofRecipe getProofRecipe(const std::set<Node> &lemma); 151 bool haveProofRecipe(const std::set<Node> &lemma); 152 153 // accessors for the leaf assertions that are being converted to CNF 154 bool isAssertion(Node node); 155 ProofRule getProofRule(Node assertion); 156 ProofRule getProofRule(ClauseId clause); 157 Node getAssertionForClause(ClauseId clause); 158 159 /** Virtual methods for printing things **/ 160 virtual void printAtomMapping(const std::set<Node>& atoms, 161 std::ostream& os, 162 std::ostream& paren) = 0; 163 virtual void printAtomMapping(const std::set<Node>& atoms, 164 std::ostream& os, 165 std::ostream& paren, 166 ProofLetMap &letMap) = 0; 167 168 // Detects whether a clause has x v ~x for some x 169 // If so, returns the positive occurence's idx first, then the negative's 170 static Maybe<std::pair<size_t, size_t>> detectTrivialTautology( 171 const prop::SatClause& clause); 172 virtual void printClause(const prop::SatClause& clause, 173 std::ostream& os, 174 std::ostream& paren) = 0; 175 virtual void printCnfProofForClause(ClauseId id, 176 const prop::SatClause* clause, 177 std::ostream& os, 178 std::ostream& paren) = 0; 179 virtual ~CnfProof(); 180 };/* class CnfProof */ 181 182 class LFSCCnfProof : public CnfProof { 183 Node clauseToNode( const prop::SatClause& clause, 184 std::map<Node, unsigned>& childIndex, 185 std::map<Node, bool>& childPol ); 186 bool printProofTopLevel(Node e, std::ostream& out); 187 public: LFSCCnfProof(CVC4::prop::CnfStream * cnfStream,context::Context * ctx,const std::string & name)188 LFSCCnfProof(CVC4::prop::CnfStream* cnfStream, 189 context::Context* ctx, 190 const std::string& name) 191 : CnfProof(cnfStream, ctx, name) 192 {} ~LFSCCnfProof()193 ~LFSCCnfProof() {} 194 195 void printAtomMapping(const std::set<Node>& atoms, 196 std::ostream& os, 197 std::ostream& paren) override; 198 199 void printAtomMapping(const std::set<Node>& atoms, 200 std::ostream& os, 201 std::ostream& paren, 202 ProofLetMap& letMap) override; 203 204 void printClause(const prop::SatClause& clause, 205 std::ostream& os, 206 std::ostream& paren) override; 207 void printCnfProofForClause(ClauseId id, 208 const prop::SatClause* clause, 209 std::ostream& os, 210 std::ostream& paren) override; 211 };/* class LFSCCnfProof */ 212 213 } /* CVC4 namespace */ 214 215 #endif /* __CVC4__CNF_PROOF_H */ 216