src/proof/cnf_proof.h

   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);
 124   inline ClauseId getTrueUnitClause() { return d_trueUnitClause; };
 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    */
 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:
 188   LFSCCnfProof(CVC4::prop::CnfStream* cnfStream,
 189                context::Context* ctx,
 190                const std::string& name)
 191     : CnfProof(cnfStream, ctx, name)
 192   {}
 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 */