X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=blobdiff_plain;f=src%2FBackend%2Fsatorderencoder.cc;h=56614fabe78a4e953ebebee916c16ae0442b6fce;hp=514bad902442f4dd0e496f1d0bd2256560c321e2;hb=d8a822b4166c0e1da167d756bc10cffbaded8972;hpb=9979be547581fdc1b75fdc09d006fa3497a7827c

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index 514bad9..56614fa 100644
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -15,8 +15,6 @@
 #include "orderpairresolver.h"
 
 Edge SATEncoder::encodeOrderSATEncoder(BooleanOrder *constraint) {
-	//This is pairwised encoding ...
-	constraint->order->setOrderResolver(new OrderPairResolver(solver, constraint->order));
 	switch ( constraint->order->type) {
 	case SATC_PARTIAL:
 		return encodePartialOrderSATEncoder(constraint);
@@ -58,7 +56,7 @@ Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) {
 	if (!edgeIsNull(gvalue))
 		return gvalue;
 
-	HashtableOrderPair *table = order->orderPairTable;
+	HashtableOrderPair *table = order->getOrderPairTable();
 	bool negate = false;
 	OrderPair flipped;
 	if (pair->first < pair->second) {
@@ -67,23 +65,46 @@ Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) {
 		flipped.second = pair->first;
 		pair = &flipped;
 	}
-	Edge constraint;
+	OrderPair *tmp;
 	if (!(table->contains(pair))) {
-		constraint = getNewVarSATEncoder();
-		OrderPair *paircopy = new OrderPair(pair->first, pair->second, constraint);
-		table->put(paircopy, paircopy);
-	} else
-		constraint = table->get(pair)->constraint;
+		tmp = new OrderPair(pair->first, pair->second, getNewVarSATEncoder());
+		table->put(tmp, tmp);
+	} else {
+		tmp = table->get(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;
 
-	return negate ? constraintNegate(constraint) : constraint;
+	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->orderPairTable == NULL) {
-		boolOrder->order->initializeOrderHashtable();
+	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) {
+			ASSERT(boolOrder->order->graph == NULL);
 			boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
 			reachMustAnalysis(solver, boolOrder->order->graph, true);
 		}
@@ -120,24 +141,6 @@ void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) {
 	}
 }
 
-Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair) {
-	ASSERT(pair->first != pair->second);
-	bool negate = false;
-	OrderPair flipped;
-	if (pair->first < pair->second) {
-		negate = true;
-		flipped.first = pair->second;
-		flipped.second = pair->first;
-		pair = &flipped;
-	}
-	if (!table->contains(pair)) {
-		return E_NULL;
-	}
-	Edge constraint = table->get(pair)->constraint;
-	ASSERT(!edgeIsNull(constraint));
-	return negate ? constraintNegate(constraint) : constraint;
-}
-
 Edge SATEncoder::generateTransOrderConstraintSATEncoder(Edge constIJ,Edge constJK,Edge constIK) {
 	Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
 	Edge loop1 = constraintOR(cnf, 3, carray);
@@ -146,7 +149,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));
+			}
+		}
+	}
+}
+
+