X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2Fcsolver.cc;h=756798b6297b510884c5fc6d2e6a93c40aa57c23;hp=cdbb919eac5c48fb80bbeab7fc259de3907b2a34;hb=52bb7ec21876cab449bbe9f14e0d28f623d46af5;hpb=c0e8b50c4010f03bec0d733ec3e677ce090577ba diff --git a/src/csolver.cc b/src/csolver.cc index cdbb919..756798b 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -11,11 +11,26 @@ #include "sattranslator.h" #include "tunable.h" #include "polarityassignment.h" -#include "orderdecompose.h" - -CSolver::CSolver() : unsat(false) { - tuner = allocTuner(); - satEncoder = allocSATEncoder(this); +#include "decomposeordertransform.h" +#include "autotuner.h" +#include "astops.h" +#include "structs.h" +#include "orderresolver.h" +#include "integerencoding.h" +#include "qsort.h" +#include "preprocess.h" +#include "serializer.h" +#include "deserializer.h" +#include "encodinggraph.h" + +CSolver::CSolver() : + boolTrue(BooleanEdge(new BooleanConst(true))), + boolFalse(boolTrue.negate()), + unsat(false), + tuner(NULL), + elapsedTime(0) +{ + satEncoder = new SATEncoder(this); } /** This function tears down the solver and the entire AST */ @@ -56,8 +71,39 @@ CSolver::~CSolver() { delete allFunctions.get(i); } - deleteSATEncoder(satEncoder); - deleteTuner(tuner); + delete boolTrue.getBoolean(); + delete satEncoder; +} + +CSolver *CSolver::clone() { + CSolver *copy = new CSolver(); + CloneMap map; + SetIteratorBooleanEdge *it = getConstraints(); + while (it->hasNext()) { + 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) { @@ -72,6 +118,15 @@ 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); +} + MutableSet *CSolver::createMutableSet(VarType type) { MutableSet *set = new MutableSet(type); allSets.push(set); @@ -83,27 +138,55 @@ 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; } +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) { - Element *element = new ElementConst(value, type); - allElements.push(element); - return element; + uint64_t array[] = {value}; + Set *set = new Set(type, array, 1); + Element *element = new ElementConst(value, set); + Element *e = elemMap.get(element); + if (e == NULL) { + allSets.push(set); + allElements.push(element); + elemMap.put(element, element); + return element; + } else { + delete set; + delete element; + return e; + } } -Boolean *CSolver::getBooleanVar(VarType type) { - Boolean *boolean = new BooleanVar(type); - allBooleans.push(boolean); - return boolean; +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; + } else { + delete element; + return e; + } } Function *CSolver::createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) { @@ -144,58 +227,285 @@ Function *CSolver::completeTable(Table *table, UndefinedBehavior behavior) { return function; } -Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, Boolean *overflowstatus) { - Element *element = new ElementFunction(function,array,numArrays,overflowstatus); - allElements.push(element); - return element; +BooleanEdge CSolver::getBooleanVar(VarType type) { + Boolean *boolean = new BooleanVar(type); + allBooleans.push(boolean); + return BooleanEdge(boolean); } -Boolean *CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) { - return applyPredicateTable(predicate, inputs, numInputs, NULL); +BooleanEdge CSolver::getBooleanTrue() { + return boolTrue; } -Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) { - Boolean *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus); - allBooleans.push(boolean); - return boolean; +BooleanEdge CSolver::getBooleanFalse() { + return boolFalse; +} + +BooleanEdge CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint numInputs) { + return applyPredicateTable(predicate, inputs, numInputs, BooleanEdge(NULL)); +} + +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 BooleanEdge(boolean); + } else { + delete boolean; + 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(); } -Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) { - return new BooleanLogic(this, op, array, asize); +BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2) { + BooleanEdge array[] = {arg1, arg2}; + return applyLogicalOperation(op, array, 2); } -void CSolver::addConstraint(Boolean *constraint) { - constraints.add(constraint); +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); +} + +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 (isTrue(array[i])) { // It can be undefined + return array[1 - i]; + } 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 < asize; i++) { + newarray[i] = applyLogicalOperation(SATC_NOT, array[i]); + } + return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize)); + } + case SATC_AND: { + uint newindex = 0; + for (uint i = 0; i < asize; i++) { + BooleanEdge b = array[i]; + if (b->type == LOGICOP) { + if (((BooleanLogic *)b.getBoolean())->replaced) + return rewriteLogicalOperation(op, array, asize); + } + if (b->type == BOOLCONST) { + if (isTrue(b)) + 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 BooleanEdge(boolean); + } else { + delete boolean; + return BooleanEdge(b); + } +} + +BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) { + ASSERT(first != second); + 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); + 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(BooleanEdge constraint) { + if (isTrue(constraint)) + return; + else if (isFalse(constraint)) { + int t = 0; + setUnSAT(); + } + else { + if (constraint->type == LOGICOP) { + 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(); + } } Order *CSolver::createOrder(OrderType type, Set *set) { Order *order = new Order(type, set); allOrders.push(order); + activeOrders.add(order); return order; } -Boolean *CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) { - Boolean *constraint = new BooleanOrder(order, first, second); - allBooleans.push(constraint); - return constraint; -} +int CSolver::solve() { + bool deleteTuner = false; + if (tuner == NULL) { + tuner = new DefaultTuner(); + deleteTuner = true; + } -int CSolver::startEncoding() { + long long startTime = getTimeNano(); computePolarities(this); - orderAnalysis(this); + + Preprocess pp(this); + pp.doTransform(); + + DecomposeOrderTransform dot(this); + dot.doTransform(); + + IntegerEncodingTransform iet(this); + iet.doTransform(); + + EncodingGraph eg(this); + eg.buildGraph(); + eg.encode(); + printConstraints(); naiveEncodingDecision(this); - encodeAllSATEncoder(this, satEncoder); - int result = solveCNF(satEncoder->cnf); - model_print("sat_solver's result:%d\tsolutionSize=%d\n", result, satEncoder->cnf->solver->solutionsize); - for (int i = 1; i <= satEncoder->cnf->solver->solutionsize; i++) { - model_print("%d, ", satEncoder->cnf->solver->solution[i]); + 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) { + delete tuner; + tuner = NULL; } - model_print("\n"); 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; + +} + uint64_t CSolver::getElementValue(Element *element) { - switch (GETELEMENTTYPE(element)) { + switch (element->type) { case ELEMSET: case ELEMCONST: case ELEMFUNCRETURN: @@ -206,8 +516,9 @@ uint64_t CSolver::getElementValue(Element *element) { exit(-1); } -bool CSolver::getBooleanValue(Boolean *boolean) { - switch (GETBOOLEANTYPE(boolean)) { +bool CSolver::getBooleanValue(BooleanEdge bedge) { + Boolean *boolean = bedge.getBoolean(); + switch (boolean->type) { case BOOLEANVAR: return getBooleanVariableValueSATTranslator(this, boolean); default: @@ -216,7 +527,17 @@ 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(); } + +long long CSolver::getSolveTime() { return satEncoder->getSolveTime(); } + +void CSolver::autoTune(uint budget) { + AutoTuner *autotuner = new AutoTuner(budget); + autotuner->addProblem(this); + autotuner->tune(); + delete autotuner; +}