mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
parent
f56749a241
commit
82a89120b0
|
@ -594,7 +594,6 @@ bool pattern_inference_cfg::reduce_quantifier(
|
|||
unsigned new_weight;
|
||||
if (m_database.match_quantifier(q, new_patterns, new_weight)) {
|
||||
DEBUG_CODE(for (unsigned i = 0; i < new_patterns.size(); i++) { SASSERT(is_well_sorted(m, new_patterns.get(i))); });
|
||||
quantifier_ref new_q(m);
|
||||
if (q->get_num_patterns() > 0) {
|
||||
// just update the weight...
|
||||
TRACE("pattern_inference", tout << "updating weight to: " << new_weight << "\n" << mk_pp(q, m) << "\n";);
|
||||
|
@ -604,10 +603,10 @@ bool pattern_inference_cfg::reduce_quantifier(
|
|||
quantifier_ref tmp(m);
|
||||
tmp = m.update_quantifier(q, new_patterns.size(), (expr**) new_patterns.c_ptr(), q->get_expr());
|
||||
result = m.update_quantifier_weight(tmp, new_weight);
|
||||
TRACE("pattern_inference", tout << "found patterns in database, weight: " << new_weight << "\n" << mk_pp(new_q, m) << "\n";);
|
||||
TRACE("pattern_inference", tout << "found patterns in database, weight: " << new_weight << "\n" << mk_pp(result, m) << "\n";);
|
||||
}
|
||||
if (m.proofs_enabled())
|
||||
result_pr = m.mk_rewrite(q, new_q);
|
||||
result_pr = m.mk_rewrite(q, result);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue