src/proof/cnf_proof.h

   1 /*********************                                                        */
   2 /*! \file cnf_proof.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Guy Katz, Morgan Deters
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 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/proof.h"
  33
  34 namespace CVC4 {
  35 namespace prop {
  36   class CnfStream;
  37 }/* CVC4::prop namespace */
  38
  39 class CnfProof;
  40
  41 typedef std::unordered_map<prop::SatVariable, Expr> SatVarToExpr;
  42 typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode;
  43 typedef std::unordered_set<ClauseId> ClauseIdSet;
  44
  45 typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode;
  46 typedef context::CDHashMap<Node, ProofRule, NodeHashFunction> NodeToProofRule;
  47 typedef std::map<std::set<Node>, LemmaProofRecipe> LemmaToRecipe;
  48 typedef std::pair<Node, Node> NodePair;
  49 typedef std::set<NodePair> NodePairSet;
  50
  51 class CnfProof {
  52 protected:
  53   CVC4::prop::CnfStream* d_cnfStream;
  54
  55   /** Map from ClauseId to the assertion that lead to adding this clause **/
  56   ClauseIdToNode d_clauseToAssertion;
  57
  58   /** Map from assertion to reason for adding assertion  **/
  59   NodeToProofRule d_assertionToProofRule;
  60
  61   /** Map from lemma to the recipe for proving it **/
  62   LemmaToRecipe d_lemmaToProofRecipe;
  63
  64   /** Top of stack is assertion currently being converted to CNF **/
  65   std::vector<Node> d_currentAssertionStack;
  66
  67   /** Top of stack is top-level fact currently being converted to CNF **/
  68   std::vector<Node> d_currentDefinitionStack;
  69
  70   /** Map from ClauseId to the top-level fact that lead to adding this clause **/
  71   ClauseIdToNode d_clauseToDefinition;
  72
  73   /** Top-level facts that follow from assertions during convertAndAssert **/
  74   NodeSet d_definitions;
  75
  76   /** Map from top-level fact to facts/assertion that it follows from **/
  77   NodeToNode d_cnfDeps;
  78
  79   ClauseIdSet d_explanations;
  80
  81   bool isDefinition(Node node);
  82
  83   Node getDefinitionForClause(ClauseId clause);
  84
  85   std::string d_name;
  86 public:
  87   CnfProof(CVC4::prop::CnfStream* cnfStream,
  88            context::Context* ctx,
  89            const std::string& name);
  90
  91
  92   Node getAtom(prop::SatVariable var);
  93   prop::SatLiteral getLiteral(TNode node);
  94   bool hasLiteral(TNode node);
  95   void ensureLiteral(TNode node, bool noPreregistration = false);
  96
  97   void collectAtoms(const prop::SatClause* clause,
  98                     std::set<Node>& atoms);
  99   void collectAtomsForClauses(const IdToSatClause& clauses,
 100                               std::set<Node>& atoms);
 101   void collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses,
 102                                         std::set<Node>& atoms,
 103                                         NodePairSet& rewrites);
 104   void collectAssertionsForClauses(const IdToSatClause& clauses,
 105                                    NodeSet& assertions);
 106
 107   /** Methods for logging what the CnfStream does **/
 108   // map the clause back to the current assertion where it came from
 109   // if it is an explanation, it does not have a CNF proof since it is
 110   // already in CNF
 111   void registerConvertedClause(ClauseId clause, bool explanation=false);
 112
 113   /** Clause is one of the clauses defining the node expression*/
 114   void setClauseDefinition(ClauseId clause, Node node);
 115
 116   /** Clause is one of the clauses defining top-level assertion node*/
 117   void setClauseAssertion(ClauseId clause, Node node);
 118
 119   void registerAssertion(Node assertion, ProofRule reason);
 120   void setCnfDependence(Node from, Node to);
 121
 122   void pushCurrentAssertion(Node assertion); // the current assertion being converted
 123   void popCurrentAssertion();
 124   Node getCurrentAssertion();
 125
 126   void pushCurrentDefinition(Node assertion); // the current Tseitin definition being converted
 127   void popCurrentDefinition();
 128   Node getCurrentDefinition();
 129
 130   void setProofRecipe(LemmaProofRecipe* proofRecipe);
 131   LemmaProofRecipe getProofRecipe(const std::set<Node> &lemma);
 132   bool haveProofRecipe(const std::set<Node> &lemma);
 133
 134   // accessors for the leaf assertions that are being converted to CNF
 135   bool isAssertion(Node node);
 136   ProofRule getProofRule(Node assertion);
 137   ProofRule getProofRule(ClauseId clause);
 138   Node getAssertionForClause(ClauseId clause);
 139
 140   /** Virtual methods for printing things **/
 141   virtual void printAtomMapping(const std::set<Node>& atoms,
 142                                 std::ostream& os,
 143                                 std::ostream& paren) = 0;
 144   virtual void printAtomMapping(const std::set<Node>& atoms,
 145                            std::ostream& os,
 146                            std::ostream& paren,
 147                            ProofLetMap &letMap) = 0;
 148
 149   virtual void printClause(const prop::SatClause& clause,
 150                            std::ostream& os,
 151                            std::ostream& paren) = 0;
 152   virtual void printCnfProofForClause(ClauseId id,
 153                                       const prop::SatClause* clause,
 154                                       std::ostream& os,
 155                                       std::ostream& paren) = 0;
 156   virtual ~CnfProof();
 157 };/* class CnfProof */
 158
 159 class LFSCCnfProof : public CnfProof {
 160   Node clauseToNode( const prop::SatClause& clause,
 161                      std::map<Node, unsigned>& childIndex,
 162                      std::map<Node, bool>& childPol );
 163   bool printProofTopLevel(Node e, std::ostream& out);
 164 public:
 165   LFSCCnfProof(CVC4::prop::CnfStream* cnfStream,
 166                context::Context* ctx,
 167                const std::string& name)
 168     : CnfProof(cnfStream, ctx, name)
 169   {}
 170   ~LFSCCnfProof() {}
 171
 172   void printAtomMapping(const std::set<Node>& atoms,
 173                         std::ostream& os,
 174                         std::ostream& paren) override;
 175
 176   void printAtomMapping(const std::set<Node>& atoms,
 177                         std::ostream& os,
 178                         std::ostream& paren,
 179                         ProofLetMap& letMap) override;
 180
 181   void printClause(const prop::SatClause& clause,
 182                    std::ostream& os,
 183                    std::ostream& paren) override;
 184   void printCnfProofForClause(ClauseId id,
 185                               const prop::SatClause* clause,
 186                               std::ostream& os,
 187                               std::ostream& paren) override;
 188 };/* class LFSCCnfProof */
 189
 190 } /* CVC4 namespace */
 191
 192 #endif /* __CVC4__CNF_PROOF_H */