From: bdemsky <bdemsky@uci.edu>
Date: Thu, 21 Mar 2019 02:59:04 +0000 (-0700)
Subject: sparse or decompose
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=06e879cba71e0b6180c1997fb0078ba80b323c34;hp=e27a40f5c5fb5e9f804acd9ebfd38d7200d92ed1

sparse or decompose
---

diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 63b5a61..84329ef 100644
--- 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 6c254b9..e3d2f33 100644
--- 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));
 			}
 		}
 	}
 }
-
-