1 /*********************                                                        */
2 /*! \file resolution_bitvector_proof.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Alex Ozdemir, Mathias Preiner, Liana Hadarean
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 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/sat_proof.h"
28 #include "proof/theory_proof.h"
29 #include "prop/bvminisat/core/Solver.h"
30 #include "prop/cnf_stream.h"
31 #include "prop/sat_solver_types.h"
32 #include "theory/bv/bitblast/bitblaster.h"
33 #include "theory/bv/theory_bv.h"
34 
35 namespace CVC4 {
36 
37 typedef TSatProof<CVC4::BVMinisat::Solver> BVSatProof;
38 
39 namespace proof {
40 
41 /**
42  * Represents a bitvector proof which is backed by
43  * (a) bitblasting and
44  * (b) a resolution unsat proof.
45  *
46  * Contains tools for constructing BV conflicts
47  */
48 class ResolutionBitVectorProof : public BitVectorProof
49 {
50  public:
51   ResolutionBitVectorProof(theory::bv::TheoryBV* bv,
52                            TheoryProofEngine* proofEngine);
53 
54   /**
55    * Create an (internal) SAT proof object
56    * Must be invoked before manipulating BV conflicts,
57    * or initializing a BNF proof
58    */
59   void initSatProof(CVC4::BVMinisat::Solver* solver);
60 
61   BVSatProof* getSatProof();
62 
63   void finalizeConflicts(std::vector<Expr>& conflicts) override;
64 
65   void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr);
66   void startBVConflict(CVC4::BVMinisat::Solver::TLit lit);
67   void endBVConflict(const BVMinisat::Solver::TLitVec& confl);
68 
markAssumptionConflict()69   void markAssumptionConflict() { d_isAssumptionConflict = true; }
isAssumptionConflict()70   bool isAssumptionConflict() const { return d_isAssumptionConflict; }
71 
72   void initCnfProof(prop::CnfStream* cnfStream,
73                     context::Context* cnf,
74                     prop::SatVariable trueVar,
75                     prop::SatVariable falseVar) override;
76 
77  protected:
78   void attachToSatSolver(prop::SatSolver& sat_solver) override;
79 
80   context::Context d_fakeContext;
81 
82   // The CNF formula that results from bit-blasting will need a proof.
83   // This is that proof.
84   std::unique_ptr<BVSatProof> d_resolutionProof;
85 
86   bool d_isAssumptionConflict;
87 
88 };
89 
90 class LfscResolutionBitVectorProof : public ResolutionBitVectorProof
91 {
92  public:
LfscResolutionBitVectorProof(theory::bv::TheoryBV * bv,TheoryProofEngine * proofEngine)93   LfscResolutionBitVectorProof(theory::bv::TheoryBV* bv,
94                                TheoryProofEngine* proofEngine)
95       : ResolutionBitVectorProof(bv, proofEngine)
96   {
97   }
98   void printTheoryLemmaProof(std::vector<Expr>& lemma,
99                              std::ostream& os,
100                              std::ostream& paren,
101                              const ProofLetMap& map) override;
102   void printBBDeclarationAndCnf(std::ostream& os,
103                                 std::ostream& paren,
104                                 ProofLetMap& letMap) override;
105   void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
106   void calculateAtomsInBitblastingProof() override;
107 };
108 
109 }  // namespace proof
110 
111 }  // namespace CVC4
112 
113 #endif /* __CVC4__PROOF__RESOLUTIONBITVECTORPROOF_H */
114