Merge pull request #6585 from diffblue/quantifier-multi-binding

Quantifiers with multiple bindings

Author: kroening

src/solvers/smt2/smt2_conv.cpp

@@ -1972,13 +1972,16 @@ void smt2_convt::convert_expr(const exprt &expr)
     else if(quantifier_expr.id() == ID_exists)
       out << "(exists ";
 
-    exprt bound = quantifier_expr.symbol();
-
-    out << "((";
-    convert_expr(bound);
-    out << " ";
-    convert_type(bound.type());
-    out << ")) ";
+    out << "( ";
+    for(const auto &bound : quantifier_expr.variables())
+    {
+      out << "(";
+      convert_expr(bound);
+      out << " ";
+      convert_type(bound.type());
+      out << ") ";
+    }
+    out << ") ";
 
     convert_expr(quantifier_expr.where());
 
@@ -4566,10 +4569,13 @@ void smt2_convt::find_symbols(const exprt &expr)
     // do not declare the quantified symbol, but record
     // as 'bound symbol'
     const auto &q_expr = to_quantifier_expr(expr);
-    const auto identifier = q_expr.symbol().get_identifier();
-    identifiert &id = identifier_map[identifier];
-    id.type = q_expr.symbol().type();
-    id.is_bound = true;
+    for(const auto &symbol : q_expr.variables())
+    {
+      const auto identifier = symbol.get_identifier();
+      identifiert &id = identifier_map[identifier];
+      id.type = symbol.type();
+      id.is_bound = true;
+    }
     find_symbols(q_expr.where());
     return;
   }

src/util/format_expr.cpp

@@ -356,16 +356,32 @@ void format_expr_configt::setup()
 
   expr_map[ID_forall] =
     [](std::ostream &os, const exprt &expr) -> std::ostream & {
-    return os << u8"\u2200 " << format(to_quantifier_expr(expr).symbol())
-              << " : " << format(to_quantifier_expr(expr).symbol().type())
-              << " . " << format(to_quantifier_expr(expr).where());
+    os << u8"\u2200 ";
+    bool first = true;
+    for(const auto &symbol : to_quantifier_expr(expr).variables())
+    {
+      if(first)
+        first = false;
+      else
+        os << ", ";
+      os << format(symbol) << " : " << format(symbol.type());
+    }
+    return os << " . " << format(to_quantifier_expr(expr).where());
   };
 
   expr_map[ID_exists] =
     [](std::ostream &os, const exprt &expr) -> std::ostream & {
-    return os << u8"\u2203 " << format(to_quantifier_expr(expr).symbol())
-              << " : " << format(to_quantifier_expr(expr).symbol().type())
-              << " . " << format(to_quantifier_expr(expr).where());
+    os << u8"\u2203 ";
+    bool first = true;
+    for(const auto &symbol : to_quantifier_expr(expr).variables())
+    {
+      if(first)
+        first = false;
+      else
+        os << ", ";
+      os << format(symbol) << " : " << format(symbol.type());
+    }
+    return os << " . " << format(to_quantifier_expr(expr).where());
   };
 
   expr_map[ID_let] = [](std::ostream &os, const exprt &expr) -> std::ostream & {

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 <>

src/util/simplify_expr_boolean.cpp

@@ -204,13 +204,13 @@ simplify_exprt::resultt<> simplify_exprt::simplify_not(const not_exprt &expr)
   else if(op.id()==ID_exists) // !(exists: a) <-> forall: not a
   {
     auto const &op_as_exists = to_exists_expr(op);
-    return forall_exprt{op_as_exists.symbol(),
+    return forall_exprt{op_as_exists.variables(),
                         simplify_not(not_exprt(op_as_exists.where()))};
   }
   else if(op.id() == ID_forall) // !(forall: a) <-> exists: not a
   {
     auto const &op_as_forall = to_forall_expr(op);
-    return exists_exprt{op_as_forall.symbol(),
+    return exists_exprt{op_as_forall.variables(),
                         simplify_not(not_exprt(op_as_forall.where()))};
   }