Partial Order ...

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index ef3edc6a1eb8bbd810d9fe15d3ece0ddcdf8bb2c..08ec52707c2fe57988df6670022be6263085e888 100644 (file)
--- 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 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);
        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 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);
        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 91e2d80b9c96f7a82574452edec7e16db258b8f4..c90dcf17d44734b5f20948e35c36e22eeeba72d4 100644 (file)
--- 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();
 }
 
        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) {
 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);
 }
 
        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 e0a60bd13294b871199b826e88c0ea13261c1b3d..7c63aa11c10edb99f259ab9a11fffcae8df89794 100644 (file)
--- a/src/mymemory.h
+++ b/src/mymemory.h
@@ -26,7 +26,7 @@
    void * ourrealloc(void *ptr, size_t size);
 */
 
    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);
 void * model_malloc(size_t size);
 void model_free(void *ptr);
 void * model_calloc(size_t count, size_t size);