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