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

fix #3716 fix #3719

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-03 11:30:29 -07:00
parent 7fe46de266
commit 8e033c1e71
3 changed files with 32 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/smt_conflict_resolution.cpp
View file

@ -1335,6 +1335,7 @@ namespace smt {
else
m_lemma_proof = m.mk_lemma(pr, fact);
m_new_proofs.reset();
reset();
}
void conflict_resolution::process_antecedent_for_unsat_core(literal antecedent) {

2
src/smt/smt_context.cpp
View file

@ -2449,9 +2449,9 @@ namespace smt {
m_th_eq_propagation_queue.reset();
m_th_diseq_propagation_queue.reset();
m_atom_propagation_queue.reset();
m_region.pop_scope(num_scopes);
m_scopes.shrink(new_lvl);
m_conflict_resolution->reset();
m_scope_lvl = new_lvl;
if (new_lvl < m_base_lvl) {

46
src/tactic/bv/elim_small_bv_tactic.cpp
View file

@ -136,34 +136,48 @@ class elim_small_bv_tactic : public tactic {
unsigned max_var_idx_p1 = uv.get_max_found_var_idx_plus_1();
expr_ref body(old_body, m);
for (unsigned i = num_decls-1; i != ((unsigned)-1) && !max_steps_exceeded(num_steps); i--) {
for (unsigned i = num_decls; i-- > 0 && !max_steps_exceeded(num_steps); ) {
sort * s = q->get_decl_sort(i);
expr_ref_vector new_bodies(m);
if (is_small_bv(s) && !max_steps_exceeded(num_steps)) {
unsigned bv_sz = m_util.get_bv_size(s);
TRACE("elim_small_bv", tout << "eliminating " << q->get_decl_name(i) <<
"; sort = " << mk_ismt2_pp(s, m) <<
"; body = " << mk_ismt2_pp(body, m) << std::endl;);
expr_ref_vector new_bodies(m);
for (unsigned j = 0; j < bv_sz && !max_steps_exceeded(num_steps); j ++) {
if (bv_sz >= 31ul || ((unsigned)(1ul << bv_sz)) + num_steps > m_max_steps) {
return false;
}
for (unsigned j = 0; j < (1ul << bv_sz) && !max_steps_exceeded(num_steps); j++) {
expr_ref n(m_util.mk_numeral(j, bv_sz), m);
new_bodies.push_back(replace_var(uv, num_decls, max_var_idx_p1, i, s, body, n));
num_steps++;
}
TRACE("elim_small_bv", tout << "new bodies: " << std::endl;
for (unsigned k = 0; k < new_bodies.size(); k++)
tout << mk_ismt2_pp(new_bodies[k].get(), m) << std::endl; );
body = is_forall(q) ? m.mk_and(new_bodies.size(), new_bodies.c_ptr()) :
m.mk_or(new_bodies.size(), new_bodies.c_ptr());
SASSERT(is_well_sorted(m, body));
proof_ref pr(m);
m_simp(body, body, pr);
m_num_eliminated++;
}
else if (m.is_bool(s)) {
new_bodies.push_back(replace_var(uv, num_decls, max_var_idx_p1, i, s, body, m.mk_true()));
new_bodies.push_back(replace_var(uv, num_decls, max_var_idx_p1, i, s, body, m.mk_false()));
}
else {
continue;
}
if (max_steps_exceeded(num_steps)) {
return false;
}
TRACE("elim_small_bv", tout << "new bodies: " << std::endl;
for (unsigned k = 0; k < new_bodies.size(); k++)
tout << mk_ismt2_pp(new_bodies[k].get(), m) << std::endl; );
body = is_forall(q) ? m.mk_and(new_bodies.size(), new_bodies.c_ptr()) :
m.mk_or(new_bodies.size(), new_bodies.c_ptr());
SASSERT(is_well_sorted(m, body));
proof_ref pr(m);
m_simp(body, body, pr);
m_num_eliminated++;
}
quantifier_ref new_q(m);