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 "analyzer.h"
  15 #include "autotuner.h"
  16
  17 CSolver::CSolver() :
  18         boolTrue(new BooleanConst(true)),
  19         boolFalse(new BooleanConst(false)),
  20         unsat(false),
  21         tuner(NULL),
  22         elapsedTime(0)
  23 {
  24         satEncoder = new SATEncoder(this);
  25 }
  26
  27 /** This function tears down the solver and the entire AST */
  28
  29 CSolver::~CSolver() {
  30         uint size = allBooleans.getSize();
  31         for (uint i = 0; i < size; i++) {
  32                 delete allBooleans.get(i);
  33         }
  34
  35         size = allSets.getSize();
  36         for (uint i = 0; i < size; i++) {
  37                 delete allSets.get(i);
  38         }
  39
  40         size = allElements.getSize();
  41         for (uint i = 0; i < size; i++) {
  42                 delete allElements.get(i);
  43         }
  44
  45         size = allTables.getSize();
  46         for (uint i = 0; i < size; i++) {
  47                 delete allTables.get(i);
  48         }
  49
  50         size = allPredicates.getSize();
  51         for (uint i = 0; i < size; i++) {
  52                 delete allPredicates.get(i);
  53         }
  54
  55         size = allOrders.getSize();
  56         for (uint i = 0; i < size; i++) {
  57                 delete allOrders.get(i);
  58         }
  59
  60         size = allFunctions.getSize();
  61         for (uint i = 0; i < size; i++) {
  62                 delete allFunctions.get(i);
  63         }
  64
  65         delete boolTrue;
  66         delete boolFalse;
  67         delete satEncoder;
  68 }
  69
  70 CSolver *CSolver::clone() {
  71         CSolver *copy = new CSolver();
  72         CloneMap map;
  73         HSIteratorBoolean *it = getConstraints();
  74         while (it->hasNext()) {
  75                 Boolean *b = it->next();
  76                 copy->addConstraint(b->clone(copy, &map));
  77         }
  78         delete it;
  79         return copy;
  80 }
  81
  82 Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
  83         Set *set = new Set(type, elements, numelements);
  84         allSets.push(set);
  85         return set;
  86 }
  87
  88 Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange) {
  89         Set *set = new Set(type, lowrange, highrange);
  90         allSets.push(set);
  91         return set;
  92 }
  93
  94 MutableSet *CSolver::createMutableSet(VarType type) {
  95         MutableSet *set = new MutableSet(type);
  96         allSets.push(set);
  97         return set;
  98 }
  99
 100 void CSolver::addItem(MutableSet *set, uint64_t element) {
 101         set->addElementMSet(element);
 102 }
 103
 104 uint64_t CSolver::createUniqueItem(MutableSet *set) {
 105         uint64_t element = set->low++;
 106         set->addElementMSet(element);
 107         return element;
 108 }
 109
 110 Element *CSolver::getElementVar(Set *set) {
 111         Element *element = new ElementSet(set);
 112         allElements.push(element);
 113         return element;
 114 }
 115
 116 Element *CSolver::getElementConst(VarType type, uint64_t value) {
 117         uint64_t array[] = {value};
 118         Set *set = new Set(type, array, 1);
 119         Element *element = new ElementConst(value, type, set);
 120         Element *e = elemMap.get(element);
 121         if (e == NULL) {
 122                 allSets.push(set);
 123                 allElements.push(element);
 124                 elemMap.put(element, element);
 125                 return element;
 126         } else {
 127                 delete set;
 128                 delete element;
 129                 return e;
 130         }
 131 }
 132
 133 Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus) {
 134         Element *element = new ElementFunction(function,array,numArrays,overflowstatus);
 135         Element *e = elemMap.get(element);
 136         if (e == NULL) {
 137                 allElements.push(element);
 138                 elemMap.put(element, element);
 139                 return element;
 140         } else {
 141                 delete element;
 142                 return e;
 143         }
 144 }
 145
 146 Function *CSolver::createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) {
 147         Function *function = new FunctionOperator(op, domain, numDomain, range, overflowbehavior);
 148         allFunctions.push(function);
 149         return function;
 150 }
 151
 152 Predicate *CSolver::createPredicateOperator(CompOp op, Set **domain, uint numDomain) {
 153         Predicate *predicate = new PredicateOperator(op, domain,numDomain);
 154         allPredicates.push(predicate);
 155         return predicate;
 156 }
 157
 158 Predicate *CSolver::createPredicateTable(Table *table, UndefinedBehavior behavior) {
 159         Predicate *predicate = new PredicateTable(table, behavior);
 160         allPredicates.push(predicate);
 161         return predicate;
 162 }
 163
 164 Table *CSolver::createTable(Set **domains, uint numDomain, Set *range) {
 165         Table *table = new Table(domains,numDomain,range);
 166         allTables.push(table);
 167         return table;
 168 }
 169
 170 Table *CSolver::createTableForPredicate(Set **domains, uint numDomain) {
 171         return createTable(domains, numDomain, NULL);
 172 }
 173
 174 void CSolver::addTableEntry(Table *table, uint64_t *inputs, uint inputSize, uint64_t result) {
 175         table->addNewTableEntry(inputs, inputSize, result);
 176 }
 177
 178 Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) {
 179         Function *function = new FunctionTable(table, behavior);
 180         allFunctions.push(function);
 181         return function;
 182 }
 183
 184 Boolean *CSolver::getBooleanVar(VarType type) {
 185         Boolean *boolean = new BooleanVar(type);
 186         allBooleans.push(boolean);
 187         return boolean;
 188 }
 189
 190 Boolean *CSolver::getBooleanTrue() {
 191         return boolTrue;
 192 }
 193
 194 Boolean *CSolver::getBooleanFalse() {
 195         return boolFalse;
 196 }
 197
 198 Boolean *CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) {
 199         return applyPredicateTable(predicate, inputs, numInputs, NULL);
 200 }
 201
 202 Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) {
 203         BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus);
 204         Boolean * b = boolMap.get(boolean);
 205         if (b == NULL) {
 206                 boolMap.put(boolean, boolean);
 207                 allBooleans.push(boolean);
 208                 return boolean;
 209         } else {
 210                 delete boolean;
 211                 return b;
 212         }
 213 }
 214
 215 Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) {
 216         Boolean * newarray[asize];
 217         switch(op) {
 218         case L_NOT: {
 219                 if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op==L_NOT) {
 220                         return ((BooleanLogic *) array[0])->inputs.get(0);
 221                 } else if (array[0]->type == BOOLCONST) {
 222                         bool isTrue = ((BooleanConst *) array[0])->isTrue;
 223                         return isTrue ? boolFalse : boolTrue;
 224                 }
 225                 break;
 226         }
 227         case L_XOR: {
 228                 for(uint i=0;i<2;i++) {
 229                         if (array[i]->type == BOOLCONST) {
 230                                 bool isTrue = ((BooleanConst *) array[i])->isTrue;
 231                                 if (isTrue) {
 232                                         newarray[0]=array[1-i];
 233                                         return applyLogicalOperation(L_NOT, newarray, 1);
 234                                 } else
 235                                         return array[1-i];
 236                         }
 237                 }
 238                 break;
 239         }
 240         case L_OR: {
 241                 uint newindex=0;
 242                 for(uint i=0;i<asize;i++) {
 243                         Boolean *b=array[i];
 244                         if (b->type == BOOLCONST) {
 245                                 bool isTrue = ((BooleanConst *) b)->isTrue;
 246                                 if (isTrue)
 247                                         return b;
 248                                 else
 249                                         continue;
 250                         } else
 251                                 newarray[newindex++]=b;
 252                 }
 253                 if (newindex==1)
 254                         return newarray[0];
 255                 else if (newindex == 2) {
 256                         bool isNot0 = (newarray[0]->type==BOOLCONST) && ((BooleanLogic *)newarray[0])->op == L_NOT;
 257                         bool isNot1 = (newarray[1]->type==BOOLCONST) && ((BooleanLogic *)newarray[1])->op == L_NOT;
 258
 259                         if (isNot0 != isNot1) {
 260                                 if (isNot0) {
 261                                         newarray[0] = ((BooleanLogic *) newarray[0])->inputs.get(0);
 262                                 } else {
 263                                         Boolean *tmp =  ((BooleanLogic *) array[1])->inputs.get(0);
 264                                         array[1] = array[0];
 265                                         array[0] = tmp;
 266                                 }
 267                                 return applyLogicalOperation(L_IMPLIES, newarray, 2);
 268                         }
 269                 } else {
 270                         array = newarray;
 271                         asize = newindex;
 272                 }
 273                 break;
 274         }
 275         case L_AND: {
 276                 uint newindex=0;
 277                 for(uint i=0;i<asize;i++) {
 278                         Boolean *b=array[i];
 279                         if (b->type == BOOLCONST) {
 280                                 bool isTrue = ((BooleanConst *) b)->isTrue;
 281                                 if (isTrue)
 282                                         continue;
 283                                 else
 284                                         return b;
 285                         } else
 286                                 newarray[newindex++]=b;
 287                 }
 288                 if(newindex==1) {
 289                         return newarray[0];
 290                 } else {
 291                         array = newarray;
 292                         asize = newindex;
 293                 }
 294                 break;
 295         }
 296         case L_IMPLIES: {
 297                 if (array[0]->type == BOOLCONST) {
 298                         BooleanConst *b=(BooleanConst *) array[0];
 299                         if (b->isTrue) {
 300                                 return array[1];
 301                         } else {
 302                                 return boolTrue;
 303                         }
 304                 } else if (array[1]->type == BOOLCONST) {
 305                         BooleanConst *b=(BooleanConst *) array[0];
 306                         if (b->isTrue) {
 307                                 return b;
 308                         } else {
 309                                 return applyLogicalOperation(L_NOT, array, 1);
 310                         }
 311                 }
 312                 break;
 313         }
 314         }
 315
 316         Boolean *boolean = new BooleanLogic(this, op, array, asize);
 317         Boolean *b = boolMap.get(boolean);
 318         if (b == NULL) {
 319                 boolMap.put(boolean, boolean);
 320                 allBooleans.push(boolean);
 321                 return boolean;
 322         } else {
 323                 delete boolean;
 324                 return b;
 325         }
 326 }
 327
 328 Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) {
 329         Boolean *constraint = new BooleanOrder(order, first, second);
 330         allBooleans.push(constraint);
 331         return constraint;
 332 }
 333
 334 void CSolver::addConstraint(Boolean *constraint) {
 335         if (constraint == boolTrue)
 336                 return;
 337         else if (constraint == boolFalse)
 338                 setUnSAT();
 339         else
 340                 constraints.add(constraint);
 341 }
 342
 343 Order *CSolver::createOrder(OrderType type, Set *set) {
 344         Order *order = new Order(type, set);
 345         allOrders.push(order);
 346         return order;
 347 }
 348
 349 int CSolver::startEncoding() {
 350         bool deleteTuner = false;
 351         if (tuner == NULL) {
 352                 tuner = new DefaultTuner();
 353                 deleteTuner = true;
 354         }
 355
 356         long long startTime = getTimeNano();
 357         computePolarities(this);
 358         orderAnalysis(this);
 359         naiveEncodingDecision(this);
 360         satEncoder->encodeAllSATEncoder(this);
 361         int result = unsat ? IS_UNSAT : satEncoder->solve();
 362         long long finishTime = getTimeNano();
 363         elapsedTime = finishTime - startTime;
 364         if (deleteTuner) {
 365                 delete tuner;
 366                 tuner = NULL;
 367         }
 368         return result;
 369 }
 370
 371 uint64_t CSolver::getElementValue(Element *element) {
 372         switch (element->type) {
 373         case ELEMSET:
 374         case ELEMCONST:
 375         case ELEMFUNCRETURN:
 376                 return getElementValueSATTranslator(this, element);
 377         default:
 378                 ASSERT(0);
 379         }
 380         exit(-1);
 381 }
 382
 383 bool CSolver::getBooleanValue(Boolean *boolean) {
 384         switch (boolean->type) {
 385         case BOOLEANVAR:
 386                 return getBooleanVariableValueSATTranslator(this, boolean);
 387         default:
 388                 ASSERT(0);
 389         }
 390         exit(-1);
 391 }
 392
 393 HappenedBefore CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) {
 394         return getOrderConstraintValueSATTranslator(this, order, first, second);
 395 }
 396
 397 long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); }
 398
 399 long long CSolver::getSolveTime() { return satEncoder->getSolveTime(); }
 400
 401 void CSolver::autoTune(uint budget) {
 402         AutoTuner * autotuner=new AutoTuner(budget);
 403         autotuner->addProblem(this);
 404         autotuner->tune();
 405         delete autotuner;
 406 }