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