add expansion for quantifiers over booleans

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

Author: kroening

regression/smt2_solver/quantifiers/boolean-quantifier.desc

@@ -3,5 +3,5 @@ boolean-quantifier.smt2
 
 ^EXIT=0$
 ^SIGNAL=0$
-^sat$
+^unsat$
 --

regression/smt2_solver/quantifiers/boolean-quantifier.smt2

@@ -1,13 +1,15 @@
-(assert (exists ((b Bool)) b))
-(assert (exists ((b Bool)) (not b)))
+(define-fun q1 () Bool (exists ((b Bool)) b))
+(define-fun q2 () Bool (exists ((b Bool)) (not b)))
 
-(assert (not (forall ((b Bool)) b)))
-(assert (not (forall ((b Bool)) (not b))))
+(define-fun q3 () Bool (not (forall ((b Bool)) b)))
+(define-fun q4 () Bool (not (forall ((b Bool)) (not b))))
 
-(assert (exists ((a Bool) (b Bool)) (= a b)))
-(assert (not (forall ((a Bool) (b Bool)) (= a b))))
+(define-fun q5 () Bool (exists ((a Bool) (b Bool)) (= a b)))
+(define-fun q6 () Bool (not (forall ((a Bool) (b Bool)) (= a b))))
 
-(assert (forall ((a Bool)) (exists ((b Bool)) (= a b))))
+(define-fun q7 () Bool (forall ((a Bool)) (exists ((b Bool)) (= a b))))
+
+; the above are all valid, and we assert one of them is not
+(assert (not (and q1 q2 q3 q4 q5 q6 q7)))
 
 (check-sat)
-(get-model)

src/solvers/flattening/boolbv_quantifier.cpp

@@ -168,29 +168,49 @@ 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(var_expr.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;
+  }
+
+  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;
 
   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)
+  if(lb > ub)
     return nullopt;
 
   std::vector<exprt> expr_insts;
-  for(mp_integer i=lb; i<=ub; ++i)
+  for(mp_integer i = lb; i <= ub; ++i)
   {
     exprt constraint_expr = re;
-    replace_expr(var_expr,
-                 from_integer(i, var_expr.type()),
-                 constraint_expr);
+    replace_expr(var_expr, from_integer(i, var_expr.type()), constraint_expr);
     expr_insts.push_back(constraint_expr);
   }
 
-  if(expr.id()==ID_forall)
+  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