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 b5127c64ba2b480b9ae14e74625da76996c4444d..fef4dcbb17aaf40626791272a67db9d68cf0de11 100644 (file)
--- 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 eaf81415bdb74a31771ad9c541761d1f78187606..4b3fc4adca1cdcc491c218ecc0043a3bfce0bb9a 100644 (file)
--- 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;