Merging + fixing memory bugs
[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 "elementopt.h"
29 #include "varorderingopt.h"
30 #include <time.h>
31 #include <stdarg.h>
32 #include "alloyinterpreter.h"
33 #include "smtinterpreter.h"
34 #include "mathsatinterpreter.h"
35 #include "smtratinterpreter.h"
36
37 CSolver::CSolver() :
38         boolTrue(BooleanEdge(new BooleanConst(true))),
39         boolFalse(boolTrue.negate()),
40         unsat(false),
41         booleanVarUsed(false),
42         incrementalMode(false),
43         optimizationsOff(false),
44         tuner(NULL),
45         elapsedTime(0),
46         satsolverTimeout(NOTIMEOUT),
47         interpreter(NULL)
48 {
49         satEncoder = new SATEncoder(this);
50 }
51
52 /** This function tears down the solver and the entire AST */
53
54 CSolver::~CSolver() {
55         //serialize();
56         uint size = allBooleans.getSize();
57         for (uint i = 0; i < size; i++) {
58                 delete allBooleans.get(i);
59         }
60
61         size = allSets.getSize();
62         for (uint i = 0; i < size; i++) {
63                 delete allSets.get(i);
64         }
65
66         size = allElements.getSize();
67         for (uint i = 0; i < size; i++) {
68                 Element *el = allElements.get(i);
69                 delete el;
70         }
71
72         size = allTables.getSize();
73         for (uint i = 0; i < size; i++) {
74                 delete allTables.get(i);
75         }
76
77         size = allPredicates.getSize();
78         for (uint i = 0; i < size; i++) {
79                 delete allPredicates.get(i);
80         }
81
82         size = allOrders.getSize();
83         for (uint i = 0; i < size; i++) {
84                 delete allOrders.get(i);
85         }
86         size = allFunctions.getSize();
87         for (uint i = 0; i < size; i++) {
88                 delete allFunctions.get(i);
89         }
90
91         if (interpreter != NULL) {
92                 delete interpreter;
93         }
94
95         delete boolTrue.getBoolean();
96         delete satEncoder;
97 }
98
99 void CSolver::resetSolver() {
100         //serialize();
101         uint size = allBooleans.getSize();
102         for (uint i = 0; i < size; i++) {
103                 delete allBooleans.get(i);
104         }
105
106         size = allSets.getSize();
107         for (uint i = 0; i < size; i++) {
108                 delete allSets.get(i);
109         }
110
111         size = allElements.getSize();
112         for (uint i = 0; i < size; i++) {
113                 Element *el = allElements.get(i);
114                 delete el;
115         }
116
117         size = allTables.getSize();
118         for (uint i = 0; i < size; i++) {
119                 delete allTables.get(i);
120         }
121
122         size = allPredicates.getSize();
123         for (uint i = 0; i < size; i++) {
124                 delete allPredicates.get(i);
125         }
126
127         size = allOrders.getSize();
128         for (uint i = 0; i < size; i++) {
129                 delete allOrders.get(i);
130         }
131         size = allFunctions.getSize();
132         for (uint i = 0; i < size; i++) {
133                 delete allFunctions.get(i);
134         }
135         delete boolTrue.getBoolean();
136         allBooleans.clear();
137         allSets.clear();
138         allElements.clear();
139         allTables.clear();
140         allPredicates.clear();
141         allOrders.clear();
142         allFunctions.clear();
143         constraints.reset();
144         encodedConstraints.reset();
145         activeOrders.reset();
146         boolMap.reset();
147         elemMap.reset();
148
149         boolTrue = BooleanEdge(new BooleanConst(true));
150         boolFalse = boolTrue.negate();
151         unsat = false;
152         booleanVarUsed = false;
153         elapsedTime = 0;
154         tuner = NULL;
155         satEncoder->resetSATEncoder();
156
157 }
158
159 CSolver *CSolver::clone() {
160         CSolver *copy = new CSolver();
161         CloneMap map;
162         SetIteratorBooleanEdge *it = getConstraints();
163         while (it->hasNext()) {
164                 BooleanEdge b = it->next();
165                 copy->addConstraint(cloneEdge(copy, &map, b));
166         }
167         delete it;
168         return copy;
169 }
170
171 CSolver *CSolver::deserialize(const char *file, InterpreterType itype) {
172         model_print("deserializing %s ...\n", file);
173         Deserializer deserializer(file, itype);
174         return deserializer.deserialize();
175 }
176
177 void CSolver::serialize() {
178         model_print("serializing ...\n");
179         char buffer[255];
180         long long nanotime = getTimeNano();
181         int numchars = sprintf(buffer, "DUMP%llu", nanotime);
182         Serializer serializer(buffer);
183         SetIteratorBooleanEdge *it = getConstraints();
184         while (it->hasNext()) {
185                 BooleanEdge b = it->next();
186                 serializeBooleanEdge(&serializer, b, true);
187         }
188         delete it;
189 }
190
191 Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
192         Set *set = new Set(type, elements, numelements);
193         allSets.push(set);
194         return set;
195 }
196
197 Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange) {
198         Set *set = new Set(type, lowrange, highrange);
199         allSets.push(set);
200         return set;
201 }
202
203 bool CSolver::itemExistInSet(Set *set, uint64_t item) {
204         return set->exists(item);
205 }
206
207 VarType CSolver::getSetVarType(Set *set) {
208         return set->getType();
209 }
210
211 Element *CSolver::createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange) {
212         Set *s = createRangeSet(type, lowrange, highrange);
213         return getElementVar(s);
214 }
215
216 MutableSet *CSolver::createMutableSet(VarType type) {
217         MutableSet *set = new MutableSet(type);
218         allSets.push(set);
219         return set;
220 }
221
222 void CSolver::addItem(MutableSet *set, uint64_t element) {
223         set->addElementMSet(element);
224 }
225
226 uint64_t CSolver::createUniqueItem(MutableSet *set) {
227         uint64_t element = set->getNewUniqueItem();
228         set->addElementMSet(element);
229         return element;
230 }
231
232 void CSolver::finalizeMutableSet(MutableSet *set) {
233         set->finalize();
234 }
235
236 Element *CSolver::getElementVar(Set *set) {
237         Element *element = new ElementSet(set);
238         allElements.push(element);
239         return element;
240 }
241
242 void CSolver::mustHaveValue(Element *element) {
243         element->anyValue = true;
244 }
245
246 void CSolver::freezeElementsVariables() {
247
248         for (uint i = 0; i < allElements.getSize(); i++) {
249                 Element *e = allElements.get(i);
250                 if (e->frozen) {
251                         satEncoder->freezeElementVariables(&e->encoding);
252                 }
253         }
254 }
255
256
257 Set *CSolver::getElementRange (Element *element) {
258         return element->getRange();
259 }
260
261
262 Element *CSolver::getElementConst(VarType type, uint64_t value) {
263         uint64_t array[] = {value};
264         Set *set = new Set(type, array, 1);
265         Element *element = new ElementConst(value, set);
266         Element *e = elemMap.get(element);
267         if (e == NULL) {
268                 allSets.push(set);
269                 allElements.push(element);
270                 elemMap.put(element, element);
271                 return element;
272         } else {
273                 delete set;
274                 delete element;
275                 return e;
276         }
277 }
278
279
280 Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) {
281         Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
282         Element *e = elemMap.get(element);
283         if (e == NULL) {
284                 element->updateParents();
285                 allElements.push(element);
286                 elemMap.put(element, element);
287                 return element;
288         } else {
289                 delete element;
290                 return e;
291         }
292 }
293
294 Function *CSolver::createFunctionOperator(ArithOp op, Set *range, OverFlowBehavior overflowbehavior) {
295         Function *function = new FunctionOperator(op, range, overflowbehavior);
296         allFunctions.push(function);
297         return function;
298 }
299
300 Predicate *CSolver::createPredicateOperator(CompOp op) {
301         Predicate *predicate = new PredicateOperator(op);
302         allPredicates.push(predicate);
303         return predicate;
304 }
305
306 Predicate *CSolver::createPredicateTable(Table *table, UndefinedBehavior behavior) {
307         Predicate *predicate = new PredicateTable(table, behavior);
308         allPredicates.push(predicate);
309         return predicate;
310 }
311
312 Table *CSolver::createTable(Set *range) {
313         Table *table = new Table(range);
314         allTables.push(table);
315         return table;
316 }
317
318 Table *CSolver::createTableForPredicate() {
319         return createTable(NULL);
320 }
321
322 void CSolver::addTableEntry(Table *table, uint64_t *inputs, uint inputSize, uint64_t result) {
323         table->addNewTableEntry(inputs, inputSize, result);
324 }
325
326 Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) {
327         Function *function = new FunctionTable(table, behavior);
328         allFunctions.push(function);
329         return function;
330 }
331
332 BooleanEdge CSolver::getBooleanVar(VarType type) {
333         Boolean *boolean = new BooleanVar(type);
334         allBooleans.push(boolean);
335         if (!booleanVarUsed)
336                 booleanVarUsed = true;
337         return BooleanEdge(boolean);
338 }
339
340 BooleanEdge CSolver::getBooleanTrue() {
341         return boolTrue;
342 }
343
344 BooleanEdge CSolver::getBooleanFalse() {
345         return boolFalse;
346 }
347
348 BooleanEdge CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) {
349         return applyPredicateTable(predicate, inputs, numInputs, BooleanEdge(NULL));
350 }
351
352 BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, BooleanEdge undefinedStatus) {
353         BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
354         Boolean *b = boolMap.get(boolean);
355         if (b == NULL) {
356                 boolean->updateParents();
357                 boolMap.put(boolean, boolean);
358                 allBooleans.push(boolean);
359                 return BooleanEdge(boolean);
360         } else {
361                 delete boolean;
362                 return BooleanEdge(b);
363         }
364 }
365
366 bool CSolver::isTrue(BooleanEdge b) {
367         return b.isNegated() ? b->isFalse() : b->isTrue();
368 }
369
370 bool CSolver::isFalse(BooleanEdge b) {
371         return b.isNegated() ? b->isTrue() : b->isFalse();
372 }
373
374 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2) {
375         BooleanEdge array[] = {arg1, arg2};
376         return applyLogicalOperation(op, array, 2);
377 }
378
379 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg) {
380         BooleanEdge array[] = {arg};
381         return applyLogicalOperation(op, array, 1);
382 }
383
384 static int booleanEdgeCompares(const void *p1, const void *p2) {
385         BooleanEdge be1 = *(BooleanEdge const *) p1;
386         BooleanEdge be2 = *(BooleanEdge const *) p2;
387         uint64_t b1 = be1->id;
388         uint64_t b2 = be2->id;
389         if (b1 < b2)
390                 return -1;
391         else if (b1 == b2)
392                 return 0;
393         else
394                 return 1;
395 }
396
397 BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
398         BooleanEdge newarray[asize];
399         memcpy(newarray, array, asize * sizeof(BooleanEdge));
400         for (uint i = 0; i < asize; i++) {
401                 BooleanEdge b = newarray[i];
402                 if (b->type == LOGICOP) {
403                         if (((BooleanLogic *) b.getBoolean())->replaced) {
404                                 newarray[i] = doRewrite(newarray[i]);
405                                 i--;//Check again
406                         }
407                 }
408         }
409         return applyLogicalOperation(op, newarray, asize);
410 }
411
412 BooleanEdge CSolver::applyExactlyOneConstraint (BooleanEdge *array, uint asize) {
413         BooleanEdge newarray[asize + 1];
414
415         newarray[asize] = applyLogicalOperation(SATC_OR, array, asize);
416         for (uint i = 0; i < asize; i++) {
417                 BooleanEdge oprand1 = array[i];
418                 BooleanEdge carray [asize - 1];
419                 uint index = 0;
420                 for ( uint j = 0; j < asize; j++) {
421                         if (i != j) {
422                                 BooleanEdge oprand2 = applyLogicalOperation(SATC_NOT, array[j]);
423                                 carray[index++] = applyLogicalOperation(SATC_IMPLIES, oprand1, oprand2);
424                         }
425                 }
426                 ASSERT(index == asize - 1);
427                 newarray[i] = applyLogicalOperation(SATC_AND, carray, asize - 1);
428         }
429         return applyLogicalOperation(SATC_AND, newarray, asize + 1);
430 }
431
432 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
433         if (!useInterpreter()) {
434                 BooleanEdge newarray[asize];
435                 switch (op) {
436                 case SATC_NOT: {
437                         return array[0].negate();
438                 }
439                 case SATC_IFF: {
440                         for (uint i = 0; i < 2; i++) {
441                                 if (isTrue(array[i])) { // It can be undefined
442                                         return array[1 - i];
443                                 } else if (isFalse(array[i])) {
444                                         newarray[0] = array[1 - i];
445                                         return applyLogicalOperation(SATC_NOT, newarray, 1);
446                                 } else if (array[i]->type == LOGICOP) {
447                                         BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
448                                         if (b->replaced) {
449                                                 return rewriteLogicalOperation(op, array, asize);
450                                         }
451                                 }
452                         }
453                         break;
454                 }
455                 case SATC_OR: {
456                         for (uint i = 0; i < asize; i++) {
457                                 newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);
458                         }
459                         return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize));
460                 }
461                 case SATC_AND: {
462                         uint newindex = 0;
463                         for (uint i = 0; i < asize; i++) {
464                                 BooleanEdge b = array[i];
465                                 if (b->type == LOGICOP) {
466                                         if (((BooleanLogic *)b.getBoolean())->replaced)
467                                                 return rewriteLogicalOperation(op, array, asize);
468                                 }
469                                 if (isTrue(b))
470                                         continue;
471                                 else if (isFalse(b)) {
472                                         return boolFalse;
473                                 } else
474                                         newarray[newindex++] = b;
475                         }
476                         if (newindex == 0) {
477                                 return boolTrue;
478                         } else if (newindex == 1) {
479                                 return newarray[0];
480                         } else {
481                                 bsdqsort(newarray, newindex, sizeof(BooleanEdge), booleanEdgeCompares);
482                                 array = newarray;
483                                 asize = newindex;
484                         }
485                         break;
486                 }
487                 case SATC_XOR: {
488                         //handle by translation
489                         return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_IFF, array, asize));
490                 }
491                 case SATC_IMPLIES: {
492                         //handle by translation
493                         return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
494                 }
495                 }
496
497                 ASSERT(asize != 0);
498                 Boolean *boolean = new BooleanLogic(this, op, array, asize);
499                 Boolean *b = boolMap.get(boolean);
500                 if (b == NULL) {
501                         boolean->updateParents();
502                         boolMap.put(boolean, boolean);
503                         allBooleans.push(boolean);
504                         return BooleanEdge(boolean);
505                 } else {
506                         delete boolean;
507                         return BooleanEdge(b);
508                 }
509         } else {
510                 ASSERT(asize != 0);
511                 Boolean *boolean = new BooleanLogic(this, op, array, asize);
512                 allBooleans.push(boolean);
513                 return BooleanEdge(boolean);
514
515         }
516 }
517
518 BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
519         //      ASSERT(first != second);
520         if (first == second)
521                 return getBooleanFalse();
522
523         bool negate = false;
524         if (order->type == SATC_TOTAL) {
525                 if (first > second) {
526                         uint64_t tmp = first;
527                         first = second;
528                         second = tmp;
529                         negate = true;
530                 }
531         }
532         Boolean *constraint = new BooleanOrder(order, first, second);
533         if (!useInterpreter() ) {
534                 Boolean *b = boolMap.get(constraint);
535
536                 if (b == NULL) {
537                         allBooleans.push(constraint);
538                         boolMap.put(constraint, constraint);
539                         constraint->updateParents();
540                         if ( order->graph != NULL) {
541                                 OrderGraph *graph = order->graph;
542                                 OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
543                                 if (from != NULL) {
544                                         OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
545                                         if (to != NULL) {
546                                                 OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
547                                                 OrderEdge *invedge;
548
549                                                 if (edge != NULL && edge->mustPos) {
550                                                         replaceBooleanWithTrueNoRemove(constraint);
551                                                 } else if (edge != NULL && edge->mustNeg) {
552                                                         replaceBooleanWithFalseNoRemove(constraint);
553                                                 } else if ((invedge = graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
554                                                                                          && invedge->mustPos) {
555                                                         replaceBooleanWithFalseNoRemove(constraint);
556                                                 }
557                                         }
558                                 }
559                         }
560                 } else {
561                         delete constraint;
562                         constraint = b;
563                 }
564         }
565         BooleanEdge be = BooleanEdge(constraint);
566         return negate ? be.negate() : be;
567 }
568
569 void CSolver::addConstraint(BooleanEdge constraint) {
570         if (!useInterpreter() && !optimizationsOff) {
571                 if (isTrue(constraint))
572                         return;
573                 else if (isFalse(constraint)) {
574                         setUnSAT();
575                 }
576                 else {
577                         if (constraint->type == LOGICOP) {
578                                 BooleanLogic *b = (BooleanLogic *) constraint.getBoolean();
579                                 if (!constraint.isNegated()) {
580                                         if (b->op == SATC_AND) {
581                                                 uint size = b->inputs.getSize();
582                                                 //Handle potential concurrent modification
583                                                 BooleanEdge array[size];
584                                                 for (uint i = 0; i < size; i++) {
585                                                         array[i] = b->inputs.get(i);
586                                                 }
587                                                 for (uint i = 0; i < size; i++) {
588                                                         addConstraint(array[i]);
589                                                 }
590                                                 return;
591                                         }
592                                 }
593                                 if (b->replaced) {
594                                         addConstraint(doRewrite(constraint));
595                                         return;
596                                 }
597                         }
598                         constraints.add(constraint);
599                         Boolean *ptr = constraint.getBoolean();
600
601                         if (ptr->boolVal == BV_UNSAT) {
602                                 setUnSAT();
603                         }
604
605                         replaceBooleanWithTrueNoRemove(constraint);
606                         constraint->parents.clear();
607                 }
608         } else {
609                 constraints.add(constraint);
610                 constraint->parents.clear();
611         }
612 }
613
614 Order *CSolver::createOrder(OrderType type, Set *set) {
615         Order *order = new Order(type, set);
616         allOrders.push(order);
617         activeOrders.add(order);
618         return order;
619 }
620
621 /** Computes static ordering information to allow isTrue/isFalse
622     queries on newly created orders to work. */
623
624 void CSolver::inferFixedOrder(Order *order) {
625         if (order->graph != NULL) {
626                 delete order->graph;
627         }
628         order->graph = buildMustOrderGraph(order);
629         reachMustAnalysis(this, order->graph, true);
630 }
631
632 void CSolver::inferFixedOrders() {
633         SetIteratorOrder *orderit = activeOrders.iterator();
634         while (orderit->hasNext()) {
635                 Order *order = orderit->next();
636                 inferFixedOrder(order);
637         }
638 }
639
640 int CSolver::solveIncremental() {
641         if (isUnSAT()) {
642                 return IS_UNSAT;
643         }
644
645
646         long long startTime = getTimeNano();
647         bool deleteTuner = false;
648         if (tuner == NULL) {
649                 tuner = new DefaultTuner();
650                 deleteTuner = true;
651         }
652         int result = IS_INDETER;
653         ASSERT (!useInterpreter());
654         if(!optimizationsOff){
655                 computePolarities(this);
656         }
657 //      long long time1 = getTimeNano();
658 //      model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
659 //      Preprocess pp(this);
660 //      pp.doTransform();
661 //      long long time2 = getTimeNano();
662 //      model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
663
664 //      DecomposeOrderTransform dot(this);
665 //      dot.doTransform();
666 //      time1 = getTimeNano();
667 //      model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
668
669 //      IntegerEncodingTransform iet(this);
670 //      iet.doTransform();
671
672         //Doing element optimization on new constraints
673 //      ElementOpt eop(this);
674 //      eop.doTransform();
675
676         //Since no new element is added, we assuming adding new constraint
677         //has no impact on previous encoding decisions
678 //      EncodingGraph eg(this);
679 //      eg.encode();
680
681         naiveEncodingDecision(this);
682         //      eg.validate();
683         //Order of sat solver variables don't change!
684 //      VarOrderingOpt bor(this, satEncoder);
685 //      bor.doTransform();
686
687         long long time2 = getTimeNano();
688         //Encoding newly added constraints
689         satEncoder->encodeAllSATEncoder(this);
690         long long time1 = getTimeNano();
691
692         model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
693
694         model_print("Is problem UNSAT after encoding: %d\n", unsat);
695
696         result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
697         model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
698         time2 = getTimeNano();
699         elapsedTime = time2 - startTime;
700         model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
701
702         if (deleteTuner) {
703                 delete tuner;
704                 tuner = NULL;
705         }
706         return result;
707 }
708
709 int CSolver::solve() {
710         if (isUnSAT()) {
711                 return IS_UNSAT;
712         }
713         long long startTime = getTimeNano();
714         bool deleteTuner = false;
715         if (tuner == NULL) {
716                 tuner = new DefaultTuner();
717                 deleteTuner = true;
718         }
719         int result = IS_INDETER;
720         if (useInterpreter()) {
721                 interpreter->encode();
722                 model_print("Problem encoded in Interpreter\n");
723                 result = interpreter->solve();
724                 model_print("Problem solved by Interpreter\n");
725         } else {
726
727                 {
728                         SetIteratorOrder *orderit = activeOrders.iterator();
729                         while (orderit->hasNext()) {
730                                 Order *order = orderit->next();
731                                 if (order->graph != NULL) {
732                                         delete order->graph;
733                                         order->graph = NULL;
734                                 }
735                         }
736                         delete orderit;
737                 }
738                 long long time1, time2;
739                 
740                 computePolarities(this);
741                 time1 = getTimeNano();
742                 model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
743                 if(!optimizationsOff){
744                         Preprocess pp(this);
745                         pp.doTransform();
746                         time2 = getTimeNano();
747                         model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
748
749                         DecomposeOrderTransform dot(this);
750                         dot.doTransform();
751                         time1 = getTimeNano();
752                         model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
753
754                         IntegerEncodingTransform iet(this);
755                         iet.doTransform();
756
757                         ElementOpt eop(this);
758                         eop.doTransform();
759
760                         EncodingGraph eg(this);
761                         eg.encode();
762                 }
763                 naiveEncodingDecision(this);
764                 //      eg.validate();
765                 if(!optimizationsOff){
766                         VarOrderingOpt bor(this, satEncoder);
767                         bor.doTransform();
768                         time2 = getTimeNano();
769                         model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
770                 }
771
772                 satEncoder->encodeAllSATEncoder(this);
773                 time1 = getTimeNano();
774
775                 model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
776
777                 model_print("Is problem UNSAT after encoding: %d\n", unsat);
778
779
780                 result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
781                 model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
782                 time2 = getTimeNano();
783                 elapsedTime = time2 - startTime;
784                 model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
785         }
786         if (deleteTuner) {
787                 delete tuner;
788                 tuner = NULL;
789         }
790         return result;
791 }
792
793 void CSolver::setInterpreter(InterpreterType type) {
794         if (interpreter == NULL) {
795                 switch (type) {
796                 case SATUNE:
797                         break;
798                 case ALLOY: {
799                         interpreter = new AlloyInterpreter(this);
800                         break;
801                 } case Z3: {
802                         interpreter = new SMTInterpreter(this);
803                         break;
804                 }
805                 case MATHSAT: {
806                         interpreter = new MathSATInterpreter(this);
807                         break;
808                 }
809                 case SMTRAT: {
810                         interpreter = new SMTRatInterpreter(this);
811                         break;
812                 }
813                 default:
814                         ASSERT(0);
815                 }
816         }
817 }
818
819 void CSolver::printConstraints() {
820         SetIteratorBooleanEdge *it = getConstraints();
821         while (it->hasNext()) {
822                 BooleanEdge b = it->next();
823                 b.print();
824         }
825         delete it;
826 }
827
828 void CSolver::printConstraint(BooleanEdge b) {
829         b.print();
830 }
831
832 uint64_t CSolver::getElementValue(Element *element) {
833         switch (element->type) {
834         case ELEMSET:
835         case ELEMCONST:
836         case ELEMFUNCRETURN:
837                 return useInterpreter() ? interpreter->getValue(element) :
838                                          getElementValueSATTranslator(this, element);
839         default:
840                 ASSERT(0);
841         }
842         exit(-1);
843 }
844
845 void CSolver::freezeElement(Element *e) {
846         e->freezeElement();
847         if (!incrementalMode) {
848                 incrementalMode = true;
849         }
850 }
851
852 bool CSolver::getBooleanValue(BooleanEdge bedge) {
853         Boolean *boolean = bedge.getBoolean();
854         switch (boolean->type) {
855         case BOOLEANVAR:
856                 return useInterpreter() ? interpreter->getBooleanValue(boolean) :
857                                          getBooleanVariableValueSATTranslator(this, boolean);
858         default:
859                 ASSERT(0);
860         }
861         exit(-1);
862 }
863
864 bool CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) {
865         return order->encoding.resolver->resolveOrder(first, second);
866 }
867
868 long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); }
869
870 long long CSolver::getSolveTime() { return satEncoder->getSolveTime(); }
871
872 void CSolver::autoTune(uint budget) {
873         AutoTuner *autotuner = new AutoTuner(budget);
874         autotuner->addProblem(this);
875         autotuner->tune();
876         delete autotuner;
877 }
878
879