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
  26 CSolver::CSolver() :
  27         boolTrue(BooleanEdge(new BooleanConst(true))),
  28         boolFalse(boolTrue.negate()),
  29         unsat(false),
  30         tuner(NULL),
  31         elapsedTime(0)
  32 {
  33         satEncoder = new SATEncoder(this);
  34 }
  35
  36 /** This function tears down the solver and the entire AST */
  37
  38 CSolver::~CSolver() {
  39         uint size = allBooleans.getSize();
  40         for (uint i = 0; i < size; i++) {
  41                 delete allBooleans.get(i);
  42         }
  43
  44         size = allSets.getSize();
  45         for (uint i = 0; i < size; i++) {
  46                 delete allSets.get(i);
  47         }
  48
  49         size = allElements.getSize();
  50         for (uint i = 0; i < size; i++) {
  51                 Element* el = allElements.get(i);
  52                 model_print("deleting ...%u", i);
  53                 ASSERT(el != NULL);
  54                 delete el;
  55         }
  56
  57         size = allTables.getSize();
  58         for (uint i = 0; i < size; i++) {
  59                 delete allTables.get(i);
  60         }
  61
  62         size = allPredicates.getSize();
  63         for (uint i = 0; i < size; i++) {
  64                 delete allPredicates.get(i);
  65         }
  66
  67         size = allOrders.getSize();
  68         for (uint i = 0; i < size; i++) {
  69                 delete allOrders.get(i);
  70         }
  71
  72         size = allFunctions.getSize();
  73         for (uint i = 0; i < size; i++) {
  74                 delete allFunctions.get(i);
  75         }
  76
  77         delete boolTrue.getBoolean();
  78         delete satEncoder;
  79 }
  80
  81 CSolver *CSolver::clone() {
  82         CSolver *copy = new CSolver();
  83         CloneMap map;
  84         SetIteratorBooleanEdge *it = getConstraints();
  85         while (it->hasNext()) {
  86                 BooleanEdge b = it->next();
  87                 copy->addConstraint(cloneEdge(copy, &map, b));
  88         }
  89         delete it;
  90         return copy;
  91 }
  92
  93 void CSolver::serialize() {
  94         model_print("serializing ...\n");
  95         {
  96                 Serializer serializer("dump");
  97                 SetIteratorBooleanEdge *it = getConstraints();
  98                 while (it->hasNext()) {
  99                         BooleanEdge b = it->next();
 100                         serializeBooleanEdge(&serializer, b);
 101                 }
 102                 delete it;
 103         }
 104 //      model_print("deserializing ...\n");
 105 //      {
 106 //              Deserializer deserializer("dump");
 107 //              deserializer.deserialize();
 108 //      }
 109 }
 110
 111 Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
 112         Set *set = new Set(type, elements, numelements);
 113         allSets.push(set);
 114         return set;
 115 }
 116
 117 Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange) {
 118         Set *set = new Set(type, lowrange, highrange);
 119         allSets.push(set);
 120         return set;
 121 }
 122
 123 VarType CSolver::getSetVarType(Set *set) {
 124         return set->getType();
 125 }
 126
 127 Element *CSolver::createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange) {
 128         Set *s = createRangeSet(type, lowrange, highrange);
 129         return getElementVar(s);
 130 }
 131
 132 MutableSet *CSolver::createMutableSet(VarType type) {
 133         MutableSet *set = new MutableSet(type);
 134         allSets.push(set);
 135         return set;
 136 }
 137
 138 void CSolver::addItem(MutableSet *set, uint64_t element) {
 139         set->addElementMSet(element);
 140 }
 141
 142 uint64_t CSolver::createUniqueItem(MutableSet *set) {
 143         uint64_t element = set->getNewUniqueItem();
 144         set->addElementMSet(element);
 145         return element;
 146 }
 147
 148 void CSolver::finalizeMutableSet(MutableSet *set) {
 149         set->finalize();
 150 }
 151
 152 Element *CSolver::getElementVar(Set *set) {
 153         Element *element = new ElementSet(set);
 154         model_println("%%%%ElementVar:%u", allElements.getSize());
 155         allElements.push(element);
 156         return element;
 157 }
 158
 159 Set *CSolver::getElementRange (Element *element) {
 160         return element->getRange();
 161 }
 162
 163
 164 Element *CSolver::getElementConst(VarType type, uint64_t value) {
 165         uint64_t array[] = {value};
 166         Set *set = new Set(type, array, 1);
 167         Element *element = new ElementConst(value, set);
 168         Element *e = elemMap.get(element);
 169         if (e == NULL) {
 170                 allSets.push(set);
 171                 model_println("%%%%ElementConst:%u", allElements.getSize());
 172                 allElements.push(element);
 173                 elemMap.put(element, element);
 174                 return element;
 175         } else {
 176                 delete set;
 177                 delete element;
 178                 return e;
 179         }
 180 }
 181
 182 Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) {
 183         Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
 184         Element *e = elemMap.get(element);
 185         if (e == NULL) {
 186                 element->updateParents();
 187                 model_println("%%%%ElementFunction:%u", allElements.getSize());
 188                 allElements.push(element);
 189                 elemMap.put(element, element);
 190                 return element;
 191         } else {
 192                 delete element;
 193                 return e;
 194         }
 195 }
 196
 197 Function *CSolver::createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) {
 198         Function *function = new FunctionOperator(op, domain, numDomain, range, overflowbehavior);
 199         allFunctions.push(function);
 200         return function;
 201 }
 202
 203 Predicate *CSolver::createPredicateOperator(CompOp op, Set **domain, uint numDomain) {
 204         Predicate *predicate = new PredicateOperator(op, domain,numDomain);
 205         allPredicates.push(predicate);
 206         return predicate;
 207 }
 208
 209 Predicate *CSolver::createPredicateTable(Table *table, UndefinedBehavior behavior) {
 210         Predicate *predicate = new PredicateTable(table, behavior);
 211         allPredicates.push(predicate);
 212         return predicate;
 213 }
 214
 215 Table *CSolver::createTable(Set **domains, uint numDomain, Set *range) {
 216         Table *table = new Table(domains,numDomain,range);
 217         allTables.push(table);
 218         return table;
 219 }
 220
 221 Table *CSolver::createTableForPredicate(Set **domains, uint numDomain) {
 222         return createTable(domains, numDomain, NULL);
 223 }
 224
 225 void CSolver::addTableEntry(Table *table, uint64_t *inputs, uint inputSize, uint64_t result) {
 226         table->addNewTableEntry(inputs, inputSize, result);
 227 }
 228
 229 Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) {
 230         Function *function = new FunctionTable(table, behavior);
 231         allFunctions.push(function);
 232         return function;
 233 }
 234
 235 BooleanEdge CSolver::getBooleanVar(VarType type) {
 236         Boolean *boolean = new BooleanVar(type);
 237         allBooleans.push(boolean);
 238         return BooleanEdge(boolean);
 239 }
 240
 241 BooleanEdge CSolver::getBooleanTrue() {
 242         return boolTrue;
 243 }
 244
 245 BooleanEdge CSolver::getBooleanFalse() {
 246         return boolFalse;
 247 }
 248
 249 BooleanEdge CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) {
 250         return applyPredicateTable(predicate, inputs, numInputs, BooleanEdge(NULL));
 251 }
 252
 253 BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, BooleanEdge undefinedStatus) {
 254         BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
 255         Boolean *b = boolMap.get(boolean);
 256         if (b == NULL) {
 257                 boolean->updateParents();
 258                 boolMap.put(boolean, boolean);
 259                 allBooleans.push(boolean);
 260                 return BooleanEdge(boolean);
 261         } else {
 262                 delete boolean;
 263                 return BooleanEdge(b);
 264         }
 265 }
 266
 267 bool CSolver::isTrue(BooleanEdge b) {
 268         return b.isNegated() ? b->isFalse() : b->isTrue();
 269 }
 270
 271 bool CSolver::isFalse(BooleanEdge b) {
 272         return b.isNegated() ? b->isTrue() : b->isFalse();
 273 }
 274
 275 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2) {
 276         BooleanEdge array[] = {arg1, arg2};
 277         return applyLogicalOperation(op, array, 2);
 278 }
 279
 280 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg) {
 281         BooleanEdge array[] = {arg};
 282         return applyLogicalOperation(op, array, 1);
 283 }
 284
 285 static int ptrcompares(const void *p1, const void *p2) {
 286         uintptr_t b1 = *(uintptr_t const *) p1;
 287         uintptr_t b2 = *(uintptr_t const *) p2;
 288         if (b1 < b2)
 289                 return -1;
 290         else if (b1 == b2)
 291                 return 0;
 292         else
 293                 return 1;
 294 }
 295
 296 BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
 297         BooleanEdge newarray[asize];
 298         memcpy(newarray, array, asize * sizeof(BooleanEdge));
 299         for (uint i = 0; i < asize; i++) {
 300                 BooleanEdge b = newarray[i];
 301                 if (b->type == LOGICOP) {
 302                         if (((BooleanLogic *) b.getBoolean())->replaced) {
 303                                 newarray[i] = doRewrite(newarray[i]);
 304                                 i--;//Check again
 305                         }
 306                 }
 307         }
 308         return applyLogicalOperation(op, newarray, asize);
 309 }
 310
 311 BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) {
 312         BooleanEdge newarray[asize];
 313         switch (op) {
 314         case SATC_NOT: {
 315                 return array[0].negate();
 316         }
 317         case SATC_IFF: {
 318                 for (uint i = 0; i < 2; i++) {
 319                         if (array[i]->type == BOOLCONST) {
 320                                 if (isTrue(array[i])) { // It can be undefined
 321                                         return array[1 - i];
 322                                 } else if (isFalse(array[i])) {
 323                                         newarray[0] = array[1 - i];
 324                                         return applyLogicalOperation(SATC_NOT, newarray, 1);
 325                                 }
 326                         } else if (array[i]->type == LOGICOP) {
 327                                 BooleanLogic *b = (BooleanLogic *)array[i].getBoolean();
 328                                 if (b->replaced) {
 329                                         return rewriteLogicalOperation(op, array, asize);
 330                                 }
 331                         }
 332                 }
 333                 break;
 334         }
 335         case SATC_OR: {
 336                 for (uint i = 0; i < asize; i++) {
 337                         newarray[i] = applyLogicalOperation(SATC_NOT, array[i]);
 338                 }
 339                 return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize));
 340         }
 341         case SATC_AND: {
 342                 uint newindex = 0;
 343                 for (uint i = 0; i < asize; i++) {
 344                         BooleanEdge b = array[i];
 345                         if (b->type == LOGICOP) {
 346                                 if (((BooleanLogic *)b.getBoolean())->replaced)
 347                                         return rewriteLogicalOperation(op, array, asize);
 348                         }
 349                         if (b->type == BOOLCONST) {
 350                                 if (isTrue(b))
 351                                         continue;
 352                                 else {
 353                                         return boolFalse;
 354                                 }
 355                         } else
 356                                 newarray[newindex++] = b;
 357                 }
 358                 if (newindex == 0) {
 359                         return boolTrue;
 360                 } else if (newindex == 1) {
 361                         return newarray[0];
 362                 } else {
 363                         bsdqsort(newarray, newindex, sizeof(BooleanEdge), ptrcompares);
 364                         array = newarray;
 365                         asize = newindex;
 366                 }
 367                 break;
 368         }
 369         case SATC_XOR: {
 370                 //handle by translation
 371                 return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_IFF, array, asize));
 372         }
 373         case SATC_IMPLIES: {
 374                 //handle by translation
 375                 return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]);
 376         }
 377         }
 378
 379         ASSERT(asize != 0);
 380         Boolean *boolean = new BooleanLogic(this, op, array, asize);
 381         Boolean *b = boolMap.get(boolean);
 382         if (b == NULL) {
 383                 boolean->updateParents();
 384                 boolMap.put(boolean, boolean);
 385                 allBooleans.push(boolean);
 386                 return BooleanEdge(boolean);
 387         } else {
 388                 delete boolean;
 389                 return BooleanEdge(b);
 390         }
 391 }
 392
 393 BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
 394         ASSERT(first != second);
 395         Boolean *constraint = new BooleanOrder(order, first, second);
 396         allBooleans.push(constraint);
 397         return BooleanEdge(constraint);
 398 }
 399
 400 void CSolver::addConstraint(BooleanEdge constraint) {
 401 #ifdef TRACE_DEBUG
 402         model_println("****New Constraint******");
 403 #endif
 404         if (isTrue(constraint))
 405                 return;
 406         else if (isFalse(constraint)) {
 407                 int t = 0;
 408                 setUnSAT();
 409         }
 410         else {
 411                 if (constraint->type == LOGICOP) {
 412                         BooleanLogic *b = (BooleanLogic *) constraint.getBoolean();
 413                         if (!constraint.isNegated()) {
 414                                 if (b->op == SATC_AND) {
 415                                         for (uint i = 0; i < b->inputs.getSize(); i++) {
 416                                                 addConstraint(b->inputs.get(i));
 417                                         }
 418                                         return;
 419                                 }
 420                         }
 421                         if (b->replaced) {
 422                                 addConstraint(doRewrite(constraint));
 423                                 return;
 424                         }
 425                 }
 426                 constraints.add(constraint);
 427                 Boolean *ptr = constraint.getBoolean();
 428
 429                 if (ptr->boolVal == BV_UNSAT) {
 430                         setUnSAT();
 431                 }
 432
 433                 replaceBooleanWithTrueNoRemove(constraint);
 434                 constraint->parents.clear();
 435         }
 436 }
 437
 438 Order *CSolver::createOrder(OrderType type, Set *set) {
 439         Order *order = new Order(type, set);
 440         allOrders.push(order);
 441         activeOrders.add(order);
 442         return order;
 443 }
 444
 445 int CSolver::solve() {
 446         bool deleteTuner = false;
 447         if (tuner == NULL) {
 448                 tuner = new DefaultTuner();
 449                 deleteTuner = true;
 450         }
 451
 452         long long startTime = getTimeNano();
 453         computePolarities(this);
 454
 455         Preprocess pp(this);
 456         pp.doTransform();
 457
 458         DecomposeOrderTransform dot(this);
 459         dot.doTransform();
 460
 461         IntegerEncodingTransform iet(this);
 462         iet.doTransform();
 463
 464         EncodingGraph eg(this);
 465         eg.buildGraph();
 466         eg.encode();
 467         printConstraints();
 468         naiveEncodingDecision(this);
 469         satEncoder->encodeAllSATEncoder(this);
 470         model_print("Is problem UNSAT after encoding: %d\n", unsat);
 471         int result = unsat ? IS_UNSAT : satEncoder->solve();
 472         model_print("Result Computed in CSolver: %d\n", result);
 473         long long finishTime = getTimeNano();
 474         elapsedTime = finishTime - startTime;
 475         if (deleteTuner) {
 476                 delete tuner;
 477                 tuner = NULL;
 478         }
 479         return result;
 480 }
 481
 482 void CSolver::printConstraints() {
 483         SetIteratorBooleanEdge *it = getConstraints();
 484         while (it->hasNext()) {
 485                 BooleanEdge b = it->next();
 486                 if (b.isNegated())
 487                         model_print("!");
 488                 b->print();
 489                 model_print("\n");
 490         }
 491         delete it;
 492
 493 }
 494
 495 uint64_t CSolver::getElementValue(Element *element) {
 496         switch (element->type) {
 497         case ELEMSET:
 498         case ELEMCONST:
 499         case ELEMFUNCRETURN:
 500                 return getElementValueSATTranslator(this, element);
 501         default:
 502                 ASSERT(0);
 503         }
 504         exit(-1);
 505 }
 506
 507 bool CSolver::getBooleanValue(BooleanEdge bedge) {
 508         Boolean *boolean = bedge.getBoolean();
 509         switch (boolean->type) {
 510         case BOOLEANVAR:
 511                 return getBooleanVariableValueSATTranslator(this, boolean);
 512         default:
 513                 ASSERT(0);
 514         }
 515         exit(-1);
 516 }
 517
 518 bool CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) {
 519         return order->encoding.resolver->resolveOrder(first, second);
 520 }
 521
 522 long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); }
 523
 524 long long CSolver::getSolveTime() { return satEncoder->getSolveTime(); }
 525
 526 void CSolver::autoTune(uint budget) {
 527         AutoTuner *autotuner = new AutoTuner(budget);
 528         autotuner->addProblem(this);
 529         autotuner->tune();
 530         delete autotuner;
 531 }