X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FBackend%2Fsatorderencoder.cc;h=c90dcf17d44734b5f20948e35c36e22eeeba72d4;hb=4901eaf03e64e4ed21f1ec0d786b75b5aa29283c;hp=7cbcd7f5eaed8cc805e49dbc16c31e018f2bebd2;hpb=7997cc8a8bbee380ba714aa52362374f2aa68ef1;p=satune.git diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index 7cbcd7f..c90dcf1 100644 --- a/src/Backend/satorderencoder.cc +++ b/src/Backend/satorderencoder.cc @@ -6,86 +6,40 @@ #include "orderpair.h" #include "set.h" #include "tunable.h" -#include "orderencoder.h" +#include "orderanalysis.h" #include "ordergraph.h" #include "orderedge.h" #include "element.h" #include "predicate.h" #include "orderelement.h" +#include "orderpairresolver.h" -Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) { - if(constraint->order->order.type == INTEGERENCODING){ - return orderIntegerEncodingSATEncoder(This, constraint); - } +Edge SATEncoder::encodeOrderSATEncoder(BooleanOrder *constraint) { switch ( constraint->order->type) { - case PARTIAL: - return encodePartialOrderSATEncoder(This, constraint); - case TOTAL: - return encodeTotalOrderSATEncoder(This, constraint); + case SATC_PARTIAL: + return encodePartialOrderSATEncoder(constraint); + case SATC_TOTAL: + return encodeTotalOrderSATEncoder(constraint); default: ASSERT(0); } return E_BOGUS; } -Edge orderIntegerEncodingSATEncoder(SATEncoder *This, BooleanOrder *boolOrder){ - if(boolOrder->order->graph == NULL){ - bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type, - OPTIMIZEORDERSTRUCTURE, &onoff); - if (doOptOrderStructure ) { - boolOrder->order->graph = buildMustOrderGraph(boolOrder->order); - reachMustAnalysis(This->solver, boolOrder->order->graph, true); - } - } - Order* order = boolOrder->order; - Edge gvalue = inferOrderConstraintFromGraph(order, boolOrder->first, boolOrder->second); - if(!edgeIsNull(gvalue)) - return gvalue; - - if (boolOrder->order->elementTable == NULL) { - boolOrder->order->initializeOrderElementsHashTable(); - } - //getting two elements and using LT predicate ... - Element* elem1 = getOrderIntegerElement(This, order, boolOrder->first); - ElementEncoding *encoding = getElementEncoding(elem1); - if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) { - setElementEncodingType(encoding, BINARYINDEX); - encodingArrayInitialization(encoding); - } - Element* elem2 = getOrderIntegerElement(This, order, boolOrder->second); - encoding = getElementEncoding(elem2); - if (getElementEncodingType(encoding) == ELEM_UNASSIGNED) { - setElementEncodingType(encoding, BINARYINDEX); - encodingArrayInitialization(encoding); - } - Set * sarray[]={order->set, order->set}; - Predicate *predicate =new PredicateOperator(LT, sarray, 2); - Element * parray[]={elem1, elem2}; - BooleanPredicate * boolean=new BooleanPredicate(predicate, parray, 2, NULL); - setFunctionEncodingType(boolean->getFunctionEncoding(), CIRCUIT); - {//Adding new elements and boolean/predicate to solver regarding memory management - This->solver->allBooleans.push(boolean); - This->solver->allPredicates.push(predicate); - This->solver->allElements.push(elem1); - This->solver->allElements.push(elem2); - } - return encodeConstraintSATEncoder(This, boolean); -} - -Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second){ +Edge SATEncoder::inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second) { if (order->graph != NULL) { - OrderGraph *graph=order->graph; - OrderNode *first=lookupOrderNodeFromOrderGraph(graph, _first); - OrderNode *second=lookupOrderNodeFromOrderGraph(graph, _second); + OrderGraph *graph = order->graph; + OrderNode *first = graph->lookupOrderNodeFromOrderGraph(_first); + OrderNode *second = graph->lookupOrderNodeFromOrderGraph(_second); if ((first != NULL) && (second != NULL)) { - OrderEdge *edge=lookupOrderEdgeFromOrderGraph(graph, first, second); + OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(first, second); if (edge != NULL) { if (edge->mustPos) return E_True; else if (edge->mustNeg) return E_False; } - OrderEdge *invedge=getOrderEdgeFromOrderGraph(graph, second, first); + OrderEdge *invedge = graph->lookupOrderEdgeFromOrderGraph(second, first); if (invedge != NULL) { if (invedge->mustPos) return E_False; @@ -97,27 +51,12 @@ Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _seco return E_NULL; } -Element* getOrderIntegerElement(SATEncoder* This,Order *order, uint64_t item) { - HashSetOrderElement* eset = order->elementTable; - OrderElement oelement ={item, NULL}; - if( !eset->contains(&oelement)){ - Element* elem = new ElementSet(order->set); - ElementEncoding* encoding = getElementEncoding(elem); - setElementEncodingType(encoding, BINARYINDEX); - encodingArrayInitialization(encoding); - encodeElementSATEncoder(This, elem); - eset->add(allocOrderElement(item, elem)); - return elem; - } else - return eset->get(&oelement)->elem; -} - -Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) { +Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) { Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second); - if(!edgeIsNull(gvalue)) + if (!edgeIsNull(gvalue)) return gvalue; - - HashTableOrderPair *table = order->orderPairTable; + + HashtableOrderPair *table = order->getOrderPairTable(); bool negate = false; OrderPair flipped; if (pair->first < pair->second) { @@ -126,86 +65,192 @@ Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) { flipped.second = pair->first; pair = &flipped; } - Edge constraint; + OrderPair* tmp; if (!(table->contains(pair))) { - constraint = getNewVarSATEncoder(This); - OrderPair *paircopy = allocOrderPair(pair->first, pair->second, constraint); - table->put(paircopy, paircopy); - } else - constraint = table->get(pair)->constraint; + tmp = new OrderPair(pair->first, pair->second, getNewVarSATEncoder()); + table->put(tmp, tmp); + } else { + tmp = table->get(pair); + } + return negate ? tmp->getNegatedConstraint() : tmp->getConstraint(); +} + +Edge SATEncoder::getPartialPairConstraint(Order *order, OrderPair *pair) { + Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second); + if (!edgeIsNull(gvalue)) + return gvalue; + + HashtableOrderPair *table = order->getOrderPairTable(); - return negate ? constraintNegate(constraint) : constraint; + OrderPair* tmp; + if (!(table->contains(pair))) { + Edge constraint = getNewVarSATEncoder(); + tmp = new OrderPair(pair->first, pair->second, constraint); + table->put(tmp, tmp); + Edge constraint2 = getNewVarSATEncoder(); + OrderPair *swap = new OrderPair(pair->second, pair->first, constraint2); + table->put(swap, swap); + addConstraintCNF(cnf, constraintNegate(constraintAND2(cnf, constraint, constraint2))); + } else { + tmp = table->get(pair); + } + return tmp->getConstraint(); } -Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) { - ASSERT(boolOrder->order->type == TOTAL); - if (boolOrder->order->orderPairTable == NULL) { - boolOrder->order->initializeOrderHashTable(); - bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff); +Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) { + ASSERT(boolOrder->order->type == SATC_TOTAL); + if (boolOrder->order->encoding.resolver == NULL) { + //This is pairwised encoding ... + boolOrder->order->setOrderResolver(new OrderPairResolver(solver, boolOrder->order)); + bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff); if (doOptOrderStructure) { boolOrder->order->graph = buildMustOrderGraph(boolOrder->order); - reachMustAnalysis(This->solver, boolOrder->order->graph, true); + reachMustAnalysis(solver, boolOrder->order->graph, true); } - createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order); + createAllTotalOrderConstraintsSATEncoder(boolOrder->order); } - OrderPair pair = {boolOrder->first, boolOrder->second, E_NULL}; - Edge constraint = getPairConstraint(This, boolOrder->order, &pair); + OrderPair pair(boolOrder->first, boolOrder->second, E_NULL); + Edge constraint = getPairConstraint(boolOrder->order, &pair); return constraint; } -void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order) { -#ifdef TRACE_DEBUG +void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) { +#ifdef CONFIG_DEBUG model_print("in total order ...\n"); #endif - ASSERT(order->type == TOTAL); - Vector *mems = order->set->members; - uint size = mems->getSize(); + ASSERT(order->type == SATC_TOTAL); + Set *set = order->set; + uint size = order->set->getSize(); for (uint i = 0; i < size; i++) { - uint64_t valueI = mems->get(i); + uint64_t valueI = set->getMemberAt(i); for (uint j = i + 1; j < size; j++) { - uint64_t valueJ = mems->get(j); - OrderPair pairIJ = {valueI, valueJ}; - Edge constIJ = getPairConstraint(This, order, &pairIJ); + uint64_t valueJ = set->getMemberAt(j); + OrderPair pairIJ(valueI, valueJ, E_NULL); + Edge constIJ = getPairConstraint(order, &pairIJ); for (uint k = j + 1; k < size; k++) { - uint64_t valueK = mems->get(k); - OrderPair pairJK = {valueJ, valueK}; - OrderPair pairIK = {valueI, valueK}; - Edge constIK = getPairConstraint(This, order, &pairIK); - Edge constJK = getPairConstraint(This, order, &pairJK); - addConstraintCNF(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK)); + uint64_t valueK = set->getMemberAt(k); + OrderPair pairJK(valueJ, valueK, E_NULL); + OrderPair pairIK(valueI, valueK, E_NULL); + Edge constIK = getPairConstraint(order, &pairIK); + Edge constJK = getPairConstraint(order, &pairJK); + addConstraintCNF(cnf, generateTransOrderConstraintSATEncoder(constIJ, constJK, constIK)); } } } } -Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair) { - ASSERT(pair->first != pair->second); - bool negate = false; - OrderPair flipped; - if (pair->first < pair->second) { - negate = true; - flipped.first = pair->second; - flipped.second = pair->first; - pair = &flipped; - } - if (!table->contains(pair)) { - return E_NULL; - } - Edge constraint = table->get(pair)->constraint; - ASSERT(!edgeIsNull(constraint)); - return negate ? constraintNegate(constraint) : constraint; -} - -Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK) { +Edge SATEncoder::generateTransOrderConstraintSATEncoder(Edge constIJ,Edge constJK,Edge constIK) { Edge carray[] = {constIJ, constJK, constraintNegate(constIK)}; - Edge loop1 = constraintOR(This->cnf, 3, carray); + Edge loop1 = constraintOR(cnf, 3, carray); Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK}; - Edge loop2 = constraintOR(This->cnf, 3, carray2 ); - return constraintAND2(This->cnf, loop1, loop2); + Edge loop2 = constraintOR(cnf, 3, carray2 ); + return constraintAND2(cnf, loop1, loop2); } -Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) { - ASSERT(constraint->order->type == PARTIAL); - return E_BOGUS; +Edge SATEncoder::generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge jk, Edge kj,Edge ik, Edge ki) { + Edge uoIJ = constraintAND2(cnf, constraintNegate(ij), constraintNegate(ji)); + Edge uoJK = constraintAND2(cnf, constraintNegate(jk), constraintNegate(kj)); + Edge uoIK = constraintAND2(cnf, constraintNegate(ik), constraintNegate(ki)); + + Edge t1[] = {ij, jk, ik}; + Edge t2[] = {ji, jk, ik}; + Edge t3[] = {ij, kj, ki}; + Edge t4[] = {ij, kj, ik}; + Edge t5[] = {ji, jk, ki}; + Edge t6[] = {ji, kj, ki}; + Edge ct1 = constraintAND(cnf, 3, t1); + Edge ct2 = constraintAND(cnf, 3, t2); + Edge ct3 = constraintAND(cnf, 3, t3); + Edge ct4 = constraintAND(cnf, 3, t4); + Edge ct5 = constraintAND(cnf, 3, t5); + Edge ct6 = constraintAND(cnf, 3, t6); + + Edge p1[] = {uoIJ, jk, ik}; + Edge p2[] = {ij, kj, uoIK}; + Edge p3[] = {ji, uoJK, ki}; + Edge p4[] = {uoIJ, kj, ki}; + Edge p5[] = {ji, jk, uoIK}; + Edge p6[] = {ij, uoJK, ik}; + Edge cp1 = constraintAND(cnf, 3, p1); + Edge cp2 = constraintAND(cnf, 3, p2); + Edge cp3 = constraintAND(cnf, 3, p3); + Edge cp4 = constraintAND(cnf, 3, p4); + Edge cp5 = constraintAND(cnf, 3, p5); + Edge cp6 = constraintAND(cnf, 3, p6); + + Edge o1[] = {uoIJ, uoJK, ik}; + Edge o2[] = {ij, uoJK, uoIK}; + Edge o3[] = {uoIK, jk, uoIK}; + Edge o4[] = {ji, uoJK, uoIK}; + Edge o5[] = {uoIJ, uoJK, ki}; + Edge o6[] = {uoIJ, kj, uoIK}; + Edge co1 = constraintAND(cnf, 3, o1); + Edge co2 = constraintAND(cnf, 3, o2); + Edge co3 = constraintAND(cnf, 3, o3); + Edge co4 = constraintAND(cnf, 3, o4); + Edge co5 = constraintAND(cnf, 3, o5); + Edge co6 = constraintAND(cnf, 3, o6); + + Edge unorder [] = {uoIJ, uoJK, uoIK}; + Edge cunorder = constraintAND(cnf, 3, unorder); + + + Edge res[] = {ct1,ct2,ct3,ct4,ct5,ct6, + cp1,cp2,cp3,cp4,cp5,cp6, + co1,co2,co3,co4,co5,co6, + cunorder}; + return constraintOR(cnf, 19, res); +} + +Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *boolOrder) { + ASSERT(boolOrder->order->type == SATC_PARTIAL); + if (boolOrder->order->encoding.resolver == NULL) { + //This is pairwised encoding ... + boolOrder->order->setOrderResolver(new OrderPairResolver(solver, boolOrder->order)); + bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff); + if (doOptOrderStructure) { + boolOrder->order->graph = buildMustOrderGraph(boolOrder->order); + reachMustAnalysis(solver, boolOrder->order->graph, true); + } + createAllPartialOrderConstraintsSATEncoder(boolOrder->order); + } + OrderPair pair(boolOrder->first, boolOrder->second, E_NULL); + Edge constraint = getPartialPairConstraint(boolOrder->order, &pair); + return constraint; } + + +void SATEncoder::createAllPartialOrderConstraintsSATEncoder(Order *order) { +#ifdef CONFIG_DEBUG + model_print("in partial order ...\n"); +#endif + ASSERT(order->type == SATC_TOTAL); + Set *set = order->set; + uint size = order->set->getSize(); + for (uint i = 0; i < size; i++) { + uint64_t valueI = set->getMemberAt(i); + for (uint j = i + 1; j < size; j++) { + uint64_t valueJ = set->getMemberAt(j); + OrderPair pairIJ(valueI, valueJ, E_NULL); + OrderPair pairJI(valueJ, valueI, E_NULL); + Edge constIJ = getPartialPairConstraint(order, &pairIJ); + Edge constJI = getPartialPairConstraint(order, &pairJI); + for (uint k = j + 1; k < size; k++) { + uint64_t valueK = set->getMemberAt(k); + OrderPair pairJK(valueJ, valueK, E_NULL); + OrderPair pairIK(valueI, valueK, E_NULL); + Edge constIK = getPartialPairConstraint(order, &pairIK); + Edge constJK = getPartialPairConstraint(order, &pairJK); + OrderPair pairKJ(valueK, valueJ, E_NULL); + OrderPair pairKI(valueK, valueI, E_NULL); + Edge constKI = getPartialPairConstraint(order, &pairKI); + Edge constKJ = getPartialPairConstraint(order, &pairKJ); + addConstraintCNF(cnf, generatePartialOrderConstraintsSATEncoder(constIJ, constJI, + constJK, constKJ, constIK, constKI)); + } + } + } +} + +