1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Aina Niemetz, Mathias Preiner |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* A bit-blaster wrapper around BBSimple for proof logging. |
14 |
|
*/ |
15 |
|
#include "theory/bv/bitblast/proof_bitblaster.h" |
16 |
|
|
17 |
|
#include <unordered_set> |
18 |
|
|
19 |
|
#include "expr/term_conversion_proof_generator.h" |
20 |
|
#include "options/proof_options.h" |
21 |
|
#include "theory/theory_model.h" |
22 |
|
|
23 |
|
namespace cvc5 { |
24 |
|
namespace theory { |
25 |
|
namespace bv { |
26 |
|
|
27 |
|
std::unordered_map<Kind, PfRule, kind::KindHashFunction> |
28 |
9397 |
BBProof::s_kindToPfRule = { |
29 |
|
{kind::CONST_BITVECTOR, PfRule::BV_BITBLAST_CONST}, |
30 |
|
{kind::EQUAL, PfRule::BV_BITBLAST_EQUAL}, |
31 |
|
{kind::BITVECTOR_ULT, PfRule::BV_BITBLAST_ULT}, |
32 |
|
{kind::BITVECTOR_ULE, PfRule::BV_BITBLAST_ULE}, |
33 |
|
{kind::BITVECTOR_UGT, PfRule::BV_BITBLAST_UGT}, |
34 |
|
{kind::BITVECTOR_UGE, PfRule::BV_BITBLAST_UGE}, |
35 |
|
{kind::BITVECTOR_SLT, PfRule::BV_BITBLAST_SLT}, |
36 |
|
{kind::BITVECTOR_SLE, PfRule::BV_BITBLAST_SLE}, |
37 |
|
{kind::BITVECTOR_SGT, PfRule::BV_BITBLAST_SGT}, |
38 |
|
{kind::BITVECTOR_SGE, PfRule::BV_BITBLAST_SGE}, |
39 |
|
{kind::BITVECTOR_NOT, PfRule::BV_BITBLAST_NOT}, |
40 |
|
{kind::BITVECTOR_CONCAT, PfRule::BV_BITBLAST_CONCAT}, |
41 |
|
{kind::BITVECTOR_AND, PfRule::BV_BITBLAST_AND}, |
42 |
|
{kind::BITVECTOR_OR, PfRule::BV_BITBLAST_OR}, |
43 |
|
{kind::BITVECTOR_XOR, PfRule::BV_BITBLAST_XOR}, |
44 |
|
{kind::BITVECTOR_XNOR, PfRule::BV_BITBLAST_XNOR}, |
45 |
|
{kind::BITVECTOR_NAND, PfRule::BV_BITBLAST_NAND}, |
46 |
|
{kind::BITVECTOR_NOR, PfRule::BV_BITBLAST_NOR}, |
47 |
|
{kind::BITVECTOR_COMP, PfRule::BV_BITBLAST_COMP}, |
48 |
|
{kind::BITVECTOR_MULT, PfRule::BV_BITBLAST_MULT}, |
49 |
|
{kind::BITVECTOR_ADD, PfRule::BV_BITBLAST_ADD}, |
50 |
|
{kind::BITVECTOR_SUB, PfRule::BV_BITBLAST_SUB}, |
51 |
|
{kind::BITVECTOR_NEG, PfRule::BV_BITBLAST_NEG}, |
52 |
|
{kind::BITVECTOR_UDIV, PfRule::BV_BITBLAST_UDIV}, |
53 |
|
{kind::BITVECTOR_UREM, PfRule::BV_BITBLAST_UREM}, |
54 |
|
{kind::BITVECTOR_SDIV, PfRule::BV_BITBLAST_SDIV}, |
55 |
|
{kind::BITVECTOR_SREM, PfRule::BV_BITBLAST_SREM}, |
56 |
|
{kind::BITVECTOR_SMOD, PfRule::BV_BITBLAST_SMOD}, |
57 |
|
{kind::BITVECTOR_SHL, PfRule::BV_BITBLAST_SHL}, |
58 |
|
{kind::BITVECTOR_LSHR, PfRule::BV_BITBLAST_LSHR}, |
59 |
|
{kind::BITVECTOR_ASHR, PfRule::BV_BITBLAST_ASHR}, |
60 |
|
{kind::BITVECTOR_ULTBV, PfRule::BV_BITBLAST_ULTBV}, |
61 |
|
{kind::BITVECTOR_SLTBV, PfRule::BV_BITBLAST_SLTBV}, |
62 |
|
{kind::BITVECTOR_ITE, PfRule::BV_BITBLAST_ITE}, |
63 |
|
{kind::BITVECTOR_EXTRACT, PfRule::BV_BITBLAST_EXTRACT}, |
64 |
|
{kind::BITVECTOR_REPEAT, PfRule::BV_BITBLAST_REPEAT}, |
65 |
|
{kind::BITVECTOR_ZERO_EXTEND, PfRule::BV_BITBLAST_ZERO_EXTEND}, |
66 |
|
{kind::BITVECTOR_SIGN_EXTEND, PfRule::BV_BITBLAST_SIGN_EXTEND}, |
67 |
|
{kind::BITVECTOR_ROTATE_RIGHT, PfRule::BV_BITBLAST_ROTATE_RIGHT}, |
68 |
|
{kind::BITVECTOR_ROTATE_LEFT, PfRule::BV_BITBLAST_ROTATE_LEFT}, |
69 |
|
}; |
70 |
|
|
71 |
15 |
BBProof::BBProof(TheoryState* state, |
72 |
|
ProofNodeManager* pnm, |
73 |
15 |
TConvProofGenerator* tcpg) |
74 |
15 |
: d_bb(new BBSimple(state)), d_pnm(pnm), d_tcpg(tcpg) |
75 |
|
{ |
76 |
15 |
} |
77 |
|
|
78 |
15 |
BBProof::~BBProof() {} |
79 |
|
|
80 |
68 |
void BBProof::bbAtom(TNode node) |
81 |
|
{ |
82 |
136 |
std::vector<TNode> visit; |
83 |
68 |
visit.push_back(node); |
84 |
136 |
std::unordered_set<TNode> visited; |
85 |
|
|
86 |
|
bool fproofs = |
87 |
68 |
options::proofGranularityMode() != options::ProofGranularityMode::OFF; |
88 |
68 |
bool fpenabled = isProofsEnabled() && fproofs; |
89 |
|
|
90 |
68 |
NodeManager* nm = NodeManager::currentNM(); |
91 |
|
|
92 |
900 |
while (!visit.empty()) |
93 |
|
{ |
94 |
728 |
TNode n = visit.back(); |
95 |
520 |
if (hasBBAtom(n) || hasBBTerm(n)) |
96 |
|
{ |
97 |
104 |
visit.pop_back(); |
98 |
104 |
continue; |
99 |
|
} |
100 |
|
|
101 |
312 |
if (visited.find(n) == visited.end()) |
102 |
|
{ |
103 |
156 |
visited.insert(n); |
104 |
156 |
if (!Theory::isLeafOf(n, theory::THEORY_BV)) |
105 |
|
{ |
106 |
96 |
visit.insert(visit.end(), n.begin(), n.end()); |
107 |
|
} |
108 |
|
} |
109 |
|
else |
110 |
|
{ |
111 |
156 |
if (Theory::isLeafOf(n, theory::THEORY_BV) && !n.isConst()) |
112 |
|
{ |
113 |
64 |
Bits bits; |
114 |
32 |
d_bb->makeVariable(n, bits); |
115 |
32 |
if (fpenabled) |
116 |
|
{ |
117 |
|
Node n_tobv = nm->mkNode(kind::BITVECTOR_BB_TERM, bits); |
118 |
|
d_bbMap.emplace(n, n_tobv); |
119 |
|
d_tcpg->addRewriteStep(n, |
120 |
|
n_tobv, |
121 |
|
PfRule::BV_BITBLAST_VAR, |
122 |
|
{}, |
123 |
|
{n.eqNode(n_tobv)}, |
124 |
|
false); |
125 |
|
} |
126 |
|
} |
127 |
124 |
else if (n.getType().isBitVector()) |
128 |
|
{ |
129 |
112 |
Bits bits; |
130 |
56 |
d_bb->bbTerm(n, bits); |
131 |
56 |
Kind kind = n.getKind(); |
132 |
56 |
if (fpenabled) |
133 |
|
{ |
134 |
|
Node n_tobv = nm->mkNode(kind::BITVECTOR_BB_TERM, bits); |
135 |
|
d_bbMap.emplace(n, n_tobv); |
136 |
|
Node c_tobv; |
137 |
|
if (n.isConst()) |
138 |
|
{ |
139 |
|
c_tobv = n; |
140 |
|
} |
141 |
|
else |
142 |
|
{ |
143 |
|
std::vector<Node> children_tobv; |
144 |
|
if (n.getMetaKind() == kind::metakind::PARAMETERIZED) |
145 |
|
{ |
146 |
|
children_tobv.push_back(n.getOperator()); |
147 |
|
} |
148 |
|
|
149 |
|
for (const auto& child : n) |
150 |
|
{ |
151 |
|
children_tobv.push_back(d_bbMap.at(child)); |
152 |
|
} |
153 |
|
c_tobv = nm->mkNode(kind, children_tobv); |
154 |
|
} |
155 |
|
d_tcpg->addRewriteStep(c_tobv, |
156 |
|
n_tobv, |
157 |
|
s_kindToPfRule.at(kind), |
158 |
|
{}, |
159 |
|
{c_tobv.eqNode(n_tobv)}, |
160 |
|
false); |
161 |
|
} |
162 |
|
} |
163 |
|
else |
164 |
|
{ |
165 |
68 |
d_bb->bbAtom(n); |
166 |
68 |
if (fpenabled) |
167 |
|
{ |
168 |
|
Node n_tobv = getStoredBBAtom(n); |
169 |
|
std::vector<Node> children_tobv; |
170 |
|
for (const auto& child : n) |
171 |
|
{ |
172 |
|
children_tobv.push_back(d_bbMap.at(child)); |
173 |
|
} |
174 |
|
Node c_tobv = nm->mkNode(n.getKind(), children_tobv); |
175 |
|
d_tcpg->addRewriteStep(c_tobv, |
176 |
|
n_tobv, |
177 |
|
s_kindToPfRule.at(n.getKind()), |
178 |
|
{}, |
179 |
|
{c_tobv.eqNode(n_tobv)}, |
180 |
|
false); |
181 |
|
} |
182 |
|
} |
183 |
156 |
visit.pop_back(); |
184 |
|
} |
185 |
|
} |
186 |
68 |
if (isProofsEnabled() && !fproofs) |
187 |
|
{ |
188 |
|
Node node_tobv = getStoredBBAtom(node); |
189 |
|
d_tcpg->addRewriteStep(node, |
190 |
|
node_tobv, |
191 |
|
PfRule::BV_BITBLAST, |
192 |
|
{}, |
193 |
|
{node.eqNode(node_tobv)}, |
194 |
|
false); |
195 |
|
} |
196 |
68 |
} |
197 |
|
|
198 |
532 |
bool BBProof::hasBBAtom(TNode atom) const { return d_bb->hasBBAtom(atom); } |
199 |
|
|
200 |
416 |
bool BBProof::hasBBTerm(TNode atom) const { return d_bb->hasBBTerm(atom); } |
201 |
|
|
202 |
116 |
Node BBProof::getStoredBBAtom(TNode node) |
203 |
|
{ |
204 |
116 |
return d_bb->getStoredBBAtom(node); |
205 |
|
} |
206 |
|
|
207 |
7 |
bool BBProof::collectModelValues(TheoryModel* m, |
208 |
|
const std::set<Node>& relevantTerms) |
209 |
|
{ |
210 |
7 |
return d_bb->collectModelValues(m, relevantTerms); |
211 |
|
} |
212 |
|
|
213 |
136 |
bool BBProof::isProofsEnabled() const { return d_pnm != nullptr; } |
214 |
|
|
215 |
|
} // namespace bv |
216 |
|
} // namespace theory |
217 |
28191 |
} // namespace cvc5 |