quantifiers are variable bindings

This commit makes the quantifier base class use the bindings base class.
Methods and constructor for the special case of quantifying over one
variable are retained.

Author: Daniel Kroening

src/ansi-c/c_typecheck_expr.cpp

@@ -292,12 +292,12 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
   else if(expr.id()==ID_forall ||
           expr.id()==ID_exists)
   {
-    // op0 is a declaration,
-    // op1 the bound expression
+    // op0 is a tuple with one declaration,
+    // op1 is the bound expression
     assert(expr.operands().size()==2);
     expr.type()=bool_typet();
 
-    if(expr.op0().get(ID_statement)!=ID_decl)
+    if(expr.op0().op0().get(ID_statement) != ID_decl)
     {
       error().source_location = expr.source_location();
       error() << "expected declaration as operand of quantifier" << eom;
@@ -311,9 +311,8 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
       throw 0;
     }
 
-    // replace declaration by symbol expression
-    symbol_exprt bound=to_symbol_expr(expr.op0().op0());
-    expr.op0().swap(bound);
+    // replace declarations by symbol expressions
+    expr.op0().op0() = to_symbol_expr(expr.op0().op0().op0());
 
     implicit_typecast_bool(expr.op1());
   }
@@ -739,9 +738,9 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr)
   else if(expr.id()==ID_forall || expr.id()==ID_exists)
   {
     assert(expr.operands().size()==2);
+    assert(expr.op0().operands().size() == 1);
 
-    ansi_c_declarationt &declaration=
-      to_ansi_c_declaration(expr.op0());
+    ansi_c_declarationt &declaration = to_ansi_c_declaration(expr.op0().op0());
 
     typecheck_declaration(declaration);
 
@@ -780,7 +779,7 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr)
     code_declt decl(symbol.symbol_expr());
     decl.add_source_location()=declaration.source_location();
 
-    expr.op0()=decl;
+    expr.op0().op0() = decl;
 
     typecheck_expr(expr.op1());
   }

src/ansi-c/expr2c.cpp

@@ -798,13 +798,17 @@ std::string expr2ct::convert_quantifier(
   if(src.operands().size()!=2)
     return convert_norep(src, precedence);
 
+  // our made-up syntax can only do one symbol
+  if(src.op0().operands().size() != 1)
+    return convert_norep(src, precedence);
+
   unsigned p0, p1;
 
-  std::string op0=convert_with_precedence(src.op0(), p0);
+  std::string op0 = convert_with_precedence(src.op0().op0(), p0);
   std::string op1=convert_with_precedence(src.op1(), p1);
 
   std::string dest=symbol+" { ";
-  dest+=convert(src.op0().type());
+  dest += convert(src.op0().op0().type());
   dest+=" "+op0+"; ";
   dest+=op1;
   dest+=" }";

src/ansi-c/parser.y

@@ -26,6 +26,8 @@ extern char *yyansi_ctext;
 
 #include "ansi_c_y.tab.h"
 
+#include <util/mathematical_expr.h>
+
 #ifdef _MSC_VER
 // possible loss of data
 #pragma warning(disable:4242)
@@ -468,7 +470,7 @@ quantifier_expression:
         {
           $$=$1;
           set($$, ID_forall);
-          mto($$, $4);
+          parser_stack($$).add_to_operands(tuple_exprt( { std::move(parser_stack($4)) } ));
           mto($$, $5);
           PARSER.pop_scope();
         }
@@ -478,15 +480,15 @@ quantifier_expression:
           // to bind only very weakly.
           $$=$1;
           set($$, ID_forall);
-          mto($$, $3);
+          parser_stack($$).add_to_operands(tuple_exprt( { std::move(parser_stack($3)) } ));
           mto($$, $4);
           PARSER.pop_scope();
         }
         | TOK_EXISTS compound_scope '{' declaration comma_expression '}'
         {
           $$=$1;
           set($$, ID_exists);
-          mto($$, $4);
+          parser_stack($$).add_to_operands(tuple_exprt( { std::move(parser_stack($4)) } ));
           mto($$, $5);
           PARSER.pop_scope();
         }
@@ -496,7 +498,7 @@ quantifier_expression:
           // to bind only very weakly.
           $$=$1;
           set($$, ID_exists);
-          mto($$, $3);
+          parser_stack($$).add_to_operands(tuple_exprt( { std::move(parser_stack($3)) } ));
           mto($$, $4);
           PARSER.pop_scope();
         }

src/util/mathematical_expr.h

@@ -315,35 +315,35 @@ class binding_exprt : public binary_exprt
 };
 
 /// \brief A base class for quantifier expressions
-class quantifier_exprt : public binary_predicate_exprt
+class quantifier_exprt : public binding_exprt
 {
 public:
-  quantifier_exprt(
-    const irep_idt &_id,
-    const symbol_exprt &_symbol,
-    const exprt &_where)
-    : binary_predicate_exprt(_symbol, _id, _where)
+  /// constructor for single variable
+  quantifier_exprt(irep_idt _id, symbol_exprt _symbol, exprt _where)
+    : binding_exprt(_id, {std::move(_symbol)}, std::move(_where), bool_typet())
   {
   }
 
-  symbol_exprt &symbol()
-  {
-    return static_cast<symbol_exprt &>(op0());
-  }
-
-  const symbol_exprt &symbol() const
+  /// constructor for multiple variables
+  quantifier_exprt(irep_idt _id, const variablest &_variables, exprt _where)
+    : binding_exprt(_id, _variables, std::move(_where), bool_typet())
   {
-    return static_cast<const symbol_exprt &>(op0());
   }
 
-  exprt &where()
+  // for the special case of one variable
+  symbol_exprt &symbol()
   {
-    return op1();
+    auto &variables = this->variables();
+    PRECONDITION(variables.size() == 1);
+    return variables.front();
   }
 
-  const exprt &where() const
+  // for the special case of one variable
+  const symbol_exprt &symbol() const
   {
-    return op1();
+    auto &variables = this->variables();
+    PRECONDITION(variables.size() == 1);
+    return variables.front();
   }
 };
 
@@ -356,8 +356,9 @@ inline bool can_cast_expr<quantifier_exprt>(const exprt &base)
 inline void validate_expr(const quantifier_exprt &value)
 {
   validate_operands(value, 2, "quantifier expressions must have two operands");
-  DATA_INVARIANT(
-    value.op0().id() == ID_symbol, "quantified variable shall be a symbol");
+  for(auto &op : value.variables())
+    DATA_INVARIANT(
+      op.id() == ID_symbol, "quantified variable shall be a symbol");
 }
 
 /// \brief Cast an exprt to a \ref quantifier_exprt