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