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

diff --combined src/ASTTransform/decomposeordertransform.cc
index eaf81415bdb74a31771ad9c541761d1f78187606,6da5e4aa5eb3765c87fe921bc48f749c033e69f0..4b3fc4adca1cdcc491c218ecc0043a3bfce0bb9a
--- 1/src/ASTTransform/decomposeordertransform.cc
--- 2/src/ASTTransform/decomposeordertransform.cc
+++ b/src/ASTTransform/decomposeordertransform.cc
@@@ -28,8 -28,6 +28,8 @@@ DecomposeOrderTransform::~DecomposeOrde
  }
  
  void DecomposeOrderTransform::doTransform() {
 +      if(solver->isUnSAT())
 +              return;
        HashsetOrder *orders = solver->getActiveOrders()->copy();
        SetIteratorOrder *orderit = orders->iterator();
        while (orderit->hasNext()) {
@@@ -330,7 -328,12 +330,12 @@@ void DecomposeOrderTransform::mergeNode
                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 -363,12 +365,12 @@@
                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;