Add lift_cond

This is just like lift_if, but for cond_exprt

Author: smowton

src/util/expr_util.cpp

@@ -216,6 +216,24 @@ if_exprt lift_if(const exprt &src, std::size_t operand_number)
   return result;
 }
 
+cond_exprt lift_cond(const exprt &src, std::size_t operand_number)
+{
+  PRECONDITION(operand_number < src.operands().size());
+  PRECONDITION(src.operands()[operand_number].id() == ID_cond);
+
+  const cond_exprt cond_expr = to_cond_expr(src.operands()[operand_number]);
+  cond_exprt result({}, src.type(), cond_expr.is_exclusive());
+
+  for(std::size_t i = 0; i < cond_expr.get_n_cases(); ++i)
+  {
+    exprt new_value = src;
+    new_value.operands()[operand_number] = cond_expr.value(i);
+    result.add_case(cond_expr.condition(i), new_value);
+  }
+
+  return result;
+}
+
 const exprt &skip_typecast(const exprt &expr)
 {
   if(expr.id()!=ID_typecast)

src/util/expr_util.h

@@ -26,6 +26,7 @@ class symbol_exprt;
 class update_exprt;
 class with_exprt;
 class if_exprt;
+class cond_exprt;
 class symbolt;
 class typet;
 class namespacet;
@@ -74,6 +75,9 @@ bool has_subtype(const typet &, const irep_idt &id, const namespacet &);
 /// lift up an if_exprt one level
 if_exprt lift_if(const exprt &, std::size_t operand_number);
 
+/// lift up an cond_exprt one level
+cond_exprt lift_cond(const exprt &, std::size_t operand_number);
+
 /// find the expression nested inside typecasts, if any
 const exprt &skip_typecast(const exprt &expr);