src/proof/resolution_bitvector_proof.h

   1 /*********************                                                        */
   2 /*! \file resolution_bitvector_proof.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Liana Hadarean, Mathias Preiner, Guy Katz
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2018 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
  13  **
  14  ** Bitvector proof
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H
  20 #define __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H
  21
  22 #include <iosfwd>
  23
  24 #include "context/context.h"
  25 #include "expr/expr.h"
  26 #include "proof/bitvector_proof.h"
  27 #include "proof/theory_proof.h"
  28 #include "prop/bvminisat/core/Solver.h"
  29
  30 namespace CVC4 {
  31
  32 namespace theory {
  33 namespace bv {
  34 class TheoryBV;
  35 template <class T>
  36 class TBitblaster;
  37 }  // namespace bv
  38 }  // namespace theory
  39
  40 // TODO(aozdemir) break the sat_solver - resolution_bitvectorproof - cnf_stream
  41 // header cycle and remove this.
  42 namespace prop {
  43 class CnfStream;
  44 }
  45
  46 } /* namespace CVC4 */
  47
  48
  49 namespace CVC4 {
  50
  51 template <class Solver>
  52 class TSatProof;
  53 typedef TSatProof<CVC4::BVMinisat::Solver> BVSatProof;
  54
  55 namespace proof {
  56
  57 /**
  58  * Represents a bitvector proof which is backed by
  59  * (a) bitblasting and
  60  * (b) a resolution unsat proof.
  61  *
  62  * Contains tools for constructing BV conflicts
  63  */
  64 class ResolutionBitVectorProof : public BitVectorProof
  65 {
  66  public:
  67   ResolutionBitVectorProof(theory::bv::TheoryBV* bv,
  68                            TheoryProofEngine* proofEngine);
  69
  70   /**
  71    * Create an (internal) SAT proof object
  72    * Must be invoked before manipulating BV conflicts,
  73    * or initializing a BNF proof
  74    */
  75   void initSatProof(CVC4::BVMinisat::Solver* solver);
  76
  77   BVSatProof* getSatProof();
  78
  79   /**
  80    * Kind of a mess.
  81    * In eager mode this must be invoked before printing a proof of the empty
  82    * clause. In lazy mode the behavior is ???
  83    * TODO(aozdemir) clean this up.
  84    */
  85   void finalizeConflicts(std::vector<Expr>& conflicts);
  86
  87   void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr);
  88   void startBVConflict(CVC4::BVMinisat::Solver::TLit lit);
  89   void endBVConflict(const BVMinisat::Solver::TLitVec& confl);
  90
  91   void markAssumptionConflict() { d_isAssumptionConflict = true; }
  92   bool isAssumptionConflict() const { return d_isAssumptionConflict; }
  93
  94   virtual void printResolutionProof(std::ostream& os,
  95                                     std::ostream& paren,
  96                                     ProofLetMap& letMap) = 0;
  97
  98   void initCnfProof(prop::CnfStream* cnfStream, context::Context* cnf) override;
  99
 100  protected:
 101   context::Context d_fakeContext;
 102
 103   // The CNF formula that results from bit-blasting will need a proof.
 104   // This is that proof.
 105   std::unique_ptr<BVSatProof> d_resolutionProof;
 106
 107   bool d_isAssumptionConflict;
 108
 109   theory::TheoryId getTheoryId() override;
 110 };
 111
 112 class LFSCBitVectorProof : public ResolutionBitVectorProof
 113 {
 114  public:
 115   LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
 116       : ResolutionBitVectorProof(bv, proofEngine)
 117   {
 118   }
 119   void printTheoryLemmaProof(std::vector<Expr>& lemma,
 120                              std::ostream& os,
 121                              std::ostream& paren,
 122                              const ProofLetMap& map) override;
 123   void printResolutionProof(std::ostream& os,
 124                             std::ostream& paren,
 125                             ProofLetMap& letMap) override;
 126   void calculateAtomsInBitblastingProof() override;
 127 };
 128
 129 }  // namespace proof
 130
 131 }  // namespace CVC4
 132
 133 #endif /* __CVC4__PROOF__RESOLUTIONBITVECTORPROOF_H */