sparse or decompose

[satune.git] / src / Backend / satorderencoder.cc

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index d525bdad0ed0b808d192e8a72004282d77b1c549..e3d2f334da517a35fe7a1e83d354687627b703a3 100644 (file)
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -65,7 +65,7 @@ Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) {
                flipped.second = pair->first;
                pair = &flipped;
        }
-       OrderPair* tmp;
+       OrderPair *tmp;
        if (!(table->contains(pair))) {
                tmp = new OrderPair(pair->first, pair->second, getNewVarSATEncoder());
                table->put(tmp, tmp);
@@ -81,8 +81,8 @@ Edge SATEncoder::getPartialPairConstraint(Order *order, OrderPair *pair) {
                return gvalue;
 
        HashtableOrderPair *table = order->getOrderPairTable();
-       
-       OrderPair* tmp;
+
+       OrderPair *tmp;
        if (!(table->contains(pair))) {
                Edge constraint = getNewVarSATEncoder();
                tmp = new OrderPair(pair->first, pair->second, constraint);
@@ -104,11 +104,14 @@ Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
                boolOrder->order->setOrderResolver(new OrderPairResolver(solver, boolOrder->order));
                bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
                if (doOptOrderStructure) {
-                        ASSERT(boolOrder->order->graph == NULL);
+                       ASSERT(boolOrder->order->graph == NULL);
                        boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
                        reachMustAnalysis(solver, boolOrder->order->graph, true);
                }
-               createAllTotalOrderConstraintsSATEncoder(boolOrder->order);
+               if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0)
+                       createAllTotalOrderConstraintsSATEncoderSparse(boolOrder->order);
+               else
+                       createAllTotalOrderConstraintsSATEncoder(boolOrder->order);
        }
        OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
        Edge constraint = getPairConstraint(boolOrder->order, &pair);
@@ -124,13 +127,13 @@ void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) {
        Set *set = order->set;
        uint size = order->set->getSize();
        for (uint i = 0; i < size; i++) {
-               uint64_t valueI = set->getMemberAt(i);
+               uint64_t valueI = set->getElement(i);
                for (uint j = i + 1; j < size; j++) {
-                       uint64_t valueJ = set->getMemberAt(j);
+                       uint64_t valueJ = set->getElement(j);
                        OrderPair pairIJ(valueI, valueJ, E_NULL);
                        Edge constIJ = getPairConstraint(order, &pairIJ);
                        for (uint k = j + 1; k < size; k++) {
-                               uint64_t valueK = set->getMemberAt(k);
+                               uint64_t valueK = set->getElement(k);
                                OrderPair pairJK(valueJ, valueK, E_NULL);
                                OrderPair pairIK(valueI, valueK, E_NULL);
                                Edge constIK = getPairConstraint(order, &pairIK);
@@ -153,7 +156,7 @@ Edge SATEncoder::generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge
        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};
@@ -166,7 +169,7 @@ Edge SATEncoder::generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge
        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};
@@ -179,7 +182,7 @@ Edge SATEncoder::generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge
        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};
@@ -192,15 +195,15 @@ Edge SATEncoder::generatePartialOrderConstraintsSATEncoder(Edge ij,Edge ji, Edge
        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};
+                                                               cp1,cp2,cp3,cp4,cp5,cp6,
+                                                               co1,co2,co3,co4,co5,co6,
+                                                               cunorder};
        return constraintOR(cnf, 19, res);
 }
 
@@ -214,7 +217,10 @@ Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *boolOrder) {
                        boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
                        reachMustAnalysis(solver, boolOrder->order->graph, true);
                }
-               createAllPartialOrderConstraintsSATEncoder(boolOrder->order);
+               if (GETVARTUNABLE(solver->getTuner(), order->type, DECOMPOSEORDER, &onoff) == 0)
+                       createAllPartialOrderConstraintsSATEncoderSparse(boolOrder->order);
+               else
+                       createAllPartialOrderConstraintsSATEncoder(boolOrder->order);
        }
        OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
        Edge constraint = getPartialPairConstraint(boolOrder->order, &pair);
@@ -230,15 +236,15 @@ void SATEncoder::createAllPartialOrderConstraintsSATEncoder(Order *order) {
        Set *set = order->set;
        uint size = order->set->getSize();
        for (uint i = 0; i < size; i++) {
-               uint64_t valueI = set->getMemberAt(i);
+               uint64_t valueI = set->getElement(i);
                for (uint j = i + 1; j < size; j++) {
-                       uint64_t valueJ = set->getMemberAt(j);
+                       uint64_t valueJ = set->getElement(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);
+                               uint64_t valueK = set->getElement(k);
                                OrderPair pairJK(valueJ, valueK, E_NULL);
                                OrderPair pairIK(valueI, valueK, E_NULL);
                                Edge constIK = getPartialPairConstraint(order, &pairIK);
@@ -248,10 +254,69 @@ void SATEncoder::createAllPartialOrderConstraintsSATEncoder(Order *order) {
                                Edge constKI = getPartialPairConstraint(order, &pairKI);
                                Edge constKJ = getPartialPairConstraint(order, &pairKJ);
                                addConstraintCNF(cnf, generatePartialOrderConstraintsSATEncoder(constIJ, constJI,
-                                       constJK, constKJ, constIK, constKI));
+                                                                                                                                                                                                                                                                                               constJK, constKJ, constIK, constKI));
                        }
                }
        }
 }
 
+void SATEncoder::createAllTotalOrderConstraintsSATEncoderSparse(Order *order) {
+#ifdef CONFIG_DEBUG
+       model_print("in total order ...\n");
+#endif
+       ASSERT(order->type == SATC_TOTAL);
+       SetIterator64Int *iti = order->getUsedIterator();
+       while (iti->hasNext()) {
+               uint64_t valueI = iti->next();
+               SetIterator64Int *itj = new SetIterator64Int(iti);
+               while (itj->hasNext()) {
+                       uint64_t valueJ = itj->next();
+                       OrderPair pairIJ(valueI, valueJ, E_NULL);
+                       Edge constIJ = getPairConstraint(order, &pairIJ);
+                       SetIterator64Int *itk = new SetIterator64Int(itj);
+                       while (itk->hasNext()) {
+                               uint64_t valueK = itk->next();
+                               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));
+                       }
+               }
+       }
+}
 
+void SATEncoder::createAllPartialOrderConstraintsSATEncoderSparse(Order *order) {
+#ifdef CONFIG_DEBUG
+       model_print("in partial order ...\n");
+#endif
+       ASSERT(order->type == SATC_TOTAL);
+       SetIterator64Int *iti = order->getUsedIterator();
+       while (iti->hasNext()) {
+               uint64_t valueI = iti->next();
+               SetIterator64Int *itj = new SetIterator64Int(iti);
+               while (itj->hasNext()) {
+                       uint64_t valueJ = itj->next();
+                       OrderPair pairIJ(valueI, valueJ, E_NULL);
+                       OrderPair pairJI(valueJ, valueI, E_NULL);
+                       Edge constIJ = getPartialPairConstraint(order, &pairIJ);
+                       Edge constJI = getPartialPairConstraint(order, &pairJI);
+                       SetIterator64Int *itk = new SetIterator64Int(itj);
+                       while (itk->hasNext()) {
+                               uint64_t valueK = itk->next();
+                               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));
+                       }
+               }
+       }
+}