1 /********************************************************************
2 * AUTHORS: Vijay Ganesh
3 *
4 * BEGIN DATE: November, 2005
5 *
6 Permission is hereby granted, free of charge, to any person obtaining a copy
7 of this software and associated documentation files (the "Software"), to deal
8 in the Software without restriction, including without limitation the rights
9 to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
10 copies of the Software, and to permit persons to whom the Software is
11 furnished to do so, subject to the following conditions:
12
13 The above copyright notice and this permission notice shall be included in
14 all copies or substantial portions of the Software.
15
16 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
17 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
18 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
19 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
20 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
21 OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
22 THE SOFTWARE.
23 ********************************************************************/
24
25 #include "stp/AbsRefineCounterExample/AbsRefine_CounterExample.h"
26 #include "stp/Printer/printers.h"
27 #include "stp/ToSat/AIG/ToSATAIG.h"
28
29 const bool debug_counterexample = false;
30
31 namespace stp
32 {
33 using std::cout;
34
35 /*FUNCTION: constructs counterexample from MINISAT counterexample
36 * step1 : iterate through MINISAT counterexample and assemble the
37 * bits for each AST term. Store it in a map from ASTNode to vector
38 * of bools (bits).
39 *
40 * step2: Iterate over the map from ASTNodes->Vector-of-Bools and
41 * populate the CounterExampleMap data structure (ASTNode -> BVConst)
42 */
ConstructCounterExample(SATSolver & newS,ToSATBase::ASTNodeToSATVar & satVarToSymbol)43 void AbsRefine_CounterExample::ConstructCounterExample(
44 SATSolver& newS, ToSATBase::ASTNodeToSATVar& satVarToSymbol)
45 {
46 if (!newS.okay())
47 return;
48 if (!bm->UserFlags.construct_counterexample_flag)
49 return;
50
51 assert(CounterExampleMap.size() == 0);
52
53 CopySolverMap_To_CounterExample();
54
55 for (ToSATBase::ASTNodeToSATVar::const_iterator it = satVarToSymbol.begin();
56 it != satVarToSymbol.end(); it++)
57 {
58 const ASTNode& symbol = it->first;
59 const vector<unsigned>& v = it->second;
60
61 const unsigned int symbolWidth = symbol.GetValueWidth();
62 assert(symbol.GetKind() == SYMBOL);
63 vector<bool> bitVector_array(symbolWidth, false);
64
65 for (size_t index = 0; index < v.size(); index++)
66 {
67 const unsigned sat_variable_index = v[index];
68
69 if (sat_variable_index == ~((unsigned)0)) // not sent to the sat solver.
70 continue;
71
72 if (newS.modelValue(sat_variable_index) == newS.undef_literal())
73 continue;
74
75 // assemble the counterexample here
76 if (symbol.GetType() == BITVECTOR_TYPE)
77 {
78 // Collect the bits of 'symbol' and store in v. Store
79 // in reverse order.
80 bitVector_array[(symbolWidth - 1) - index] =
81 (newS.modelValue(sat_variable_index) == newS.true_literal());
82 }
83 else
84 {
85 assert(symbol.GetType() == BOOLEAN_TYPE);
86 if (newS.modelValue(sat_variable_index) == newS.true_literal())
87 CounterExampleMap[symbol] = ASTTrue;
88 else if (newS.modelValue(sat_variable_index) == newS.false_literal())
89 CounterExampleMap[symbol] = ASTFalse;
90 else
91 FatalError("never heres.");
92 }
93 }
94
95 if (symbol.GetType() == BITVECTOR_TYPE)
96 {
97 CounterExampleMap[symbol] =
98 BoolVectoBVConst(&bitVector_array, symbol.GetValueWidth());
99 }
100 }
101
102 for (ArrayTransformer::ArrType::const_iterator
103 it = ArrayTransform->arrayToIndexToRead.begin(),
104 itend = ArrayTransform->arrayToIndexToRead.end();
105 it != itend; it++)
106 {
107 const ASTNode& array = it->first;
108 const std::map<ASTNode, ArrayTransformer::ArrayRead>& mapper = it->second;
109
110 for (std::map<ASTNode, ArrayTransformer::ArrayRead>::const_iterator
111 it2 = mapper.begin(),
112 it2end = mapper.end();
113 it2 != it2end; it2++)
114 {
115 const ASTNode& index = it2->first;
116 const ASTNode& value_ite = it2->second.ite;
117
118 // convert it to a constant array-read and store it in the
119 // counter-example. First convert the index into a constant. then
120 // construct the appropriate array-read and store it in the
121 // counterexample
122 ASTNode arrayread_index = TermToConstTermUsingModel(index, false);
123 ASTNode key =
124 bm->CreateTerm(READ, array.GetValueWidth(), array, arrayread_index);
125
126 // Get the ITE corresponding to the array-read and convert it
127 // to a constant against the model
128 ASTNode value = TermToConstTermUsingModel(value_ite);
129 // save the result in the counter_example
130 if (!simp->InsideSubstitutionMap(key))
131 CounterExampleMap[key] = value;
132 }
133 }
134 }
135
136 // FUNCTION: accepts a non-constant term, and returns the
137 // corresponding constant term with respect to a model.
138 //
139 // term READ(A,i) is treated as follows:
140 //
141 // 1. If (the boolean variable 'ArrayReadFlag' is true && ArrayRead
142 // 1. has value in counterexample), then return the value of the
143 // 1. arrayread.
144 //
145 // 2. If (the boolean variable 'ArrayReadFlag' is true && ArrayRead
146 // 2. doesn't have value in counterexample), then return the
147 // 2. arrayread itself (normalized such that arrayread has a constant
148 // 2. index)
149 //
150 // 3. If (the boolean variable 'ArrayReadFlag' is false) && ArrayRead
151 // 3. has a value in the counterexample then return the value of the
152 // 3. arrayread.
153 //
154 // 4. If (the boolean variable 'ArrayReadFlag' is false) && ArrayRead
155 // 4. doesn't have a value in the counterexample then return 0 as the
156 // 4. value of the arrayread.
TermToConstTermUsingModel(const ASTNode & term,bool ArrayReadFlag)157 ASTNode AbsRefine_CounterExample::TermToConstTermUsingModel(const ASTNode& term,
158 bool ArrayReadFlag)
159 {
160 if (term.GetKind() == BVCONST)
161 return term;
162
163 const Kind k = term.GetKind();
164
165 assert(is_Term_kind(k));
166 assert(k != WRITE);
167 assert(BOOLEAN_TYPE != term.GetType());
168
169 ASTNodeMap::const_iterator it1;
170 if ((it1 = CounterExampleMap.find(term)) != CounterExampleMap.end())
171 {
172 const ASTNode& val = it1->second;
173 if (BVCONST != val.GetKind())
174 {
175 // CounterExampleMap has two maps rolled into
176 // one. SubstitutionMap and SolverMap.
177 //
178 // recursion is fine here. There are two maps that are checked
179 // here. One is the substitutionmap. We garuntee that the value
180 // of a key in the substitutionmap is always a constant.
181 //
182 // in the SolverMap we garuntee that "term" does not occur in
183 // the value part of the map
184 if (term == val)
185 {
186 FatalError("TermToConstTermUsingModel: "
187 "The input term is stored as-is "
188 "in the CounterExample: Not ok: ",
189 term);
190 }
191 return TermToConstTermUsingModel(val, ArrayReadFlag);
192 }
193 else
194 {
195 return val;
196 }
197 }
198
199 ASTNode output;
200 switch (k)
201 {
202 case BVCONST:
203 output = term;
204 break;
205 case SYMBOL:
206 {
207 if (term.GetType() == ARRAY_TYPE)
208 {
209 return term;
210 }
211
212 // Has been simplified out. Can take any value.
213 output = bm->CreateZeroConst(term.GetValueWidth());
214 break;
215 }
216 case READ:
217 {
218 ASTNode arrName = term[0];
219 ASTNode index = term[1];
220 if (0 == arrName.GetIndexWidth())
221 {
222 FatalError("TermToConstTermUsingModel: "
223 "array has 0 index width: ",
224 arrName);
225 }
226
227 if (WRITE == arrName.GetKind()) // READ over a WRITE
228 {
229 ASTNode wrtterm = Expand_ReadOverWrite_UsingModel(term, ArrayReadFlag);
230 if (wrtterm == term)
231 {
232 FatalError("TermToConstTermUsingModel: "
233 "Read_Over_Write term must be expanded "
234 "into an ITE",
235 term);
236 }
237 ASTNode rtterm = TermToConstTermUsingModel(wrtterm, ArrayReadFlag);
238 assert(ArrayReadFlag || (BVCONST == rtterm.GetKind()));
239 return rtterm;
240 }
241 else if (ITE == arrName.GetKind()) // READ over an ITE
242 {
243 // The "then" and "else" branch are arrays.
244 ASTNode indexVal = TermToConstTermUsingModel(index, ArrayReadFlag);
245
246 ASTNode condcompute =
247 ComputeFormulaUsingModel(arrName[0]); // Get the truth value.
248 unsigned int wid = arrName.GetValueWidth();
249 if (ASTTrue == condcompute)
250 {
251 const ASTNode& result = TermToConstTermUsingModel(
252 bm->CreateTerm(READ, wid, arrName[1], indexVal), ArrayReadFlag);
253 assert(ArrayReadFlag || (BVCONST == result.GetKind()));
254 return result;
255 }
256 else if (ASTFalse == condcompute)
257 {
258 const ASTNode& result = TermToConstTermUsingModel(
259 bm->CreateTerm(READ, wid, arrName[2], indexVal), ArrayReadFlag);
260 assert(ArrayReadFlag || (BVCONST == result.GetKind()));
261 return result;
262 }
263 else
264 {
265 FatalError(" TermToConstTermUsingModel: termITE: "
266 "cannot compute ITE conditional against model: ",
267 term);
268 }
269 }
270
271 ASTNode modelentry;
272 if (CounterExampleMap.find(index) != CounterExampleMap.end())
273 {
274 // index has a const value in the CounterExampleMap
275 // ASTNode indexVal = CounterExampleMap[index];
276 ASTNode indexVal =
277 TermToConstTermUsingModel(CounterExampleMap[index], ArrayReadFlag);
278 modelentry =
279 bm->CreateTerm(READ, arrName.GetValueWidth(), arrName, indexVal);
280 }
281 else
282 {
283 // index does not have a const value in the
284 // CounterExampleMap. compute it.
285 ASTNode indexconstval = TermToConstTermUsingModel(index, ArrayReadFlag);
286 // update model with value of the index
287 // CounterExampleMap[index] = indexconstval;
288 modelentry = bm->CreateTerm(READ, arrName.GetValueWidth(), arrName,
289 indexconstval);
290 }
291 // modelentry is now an arrayread over a constant index
292 BVTypeCheck(modelentry);
293
294 // if a value exists in the CounterExampleMap then return it
295 if (CounterExampleMap.find(modelentry) != CounterExampleMap.end())
296 {
297 output = TermToConstTermUsingModel(CounterExampleMap[modelentry],
298 ArrayReadFlag);
299 }
300 else if (ArrayReadFlag)
301 {
302 // return the array read over a constantindex
303 output = modelentry;
304 }
305 else
306 {
307 // Has been simplified out. Can take any value.
308 output = bm->CreateMaxConst(modelentry.GetValueWidth());
309 }
310 break;
311 }
312 case ITE:
313 {
314 ASTNode condcompute = ComputeFormulaUsingModel(term[0]);
315 if (ASTTrue == condcompute)
316 {
317 output = TermToConstTermUsingModel(term[1], ArrayReadFlag);
318 }
319 else if (ASTFalse == condcompute)
320 {
321 output = TermToConstTermUsingModel(term[2], ArrayReadFlag);
322 }
323 else
324 {
325 FatalError(" TermToConstTermUsingModel: termITE: cannot "
326 "compute ITE conditional against model: ",
327 term);
328 }
329 break;
330 }
331 default:
332 {
333 const ASTVec& c = term.GetChildren();
334 ASTVec o;
335 o.reserve(c.size());
336 for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend;
337 it++)
338 {
339 ASTNode ff = TermToConstTermUsingModel(*it, ArrayReadFlag);
340 o.push_back(ff);
341 }
342
343 output = NonMemberBVConstEvaluator(bm, k, o, term.GetValueWidth());
344 break;
345 }
346 }
347
348 assert(ArrayReadFlag || (BVCONST == output.GetKind()));
349
350 // when this flag is false, we should compute the arrayread to a
351 // constant. this constant is stored in the counter_example
352 // datastructure
353 // if (!ArrayReadFlag)
354 {
355 CounterExampleMap[term] = output;
356 }
357
358 // cerr << "Output to TermToConstTermUsingModel: " << output << endl;
359 return output;
360 }
361
362 // Expands read-over-write by evaluating (readIndex=writeIndex) for
363 // every writeindex until, either it evaluates to TRUE or all
364 //(readIndex=writeIndex) evaluate to FALSE
365 ASTNode
Expand_ReadOverWrite_UsingModel(const ASTNode & term,bool arrayread_flag)366 AbsRefine_CounterExample::Expand_ReadOverWrite_UsingModel(const ASTNode& term,
367 bool arrayread_flag)
368 {
369 if (READ != term.GetKind() || WRITE != term[0].GetKind())
370 {
371 FatalError("RemovesWrites: Input must be a READ over a WRITE", term);
372 }
373
374 ASTNode output;
375 ASTNodeMap::iterator it1;
376 if ((it1 = CounterExampleMap.find(term)) != CounterExampleMap.end())
377 {
378 const ASTNode& val = it1->second;
379 if (BVCONST != val.GetKind())
380 {
381 // recursion is fine here. There are two maps that are checked
382 // here. One is the substitutionmap. We garuntee that the value
383 // of a key in the substitutionmap is always a constant.
384 if (term == val)
385 {
386 FatalError("TermToConstTermUsingModel: The input term is "
387 "stored as-is "
388 "in the CounterExample: Not ok: ",
389 term);
390 }
391 return TermToConstTermUsingModel(val, arrayread_flag);
392 }
393 else
394 {
395 return val;
396 }
397 }
398
399 ASTNode newRead = term;
400 const ASTNode readIndex = TermToConstTermUsingModel(newRead[1], false);
401 // iteratively expand read-over-write, and evaluate against the
402 // model at every iteration
403 ASTNode write = newRead[0];
404 do
405 {
406 ASTNode writeIndex = TermToConstTermUsingModel(write[1], false);
407
408 if (writeIndex == readIndex)
409 {
410 // found the write-value. return it
411 output = TermToConstTermUsingModel(write[2], false);
412 CounterExampleMap[term] = output;
413 return output;
414 }
415
416 write = write[0];
417 } while (WRITE == write.GetKind());
418
419 const unsigned int width = term.GetValueWidth();
420 newRead = bm->CreateTerm(READ, width, write, readIndex);
421 output = TermToConstTermUsingModel(newRead, arrayread_flag);
422
423 // memoize
424 CounterExampleMap[term] = output;
425 return output;
426 } // Expand_ReadOverWrite_UsingModel()
427
428 /* FUNCTION: accepts a non-constant formula, and checks if the
429 * formula is ASTTrue or ASTFalse w.r.t to a model
430 */
ComputeFormulaUsingModel(const ASTNode & form)431 ASTNode AbsRefine_CounterExample::ComputeFormulaUsingModel(const ASTNode& form)
432 {
433 const Kind k = form.GetKind();
434 if (!(is_Form_kind(k) && BOOLEAN_TYPE == form.GetType()))
435 {
436 FatalError(" ComputeConstFormUsingModel: "
437 "The input is a non-formula: ",
438 form);
439 }
440
441 // cerr << "Input to ComputeFormulaUsingModel:" << form << endl;
442 ASTNodeMap::const_iterator it1;
443 if ((it1 = ComputeFormulaMap.find(form)) != ComputeFormulaMap.end())
444 {
445 const ASTNode& res = it1->second;
446 if (ASTTrue == res || ASTFalse == res)
447 {
448 return res;
449 }
450 else
451 {
452 FatalError("ComputeFormulaUsingModel: "
453 "The value of a formula must be TRUE or FALSE:",
454 form);
455 }
456 }
457
458 ASTNode output = ASTUndefined;
459 switch (k)
460 {
461 case TRUE:
462 case FALSE:
463 output = form;
464 break;
465 case SYMBOL:
466 if (BOOLEAN_TYPE != form.GetType())
467 FatalError(" ComputeFormulaUsingModel: "
468 "Non-Boolean variables are not formulas",
469 form);
470 if (CounterExampleMap.find(form) != CounterExampleMap.end())
471 {
472 ASTNode counterexample_val = CounterExampleMap[form];
473 if (!bm->VarSeenInTerm(form, counterexample_val))
474 {
475 output = ComputeFormulaUsingModel(counterexample_val);
476 }
477 else
478 {
479 output = counterexample_val;
480 }
481 }
482 else
483 {
484 // Has been simplified out. Can take any value.
485 output = ASTFalse;
486 }
487 break;
488 case BOOLEXTRACT:
489 {
490 ASTNode t0 = TermToConstTermUsingModel(form[0]);
491 output = simp->BVConstEvaluator(bm->CreateNode(BOOLEXTRACT, t0, form[1]));
492 break;
493 }
494 case EQ:
495 case BVLT:
496 case BVLE:
497 case BVGT:
498 case BVGE:
499 case BVSLT:
500 case BVSLE:
501 case BVSGT:
502 case BVSGE:
503 {
504 ASTVec children;
505 children.reserve(form.Degree());
506
507 for (ASTVec::const_iterator it = form.begin(), itend = form.end();
508 it != itend; it++)
509 {
510 children.push_back(TermToConstTermUsingModel(*it, false));
511 }
512
513 output = NonMemberBVConstEvaluator(bm, k, children, form.GetValueWidth());
514 }
515 break;
516
517 case NAND:
518 case NOR:
519 case NOT:
520 case AND:
521 case XOR:
522 case IFF:
523 case IMPLIES:
524 case OR:
525 {
526 ASTVec children;
527 children.reserve(form.Degree());
528
529 for (ASTVec::const_iterator it = form.begin(), itend = form.end();
530 it != itend; it++)
531 {
532 children.push_back(ComputeFormulaUsingModel(*it));
533 }
534
535 output = NonMemberBVConstEvaluator(bm, k, children, form.GetValueWidth());
536 }
537 break;
538
539 case ITE:
540 {
541 ASTNode t0 = ComputeFormulaUsingModel(form[0]);
542 if (ASTTrue == t0)
543 output = ComputeFormulaUsingModel(form[1]);
544 else if (ASTFalse == t0)
545 output = ComputeFormulaUsingModel(form[2]);
546 else
547 FatalError("ComputeFormulaUsingModel: ITE: "
548 "something is wrong with the formula: ",
549 form);
550 }
551 break;
552 case PARAMBOOL:
553 output = bm->NewParameterized_BooleanVar(form[0], form[1]);
554 output = ComputeFormulaUsingModel(output);
555 break;
556 default:
557 cerr << _kind_names[k];
558 FatalError(" ComputeFormulaUsingModel: "
559 "the kind has not been implemented",
560 ASTUndefined);
561 break;
562 }
563
564 assert(ASTUndefined != output);
565 assert(output.isConstant());
566 ComputeFormulaMap[form] = output;
567 return output;
568 }
569
CheckCounterExample(bool t)570 void AbsRefine_CounterExample::CheckCounterExample(bool t)
571 {
572 // input is valid, no counterexample to check
573 if (bm->ValidFlag)
574 return;
575
576 // t is true if SAT solver generated a counterexample, else it is false
577 if (!t)
578 FatalError("CheckCounterExample: "
579 "No CounterExample to check",
580 ASTUndefined);
581 const ASTVec c = bm->GetAsserts();
582
583 if (bm->UserFlags.stats_flag)
584 printf("checking counterexample\n");
585
586 for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend;
587 it++)
588 {
589 if (debug_counterexample)
590 cerr << "checking" << *it;
591
592 if (ASTFalse == ComputeFormulaUsingModel(*it))
593 FatalError("CheckCounterExample:counterexample bogus:"
594 "assert evaluates to FALSE under counterexample: "
595 "NOT OK",
596 *it);
597 }
598
599 // The smtlib ones don't have a query defined.
600 if ((bm->GetQuery() != ASTUndefined) &&
601 ASTTrue == ComputeFormulaUsingModel(bm->GetQuery()))
602 FatalError("CheckCounterExample:counterexample bogus:"
603 "query evaluates to TRUE under counterexample: "
604 "NOT OK",
605 bm->GetQuery());
606 }
607
608 /* FUNCTION: queries the value of expr given the current counterexample.
609 */
GetCounterExample(const ASTNode & expr)610 ASTNode AbsRefine_CounterExample::GetCounterExample(const ASTNode& expr)
611 {
612 // input is valid, no counterexample to get
613 if (bm->ValidFlag)
614 return ASTUndefined;
615
616 if (BOOLEAN_TYPE == expr.GetType())
617 {
618 return ComputeFormulaUsingModel(expr);
619 }
620
621 return TermToConstTermUsingModel(expr, false);
622 }
623
624 // FUNCTION: queries the counterexample, and returns the number of array
625 // locations for e
626 vector<std::pair<ASTNode, ASTNode>>
GetCounterExampleArray(bool t,const ASTNode & e)627 AbsRefine_CounterExample::GetCounterExampleArray(bool t, const ASTNode& e)
628 {
629 vector<std::pair<ASTNode, ASTNode>> entries;
630
631 // input is valid, no counterexample to print
632 if (bm->ValidFlag)
633 {
634 return entries;
635 }
636
637 // t is true if SAT solver generated a counterexample, else it is
638 // false
639 if (!t)
640 {
641 return entries;
642 }
643
644 // Take a copy of the counterexample map, 'cause TermToConstTermUsingModel
645 // changes it. Which breaks the iterator otherwise.
646 const ASTNodeMap c(CounterExampleMap);
647
648 ASTNodeMap::const_iterator it = c.begin();
649 ASTNodeMap::const_iterator itend = c.end();
650 for (; it != itend; it++)
651 {
652 const ASTNode& f = it->first;
653 const ASTNode& se = it->second;
654
655 if (ARRAY_TYPE == se.GetType())
656 {
657 FatalError("TermToConstTermUsingModel: "
658 "entry in counterexample is an arraytype. bogus:",
659 se);
660 }
661
662 // skip over introduced variables
663 if (f.GetKind() == SYMBOL && (bm->FoundIntroducedSymbolSet(f)))
664 {
665 continue;
666 }
667 if (f.GetKind() == READ && f[0] == e && f[0].GetKind() == SYMBOL &&
668 f[1].GetKind() == BVCONST)
669 {
670 ASTNode rhs;
671 if (BITVECTOR_TYPE == se.GetType())
672 {
673 rhs = TermToConstTermUsingModel(se, false);
674 }
675 else
676 {
677 rhs = ComputeFormulaUsingModel(se);
678 }
679 assert(rhs.isConstant());
680 entries.push_back(std::make_pair(f[1], rhs));
681 }
682 }
683
684 return entries;
685 }
686
687 // TODO printing of expressions.
688 // TODO move to printer file.
PrintSMTLIB2(std::ostream & os,const ASTNode & n)689 void AbsRefine_CounterExample::PrintSMTLIB2(std::ostream& os, const ASTNode& n)
690 {
691 if (n.GetKind() == SYMBOL)
692 {
693 os << "( ";
694
695 os << "|";
696 n.nodeprint(os);
697 os << "| ";
698
699 if (n.GetType() == stp::BITVECTOR_TYPE)
700 printer::outputBitVecSMTLIB2(TermToConstTermUsingModel(n, false), os);
701 else
702 {
703 if (ASTTrue == ComputeFormulaUsingModel(n))
704 os << "true";
705 else
706 os << "false";
707 }
708 os << " )";
709 }
710 }
711
PrintCounterExampleSMTLIB2(std::ostream & os)712 void AbsRefine_CounterExample::PrintCounterExampleSMTLIB2(std::ostream& os)
713 {
714 // Take a copy of the counterexample map, 'cause TermToConstTermUsingModel
715 // changes it. Which breaks the iterator otherwise.
716 const ASTNodeMap c(CounterExampleMap);
717
718 ASTNodeMap::const_iterator it = c.begin();
719 ASTNodeMap::const_iterator itend = c.end();
720 for (; it != itend; it++)
721 {
722 const ASTNode& f = it->first;
723 const ASTNode& se = it->second;
724
725 if (ARRAY_TYPE == se.GetType())
726 {
727 FatalError("PrintCounterExampleSMTLIB2: "
728 "entry in counterexample is an arraytype. bogus:",
729 se);
730 }
731
732 // skip over introduced variables
733 if (f.GetKind() == SYMBOL && (bm->FoundIntroducedSymbolSet(f)))
734 {
735 continue;
736 }
737
738 if (f.GetKind() == SYMBOL)
739 {
740 os << "( define-fun ";
741 os << "|";
742 f.nodeprint(os);
743 os << "|";
744
745 if (f.GetType() == stp::BITVECTOR_TYPE)
746 {
747 os << " () (";
748 os << "_ BitVec " << f.GetValueWidth() << ")";
749 printer::outputBitVecSMTLIB2(TermToConstTermUsingModel(se, false), os);
750 }
751 else if (f.GetType() == stp::BOOLEAN_TYPE)
752 {
753 os << " () Bool ";
754 }
755 else
756 {
757 FatalError("Wrong Type");
758 }
759
760 os << " )" << std::endl;
761 }
762
763 //TODO completely the wrong format.
764 if ((f.GetKind() == READ && f[0].GetKind() == SYMBOL &&
765 f[1].GetKind() == BVCONST))
766 {
767
768 os << "( define-fun ";
769
770 os << "|";
771 f[0].nodeprint(os);
772 os << "| ";
773
774 os << " (";
775 os << "_ BitVec " << f[0].GetIndexWidth() << ")";
776
777 os << " (";
778 os << "_ BitVec " << f[0].GetValueWidth() << ")";
779
780 printer::outputBitVecSMTLIB2(TermToConstTermUsingModel(f[1], false), os);
781
782 printer::outputBitVecSMTLIB2(TermToConstTermUsingModel(se, false), os);
783 os << " )" << endl;
784 }
785 }
786 os.flush();
787 }
788
789 // FUNCTION: prints a counterexample for INVALID inputs. iterate
790 // through the CounterExampleMap data structure and print it to
791 // stdout
PrintCounterExample(bool t,std::ostream & os)792 void AbsRefine_CounterExample::PrintCounterExample(bool t, std::ostream& os)
793 {
794 // input is valid, no counterexample to print
795 if (bm->ValidFlag)
796 {
797 return;
798 }
799
800 // if this option is true then print the way dawson wants using a
801 // different printer. do not use this printer.
802 if (bm->UserFlags.print_arrayval_declaredorder_flag)
803 {
804 return;
805 }
806
807 // t is true if SAT solver generated a counterexample, else it is
808 // false
809 if (!t)
810 {
811 os << "PrintCounterExample: No CounterExample to print: " << endl;
812 return;
813 }
814
815 bm->PLPrintNodeSet.clear();
816 bm->NodeLetVarMap.clear();
817 bm->NodeLetVarVec.clear();
818 bm->NodeLetVarMap1.clear();
819
820 // Take a copy of the counterexample map, 'cause TermToConstTermUsingModel
821 // changes it. Which breaks the iterator otherwise.
822 const ASTNodeMap c(CounterExampleMap);
823
824 ASTNodeMap::const_iterator it = c.begin();
825 ASTNodeMap::const_iterator itend = c.end();
826 for (; it != itend; it++)
827 {
828 const ASTNode& f = it->first;
829 const ASTNode& se = it->second;
830
831 if (ARRAY_TYPE == se.GetType())
832 {
833 FatalError("TermToConstTermUsingModel: "
834 "entry in counterexample is an arraytype. bogus:",
835 se);
836 }
837
838 // skip over introduced variables
839 if (f.GetKind() == SYMBOL && (bm->FoundIntroducedSymbolSet(f)))
840 {
841 continue;
842 }
843 if (f.GetKind() == SYMBOL ||
844 (f.GetKind() == READ && f[0].GetKind() == SYMBOL &&
845 f[1].GetKind() == BVCONST))
846 {
847
848 os << "ASSERT( ";
849
850 printer::PL_Print1(os, f, 0, false, bm);
851 if (BOOLEAN_TYPE == f.GetType())
852 {
853 os << "<=>";
854 }
855 else
856 {
857 os << " = ";
858 }
859
860 ASTNode rhs;
861 if (BITVECTOR_TYPE == se.GetType())
862 {
863 rhs = TermToConstTermUsingModel(se, false);
864 }
865 else
866 {
867 rhs = ComputeFormulaUsingModel(se);
868 }
869 assert(rhs.isConstant());
870 printer::PL_Print1(os, rhs, 0, false, bm);
871
872 os << " );" << endl;
873 }
874 }
875 }
876
877 /* iterate through the CounterExampleMap data structure and print it
878 * to stdout. this function prints only the declared array variables
879 * IN the ORDER in which they were declared. It also assumes that
880 * the variables are of the form 'varname_number'. otherwise it will
881 * not print anything. This function was specifically written for
882 * Dawson Engler's group (bug finding research group at Stanford)
883 */
PrintCounterExample_InOrder(bool t)884 void AbsRefine_CounterExample::PrintCounterExample_InOrder(bool t)
885 {
886 // global command-line option to print counterexample. we do not
887 // want both counterexample printers to print at the sametime.
888 // FIXME: This should always print the counterexample. If you want
889 // to turn it off, check the switch at the point of call.
890 if (bm->UserFlags.print_counterexample_flag)
891 return;
892
893 // input is valid, no counterexample to print
894 if (bm->ValidFlag)
895 return;
896
897 // print if the commandline option is '-q'. allows printing the
898 // counterexample in order.
899 if (!bm->UserFlags.print_arrayval_declaredorder_flag)
900 return;
901
902 // t is true if SAT solver generated a counterexample, else it is
903 // false
904 if (!t)
905 {
906 cerr << "PrintCounterExample: No CounterExample to print: " << endl;
907 return;
908 }
909
910 // vector to store the integer values
911 vector<int> out_int;
912 cout << "% ";
913 for (ASTVec::iterator it = bm->ListOfDeclaredVars.begin(),
914 itend = bm->ListOfDeclaredVars.end();
915 it != itend; it++)
916 {
917 if (ARRAY_TYPE == it->GetType())
918 {
919 // get the name of the variable
920 const char* c = it->GetName();
921 std::string ss(c);
922 if (!(0 == strncmp(ss.c_str(), "ini_", 4)))
923 continue;
924 reverse(ss.begin(), ss.end());
925
926 // cout << "debugging: " << ss;
927 size_t pos = ss.find('_', 0);
928 if (!((0 < pos) && (pos < ss.size())))
929 continue;
930
931 // get the associated length
932 std::string sss = ss.substr(0, pos);
933 reverse(sss.begin(), sss.end());
934 int n = atoi(sss.c_str());
935
936 it->PL_Print(cout, bm, 2);
937 for (int j = 0; j < n; j++)
938 {
939 ASTNode index = bm->CreateBVConst(it->GetIndexWidth(), j);
940 ASTNode readexpr =
941 bm->CreateTerm(READ, it->GetValueWidth(), *it, index);
942 ASTNode val = GetCounterExample(readexpr);
943 // cout << "ASSERT( ";
944 // cout << " = ";
945 out_int.push_back(val.GetUnsignedConst());
946 // cout << "\n";
947 }
948 }
949 }
950 cout << endl;
951 for (unsigned int jj = 0; jj < out_int.size(); jj++)
952 cout << out_int[jj] << endl;
953 cout << endl;
954 }
955
956 // Prints Satisfying assignment directly, for debugging.
PrintSATModel(SATSolver & newS,ToSATBase::ASTNodeToSATVar & m)957 void AbsRefine_CounterExample::PrintSATModel(SATSolver& newS,
958 ToSATBase::ASTNodeToSATVar& m)
959 {
960 if (!newS.okay())
961 FatalError("PrintSATModel: NO COUNTEREXAMPLE TO PRINT", ASTUndefined);
962 if (!(bm->UserFlags.stats_flag && bm->UserFlags.print_nodes_flag))
963 return;
964
965 cout << "Satisfying assignment: " << endl;
966 for (ToSATBase::ASTNodeToSATVar::const_iterator it = m.begin(); it != m.end();
967 it++)
968 {
969 ASTNode symbol = it->first;
970 vector<unsigned> v = it->second;
971
972 for (size_t i = 0; i < v.size(); i++)
973 {
974 if (v[i] == ~((unsigned)0)) // nb. special value.
975 continue;
976
977 if (newS.modelValue(v[i]) == newS.true_literal())
978 {
979 it->first.nodeprint(cout);
980 cout << " {" << i << "}" << endl;
981 }
982 else if (newS.modelValue(v[i]) == newS.false_literal())
983 {
984 cout << "NOT ";
985 it->first.nodeprint(cout);
986 cout << " {" << i << "}" << endl;
987 }
988 }
989 }
990 }
991
992 // FUNCTION: this function accepts a boolvector and returns a BVConst
BoolVectoBVConst(const vector<bool> * w,const unsigned int l)993 ASTNode AbsRefine_CounterExample::BoolVectoBVConst(const vector<bool>* w,
994 const unsigned int l)
995 {
996 assert(l == (unsigned)w->size());
997
998 CBV cc = CONSTANTBV::BitVector_Create(l, true);
999 for (unsigned int jj = 0; jj < l; jj++)
1000 {
1001 if ((*w)[jj] == true)
1002 CONSTANTBV::BitVector_Bit_On(cc, l - 1 - jj);
1003 }
1004
1005 return bm->CreateBVConst(cc, l);
1006 }
1007
CopySolverMap_To_CounterExample(void)1008 void AbsRefine_CounterExample::CopySolverMap_To_CounterExample(void)
1009 {
1010
1011 if (!simp->Return_SolverMap()->empty())
1012 {
1013 CounterExampleMap.insert(simp->Return_SolverMap()->begin(),
1014 simp->Return_SolverMap()->end());
1015 }
1016 }
1017
1018 SOLVER_RETURN_TYPE
CallSAT_ResultCheck(SATSolver & SatSolver,const ASTNode & modified_input,const ASTNode & original_input,ToSATBase * tosat,bool refinement)1019 AbsRefine_CounterExample::CallSAT_ResultCheck(SATSolver& SatSolver,
1020 const ASTNode& modified_input,
1021 const ASTNode& original_input,
1022 ToSATBase* tosat, bool refinement)
1023 {
1024 bool sat = tosat->CallSAT(SatSolver, modified_input, refinement);
1025
1026 if (bm->soft_timeout_expired)
1027 return SOLVER_TIMEOUT;
1028
1029 if (!sat)
1030 {
1031 return SOLVER_VALID;
1032 }
1033 else if (SatSolver.okay())
1034 {
1035 if (!bm->UserFlags.construct_counterexample_flag)
1036 return SOLVER_INVALID;
1037
1038 bm->GetRunTimes()->start(RunTimes::CounterExampleGeneration);
1039 CounterExampleMap.clear();
1040 ComputeFormulaMap.clear();
1041
1042 ToSAT::ASTNodeToSATVar satVarToSymbol = tosat->SATVar_to_SymbolIndexMap();
1043 ConstructCounterExample(SatSolver, satVarToSymbol);
1044 if (bm->UserFlags.stats_flag && bm->UserFlags.print_nodes_flag)
1045 {
1046 ToSAT::ASTNodeToSATVar m = tosat->SATVar_to_SymbolIndexMap();
1047 PrintSATModel(SatSolver, m);
1048 }
1049 // check if the counterexample is good or not
1050 ASTNode orig_result = ComputeFormulaUsingModel(original_input);
1051 if (!(ASTTrue == orig_result || ASTFalse == orig_result))
1052 FatalError("TopLevelSat: Original input must compute to "
1053 "true or false against model");
1054 bm->GetRunTimes()->stop(RunTimes::CounterExampleGeneration);
1055
1056 // if the counterexample is indeed a good one, then return
1057 // invalid
1058 if (ASTTrue == orig_result)
1059 {
1060 if (bm->UserFlags.check_counterexample_flag)
1061 {
1062 CheckCounterExample(SatSolver.okay());
1063 }
1064
1065 if (bm->UserFlags.stats_flag || bm->UserFlags.print_counterexample_flag)
1066 {
1067 PrintCounterExample(SatSolver.okay());
1068 PrintCounterExample_InOrder(SatSolver.okay());
1069 }
1070 return SOLVER_INVALID;
1071 }
1072 // counterexample is bogus: flag it
1073 else
1074 {
1075 if (bm->UserFlags.stats_flag && bm->UserFlags.print_nodes_flag)
1076 {
1077 cout << "Supposedly bogus one: \n";
1078 PrintCounterExample(true);
1079 }
1080
1081 return SOLVER_UNDECIDED;
1082 }
1083 }
1084 else
1085 {
1086 // Control should never reach here
1087 // PrintOutput(true);
1088 return SOLVER_ERROR;
1089 }
1090 }
1091 }
1092