sparse or decompose

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 63b5a619babcdd4f9b7152457436f55c05fe7e1a..84329ef4e5295317122b6ca2e5579afb67d87a6d 100644 (file)
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -55,6 +55,8 @@ private:
        Edge encodePartialOrderSATEncoder(BooleanOrder *constraint);
        void createAllTotalOrderConstraintsSATEncoder(Order *order);
        void createAllPartialOrderConstraintsSATEncoder(Order *order);
+       void createAllTotalOrderConstraintsSATEncoderSparse(Order *order);
+       void createAllPartialOrderConstraintsSATEncoderSparse(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);

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index 6c254b98a2c98cff1ee6ffa24b5f46e8c726dbff..e3d2f334da517a35fe7a1e83d354687627b703a3 100644 (file)
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -108,7 +108,10 @@ Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
                        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);
@@ -121,17 +124,16 @@ void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) {
        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();
+       Set *set = order->set;
+       uint size = order->set->getSize();
+       for (uint i = 0; i < size; i++) {
+               uint64_t valueI = set->getElement(i);
+               for (uint j = i + 1; j < size; j++) {
+                       uint64_t valueJ = set->getElement(j);
                        OrderPair pairIJ(valueI, valueJ, E_NULL);
                        Edge constIJ = getPairConstraint(order, &pairIJ);
-                       SetIterator64Int *itk = new SetIterator64Int(itj);
-                       while (itk->hasNext()) {
-                               uint64_t valueK = itk->next();
+                       for (uint k = j + 1; k < size; k++) {
+                               uint64_t valueK = set->getElement(k);
                                OrderPair pairJK(valueJ, valueK, E_NULL);
                                OrderPair pairIK(valueI, valueK, E_NULL);
                                Edge constIK = getPairConstraint(order, &pairIK);
@@ -215,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);
@@ -224,6 +229,64 @@ Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *boolOrder) {
 
 
 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->getElement(i);
+               for (uint j = i + 1; j < size; 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->getElement(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));
+                       }
+               }
+       }
+}
+
+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
@@ -250,10 +313,10 @@ void SATEncoder::createAllPartialOrderConstraintsSATEncoder(Order *order) {
                                Edge constKI = getPartialPairConstraint(order, &pairKI);
                                Edge constKJ = getPartialPairConstraint(order, &pairKJ);
                                addConstraintCNF(cnf, generatePartialOrderConstraintsSATEncoder(constIJ, constJI,
+
+
                                                                                                                                                                                                                                                                                                constJK, constKJ, constIK, constKI));
                        }
                }
        }
 }
-
-