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