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
133
134
135
136
137
138
|
/********************* */
/*! \file clausal_bitvector_proof.h
** \verbatim
** Top contributors (to current version):
** Alex Ozdemir, Mathias Preiner
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 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 for clausal (DRAT/LRAT) formats
**
** An internal string stream is hooked up to CryptoMiniSat, which spits out a
** binary DRAT proof. Depending on which kind of proof we're going to turn
** that into, we process it in different ways.
**/
#include "cvc4_private.h"
#ifndef __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
#define __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
#include <iostream>
#include <sstream>
#include <unordered_map>
#include "expr/expr.h"
#include "proof/bitvector_proof.h"
#include "proof/drat/drat_proof.h"
#include "proof/lrat/lrat_proof.h"
#include "proof/theory_proof.h"
#include "prop/cnf_stream.h"
#include "prop/sat_solver_types.h"
#include "theory/bv/theory_bv.h"
namespace CVC4 {
namespace proof {
class ClausalBitVectorProof : public BitVectorProof
{
public:
ClausalBitVectorProof(theory::bv::TheoryBV* bv,
TheoryProofEngine* proofEngine);
~ClausalBitVectorProof() = default;
void attachToSatSolver(prop::SatSolver& sat_solver) override;
void initCnfProof(prop::CnfStream* cnfStream,
context::Context* cnf,
prop::SatVariable trueVar,
prop::SatVariable falseVar) override;
std::ostream& getDratOstream() { return d_binaryDratProof; }
void registerUsedClause(ClauseId id, prop::SatClause& clause);
void calculateAtomsInBitblastingProof() override;
protected:
// A list of all clauses and their ids which are passed into the SAT solver
std::vector<std::pair<ClauseId, prop::SatClause>> d_usedClauses;
// Stores the proof recieved from the SAT solver.
std::ostringstream d_binaryDratProof;
};
/**
* A representation of a clausal proof of a bitvector problem's UNSAT nature
*/
class LfscClausalBitVectorProof : public ClausalBitVectorProof
{
public:
LfscClausalBitVectorProof(theory::bv::TheoryBV* bv,
TheoryProofEngine* proofEngine)
: ClausalBitVectorProof(bv, proofEngine)
{
}
void printTheoryLemmaProof(std::vector<Expr>& lemma,
std::ostream& os,
std::ostream& paren,
const ProofLetMap& map) override;
void printBBDeclarationAndCnf(std::ostream& os,
std::ostream& paren,
ProofLetMap& letMap) override;
};
/**
* A DRAT proof for a bit-vector problem
*/
class LfscDratBitVectorProof : public LfscClausalBitVectorProof
{
public:
LfscDratBitVectorProof(theory::bv::TheoryBV* bv,
TheoryProofEngine* proofEngine)
: LfscClausalBitVectorProof(bv, proofEngine)
{
}
void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
};
/**
* An LRAT proof for a bit-vector problem
*/
class LfscLratBitVectorProof : public LfscClausalBitVectorProof
{
public:
LfscLratBitVectorProof(theory::bv::TheoryBV* bv,
TheoryProofEngine* proofEngine)
: LfscClausalBitVectorProof(bv, proofEngine)
{
}
void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
};
/**
* An Extended Resolution proof for a bit-vector problem
*/
class LfscErBitVectorProof : public LfscClausalBitVectorProof
{
public:
LfscErBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
: LfscClausalBitVectorProof(bv, proofEngine)
{
}
void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
};
} // namespace proof
} // namespace CVC4
#endif /* __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H */
|
