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