Add to_forall_expr

There was a cast operation for exists, but none for forall.

Author: tautschnig

src/util/mathematical_expr.h

@@ -257,7 +257,7 @@ inline void validate_expr(const function_application_exprt &value)
 }
 
 /// \brief A base class for quantifier expressions
-class quantifier_exprt : public binary_predicate_exprt
+class quantifier_exprt:public binary_predicate_exprt
 {
 public:
   quantifier_exprt(
@@ -297,9 +297,8 @@ class quantifier_exprt : public binary_predicate_exprt
 /// \return Object of type \ref quantifier_exprt
 inline const quantifier_exprt &to_quantifier_expr(const exprt &expr)
 {
-  DATA_INVARIANT(
-    expr.operands().size() == 2,
-    "quantifier expressions must have two operands");
+  DATA_INVARIANT(expr.operands().size()==2,
+                 "quantifier expressions must have two operands");
   DATA_INVARIANT(
     expr.op0().id() == ID_symbol, "quantified variable shall be a symbol");
   return static_cast<const quantifier_exprt &>(expr);
@@ -308,27 +307,26 @@ inline const quantifier_exprt &to_quantifier_expr(const exprt &expr)
 /// \copydoc to_quantifier_expr(const exprt &)
 inline quantifier_exprt &to_quantifier_expr(exprt &expr)
 {
-  DATA_INVARIANT(
-    expr.operands().size() == 2,
-    "quantifier expressions must have two operands");
+  DATA_INVARIANT(expr.operands().size()==2,
+                 "quantifier expressions must have two operands");
   DATA_INVARIANT(
     expr.op0().id() == ID_symbol, "quantified variable shall be a symbol");
   return static_cast<quantifier_exprt &>(expr);
 }
 
-template <>
-inline bool can_cast_expr<quantifier_exprt>(const exprt &base)
+template<> inline bool can_cast_expr<quantifier_exprt>(const exprt &base)
 {
   return base.id() == ID_forall || base.id() == ID_exists;
 }
 
 inline void validate_expr(const quantifier_exprt &value)
 {
-  validate_operands(value, 2, "quantifier expressions must have two operands");
+  validate_operands(value, 2,
+    "quantifier expressions must have two operands");
 }
 
 /// \brief A forall expression
-class forall_exprt : public quantifier_exprt
+class forall_exprt:public quantifier_exprt
 {
 public:
   forall_exprt(const symbol_exprt &_symbol, const exprt &_where)
@@ -337,8 +335,26 @@ class forall_exprt : public quantifier_exprt
   }
 };
 
+inline const forall_exprt &to_forall_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_forall);
+  DATA_INVARIANT(
+    expr.operands().size() == 2,
+    "forall expressions have exactly two operands");
+  return static_cast<const forall_exprt &>(expr);
+}
+
+inline forall_exprt &to_forall_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_forall);
+  DATA_INVARIANT(
+    expr.operands().size() == 2,
+    "forall expressions have exactly two operands");
+  return static_cast<forall_exprt &>(expr);
+}
+
 /// \brief An exists expression
-class exists_exprt : public quantifier_exprt
+class exists_exprt:public quantifier_exprt
 {
 public:
   exists_exprt(const symbol_exprt &_symbol, const exprt &_where)