1 /********************************************************************
2 * AUTHORS: Unknown
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/Simplifier/constantBitP/ConstantBitP_MaxPrecision.h"
26 #include "stp/AST/AST.h"
27 #include "stp/AbsRefineCounterExample/AbsRefine_CounterExample.h"
28 #include "stp/AbsRefineCounterExample/ArrayTransformer.h"
29 #include "stp/STPManager/STPManager.h"
30 #include "stp/Sat/MinisatCore.h"
31 #include "stp/Simplifier/Simplifier.h"
32 #include "stp/ToSat/AIG/BBNodeManagerAIG.h"
33 #include "stp/ToSat/AIG/ToSATAIG.h"
34 #include "stp/ToSat/ASTNode/ToSAT.h"
35 #include "stp/ToSat/BitBlaster.h"
36
37 using namespace stp;
38
39 namespace simplifier
40 {
41
42 namespace constantBitP
43 {
44
45 void print(const vector<FixedBits*> children, const FixedBits& output, Kind k);
46
47 //// Help node creation functions.
48
createConstant(int bitWidth,int val,STPMgr * beev)49 ASTNode createConstant(int bitWidth, int val, STPMgr* beev)
50 {
51 CBV cbv = CONSTANTBV::BitVector_Create(bitWidth, true);
52 int max = bitWidth > ((int)sizeof(int) * 8) ? sizeof(int) * 8 : bitWidth;
53 for (int i = 0; i < max; i++)
54 if (val & (1 << i))
55 CONSTANTBV::BitVector_Bit_On(cbv, i);
56 return beev->CreateBVConst(cbv, bitWidth);
57 }
58
createTerm(Kind k,int width,const ASTNode & n1,STPMgr * beev)59 ASTNode createTerm(Kind k, int width, const ASTNode& n1, STPMgr* beev)
60 {
61 ASTNode result = beev->CreateTerm(k, width, n1);
62 BVTypeCheck(result);
63 return result;
64 }
65
createTerm(Kind k,int width,const ASTNode & n1,const ASTNode & n2,STPMgr * beev)66 ASTNode createTerm(Kind k, int width, const ASTNode& n1, const ASTNode& n2,
67 STPMgr* beev)
68 {
69 ASTNode result = beev->CreateTerm(k, width, n1, n2);
70 BVTypeCheck(result);
71 return result;
72 }
73
createNode(Kind k,const ASTNode & n1,const ASTNode & n2,STPMgr * beev)74 ASTNode createNode(Kind k, const ASTNode& n1, const ASTNode& n2, STPMgr* beev)
75 {
76 ASTNode result = beev->CreateNode(k, n1, n2);
77 BVTypeCheck(result);
78 return result;
79 }
80
createTerm(Kind k,int width,const ASTNode & n1,const ASTNode & n2,const ASTNode & n3,STPMgr * beev)81 ASTNode createTerm(Kind k, int width, const ASTNode& n1, const ASTNode& n2,
82 const ASTNode& n3, STPMgr* beev)
83 {
84 ASTNode result = beev->CreateTerm(k, width, n1, n2, n3);
85 BVTypeCheck(result);
86 return result;
87 }
88
89 //////////////////////////////////////////////////
90
91 // Concretisation function. Gamma.
concretise(const ASTNode & variable,const FixedBits & fixed,ASTVec & list,STPMgr * beev)92 void concretise(const ASTNode& variable, const FixedBits& fixed, ASTVec& list,
93 STPMgr* beev)
94 {
95 if (BOOLEAN_TYPE == variable.GetType())
96 {
97 assert(1 == fixed.getWidth());
98 assert(fixed.isBoolean());
99
100 if (fixed.isFixed(0))
101 {
102 ASTNode assert;
103 if (!fixed.getValue(0)) // if it's false, try to find a true assignment.
104 assert = variable;
105 else
106 assert = beev->CreateNode(NOT, variable);
107 list.push_back(assert);
108 }
109 }
110 else
111 {
112 assert(BITVECTOR_TYPE == variable.GetType());
113 assert(variable.GetValueWidth() == (unsigned)fixed.getWidth());
114 for (unsigned i = 0; i < fixed.getWidth(); i++)
115 {
116 if (fixed.isFixed(i))
117 {
118 ASTNode oneOrZero =
119 createConstant(1, fixed.getValue(i) ? 0 : -1, beev); // NB: swapped.
120 ASTNode location = createConstant(32, i, beev);
121 ASTNode extract =
122 createTerm(BVEXTRACT, 1, variable, location, location, beev);
123 ASTNode assert = createNode(EQ, extract, oneOrZero, beev);
124 list.push_back(assert);
125 }
126 }
127 }
128 }
129
130 // Concretisation function. Gamma.
concretise(const ASTNode & variable,const FixedBits & fixed,SATSolver::vec_literals & satSolverClause,STPMgr *,ToSATBase::ASTNodeToSATVar & map)131 void concretise(const ASTNode& variable, const FixedBits& fixed,
132 SATSolver::vec_literals& satSolverClause, STPMgr* /*beev*/,
133 ToSATBase::ASTNodeToSATVar& map)
134 {
135 if (BOOLEAN_TYPE == variable.GetType())
136 {
137 assert(1 == fixed.getWidth());
138 assert(fixed.isBoolean());
139
140 if (fixed.isFixed(0))
141 {
142 if (!fixed.getValue(0)) // if it's false, try to find a true assignment.
143 {
144 assert(map.find(variable) != map.end());
145 int v = (map.find(variable)->second)[0];
146 satSolverClause.push(SATSolver::mkLit(v, false));
147 }
148 else
149 {
150 assert(map.find(variable) != map.end());
151 int v = (map.find(variable)->second)[0];
152 satSolverClause.push(SATSolver::mkLit(v, true));
153 }
154 }
155 }
156 else
157 {
158 assert(BITVECTOR_TYPE == variable.GetType());
159 assert(variable.GetValueWidth() == (unsigned)fixed.getWidth());
160 for (unsigned i = 0; i < fixed.getWidth(); i++)
161 {
162 if (fixed.isFixed(i))
163 {
164 assert(map.find(variable) != map.end());
165 int v = (map.find(variable)->second)[i];
166 satSolverClause.push(SATSolver::mkLit(v, fixed.getValue(i)));
167 }
168 }
169 }
170 }
171
172 // Concretisation function. Gamma.
concretiseB(const ASTNode & variable,const ASTNode & min,const ASTNode & max,ASTVec & list,STPMgr * beev)173 void concretiseB(const ASTNode& variable, const ASTNode& min,
174 const ASTNode& max, ASTVec& list, STPMgr* beev)
175 {
176 assert(min.isConstant());
177 assert(max.isConstant());
178
179 if (BOOLEAN_TYPE == variable.GetType())
180 {
181 assert(false); // not yet implemented.
182 }
183 else
184 {
185 assert(BITVECTOR_TYPE == variable.GetType());
186 ASTNode assert = createNode(BVLT, variable, min, beev);
187 list.push_back(assert);
188
189 assert = createNode(BVGT, variable, max, beev);
190 list.push_back(assert);
191 }
192 }
193
194 bool fix(FixedBits& a, const FixedBits& b, const int i);
195
196 Result fix(FixedBits& b, stp::CBV low, stp::CBV high);
197
198 // The bitWidth isn't necessarily the same for all children. e.g. ITE(boolean,
199 // x-bit, x-bit)
maxBoundsPrecision(vector<FixedBits * > children,FixedBits & output,Kind kind,STPMgr * beev)200 bool maxBoundsPrecision(vector<FixedBits*> children, FixedBits& output,
201 Kind kind, STPMgr* beev)
202 {
203 const int numberOfChildren = children.size();
204
205 bool disabledProp = !beev->UserFlags.bitConstantProp_flag;
206 bool printOutput = beev->UserFlags.print_output_flag;
207
208 beev->UserFlags.bitConstantProp_flag = false;
209 beev->UserFlags.print_output_flag = false;
210
211 ASTVec initialFixing;
212
213 // Create a variable to represent each input, and one for the output.
214 ASTVec variables;
215 for (int i = 0; i < numberOfChildren; i++)
216 {
217 std::stringstream out;
218 out << "v" << i;
219
220 unsigned valueWidth;
221
222 if (children[i]->isBoolean())
223 valueWidth = 0;
224 else
225 valueWidth = (children[i]->getWidth());
226
227 ASTNode node = beev->CreateSymbol(out.str().c_str(), 0, valueWidth);
228 variables.push_back(node);
229
230 // constrain the fixed bits of each input variable not to change.
231 concretise(node, *children[i], initialFixing, beev);
232 }
233
234 unsigned outputWidth = output.isBoolean() ? 0 : output.getWidth();
235 ASTNode outputNode = beev->CreateSymbol("result", 0, outputWidth);
236
237 ASTNode expr;
238 if (output.isBoolean())
239 {
240 ASTNode p1 = beev->CreateNode(kind, variables);
241 BVTypeCheck(p1);
242 expr = createNode(IFF, p1, outputNode, beev);
243 }
244 else
245 {
246 ASTNode p1 = beev->CreateTerm(kind, output.getWidth(), variables);
247 BVTypeCheck(p1);
248 expr = createNode(EQ, p1, outputNode, beev);
249 }
250
251 // constrain the input to equal the output.
252 BVTypeCheck(expr);
253
254 // constrain the fixed parts of the output node not to change.
255 concretise(outputNode, output, initialFixing, beev);
256
257 ASTVec notted;
258 for (ASTVec::const_iterator i = initialFixing.begin();
259 i != initialFixing.end(); i++)
260 notted.push_back(beev->CreateNode(NOT, *i));
261
262 if (notted.size() > 0) // some are specified.
263 {
264 expr = beev->CreateNode(stp::AND, expr, beev->CreateNode(stp::AND, notted));
265 }
266
267 bool first = true;
268 ASTVec ors;
269 ASTNode total = beev->ASTTrue;
270 Simplifier simp(beev);
271 ArrayTransformer at(beev, &simp);
272 AbsRefine_CounterExample ce(beev, &simp, &at);
273 ToSAT tosat(beev);
274 MinisatCore newS;
275
276 vector<ASTNode> min_children(children.size());
277 vector<ASTNode> max_children(children.size());
278 ASTNode min_output;
279 ASTNode max_output;
280
281 while (true)
282 {
283 ASTNode toSolve;
284
285 if (first)
286 {
287 toSolve = expr;
288 }
289 else
290 {
291 assert(ors.size() != 0);
292 if (ors.size() > 1)
293 toSolve = beev->CreateNode(stp::OR, ors);
294 else
295 toSolve = ors[0];
296 ors.clear();
297 }
298
299 BVTypeCheck(toSolve);
300
301 // Some operations aren't bitblasted directly. For example sbvmod is
302 // converted into
303 // other operations first.
304 // ArrayTransformer(STPMgr * bm, Simplifier* s, NodeFactory &nodeFactory_) :
305
306 toSolve = at.TransformFormula_TopLevel(toSolve);
307 total = beev->CreateNode(AND, total, toSolve);
308 int result = ce.CallSAT_ResultCheck(newS, total, total, &tosat, true);
309
310 if (2 == result)
311 FatalError("error from solver");
312 else if (1 == result)
313 {
314 break; // UNSAT use the last one..
315 }
316
317 if (first)
318 {
319 // Don't do the meet the first time through. Set the input and output.
320
321 for (int i = 0; i < numberOfChildren; i++)
322 {
323 ASTNode n = (ce.GetCounterExample(variables[i]));
324 min_children[i] = n;
325 max_children[i] = n;
326 concretiseB(variables[i], n, n, ors, beev);
327 }
328
329 ASTNode n = (ce.GetCounterExample(outputNode));
330 min_output = n;
331 max_output = n;
332 concretiseB(outputNode, n, n, ors, beev);
333 }
334 else
335 {
336 for (int i = 0; i < numberOfChildren; i++)
337 {
338 ASTNode n = (ce.GetCounterExample(variables[i]));
339 // cerr << variables[i].GetName() << " " << n << endl;
340 ASTNode t = beev->CreateNode(BVLT, n, min_children[i]);
341 if (beev->ASTTrue == NonMemberBVConstEvaluator(beev, t))
342 min_children[i] = n;
343 t = beev->CreateNode(BVGT, n, max_children[i]);
344 if (beev->ASTTrue == NonMemberBVConstEvaluator(beev, t))
345 max_children[i] = n;
346 concretiseB(variables[i], min_children[i], max_children[i], ors, beev);
347 }
348
349 ASTNode n = (ce.GetCounterExample(outputNode));
350 // cerr << variables[i].GetName() << " " << n << endl;
351 ASTNode t = beev->CreateNode(BVLT, n, min_output);
352 if (beev->ASTTrue == NonMemberBVConstEvaluator(beev, t))
353 min_output = n;
354 t = beev->CreateNode(BVGT, n, max_output);
355 if (beev->ASTTrue == NonMemberBVConstEvaluator(beev, t))
356 max_output = n;
357 concretiseB(outputNode, min_output, max_output, ors, beev);
358 }
359
360 first = false;
361
362 // print(children, output, kind);
363
364 if (0 == ors.size())
365 break; // everything is at top.
366
367 // beev->AddAssert(beev->CreateNode(stp::OR, ors));
368 }
369
370 if (!first)
371 {
372 for (int i = 0; i < numberOfChildren; i++)
373 {
374 simplifier::constantBitP::fix(*children[i], min_children[i].GetBVConst(),
375 max_children[i].GetBVConst());
376 }
377
378 simplifier::constantBitP::fix(output, min_output.GetBVConst(),
379 max_output.GetBVConst());
380 }
381
382 // beev->ClearSATTables();
383 // beev->ClearAllCaches();
384
385 // The first time we AddAsserts() it creates a new ASTVec to store them (on
386 // the heap).
387 beev->Pop();
388
389 beev->UserFlags.bitConstantProp_flag = !disabledProp;
390 beev->UserFlags.print_output_flag = printOutput;
391
392 return first;
393 }
394
395 // The bitWidth isn't necessarily the same for all children. e.g. ITE(boolean,
396 // x-bit, x-bit)
maxPrecision(vector<FixedBits * > children,FixedBits & output,Kind kind,STPMgr * beev)397 bool maxPrecision(vector<FixedBits*> children, FixedBits& output, Kind kind,
398 STPMgr* beev)
399 {
400 const int numberOfChildren = children.size();
401
402 bool disabledProp = !beev->UserFlags.bitConstantProp_flag;
403 bool printOutput = beev->UserFlags.print_output_flag;
404 bool checkCounter = beev->UserFlags.check_counterexample_flag;
405
406 beev->UserFlags.bitConstantProp_flag = false;
407 beev->UserFlags.print_output_flag = false;
408 beev->UserFlags.check_counterexample_flag = false;
409
410 ASTVec initialFixing;
411
412 // Create a variable to represent each input, and one for the output.
413 ASTVec variables;
414 for (int i = 0; i < numberOfChildren; i++)
415 {
416 std::stringstream out;
417 out << "v_VERY_SPECIALLY_NAMES" << i;
418
419 unsigned valueWidth;
420
421 if (children[i]->isBoolean())
422 valueWidth = 0;
423 else
424 valueWidth = (children[i]->getWidth());
425
426 ASTNode node = beev->CreateSymbol(out.str().c_str(), 0, valueWidth);
427 variables.push_back(node);
428
429 // constrain the fixed bits of each input variable not to change.
430 concretise(node, *children[i], initialFixing, beev);
431 }
432
433 unsigned outputWidth = output.isBoolean() ? 0 : output.getWidth();
434 ASTNode outputNode =
435 beev->CreateSymbol("result_WITH_SPECIAL_NAME", 0, outputWidth);
436
437 ASTNode expr;
438 if (output.isBoolean())
439 {
440 ASTNode p1 = beev->CreateNode(kind, variables);
441 BVTypeCheck(p1);
442 expr = createNode(IFF, p1, outputNode, beev);
443 }
444 else
445 {
446 ASTNode p1 = beev->CreateTerm(kind, output.getWidth(), variables);
447 BVTypeCheck(p1);
448 expr = createNode(EQ, p1, outputNode, beev);
449 }
450
451 // constrain the input to equal the output.
452 BVTypeCheck(expr);
453
454 // constrain the fixed parts of the output node not to change.
455 concretise(outputNode, output, initialFixing, beev);
456
457 ASTVec notted;
458 for (ASTVec::const_iterator i = initialFixing.begin();
459 i != initialFixing.end(); i++)
460 notted.push_back(beev->CreateNode(NOT, *i));
461
462 if (notted.size() > 0) // some are specified.
463 {
464 expr = beev->CreateNode(stp::AND, expr, beev->CreateNode(stp::AND, notted));
465 }
466
467 bool first = true;
468 Simplifier simp(beev);
469 ArrayTransformer at(beev, &simp);
470 AbsRefine_CounterExample ce(beev, &simp, &at);
471 MinisatCore newS;
472
473 ToSATAIG tosat(beev, &at);
474
475 SATSolver::vec_literals satSolverClause;
476
477 while (true)
478 {
479
480 int result;
481
482 if (first)
483 {
484 beev->SetQuery(beev->ASTUndefined);
485 result = ce.CallSAT_ResultCheck(newS, expr, expr, &tosat, true);
486 }
487 else
488 {
489 assert(satSolverClause.size() > 0);
490 newS.addClause(satSolverClause);
491 satSolverClause.clear();
492
493 beev->SetQuery(beev->ASTUndefined);
494 result = ce.CallSAT_ResultCheck(newS, beev->ASTTrue, beev->ASTTrue,
495 &tosat, true);
496 }
497
498 if (2 == result)
499 FatalError("error from solver");
500 else if (1 == result)
501 {
502 break; // UNSAT use the last one..
503 }
504
505 if (first)
506 {
507 // Don't do the meet the first time through. Set the input and output.
508
509 for (int i = 0; i < numberOfChildren; i++)
510 {
511 ASTNode n = (ce.GetCounterExample(variables[i]));
512 *children[i] = FixedBits::concreteToAbstract(n);
513 concretise(variables[i], *(children[i]), satSolverClause, beev,
514 tosat.SATVar_to_SymbolIndexMap());
515 }
516
517 ASTNode n = (ce.GetCounterExample(outputNode));
518 output = FixedBits::concreteToAbstract(n);
519 // cerr << resultNode.GetName() << " " << n << endl;
520 concretise(outputNode, output, satSolverClause, beev,
521 tosat.SATVar_to_SymbolIndexMap());
522 }
523 else
524 {
525 for (int i = 0; i < numberOfChildren; i++)
526 {
527 ASTNode n = (ce.GetCounterExample(variables[i]));
528 // cerr << variables[i].GetName() << " " << n << endl;
529 *children[i] =
530 FixedBits::meet(FixedBits::concreteToAbstract(n), *children[i]);
531 concretise(variables[i], *(children[i]), satSolverClause, beev,
532 tosat.SATVar_to_SymbolIndexMap());
533 }
534
535 ASTNode n = (ce.GetCounterExample(outputNode));
536 output = FixedBits::meet(FixedBits::concreteToAbstract(n), output);
537 // cerr << resultNode.GetName() << " " << n << endl;
538 concretise(outputNode, output, satSolverClause, beev,
539 tosat.SATVar_to_SymbolIndexMap());
540 }
541
542 first = false;
543
544 if (satSolverClause.size() == 0)
545 break; // everything is at top.
546 }
547
548 beev->UserFlags.bitConstantProp_flag = !disabledProp;
549 beev->UserFlags.print_output_flag = printOutput;
550 beev->UserFlags.check_counterexample_flag = checkCounter;
551
552 return first;
553 }
554 }
555 }
556