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::applyAtMostOneConstraint (BooleanEdge *array, uint asize) {
 413         if(asize == 0 || asize == 1){
 414                 return getBooleanTrue();
 415         }
 416         BooleanEdge newarray[asize*(asize-1)];
 417         uint newsize = 0;
 418         for (uint i = 0; i < asize -1; i++) {
 419                 for(uint j = i +1; j < asize; j++){
 420                         BooleanEdge oprand1 = array[i];
 421                         BooleanEdge oprand2 = applyLogicalOperation(SATC_NOT, array[j]);
 422                         newarray[newsize++] = applyLogicalOperation(SATC_IMPLIES, oprand1, oprand2);
 423                 }
 424         }
 425         return applyLogicalOperation(SATC_AND, newarray, newsize);
 426 }
 427
 428 BooleanEdge CSolver::applyExactlyOneConstraint (BooleanEdge *array, uint asize) {
 429         BooleanEdge atleastOne = applyLogicalOperation(SATC_OR, array, asize);
 430         BooleanEdge atmostOne = applyAtMostOneConstraint (array, asize);
 431         return applyLogicalOperation(SATC_AND, atleastOne, atmostOne);
 432 }
 433
 434 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
 435         if (!useInterpreter() && !optimizationsOff) {
 436                 BooleanEdge newarray[asize];
 437                 switch (op) {
 438                 case SATC_NOT: {
 439                         return array[0].negate();
 440                 }
 441                 case SATC_IFF: {
 442                         for (uint i = 0; i < 2; i++) {
 443                                 if (isTrue(array[i])) { // It can be undefined
 444                                         return array[1 - i];
 445                                 } else if (isFalse(array[i])) {
 446                                         newarray[0] = array[1 - i];
 447                                         return applyLogicalOperation(SATC_NOT, newarray, 1);
 448                                 } else if (array[i]->type == LOGICOP) {
 449                                         BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
 450                                         if (b->replaced) {
 451                                                 return rewriteLogicalOperation(op, array, asize);
 452                                         }
 453                                 }
 454                         }
 455                         break;
 456                 }
 457                 case SATC_OR: {
 458                         for (uint i = 0; i < asize; i++) {
 459                                 newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);
 460                         }
 461                         return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize));
 462                 }
 463                 case SATC_AND: {
 464                         uint newindex = 0;
 465                         for (uint i = 0; i < asize; i++) {
 466                                 BooleanEdge b = array[i];
 467                                 if (b->type == LOGICOP) {
 468                                         if (((BooleanLogic *)b.getBoolean())->replaced)
 469                                                 return rewriteLogicalOperation(op, array, asize);
 470                                 }
 471                                 if (isTrue(b))
 472                                         continue;
 473                                 else if (isFalse(b)) {
 474                                         return boolFalse;
 475                                 } else
 476                                         newarray[newindex++] = b;
 477                         }
 478                         if (newindex == 0) {
 479                                 return boolTrue;
 480                         } else if (newindex == 1) {
 481                                 return newarray[0];
 482                         } else {
 483                                 bsdqsort(newarray, newindex, sizeof(BooleanEdge), booleanEdgeCompares);
 484                                 array = newarray;
 485                                 asize = newindex;
 486                         }
 487                         break;
 488                 }
 489                 case SATC_XOR: {
 490                         //handle by translation
 491                         return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_IFF, array, asize));
 492                 }
 493                 case SATC_IMPLIES: {
 494                         //handle by translation
 495                         return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
 496                 }
 497                 }
 498
 499                 ASSERT(asize != 0);
 500                 Boolean *boolean = new BooleanLogic(this, op, array, asize);
 501                 Boolean *b = boolMap.get(boolean);
 502                 if (b == NULL) {
 503                         boolean->updateParents();
 504                         boolMap.put(boolean, boolean);
 505                         allBooleans.push(boolean);
 506                         return BooleanEdge(boolean);
 507                 } else {
 508                         delete boolean;
 509                         return BooleanEdge(b);
 510                 }
 511         } else {
 512                 ASSERT(asize != 0);
 513                 Boolean *boolean = new BooleanLogic(this, op, array, asize);
 514                 allBooleans.push(boolean);
 515                 return BooleanEdge(boolean);
 516
 517         }
 518 }
 519
 520 BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
 521         //      ASSERT(first != second);
 522         if (first == second)
 523                 return getBooleanFalse();
 524
 525         bool negate = false;
 526         if (order->type == SATC_TOTAL) {
 527                 if (first > second) {
 528                         uint64_t tmp = first;
 529                         first = second;
 530                         second = tmp;
 531                         negate = true;
 532                 }
 533         }
 534         Boolean *constraint = new BooleanOrder(order, first, second);
 535         if (!useInterpreter() && !optimizationsOff ) {
 536                 Boolean *b = boolMap.get(constraint);
 537
 538                 if (b == NULL) {
 539                         allBooleans.push(constraint);
 540                         boolMap.put(constraint, constraint);
 541                         constraint->updateParents();
 542                         if ( order->graph != NULL) {
 543                                 OrderGraph *graph = order->graph;
 544                                 OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first);
 545                                 if (from != NULL) {
 546                                         OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second);
 547                                         if (to != NULL) {
 548                                                 OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to);
 549                                                 OrderEdge *invedge;
 550
 551                                                 if (edge != NULL && edge->mustPos) {
 552                                                         replaceBooleanWithTrueNoRemove(constraint);
 553                                                 } else if (edge != NULL && edge->mustNeg) {
 554                                                         replaceBooleanWithFalseNoRemove(constraint);
 555                                                 } else if ((invedge = graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL
 556                                                                                          && invedge->mustPos) {
 557                                                         replaceBooleanWithFalseNoRemove(constraint);
 558                                                 }
 559                                         }
 560                                 }
 561                         }
 562                 } else {
 563                         delete constraint;
 564                         constraint = b;
 565                 }
 566         }
 567         BooleanEdge be = BooleanEdge(constraint);
 568         return negate ? be.negate() : be;
 569 }
 570
 571 void CSolver::addConstraint(BooleanEdge constraint) {
 572         if (!useInterpreter() && !optimizationsOff) {
 573                 if (isTrue(constraint))
 574                         return;
 575                 else if (isFalse(constraint)) {
 576                         setUnSAT();
 577                 }
 578                 else {
 579                         if (constraint->type == LOGICOP) {
 580                                 BooleanLogic *b = (BooleanLogic *) constraint.getBoolean();
 581                                 if (!constraint.isNegated()) {
 582                                         if (b->op == SATC_AND) {
 583                                                 uint size = b->inputs.getSize();
 584                                                 //Handle potential concurrent modification
 585                                                 BooleanEdge array[size];
 586                                                 for (uint i = 0; i < size; i++) {
 587                                                         array[i] = b->inputs.get(i);
 588                                                 }
 589                                                 for (uint i = 0; i < size; i++) {
 590                                                         addConstraint(array[i]);
 591                                                 }
 592                                                 return;
 593                                         }
 594                                 }
 595                                 if (b->replaced) {
 596                                         addConstraint(doRewrite(constraint));
 597                                         return;
 598                                 }
 599                         }
 600                         constraints.add(constraint);
 601                         Boolean *ptr = constraint.getBoolean();
 602
 603                         if (ptr->boolVal == BV_UNSAT) {
 604                                 setUnSAT();
 605                         }
 606
 607                         replaceBooleanWithTrueNoRemove(constraint);
 608                         constraint->parents.clear();
 609                 }
 610         } else {
 611                 constraints.add(constraint);
 612                 constraint->parents.clear();
 613         }
 614 }
 615
 616 Order *CSolver::createOrder(OrderType type, Set *set) {
 617         Order *order = new Order(type, set);
 618         allOrders.push(order);
 619         activeOrders.add(order);
 620         return order;
 621 }
 622
 623 /** Computes static ordering information to allow isTrue/isFalse
 624     queries on newly created orders to work. */
 625
 626 void CSolver::inferFixedOrder(Order *order) {
 627         if (order->graph != NULL) {
 628                 delete order->graph;
 629         }
 630         order->graph = buildMustOrderGraph(order);
 631         reachMustAnalysis(this, order->graph, true);
 632 }
 633
 634 void CSolver::inferFixedOrders() {
 635         SetIteratorOrder *orderit = activeOrders.iterator();
 636         while (orderit->hasNext()) {
 637                 Order *order = orderit->next();
 638                 inferFixedOrder(order);
 639         }
 640 }
 641
 642 int CSolver::solveIncremental() {
 643         if (isUnSAT()) {
 644                 return IS_UNSAT;
 645         }
 646
 647
 648         long long startTime = getTimeNano();
 649         bool deleteTuner = false;
 650         if (tuner == NULL) {
 651                 tuner = new DefaultTuner();
 652                 deleteTuner = true;
 653         }
 654         int result = IS_INDETER;
 655         ASSERT (!useInterpreter());
 656         if(!optimizationsOff){
 657                 computePolarities(this);
 658         }
 659 //      long long time1 = getTimeNano();
 660 //      model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
 661 //      Preprocess pp(this);
 662 //      pp.doTransform();
 663 //      long long time2 = getTimeNano();
 664 //      model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
 665
 666 //      DecomposeOrderTransform dot(this);
 667 //      dot.doTransform();
 668 //      time1 = getTimeNano();
 669 //      model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
 670
 671 //      IntegerEncodingTransform iet(this);
 672 //      iet.doTransform();
 673
 674         //Doing element optimization on new constraints
 675 //      ElementOpt eop(this);
 676 //      eop.doTransform();
 677
 678         //Since no new element is added, we assuming adding new constraint
 679         //has no impact on previous encoding decisions
 680 //      EncodingGraph eg(this);
 681 //      eg.encode();
 682
 683         naiveEncodingDecision(this);
 684         //      eg.validate();
 685         //Order of sat solver variables don't change!
 686 //      VarOrderingOpt bor(this, satEncoder);
 687 //      bor.doTransform();
 688
 689         long long time2 = getTimeNano();
 690         //Encoding newly added constraints
 691         satEncoder->encodeAllSATEncoder(this);
 692         long long time1 = getTimeNano();
 693
 694         model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
 695
 696         model_print("Is problem UNSAT after encoding: %d\n", unsat);
 697
 698         result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
 699         model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
 700         time2 = getTimeNano();
 701         elapsedTime = time2 - startTime;
 702         model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
 703
 704         if (deleteTuner) {
 705                 delete tuner;
 706                 tuner = NULL;
 707         }
 708         return result;
 709 }
 710
 711 int CSolver::solve() {
 712         if (isUnSAT()) {
 713                 return IS_UNSAT;
 714         }
 715         long long startTime = getTimeNano();
 716         bool deleteTuner = false;
 717         if (tuner == NULL) {
 718                 tuner = new DefaultTuner();
 719                 deleteTuner = true;
 720         }
 721         int result = IS_INDETER;
 722         if (useInterpreter()) {
 723                 interpreter->encode();
 724                 model_print("Problem encoded in Interpreter\n");
 725                 result = interpreter->solve();
 726                 model_print("Problem solved by Interpreter\n");
 727         } else {
 728
 729                 {
 730                         SetIteratorOrder *orderit = activeOrders.iterator();
 731                         while (orderit->hasNext()) {
 732                                 Order *order = orderit->next();
 733                                 if (order->graph != NULL) {
 734                                         delete order->graph;
 735                                         order->graph = NULL;
 736                                 }
 737                         }
 738                         delete orderit;
 739                 }
 740                 long long time1, time2;
 741
 742                 computePolarities(this);
 743                 time1 = getTimeNano();
 744                 model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC);
 745                 if(!optimizationsOff){
 746                         Preprocess pp(this);
 747                         pp.doTransform();
 748                         time2 = getTimeNano();
 749                         model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC);
 750
 751                         DecomposeOrderTransform dot(this);
 752                         dot.doTransform();
 753                         time1 = getTimeNano();
 754                         model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC);
 755
 756                         IntegerEncodingTransform iet(this);
 757                         iet.doTransform();
 758
 759                         ElementOpt eop(this);
 760                         eop.doTransform();
 761
 762                         EncodingGraph eg(this);
 763                         eg.encode();
 764                 }
 765                 naiveEncodingDecision(this);
 766                 //      eg.validate();
 767                 if(!optimizationsOff){
 768                         VarOrderingOpt bor(this, satEncoder);
 769                         bor.doTransform();
 770                         time2 = getTimeNano();
 771                         model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC);
 772                 }
 773
 774                 satEncoder->encodeAllSATEncoder(this);
 775                 time1 = getTimeNano();
 776
 777                 model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC);
 778
 779                 model_print("Is problem UNSAT after encoding: %d\n", unsat);
 780
 781
 782                 result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout);
 783                 model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT ? "SAT" : result == IS_INDETER ? "INDETERMINATE" : " UNSAT");
 784                 time2 = getTimeNano();
 785                 elapsedTime = time2 - startTime;
 786                 model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC);
 787         }
 788         if (deleteTuner) {
 789                 delete tuner;
 790                 tuner = NULL;
 791         }
 792         return result;
 793 }
 794
 795 void CSolver::setInterpreter(InterpreterType type) {
 796         if (interpreter == NULL) {
 797                 switch (type) {
 798                 case SATUNE:
 799                         break;
 800                 case ALLOY: {
 801                         interpreter = new AlloyInterpreter(this);
 802                         break;
 803                 } case Z3: {
 804                         interpreter = new SMTInterpreter(this);
 805                         break;
 806                 }
 807                 case MATHSAT: {
 808                         interpreter = new MathSATInterpreter(this);
 809                         break;
 810                 }
 811                 case SMTRAT: {
 812                         interpreter = new SMTRatInterpreter(this);
 813                         break;
 814                 }
 815                 default:
 816                         ASSERT(0);
 817                 }
 818         }
 819 }
 820
 821 void CSolver::printConstraints() {
 822         SetIteratorBooleanEdge *it = getConstraints();
 823         while (it->hasNext()) {
 824                 BooleanEdge b = it->next();
 825                 b.print();
 826         }
 827         delete it;
 828 }
 829
 830 void CSolver::printConstraint(BooleanEdge b) {
 831         b.print();
 832 }
 833
 834 uint64_t CSolver::getElementValue(Element *element) {
 835         switch (element->type) {
 836         case ELEMSET:
 837         case ELEMCONST:
 838         case ELEMFUNCRETURN:
 839                 return useInterpreter() ? interpreter->getValue(element) :
 840                                          getElementValueSATTranslator(this, element);
 841         default:
 842                 ASSERT(0);
 843         }
 844         exit(-1);
 845 }
 846
 847 void CSolver::freezeElement(Element *e) {
 848         e->freezeElement();
 849         if (!incrementalMode) {
 850                 incrementalMode = true;
 851         }
 852 }
 853
 854 bool CSolver::getBooleanValue(BooleanEdge bedge) {
 855         Boolean *boolean = bedge.getBoolean();
 856         switch (boolean->type) {
 857         case BOOLEANVAR:
 858                 return useInterpreter() ? interpreter->getBooleanValue(boolean) :
 859                                          getBooleanVariableValueSATTranslator(this, boolean);
 860         default:
 861                 ASSERT(0);
 862         }
 863         exit(-1);
 864 }
 865
 866 bool CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) {
 867         return order->encoding.resolver->resolveOrder(first, second);
 868 }
 869
 870 long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); }
 871
 872 long long CSolver::getSolveTime() { return satEncoder->getSolveTime(); }
 873
 874 void CSolver::autoTune(uint budget) {
 875         AutoTuner *autotuner = new AutoTuner(budget);
 876         autotuner->addProblem(this);
 877         autotuner->tune();
 878         delete autotuner;
 879 }
 880
 881