add expansion for quantifiers over booleans

This adds support for eager instantiation of quantifiers over booleans,
using George Boole's Proposition II.

Author: kroening

src/solvers/flattening/boolbv_quantifier.cpp

@@ -169,58 +169,80 @@ static optionalt<exprt> eager_quantifier_instantiation(
     return re;
   }
 
-  const optionalt<constant_exprt> min_i = get_quantifier_var_min(var_expr, re);
-  const optionalt<constant_exprt> max_i = get_quantifier_var_max(var_expr, re);
+  if(re.is_boolean())
+  {
+    // Expand in full.
+    // This grows worst-case exponentially in the quantifier nesting depth.
+    if(expr.id() == ID_forall)
+    {
+      // ∀b.f(b) <===> f(0)∧f(1)
+      return and_exprt(
+        expr.instantiate({false_exprt()}), expr.instantiate({true_exprt()}));
+    }
+    else if(expr.id() == ID_exists)
+    {
+      // ∃b.f(b) <===> f(0)∨f(1)
+      return or_exprt(
+        expr.instantiate({false_exprt()}), expr.instantiate({true_exprt()}));
+    }
+    else
+      UNREACHABLE;
+  }
+  else
+  {
+    const optionalt<constant_exprt> min_i =
+      get_quantifier_var_min(var_expr, re);
+    const optionalt<constant_exprt> max_i =
+      get_quantifier_var_max(var_expr, re);
 
-  if(!min_i.has_value() || !max_i.has_value())
-    return nullopt;
+    if(!min_i.has_value() || !max_i.has_value())
+      return nullopt;
 
-  mp_integer lb = numeric_cast_v<mp_integer>(min_i.value());
-  mp_integer ub = numeric_cast_v<mp_integer>(max_i.value());
+    mp_integer lb = numeric_cast_v<mp_integer>(min_i.value());
+    mp_integer ub = numeric_cast_v<mp_integer>(max_i.value());
 
-  if(lb>ub)
-    return nullopt;
+    if(lb > ub)
+      return nullopt;
 
-  std::vector<exprt> expr_insts;
-  for(mp_integer i=lb; i<=ub; ++i)
-  {
-    exprt constraint_expr = re;
-    replace_expr(var_expr,
-                 from_integer(i, var_expr.type()),
-                 constraint_expr);
-    expr_insts.push_back(constraint_expr);
-  }
+    std::vector<exprt> expr_insts;
+    for(mp_integer i = lb; i <= ub; ++i)
+    {
+      exprt constraint_expr = re;
+      replace_expr(var_expr, from_integer(i, var_expr.type()), constraint_expr);
+      expr_insts.push_back(constraint_expr);
+    }
 
-  if(expr.id()==ID_forall)
-  {
-    // maintain the domain constraint if it isn't guaranteed by the
-    // instantiations (for a disjunction the domain constraint is implied by the
-    // instantiations)
-    if(re.id() == ID_and)
+    if(expr.id() == ID_forall)
     {
-      expr_insts.push_back(binary_predicate_exprt(
-        var_expr, ID_gt, from_integer(lb, var_expr.type())));
-      expr_insts.push_back(binary_predicate_exprt(
-        var_expr, ID_le, from_integer(ub, var_expr.type())));
+      // maintain the domain constraint if it isn't guaranteed by the
+      // instantiations (for a disjunction the domain constraint is implied by the
+      // instantiations)
+      if(re.id() == ID_and)
+      {
+        expr_insts.push_back(binary_predicate_exprt(
+          var_expr, ID_gt, from_integer(lb, var_expr.type())));
+        expr_insts.push_back(binary_predicate_exprt(
+          var_expr, ID_le, from_integer(ub, var_expr.type())));
+      }
+      return simplify_expr(conjunction(expr_insts), ns);
     }
-    return simplify_expr(conjunction(expr_insts), ns);
-  }
-  else if(expr.id() == ID_exists)
-  {
-    // maintain the domain constraint if it isn't trivially satisfied by the
-    // instantiations (for a conjunction the instantiations are stronger
-    // constraints)
-    if(re.id() == ID_or)
+    else if(expr.id() == ID_exists)
     {
-      expr_insts.push_back(binary_predicate_exprt(
-        var_expr, ID_gt, from_integer(lb, var_expr.type())));
-      expr_insts.push_back(binary_predicate_exprt(
-        var_expr, ID_le, from_integer(ub, var_expr.type())));
+      // maintain the domain constraint if it isn't trivially satisfied by the
+      // instantiations (for a conjunction the instantiations are stronger
+      // constraints)
+      if(re.id() == ID_or)
+      {
+        expr_insts.push_back(binary_predicate_exprt(
+          var_expr, ID_gt, from_integer(lb, var_expr.type())));
+        expr_insts.push_back(binary_predicate_exprt(
+          var_expr, ID_le, from_integer(ub, var_expr.type())));
+      }
+      return simplify_expr(disjunction(expr_insts), ns);
     }
-    return simplify_expr(disjunction(expr_insts), ns);
-  }
 
-  UNREACHABLE;
+    UNREACHABLE;
+  }
 }
 
 literalt boolbvt::convert_quantifier(const quantifier_exprt &src)