From: bdemsky <bdemsky@uci.edu>
Date: Thu, 7 Sep 2017 22:02:14 +0000 (-0700)
Subject: Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/constraint_compiler
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=3552af833b3ff76f221d6c9a9e410da96dd58734;hp=b510348e650406a2bb812bb6f599cc32b508403b

Merge branch 'master' of ssh://plrg.eecs.uci.edu/home/git/constraint_compiler
---

diff --git a/src/AST/order.cc b/src/AST/order.cc
index 35bca4a..609b469 100644
--- a/src/AST/order.cc
+++ b/src/AST/order.cc
@@ -4,21 +4,16 @@
 #include "boolean.h"
 #include "ordergraph.h"
 #include "csolver.h"
+#include "orderpairresolver.h"
 
 Order::Order(OrderType _type, Set *_set) :
 	type(_type),
 	set(_set),
-	orderPairTable(NULL),
 	graph(NULL),
 	encoding(this)
 {
 }
 
-void Order::initializeOrderHashtable() {
-	orderPairTable = new HashtableOrderPair();
-}
-
-
 void Order::addOrderConstraint(BooleanOrder *constraint) {
 	constraints.push(constraint);
 }
@@ -36,12 +31,16 @@ Order *Order::clone(CSolver *solver, CloneMap *map) {
 	return o;
 }
 
