X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2Fcsolver.cc;h=b42dbe0974224df3560d5f95b96aed1e5fce56f2;hp=81329914c80acea519b310c0bad122328876aff8;hb=fd09b2b8edb8d7151cb4fdd861da7d643f176295;hpb=cfbb106cf7c1281029b012c47580c9f14df1014b diff --git a/src/csolver.cc b/src/csolver.cc index 8132991..b42dbe0 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -22,6 +22,12 @@ #include "serializer.h" #include "deserializer.h" #include "encodinggraph.h" +#include "ordergraph.h" +#include "orderedge.h" +#include "orderanalysis.h" +#include "elementopt.h" +#include +#include CSolver::CSolver() : boolTrue(BooleanEdge(new BooleanConst(true))), @@ -36,6 +42,7 @@ CSolver::CSolver() : /** This function tears down the solver and the entire AST */ CSolver::~CSolver() { + //serialize(); uint size = allBooleans.getSize(); for (uint i = 0; i < size; i++) { delete allBooleans.get(i); @@ -48,9 +55,7 @@ CSolver::~CSolver() { size = allElements.getSize(); for (uint i = 0; i < size; i++) { - Element* el = allElements.get(i); - model_print("deleting ...%u", i); - ASSERT(el != NULL); + Element *el = allElements.get(i); delete el; } @@ -68,7 +73,6 @@ CSolver::~CSolver() { for (uint i = 0; i < size; i++) { delete allOrders.get(i); } - size = allFunctions.getSize(); for (uint i = 0; i < size; i++) { delete allFunctions.get(i); @@ -78,6 +82,64 @@ CSolver::~CSolver() { delete satEncoder; } +void CSolver::resetSolver() { + //serialize(); + uint size = allBooleans.getSize(); + for (uint i = 0; i < size; i++) { + delete allBooleans.get(i); + } + + size = allSets.getSize(); + for (uint i = 0; i < size; i++) { + delete allSets.get(i); + } + + size = allElements.getSize(); + for (uint i = 0; i < size; i++) { + Element *el = allElements.get(i); + delete el; + } + + size = allTables.getSize(); + for (uint i = 0; i < size; i++) { + delete allTables.get(i); + } + + size = allPredicates.getSize(); + for (uint i = 0; i < size; i++) { + delete allPredicates.get(i); + } + + size = allOrders.getSize(); + for (uint i = 0; i < size; i++) { + delete allOrders.get(i); + } + size = allFunctions.getSize(); + for (uint i = 0; i < size; i++) { + delete allFunctions.get(i); + } + delete boolTrue.getBoolean(); + allBooleans.clear(); + allSets.clear(); + allElements.clear(); + allTables.clear(); + allPredicates.clear(); + allOrders.clear(); + allFunctions.clear(); + constraints.reset(); + activeOrders.reset(); + boolMap.reset(); + elemMap.reset(); + + boolTrue = BooleanEdge(new BooleanConst(true)); + boolFalse = boolTrue.negate(); + unsat = false; + elapsedTime = 0; + tuner = NULL; + satEncoder->resetSATEncoder(); + +} + CSolver *CSolver::clone() { CSolver *copy = new CSolver(); CloneMap map; @@ -90,22 +152,24 @@ CSolver *CSolver::clone() { return copy; } +CSolver *CSolver::deserialize(const char *file) { + model_print("deserializing ...\n"); + Deserializer deserializer(file); + return deserializer.deserialize(); +} + 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; + char buffer[255]; + long long nanotime = getTimeNano(); + int numchars = sprintf(buffer, "DUMP%llu", nanotime); + Serializer serializer(buffer); + SetIteratorBooleanEdge *it = getConstraints(); + while (it->hasNext()) { + BooleanEdge b = it->next(); + serializeBooleanEdge(&serializer, b, true); } -// model_print("deserializing ...\n"); -// { -// Deserializer deserializer("dump"); -// deserializer.deserialize(); -// } + delete it; } Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) { @@ -120,6 +184,10 @@ Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange return set; } +bool CSolver::itemExistInSet(Set *set, uint64_t item){ + return set->exists(item); +} + VarType CSolver::getSetVarType(Set *set) { return set->getType(); } @@ -151,11 +219,14 @@ void CSolver::finalizeMutableSet(MutableSet *set) { Element *CSolver::getElementVar(Set *set) { Element *element = new ElementSet(set); - model_println("%%%%ElementVar:%u", allElements.getSize()); allElements.push(element); return element; } +void CSolver::mustHaveValue(Element *element){ + element->getElementEncoding()->anyValue = true; +} + Set *CSolver::getElementRange (Element *element) { return element->getRange(); } @@ -168,7 +239,6 @@ Element *CSolver::getElementConst(VarType type, uint64_t value) { Element *e = elemMap.get(element); if (e == NULL) { allSets.push(set); - model_println("%%%%ElementConst:%u", allElements.getSize()); allElements.push(element); elemMap.put(element, element); return element; @@ -179,12 +249,12 @@ Element *CSolver::getElementConst(VarType type, uint64_t value) { } } + 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(); - model_println("%%%%ElementFunction:%u", allElements.getSize()); allElements.push(element); elemMap.put(element, element); return element; @@ -194,14 +264,14 @@ Element *CSolver::applyFunction(Function *function, Element **array, uint numArr } } -Function *CSolver::createFunctionOperator(ArithOp op, Set **domain, uint numDomain, Set *range,OverFlowBehavior overflowbehavior) { - Function *function = new FunctionOperator(op, domain, numDomain, range, overflowbehavior); +Function *CSolver::createFunctionOperator(ArithOp op, Set *range, OverFlowBehavior overflowbehavior) { + Function *function = new FunctionOperator(op, range, overflowbehavior); allFunctions.push(function); return function; } -Predicate *CSolver::createPredicateOperator(CompOp op, Set **domain, uint numDomain) { - Predicate *predicate = new PredicateOperator(op, domain,numDomain); +Predicate *CSolver::createPredicateOperator(CompOp op) { + Predicate *predicate = new PredicateOperator(op); allPredicates.push(predicate); return predicate; } @@ -212,14 +282,14 @@ Predicate *CSolver::createPredicateTable(Table *table, UndefinedBehavior behavio return predicate; } -Table *CSolver::createTable(Set **domains, uint numDomain, Set *range) { - Table *table = new Table(domains,numDomain,range); +Table *CSolver::createTable(Set *range) { + Table *table = new Table(range); allTables.push(table); return table; } -Table *CSolver::createTableForPredicate(Set **domains, uint numDomain) { - return createTable(domains, numDomain, NULL); +Table *CSolver::createTableForPredicate() { + return createTable(NULL); } void CSolver::addTableEntry(Table *table, uint64_t *inputs, uint inputSize, uint64_t result) { @@ -282,9 +352,11 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge 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; +static int booleanEdgeCompares(const void *p1, const void *p2) { + BooleanEdge be1 = *(BooleanEdge const *) p1; + BooleanEdge be2 = *(BooleanEdge const *) p2; + uint64_t b1 = be1->id; + uint64_t b2 = be2->id; if (b1 < b2) return -1; else if (b1 == b2) @@ -316,13 +388,11 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint } 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); - } + 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) { @@ -346,12 +416,10 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint if (((BooleanLogic *)b.getBoolean())->replaced) return rewriteLogicalOperation(op, array, asize); } - if (b->type == BOOLCONST) { - if (isTrue(b)) - continue; - else { - return boolFalse; - } + if (isTrue(b)) + continue; + else if (isFalse(b)) { + return boolFalse; } else newarray[newindex++] = b; } @@ -360,7 +428,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint } else if (newindex == 1) { return newarray[0]; } else { - bsdqsort(newarray, newindex, sizeof(BooleanEdge), ptrcompares); + bsdqsort(newarray, newindex, sizeof(BooleanEdge), booleanEdgeCompares); array = newarray; asize = newindex; } @@ -391,16 +459,56 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint } BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t second) { - ASSERT(first != 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 BooleanEdge(constraint); + Boolean *b = boolMap.get(constraint); + + if (b == NULL) { + allBooleans.push(constraint); + boolMap.put(constraint, constraint); + constraint->updateParents(); + if (order->graph != NULL) { + OrderGraph *graph = order->graph; + OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first); + if (from != NULL) { + OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second); + if (to != NULL) { + OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(from, to); + OrderEdge *invedge; + + if (edge != NULL && edge->mustPos) { + replaceBooleanWithTrueNoRemove(constraint); + } else if (edge != NULL && edge->mustNeg) { + replaceBooleanWithFalseNoRemove(constraint); + } else if ((invedge = graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL + && invedge->mustPos) { + replaceBooleanWithFalseNoRemove(constraint); + } + } + } + } + } else { + delete constraint; + constraint = b; + } + + BooleanEdge be = BooleanEdge(constraint); + return negate ? be.negate() : be; } void CSolver::addConstraint(BooleanEdge constraint) { -#ifdef TRACE_DEBUG - model_println("****New Constraint******"); -#endif if (isTrue(constraint)) return; else if (isFalse(constraint)) { @@ -442,36 +550,84 @@ Order *CSolver::createOrder(OrderType type, Set *set) { return order; } +/** Computes static ordering information to allow isTrue/isFalse + queries on newly created orders to work. */ + +void CSolver::inferFixedOrder(Order *order) { + if (order->graph != NULL) { + delete order->graph; + } + order->graph = buildMustOrderGraph(order); + reachMustAnalysis(this, order->graph, true); +} + +void CSolver::inferFixedOrders() { + SetIteratorOrder *orderit = activeOrders.iterator(); + while (orderit->hasNext()) { + Order *order = orderit->next(); + inferFixedOrder(order); + } +} + +#define NANOSEC 1000000000.0 int CSolver::solve() { + long long starttime = getTimeNano(); bool deleteTuner = false; if (tuner == NULL) { tuner = new DefaultTuner(); deleteTuner = true; } - long long startTime = getTimeNano(); - computePolarities(this); + { + SetIteratorOrder *orderit = activeOrders.iterator(); + while (orderit->hasNext()) { + Order *order = orderit->next(); + if (order->graph != NULL) { + delete order->graph; + order->graph = NULL; + } + } + delete orderit; + } + computePolarities(this); + long long time2 = getTimeNano(); + model_print("Polarity time: %f\n", (time2 - starttime) / NANOSEC); Preprocess pp(this); pp.doTransform(); + long long time3 = getTimeNano(); + model_print("Preprocess time: %f\n", (time3 - time2) / NANOSEC); DecomposeOrderTransform dot(this); dot.doTransform(); + long long time4 = getTimeNano(); + model_print("Decompose Order: %f\n", (time4 - time3) / NANOSEC); IntegerEncodingTransform iet(this); iet.doTransform(); + ElementOpt eop(this); + eop.doTransform(); + EncodingGraph eg(this); eg.buildGraph(); eg.encode(); - printConstraints(); + naiveEncodingDecision(this); + long long time5 = getTimeNano(); + model_print("Encoding Graph Time: %f\n", (time5 - time4) / NANOSEC); + + long long startTime = getTimeNano(); satEncoder->encodeAllSATEncoder(this); + long long endTime = getTimeNano(); + + elapsedTime = endTime - startTime; + model_print("Elapse Encode time: %f\n", elapsedTime / NANOSEC); + 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; + model_print("Result Computed in SAT solver: %d\n", result); + if (deleteTuner) { delete tuner; tuner = NULL; @@ -489,7 +645,13 @@ void CSolver::printConstraints() { 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) { @@ -529,3 +691,21 @@ void CSolver::autoTune(uint budget) { autotuner->tune(); delete autotuner; } + +//Set* CSolver::addItemsToRange(Element* element, uint num, ...){ +// va_list args; +// va_start(args, num); +// element->getRange() +// uint setSize = set->getSize(); +// uint newSize = setSize+ num; +// uint64_t members[newSize]; +// for(uint i=0; igetElement(i); +// } +// for( uint i=0; i< num; i++){ +// uint64_t arg = va_arg(args, uint64_t); +// members[setSize+i] = arg; +// } +// va_end(args); +// return createSet(set->getType(), members, newSize); +//}