From 84e9269f9599240ee7e574e693b69909502e84d5 Mon Sep 17 00:00:00 2001 From: Hamed Date: Wed, 6 Sep 2017 18:30:27 -0700 Subject: [PATCH] Partial Order ... --- src/Backend/satencoder.h | 3 + src/Backend/satorderencoder.cc | 130 ++++++++++++++++++++++++++++++++- src/mymemory.h | 2 +- 3 files changed, 131 insertions(+), 4 deletions(-) diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h index ef3edc6..08ec527 100644 --- a/src/Backend/satencoder.h +++ b/src/Backend/satencoder.h @@ -47,11 +47,14 @@ private: Edge encodeOrderSATEncoder(BooleanOrder *constraint); Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second); Edge getPairConstraint(Order *order, OrderPair *pair); + Edge getPartialPairConstraint(Order *order, OrderPair *pair); Edge encodeTotalOrderSATEncoder(BooleanOrder *constraint); Edge encodePartialOrderSATEncoder(BooleanOrder *constraint); void createAllTotalOrderConstraintsSATEncoder(Order *order); + void createAllPartialOrderConstraintsSATEncoder(Order *order); Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair); Edge generateTransOrderConstraintSATEncoder(Edge constIJ, Edge constJK, Edge constIK); + Edge generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge jk, Edge kj,Edge ik, Edge ki); Edge encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *constraint); Edge encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint); void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This); diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc index 91e2d80..c90dcf1 100644 --- a/src/Backend/satorderencoder.cc +++ b/src/Backend/satorderencoder.cc @@ -75,6 +75,28 @@ Edge SATEncoder::getPairConstraint(Order *order, OrderPair *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(); + + 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 == SATC_TOTAL); if (boolOrder->order->encoding.resolver == NULL) { @@ -126,7 +148,109 @@ Edge SATEncoder::generateTransOrderConstraintSATEncoder(Edge constIJ,Edge constJ return constraintAND2(cnf, loop1, loop2); } -Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *constraint) { - ASSERT(constraint->order->type == SATC_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)); + } + } + } +} + + diff --git a/src/mymemory.h b/src/mymemory.h index e0a60bd..7c63aa1 100644 --- a/src/mymemory.h +++ b/src/mymemory.h @@ -26,7 +26,7 @@ void * ourrealloc(void *ptr, size_t size); */ -#if 1 +#if 0 void * model_malloc(size_t size); void model_free(void *ptr); void * model_calloc(size_t count, size_t size); -- 2.34.1