-Order::~Order() {
-	if (orderPairTable != NULL) {
-		orderPairTable->resetanddelete();
-		delete orderPairTable;
+HashtableOrderPair* Order::getOrderPairTable(){
+	ASSERT( encoding.resolver != NULL);
+	if (OrderPairResolver* t = dynamic_cast<OrderPairResolver*>(encoding.resolver)){
+		return t->getOrderPairTable();
+	} else {
+		ASSERT(0);
 	}
+}
 
+Order::~Order() {
 	if (graph != NULL) {
 		delete graph;
 	}
diff --git a/src/AST/order.h b/src/AST/order.h
index cc8b45e..b1f0559 100644
--- a/src/AST/order.h
+++ b/src/AST/order.h
@@ -14,16 +14,15 @@ public:
 	~Order();
 	OrderType type;
 	Set *set;
-	HashtableOrderPair *orderPairTable;
 	OrderGraph *graph;
 	Order *clone(CSolver *solver, CloneMap *map);
 	Vector<BooleanOrder *> constraints;
 	OrderEncoding encoding;
 	void setOrderResolver(OrderResolver *_resolver) { ASSERT(encoding.resolver == NULL); encoding.resolver = _resolver;};
-	void initializeOrderHashtable();
 	void initializeOrderElementsHashtable();
 	void addOrderConstraint(BooleanOrder *constraint);
 	void setOrderEncodingType(OrderEncodingType type);
+	HashtableOrderPair* getOrderPairTable();
 	CMEMALLOC;
 };
 
diff --git a/src/ASTAnalyses/Order/ordergraph.cc b/src/ASTAnalyses/Order/ordergraph.cc
index 2127db9..ce9a071 100644
--- a/src/ASTAnalyses/Order/ordergraph.cc
+++ b/src/ASTAnalyses/Order/ordergraph.cc
@@ -184,16 +184,19 @@ bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination){
 	SetIteratorOrderEdge *iterator = source->outEdges.iterator();
 	bool found = false;
 	while(iterator->hasNext()){
-		OrderNode* node = iterator->next()->sink;
-		if(!visited.contains(node)){
-			if( node == destination ){
-				found = true;
-				break;
-			}
-			visited.add(node);
-			found =isTherePathVisit(visited, node, destination);
-			if(found){
-				break;
+		OrderEdge* edge = iterator->next();
+		if(edge->polPos){
+			OrderNode* node = edge->sink;
+			if(!visited.contains(node)){
+				if( node == destination ){
+					found = true;
+					break;
+				}
+				visited.add(node);
+				found =isTherePathVisit(visited, node, destination);
+				if(found){
+					break;
+				}
 			}
 		}
 	}
@@ -205,15 +208,18 @@ bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode* current,
 	SetIteratorOrderEdge *iterator = current->outEdges.iterator();
 	bool found = false;
 	while(iterator->hasNext()){
-		OrderNode* node = iterator->next()->sink;
-		if(node == destination){
-			found = true;
-			break;
-		}
-		visited.add(node);
-		if(isTherePathVisit(visited, node, destination)){
-			found = true;
-			break;
+		OrderEdge* edge = iterator->next();
+		if(edge->polPos){
+			OrderNode* node = edge->sink;
+			if(node == destination){
+				found = true;
+				break;
+			}
+			visited.add(node);
+			if(isTherePathVisit(visited, node, destination)){
+				found = true;
+				break;
+			}
 		}
 	}
 	delete iterator;
diff --git a/src/Backend/orderpair.cc b/src/Backend/orderpair.cc
index 89913bb..abe29cc 100644
--- a/src/Backend/orderpair.cc
+++ b/src/Backend/orderpair.cc
@@ -1,5 +1,7 @@
 #include "orderpair.h"
-
+#include "constraint.h"
+#include "csolver.h"
+#include "satencoder.h"
 
 OrderPair::OrderPair(uint64_t _first, uint64_t _second, Edge _constraint) :
 	first(_first),
@@ -12,3 +14,22 @@ OrderPair::OrderPair() :
 	second(0),
 	constraint(E_NULL) {
 }
+
+OrderPair::~OrderPair(){
+}
+
+Edge OrderPair::getConstraint(){
+	return constraint;
+}
+
+Edge OrderPair::getNegatedConstraint(){
+	return constraintNegate(constraint);
+}
+
+bool OrderPair::getConstraintValue(CSolver* solver){
+	return getValueCNF(solver->getSATEncoder()->getCNF(), constraint);
+}
+
+bool OrderPair::getNegatedConstraintValue(CSolver* solver){
+	return getValueCNF(solver->getSATEncoder()->getCNF(), constraintNegate(constraint));
+}
diff --git a/src/Backend/orderpair.h b/src/Backend/orderpair.h
index aad68ff..f650648 100644
--- a/src/Backend/orderpair.h
+++ b/src/Backend/orderpair.h
@@ -14,12 +14,20 @@
 
 class OrderPair {
 public:
-	OrderPair(uint64_t first, uint64_t second, Edge constraint);
+	OrderPair(uint64_t first, uint64_t second, Edge constraint = E_NULL);
 	OrderPair();
+	virtual ~OrderPair();
+	virtual Edge getConstraint();
+	virtual bool getConstraintValue(CSolver* solver);
+	//for the cases that we swap first and second ... For total order is straight forward.
+	// but for partial order it has some complexity which should be hidden ... -HG
+	virtual Edge getNegatedConstraint();
+	virtual bool getNegatedConstraintValue(CSolver* solver);
 	uint64_t first;
 	uint64_t second;
-	Edge constraint;
 	CMEMALLOC;
+protected:
+	Edge constraint;
 };
 
 #endif/* ORDERPAIR_H */
diff --git a/src/Backend/satencoder.h b/src/Backend/satencoder.h
index 7af3e55..08ec527 100644
--- a/src/Backend/satencoder.h
+++ b/src/Backend/satencoder.h
@@ -47,11 +47,14 @@ private:
 	Edge encodeOrderSATEncoder(BooleanOrder *constraint);
 	Edge inferOrderConstraintFromGraph(Order *order, uint64_t _first, uint64_t _second);
 	Edge getPairConstraint(Order *order, OrderPair *pair);
+	Edge getPartialPairConstraint(Order *order, OrderPair *pair);
 	Edge encodeTotalOrderSATEncoder(BooleanOrder *constraint);
 	Edge encodePartialOrderSATEncoder(BooleanOrder *constraint);
 	void createAllTotalOrderConstraintsSATEncoder(Order *order);
+	void createAllPartialOrderConstraintsSATEncoder(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);
 	Edge encodeEnumEntriesTablePredicateSATEncoder(BooleanPredicate *constraint);
 	Edge encodeEnumTablePredicateSATEncoder(BooleanPredicate *constraint);
 	void encodeEnumTableElemFunctionSATEncoder(ElementFunction *This);
@@ -64,5 +67,4 @@ private:
 };
 
 void allocElementConstraintVariables(ElementEncoding *ee, uint numVars);
-Edge getOrderConstraint(HashtableOrderPair *table, OrderPair *pair);
 #endif
diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index b977efa..c90dcf1 100644
--- a/src/Backend/satorderencoder.cc
+++ b/src/Backend/satorderencoder.cc
@@ -56,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) {
@@ -65,23 +65,43 @@ 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();
+}
 
-	return negate ? constraintNegate(constraint) : constraint;
+Edge SATEncoder::getPartialPairConstraint(Order *order, OrderPair *pair) {
+	Edge gvalue = inferOrderConstraintFromGraph(order, pair->first, pair->second);
+	if (!edgeIsNull(gvalue))
+		return gvalue;
+
+	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) {
+	if (boolOrder->order->encoding.resolver == NULL) {
 		//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);
@@ -120,24 +140,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 +148,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));
+			}
+		}
+	}
+}
+
+
diff --git a/src/Translator/orderpairresolver.cc b/src/Translator/orderpairresolver.cc
index f0cb98d..e32a757 100644
--- a/src/Translator/orderpairresolver.cc
+++ b/src/Translator/orderpairresolver.cc
@@ -16,11 +16,16 @@
 
 OrderPairResolver::OrderPairResolver(CSolver *_solver, Order *_order) :
 	solver(_solver),
