X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2Fcsolver.cc;h=9f374cc00df78fc08ac6c7097f0e78aaa4b12b2d;hp=e4e045293ab1bf846abf2b4a6ffa182e7bd66e5e;hb=9eb16333c26996a97567f88d0f2e62e72eb9a9e6;hpb=6372bfaf0fe5c6e24bd46005e95209316d8d5a9a diff --git a/src/csolver.cc b/src/csolver.cc index e4e0452..9f374cc 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -25,14 +25,17 @@ #include "ordergraph.h" #include "orderedge.h" #include "orderanalysis.h" +#include "elementopt.h" #include +#include CSolver::CSolver() : boolTrue(BooleanEdge(new BooleanConst(true))), boolFalse(boolTrue.negate()), unsat(false), tuner(NULL), - elapsedTime(0) + elapsedTime(0), + satsolverTimeout(NOTIMEOUT) { satEncoder = new SATEncoder(this); } @@ -53,7 +56,7 @@ CSolver::~CSolver() { size = allElements.getSize(); for (uint i = 0; i < size; i++) { - Element* el = allElements.get(i); + Element *el = allElements.get(i); delete el; } @@ -80,9 +83,9 @@ CSolver::~CSolver() { delete satEncoder; } -void CSolver::resetSolver(){ - //serialize(); - uint size = allBooleans.getSize(); +void CSolver::resetSolver() { + //serialize(); + uint size = allBooleans.getSize(); for (uint i = 0; i < size; i++) { delete allBooleans.get(i); } @@ -94,7 +97,7 @@ void CSolver::resetSolver(){ size = allElements.getSize(); for (uint i = 0; i < size; i++) { - Element* el = allElements.get(i); + Element *el = allElements.get(i); delete el; } @@ -117,25 +120,25 @@ void CSolver::resetSolver(){ 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(); + 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)); + + boolTrue = BooleanEdge(new BooleanConst(true)); boolFalse = boolTrue.negate(); - unsat = false; - elapsedTime = 0; - tuner = NULL; - satEncoder->resetSATEncoder(); - + unsat = false; + elapsedTime = 0; + tuner = NULL; + satEncoder->resetSATEncoder(); + } CSolver *CSolver::clone() { @@ -150,8 +153,8 @@ CSolver *CSolver::clone() { return copy; } -CSolver* CSolver::deserialize(const char * file){ - model_print("deserializing ...\n"); +CSolver *CSolver::deserialize(const char *file) { + model_print("deserializing %s ...\n", file); Deserializer deserializer(file); return deserializer.deserialize(); } @@ -159,8 +162,8 @@ CSolver* CSolver::deserialize(const char * file){ void CSolver::serialize() { model_print("serializing ...\n"); char buffer[255]; - long long nanotime=getTimeNano(); - int numchars=sprintf(buffer, "DUMP%llu", nanotime); + long long nanotime = getTimeNano(); + int numchars = sprintf(buffer, "DUMP%llu", nanotime); Serializer serializer(buffer); SetIteratorBooleanEdge *it = getConstraints(); while (it->hasNext()) { @@ -182,6 +185,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(); } @@ -217,6 +224,10 @@ Element *CSolver::getElementVar(Set *set) { return element; } +void CSolver::mustHaveValue(Element *element) { + element->anyValue = true; +} + Set *CSolver::getElementRange (Element *element) { return element->getRange(); } @@ -241,6 +252,7 @@ Element *CSolver::getElementConst(VarType type, uint64_t value) { Element *CSolver::applyFunction(Function *function, Element **array, uint numArrays, BooleanEdge overflowstatus) { + ASSERT(numArrays == 2); Element *element = new ElementFunction(function,array,numArrays,overflowstatus); Element *e = elemMap.get(element); if (e == NULL) { @@ -254,14 +266,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; } @@ -272,14 +284,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) { @@ -342,9 +354,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) @@ -416,7 +430,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; } @@ -468,19 +482,19 @@ BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t seco boolMap.put(constraint, constraint); constraint->updateParents(); if (order->graph != NULL) { - OrderGraph *graph=order->graph; - OrderNode *from=graph->lookupOrderNodeFromOrderGraph(first); + OrderGraph *graph = order->graph; + OrderNode *from = graph->lookupOrderNodeFromOrderGraph(first); if (from != NULL) { - OrderNode *to=graph->lookupOrderNodeFromOrderGraph(second); + OrderNode *to = graph->lookupOrderNodeFromOrderGraph(second); if (to != NULL) { - OrderEdge *edge=graph->lookupOrderEdgeFromOrderGraph(from, to); + 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 + } else if ((invedge = graph->lookupOrderEdgeFromOrderGraph(to, from)) != NULL && invedge->mustPos) { replaceBooleanWithFalseNoRemove(constraint); } @@ -500,7 +514,6 @@ void CSolver::addConstraint(BooleanEdge constraint) { if (isTrue(constraint)) return; else if (isFalse(constraint)) { - int t = 0; setUnSAT(); } else { @@ -508,8 +521,14 @@ void CSolver::addConstraint(BooleanEdge constraint) { 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)); + uint size = b->inputs.getSize(); + //Handle potential concurrent modification + BooleanEdge array[size]; + for (uint i = 0; i < size; i++) { + array[i] = b->inputs.get(i); + } + for (uint i = 0; i < size; i++) { + addConstraint(array[i]); } return; } @@ -539,7 +558,7 @@ Order *CSolver::createOrder(OrderType type, Set *set) { } /** Computes static ordering information to allow isTrue/isFalse - queries on newly created orders to work. */ + queries on newly created orders to work. */ void CSolver::inferFixedOrder(Order *order) { if (order->graph != NULL) { @@ -548,7 +567,7 @@ void CSolver::inferFixedOrder(Order *order) { order->graph = buildMustOrderGraph(order); reachMustAnalysis(this, order->graph, true); } - + void CSolver::inferFixedOrders() { SetIteratorOrder *orderit = activeOrders.iterator(); while (orderit->hasNext()) { @@ -559,7 +578,7 @@ void CSolver::inferFixedOrders() { #define NANOSEC 1000000000.0 int CSolver::solve() { - long long starttime = getTimeNano(); + long long startTime = getTimeNano(); bool deleteTuner = false; if (tuner == NULL) { tuner = new DefaultTuner(); @@ -578,42 +597,45 @@ int CSolver::solve() { } delete orderit; } - computePolarities(this); - long long time2 = getTimeNano(); - model_print("Polarity time: %f\n", (time2-starttime)/NANOSEC); + long long time1 = getTimeNano(); + model_print("Polarity time: %f\n", (time1 - startTime) / NANOSEC); Preprocess pp(this); pp.doTransform(); - long long time3 = getTimeNano(); - model_print("Preprocess time: %f\n", (time3-time2)/NANOSEC); - + long long time2 = getTimeNano(); + model_print("Preprocess time: %f\n", (time2 - time1) / NANOSEC); + DecomposeOrderTransform dot(this); dot.doTransform(); - long long time4 = getTimeNano(); - model_print("Decompose Order: %f\n", (time4-time3)/NANOSEC); + time1 = getTimeNano(); + model_print("Decompose Order: %f\n", (time1 - time2) / NANOSEC); IntegerEncodingTransform iet(this); iet.doTransform(); + ElementOpt eop(this); + eop.doTransform(); + EncodingGraph eg(this); - eg.buildGraph(); eg.encode(); naiveEncodingDecision(this); - long long time5 = getTimeNano(); - model_print("Encoding Graph Time: %f\n", (time5-time4)/NANOSEC); - - long long startTime = getTimeNano(); +// eg.validate(); + + time2 = getTimeNano(); + model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC); + satEncoder->encodeAllSATEncoder(this); - long long endTime = getTimeNano(); + time1 = getTimeNano(); + + model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC); - 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); - + int result = unsat ? IS_UNSAT : satEncoder->solve(satsolverTimeout); + model_print("Result Computed in SAT solver:\t%s\n", result == IS_SAT? "SAT" : result == IS_INDETER? "INDETERMINATE" : " UNSAT"); + time2 = getTimeNano(); + elapsedTime = time2 - startTime; + model_print("CSOLVER solve time: %f\n", elapsedTime / NANOSEC); if (deleteTuner) { delete tuner; tuner = NULL; @@ -625,19 +647,13 @@ void CSolver::printConstraints() { SetIteratorBooleanEdge *it = getConstraints(); while (it->hasNext()) { BooleanEdge b = it->next(); - if (b.isNegated()) - model_print("!"); - b->print(); - model_print("\n"); + b.print(); } delete it; } void CSolver::printConstraint(BooleanEdge b) { - if (b.isNegated()) - model_print("!"); - b->print(); - model_print("\n"); + b.print(); } uint64_t CSolver::getElementValue(Element *element) { @@ -677,3 +693,5 @@ void CSolver::autoTune(uint budget) { autotuner->tune(); delete autotuner; } + +