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