X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FBackend%2Fsatorderencoder.cc;h=c90dcf17d44734b5f20948e35c36e22eeeba72d4;hb=4901eaf03e64e4ed21f1ec0d786b75b5aa29283c;hp=750be42a73d954bd53d57fbc945850393954a57e;hpb=4a0700a15422c8bacce0b27680bf8d3bd3351504;p=satune.git diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index 750be42..c90dcf1 100644 --- a/src/Backend/satorderencoder.cc +++ b/src/Backend/satorderencoder.cc @@ -12,12 +12,13 @@ #include "element.h" #include "predicate.h" #include "orderelement.h" +#include "orderpairresolver.h" Edge SATEncoder::encodeOrderSATEncoder(BooleanOrder *constraint) { switch ( constraint->order->type) { - case PARTIAL: + case SATC_PARTIAL: return encodePartialOrderSATEncoder(constraint); - case TOTAL: + case SATC_TOTAL: return encodeTotalOrderSATEncoder(constraint); default: ASSERT(0); @@ -25,7 +26,7 @@ Edge SATEncoder::encodeOrderSATEncoder(BooleanOrder *constraint) { return E_BOGUS; } -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 = graph->lookupOrderNodeFromOrderGraph(_first); @@ -55,7 +56,7 @@ Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) { if (!edgeIsNull(gvalue)) return gvalue; - HashTableOrderPair *table = order->orderPairTable; + HashtableOrderPair *table = order->getOrderPairTable(); bool negate = false; OrderPair flipped; if (pair->first < pair->second) { @@ -64,21 +65,43 @@ Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) { flipped.second = pair->first; pair = &flipped; } - Edge constraint; + OrderPair* tmp; if (!(table->contains(pair))) { - constraint = getNewVarSATEncoder(); - OrderPair *paircopy = new OrderPair(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; - return negate ? constraintNegate(constraint) : constraint; + HashtableOrderPair *table = order->getOrderPairTable(); + + 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 SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) { - ASSERT(boolOrder->order->type == TOTAL); - if (boolOrder->order->orderPairTable == NULL) { - boolOrder->order->initializeOrderHashTable(); + 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); @@ -93,20 +116,20 @@ Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) { void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) { -#ifdef TRACE_DEBUG +#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); + 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); + uint64_t valueK = set->getMemberAt(k); OrderPair pairJK(valueJ, valueK, E_NULL); OrderPair pairIK(valueI, valueK, E_NULL); Edge constIK = getPairConstraint(order, &pairIK); @@ -117,24 +140,6 @@ void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) { } } -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 SATEncoder::generateTransOrderConstraintSATEncoder(Edge constIJ,Edge constJK,Edge constIK) { Edge carray[] = {constIJ, constJK, constraintNegate(constIK)}; Edge loop1 = constraintOR(cnf, 3, carray); @@ -143,7 +148,109 @@ Edge SATEncoder::generateTransOrderConstraintSATEncoder(Edge constIJ,Edge constJ return constraintAND2(cnf, loop1, loop2); } -Edge SATEncoder::encodePartialOrderSATEncoder(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)); + } + } + } +} + +