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