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,30 +292,35 @@ 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
-    assert(expr.operands().size()==2);
-    expr.type()=bool_typet();
+    // These have two operands.
+    // op0 is a tuple with one declaration,
+    // op1 is the bound expression
+    auto &binary_expr = to_binary_expr(expr);
+    auto &binding = binary_expr.op0().operands();
+    auto &where = binary_expr.op1();
+
+    DATA_INVARIANT(binding.size() == 1, "we expect one declaration in forall/exists");
 
-    if(expr.op0().get(ID_statement)!=ID_decl)
+    if(binding.front().get(ID_statement) != ID_decl)
     {
       error().source_location = expr.source_location();
       error() << "expected declaration as operand of quantifier" << eom;
       throw 0;
     }
 
-    if(has_subexpr(expr.op1(), ID_side_effect))
+    if(has_subexpr(where, ID_side_effect))
     {
       error().source_location = expr.source_location();
       error() << "quantifier must not contain side effects" << eom;
       throw 0;
     }
 
-    // replace declaration by symbol expression
-    symbol_exprt bound=to_symbol_expr(expr.op0().op0());
-    expr.op0().swap(bound);
+    expr.type() = bool_typet();
 
-    implicit_typecast_bool(expr.op1());
+    // replace declarations by symbol expressions
+    binding.front() = to_code_decl(to_code(binding.front())).symbol();
+
+    implicit_typecast_bool(binary_expr.op1());
   }
   else if(expr.id()==ID_label)
   {
@@ -738,10 +743,16 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr)
   }
   else if(expr.id()==ID_forall || expr.id()==ID_exists)
   {
-    assert(expr.operands().size()==2);
+    // These introduce new symbols, which need to be added to the symbol table
+    // before the second operand is typechecked.
+
+    DATA_INVARIANT(expr.operands().size() == 2, "forall/exists are binary");
+    DATA_INVARIANT(
+      to_binary_expr(expr).op0().operands().size() == 1,
+      "forall/exists have one declaration as first operand");
 
-    ansi_c_declarationt &declaration=
-      to_ansi_c_declaration(expr.op0());
+    ansi_c_declarationt &declaration =
+      to_ansi_c_declaration(to_binary_expr(expr).op0().op0());
 
     typecheck_declaration(declaration);
 
@@ -762,7 +773,7 @@ void c_typecheck_baset::typecheck_expr_operands(exprt &expr)
     if(s_it==symbol_table.symbols.end())
     {
       error().source_location = expr.source_location();
-      error() << "failed to find decl symbol '" << identifier
+      error() << "failed to find bound symbol `" << identifier
               << "' in symbol table" << eom;
       throw 0;
     }
@@ -780,7 +791,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,15 +470,15 @@ 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();
         }
         | 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();
         }
@@ -806,15 +808,15 @@ ACSL_binding_expression:
         {
           $$=$1;
           set($$, ID_forall);
-          mto($$, $3);
+          parser_stack($$).add_to_operands(tuple_exprt( { std::move(parser_stack($3)) } ));
           mto($$, $4);
           PARSER.pop_scope();
         }
         | TOK_ACSL_EXISTS compound_scope declaration ACSL_binding_expression
         {
           $$=$1;
           set($$, ID_exists);
-          mto($$, $3);
+          parser_stack($$).add_to_operands(tuple_exprt( { std::move(parser_stack($3)) } ));
           mto($$, $4);
           PARSER.pop_scope();
         }

src/solvers/smt2/smt2_conv.cpp

@@ -1807,7 +1807,7 @@ void smt2_convt::convert_expr(const exprt &expr)
     else if(quantifier_expr.id() == ID_exists)
       out << "(exists ";
 
-    exprt bound=expr.op0();
+    exprt bound=quantifier_expr.symbol();
 
     out << "((";
     convert_expr(bound);

src/solvers/smt2/smt2_parser.cpp

@@ -283,7 +283,7 @@ exprt smt2_parsert::quantifier_expression(irep_idt id)
   // go backwards, build quantified expression
   for(auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++)
   {
-    binary_predicate_exprt quantifier(*r_it, id, result);
+    quantifier_exprt quantifier(id, *r_it, result);
     result=quantifier;
   }
 

src/util/mathematical_expr.h

@@ -313,35 +313,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)
-  {
-  }
-
-  symbol_exprt &symbol()
+  /// 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())
   {
-    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();
   }
 };
 
@@ -354,8 +354,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