-	order(_order)
+	order(_order),
+	orderPairTable(new HashtableOrderPair())
 {
 }
 
 OrderPairResolver::~OrderPairResolver() {
+	if (orderPairTable != NULL) {
+		orderPairTable->resetanddelete();
+		delete orderPairTable;
+	}
 }
 
 bool OrderPairResolver::resolveOrder(uint64_t first, uint64_t second) {
@@ -42,24 +47,21 @@ bool OrderPairResolver::resolveOrder(uint64_t first, uint64_t second) {
 	}
 
 	//Couldn't infer from graph. Should call the SAT Solver ...
-	switch ( order->type) {
-	case SATC_TOTAL:
-		resolveTotalOrder(first, second);
-	case SATC_PARTIAL:
-	//TODO: Support for partial order ...
-	default:
-		ASSERT(0);
-	}
-
-
+	return getOrderConstraintValue(first, second);
 }
 
-
-bool OrderPairResolver::resolveTotalOrder(uint64_t first, uint64_t second) {
-	ASSERT(order->orderPairTable != NULL);
-	OrderPair pair(first, second, E_NULL);
-	Edge var = getOrderConstraint(order->orderPairTable, &pair);
-	if (edgeIsNull(var))
+bool OrderPairResolver::getOrderConstraintValue(uint64_t first, uint64_t second) {
+	ASSERT(first != second);
+	bool negate = false;
+	OrderPair tmp(first, second);
+	if (first < second) {
+		negate = true;
+		tmp.first = second;
+		tmp.second = first;
+	}
+	if (!orderPairTable->contains(&tmp)) {
 		return false;
-	return getValueCNF(solver->getSATEncoder()->getCNF(), var);
+	}
+	OrderPair *pair = orderPairTable->get(&tmp);
+	return negate ? pair->getNegatedConstraintValue(solver) : pair->getConstraintValue(solver);
 }
diff --git a/src/Translator/orderpairresolver.h b/src/Translator/orderpairresolver.h
index bf7210c..dde7378 100644
--- a/src/Translator/orderpairresolver.h
+++ b/src/Translator/orderpairresolver.h
@@ -15,11 +15,14 @@ class OrderPairResolver : public OrderResolver {
 public:
 	OrderPairResolver(CSolver *_solver, Order *_order);
 	bool resolveOrder(uint64_t first, uint64_t second);
+	HashtableOrderPair* getOrderPairTable() { return orderPairTable;}
 	virtual ~OrderPairResolver();
 private:
 	CSolver *solver;
 	Order *order;
-	bool resolveTotalOrder(uint64_t first, uint64_t second);
+	HashtableOrderPair *orderPairTable;
+	
+	bool getOrderConstraintValue(uint64_t first, uint64_t second);
 };
 
 #endif/* ORDERPAIRRESOLVER_H */