Avoid use of sort_and_join in guard operations

Author: tautschnig

src/goto-symex/goto_symex_state.h

@@ -188,6 +188,7 @@ class goto_symex_statet
     level2t::current_namest level2_current_names;
     value_sett value_set;
     guardt guard;
+    guardt guard_before_branch;
     propagationt propagation;
     unsigned atomic_section_id;
 

src/goto-symex/symex_goto.cpp

@@ -158,6 +158,7 @@ void goto_symext::symex_goto(statet &state)
       state.rename(guard_expr, ns);
     }
 
+    new_state.guard_before_branch=state.guard;
     if(forward)
     {
       new_state.guard.add(guard_expr);
@@ -366,11 +367,38 @@ void goto_symext::phi_function(
     else
     {
       guardt tmp_guard(goto_state.guard);
+      guardt tmp_guard2(goto_state.guard);
 
       // this gets the diff between the guards
-      tmp_guard-=dest_state.guard;
-
-      rhs=if_exprt(tmp_guard.as_expr(), goto_state_rhs, dest_state_rhs);
+      // tmp_guard-=dest_state.guard;
+      if(!goto_state.guard_before_branch.is_constant())
+      {
+        assert(tmp_guard2.id()==ID_and);
+
+        if(goto_state.guard_before_branch.id()==ID_and)
+        {
+          assert(tmp_guard2.operands().size()>
+                 goto_state.guard_before_branch.operands().size());
+          for(const auto & op : goto_state.guard_before_branch.operands())
+          {
+            // assert(tmp_guard2.operands().front()==op);
+            (void)op;
+            tmp_guard2.operands().erase(tmp_guard2.operands().begin());
+          }
+        }
+        else
+        {
+          assert(tmp_guard2.operands().front()==
+                 goto_state.guard_before_branch);
+          tmp_guard2.operands().erase(tmp_guard2.operands().begin());
+        }
+
+        if(tmp_guard2.operands().size()==1)
+          tmp_guard2=tmp_guard2.op0();
+      }
+      // assert(tmp_guard==tmp_guard2);
+
+      rhs=if_exprt(tmp_guard2.as_expr(), goto_state_rhs, dest_state_rhs);
       do_simplify(rhs);
     }
 

src/util/guard.cpp

@@ -187,6 +187,22 @@ guardt& guardt::logical_or(const guardt &g2, const namespacet &ns)
   if(g2.is_false() || g1.is_true()) return g1;
   if(g1.is_false() || g2.is_true()) { g1=g2; return g1; }
 
+  {
+    exprt tmp(g2);
+    tmp.make_not();
+
+    if(tmp==g1)
+      g1.make_true();
+    else
+      g1=or_exprt(g1, g2);
+
+    bdd_exprt t(ns);
+    t.from_expr(g1);
+    g1=t.as_expr();
+
+    return g1;
+  }
+
   if(g1.id()!=ID_and || g2.id()!=ID_and)
   {
     exprt tmp(g2);