X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2Fcsolver.cc;h=533fc4b8dfd0023c3b66498c898599056fb7b2c4;hb=fcd1280d92704662fec5ee8bac68cd44619cd5c2;hp=575a12b6f347714e5711eccd08c6131ec381de81;hpb=bdb495e03a14ca5adf4b4b4a53233ed373121642;p=satune.git diff --git a/src/csolver.cc b/src/csolver.cc index 575a12b..533fc4b 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -21,6 +21,8 @@ #include "preprocess.h" #include "serializer.h" #include "deserializer.h" +#include "encodinggraph.h" +#include CSolver::CSolver() : boolTrue(BooleanEdge(new BooleanConst(true))), @@ -47,7 +49,8 @@ CSolver::~CSolver() { size = allElements.getSize(); for (uint i = 0; i < size; i++) { - delete allElements.get(i); + Element* el = allElements.get(i); + delete el; } size = allTables.getSize(); @@ -64,7 +67,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); @@ -86,23 +88,27 @@ 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; - } - model_print("deserializing ...\n"); - { - Deserializer deserializer("dump"); - deserializer.deserialize(); + char buffer[255]; + struct timespec t; + clock_gettime(CLOCK_REALTIME, &t); + + unsigned long long nanotime=t.tv_sec*1000000000+t.tv_nsec; + int numchars=sprintf(buffer, "DUMP%llu", nanotime); + Serializer serializer(buffer); + SetIteratorBooleanEdge *it = getConstraints(); + while (it->hasNext()) { + BooleanEdge b = it->next(); + serializeBooleanEdge(&serializer, b, true); } - + delete it; } Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) { @@ -117,6 +123,10 @@ 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); @@ -138,7 +148,7 @@ uint64_t CSolver::createUniqueItem(MutableSet *set) { return element; } -void CSolver::finalizeMutableSet(MutableSet* set){ +void CSolver::finalizeMutableSet(MutableSet *set) { set->finalize(); } @@ -148,6 +158,11 @@ Element *CSolver::getElementVar(Set *set) { return element; } +Set *CSolver::getElementRange (Element *element) { + return element->getRange(); +} + + Element *CSolver::getElementConst(VarType type, uint64_t value) { uint64_t array[] = {value}; Set *set = new Set(type, array, 1); @@ -165,6 +180,7 @@ 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); @@ -250,11 +266,11 @@ BooleanEdge CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, } bool CSolver::isTrue(BooleanEdge b) { - return b.isNegated()?b->isFalse():b->isTrue(); + return b.isNegated() ? b->isFalse() : b->isTrue(); } bool CSolver::isFalse(BooleanEdge b) { - return b.isNegated()?b->isTrue():b->isFalse(); + return b.isNegated() ? b->isTrue() : b->isFalse(); } BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg1, BooleanEdge arg2) { @@ -269,7 +285,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge arg) { static int ptrcompares(const void *p1, const void *p2) { uintptr_t b1 = *(uintptr_t const *) p1; - uintptr_t b2 = *(uintptr_t const *) p2; + uintptr_t b2 = *(uintptr_t const *) p2; if (b1 < b2) return -1; else if (b1 == b2) @@ -278,11 +294,11 @@ static int ptrcompares(const void *p1, const void *p2) { return 1; } -BooleanEdge CSolver::rewriteLogicalOperation(LogicOp op, BooleanEdge * array, uint asize) { +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]; + 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]); @@ -301,15 +317,13 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint } 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); - } + 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(); + BooleanLogic *b = (BooleanLogic *)array[i].getBoolean(); if (b->replaced) { return rewriteLogicalOperation(op, array, asize); } @@ -318,7 +332,7 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint break; } case SATC_OR: { - for (uint i =0; i replaced) return rewriteLogicalOperation(op, array, asize); } - if (b->type == BOOLCONST) { - if (b->isTrue()) - continue; - else - return boolFalse; + if (isTrue(b)) + continue; + else if (isFalse(b)) { + return boolFalse; } else newarray[newindex++] = b; } @@ -375,22 +388,48 @@ BooleanEdge CSolver::applyLogicalOperation(LogicOp op, BooleanEdge *array, uint } BooleanEdge CSolver::orderConstraint(Order *order, uint64_t first, uint64_t 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(); + } 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)) + else if (isFalse(constraint)) { + int t = 0; setUnSAT(); + } else { if (constraint->type == LOGICOP) { - BooleanLogic *b=(BooleanLogic *) constraint.getBoolean(); + BooleanLogic *b = (BooleanLogic *) constraint.getBoolean(); if (!constraint.isNegated()) { - if (b->op==SATC_AND) { - for(uint i=0;iinputs.getSize();i++) { + if (b->op == SATC_AND) { + for (uint i = 0; i < b->inputs.getSize(); i++) { addConstraint(b->inputs.get(i)); } return; @@ -402,11 +441,12 @@ void CSolver::addConstraint(BooleanEdge constraint) { } } constraints.add(constraint); - Boolean *ptr=constraint.getBoolean(); - - if (ptr->boolVal == BV_UNSAT) + Boolean *ptr = constraint.getBoolean(); + + if (ptr->boolVal == BV_UNSAT) { setUnSAT(); - + } + replaceBooleanWithTrueNoRemove(constraint); constraint->parents.clear(); } @@ -425,22 +465,28 @@ int CSolver::solve() { tuner = new DefaultTuner(); deleteTuner = true; } - + long long startTime = getTimeNano(); computePolarities(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); 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) { @@ -450,6 +496,25 @@ int CSolver::solve() { 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; +} + +void CSolver::printConstraint(BooleanEdge b) { + if (b.isNegated()) + model_print("!"); + b->print(); + model_print("\n"); +} + uint64_t CSolver::getElementValue(Element *element) { switch (element->type) { case ELEMSET: @@ -463,7 +528,7 @@ uint64_t CSolver::getElementValue(Element *element) { } bool CSolver::getBooleanValue(BooleanEdge bedge) { - Boolean *boolean=bedge.getBoolean(); + Boolean *boolean = bedge.getBoolean(); switch (boolean->type) { case BOOLEANVAR: return getBooleanVariableValueSATTranslator(this, boolean);