X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2FBackend%2Fsatorderencoder.cc;h=b977efa782c4ea963f03a4a3da6bbeac80b8da01;hb=516fb5585a776bde6277eeb3c46f09620dd20a5f;hp=9061f76f432aa1ff3af7c3df490aaa65f9779824;hpb=4b5b02d3c28129def15b8945c0332269f72acc9d;p=satune.git

diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index 9061f76..b977efa 100644
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -6,41 +6,40 @@
 #include "orderpair.h"
 #include "set.h"
 #include "tunable.h"
-#include "orderencoder.h"
+#include "orderanalysis.h"
 #include "ordergraph.h"
 #include "orderedge.h"
 #include "element.h"
 #include "predicate.h"
 #include "orderelement.h"
+#include "orderpairresolver.h"
 
-Edge encodeOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
+Edge SATEncoder::encodeOrderSATEncoder(BooleanOrder *constraint) {
 	switch ( constraint->order->type) {
-		case PARTIAL:
-			return encodePartialOrderSATEncoder(This, constraint);
-		case TOTAL:
-			return encodeTotalOrderSATEncoder(This, constraint);
-		default:
-			ASSERT(0);
-	}
+	case SATC_PARTIAL:
+		return encodePartialOrderSATEncoder(constraint);
+	case SATC_TOTAL:
+		return encodeTotalOrderSATEncoder(constraint);
 	default:
 		ASSERT(0);
+	}
 	return E_BOGUS;
 }
 
-Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _second){
+Edge SATEncoder::inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second) {
 	if (order->graph != NULL) {
-		OrderGraph *graph=order->graph;
-		OrderNode *first=lookupOrderNodeFromOrderGraph(graph, _first);
-		OrderNode *second=lookupOrderNodeFromOrderGraph(graph, _second);
+		OrderGraph *graph = order->graph;
+		OrderNode *first = graph->lookupOrderNodeFromOrderGraph(_first);
+		OrderNode *second = graph->lookupOrderNodeFromOrderGraph(_second);
 		if ((first != NULL) && (second != NULL)) {
-			OrderEdge *edge=lookupOrderEdgeFromOrderGraph(graph, first, second);
+			OrderEdge *edge = graph->lookupOrderEdgeFromOrderGraph(first, second);
 			if (edge != NULL) {
 				if (edge->mustPos)
 					return E_True;
 				else if (edge->mustNeg)
 					return E_False;
 			}
-			OrderEdge *invedge=getOrderEdgeFromOrderGraph(graph, second, first);
+			OrderEdge *invedge = graph->lookupOrderEdgeFromOrderGraph(second, first);
 			if (invedge != NULL) {
 				if (invedge->mustPos)
 					return E_False;
@@ -52,12 +51,12 @@ Edge inferOrderConstraintFromGraph(Order* order, uint64_t _first, uint64_t _seco
 	return E_NULL;
 }
 
-Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
+Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) {
 	Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
-	if(!edgeIsNull(gvalue))
+	if (!edgeIsNull(gvalue))
 		return gvalue;
-	
-	HashTableOrderPair *table = order->orderPairTable;
+
+	HashtableOrderPair *table = order->orderPairTable;
 	bool negate = false;
 	OrderPair flipped;
 	if (pair->first < pair->second) {
@@ -68,58 +67,60 @@ Edge getPairConstraint(SATEncoder *This, Order *order, OrderPair *pair) {
 	}
 	Edge constraint;
 	if (!(table->contains(pair))) {
-		constraint = getNewVarSATEncoder(This);
+		constraint = getNewVarSATEncoder();
 		OrderPair *paircopy = new OrderPair(pair->first, pair->second, constraint);
 		table->put(paircopy, paircopy);
 	} else
 		constraint = table->get(pair)->constraint;
-	
+
 	return negate ? constraintNegate(constraint) : constraint;
 }
 
-Edge encodeTotalOrderSATEncoder(SATEncoder *This, BooleanOrder *boolOrder) {
-	ASSERT(boolOrder->order->type == TOTAL);
+Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
+	ASSERT(boolOrder->order->type == SATC_TOTAL);
 	if (boolOrder->order->orderPairTable == NULL) {
-		boolOrder->order->initializeOrderHashTable();
-		bool doOptOrderStructure=GETVARTUNABLE(This->solver->tuner, boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
+		//This is pairwised encoding ...
+		boolOrder->order->setOrderResolver(new OrderPairResolver(solver, boolOrder->order));
+		boolOrder->order->initializeOrderHashtable();
+		bool doOptOrderStructure = GETVARTUNABLE(solver->getTuner(), boolOrder->order->type, OPTIMIZEORDERSTRUCTURE, &onoff);
 		if (doOptOrderStructure) {
 			boolOrder->order->graph = buildMustOrderGraph(boolOrder->order);
-			reachMustAnalysis(This->solver, boolOrder->order->graph, true);
+			reachMustAnalysis(solver, boolOrder->order->graph, true);
 		}
-		createAllTotalOrderConstraintsSATEncoder(This, boolOrder->order);
+		createAllTotalOrderConstraintsSATEncoder(boolOrder->order);
 	}
 	OrderPair pair(boolOrder->first, boolOrder->second, E_NULL);
-	Edge constraint = getPairConstraint(This, boolOrder->order, &pair);
+	Edge constraint = getPairConstraint(boolOrder->order, &pair);
 	return constraint;
 }
 
 
-void createAllTotalOrderConstraintsSATEncoder(SATEncoder *This, Order *order) {
-#ifdef TRACE_DEBUG
+void SATEncoder::createAllTotalOrderConstraintsSATEncoder(Order *order) {
+#ifdef CONFIG_DEBUG
 	model_print("in total order ...\n");
 #endif
-	ASSERT(order->type == TOTAL);
-	Vector<uint64_t> *mems = order->set->members;
-	uint size = mems->getSize();
+	ASSERT(order->type == SATC_TOTAL);
+	Set *set = order->set;
+	uint size = order->set->getSize();
 	for (uint i = 0; i < size; i++) {
-		uint64_t valueI = mems->get(i);
+		uint64_t valueI = set->getMemberAt(i);
 		for (uint j = i + 1; j < size; j++) {
-			uint64_t valueJ = mems->get(j);
+			uint64_t valueJ = set->getMemberAt(j);
 			OrderPair pairIJ(valueI, valueJ, E_NULL);
-			Edge constIJ = getPairConstraint(This, order, &pairIJ);
+			Edge constIJ = getPairConstraint(order, &pairIJ);
 			for (uint k = j + 1; k < size; k++) {
-				uint64_t valueK = mems->get(k);
+				uint64_t valueK = set->getMemberAt(k);
 				OrderPair pairJK(valueJ, valueK, E_NULL);
 				OrderPair pairIK(valueI, valueK, E_NULL);
-				Edge constIK = getPairConstraint(This, order, &pairIK);
-				Edge constJK = getPairConstraint(This, order, &pairJK);
-				addConstraintCNF(This->cnf, generateTransOrderConstraintSATEncoder(This, constIJ, constJK, constIK));
+				Edge constIK = getPairConstraint(order, &pairIK);
+				Edge constJK = getPairConstraint(order, &pairJK);
+				addConstraintCNF(cnf, generateTransOrderConstraintSATEncoder(constIJ, constJK, constIK));
 			}
 		}
 	}
 }
 
-Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair) {
+Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair) {
 	ASSERT(pair->first != pair->second);
 	bool negate = false;
 	OrderPair flipped;
@@ -137,15 +138,15 @@ Edge getOrderConstraint(HashTableOrderPair *table, OrderPair *pair) {
 	return negate ? constraintNegate(constraint) : constraint;
 }
 
-Edge generateTransOrderConstraintSATEncoder(SATEncoder *This, Edge constIJ,Edge constJK,Edge constIK) {
+Edge SATEncoder::generateTransOrderConstraintSATEncoder(Edge constIJ,Edge constJK,Edge constIK) {
 	Edge carray[] = {constIJ, constJK, constraintNegate(constIK)};
-	Edge loop1 = constraintOR(This->cnf, 3, carray);
+	Edge loop1 = constraintOR(cnf, 3, carray);
 	Edge carray2[] = {constraintNegate(constIJ), constraintNegate(constJK), constIK};
-	Edge loop2 = constraintOR(This->cnf, 3, carray2 );
-	return constraintAND2(This->cnf, loop1, loop2);
+	Edge loop2 = constraintOR(cnf, 3, carray2 );
+	return constraintAND2(cnf, loop1, loop2);
 }
 
-Edge encodePartialOrderSATEncoder(SATEncoder *This, BooleanOrder *constraint) {
-	ASSERT(constraint->order->type == PARTIAL);
+Edge SATEncoder::encodePartialOrderSATEncoder(BooleanOrder *constraint) {
+	ASSERT(constraint->order->type == SATC_PARTIAL);
 	return E_BOGUS;
 }