introduce binding_exprt

This is a base class that factors out some common functionality of various
expressions that are variable bindings; examples are let, lambda, forall,
exists; future additions might include choose.

Author: Daniel Kroening

src/util/mathematical_expr.h

@@ -273,6 +273,47 @@ inline function_application_exprt &to_function_application_expr(exprt &expr)
   return ret;
 }
 
+/// \brief A base class for variable bindings (quantifiers, let, lambda)
+class binding_exprt : public binary_exprt
+{
+public:
+  using variablest = std::vector<symbol_exprt>;
+
+  /// construct the binding expression
+  binding_exprt(
+    irep_idt _id,
+    const variablest &_variables,
+    exprt _where,
+    typet _type)
+    : binary_exprt(
+        tuple_exprt((const operandst &)_variables),
+        _id,
+        std::move(_where),
+        std::move(_type))
+  {
+  }
+
+  variablest &variables()
+  {
+    return (variablest &)static_cast<tuple_exprt &>(op0()).operands();
+  }
+
+  const variablest &variables() const
+  {
+    return (variablest &)static_cast<const tuple_exprt &>(op0()).operands();
+  }
+
+  exprt &where()
+  {
+    return op1();
+  }
+
+  const exprt &where() const
+  {
+    return op1();
+  }
+};
+
 /// \brief A base class for quantifier expressions
 class quantifier_exprt : public binary_predicate_exprt
 {