1 /********************* */
2 /*! \file resolution_bitvector_proof.h
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
12 ** \brief Bitvector proof
17 #include "cvc4_private.h"
19 #ifndef __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H
20 #define __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H
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"
40 // TODO(aozdemir) break the sat_solver - resolution_bitvectorproof - cnf_stream
41 // header cycle and remove this.
46 } /* namespace CVC4 */
51 template <class Solver
>
53 typedef TSatProof
<CVC4::BVMinisat::Solver
> BVSatProof
;
58 * Represents a bitvector proof which is backed by
60 * (b) a resolution unsat proof.
62 * Contains tools for constructing BV conflicts
64 class ResolutionBitVectorProof
: public BitVectorProof
67 ResolutionBitVectorProof(theory::bv::TheoryBV
* bv
,
68 TheoryProofEngine
* proofEngine
);
71 * Create an (internal) SAT proof object
72 * Must be invoked before manipulating BV conflicts,
73 * or initializing a BNF proof
75 void initSatProof(CVC4::BVMinisat::Solver
* solver
);
77 BVSatProof
* getSatProof();
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.
85 void finalizeConflicts(std::vector
<Expr
>& conflicts
);
87 void startBVConflict(CVC4::BVMinisat::Solver::TCRef cr
);
88 void startBVConflict(CVC4::BVMinisat::Solver::TLit lit
);
89 void endBVConflict(const BVMinisat::Solver::TLitVec
& confl
);
91 void markAssumptionConflict() { d_isAssumptionConflict
= true; }
92 bool isAssumptionConflict() const { return d_isAssumptionConflict
; }
94 virtual void printResolutionProof(std::ostream
& os
,
96 ProofLetMap
& letMap
) = 0;
98 void initCnfProof(prop::CnfStream
* cnfStream
, context::Context
* cnf
) override
;
101 context::Context d_fakeContext
;
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
;
107 bool d_isAssumptionConflict
;
109 theory::TheoryId
getTheoryId() override
;
112 class LFSCBitVectorProof
: public ResolutionBitVectorProof
115 LFSCBitVectorProof(theory::bv::TheoryBV
* bv
, TheoryProofEngine
* proofEngine
)
116 : ResolutionBitVectorProof(bv
, proofEngine
)
119 void printTheoryLemmaProof(std::vector
<Expr
>& lemma
,
122 const ProofLetMap
& map
) override
;
123 void printResolutionProof(std::ostream
& os
,
125 ProofLetMap
& letMap
) override
;
126 void calculateAtomsInBitblastingProof() override
;
133 #endif /* __CVC4__PROOF__RESOLUTIONBITVECTORPROOF_H */