X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2Fcsolver.cc;h=a8ffc492c156064cb6fdb693b7084b76c737d478;hp=7c13eae9c8bebe007000abf801f735522dd36d67;hb=e0ee8656d201f77504bd239612969ce43636c324;hpb=d7ac61501176eddf35c154d3bbd2b87c566b60ce diff --git a/src/csolver.cc b/src/csolver.cc index 7c13eae..a8ffc49 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -25,6 +25,8 @@ #include "ordergraph.h" #include "orderedge.h" #include "orderanalysis.h" +#include "elementopt.h" +#include "varorderingopt.h" #include #include @@ -33,7 +35,8 @@ CSolver::CSolver() : boolFalse(boolTrue.negate()), unsat(false), tuner(NULL), - elapsedTime(0) + elapsedTime(0), + satsolverTimeout(NOTIMEOUT) { satEncoder = new SATEncoder(this); } @@ -152,7 +155,7 @@ CSolver *CSolver::clone() { } CSolver *CSolver::deserialize(const char *file) { - model_print("deserializing ...\n"); + model_print("deserializing %s ...\n", file); Deserializer deserializer(file); return deserializer.deserialize(); } @@ -183,8 +186,8 @@ 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); +bool CSolver::itemExistInSet(Set *set, uint64_t item) { + return set->exists(item); } VarType CSolver::getSetVarType(Set *set) { @@ -222,8 +225,8 @@ Element *CSolver::getElementVar(Set *set) { return element; } -void CSolver::mustHaveValue(Element *element){ - element->getElementEncoding()->anyValue = true; +void CSolver::mustHaveValue(Element *element) { + element->anyValue = true; } Set *CSolver::getElementRange (Element *element) { @@ -250,6 +253,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) { @@ -263,14 +267,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; } @@ -281,14 +285,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) { @@ -511,7 +515,6 @@ void CSolver::addConstraint(BooleanEdge constraint) { if (isTrue(constraint)) return; else if (isFalse(constraint)) { - int t = 0; setUnSAT(); } else { @@ -519,8 +522,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; } @@ -570,7 +579,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(); @@ -590,40 +599,47 @@ 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(); + + VarOrderingOpt bor(this, satEncoder); + bor.doTransform(); + + time2 = getTimeNano(); + model_print("Encoding Graph Time: %f\n", (time2 - time1) / NANOSEC); + satEncoder->encodeAllSATEncoder(this); - long long endTime = getTimeNano(); + time1 = getTimeNano(); - elapsedTime = endTime - startTime; - model_print("Elapse Encode time: %f\n", elapsedTime / NANOSEC); + model_print("Elapse Encode time: %f\n", (time1 - startTime) / NANOSEC); model_print("Is problem UNSAT after encoding: %d\n", unsat); - int result = unsat ? IS_UNSAT : satEncoder->solve(); - model_print("Result Computed in SAT solver: %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; @@ -635,19 +651,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) { @@ -688,20 +698,4 @@ void CSolver::autoTune(uint budget) { 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); -//} \ No newline at end of file +