src/proof/cnf_proof.h

   1 /*********************                                                        */
   2 /*! \file cnf_proof.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Haniel Barbosa, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 <unordered_map>
  25 #include <unordered_set>
  26
  27 #include "context/cdhashmap.h"
  28 #include "proof/clause_id.h"
  29 #include "proof/proof_manager.h"
  30
  31 namespace CVC4 {
  32 namespace prop {
  33   class CnfStream;
  34 }/* CVC4::prop namespace */
  35
  36 class CnfProof;
  37
  38 typedef std::unordered_map<prop::SatVariable, Expr> SatVarToExpr;
  39 typedef std::unordered_map<Node, Node, NodeHashFunction> NodeToNode;
  40 typedef std::unordered_set<ClauseId> ClauseIdSet;
  41
  42 typedef context::CDHashMap<ClauseId, Node> ClauseIdToNode;
  43 typedef std::pair<Node, Node> NodePair;
  44 typedef std::set<NodePair> NodePairSet;
  45
  46 typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
  47
  48 class CnfProof {
  49 protected:
  50   CVC4::prop::CnfStream* d_cnfStream;
  51
  52   /** Map from ClauseId to the assertion that lead to adding this clause **/
  53   ClauseIdToNode d_clauseToAssertion;
  54
  55   /** Top of stack is assertion currently being converted to CNF. Also saves
  56    * whether it is input (rather than a lemma). **/
  57   std::vector<std::pair<Node, bool>> d_currentAssertionStack;
  58
  59   /** Map from top-level fact to facts/assertion that it follows from **/
  60   NodeToNode d_cnfDeps;
  61
  62   ClauseIdSet d_explanations;
  63
  64   // The clause ID of the unit clause defining the true SAT literal.
  65   ClauseId d_trueUnitClause;
  66   // The clause ID of the unit clause defining the false SAT literal.
  67   ClauseId d_falseUnitClause;
  68
  69   std::string d_name;
  70 public:
  71   CnfProof(CVC4::prop::CnfStream* cnfStream,
  72            context::Context* ctx,
  73            const std::string& name);
  74   ~CnfProof();
  75
  76   /** Methods for logging what the CnfStream does **/
  77   // map the clause back to the current assertion where it came from
  78   void registerConvertedClause(ClauseId clause);
  79
  80   /** Clause is one of the clauses defining top-level assertion node*/
  81   void setClauseAssertion(ClauseId clause, Node node);
  82
  83   /** Current assertion being converted and whether it is an input (rather than
  84    * a lemma) */
  85   void pushCurrentAssertion(Node assertion, bool isInput = false);
  86   void popCurrentAssertion();
  87   Node getCurrentAssertion();
  88   bool getCurrentAssertionKind();
  89
  90   /**
  91    * Checks whether the assertion stack is empty.
  92    */
  93   bool isAssertionStackEmpty() const { return d_currentAssertionStack.empty(); }
  94
  95   // accessors for the leaf assertions that are being converted to CNF
  96   Node getAssertionForClause(ClauseId clause);
  97 };/* class CnfProof */
  98
  99 } /* CVC4 namespace */
 100
 101 #endif /* CVC4__CNF_PROOF_H */