Merge pull request #3236 from diffblue/cond_exprt

added cond_exprt

Author: Daniel Kroening

src/solvers/flattening/boolbv.cpp

@@ -207,7 +207,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   else if(expr.id()==ID_case)
     return convert_case(expr);
   else if(expr.id()==ID_cond)
-    return convert_cond(expr);
+    return convert_cond(to_cond_expr(expr));
   else if(expr.id()==ID_if)
     return convert_if(to_if_expr(expr));
   else if(expr.id()==ID_constant)
@@ -481,7 +481,7 @@ literalt boolbvt::convert_rest(const exprt &expr)
   }
   else if(expr.id()==ID_cond)
   {
-    bvt bv=convert_cond(expr);
+    bvt bv = convert_cond(to_cond_expr(expr));
     CHECK_RETURN(bv.size() == 1);
     return bv[0];
   }

src/solvers/flattening/boolbv.h

@@ -161,7 +161,7 @@ class boolbvt:public arrayst
   virtual bvt convert_with(const exprt &expr);
   virtual bvt convert_update(const exprt &expr);
   virtual bvt convert_case(const exprt &expr);
-  virtual bvt convert_cond(const exprt &expr);
+  virtual bvt convert_cond(const cond_exprt &);
   virtual bvt convert_shift(const binary_exprt &expr);
   virtual bvt convert_bitwise(const exprt &expr);
   virtual bvt convert_unary_minus(const unary_minus_exprt &expr);

src/solvers/flattening/boolbv_cond.cpp

@@ -10,10 +10,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/invariant.h>
 
-bvt boolbvt::convert_cond(const exprt &expr)
+bvt boolbvt::convert_cond(const cond_exprt &expr)
 {
-  PRECONDITION(expr.id() == ID_cond);
-
   const exprt::operandst &operands=expr.operands();
 
   std::size_t width=boolbv_width(expr.type());

src/util/std_expr.h

@@ -4749,4 +4749,49 @@ inline void validate_expr(const popcount_exprt &value)
   validate_operands(value, 1, "popcount must have one operand");
 }
 
+/// this is a parametric version of an if-expression: it returns
+/// the value of the first case (using the ordering of the operands)
+/// whose condition evaluates to true.
+class cond_exprt : public multi_ary_exprt
+{
+public:
+  explicit cond_exprt(const typet &_type) : multi_ary_exprt(ID_cond, _type)
+  {
+  }
+
+  /// adds a case to a cond expression
+  /// \param condition: the condition for the case
+  /// \param value: the value for the case
+  void add_case(const exprt &condition, const exprt &value)
+  {
+    PRECONDITION(condition.type().id() == ID_bool);
+    operands().reserve(operands().size() + 2);
+    operands().push_back(condition);
+    operands().push_back(value);
+  }
+};
+
+/// \brief Cast an exprt to a \ref cond_exprt
+///
+/// \a expr must be known to be \ref cond_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref cond_exprt
+inline const cond_exprt &to_cond_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_cond);
+  DATA_INVARIANT(
+    expr.operands().size() % 2 != 0, "cond must have even number of operands");
+  return static_cast<const cond_exprt &>(expr);
+}
+
+/// \copydoc to_popcount_expr(const exprt &)
+inline cond_exprt &to_cond_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_cond);
+  DATA_INVARIANT(
+    expr.operands().size() % 2 != 0, "cond must have even number of operands");
+  return static_cast<cond_exprt &>(expr);
+}
+
 #endif // CPROVER_UTIL_STD_EXPR_H