1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Liana Hadarean, 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 |
|
* [[ Add lengthier description here ]] |
14 |
|
* \todo document this file |
15 |
|
*/ |
16 |
|
#include "theory/bv/abstraction.h" |
17 |
|
|
18 |
|
#include "expr/skolem_manager.h" |
19 |
|
#include "options/bv_options.h" |
20 |
|
#include "printer/printer.h" |
21 |
|
#include "smt/dump.h" |
22 |
|
#include "smt/smt_engine.h" |
23 |
|
#include "smt/smt_engine_scope.h" |
24 |
|
#include "smt/smt_statistics_registry.h" |
25 |
|
#include "theory/bv/theory_bv_utils.h" |
26 |
|
#include "theory/rewriter.h" |
27 |
|
#include "util/bitvector.h" |
28 |
|
|
29 |
|
using namespace cvc5; |
30 |
|
using namespace cvc5::theory; |
31 |
|
using namespace cvc5::theory::bv; |
32 |
|
using namespace cvc5::context; |
33 |
|
|
34 |
|
using namespace std; |
35 |
|
using namespace cvc5::theory::bv::utils; |
36 |
|
|
37 |
|
bool AbstractionModule::applyAbstraction(const std::vector<Node>& assertions, |
38 |
|
std::vector<Node>& new_assertions) |
39 |
|
{ |
40 |
|
Debug("bv-abstraction") << "AbstractionModule::applyAbstraction\n"; |
41 |
|
|
42 |
|
TimerStat::CodeTimer abstractionTimer(d_statistics.d_abstractionTime); |
43 |
|
|
44 |
|
TNodeSet seen; |
45 |
|
for (unsigned i = 0; i < assertions.size(); ++i) |
46 |
|
{ |
47 |
|
if (assertions[i].getKind() == kind::OR) |
48 |
|
{ |
49 |
|
for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j) |
50 |
|
{ |
51 |
|
if (!isConjunctionOfAtoms(assertions[i][j], seen)) |
52 |
|
{ |
53 |
|
continue; |
54 |
|
} |
55 |
|
Node signature = computeSignature(assertions[i][j]); |
56 |
|
storeSignature(signature, assertions[i][j]); |
57 |
|
Debug("bv-abstraction") << " assertion: " << assertions[i][j] << "\n"; |
58 |
|
Debug("bv-abstraction") << " signature: " << signature << "\n"; |
59 |
|
} |
60 |
|
} |
61 |
|
} |
62 |
|
finalizeSignatures(); |
63 |
|
|
64 |
|
for (unsigned i = 0; i < assertions.size(); ++i) |
65 |
|
{ |
66 |
|
if (assertions[i].getKind() == kind::OR |
67 |
|
&& assertions[i][0].getKind() == kind::AND) |
68 |
|
{ |
69 |
|
std::vector<Node> new_children; |
70 |
|
for (unsigned j = 0; j < assertions[i].getNumChildren(); ++j) |
71 |
|
{ |
72 |
|
if (hasSignature(assertions[i][j])) |
73 |
|
{ |
74 |
|
new_children.push_back(abstractSignatures(assertions[i][j])); |
75 |
|
} |
76 |
|
else |
77 |
|
{ |
78 |
|
new_children.push_back(assertions[i][j]); |
79 |
|
} |
80 |
|
} |
81 |
|
new_assertions.push_back(utils::mkOr(new_children)); |
82 |
|
} |
83 |
|
else |
84 |
|
{ |
85 |
|
// assertions that are not changed |
86 |
|
new_assertions.push_back(assertions[i]); |
87 |
|
} |
88 |
|
} |
89 |
|
|
90 |
|
if (options::skolemizeArguments()) |
91 |
|
{ |
92 |
|
skolemizeArguments(new_assertions); |
93 |
|
} |
94 |
|
|
95 |
|
// if we are using the eager solver reverse the abstraction |
96 |
|
if (options::bitblastMode() == options::BitblastMode::EAGER) |
97 |
|
{ |
98 |
|
if (d_funcToSignature.size() == 0) |
99 |
|
{ |
100 |
|
// we did not change anything |
101 |
|
return false; |
102 |
|
} |
103 |
|
NodeNodeMap seen_rev; |
104 |
|
for (unsigned i = 0; i < new_assertions.size(); ++i) |
105 |
|
{ |
106 |
|
new_assertions[i] = reverseAbstraction(new_assertions[i], seen_rev); |
107 |
|
} |
108 |
|
// we undo the abstraction functions so the logic is QF_BV still |
109 |
|
return true; |
110 |
|
} |
111 |
|
|
112 |
|
// return true if we have created new function symbols for the problem |
113 |
|
return d_funcToSignature.size() != 0; |
114 |
|
} |
115 |
|
|
116 |
|
bool AbstractionModule::isConjunctionOfAtoms(TNode node, TNodeSet& seen) |
117 |
|
{ |
118 |
|
if (seen.find(node)!= seen.end()) |
119 |
|
return true; |
120 |
|
|
121 |
|
if (!node.getType().isBitVector() && node.getKind() != kind::AND) |
122 |
|
{ |
123 |
|
return utils::isBVPredicate(node); |
124 |
|
} |
125 |
|
|
126 |
|
if (node.getNumChildren() == 0) |
127 |
|
return true; |
128 |
|
|
129 |
|
for (unsigned i = 0; i < node.getNumChildren(); ++i) { |
130 |
|
if (!isConjunctionOfAtoms(node[i], seen)) |
131 |
|
{ |
132 |
|
return false; |
133 |
|
} |
134 |
|
} |
135 |
|
seen.insert(node); |
136 |
|
return true; |
137 |
|
} |
138 |
|
|
139 |
|
|
140 |
|
Node AbstractionModule::reverseAbstraction(Node assertion, NodeNodeMap& seen) { |
141 |
|
|
142 |
|
if (seen.find(assertion) != seen.end()) |
143 |
|
return seen[assertion]; |
144 |
|
|
145 |
|
if (isAbstraction(assertion)) { |
146 |
|
Node interp = getInterpretation(assertion); |
147 |
|
seen[assertion] = interp; |
148 |
|
Assert(interp.getType() == assertion.getType()); |
149 |
|
return interp; |
150 |
|
} |
151 |
|
|
152 |
|
if (assertion.getNumChildren() == 0) { |
153 |
|
seen[assertion] = assertion; |
154 |
|
return assertion; |
155 |
|
} |
156 |
|
|
157 |
|
NodeBuilder result(assertion.getKind()); |
158 |
|
if (assertion.getMetaKind() == kind::metakind::PARAMETERIZED) { |
159 |
|
result << assertion.getOperator(); |
160 |
|
} |
161 |
|
|
162 |
|
for (unsigned i = 0; i < assertion.getNumChildren(); ++i) { |
163 |
|
result << reverseAbstraction(assertion[i], seen); |
164 |
|
} |
165 |
|
Node res = result; |
166 |
|
seen[assertion] = res; |
167 |
|
return res; |
168 |
|
} |
169 |
|
|
170 |
|
void AbstractionModule::skolemizeArguments(std::vector<Node>& assertions) |
171 |
|
{ |
172 |
|
NodeManager* nm = NodeManager::currentNM(); |
173 |
|
for (unsigned i = 0; i < assertions.size(); ++i) |
174 |
|
{ |
175 |
|
TNode assertion = assertions[i]; |
176 |
|
if (assertion.getKind() != kind::OR) continue; |
177 |
|
|
178 |
|
bool is_skolemizable = true; |
179 |
|
for (unsigned k = 0; k < assertion.getNumChildren(); ++k) |
180 |
|
{ |
181 |
|
if (assertion[k].getKind() != kind::EQUAL |
182 |
|
|| assertion[k][0].getKind() != kind::APPLY_UF |
183 |
|
|| assertion[k][1].getKind() != kind::CONST_BITVECTOR |
184 |
|
|| assertion[k][1].getConst<BitVector>() != BitVector(1, 1u)) |
185 |
|
{ |
186 |
|
is_skolemizable = false; |
187 |
|
break; |
188 |
|
} |
189 |
|
} |
190 |
|
|
191 |
|
if (!is_skolemizable) continue; |
192 |
|
|
193 |
|
ArgsTable assertion_table; |
194 |
|
|
195 |
|
// collect function symbols and their arguments |
196 |
|
for (unsigned j = 0; j < assertion.getNumChildren(); ++j) |
197 |
|
{ |
198 |
|
TNode current = assertion[j]; |
199 |
|
Assert(current.getKind() == kind::EQUAL |
200 |
|
&& current[0].getKind() == kind::APPLY_UF); |
201 |
|
TNode func = current[0]; |
202 |
|
ArgsVec args; |
203 |
|
for (unsigned k = 0; k < func.getNumChildren(); ++k) |
204 |
|
{ |
205 |
|
args.push_back(func[k]); |
206 |
|
} |
207 |
|
assertion_table.addEntry(func.getOperator(), args); |
208 |
|
} |
209 |
|
|
210 |
|
NodeBuilder assertion_builder(kind::OR); |
211 |
|
// construct skolemized assertion |
212 |
|
for (ArgsTable::iterator it = assertion_table.begin(); |
213 |
|
it != assertion_table.end(); |
214 |
|
++it) |
215 |
|
{ |
216 |
|
// for each function symbol |
217 |
|
++(d_statistics.d_numArgsSkolemized); |
218 |
|
TNode func = it->first; |
219 |
|
ArgsTableEntry& args = it->second; |
220 |
|
NodeBuilder skolem_func(kind::APPLY_UF); |
221 |
|
skolem_func << func; |
222 |
|
std::vector<Node> skolem_args; |
223 |
|
|
224 |
|
for (unsigned j = 0; j < args.getArity(); ++j) |
225 |
|
{ |
226 |
|
bool all_same = true; |
227 |
|
for (unsigned k = 1; k < args.getNumEntries(); ++k) |
228 |
|
{ |
229 |
|
if (args.getEntry(k)[j] != args.getEntry(0)[j]) all_same = false; |
230 |
|
} |
231 |
|
Node new_arg = all_same |
232 |
|
? (Node)args.getEntry(0)[j] |
233 |
|
: utils::mkVar(utils::getSize(args.getEntry(0)[j])); |
234 |
|
skolem_args.push_back(new_arg); |
235 |
|
skolem_func << new_arg; |
236 |
|
} |
237 |
|
|
238 |
|
Node skolem_func_eq1 = |
239 |
|
nm->mkNode(kind::EQUAL, (Node)skolem_func, utils::mkConst(1, 1u)); |
240 |
|
|
241 |
|
// enumerate arguments assignments |
242 |
|
std::vector<Node> or_assignments; |
243 |
|
for (const ArgsVec& av : args) |
244 |
|
// for (ArgsTableEntry::iterator it = args.begin(); it != args.end(); |
245 |
|
// ++it) |
246 |
|
{ |
247 |
|
NodeBuilder arg_assignment(kind::AND); |
248 |
|
// ArgsVec& args = *it; |
249 |
|
for (unsigned k = 0; k < av.size(); ++k) |
250 |
|
{ |
251 |
|
Node eq = nm->mkNode(kind::EQUAL, av[k], skolem_args[k]); |
252 |
|
arg_assignment << eq; |
253 |
|
} |
254 |
|
or_assignments.push_back(arg_assignment); |
255 |
|
} |
256 |
|
|
257 |
|
Node new_func_def = |
258 |
|
utils::mkAnd(skolem_func_eq1, utils::mkOr(or_assignments)); |
259 |
|
assertion_builder << new_func_def; |
260 |
|
} |
261 |
|
Node new_assertion = assertion_builder; |
262 |
|
Debug("bv-abstraction-dbg") << "AbstractionModule::skolemizeArguments " |
263 |
|
<< assertions[i] << " => \n"; |
264 |
|
Debug("bv-abstraction-dbg") << " " << new_assertion; |
265 |
|
assertions[i] = new_assertion; |
266 |
|
} |
267 |
|
} |
268 |
|
|
269 |
|
void AbstractionModule::storeSignature(Node signature, TNode assertion) { |
270 |
|
if(d_signatures.find(signature) == d_signatures.end()) { |
271 |
|
d_signatures[signature] = 0; |
272 |
|
} |
273 |
|
d_signatures[signature] = d_signatures[signature] + 1; |
274 |
|
d_assertionToSignature[assertion] = signature; |
275 |
|
} |
276 |
|
|
277 |
|
Node AbstractionModule::computeSignature(TNode node) { |
278 |
|
resetSignatureIndex(); |
279 |
|
NodeNodeMap cache; |
280 |
|
Node sig = computeSignatureRec(node, cache); |
281 |
|
return sig; |
282 |
|
} |
283 |
|
|
284 |
|
Node AbstractionModule::getSignatureSkolem(TNode node) |
285 |
|
{ |
286 |
|
Assert(node.getMetaKind() == kind::metakind::VARIABLE); |
287 |
|
NodeManager* nm = NodeManager::currentNM(); |
288 |
|
SkolemManager* sm = nm->getSkolemManager(); |
289 |
|
unsigned bitwidth = utils::getSize(node); |
290 |
|
if (d_signatureSkolems.find(bitwidth) == d_signatureSkolems.end()) |
291 |
|
{ |
292 |
|
d_signatureSkolems[bitwidth] = vector<Node>(); |
293 |
|
} |
294 |
|
|
295 |
|
vector<Node>& skolems = d_signatureSkolems[bitwidth]; |
296 |
|
// get the index of bv variables of this size |
297 |
|
unsigned index = getBitwidthIndex(bitwidth); |
298 |
|
Assert(skolems.size() + 1 >= index); |
299 |
|
if (skolems.size() == index) |
300 |
|
{ |
301 |
|
ostringstream os; |
302 |
|
os << "sig_" << bitwidth << "_" << index; |
303 |
|
skolems.push_back(sm->mkDummySkolem(os.str(), |
304 |
|
nm->mkBitVectorType(bitwidth), |
305 |
|
"skolem for computing signatures")); |
306 |
|
} |
307 |
|
++(d_signatureIndices[bitwidth]); |
308 |
|
return skolems[index]; |
309 |
|
} |
310 |
|
|
311 |
|
unsigned AbstractionModule::getBitwidthIndex(unsigned bitwidth) { |
312 |
|
if (d_signatureIndices.find(bitwidth) == d_signatureIndices.end()) { |
313 |
|
d_signatureIndices[bitwidth] = 0; |
314 |
|
} |
315 |
|
return d_signatureIndices[bitwidth]; |
316 |
|
} |
317 |
|
|
318 |
|
void AbstractionModule::resetSignatureIndex() { |
319 |
|
for (IndexMap::iterator it = d_signatureIndices.begin(); it != d_signatureIndices.end(); ++it) { |
320 |
|
it->second = 0; |
321 |
|
} |
322 |
|
} |
323 |
|
|
324 |
|
bool AbstractionModule::hasSignature(Node node) { |
325 |
|
return d_assertionToSignature.find(node) != d_assertionToSignature.end(); |
326 |
|
} |
327 |
|
|
328 |
|
Node AbstractionModule::getGeneralizedSignature(Node node) { |
329 |
|
NodeNodeMap::const_iterator it = d_assertionToSignature.find(node); |
330 |
|
Assert(it != d_assertionToSignature.end()); |
331 |
|
Node generalized_signature = getGeneralization(it->second); |
332 |
|
return generalized_signature; |
333 |
|
} |
334 |
|
|
335 |
|
Node AbstractionModule::computeSignatureRec(TNode node, NodeNodeMap& cache) { |
336 |
|
if (cache.find(node) != cache.end()) { |
337 |
|
return cache.find(node)->second; |
338 |
|
} |
339 |
|
|
340 |
|
if (node.getNumChildren() == 0) { |
341 |
|
if (node.getKind() == kind::CONST_BITVECTOR) |
342 |
|
return node; |
343 |
|
|
344 |
|
Node sig = getSignatureSkolem(node); |
345 |
|
cache[node] = sig; |
346 |
|
return sig; |
347 |
|
} |
348 |
|
|
349 |
|
NodeBuilder builder(node.getKind()); |
350 |
|
if (node.getMetaKind() == kind::metakind::PARAMETERIZED) { |
351 |
|
builder << node.getOperator(); |
352 |
|
} |
353 |
|
for (unsigned i = 0; i < node.getNumChildren(); ++i) { |
354 |
|
Node converted = computeSignatureRec(node[i], cache); |
355 |
|
builder << converted; |
356 |
|
} |
357 |
|
Node result = builder; |
358 |
|
cache[node] = result; |
359 |
|
return result; |
360 |
|
} |
361 |
|
|
362 |
|
/** |
363 |
|
* Returns 0, if the two are equal, |
364 |
|
* 1 if s is a generalization of t |
365 |
|
* 2 if t is a generalization of s |
366 |
|
* -1 if the two cannot be unified |
367 |
|
* |
368 |
|
* @param s |
369 |
|
* @param t |
370 |
|
* |
371 |
|
* @return |
372 |
|
*/ |
373 |
|
int AbstractionModule::comparePatterns(TNode s, TNode t) { |
374 |
|
if (s.getKind() == kind::SKOLEM && |
375 |
|
t.getKind() == kind::SKOLEM) { |
376 |
|
return 0; |
377 |
|
} |
378 |
|
|
379 |
|
if (s.getKind() == kind::CONST_BITVECTOR && |
380 |
|
t.getKind() == kind::CONST_BITVECTOR) { |
381 |
|
if (s == t) { |
382 |
|
return 0; |
383 |
|
} else { |
384 |
|
return -1; |
385 |
|
} |
386 |
|
} |
387 |
|
|
388 |
|
if (s.getKind() == kind::SKOLEM && |
389 |
|
t.getKind() == kind::CONST_BITVECTOR) { |
390 |
|
return 1; |
391 |
|
} |
392 |
|
|
393 |
|
if (s.getKind() == kind::CONST_BITVECTOR && |
394 |
|
t.getKind() == kind::SKOLEM) { |
395 |
|
return 2; |
396 |
|
} |
397 |
|
|
398 |
|
if (s.getNumChildren() != t.getNumChildren() || |
399 |
|
s.getKind() != t.getKind()) |
400 |
|
return -1; |
401 |
|
|
402 |
|
int unify = 0; |
403 |
|
for (unsigned i = 0; i < s.getNumChildren(); ++i) { |
404 |
|
int unify_i = comparePatterns(s[i], t[i]); |
405 |
|
if (unify_i < 0) |
406 |
|
return -1; |
407 |
|
if (unify == 0) { |
408 |
|
unify = unify_i; |
409 |
|
} else if (unify != unify_i && unify_i != 0) { |
410 |
|
return -1; |
411 |
|
} |
412 |
|
} |
413 |
|
return unify; |
414 |
|
} |
415 |
|
|
416 |
|
TNode AbstractionModule::getGeneralization(TNode term) { |
417 |
|
NodeNodeMap::iterator it = d_sigToGeneralization.find(term); |
418 |
|
// if not in the map we add it |
419 |
|
if (it == d_sigToGeneralization.end()) { |
420 |
|
d_sigToGeneralization[term] = term; |
421 |
|
return term; |
422 |
|
} |
423 |
|
// doesn't have a generalization |
424 |
|
if (it->second == term) |
425 |
|
return term; |
426 |
|
|
427 |
|
TNode generalization = getGeneralization(it->second); |
428 |
|
Assert(generalization != term); |
429 |
|
d_sigToGeneralization[term] = generalization; |
430 |
|
return generalization; |
431 |
|
} |
432 |
|
|
433 |
|
void AbstractionModule::storeGeneralization(TNode s, TNode t) { |
434 |
|
Assert(s == getGeneralization(s)); |
435 |
|
Assert(t == getGeneralization(t)); |
436 |
|
d_sigToGeneralization[s] = t; |
437 |
|
} |
438 |
|
|
439 |
|
void AbstractionModule::finalizeSignatures() |
440 |
|
{ |
441 |
|
NodeManager* nm = NodeManager::currentNM(); |
442 |
|
SkolemManager* sm = nm->getSkolemManager(); |
443 |
|
Debug("bv-abstraction") |
444 |
|
<< "AbstractionModule::finalizeSignatures num signatures = " |
445 |
|
<< d_signatures.size() << "\n"; |
446 |
|
TNodeSet new_signatures; |
447 |
|
|
448 |
|
// "unify" signatures |
449 |
|
for (SignatureMap::const_iterator ss = d_signatures.begin(); |
450 |
|
ss != d_signatures.end(); |
451 |
|
++ss) |
452 |
|
{ |
453 |
|
for (SignatureMap::const_iterator tt = ss; tt != d_signatures.end(); ++tt) |
454 |
|
{ |
455 |
|
TNode t = getGeneralization(tt->first); |
456 |
|
TNode s = getGeneralization(ss->first); |
457 |
|
|
458 |
|
if (t != s) |
459 |
|
{ |
460 |
|
int status = comparePatterns(s, t); |
461 |
|
Assert(status); |
462 |
|
if (status < 0) continue; |
463 |
|
if (status == 1) |
464 |
|
{ |
465 |
|
storeGeneralization(t, s); |
466 |
|
} |
467 |
|
else |
468 |
|
{ |
469 |
|
storeGeneralization(s, t); |
470 |
|
} |
471 |
|
} |
472 |
|
} |
473 |
|
} |
474 |
|
// keep only most general signatures |
475 |
|
for (SignatureMap::iterator it = d_signatures.begin(); |
476 |
|
it != d_signatures.end();) |
477 |
|
{ |
478 |
|
TNode sig = it->first; |
479 |
|
TNode gen = getGeneralization(sig); |
480 |
|
if (sig != gen) |
481 |
|
{ |
482 |
|
Assert(d_signatures.find(gen) != d_signatures.end()); |
483 |
|
// update the count |
484 |
|
d_signatures[gen] += d_signatures[sig]; |
485 |
|
d_signatures.erase(it++); |
486 |
|
} |
487 |
|
else |
488 |
|
{ |
489 |
|
++it; |
490 |
|
} |
491 |
|
} |
492 |
|
|
493 |
|
// remove signatures that are not frequent enough |
494 |
|
for (SignatureMap::iterator it = d_signatures.begin(); |
495 |
|
it != d_signatures.end();) |
496 |
|
{ |
497 |
|
if (it->second <= 7) |
498 |
|
{ |
499 |
|
d_signatures.erase(it++); |
500 |
|
} |
501 |
|
else |
502 |
|
{ |
503 |
|
++it; |
504 |
|
} |
505 |
|
} |
506 |
|
|
507 |
|
for (SignatureMap::const_iterator it = d_signatures.begin(); |
508 |
|
it != d_signatures.end(); |
509 |
|
++it) |
510 |
|
{ |
511 |
|
TNode signature = it->first; |
512 |
|
// we already processed this signature |
513 |
|
Assert(d_signatureToFunc.find(signature) == d_signatureToFunc.end()); |
514 |
|
|
515 |
|
Debug("bv-abstraction") << "Processing signature " << signature << " count " |
516 |
|
<< it->second << "\n"; |
517 |
|
std::vector<TypeNode> arg_types; |
518 |
|
TNodeSet seen; |
519 |
|
collectArgumentTypes(signature, arg_types, seen); |
520 |
|
Assert(signature.getType().isBoolean()); |
521 |
|
// make function return a bitvector of size 1 |
522 |
|
// Node bv_function = nm->mkNode(kind::ITE, signature, utils::mkConst(1, |
523 |
|
// 1u), utils::mkConst(1, 0u)); |
524 |
|
TypeNode range = nm->mkBitVectorType(1); |
525 |
|
|
526 |
|
TypeNode abs_type = nm->mkFunctionType(arg_types, range); |
527 |
|
Node abs_func = sm->mkDummySkolem( |
528 |
|
"abs_$$", abs_type, "abstraction function for bv theory"); |
529 |
|
Debug("bv-abstraction") << " abstracted by function " << abs_func << "\n"; |
530 |
|
|
531 |
|
// NOTE: signature expression type is BOOLEAN |
532 |
|
d_signatureToFunc[signature] = abs_func; |
533 |
|
d_funcToSignature[abs_func] = signature; |
534 |
|
} |
535 |
|
|
536 |
|
Debug("bv-abstraction") << "AbstractionModule::finalizeSignatures abstracted " |
537 |
|
<< d_signatureToFunc.size() << " signatures. \n"; |
538 |
|
} |
539 |
|
|
540 |
|
void AbstractionModule::collectArgumentTypes(TNode sig, std::vector<TypeNode>& types, TNodeSet& seen) { |
541 |
|
if (seen.find(sig) != seen.end()) |
542 |
|
return; |
543 |
|
|
544 |
|
if (sig.getKind() == kind::SKOLEM) { |
545 |
|
types.push_back(sig.getType()); |
546 |
|
seen.insert(sig); |
547 |
|
return; |
548 |
|
} |
549 |
|
|
550 |
|
for (unsigned i = 0; i < sig.getNumChildren(); ++i) { |
551 |
|
collectArgumentTypes(sig[i], types, seen); |
552 |
|
seen.insert(sig); |
553 |
|
} |
554 |
|
} |
555 |
|
|
556 |
|
void AbstractionModule::collectArguments(TNode node, TNode signature, std::vector<Node>& args, TNodeSet& seen) { |
557 |
|
if (seen.find(node)!= seen.end()) |
558 |
|
return; |
559 |
|
|
560 |
|
if (node.getMetaKind() == kind::metakind::VARIABLE |
561 |
|
|| node.getKind() == kind::CONST_BITVECTOR) |
562 |
|
{ |
563 |
|
// a constant in the node can either map to an argument of the abstraction |
564 |
|
// or can be hard-coded and part of the abstraction |
565 |
|
if (signature.getKind() == kind::SKOLEM) { |
566 |
|
args.push_back(node); |
567 |
|
seen.insert(node); |
568 |
|
} else { |
569 |
|
Assert(signature.getKind() == kind::CONST_BITVECTOR); |
570 |
|
} |
571 |
|
// |
572 |
|
return; |
573 |
|
} |
574 |
|
Assert(node.getKind() == signature.getKind() |
575 |
|
&& node.getNumChildren() == signature.getNumChildren()); |
576 |
|
|
577 |
|
for (unsigned i = 0; i < node.getNumChildren(); ++i) { |
578 |
|
collectArguments(node[i], signature[i], args, seen); |
579 |
|
seen.insert(node); |
580 |
|
} |
581 |
|
} |
582 |
|
|
583 |
|
Node AbstractionModule::abstractSignatures(TNode assertion) |
584 |
|
{ |
585 |
|
Debug("bv-abstraction") << "AbstractionModule::abstractSignatures " |
586 |
|
<< assertion << "\n"; |
587 |
|
NodeManager* nm = NodeManager::currentNM(); |
588 |
|
// assume the assertion has been fully abstracted |
589 |
|
Node signature = getGeneralizedSignature(assertion); |
590 |
|
|
591 |
|
Debug("bv-abstraction") << " with sig " << signature << "\n"; |
592 |
|
NodeNodeMap::iterator it = d_signatureToFunc.find(signature); |
593 |
|
if (it != d_signatureToFunc.end()) |
594 |
|
{ |
595 |
|
std::vector<Node> args; |
596 |
|
TNode func = it->second; |
597 |
|
// pushing the function symbol |
598 |
|
args.push_back(func); |
599 |
|
TNodeSet seen; |
600 |
|
collectArguments(assertion, signature, args, seen); |
601 |
|
std::vector<TNode> real_args; |
602 |
|
for (unsigned i = 1; i < args.size(); ++i) |
603 |
|
{ |
604 |
|
real_args.push_back(args[i]); |
605 |
|
} |
606 |
|
d_argsTable.addEntry(func, real_args); |
607 |
|
Node result = nm->mkNode( |
608 |
|
kind::EQUAL, |
609 |
|
nm->mkNode(kind::APPLY_UF, args), utils::mkConst(1, 1u)); |
610 |
|
Debug("bv-abstraction") << "=> " << result << "\n"; |
611 |
|
Assert(result.getType() == assertion.getType()); |
612 |
|
return result; |
613 |
|
} |
614 |
|
return assertion; |
615 |
|
} |
616 |
|
|
617 |
|
bool AbstractionModule::isAbstraction(TNode node) { |
618 |
|
if (node.getKind() != kind::EQUAL) |
619 |
|
return false; |
620 |
|
if ((node[0].getKind() != kind::CONST_BITVECTOR || |
621 |
|
node[1].getKind() != kind::APPLY_UF) && |
622 |
|
(node[1].getKind() != kind::CONST_BITVECTOR || |
623 |
|
node[0].getKind() != kind::APPLY_UF)) |
624 |
|
return false; |
625 |
|
|
626 |
|
TNode constant = node[0].getKind() == kind::CONST_BITVECTOR ? node[0] : node[1]; |
627 |
|
TNode func = node[0].getKind() == kind::APPLY_UF ? node[0] : node[1]; |
628 |
|
Assert(constant.getKind() == kind::CONST_BITVECTOR |
629 |
|
&& func.getKind() == kind::APPLY_UF); |
630 |
|
if (utils::getSize(constant) != 1) |
631 |
|
return false; |
632 |
|
if (constant != utils::mkConst(1, 1u)) |
633 |
|
return false; |
634 |
|
|
635 |
|
TNode func_symbol = func.getOperator(); |
636 |
|
if (d_funcToSignature.find(func_symbol) == d_funcToSignature.end()) |
637 |
|
return false; |
638 |
|
|
639 |
|
return true; |
640 |
|
} |
641 |
|
|
642 |
|
Node AbstractionModule::getInterpretation(TNode node) { |
643 |
|
Assert(isAbstraction(node)); |
644 |
|
TNode constant = node[0].getKind() == kind::CONST_BITVECTOR ? node[0] : node[1]; |
645 |
|
TNode apply = node[0].getKind() == kind::APPLY_UF ? node[0] : node[1]; |
646 |
|
Assert(constant.getKind() == kind::CONST_BITVECTOR |
647 |
|
&& apply.getKind() == kind::APPLY_UF); |
648 |
|
|
649 |
|
Node func = apply.getOperator(); |
650 |
|
Assert(d_funcToSignature.find(func) != d_funcToSignature.end()); |
651 |
|
|
652 |
|
Node sig = d_funcToSignature[func]; |
653 |
|
|
654 |
|
// substitute arguments in signature |
655 |
|
TNodeTNodeMap seen; |
656 |
|
unsigned index = 0; |
657 |
|
Node result = substituteArguments(sig, apply, index, seen); |
658 |
|
Assert(result.getType().isBoolean()); |
659 |
|
Assert(index == apply.getNumChildren()); |
660 |
|
// Debug("bv-abstraction") << "AbstractionModule::getInterpretation " << node << "\n"; |
661 |
|
// Debug("bv-abstraction") << " => " << result << "\n"; |
662 |
|
return result; |
663 |
|
} |
664 |
|
|
665 |
|
Node AbstractionModule::substituteArguments(TNode signature, TNode apply, unsigned& index, TNodeTNodeMap& seen) { |
666 |
|
if (seen.find(signature) != seen.end()) { |
667 |
|
return seen[signature]; |
668 |
|
} |
669 |
|
|
670 |
|
if (signature.getKind() == kind::SKOLEM) { |
671 |
|
// return corresponding argument and increment counter |
672 |
|
seen[signature] = apply[index]; |
673 |
|
return apply[index++]; |
674 |
|
} |
675 |
|
|
676 |
|
if (signature.getNumChildren() == 0) { |
677 |
|
Assert(signature.getMetaKind() != kind::metakind::VARIABLE); |
678 |
|
seen[signature] = signature; |
679 |
|
return signature; |
680 |
|
} |
681 |
|
|
682 |
|
NodeBuilder builder(signature.getKind()); |
683 |
|
if (signature.getMetaKind() == kind::metakind::PARAMETERIZED) { |
684 |
|
builder << signature.getOperator(); |
685 |
|
} |
686 |
|
|
687 |
|
for (unsigned i = 0; i < signature.getNumChildren(); ++i) { |
688 |
|
Node child = substituteArguments(signature[i], apply, index, seen); |
689 |
|
builder << child; |
690 |
|
} |
691 |
|
|
692 |
|
Node result = builder; |
693 |
|
seen[signature]= result; |
694 |
|
|
695 |
|
return result; |
696 |
|
} |
697 |
|
|
698 |
|
Node AbstractionModule::simplifyConflict(TNode conflict) { |
699 |
|
Debug("bv-abstraction-dbg") << "AbstractionModule::simplifyConflict " << conflict << "\n"; |
700 |
|
if (conflict.getKind() != kind::AND) |
701 |
|
return conflict; |
702 |
|
|
703 |
|
std::vector<Node> conjuncts; |
704 |
|
for (unsigned i = 0; i < conflict.getNumChildren(); ++i) |
705 |
|
conjuncts.push_back(conflict[i]); |
706 |
|
|
707 |
|
theory::SubstitutionMap subst(new context::Context()); |
708 |
|
for (unsigned i = 0; i < conjuncts.size(); ++i) { |
709 |
|
TNode conjunct = conjuncts[i]; |
710 |
|
// substitute s -> t |
711 |
|
Node s, t; |
712 |
|
|
713 |
|
if (conjunct.getKind() == kind::EQUAL) { |
714 |
|
if (conjunct[0].getMetaKind() == kind::metakind::VARIABLE && |
715 |
|
conjunct[1].getKind() == kind::CONST_BITVECTOR) { |
716 |
|
s = conjunct[0]; |
717 |
|
t = conjunct[1]; |
718 |
|
} |
719 |
|
else if (conjunct[1].getMetaKind() == kind::metakind::VARIABLE && |
720 |
|
conjunct[0].getKind() == kind::CONST_BITVECTOR) { |
721 |
|
s = conjunct[1]; |
722 |
|
t = conjunct[0]; |
723 |
|
} else { |
724 |
|
continue; |
725 |
|
} |
726 |
|
|
727 |
|
Assert(!subst.hasSubstitution(s)); |
728 |
|
Assert(!t.isNull() && !s.isNull() && s != t); |
729 |
|
subst.addSubstitution(s, t); |
730 |
|
|
731 |
|
for (unsigned k = 0; k < conjuncts.size(); k++) { |
732 |
|
conjuncts[k] = subst.apply(conjuncts[k]); |
733 |
|
} |
734 |
|
} |
735 |
|
} |
736 |
|
Node new_conflict = Rewriter::rewrite(utils::mkAnd(conjuncts)); |
737 |
|
|
738 |
|
Debug("bv-abstraction") << "AbstractionModule::simplifyConflict conflict " << conflict <<"\n"; |
739 |
|
Debug("bv-abstraction") << " => " << new_conflict <<"\n"; |
740 |
|
|
741 |
|
return new_conflict; |
742 |
|
} |
743 |
|
|
744 |
|
void DebugPrintInstantiations( |
745 |
|
const std::vector<std::vector<ArgsVec> >& instantiations, |
746 |
|
const std::vector<TNode>& functions) |
747 |
|
{ |
748 |
|
// print header |
749 |
|
Debug("bv-abstraction-dbg") <<"[ "; |
750 |
|
for (unsigned i = 0; i < functions.size(); ++i) { |
751 |
|
for (unsigned j = 1; j < functions[i].getNumChildren(); ++j) { |
752 |
|
Debug("bv-abstraction-dgb") << functions[i][j] <<" "; |
753 |
|
} |
754 |
|
Debug("bv-abstraction-dgb") << " || "; |
755 |
|
} |
756 |
|
Debug("bv-abstraction-dbg") <<"]\n"; |
757 |
|
|
758 |
|
for (unsigned i = 0; i < instantiations.size(); ++i) { |
759 |
|
Debug("bv-abstraction-dbg") <<"["; |
760 |
|
const std::vector<ArgsVec>& inst = instantiations[i]; |
761 |
|
for (unsigned j = 0; j < inst.size(); ++j) { |
762 |
|
for (unsigned k = 0; k < inst[j].size(); ++k) { |
763 |
|
Debug("bv-abstraction-dbg") << inst[j][k] << " "; |
764 |
|
} |
765 |
|
Debug("bv-abstraction-dbg") << " || "; |
766 |
|
} |
767 |
|
Debug("bv-abstraction-dbg") <<"]\n"; |
768 |
|
} |
769 |
|
} |
770 |
|
|
771 |
|
void AbstractionModule::generalizeConflict(TNode conflict, std::vector<Node>& lemmas) { |
772 |
|
Debug("bv-abstraction") << "AbstractionModule::generalizeConflict " << conflict << "\n"; |
773 |
|
std::vector<TNode> functions; |
774 |
|
|
775 |
|
// collect abstract functions |
776 |
|
if (conflict.getKind() != kind::AND) { |
777 |
|
if (isAbstraction(conflict)) { |
778 |
|
Assert(conflict[0].getKind() == kind::APPLY_UF); |
779 |
|
functions.push_back(conflict[0]); |
780 |
|
} |
781 |
|
} else { |
782 |
|
for (unsigned i = 0; i < conflict.getNumChildren(); ++i) { |
783 |
|
TNode conjunct = conflict[i]; |
784 |
|
if (isAbstraction(conjunct)) { |
785 |
|
Assert(conjunct[0].getKind() == kind::APPLY_UF); |
786 |
|
functions.push_back(conjunct[0]); |
787 |
|
} |
788 |
|
} |
789 |
|
} |
790 |
|
|
791 |
|
// if (functions.size() >= 3) { |
792 |
|
// // dump conflict |
793 |
|
// NodeNodeMap seen; |
794 |
|
// Node reversed = reverseAbstraction(conflict, seen); |
795 |
|
// std::cout << "CONFLICT " << reversed << "\n"; |
796 |
|
// } |
797 |
|
|
798 |
|
|
799 |
|
if (functions.size() == 0 || functions.size() > options::bvNumFunc()) { |
800 |
|
return; |
801 |
|
} |
802 |
|
|
803 |
|
|
804 |
|
// Skolemize function arguments to avoid confusion in pattern matching |
805 |
|
SubstitutionMap skolem_subst(new context::Context()); |
806 |
|
SubstitutionMap reverse_skolem(new context::Context()); |
807 |
|
makeFreshSkolems(conflict, skolem_subst, reverse_skolem); |
808 |
|
|
809 |
|
Node skolemized_conflict = skolem_subst.apply(conflict); |
810 |
|
for (unsigned i = 0; i < functions.size(); ++i) { |
811 |
|
functions[i] = skolem_subst.apply(functions[i]); |
812 |
|
} |
813 |
|
|
814 |
|
conflict = skolem_subst.apply(conflict); |
815 |
|
|
816 |
|
LemmaInstantiatior inst(functions, d_argsTable, conflict); |
817 |
|
std::vector<Node> new_lemmas; |
818 |
|
inst.generateInstantiations(new_lemmas); |
819 |
|
for (unsigned i = 0; i < new_lemmas.size(); ++i) { |
820 |
|
TNode lemma = reverse_skolem.apply(new_lemmas[i]); |
821 |
|
if (d_addedLemmas.find(lemma) == d_addedLemmas.end()) { |
822 |
|
lemmas.push_back(lemma); |
823 |
|
Debug("bv-abstraction-gen") << "adding lemma " << lemma << "\n"; |
824 |
|
storeLemma(lemma); |
825 |
|
} |
826 |
|
} |
827 |
|
} |
828 |
|
|
829 |
|
int AbstractionModule::LemmaInstantiatior::next(int val, int index) { |
830 |
|
if (val < d_maxMatch[index] - 1) |
831 |
|
return val + 1; |
832 |
|
return -1; |
833 |
|
} |
834 |
|
|
835 |
|
/** |
836 |
|
* Assumes the stack without top is consistent, and checks that the |
837 |
|
* full stack is consistent |
838 |
|
* |
839 |
|
* @param stack |
840 |
|
* |
841 |
|
* @return |
842 |
|
*/ |
843 |
|
bool AbstractionModule::LemmaInstantiatior::isConsistent(const vector<int>& stack) { |
844 |
|
if (stack.empty()) |
845 |
|
return true; |
846 |
|
|
847 |
|
unsigned current = stack.size() - 1; |
848 |
|
TNode func = d_functions[current]; |
849 |
|
ArgsTableEntry& matches = d_argsTable.getEntry(func.getOperator()); |
850 |
|
ArgsVec& args = matches.getEntry(stack[current]); |
851 |
|
Assert(args.size() == func.getNumChildren()); |
852 |
|
for (unsigned k = 0; k < args.size(); ++k) { |
853 |
|
TNode s = func[k]; |
854 |
|
TNode t = args[k]; |
855 |
|
|
856 |
|
TNode s0 = s; |
857 |
|
while (d_subst.hasSubstitution(s0)) { |
858 |
|
s0 = d_subst.getSubstitution(s0); |
859 |
|
} |
860 |
|
|
861 |
|
TNode t0 = t; |
862 |
|
while (d_subst.hasSubstitution(t0)) { |
863 |
|
t0 = d_subst.getSubstitution(t0); |
864 |
|
} |
865 |
|
|
866 |
|
if (s0.isConst() && t0.isConst()) { |
867 |
|
if (s0 != t0) |
868 |
|
return false; // fail |
869 |
|
else |
870 |
|
continue; |
871 |
|
} |
872 |
|
|
873 |
|
if(s0.getMetaKind() == kind::metakind::VARIABLE && |
874 |
|
t0.isConst()) { |
875 |
|
d_subst.addSubstitution(s0, t0); |
876 |
|
continue; |
877 |
|
} |
878 |
|
|
879 |
|
if (s0.isConst() && |
880 |
|
t0.getMetaKind() == kind::metakind::VARIABLE) { |
881 |
|
d_subst.addSubstitution(t0, s0); |
882 |
|
continue; |
883 |
|
} |
884 |
|
|
885 |
|
Assert(s0.getMetaKind() == kind::metakind::VARIABLE |
886 |
|
&& t0.getMetaKind() == kind::metakind::VARIABLE); |
887 |
|
|
888 |
|
if (s0 != t0) { |
889 |
|
d_subst.addSubstitution(s0, t0); |
890 |
|
} |
891 |
|
} |
892 |
|
return true; |
893 |
|
} |
894 |
|
|
895 |
|
bool AbstractionModule::LemmaInstantiatior::accept(const vector<int>& stack) { |
896 |
|
return stack.size() == d_functions.size(); |
897 |
|
} |
898 |
|
|
899 |
|
void AbstractionModule::LemmaInstantiatior::mkLemma() { |
900 |
|
Node lemma = d_subst.apply(d_conflict); |
901 |
|
// Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::mkLemma " << lemma <<"\n"; |
902 |
|
d_lemmas.push_back(lemma); |
903 |
|
} |
904 |
|
|
905 |
|
void AbstractionModule::LemmaInstantiatior::backtrack(vector<int>& stack) { |
906 |
|
if (!isConsistent(stack)) |
907 |
|
return; |
908 |
|
|
909 |
|
if (accept(stack)) { |
910 |
|
mkLemma(); |
911 |
|
return; |
912 |
|
} |
913 |
|
|
914 |
|
int x = 0; |
915 |
|
while (x != -1) { |
916 |
|
d_ctx->push(); |
917 |
|
stack.push_back(x); |
918 |
|
backtrack(stack); |
919 |
|
|
920 |
|
d_ctx->pop(); |
921 |
|
stack.pop_back(); |
922 |
|
x = next(x, stack.size()); |
923 |
|
} |
924 |
|
} |
925 |
|
|
926 |
|
|
927 |
|
void AbstractionModule::LemmaInstantiatior::generateInstantiations(std::vector<Node>& lemmas) { |
928 |
|
Debug("bv-abstraction-gen") << "AbstractionModule::LemmaInstantiatior::generateInstantiations "; |
929 |
|
|
930 |
|
std::vector<int> stack; |
931 |
|
backtrack(stack); |
932 |
|
Assert(d_ctx->getLevel() == 0); |
933 |
|
Debug("bv-abstraction-gen") << "numLemmas=" << d_lemmas.size() <<"\n"; |
934 |
|
lemmas.swap(d_lemmas); |
935 |
|
} |
936 |
|
|
937 |
|
void AbstractionModule::makeFreshSkolems(TNode node, SubstitutionMap& map, SubstitutionMap& reverse_map) { |
938 |
|
if (map.hasSubstitution(node)) { |
939 |
|
return; |
940 |
|
} |
941 |
|
if (node.getMetaKind() == kind::metakind::VARIABLE) { |
942 |
|
Node skolem = utils::mkVar(utils::getSize(node)); |
943 |
|
map.addSubstitution(node, skolem); |
944 |
|
reverse_map.addSubstitution(skolem, node); |
945 |
|
return; |
946 |
|
} |
947 |
|
if (node.isConst()) |
948 |
|
return; |
949 |
|
|
950 |
|
for (unsigned i = 0; i < node.getNumChildren(); ++i) { |
951 |
|
makeFreshSkolems(node[i], map, reverse_map); |
952 |
|
} |
953 |
|
} |
954 |
|
|
955 |
|
void AbstractionModule::makeFreshArgs(TNode func, std::vector<Node>& fresh_args) { |
956 |
|
Assert(fresh_args.size() == 0); |
957 |
|
Assert(func.getKind() == kind::APPLY_UF); |
958 |
|
TNodeNodeMap d_map; |
959 |
|
for (unsigned i = 0; i < func.getNumChildren(); ++i) { |
960 |
|
TNode arg = func[i]; |
961 |
|
if (arg.isConst()) { |
962 |
|
fresh_args.push_back(arg); |
963 |
|
continue; |
964 |
|
} |
965 |
|
Assert(arg.getMetaKind() == kind::metakind::VARIABLE); |
966 |
|
TNodeNodeMap::iterator it = d_map.find(arg); |
967 |
|
if (it != d_map.end()) { |
968 |
|
fresh_args.push_back(it->second); |
969 |
|
} else { |
970 |
|
Node skolem = utils::mkVar(utils::getSize(arg)); |
971 |
|
d_map[arg] = skolem; |
972 |
|
fresh_args.push_back(skolem); |
973 |
|
} |
974 |
|
} |
975 |
|
Assert(fresh_args.size() == func.getNumChildren()); |
976 |
|
} |
977 |
|
|
978 |
|
Node AbstractionModule::tryMatching(const std::vector<Node>& ss, const std::vector<TNode>& tt, TNode conflict) { |
979 |
|
Assert(ss.size() == tt.size()); |
980 |
|
|
981 |
|
Debug("bv-abstraction-dbg") << "AbstractionModule::tryMatching conflict = " << conflict << "\n"; |
982 |
|
if (Debug.isOn("bv-abstraction-dbg")) { |
983 |
|
Debug("bv-abstraction-dbg") << " Match: "; |
984 |
|
for (unsigned i = 0; i < ss.size(); ++i) { |
985 |
|
Debug("bv-abstraction-dbg") << ss[i] <<" "; |
986 |
|
|
987 |
|
} |
988 |
|
Debug("bv-abstraction-dbg") << "\n To: "; |
989 |
|
for (unsigned i = 0; i < tt.size(); ++i) { |
990 |
|
Debug("bv-abstraction-dbg") << tt[i] <<" "; |
991 |
|
} |
992 |
|
Debug("bv-abstraction-dbg") <<"\n"; |
993 |
|
} |
994 |
|
|
995 |
|
|
996 |
|
SubstitutionMap subst(new context::Context()); |
997 |
|
|
998 |
|
for (unsigned i = 0; i < ss.size(); ++i) { |
999 |
|
TNode s = ss[i]; |
1000 |
|
TNode t = tt[i]; |
1001 |
|
|
1002 |
|
TNode s0 = subst.hasSubstitution(s) ? subst.getSubstitution(s) : s; |
1003 |
|
TNode t0 = subst.hasSubstitution(t) ? subst.getSubstitution(t) : t; |
1004 |
|
|
1005 |
|
if (s0.isConst() && t0.isConst()) { |
1006 |
|
if (s0 != t0) |
1007 |
|
return Node(); // fail |
1008 |
|
else |
1009 |
|
continue; |
1010 |
|
} |
1011 |
|
|
1012 |
|
if(s0.getMetaKind() == kind::metakind::VARIABLE && |
1013 |
|
t0.isConst()) { |
1014 |
|
subst.addSubstitution(s0, t0); |
1015 |
|
continue; |
1016 |
|
} |
1017 |
|
|
1018 |
|
if (s0.isConst() && |
1019 |
|
t0.getMetaKind() == kind::metakind::VARIABLE) { |
1020 |
|
subst.addSubstitution(t0, s0); |
1021 |
|
continue; |
1022 |
|
} |
1023 |
|
|
1024 |
|
Assert(s0.getMetaKind() == kind::metakind::VARIABLE |
1025 |
|
&& t0.getMetaKind() == kind::metakind::VARIABLE); |
1026 |
|
|
1027 |
|
Assert(s0 != t0); |
1028 |
|
subst.addSubstitution(s0, t0); |
1029 |
|
} |
1030 |
|
|
1031 |
|
Node res = subst.apply(conflict); |
1032 |
|
Debug("bv-abstraction-dbg") << " Lemma: " << res <<"\n"; |
1033 |
|
return res; |
1034 |
|
} |
1035 |
|
|
1036 |
|
void AbstractionModule::storeLemma(TNode lemma) { |
1037 |
|
d_addedLemmas.insert(lemma); |
1038 |
|
if (lemma.getKind() == kind::AND) { |
1039 |
|
for (unsigned i = 0; i < lemma.getNumChildren(); i++) { |
1040 |
|
TNode atom = lemma[i]; |
1041 |
|
atom = atom.getKind() == kind::NOT ? atom[0] : atom; |
1042 |
|
Assert(atom.getKind() != kind::NOT); |
1043 |
|
Assert(utils::isBVPredicate(atom)); |
1044 |
|
d_lemmaAtoms.insert(atom); |
1045 |
|
} |
1046 |
|
} else { |
1047 |
|
lemma = lemma.getKind() == kind::NOT? lemma[0] : lemma; |
1048 |
|
Assert(utils::isBVPredicate(lemma)); |
1049 |
|
d_lemmaAtoms.insert(lemma); |
1050 |
|
} |
1051 |
|
} |
1052 |
|
|
1053 |
|
|
1054 |
|
bool AbstractionModule::isLemmaAtom(TNode node) const { |
1055 |
|
Assert(node.getType().isBoolean()); |
1056 |
|
node = node.getKind() == kind::NOT? node[0] : node; |
1057 |
|
|
1058 |
|
return d_inputAtoms.find(node) == d_inputAtoms.end() && |
1059 |
|
d_lemmaAtoms.find(node) != d_lemmaAtoms.end(); |
1060 |
|
} |
1061 |
|
|
1062 |
|
void AbstractionModule::addInputAtom(TNode atom) { |
1063 |
|
if (options::bitblastMode() == options::BitblastMode::LAZY) |
1064 |
|
{ |
1065 |
|
d_inputAtoms.insert(atom); |
1066 |
|
} |
1067 |
|
} |
1068 |
|
|
1069 |
|
void AbstractionModule::ArgsTableEntry::addArguments(const ArgsVec& args) { |
1070 |
|
Assert(args.size() == d_arity); |
1071 |
|
d_data.push_back(args); |
1072 |
|
} |
1073 |
|
|
1074 |
|
void AbstractionModule::ArgsTable::addEntry(TNode signature, const ArgsVec& args) { |
1075 |
|
if (d_data.find(signature) == d_data.end()) { |
1076 |
|
d_data[signature] = ArgsTableEntry(args.size()); |
1077 |
|
} |
1078 |
|
ArgsTableEntry& entry = d_data[signature]; |
1079 |
|
entry.addArguments(args); |
1080 |
|
} |
1081 |
|
|
1082 |
|
|
1083 |
|
bool AbstractionModule::ArgsTable::hasEntry(TNode signature) const { |
1084 |
|
return d_data.find(signature) != d_data.end(); |
1085 |
|
} |
1086 |
|
|
1087 |
|
AbstractionModule::ArgsTableEntry& AbstractionModule::ArgsTable::getEntry(TNode signature) { |
1088 |
|
Assert(hasEntry(signature)); |
1089 |
|
return d_data.find(signature)->second; |
1090 |
|
} |
1091 |
|
|
1092 |
2 |
AbstractionModule::Statistics::Statistics( |
1093 |
2 |
const std::string& name, const NodeNodeMap& functionsAbstracted) |
1094 |
|
: d_numFunctionsAbstracted( |
1095 |
2 |
smtStatisticsRegistry().registerSize<NodeNodeMap>( |
1096 |
4 |
name + "NumFunctionsAbstracted", functionsAbstracted)), |
1097 |
|
d_numArgsSkolemized( |
1098 |
4 |
smtStatisticsRegistry().registerInt(name + "NumArgsSkolemized")), |
1099 |
|
d_abstractionTime( |
1100 |
6 |
smtStatisticsRegistry().registerTimer(name + "AbstractionTime")) |
1101 |
|
{ |
1102 |
29351 |
} |