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