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