From: Hamed Gorjiara <hgorjiar@uci.edu>
Date: Tue, 19 Mar 2019 01:10:38 +0000 (-0700)
Subject: Merge branch 'tuner' of ssh://demsky.eecs.uci.edu/home/git/constraint_compiler
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=860bf6b84ae2317d04e6c6494e4bc9ad824786b9;hp=8b4305d89bd420fa061f9a40ff813ec0ba6fb9fe

Merge branch 'tuner' of ssh://demsky.eecs.uci.edu/home/git/constraint_compiler
---

diff --git a/src/AST/rewriter.cc b/src/AST/rewriter.cc
index b5127c6..fef4dcb 100644
--- a/src/AST/rewriter.cc
+++ b/src/AST/rewriter.cc
@@ -23,7 +23,7 @@ void CSolver::replaceBooleanWithFalseNoRemove(BooleanEdge bexpr) {
 void CSolver::replaceBooleanWithTrueNoRemove(BooleanEdge bexpr) {
 	updateMustValue(bexpr.getBoolean(), bexpr.isNegated() ? BV_MUSTBEFALSE : BV_MUSTBETRUE);
 
-	ASSERT(bexpr->boolVal != BV_UNSAT);
+	ASSERT((bexpr->boolVal != BV_UNSAT ) || unsat);
 
 	uint size = bexpr->parents.getSize();
 	for (uint i = 0; i < size; i++) {
diff --git a/src/ASTTransform/decomposeordertransform.cc b/src/ASTTransform/decomposeordertransform.cc
index eaf8141..4b3fc4a 100644
--- a/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@ -330,7 +330,12 @@ void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, Ord
 		BooleanEdge be = solver->orderConstraint(graph->getOrder(), source->getID(), dstnode->getID());
 		BooleanEdge benew = solver->orderConstraint(graph->getOrder(), source->getID(), node->getID());
 		updateEdgePolarity(benew, be);
-		solver->replaceBooleanWithBoolean(be, benew);
+		if (solver->isTrue(benew))
+		  solver->replaceBooleanWithTrue(be);
+		else if (solver->isFalse(benew))
+		  solver->replaceBooleanWithFalse(be);
+		else
+		  solver->replaceBooleanWithBoolean(be, benew);
 	}
 	dstnode->inEdges.reset();
 	delete inedgeit;
@@ -360,7 +365,12 @@ void DecomposeOrderTransform::mergeNodes(OrderGraph *graph, OrderNode *node, Ord
 		BooleanEdge be = solver->orderConstraint(graph->getOrder(), dstnode->getID(), sink->getID());
 		BooleanEdge benew = solver->orderConstraint(graph->getOrder(), node->getID(), sink->getID());
 		updateEdgePolarity(benew, be);
-		solver->replaceBooleanWithBoolean(be, benew);
+		if (solver->isTrue(benew))
+		  solver->replaceBooleanWithTrue(be);
+		else if (solver->isFalse(benew))
+		  solver->replaceBooleanWithFalse(be);
+		else
+		  solver->replaceBooleanWithBoolean(be, benew);
 	}
 	dstnode->outEdges.reset();
 	delete outedgeit;