src/proof/clausal_bitvector_proof.h

   1 /*********************                                                        */
   2 /*! \file clausal_bitvector_proof.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Alex Ozdemir, Mathias Preiner
   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 Bitvector proof for clausal (DRAT/LRAT) formats
  13  **
  14  ** An internal string stream is hooked up to CryptoMiniSat, which spits out a
  15  ** binary DRAT proof. Depending on which kind of proof we're going to turn
  16  ** that into, we process it in different ways.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
  22 #define CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
  23
  24 #include <iostream>
  25 #include <sstream>
  26 #include <unordered_map>
  27
  28 #include "expr/expr.h"
  29 #include "proof/bitvector_proof.h"
  30 #include "proof/drat/drat_proof.h"
  31 #include "proof/lrat/lrat_proof.h"
  32 #include "proof/theory_proof.h"
  33 #include "prop/cnf_stream.h"
  34 #include "prop/sat_solver_types.h"
  35 #include "theory/bv/theory_bv.h"
  36 #include "util/statistics_registry.h"
  37
  38 namespace CVC4 {
  39
  40 namespace proof {
  41
  42 class ClausalBitVectorProof : public BitVectorProof
  43 {
  44  public:
  45   ClausalBitVectorProof(theory::bv::TheoryBV* bv,
  46                         TheoryProofEngine* proofEngine);
  47
  48   ~ClausalBitVectorProof() = default;
  49
  50   void attachToSatSolver(prop::SatSolver& sat_solver) override;
  51
  52   void initCnfProof(prop::CnfStream* cnfStream,
  53                     context::Context* cnf,
  54                     prop::SatVariable trueVar,
  55                     prop::SatVariable falseVar) override;
  56
  57   std::ostream& getDratOstream() { return d_binaryDratProof; }
  58
  59   void registerUsedClause(ClauseId id, prop::SatClause& clause);
  60
  61   void calculateAtomsInBitblastingProof() override;
  62
  63  protected:
  64   // A list of all clauses and their ids which are passed into the SAT solver
  65   std::unordered_map<ClauseId, prop::SatClause> d_clauses{};
  66   std::vector<ClauseId> d_originalClauseIndices{};
  67   // Stores the proof recieved from the SAT solver.
  68   std::ostringstream d_binaryDratProof{};
  69   std::vector<ClauseId> d_coreClauseIndices{};
  70
  71   struct DratTranslationStatistics
  72   {
  73     DratTranslationStatistics();
  74     ~DratTranslationStatistics();
  75
  76     // Total time spent doing translation (optimized binary DRAT -> in memory
  77     // target format including IO, postprocessing, etc.)
  78     TimerStat d_totalTime;
  79     // Time that the external tool actually spent
  80     TimerStat d_toolTime;
  81   };
  82
  83   DratTranslationStatistics d_dratTranslationStatistics;
  84
  85  private:
  86   // Optimizes the DRAT proof stored in `d_binaryDratProof` and returns a list
  87   // of clause actually needed to check that proof (a smaller UNSAT core)
  88   void optimizeDratProof();
  89
  90   // Given reference to a SAT clause encoded as a vector of literals, puts the
  91   // literals into a canonical order
  92   static void canonicalizeClause(prop::SatClause& clause);
  93
  94   struct DratOptimizationStatistics
  95   {
  96     DratOptimizationStatistics();
  97     ~DratOptimizationStatistics();
  98
  99     // Total time spent using drat-trim to optimize the DRAT proof/formula
 100     // (including IO, etc.)
 101     TimerStat d_totalTime;
 102     // Time that drat-trim actually spent optimizing the DRAT proof/formula
 103     TimerStat d_toolTime;
 104     // Time that was spent matching clauses in drat-trim's output to clauses in
 105     // its input
 106     TimerStat d_clauseMatchingTime;
 107     // Bytes in binary DRAT proof before optimization
 108     IntStat d_initialDratSize;
 109     // Bytes in binary DRAT proof after optimization
 110     IntStat d_optimizedDratSize;
 111     // Bytes in textual DIMACS bitblasted formula before optimization
 112     IntStat d_initialFormulaSize;
 113     // Bytes in textual DIMACS bitblasted formula after optimization
 114     IntStat d_optimizedFormulaSize;
 115   };
 116
 117   DratOptimizationStatistics d_dratOptimizationStatistics;
 118 };
 119
 120 /**
 121  * A representation of a clausal proof of a bitvector problem's UNSAT nature
 122  */
 123 class LfscClausalBitVectorProof : public ClausalBitVectorProof
 124 {
 125  public:
 126   LfscClausalBitVectorProof(theory::bv::TheoryBV* bv,
 127                             TheoryProofEngine* proofEngine)
 128       : ClausalBitVectorProof(bv, proofEngine)
 129   {
 130   }
 131
 132   void printTheoryLemmaProof(std::vector<Expr>& lemma,
 133                              std::ostream& os,
 134                              std::ostream& paren,
 135                              const ProofLetMap& map) override;
 136   void printBBDeclarationAndCnf(std::ostream& os,
 137                                 std::ostream& paren,
 138                                 ProofLetMap& letMap) override;
 139 };
 140
 141 /**
 142  * A DRAT proof for a bit-vector problem
 143  */
 144 class LfscDratBitVectorProof : public LfscClausalBitVectorProof
 145 {
 146  public:
 147   LfscDratBitVectorProof(theory::bv::TheoryBV* bv,
 148                          TheoryProofEngine* proofEngine)
 149       : LfscClausalBitVectorProof(bv, proofEngine)
 150   {
 151   }
 152
 153   void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
 154 };
 155
 156 /**
 157  * An LRAT proof for a bit-vector problem
 158  */
 159 class LfscLratBitVectorProof : public LfscClausalBitVectorProof
 160 {
 161  public:
 162   LfscLratBitVectorProof(theory::bv::TheoryBV* bv,
 163                          TheoryProofEngine* proofEngine)
 164       : LfscClausalBitVectorProof(bv, proofEngine)
 165   {
 166   }
 167
 168   void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
 169 };
 170
 171 /**
 172  * An Extended Resolution proof for a bit-vector problem
 173  */
 174 class LfscErBitVectorProof : public LfscClausalBitVectorProof
 175 {
 176  public:
 177   LfscErBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
 178       : LfscClausalBitVectorProof(bv, proofEngine)
 179   {
 180   }
 181
 182   void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
 183 };
 184
 185 }  // namespace proof
 186
 187 }  // namespace CVC4
 188
 189 #endif /* CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H */