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