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