X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2Fcsolver.cc;h=be4a3a88063882cc05f5cfafca9218724b870f72;hp=c3208b91ec5fdd2747ffc763fa3e3b52dd60291a;hb=77f32c79afdf12f29c040d511cd84f15d703ceb9;hpb=f9546315ab6ece42f48fa8b2e2e53abcd1f00b74 diff --git a/src/csolver.cc b/src/csolver.cc index c3208b9..be4a3a8 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -17,11 +17,15 @@ #include "structs.h" #include "orderresolver.h" #include "integerencoding.h" -#include +#include "qsort.h" +#include "preprocess.h" +#include "serializer.h" +#include "deserializer.h" +#include "encodinggraph.h" CSolver::CSolver() : - boolTrue(new BooleanConst(true)), - boolFalse(new BooleanConst(false)), + boolTrue(BooleanEdge(new BooleanConst(true))), + boolFalse(boolTrue.negate()), unsat(false), tuner(NULL), elapsedTime(0) @@ -67,23 +71,41 @@ CSolver::~CSolver() { delete allFunctions.get(i); } - delete boolTrue; - delete boolFalse; + delete boolTrue.getBoolean(); delete satEncoder; } CSolver *CSolver::clone() { CSolver *copy = new CSolver(); CloneMap map; - SetIteratorBoolean *it = getConstraints(); + SetIteratorBooleanEdge *it = getConstraints(); while (it->hasNext()) { - Boolean *b = it->next(); - copy->addConstraint(b->clone(copy, &map)); + BooleanEdge b = it->next(); + copy->addConstraint(cloneEdge(copy, &map, b)); } delete it; return copy; } +void CSolver::serialize() { + model_print("serializing ...\n"); + { + Serializer serializer("dump"); + SetIteratorBooleanEdge *it = getConstraints(); + while (it->hasNext()) { + BooleanEdge b = it->next(); + serializeBooleanEdge(&serializer, b); + } + delete it; + } + model_print("deserializing ...\n"); + { + Deserializer deserializer("dump"); + deserializer.deserialize(); + } + +} + Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) { Set *set = new Set(type, elements, numelements); allSets.push(set); @@ -96,6 +118,10 @@ Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange return set; } +VarType CSolver::getSetVarType(Set *set) { + return set->getType(); +} + Element *CSolver::createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange) { Set *s = createRangeSet(type, lowrange, highrange); return getElementVar(s); @@ -117,16 +143,25 @@ uint64_t CSolver::createUniqueItem(MutableSet *set) { return element; } +void CSolver::finalizeMutableSet(MutableSet *set) { + set->finalize(); +} + Element *CSolver::getElementVar(Set *set) { Element *element = new ElementSet(set); allElements.push(element); return element; } +Set *CSolver::getElementRange (Element *element) { + return element->getRange(); +} + + Element *CSolver::getElementConst(VarType type, uint64_t value) { uint64_t array[] = {value}; Set *set = new Set(type, array, 1); - Element *element = new ElementConst(value, type, set); + Element *element = new ElementConst(value, set); Element *e = elemMap.get(element); if (e == NULL) { allSets.push(set); @@ -140,10 +175,11 @@ Element *CSolver::getElementConst(VarType type, uint64_t value) { } } -Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus) { +Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) { Element *element = new ElementFunction(function,array,numArrays,overflowstatus); Element *e = elemMap.get(element); if (e == NULL) { + element->updateParents(); allElements.push(element); elemMap.put(element, element); return element; @@ -191,58 +227,59 @@ Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) { return function; } -Boolean *CSolver::getBooleanVar(VarType type) { +BooleanEdge CSolver::getBooleanVar(VarType type) { Boolean *boolean = new BooleanVar(type); allBooleans.push(boolean); - return boolean; + return BooleanEdge(boolean); } -Boolean *CSolver::getBooleanTrue() { +BooleanEdge CSolver::getBooleanTrue() { return boolTrue; } -Boolean *CSolver::getBooleanFalse() { +BooleanEdge CSolver::getBooleanFalse() { return boolFalse; } -Boolean *CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) { - return applyPredicateTable(predicate, inputs, numInputs, NULL); +BooleanEdge CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) { + return applyPredicateTable(predicate, inputs, numInputs, BooleanEdge(NULL)); } -Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) { +BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, BooleanEdge undefinedStatus) { BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus); Boolean *b = boolMap.get(boolean); if (b == NULL) { + boolean->updateParents(); boolMap.put(boolean, boolean); allBooleans.push(boolean); - return boolean; + return BooleanEdge(boolean); } else { delete boolean; - return b; + return BooleanEdge(b); } } -bool CSolver::isTrue(Boolean *b) { - return b->isTrue(); +bool CSolver::isTrue(BooleanEdge b) { + return b.isNegated() ? b->isFalse() : b->isTrue(); } -bool CSolver::isFalse(Boolean *b) { - return b->isFalse(); +bool CSolver::isFalse(BooleanEdge b) { + return b.isNegated() ? b->isTrue() : b->isFalse(); } -Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean *arg1, Boolean *arg2) { - Boolean *array[] = {arg1, arg2}; +BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2) { + BooleanEdge array[] = {arg1, arg2}; return applyLogicalOperation(op, array, 2); } -Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean *arg) { - Boolean *array[] = {arg}; +BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg) { + BooleanEdge array[] = {arg}; return applyLogicalOperation(op, array, 1); } static int ptrcompares(const void *p1, const void *p2) { uintptr_t b1 = *(uintptr_t const *) p1; - uintptr_t b2 = *(uintptr_t const *) p2; + uintptr_t b2 = *(uintptr_t const *) p2; if (b1 < b2) return -1; else if (b1 == b2) @@ -251,32 +288,47 @@ static int ptrcompares(const void *p1, const void *p2) { return 1; } -Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) { - Boolean *newarray[asize]; +BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) { + BooleanEdge newarray[asize]; + memcpy(newarray, array, asize * sizeof(BooleanEdge)); + for (uint i = 0; i < asize; i++) { + BooleanEdge b = newarray[i]; + if (b->type == LOGICOP) { + if (((BooleanLogic *) b.getBoolean())->replaced) { + newarray[i] = doRewrite(newarray[i]); + i--;//Check again + } + } + } + return applyLogicalOperation(op, newarray, asize); +} + +BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) { + BooleanEdge newarray[asize]; switch (op) { case SATC_NOT: { - if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op == SATC_NOT) { - return ((BooleanLogic *) array[0])->inputs.get(0); - } else if (array[0]->type == BOOLCONST) { - return array[0]->isTrue() ? boolFalse : boolTrue; - } - break; + return array[0].negate(); } case SATC_IFF: { for (uint i = 0; i < 2; i++) { if (array[i]->type == BOOLCONST) { - if (array[i]->isTrue()) { + if (isTrue(array[i])) { // It can be undefined return array[1 - i]; - } else { + } else if (isFalse(array[i])) { newarray[0] = array[1 - i]; return applyLogicalOperation(SATC_NOT, newarray, 1); } + } else if (array[i]->type == LOGICOP) { + BooleanLogic *b = (BooleanLogic *)array[i].getBoolean(); + if (b->replaced) { + return rewriteLogicalOperation(op, array, asize); + } } } break; } case SATC_OR: { - for (uint i =0; i type == LOGICOP) { + if (((BooleanLogic *)b.getBoolean())->replaced) + return rewriteLogicalOperation(op, array, asize); + } if (b->type == BOOLCONST) { - if (b->isTrue()) + if (isTrue(b)) continue; - else + else { return boolFalse; + } } else newarray[newindex++] = b; } @@ -298,7 +355,7 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) } else if (newindex == 1) { return newarray[0]; } else { - qsort(newarray, asize, sizeof(Boolean *), ptrcompares); + bsdqsort(newarray, newindex, sizeof(BooleanEdge), ptrcompares); array = newarray; asize = newindex; } @@ -318,38 +375,78 @@ Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) Boolean *boolean = new BooleanLogic(this, op, array, asize); Boolean *b = boolMap.get(boolean); if (b == NULL) { + boolean->updateParents(); boolMap.put(boolean, boolean); allBooleans.push(boolean); - return boolean; + return BooleanEdge(boolean); } else { delete boolean; - return b; + return BooleanEdge(b); } } -Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) { +BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) { + // ASSERT(first != second); + if (first == second) + return getBooleanFalse(); + + bool negate = false; + if (order->type == SATC_TOTAL) { + if (first > second) { + uint64_t tmp = first; + first = second; + second = tmp; + negate = true; + } + } Boolean *constraint = new BooleanOrder(order, first, second); - allBooleans.push(constraint); - return constraint; + Boolean *b = boolMap.get(constraint); + + if (b == NULL) { + allBooleans.push(constraint); + boolMap.put(constraint, constraint); + constraint->updateParents(); + } else { + delete constraint; + constraint = b; + } + + BooleanEdge be = BooleanEdge(constraint); + return negate ? be.negate() : be; } -void CSolver::addConstraint(Boolean *constraint) { - if (constraint == boolTrue) +void CSolver::addConstraint(BooleanEdge constraint) { + if (isTrue(constraint)) return; - else if (constraint == boolFalse) + else if (isFalse(constraint)) { + int t = 0; setUnSAT(); + } else { if (constraint->type == LOGICOP) { - BooleanLogic *b=(BooleanLogic *) constraint; - if (b->op==SATC_AND) { - for(uint i=0;iinputs.getSize();i++) { - addConstraint(b->inputs.get(i)); + BooleanLogic *b = (BooleanLogic *) constraint.getBoolean(); + if (!constraint.isNegated()) { + if (b->op == SATC_AND) { + for (uint i = 0; i < b->inputs.getSize(); i++) { + addConstraint(b->inputs.get(i)); + } + return; } + } + if (b->replaced) { + addConstraint(doRewrite(constraint)); return; } } - constraints.add(constraint); + Boolean *ptr = constraint.getBoolean(); + + if (ptr->boolVal == BV_UNSAT) { + setUnSAT(); + } + + replaceBooleanWithTrueNoRemove(constraint); + constraint->parents.clear(); } } @@ -370,16 +467,24 @@ int CSolver::solve() { long long startTime = getTimeNano(); computePolarities(this); + Preprocess pp(this); + pp.doTransform(); + DecomposeOrderTransform dot(this); dot.doTransform(); - //This leaks like crazy - // IntegerEncodingTransform iet(this); + //IntegerEncodingTransform iet(this); //iet.doTransform(); + //EncodingGraph eg(this); + //eg.buildGraph(); + //eg.encode(); + //printConstraints(); naiveEncodingDecision(this); satEncoder->encodeAllSATEncoder(this); + model_print("Is problem UNSAT after encoding: %d\n", unsat); int result = unsat ? IS_UNSAT : satEncoder->solve(); + model_print("Result Computed in CSolver: %d\n", result); long long finishTime = getTimeNano(); elapsedTime = finishTime - startTime; if (deleteTuner) { @@ -389,6 +494,26 @@ int CSolver::solve() { return result; } +void CSolver::printConstraints() { + SetIteratorBooleanEdge *it = getConstraints(); + while (it->hasNext()) { + BooleanEdge b = it->next(); + if (b.isNegated()) + model_print("!"); + b->print(); + model_print("\n"); + } + delete it; + +} + +void CSolver::printConstraint(BooleanEdge b) { + if (b.isNegated()) + model_print("!"); + b->print(); + model_print("\n"); +} + uint64_t CSolver::getElementValue(Element *element) { switch (element->type) { case ELEMSET: @@ -401,7 +526,8 @@ uint64_t CSolver::getElementValue(Element *element) { exit(-1); } -bool CSolver::getBooleanValue(Boolean *boolean) { +bool CSolver::getBooleanValue(BooleanEdge bedge) { + Boolean *boolean = bedge.getBoolean(); switch (boolean->type) { case BOOLEANVAR: return getBooleanVariableValueSATTranslator(this, boolean);