X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2Fcsolver.cc;h=c3208b91ec5fdd2747ffc763fa3e3b52dd60291a;hb=f9546315ab6ece42f48fa8b2e2e53abcd1f00b74;hp=5ee5157d31f29246f3d6dddd0c7058947d217e6f;hpb=d0f23c6eaff8ec5c1721d1fd92ceb05eca6db316;p=satune.git diff --git a/src/csolver.cc b/src/csolver.cc index 5ee5157..c3208b9 100644 --- a/src/csolver.cc +++ b/src/csolver.cc @@ -11,10 +11,13 @@ #include "sattranslator.h" #include "tunable.h" #include "polarityassignment.h" -#include "analyzer.h" +#include "decomposeordertransform.h" #include "autotuner.h" #include "astops.h" #include "structs.h" +#include "orderresolver.h" +#include "integerencoding.h" +#include CSolver::CSolver() : boolTrue(new BooleanConst(true)), @@ -93,6 +96,11 @@ Set *CSolver::createRangeSet(VarType type, uint64_t lowrange, uint64_t highrange return set; } +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); @@ -203,7 +211,7 @@ Boolean *CSolver::applyPredicate(Predicate *predicate, Element **inputs, uint nu Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, uint numInputs, Boolean *undefinedStatus) { BooleanPredicate *boolean = new BooleanPredicate(predicate, inputs, numInputs, undefinedStatus); - Boolean * b = boolMap.get(boolean); + Boolean *b = boolMap.get(boolean); if (b == NULL) { boolMap.put(boolean, boolean); allBooleans.push(boolean); @@ -214,113 +222,105 @@ Boolean *CSolver::applyPredicateTable(Predicate *predicate, Element **inputs, ui } } +bool CSolver::isTrue(Boolean *b) { + return b->isTrue(); +} + +bool CSolver::isFalse(Boolean *b) { + return b->isFalse(); +} + +Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean *arg1, Boolean *arg2) { + Boolean *array[] = {arg1, arg2}; + return applyLogicalOperation(op, array, 2); +} + +Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean *arg) { + Boolean *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; +} + Boolean *CSolver::applyLogicalOperation(LogicOp op, Boolean **array, uint asize) { - Boolean * newarray[asize]; - switch(op) { + Boolean *newarray[asize]; + switch (op) { case SATC_NOT: { - if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op==SATC_NOT) { + if (array[0]->type == LOGICOP && ((BooleanLogic *)array[0])->op == SATC_NOT) { return ((BooleanLogic *) array[0])->inputs.get(0); } else if (array[0]->type == BOOLCONST) { - bool isTrue = ((BooleanConst *) array[0])->isTrue; - return isTrue ? boolFalse : boolTrue; + return array[0]->isTrue() ? boolFalse : boolTrue; } break; } - case SATC_XOR: { - for(uint i=0;i<2;i++) { + case SATC_IFF: { + for (uint i = 0; i < 2; i++) { if (array[i]->type == BOOLCONST) { - bool isTrue = ((BooleanConst *) array[i])->isTrue; - if (isTrue) { - newarray[0]=array[1-i]; + if (array[i]->isTrue()) { + return array[1 - i]; + } else { + newarray[0] = array[1 - i]; return applyLogicalOperation(SATC_NOT, newarray, 1); - } else - return array[1-i]; + } } } break; } case SATC_OR: { - uint newindex=0; - for(uint i=0;itype == BOOLCONST) { - bool isTrue = ((BooleanConst *) b)->isTrue; - if (isTrue) - return b; - else - continue; - } else - newarray[newindex++]=b; + for (uint i =0; i type==BOOLCONST) && ((BooleanLogic *)newarray[0])->op == SATC_NOT; - bool isNot1 = (newarray[1]->type==BOOLCONST) && ((BooleanLogic *)newarray[1])->op == SATC_NOT; - - if (isNot0 != isNot1) { - if (isNot0) { - newarray[0] = ((BooleanLogic *) newarray[0])->inputs.get(0); - } else { - Boolean *tmp = ((BooleanLogic *) array[1])->inputs.get(0); - array[1] = array[0]; - array[0] = tmp; - } - return applyLogicalOperation(SATC_IMPLIES, newarray, 2); - } - } else { - array = newarray; - asize = newindex; - } - break; + return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_AND, newarray, asize)); } case SATC_AND: { - uint newindex=0; - for(uint i=0;itype == BOOLCONST) { - bool isTrue = ((BooleanConst *) b)->isTrue; - if (isTrue) + if (b->isTrue()) continue; else - return b; + return boolFalse; } else - newarray[newindex++]=b; + newarray[newindex++] = b; } - if(newindex==1) { + if (newindex == 0) { + return boolTrue; + } else if (newindex == 1) { return newarray[0]; } else { + qsort(newarray, asize, sizeof(Boolean *), ptrcompares); array = newarray; asize = newindex; } break; } + case SATC_XOR: { + //handle by translation + return applyLogicalOperation(SATC_NOT, applyLogicalOperation(SATC_IFF, array, asize)); + } case SATC_IMPLIES: { - if (array[0]->type == BOOLCONST) { - BooleanConst *b=(BooleanConst *) array[0]; - if (b->isTrue) { - return array[1]; - } else { - return boolTrue; - } - } else if (array[1]->type == BOOLCONST) { - BooleanConst *b=(BooleanConst *) array[0]; - if (b->isTrue) { - return b; - } else { - return applyLogicalOperation(SATC_NOT, array, 1); - } - } - break; + //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) { boolMap.put(boolean, boolean); allBooleans.push(boolean); - return boolean; + return boolean; } else { delete boolean; return b; @@ -338,26 +338,45 @@ void CSolver::addConstraint(Boolean *constraint) { return; else if (constraint == boolFalse) setUnSAT(); - else + else { + if (constraint->type == LOGICOP) { + BooleanLogic *b=(BooleanLogic *) constraint; + if (b->op==SATC_AND) { + for(uint i=0;iinputs.getSize();i++) { + addConstraint(b->inputs.get(i)); + } + return; + } + } + constraints.add(constraint); + } } Order *CSolver::createOrder(OrderType type, Set *set) { Order *order = new Order(type, set); allOrders.push(order); + activeOrders.add(order); return order; } -int CSolver::startEncoding() { +int CSolver::solve() { bool deleteTuner = false; if (tuner == NULL) { tuner = new DefaultTuner(); deleteTuner = true; } - + long long startTime = getTimeNano(); computePolarities(this); - orderAnalysis(this); + + DecomposeOrderTransform dot(this); + dot.doTransform(); + + //This leaks like crazy + // IntegerEncodingTransform iet(this); + //iet.doTransform(); + naiveEncodingDecision(this); satEncoder->encodeAllSATEncoder(this); int result = unsat ? IS_UNSAT : satEncoder->solve(); @@ -392,8 +411,8 @@ 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(); } @@ -401,7 +420,7 @@ 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 *autotuner = new AutoTuner(budget); autotuner->addProblem(this); autotuner->tune(); delete autotuner;