bug fix
authorbdemsky <bdemsky@uci.edu>
Mon, 18 Mar 2019 23:41:46 +0000 (16:41 -0700)
committerbdemsky <bdemsky@uci.edu>
Mon, 18 Mar 2019 23:41:46 +0000 (16:41 -0700)
src/AST/rewriter.cc
src/ASTTransform/decomposeordertransform.cc

index b5127c6..fef4dcb 100644 (file)
@@ -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++) {
index 62b0828..6da5e4a 100644 (file)
@@ -328,7 +328,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;
@@ -358,7 +363,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;