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