mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
This commit is contained in:
parent
614cb26489
commit
134562162a
|
@ -40,34 +40,25 @@ namespace q {
|
|||
return;
|
||||
quantifier* q = to_quantifier(e);
|
||||
|
||||
auto const& exp = expand(q);
|
||||
if (exp.size() > 1 && is_forall(q) && !l.sign()) {
|
||||
for (expr* e : exp) {
|
||||
sat::literal lit = ctx.internalize(e, l.sign(), false, false);
|
||||
add_clause(~l, lit);
|
||||
ctx.add_aux(~l, lit);
|
||||
}
|
||||
return;
|
||||
}
|
||||
if (exp.size() > 1 && is_exists(q) && l.sign()) {
|
||||
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);
|
||||
ctx.add_aux(lits);
|
||||
return;
|
||||
}
|
||||
|
||||
if (l.sign() == is_forall(e)) {
|
||||
sat::literal lit = skolemize(q);
|
||||
add_clause(~l, lit);
|
||||
ctx.add_root(~l, lit);
|
||||
}
|
||||
else {
|
||||
ctx.push_vec(m_universal, l);
|
||||
if (ctx.get_config().m_ematching)
|
||||
m_ematch.add(q);
|
||||
auto const& exp = expand(q);
|
||||
if (exp.size() > 1) {
|
||||
for (expr* e : exp) {
|
||||
sat::literal lit = ctx.internalize(e, l.sign(), false, false);
|
||||
add_clause(~l, lit);
|
||||
ctx.add_aux(~l, lit);
|
||||
}
|
||||
}
|
||||
else {
|
||||
ctx.push_vec(m_universal, l);
|
||||
if (ctx.get_config().m_ematching)
|
||||
m_ematch.add(q);
|
||||
}
|
||||
}
|
||||
m_stats.m_num_quantifier_asserts++;
|
||||
}
|
||||
|
@ -146,9 +137,9 @@ namespace q {
|
|||
}
|
||||
|
||||
/*
|
||||
* Find initial values to instantiate quantifier with so to make it as hard as possible for solver
|
||||
* to find values to free variables.
|
||||
*/
|
||||
* Find initial values to instantiate quantifier with so to make it as hard as possible for solver
|
||||
* to find values to free variables.
|
||||
*/
|
||||
sat::literal solver::specialize(quantifier* q) {
|
||||
std::function<expr* (quantifier*, unsigned)> mk_var = [&](quantifier* q, unsigned i) {
|
||||
return get_unit(q->get_decl_sort(i));
|
||||
|
@ -243,46 +234,11 @@ namespace q {
|
|||
ctx.get_rewriter()(tmp);
|
||||
m_expanded[i] = tmp;
|
||||
}
|
||||
return m_expanded;
|
||||
}
|
||||
|
||||
#if 0
|
||||
m_expanded.reset();
|
||||
m_expanded2.reset();
|
||||
if (is_forall(q))
|
||||
flatten_or(q->get_expr(), m_expanded2);
|
||||
else if (is_exists(q))
|
||||
flatten_and(q->get_expr(), m_expanded2);
|
||||
else
|
||||
UNREACHABLE();
|
||||
for (unsigned i = m_expanded2.size(); i-- > 0; ) {
|
||||
expr* lit = m_expanded2.get(i);
|
||||
if (!is_ground(lit) && is_and(lit) && is_forall(q)) {
|
||||
|
||||
// get free vars of lit
|
||||
// create fresh predicate over free vars
|
||||
// replace in expanded, pack and push on m_expanded
|
||||
|
||||
expr_ref p(m);
|
||||
// TODO introduce fresh p.
|
||||
flatten_and(lit, m_expanded);
|
||||
for (unsigned i = m_expanded.size(); i-- > 0; ) {
|
||||
tmp = m.mk_or(m.mk_not(p), m_expanded.get(i));
|
||||
expr_ref tmp(m.update_quantifier(q, tmp), m);
|
||||
ctx.get_rewriter()(tmp);
|
||||
m_expanded[i] = tmp;
|
||||
}
|
||||
m_expanded2[i] = p;
|
||||
tmp = m.mk_or(m_expanded2);
|
||||
expr_ref tmp(m.update_quantifier(q, tmp), m);
|
||||
ctx.get_rewriter()(tmp);
|
||||
m_expanded.push_back(tmp);
|
||||
return m_expanded;
|
||||
}
|
||||
else {
|
||||
m_expanded.reset();
|
||||
m_expanded.push_back(q);
|
||||
}
|
||||
#endif
|
||||
m_expanded.reset();
|
||||
m_expanded.push_back(q);
|
||||
return m_expanded;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue