X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2Fcsolver.cc;h=62f76ab2223065363a8fcbdcfccdba0cb2e5b862;hb=5f6c2114c698f112e4c763c9c464b6b917e7150d;hp=06ecf78dddbb3b668ec36650879d81e5004affb2;hpb=1baf38f8e307dbf035530c976979be00f0a1d09e;p=satune.git diff --git a/src/csolver.cc b/src/csolver.cc index 06ecf78..62f76ab 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -11,10 +11,17 @@ #include "sattranslator.h" #include "tunable.h" #include "polarityassignment.h" -#include "orderdecompose.h" +#include "decomposeordertransform.h" #include "autotuner.h" +#include "astops.h" +#include "structs.h" +#include "orderresolver.h" +#include "integerencoding.h" +#include "qsort.h" CSolver::CSolver() : + boolTrue(BooleanEdge(new BooleanConst(true))), + boolFalse(boolTrue.negate()), unsat(false), tuner(NULL), elapsedTime(0) @@ -60,16 +67,17 @@ CSolver::~CSolver() { delete allFunctions.get(i); } + delete boolTrue.getBoolean(); delete satEncoder; } CSolver *CSolver::clone() { CSolver *copy = new CSolver(); CloneMap map; - HSIteratorBoolean *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; @@ -87,6 +95,11 @@ Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange return set; } +Element *CSolver::createRangeVar(VarType type, uint64_t lowrange, uint64_t highrange) { + Set *s = createRangeSet(type, lowrange, highrange); + return getElementVar(s); +} + MutableSet *CSolver::createMutableSet(VarType type) { MutableSet *set = new MutableSet(type); allSets.push(set); @@ -98,7 +111,7 @@ void CSolver::addItem(MutableSet *set, uint64_t element) { } uint64_t CSolver::createUniqueItem(MutableSet *set) { - uint64_t element = set->low++; + uint64_t element = set->getNewUniqueItem(); set->addElementMSet(element); return element; } @@ -126,10 +139,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; @@ -177,68 +191,224 @@ 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::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) { +BooleanEdge CSolver::getBooleanTrue() { + return boolTrue; +} + +BooleanEdge CSolver::getBooleanFalse() { + return boolFalse; +} + +BooleanEdge CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) { return applyPredicateTable(predicate, inputs, numInputs, 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); + 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(BooleanEdge b) { + return b.isNegated()?b->isFalse():b->isTrue(); +} + +bool CSolver::isFalse(BooleanEdge b) { + return b.isNegated()?b->isTrue():b->isFalse(); +} + +BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2) { + BooleanEdge array[] = {arg1, arg2}; + return applyLogicalOperation(op, array, 2); +} + +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; + if (b1 < b2) + return -1; + else if (b1 == b2) + return 0; + else + return 1; +} + +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); } -Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) { +BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint asize) { + BooleanEdge newarray[asize]; + switch (op) { + case SATC_NOT: { + return array[0].negate(); + } + case SATC_IFF: { + for (uint i = 0; i < 2; i++) { + if (array[i]->type == BOOLCONST) { + if (array[i]->isTrue()) { + return array[1 - i]; + } else { + 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()) + continue; + else + return boolFalse; + } else + newarray[newindex++] = b; + } + if (newindex == 0) { + return boolTrue; + } else if (newindex == 1) { + return newarray[0]; + } else { + bsdqsort(newarray, newindex, sizeof(BooleanEdge), ptrcompares); + array = newarray; + asize = newindex; + } + break; + } + case SATC_XOR: { + //handle by translation + return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_IFF, array, asize)); + } + case SATC_IMPLIES: { + //handle by translation + return applyLogicalOperation(SATC_OR, applyLogicalOperation(SATC_NOT, array[0]), array[1]); + } + } + + ASSERT(asize != 0); 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) { Boolean *constraint = new BooleanOrder(order, first, second); allBooleans.push(constraint); - return constraint; + return BooleanEdge(constraint); } -void CSolver::addConstraint(Boolean *constraint) { - constraints.add(constraint); +void CSolver::addConstraint(BooleanEdge constraint) { + if (isTrue(constraint)) + return; + else if (isFalse(constraint)) + setUnSAT(); + else { + if (constraint->type == LOGICOP) { + BooleanLogic *b=(BooleanLogic *) constraint.getBoolean(); + if (!constraint.isNegated()) { + if (b->op==SATC_AND) { + for(uint i=0;iinputs.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(); + } } Order *CSolver::createOrder(OrderType type, Set *set) { Order *order = new Order(type, set); allOrders.push(order); + activeOrders.add(order); return order; } -int CSolver::startEncoding() { +int CSolver::solve() { bool deleteTuner = false; if (tuner == NULL) { tuner = new DefaultTuner(); deleteTuner = true; } - + long long startTime = getTimeNano(); computePolarities(this); - orderAnalysis(this); + + DecomposeOrderTransform dot(this); + dot.doTransform(); + + IntegerEncodingTransform iet(this); + iet.doTransform(); + naiveEncodingDecision(this); satEncoder->encodeAllSATEncoder(this); int result = unsat ? IS_UNSAT : satEncoder->solve(); @@ -263,7 +433,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); @@ -273,8 +444,8 @@ bool CSolver::getBooleanValue(Boolean *boolean) { exit(-1); } -HappenedBefore CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) { - return getOrderConstraintValueSATTranslator(this, order, first, second); +bool CSolver::getOrderConstraintValue(Order *order, uint64_t first, uint64_t second) { + return order->encoding.resolver->resolveOrder(first, second); } long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); } @@ -282,7 +453,7 @@ long long CSolver::getEncodeTime() { return satEncoder->getEncodeTime(); } long long CSolver::getSolveTime() { return satEncoder->getSolveTime(); } void CSolver::autoTune(uint budget) { - AutoTuner * autotuner=new AutoTuner(budget); + AutoTuner *autotuner = new AutoTuner(budget); autotuner->addProblem(this); autotuner->tune(); delete autotuner;