mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

#5324

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-04 09:40:31 -07:00
parent 7c86134e85
commit 73118012c5
1 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/sat/smt/q_solver.cpp
View file

@ -41,11 +41,19 @@ namespace q {
quantifier* q = to_quantifier(e); quantifier* q = to_quantifier(e);
auto const& exp = expand(q); auto const& exp = expand(q);
if (exp.size() > 1) { if (exp.size() > 1 && is_forall(q)) {
for (expr* e : exp) for (expr* e : exp)
add_clause(~l, ctx.internalize(e, l.sign(), false, false)); add_clause(~l, ctx.internalize(e, l.sign(), false, false));
return; return;
} }
if (exp.size() > 1 && is_exists(q)) {
sat::literal_vector lits;
lits.push_back(~l);
for (expr* e : exp)
lits.push_back(ctx.internalize(e, l.sign(), false, false));
add_clause(lits);
return;
}
if (l.sign() == is_forall(e)) if (l.sign() == is_forall(e))
add_clause(~l, skolemize(q)); add_clause(~l, skolemize(q));