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://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=3552af833b3ff76f221d6c9a9e410da96dd58734;p=satune.git

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

3552af833b3ff76f221d6c9a9e410da96dd58734
diff --cc src/ASTAnalyses/Order/ordergraph.cc
index 2127db9,0000000..ce9a071
mode 100644,000000..100644
--- a/src/ASTAnalyses/Order/ordergraph.cc
+++ b/src/ASTAnalyses/Order/ordergraph.cc
@@@ -1,221 -1,0 +1,227 @@@
 +#include "ordergraph.h"
 +#include "ordernode.h"
 +#include "boolean.h"
 +#include "orderedge.h"
 +#include "ordergraph.h"
 +#include "order.h"
 +
 +OrderGraph::OrderGraph(Order *_order) :
 +	nodes(new HashsetOrderNode()),
 +	edges(new HashsetOrderEdge()),
 +	order(_order) {
 +}
 +
 +OrderGraph *buildOrderGraph(Order *order) {
 +	OrderGraph *orderGraph = new OrderGraph(order);
 +	order->graph = orderGraph;
 +	uint constrSize = order->constraints.getSize();
 +	for (uint j = 0; j < constrSize; j++) {
 +		orderGraph->addOrderConstraintToOrderGraph(order->constraints.get(j));
 +	}
 +	return orderGraph;
 +}
 +
 +//Builds only the subgraph for the must order graph.
 +OrderGraph *buildMustOrderGraph(Order *order) {
 +	OrderGraph *orderGraph = new OrderGraph(order);
 +	uint constrSize = order->constraints.getSize();
 +	for (uint j = 0; j < constrSize; j++) {
 +		orderGraph->addMustOrderConstraintToOrderGraph(order->constraints.get(j));
 +	}
 +	return orderGraph;
 +}
 +
 +void OrderGraph::addOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
 +	Polarity polarity = constr->polarity;
 +	BooleanValue mustval = constr->boolVal;
 +	switch (polarity) {
 +	case P_BOTHTRUEFALSE:
 +	case P_TRUE: {
 +		OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
 +		if (mustval == BV_MUSTBETRUE || mustval == BV_UNSAT)
 +			_1to2->mustPos = true;
 +		_1to2->polPos = true;
 +		node1->addNewOutgoingEdge(_1to2);
 +		node2->addNewIncomingEdge(_1to2);
 +		if (constr->polarity == P_TRUE)
 +			break;
 +	}
 +	case P_FALSE: {
 +		if (order->type == SATC_TOTAL) {
 +			OrderEdge *_2to1 = getOrderEdgeFromOrderGraph( node2, node1);
 +			if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
 +				_2to1->mustPos = true;
 +			_2to1->polPos = true;
 +			node2->addNewOutgoingEdge(_2to1);
 +			node1->addNewIncomingEdge(_2to1);
 +		} else {
 +			OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
 +			if (mustval == BV_MUSTBEFALSE || mustval == BV_UNSAT)
 +				_1to2->mustNeg = true;
 +			_1to2->polNeg = true;
 +			node1->addNewOutgoingEdge(_1to2);
 +			node2->addNewIncomingEdge(_1to2);
 +		}
 +		break;
 +	}
 +	case P_UNDEFINED:
 +		//There is an unreachable order constraint if this assert fires
 +		//Clients can easily do this, so don't do anything.
 +		;
 +	}
 +}
 +
 +void OrderGraph::addMustOrderEdge(OrderNode *node1, OrderNode *node2, BooleanOrder *constr) {
 +	BooleanValue mustval = constr->boolVal;
 +	switch (mustval) {
 +	case BV_UNSAT:
 +	case BV_MUSTBETRUE: {
 +		OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
 +		_1to2->mustPos = true;
 +		_1to2->polPos = true;
 +		node1->addNewOutgoingEdge(_1to2);
 +		node2->addNewIncomingEdge(_1to2);
 +		if (constr->boolVal == BV_MUSTBETRUE)
 +			break;
 +	}
 +	case BV_MUSTBEFALSE: {
 +		if (order->type == SATC_TOTAL) {
 +			OrderEdge *_2to1 = getOrderEdgeFromOrderGraph(node2, node1);
 +			_2to1->mustPos = true;
 +			_2to1->polPos = true;
 +			node2->addNewOutgoingEdge(_2to1);
 +			node1->addNewIncomingEdge(_2to1);
 +		} else {
 +			OrderEdge *_1to2 = getOrderEdgeFromOrderGraph(node1, node2);
 +			_1to2->mustNeg = true;
 +			_1to2->polNeg = true;
 +			node1->addNewOutgoingEdge(_1to2);
 +			node2->addNewIncomingEdge(_1to2);
 +		}
 +		break;
 +	}
 +	case BV_UNDEFINED:
 +		//Do Nothing
 +		break;
 +	}
 +}
 +
 +OrderNode *OrderGraph::getOrderNodeFromOrderGraph(uint64_t id) {
 +	OrderNode *node = new OrderNode(id);
 +	OrderNode *tmp = nodes->get(node);
 +	if ( tmp != NULL) {
 +		delete node;
 +		node = tmp;
 +	} else {
 +		nodes->add(node);
 +	}
 +	return node;
 +}
 +
 +OrderNode *OrderGraph::lookupOrderNodeFromOrderGraph(uint64_t id) {
 +	OrderNode node(id);
 +	OrderNode *tmp = nodes->get(&node);
 +	return tmp;
 +}
 +
 +OrderEdge *OrderGraph::getOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
 +	OrderEdge *edge = new OrderEdge(begin, end);
 +	OrderEdge *tmp = edges->get(edge);
 +	if ( tmp != NULL ) {
 +		delete edge;
 +		edge = tmp;
 +	} else {
 +		edges->add(edge);
 +	}
 +	return edge;
 +}
 +
 +OrderEdge *OrderGraph::lookupOrderEdgeFromOrderGraph(OrderNode *begin, OrderNode *end) {
 +	OrderEdge edge(begin, end);
 +	OrderEdge *tmp = edges->get(&edge);
 +	return tmp;
 +}
 +
 +OrderEdge *OrderGraph::getInverseOrderEdge(OrderEdge *edge) {
 +	OrderEdge inverseedge(edge->sink, edge->source);
 +	OrderEdge *tmp = edges->get(&inverseedge);
 +	return tmp;
 +}
 +
 +void OrderGraph::addOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
 +	OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
 +	OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
 +	addOrderEdge(from, to, bOrder);
 +}
 +
 +void OrderGraph::addMustOrderConstraintToOrderGraph(BooleanOrder *bOrder) {
 +	OrderNode *from = getOrderNodeFromOrderGraph(bOrder->first);
 +	OrderNode *to = getOrderNodeFromOrderGraph(bOrder->second);
 +	addMustOrderEdge(from, to, bOrder);
 +}
 +
 +OrderGraph::~OrderGraph() {
 +	SetIteratorOrderNode *iterator = nodes->iterator();
 +	while (iterator->hasNext()) {
 +		OrderNode *node = iterator->next();
 +		delete node;
 +	}
 +	delete iterator;
 +
 +	SetIteratorOrderEdge *eiterator = edges->iterator();
 +	while (eiterator->hasNext()) {
 +		OrderEdge *edge = eiterator->next();
 +		delete edge;
 +	}
 +	delete eiterator;
 +	delete nodes;
 +	delete edges;
 +}
 +
 +bool OrderGraph::isTherePath(OrderNode *source, OrderNode *destination){
 +	HashsetOrderNode visited;
 +	visited.add(source);
 +	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;
++				}
 +			}
 +		}
 +	}
 +	delete iterator;
 +	return found;
 +}
 +
 +bool OrderGraph::isTherePathVisit(HashsetOrderNode &visited, OrderNode* current, OrderNode* destination){
 +	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;
 +	return found;
 +}