constructors for forall_expr/exists_exprt with multiple bindings

This adds convenience constructors for forall/exists expressions with
multiple bindings.

Author: kroening

src/util/mathematical_expr.h

@@ -336,6 +336,11 @@ class forall_exprt : public quantifier_exprt
     : quantifier_exprt(ID_forall, _symbol, _where)
   {
   }
+
+  forall_exprt(const binding_exprt::variablest &_variables, const exprt &_where)
+    : quantifier_exprt(ID_forall, _variables, _where)
+  {
+  }
 };
 
 template <>
@@ -373,6 +378,11 @@ class exists_exprt : public quantifier_exprt
     : quantifier_exprt(ID_exists, _symbol, _where)
   {
   }
+
+  exists_exprt(const binding_exprt::variablest &_variables, const exprt &_where)
+    : quantifier_exprt(ID_exists, _variables, _where)
+  {
+  }
 };
 
 template <>