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