Skip to content

Commit fb6b286

Browse files
committed
add expansion for quantifiers over booleans
This adds support for eager instantiation of quantifiers over booleans, using George Boole's Proposition II.
1 parent 782beb8 commit fb6b286

File tree

3 files changed

+39
-17
lines changed

3 files changed

+39
-17
lines changed

regression/smt2_solver/quantifiers/boolean-quantifier.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,5 +3,5 @@ boolean-quantifier.smt2
33

44
^EXIT=0$
55
^SIGNAL=0$
6-
^sat$
6+
^unsat$
77
--

regression/smt2_solver/quantifiers/boolean-quantifier.smt2

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,15 @@
1-
(assert (exists ((b Bool)) b))
2-
(assert (exists ((b Bool)) (not b)))
1+
(define-fun q1 () Bool (exists ((b Bool)) b))
2+
(define-fun q2 () Bool (exists ((b Bool)) (not b)))
33

4-
(assert (not (forall ((b Bool)) b)))
5-
(assert (not (forall ((b Bool)) (not b))))
4+
(define-fun q3 () Bool (not (forall ((b Bool)) b)))
5+
(define-fun q4 () Bool (not (forall ((b Bool)) (not b))))
66

7-
(assert (exists ((a Bool) (b Bool)) (= a b)))
8-
(assert (not (forall ((a Bool) (b Bool)) (= a b))))
7+
(define-fun q5 () Bool (exists ((a Bool) (b Bool)) (= a b)))
8+
(define-fun q6 () Bool (not (forall ((a Bool) (b Bool)) (= a b))))
99

10-
(assert (forall ((a Bool)) (exists ((b Bool)) (= a b))))
10+
(define-fun q7 () Bool (forall ((a Bool)) (exists ((b Bool)) (= a b))))
11+
12+
; the above are all valid, and we assert one of them is not
13+
(assert (not (and q1 q2 q3 q4 q5 q6 q7)))
1114

1215
(check-sat)
13-
(get-model)

src/solvers/flattening/boolbv_quantifier.cpp

Lines changed: 28 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -168,29 +168,49 @@ static optionalt<exprt> eager_quantifier_instantiation(
168168
return re;
169169
}
170170

171-
const optionalt<constant_exprt> min_i = get_quantifier_var_min(var_expr, re);
172-
const optionalt<constant_exprt> max_i = get_quantifier_var_max(var_expr, re);
171+
if(var_expr.is_boolean())
172+
{
173+
// Expand in full.
174+
// This grows worst-case exponentially in the quantifier nesting depth.
175+
if(expr.id() == ID_forall)
176+
{
177+
// ∀b.f(b) <===> f(0)∧f(1)
178+
return and_exprt(
179+
expr.instantiate({false_exprt()}), expr.instantiate({true_exprt()}));
180+
}
181+
else if(expr.id() == ID_exists)
182+
{
183+
// ∃b.f(b) <===> f(0)∨f(1)
184+
return or_exprt(
185+
expr.instantiate({false_exprt()}), expr.instantiate({true_exprt()}));
186+
}
187+
else
188+
UNREACHABLE;
189+
}
190+
191+
const optionalt<constant_exprt> min_i =
192+
get_quantifier_var_min(var_expr, re);
193+
const optionalt<constant_exprt> max_i =
194+
get_quantifier_var_max(var_expr, re);
173195

174196
if(!min_i.has_value() || !max_i.has_value())
175197
return nullopt;
176198

177199
mp_integer lb = numeric_cast_v<mp_integer>(min_i.value());
178200
mp_integer ub = numeric_cast_v<mp_integer>(max_i.value());
179201

180-
if(lb>ub)
202+
if(lb > ub)
181203
return nullopt;
182204

183205
std::vector<exprt> expr_insts;
184-
for(mp_integer i=lb; i<=ub; ++i)
206+
for(mp_integer i = lb; i <= ub; ++i)
185207
{
186208
exprt constraint_expr = re;
187-
replace_expr(var_expr,
188-
from_integer(i, var_expr.type()),
189-
constraint_expr);
209+
replace_expr(var_expr, from_integer(i, var_expr.type()), constraint_expr);
190210
expr_insts.push_back(constraint_expr);
191211
}
192212

193-
if(expr.id()==ID_forall)
213+
if(expr.id() == ID_forall)
194214
{
195215
// maintain the domain constraint if it isn't guaranteed by the
196216
// instantiations (for a disjunction the domain constraint is implied by the

0 commit comments

Comments
 (0)