mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
optimize model pruning
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
95fbf073f8
commit
16cfb3895d
|
@ -514,7 +514,7 @@ namespace pdr {
|
|||
|
||||
proof_ref pr(root, m);
|
||||
proof_utils::reduce_hypotheses(pr);
|
||||
IF_VERBOSE(2, verbose_stream() << "Elim Hyps:\n" << mk_ismt2_pp(pr, m) << "\n";);
|
||||
IF_VERBOSE(3, verbose_stream() << "Elim Hyps:\n" << mk_ismt2_pp(pr, m) << "\n";);
|
||||
proof_utils::permute_unit_resolution(pr);
|
||||
|
||||
ptr_vector<expr_set> hyprefs;
|
||||
|
|
|
@ -105,14 +105,14 @@ namespace pdr {
|
|||
lit = core[i].get();
|
||||
core[i] = m.mk_true();
|
||||
state = m.mk_not(n.pt().get_pdr_manager().mk_and(core));
|
||||
bool assumes_level = false;
|
||||
if (n.pt().is_invariant(n.level(), state, true, assumes_level, 0)) {
|
||||
bool uses_level_tmp = false;
|
||||
if (n.pt().is_invariant(n.level(), state, true, uses_level_tmp, 0)) {
|
||||
num_failures = 0;
|
||||
core[i] = core.back();
|
||||
core.pop_back();
|
||||
TRACE("pdr", tout << "Remove: " << mk_pp(lit, m) << "\n";);
|
||||
++num_changes;
|
||||
uses_level = assumes_level;
|
||||
uses_level = uses_level_tmp;
|
||||
}
|
||||
else {
|
||||
core[i] = lit;
|
||||
|
@ -120,6 +120,7 @@ namespace pdr {
|
|||
++i;
|
||||
}
|
||||
}
|
||||
IF_VERBOSE(1, verbose_stream() << "changes: " << num_changes << " size: " << core.size() << "\n";);
|
||||
TRACE("pdr", tout << "changes: " << num_changes << " index: " << i << " size: " << core.size() << "\n";);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue