be657815fe789f4f50324ba23f07bb0a893845d6
[satune.git] / src / csolver.cc
1 #include "csolver.h"
2 #include "set.h"
3 #include "mutableset.h"
4 #include "element.h"
5 #include "boolean.h"
6 #include "predicate.h"
7 #include "order.h"
8 #include "table.h"
9 #include "function.h"
10 #include "satencoder.h"
11 #include "sattranslator.h"
12 #include "tunable.h"
13 #include "polarityassignment.h"
14 #include "decomposeordertransform.h"
15 #include "autotuner.h"
16 #include "astops.h"
17 #include "structs.h"
18 #include "orderresolver.h"
19 #include "integerencoding.h"
20 #include "qsort.h"
21 #include "preprocess.h"
22 #include "serializer.h"
23 #include "deserializer.h"
24 #include "encodinggraph.h"
25 #include "ordergraph.h"
26 #include "orderedge.h"
27 #include "orderanalysis.h"
28 #include <time.h>
29 #include <stdarg.h>
30
31 CSolver::CSolver() :
32         boolTrue(BooleanEdge(new BooleanConst(true))),
33         boolFalse(boolTrue.negate()),
34         unsat(false),
35         tuner(NULL),
36         elapsedTime(0)
37 {
38         satEncoder = new SATEncoder(this);
39 }
40
41 /** This function tears down the solver and the entire AST */
42
43 CSolver::~CSolver() {
44         //serialize();
45         uint size = allBooleans.getSize();
46         for (uint i = 0; i < size; i++) {
47                 delete allBooleans.get(i);
48         }
49
50         size = allSets.getSize();
51         for (uint i = 0; i < size; i++) {
52                 delete allSets.get(i);
53         }
54
55         size = allElements.getSize();
56         for (uint i = 0; i < size; i++) {
57                 Element *el = allElements.get(i);
58                 delete el;
59         }
60
61         size = allTables.getSize();
62         for (uint i = 0; i < size; i++) {
63                 delete allTables.get(i);
64         }
65
66         size = allPredicates.getSize();
67         for (uint i = 0; i < size; i++) {
68                 delete allPredicates.get(i);
69         }
70
71         size = allOrders.getSize();
72         for (uint i = 0; i < size; i++) {
73                 delete allOrders.get(i);
74         }
75         size = allFunctions.getSize();
76         for (uint i = 0; i < size; i++) {
77                 delete allFunctions.get(i);
78         }
79
80         delete boolTrue.getBoolean();
81         delete satEncoder;
82 }
83
84 void CSolver::resetSolver() {
85         //serialize();
86         uint size = allBooleans.getSize();
87         for (uint i = 0; i < size; i++) {
88                 delete allBooleans.get(i);
89         }
90
91         size = allSets.getSize();
92         for (uint i = 0; i < size; i++) {
93                 delete allSets.get(i);
94         }
95
96         size = allElements.getSize();
97         for (uint i = 0; i < size; i++) {
98                 Element *el = allElements.get(i);
99                 delete el;
100         }
101
102         size = allTables.getSize();
103         for (uint i = 0; i < size; i++) {
104                 delete allTables.get(i);
105         }
106
107         size = allPredicates.getSize();
108         for (uint i = 0; i < size; i++) {
109                 delete allPredicates.get(i);
110         }
111
112         size = allOrders.getSize();
113         for (uint i = 0; i < size; i++) {
114                 delete allOrders.get(i);
115         }
116         size = allFunctions.getSize();
117         for (uint i = 0; i < size; i++) {
118                 delete allFunctions.get(i);
119         }
120         delete boolTrue.getBoolean();
121         allBooleans.clear();
122         allSets.clear();
123         allElements.clear();
124         allTables.clear();
125         allPredicates.clear();
126         allOrders.clear();
127         allFunctions.clear();
128         constraints.reset();
129         activeOrders.reset();
130         boolMap.reset();
131         elemMap.reset();
132
133         boolTrue = BooleanEdge(new BooleanConst(true));
134         boolFalse = boolTrue.negate();
135         unsat = false;
136         elapsedTime = 0;
137         tuner = NULL;
138         satEncoder->resetSATEncoder();
139
140 }
141
142 CSolver *CSolver::clone() {
143         CSolver *copy = new CSolver();
144         CloneMap map;
145         SetIteratorBooleanEdge *it = getConstraints();
146         while (it->hasNext()) {
147                 BooleanEdge b = it->next();
148                 copy->addConstraint(cloneEdge(copy, &map, b));
149         }
150         delete it;
151         return copy;
152 }
153
154 CSolver *CSolver::deserialize(const char *file) {
155         model_print("deserializing ...\n");
156         Deserializer deserializer(file);
157         return deserializer.deserialize();
158 }
159
160 void CSolver::serialize() {
161         model_print("serializing ...\n");
162         char buffer[255];
163         long long nanotime = getTimeNano();
164         int numchars = sprintf(buffer, "DUMP%llu", nanotime);
165         Serializer serializer(buffer);
166         SetIteratorBooleanEdge *it = getConstraints();
167         while (it->hasNext()) {
168                 BooleanEdge b = it->next();
169                 serializeBooleanEdge(&serializer, b, true);
170         }
171         delete it;
172 }
173
174 Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
175         Set *set = new Set(type, elements, numelements);
176         allSets.push(set);
177         return set;
178 }
179
180 Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange) {
181         Set *set = new Set(type, lowrange, highrange);
182         allSets.push(set);
183         return set;
184 }
185
186 bool CSolver::itemExistInSet(Set *set, uint64_t item){
187         return set->exists(item);
188 }
189
190 VarType CSolver::getSetVarType(Set *set) {
191         return set->getType();
192 }
193
194 Element *CSolver::createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange) {
195         Set *s = createRangeSet(type, lowrange, highrange);
196         return getElementVar(s);
197 }
198
199 MutableSet *CSolver::createMutableSet(VarType type) {
200         MutableSet *set = new MutableSet(type);
201         allSets.push(set);
202         return set;
203 }
204
205 void CSolver::addItem(MutableSet *set, uint64_t element) {
206         set->addElementMSet(element);
207 }
208
209 uint64_t CSolver::createUniqueItem(MutableSet *set) {
210         uint64_t element = set->getNewUniqueItem();
211         set->addElementMSet(element);
212         return element;
213 }
214
215 void CSolver::finalizeMutableSet(MutableSet *set) {
216         set->finalize();
217 }
218
219 Element *CSolver::getElementVar(Set *set) {
220         Element *element = new ElementSet(set);
221         allElements.push(element);
222         return element;
223 }
224
225 Set *CSolver::getElementRange (Element *element) {
226         return element->getRange();
227 }
228
229
230 Element *CSolver::getElementConst(VarType type, uint64_t value) {
231         uint64_t array[] = {value};
232         Set *set = new Set(type, array, 1);
233         Element *element = new ElementConst(value, set);
234         Element *e = elemMap.get(element);
235         if (e == NULL) {
236                 allSets.push(set);
237                 allElements.push(element);
238                 elemMap.put(element, element);
239                 return element;
240         } else {
241                 delete set;
242                 delete element;
243                 return e;
244         }
245 }
246
247
248 Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) {
249         Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
250         Element *e = elemMap.get(element);
251         if (e == NULL) {
252                 element->updateParents();
253                 allElements.push(element);
254                 elemMap.put(element, element);
255                 return element;
256         } else {
257                 delete element;
258                 return e;
259         }
260 }
261
262 Function *CSolver::createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) {
263         Function *function = new FunctionOperator(op, domain, numDomain, range, overflowbehavior);
264         allFunctions.push(function);
265         return function;
266 }
267
268 Predicate *CSolver::createPredicateOperator(CompOp op, Set **domain, uint numDomain) {
269         Predicate *predicate = new PredicateOperator(op, domain,numDomain);
270         allPredicates.push(predicate);
271         return predicate;
272 }
273
274 Predicate *CSolver::createPredicateTable(Table *table, UndefinedBehavior behavior) {
275         Predicate *predicate = new PredicateTable(table, behavior);
276         allPredicates.push(predicate);
277         return predicate;
278 }
279
280 Table *CSolver::createTable(Set **domains, uint numDomain, Set *range) {
281         Table *table = new Table(domains,numDomain,range);
282         allTables.push(table);
283         return table;
284 }
285
286 Table *CSolver::createTableForPredicate(Set **domains, uint numDomain) {
287         return createTable(domains, numDomain, NULL);
288 }
289
290 void CSolver::addTableEntry(Table *table, uint64_t *inputs, uint inputSize, uint64_t result) {
291         table->addNewTableEntry(inputs, inputSize, result);
292 }
293
294 Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) {
295         Function *function = new FunctionTable(table, behavior);
296         allFunctions.push(function);
297         return function;
298 }
299
300 BooleanEdge CSolver::getBooleanVar(VarType type) {
301         Boolean *boolean = new BooleanVar(type);
302         allBooleans.push(boolean);
303         return BooleanEdge(boolean);
304 }
305
306 BooleanEdge CSolver::getBooleanTrue() {
307         return boolTrue;
308 }
309
310 BooleanEdge CSolver::getBooleanFalse() {
311         return boolFalse;
312 }
313
314 BooleanEdge CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) {
315         return applyPredicateTable(predicate, inputs, numInputs, BooleanEdge(NULL));
316 }
317
318 BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, BooleanEdge undefinedStatus) {
319         BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
320         Boolean *b = boolMap.get(boolean);
321         if (b == NULL) {
322                 boolean->updateParents();
323                 boolMap.put(boolean, boolean);
324                 allBooleans.push(boolean);
325                 return BooleanEdge(boolean);
326         } else {
327                 delete boolean;
328                 return BooleanEdge(b);
329         }
330 }
331
332 bool CSolver::isTrue(BooleanEdge b) {
333         return b.isNegated() ? b->isFalse() : b->isTrue();
334 }
335
336 bool CSolver::isFalse(BooleanEdge b) {
337         return b.isNegated() ? b->isTrue() : b->isFalse();
338 }
339
340 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2) {
341         BooleanEdge array[] = {arg1, arg2};
342         return applyLogicalOperation(op, array, 2);
343 }
344
345 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg) {
346         BooleanEdge array[] = {arg};
347         return applyLogicalOperation(op, array, 1);
348 }
349
350 static int ptrcompares(const void *p1, const void *p2) {
351         uintptr_t b1 = *(uintptr_t const *) p1;
352         uintptr_t b2 = *(uintptr_t const *) p2;
353         if (b1 < b2)
354                 return -1;
355         else if (b1 == b2)
356                 return 0;
357         else
358                 return 1;
359 }
360
361 BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
362         BooleanEdge newarray[asize];
363         memcpy(newarray, array, asize * sizeof(BooleanEdge));
364         for (uint i = 0; i < asize; i++) {
365                 BooleanEdge b = newarray[i];
366                 if (b->type == LOGICOP) {
367                         if (((BooleanLogic *) b.getBoolean())->replaced) {
368                                 newarray[i] = doRewrite(newarray[i]);
369                                 i--;//Check again
370                         }
371                 }
372         }
373         return applyLogicalOperation(op, newarray, asize);
374 }
375
376 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
377         BooleanEdge newarray[asize];
378         switch (op) {
379         case SATC_NOT: {
380                 return array[0].negate();
381         }
382         case SATC_IFF: {
383                 for (uint i = 0; i < 2; i++) {
384                         if (isTrue(array[i])) { // It can be undefined
385                                 return array[1 - i];
386                         } else if (isFalse(array[i])) {
387                                 newarray[0] = array[1 - i];
388                                 return applyLogicalOperation(SATC_NOT, newarray, 1);
389                         } else if (array[i]->type == LOGICOP) {
390                                 BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
391                                 if (b->replaced) {
392                                         return rewriteLogicalOperation(op, array, asize);
393                                 }
394                         }
395                 }
396                 break;
397         }
398         case SATC_OR: {
399                 for (uint i = 0; i < asize; i++) {
400                         newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);
401                 }
402                 return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize));
403         }
404         case SATC_AND: {
405                 uint newindex = 0;
406                 for (uint i = 0; i < asize; i++) {
407                         BooleanEdge b = array[i];
408                         if (b->type == LOGICOP) {
409                                 if (((BooleanLogic *)b.getBoolean())->replaced)
410                                         return rewriteLogicalOperation(op, array, asize);
411                         }
412                         if (isTrue(b))
413                                 continue;
414                         else if (isFalse(b)) {
415                                 return boolFalse;
416                         } else
417                                 newarray[newindex++] = b;
418                 }
419                 if (newindex == 0) {
420                         return boolTrue;
421                 } else if (newindex == 1) {
422                         return newarray[0];
423                 } else {
424                         bsdqsort(newarray, newindex, sizeof(BooleanEdge), ptrcompares);
425                         array = newarray;
426                         asize = newindex;
427                 }
428                 break;
429         }
430         case SATC_XOR: {
431                 //handle by translation
432                 return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_IFF, array, asize));
433         }
434         case SATC_IMPLIES: {
435                 //handle by translation
436                 return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
437         }
438         }
439
440         ASSERT(asize != 0);
441         Boolean *boolean = new BooleanLogic(this, op, array, asize);
442         Boolean *b = boolMap.get(boolean);
443         if (b == NULL) {
444                 boolean->updateParents();
445                 boolMap.put(boolean, boolean);
446                 allBooleans.push(boolean);
447                 return BooleanEdge(boolean);
448         } else {
449                 delete boolean;
450                 return BooleanEdge(b);
451         }
452 }
453
454 BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
455         //      ASSERT(first != second);
456         if (first == second)
457                 return getBooleanFalse();
458
459         bool negate = false;
460         if (order->type == SATC_TOTAL) {
461                 if (first > second) {
462                         uint64_t tmp = first;
463                         first = second;
464                         second = tmp;
465                         negate = true;
466                 }
467         }
468         Boolean *constraint = new BooleanOrder(order, first, second);
469         Boolean *b = boolMap.get(constraint);
470
471         if (b == NULL) {
472                 allBooleans.push(constraint);
473                 boolMap.put(constraint, constraint);
474                 constraint->updateParents();
475                 if (order->graph != NULL) {
476                         OrderGraph *graph = order->graph;
477                         OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
478                         if (from != NULL) {
479                                 OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
480                                 if (to != NULL) {
481                                         OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
482                                         OrderEdge *invedge;
483
484                                         if (edge != NULL && edge->mustPos) {
485                                                 replaceBooleanWithTrueNoRemove(constraint);
486                                         } else if (edge != NULL && edge->mustNeg) {
487                                                 replaceBooleanWithFalseNoRemove(constraint);
488                                         } else if ((invedge = graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
489                                                                                  && invedge->mustPos) {
490                                                 replaceBooleanWithFalseNoRemove(constraint);
491                                         }
492                                 }
493                         }
494                 }
495         } else {
496                 delete constraint;
497                 constraint = b;
498         }
499
500         BooleanEdge be = BooleanEdge(constraint);
501         return negate ? be.negate() : be;
502 }
503
504 void CSolver::addConstraint(BooleanEdge constraint) {
505         if (isTrue(constraint))
506                 return;
507         else if (isFalse(constraint)) {
508                 int t = 0;
509                 setUnSAT();
510         }
511         else {
512                 if (constraint->type == LOGICOP) {
513                         BooleanLogic *b = (BooleanLogic *) constraint.getBoolean();
514                         if (!constraint.isNegated()) {
515                                 if (b->op == SATC_AND) {
516                                         for (uint i = 0; i < b->inputs.getSize(); i++) {
517                                                 addConstraint(b->inputs.get(i));
518                                         }
519                                         return;
520                                 }
521                         }
522                         if (b->replaced) {
523                                 addConstraint(doRewrite(constraint));
524                                 return;
525                         }
526                 }
527                 constraints.add(constraint);
528                 Boolean *ptr = constraint.getBoolean();
529
530                 if (ptr->boolVal == BV_UNSAT) {
531                         setUnSAT();
532                 }
533
534                 replaceBooleanWithTrueNoRemove(constraint);
535                 constraint->parents.clear();
536         }
537 }
538
539 Order *CSolver::createOrder(OrderType type, Set *set) {
540         Order *order = new Order(type, set);
541         allOrders.push(order);
542         activeOrders.add(order);
543         return order;
544 }
545
546 /** Computes static ordering information to allow isTrue/isFalse
547     queries on newly created orders to work. */
548
549 void CSolver::inferFixedOrder(Order *order) {
550         if (order->graph != NULL) {
551                 delete order->graph;
552         }
553         order->graph = buildMustOrderGraph(order);
554         reachMustAnalysis(this, order->graph, true);
555 }
556
557 void CSolver::inferFixedOrders() {
558         SetIteratorOrder *orderit = activeOrders.iterator();
559         while (orderit->hasNext()) {
560                 Order *order = orderit->next();
561                 inferFixedOrder(order);
562         }
563 }
564
565 #define NANOSEC 1000000000.0
566 int CSolver::solve() {
567         long long starttime = getTimeNano();
568         bool deleteTuner = false;
569         if (tuner == NULL) {
570                 tuner = new DefaultTuner();
571                 deleteTuner = true;
572         }
573
574
575         {
576                 SetIteratorOrder *orderit = activeOrders.iterator();
577                 while (orderit->hasNext()) {
578                         Order *order = orderit->next();
579                         if (order->graph != NULL) {
580                                 delete order->graph;
581                                 order->graph = NULL;
582                         }
583                 }
584                 delete orderit;
585         }
586         model_print("*****************Before any modifications:************\n");
587         printConstraints();
588         computePolarities(this);
589         long long time2 = getTimeNano();
590         model_print("Polarity time: %f\n", (time2 - starttime) / NANOSEC);
591 //      Preprocess pp(this);
592 //      pp.doTransform();
593         long long time3 = getTimeNano();
594 //      model_print("Preprocess time: %f\n", (time3 - time2) / NANOSEC);
595
596         DecomposeOrderTransform dot(this);
597         dot.doTransform();
598         long long time4 = getTimeNano();
599         model_print("Decompose Order: %f\n", (time4 - time3) / NANOSEC);
600
601         IntegerEncodingTransform iet(this);
602         iet.doTransform();
603
604         EncodingGraph eg(this);
605         eg.buildGraph();
606         eg.encode();
607
608         naiveEncodingDecision(this);
609         long long time5 = getTimeNano();
610         model_print("Encoding Graph Time: %f\n", (time5 - time4) / NANOSEC);
611
612         long long startTime = getTimeNano();
613         satEncoder->encodeAllSATEncoder(this);
614         long long endTime = getTimeNano();
615
616         elapsedTime = endTime - startTime;
617         model_print("Elapse Encode time: %f\n", elapsedTime / NANOSEC);
618
619         model_print("Is problem UNSAT after encoding: %d\n", unsat);
620         model_print("########## After all modifications: #############\n");
621         printConstraints();
622         int result = unsat ? IS_UNSAT : satEncoder->solve();
623         model_print("Result Computed in CSolver: %d\n", result);
624
625         if (deleteTuner) {
626                 delete tuner;
627                 tuner = NULL;
628         }
629         return result;
630 }
631
632 void CSolver::printConstraints() {
633         SetIteratorBooleanEdge *it = getConstraints();
634         while (it->hasNext()) {
635                 BooleanEdge b = it->next();
636                 if (b.isNegated())
637                         model_print("!");
638                 b->print();
639                 model_print("\n");
640         }
641         delete it;
642 }
643
644 void CSolver::printConstraint(BooleanEdge b) {
645         if (b.isNegated())
646                 model_print("!");
647         b->print();
648         model_print("\n");
649 }
650
651 uint64_t CSolver::getElementValue(Element *element) {
652         switch (element->type) {
653         case ELEMSET:
654         case ELEMCONST:
655         case ELEMFUNCRETURN:
656                 return getElementValueSATTranslator(this, element);
657         default:
658                 ASSERT(0);
659         }
660         exit(-1);
661 }
662
663 bool CSolver::getBooleanValue(BooleanEdge bedge) {
664         Boolean *boolean = bedge.getBoolean();
665         switch (boolean->type) {
666         case BOOLEANVAR:
667                 return getBooleanVariableValueSATTranslator(this, boolean);
668         default:
669                 ASSERT(0);
670         }
671         exit(-1);
672 }
673
674 bool CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) {
675         return order->encoding.resolver->resolveOrder(first, second);
676 }
677
678 long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); }
679
680 long long CSolver::getSolveTime() { return satEncoder->getSolveTime(); }
681
682 void CSolver::autoTune(uint budget) {
683         AutoTuner *autotuner = new AutoTuner(budget);
684         autotuner->addProblem(this);
685         autotuner->tune();
686         delete autotuner;
687 }
688
689 //Set* CSolver::addItemsToRange(Element* element, uint num, ...){
690 //        va_list args;
691 //        va_start(args, num);
692 //        element->getRange()
693 //        uint setSize = set->getSize();
694 //        uint newSize = setSize+ num;
695 //        uint64_t members[newSize];
696 //        for(uint i=0; i<setSize; i++){
697 //                members[i] = set->getElement(i);
698 //        }
699 //        for( uint i=0; i< num; i++){
700 //                uint64_t arg = va_arg(args, uint64_t);
701 //                members[setSize+i] = arg;
702 //        }
703 //        va_end(args);
704 //        return createSet(set->getType(), members, newSize);
705 //}