From 3b44d67aa34198bde59d8b346ea316ba7fb6d73d Mon Sep 17 00:00:00 2001
From: bdemsky <bdemsky@uci.edu>
Date: Mon, 4 Sep 2017 23:15:20 -0700
Subject: [PATCH] Tons of bugs

---
 src/AST/boolean.cc                          |  3 ++
 src/AST/rewriter.cc                         | 11 +++----
 src/ASTTransform/decomposeordertransform.cc | 33 ++++++++++++++++-----
 src/ASTTransform/integerencoding.cc         |  1 -
 src/Backend/satorderencoder.cc              |  4 +--
 5 files changed, 37 insertions(+), 15 deletions(-)

diff --git a/src/AST/boolean.cc b/src/AST/boolean.cc
index 5d8865e..4ca9c40 100644
--- a/src/AST/boolean.cc
+++ b/src/AST/boolean.cc
@@ -47,6 +47,9 @@ BooleanLogic::BooleanLogic(CSolver *solver, LogicOp _op, BooleanEdge *array, uin
 	op(_op),
 	replaced(false),
 	inputs(array, asize) {
+	for (uint i = 0; i < asize; i++) {
+		array[i]->parents.push(this);
+	}
 }
 
 BooleanEdge cloneEdge(CSolver *solver, CloneMap *map, BooleanEdge e) {
diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index cdb2fb4..937a8b7 100644
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -59,19 +59,20 @@ void CSolver::replaceBooleanWithBoolean(BooleanEdge oldb, BooleanEdge newb) {
 	for (uint i = 0; i < size; i++) {
 		Boolean *parent = oldb->parents.get(i);
 		BooleanLogic *logicop = (BooleanLogic *) parent;
-
+		boolMap.remove(parent); //could change parent's hash
+		
 		uint parentsize = logicop->inputs.getSize();
-
 		for (uint j = 0; j < parentsize; j++) {
-			BooleanEdge b = logicop->inputs.get(i);
+			BooleanEdge b = logicop->inputs.get(j);
 			if (b == oldb) {
-				logicop->inputs.set(i, newb);
+				logicop->inputs.set(j, newb);
 				newb->parents.push(parent);
 			} else if (b == oldbnegated) {
-				logicop->inputs.set(i, newb.negate());
+				logicop->inputs.set(j, newb.negate());
 				newb->parents.push(parent);
 			}
 		}
+		boolMap.put(parent, parent);
 	}
 }
 
diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index 359a3a3..3791b10 100644
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -84,14 +84,33 @@ void DecomposeOrderTransform::decomposeOrder (Order *currOrder, OrderGraph *curr
 		OrderNode *from = currGraph->getOrderNodeFromOrderGraph(orderconstraint->first);
 		OrderNode *to = currGraph->getOrderNodeFromOrderGraph(orderconstraint->second);
 		if (from->sccNum != to->sccNum) {
-			OrderEdge *edge = currGraph->getOrderEdgeFromOrderGraph(from, to);
-			if (edge->polPos) {
-				solver->replaceBooleanWithTrue(orderconstraint);
-			} else if (edge->polNeg) {
-				solver->replaceBooleanWithFalse(orderconstraint);
+			OrderEdge *edge = currGraph->lookupOrderEdgeFromOrderGraph(from, to);
+			if (edge != NULL) {
+				if (edge->polPos) {
+					solver->replaceBooleanWithTrue(orderconstraint);
+				} else if (edge->polNeg) {
+					solver->replaceBooleanWithFalse(orderconstraint);
+				} else {
+					//This case should only be possible if constraint isn't in AST
+					//This can happen, so don't do anything
+					;
+				}
 			} else {
-				//This case should only be possible if constraint isn't in AST
-				ASSERT(0);
+				OrderEdge *invedge = currGraph->lookupOrderEdgeFromOrderGraph(to, from);
+				if (invedge != NULL) {
+					if (invedge->polPos) {
+						solver->replaceBooleanWithFalse(orderconstraint);
+					} else if (edge->polNeg) {
+						//This case shouldn't happen...  If we have a partial order,
+						//then we should have our own edge...If we have a total
+						//order, then this edge should be positive...
+						ASSERT(0);
+					} else {
+						//This case should only be possible if constraint isn't in AST
+						//This can happen, so don't do anything
+						;
+					}
+				}
 			}
 		} else {
 			//Build new order and change constraint's order
diff --git a/src/ASTTransform/integerencoding.cc b/src/ASTTransform/integerencoding.cc
index b52ccf8..25ef990 100644
--- a/src/ASTTransform/integerencoding.cc
+++ b/src/ASTTransform/integerencoding.cc
@@ -48,7 +48,6 @@ void IntegerEncodingTransform::orderIntegerEncodingSATEncoder(BooleanOrder *bool
 	Predicate *predicate = solver->createPredicateOperator(SATC_LT, sarray, 2);
 	Element *parray[] = {elem1, elem2};
 	BooleanEdge boolean = solver->applyPredicate(predicate, parray, 2);
-	solver->addConstraint(boolean);
 	solver->replaceBooleanWithBoolean(boolOrder, boolean);
 }
 
diff --git a/src/Backend/satorderencoder.cc b/src/Backend/satorderencoder.cc
index 514bad9..b977efa 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);
@@ -81,6 +79,8 @@ Edge SATEncoder::getPairConstraint(Order *order, OrderPair *pair) {
 Edge SATEncoder::encodeTotalOrderSATEncoder(BooleanOrder *boolOrder) {
 	ASSERT(boolOrder->order->type == SATC_TOTAL);
 	if (boolOrder->order->orderPairTable == 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) {
-- 
2.34.1