WIP

Author: tautschnig

src/solvers/strings/string_refinement.cpp

@@ -854,6 +854,34 @@ decision_proceduret::resultt string_refinementt::dec_solve()
   return resultt::D_ERROR;
 }
 
+static exprt simplify_if_recursive(exprt expr, const namespacet &ns)
+{
+  for(auto it = expr.depth_begin(); it != expr.depth_end(); )
+  {
+    if(it->id() == ID_if)
+    {
+      if_exprt if_expr = to_if_expr(*it);
+      const exprt simp_cond = simplify_expr(if_expr.cond(), ns);
+      if(simp_cond.is_true())
+      {
+        it.mutate() = simplify_if_recursive(if_expr.true_case(), ns);
+        it.next_sibling_or_parent();
+      }
+      else if(simp_cond.is_false())
+      {
+        it.mutate() = simplify_if_recursive(if_expr.false_case(), ns);
+        it.next_sibling_or_parent();
+      }
+      else
+        ++it;
+    }
+    else
+      ++it;
+  }
+
+  return expr;
+}
+
 /// Add the given lemma to the solver.
 /// \param lemma: a Boolean expression
 /// \param simplify_lemma: whether the lemma should be simplified before being
@@ -869,7 +897,10 @@ void string_refinementt::add_lemma(
 
   exprt simple_lemma = lemma;
   if(simplify_lemma)
+  {
+    simple_lemma = simplify_if_recursive(std::move(simple_lemma), ns);
     simplify(simple_lemma, ns);
+  }
 
   if(simple_lemma.is_true())
   {

src/util/simplify_expr.cpp

@@ -31,10 +31,10 @@ Author: Daniel Kroening, [email protected]
 
 // #define DEBUGX
 
-#ifdef DEBUGX
+//#ifdef DEBUGX
 #include "format_expr.h"
 #include <iostream>
-#endif
+//#endif
 
 #include "simplify_expr_class.h"
 
@@ -2542,6 +2542,12 @@ bool simplify_exprt::simplify_rec(exprt &expr)
 
   if(!result)
   {
+    if(tmp.type() != expr.type())
+    {
+      std::cerr << format(tmp) << std::endl;
+      std::cerr << format(expr) << std::endl;
+      std::cerr << expr.type().pretty() << std::endl;
+    }
     POSTCONDITION(tmp.type() == expr.type());
     expr.swap(tmp);