Skip to content

Commit 782beb8

Browse files
committed
don't fail on quantifiers with more than one symbol
This adds support for eager instantiation of forall or exists quantifier expressions that have more than one symbol using the trivial rewrite.
1 parent 5828e70 commit 782beb8

File tree

3 files changed

+32
-0
lines changed

3 files changed

+32
-0
lines changed
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
boolean-quantifier.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^sat$
7+
--
Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
(assert (exists ((b Bool)) b))
2+
(assert (exists ((b Bool)) (not b)))
3+
4+
(assert (not (forall ((b Bool)) b)))
5+
(assert (not (forall ((b Bool)) (not b))))
6+
7+
(assert (exists ((a Bool) (b Bool)) (= a b)))
8+
(assert (not (forall ((a Bool) (b Bool)) (= a b))))
9+
10+
(assert (forall ((a Bool)) (exists ((b Bool)) (= a b))))
11+
12+
(check-sat)
13+
(get-model)

src/solvers/flattening/boolbv_quantifier.cpp

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -142,6 +142,18 @@ static optionalt<exprt> eager_quantifier_instantiation(
142142
const quantifier_exprt &expr,
143143
const namespacet &ns)
144144
{
145+
if(expr.variables().size() > 1)
146+
{
147+
// Qx,y.P(x,y) is the same as Qx.Qy.P(x,y)
148+
auto new_variables = expr.variables();
149+
new_variables.pop_back();
150+
auto new_expression = quantifier_exprt(
151+
expr.id(),
152+
expr.variables().back(),
153+
quantifier_exprt(expr.id(), new_variables, expr.where()));
154+
return eager_quantifier_instantiation(new_expression, ns);
155+
}
156+
145157
const symbol_exprt &var_expr = expr.symbol();
146158

147159
/**

0 commit comments

Comments
 (0)