Avoid use of sort_and_join in guard operations

Author: tautschnig

src/goto-symex/goto_symex_state.h

@@ -193,6 +193,7 @@ class goto_symex_statet
     value_sett value_set;
     guardt guard;
     symex_targett::sourcet source;
+    guardt guard_before_branch;
     propagationt propagation;
     unsigned atomic_section_id;
 

src/goto-symex/symex_goto.cpp

@@ -175,6 +175,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);
@@ -280,10 +281,38 @@ void goto_symext::phi_function(
 
   if(!variables.empty())
   {
-    diff_guard=goto_state.guard;
+    guardt tmp_guard(goto_state.guard);
+    guardt tmp_guard2(goto_state.guard);
 
     // this gets the diff between the guards
-    diff_guard-=dest_state.guard;
+    // 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);
+    diff_guard=tmp_guard2;
   }
 
   for(std::unordered_set<ssa_exprt, irep_hash>::const_iterator

src/util/guard.cpp

@@ -132,6 +132,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);