From eabd67c6e77440393a041f309e47837e985e893b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 3 Jan 2017 13:47:51 +0000 Subject: [PATCH] Do not unnecessarily sort guard conjuncts Guards are (no longer) generic conjunctions. They are constructed in a consistent order. If a more generic set-up is required, use BDD-backed guards. --- src/analyses/guard_expr.cpp | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/analyses/guard_expr.cpp b/src/analyses/guard_expr.cpp index a5c09fb3241..b290e214fff 100644 --- a/src/analyses/guard_expr.cpp +++ b/src/analyses/guard_expr.cpp @@ -101,9 +101,7 @@ guard_exprt &operator-=(guard_exprt &g1, const guard_exprt &g2) return g1; } - sort_and_join(g1.expr); exprt g2_sorted = g2.as_expr(); - sort_and_join(g2_sorted); exprt::operandst &op1 = g1.expr.operands(); const exprt::operandst &op2 = g2_sorted.operands(); @@ -112,10 +110,10 @@ guard_exprt &operator-=(guard_exprt &g1, const guard_exprt &g2) for(exprt::operandst::const_iterator it2 = op2.begin(); it2 != op2.end(); ++it2) { - while(it1 != op1.end() && *it1 < *it2) - ++it1; if(it1 != op1.end() && *it1 == *it2) it1 = op1.erase(it1); + else + break; } g1.expr = conjunction(op1); @@ -159,9 +157,7 @@ guard_exprt &operator|=(guard_exprt &g1, const guard_exprt &g2) } // find common prefix - sort_and_join(g1.expr); exprt g2_sorted = g2.as_expr(); - sort_and_join(g2_sorted); exprt::operandst &op1 = g1.expr.operands(); const exprt::operandst &op2 = g2_sorted.operands();