mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 16:38:45 +00:00
Code Activity

fix #3423

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-23 10:27:42 -07:00
parent f158ab8395
commit 84090aaf24
4 changed files with 18 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/dyn_ack.cpp
View file

@ -355,7 +355,6 @@ namespace smt {
void dyn_ack_manager::del_clause_eh(clause * cls) { void dyn_ack_manager::del_clause_eh(clause * cls) {
m_context.m_stats.m_num_del_dyn_ack++; m_context.m_stats.m_num_del_dyn_ack++;
app_pair p((app*)nullptr,(app*)nullptr); app_pair p((app*)nullptr,(app*)nullptr);
if (m_clause2app_pair.find(cls, p)) { if (m_clause2app_pair.find(cls, p)) {
SASSERT(p.first && p.second); SASSERT(p.first && p.second);

4
src/smt/smt_context.cpp
View file

@ -2928,12 +2928,12 @@ namespace smt {
m_model_generator->reset(); m_model_generator->reset();
for (theory* t : m_theory_set) for (theory* t : m_theory_set)
t->flush_eh(); t->flush_eh();
undo_trail_stack(0);
m_qmanager = nullptr;
del_clauses(m_aux_clauses, 0); del_clauses(m_aux_clauses, 0);
del_clauses(m_lemmas, 0); del_clauses(m_lemmas, 0);
del_justifications(m_justifications, 0); del_justifications(m_justifications, 0);
reset_tmp_clauses(); reset_tmp_clauses();
undo_trail_stack(0);
m_qmanager = nullptr;
if (m_is_diseq_tmp) { if (m_is_diseq_tmp) {
m_is_diseq_tmp->del_eh(m, false); m_is_diseq_tmp->del_eh(m, false);
m.dec_ref(m_is_diseq_tmp->get_owner()); m.dec_ref(m_is_diseq_tmp->get_owner());

22
src/tactic/arith/purify_arith_tactic.cpp
View file

@ -258,7 +258,7 @@ struct purify_arith_proc {
} }
void push_cnstr_pr(proof * def_pr) { void push_cnstr_pr(proof * def_pr) {
if (produce_proofs()) if (produce_proofs())
m_new_cnstr_prs.push_back(m().mk_th_lemma(u().get_family_id(), m_new_cnstrs.back(), 1, &def_pr)); m_new_cnstr_prs.push_back(m().mk_th_lemma(u().get_family_id(), m_new_cnstrs.back(), 1, &def_pr));
} }
@ -725,15 +725,15 @@ struct purify_arith_proc {
r(q->get_expr(), new_body, new_body_pr); r(q->get_expr(), new_body, new_body_pr);
unsigned num_vars = r.cfg().m_new_vars.size(); unsigned num_vars = r.cfg().m_new_vars.size();
expr_ref_vector & cnstrs = r.cfg().m_new_cnstrs; expr_ref_vector & cnstrs = r.cfg().m_new_cnstrs;
cnstrs.push_back(new_body); if (true || !cnstrs.empty()) {
new_body = m().mk_and(cnstrs.size(), cnstrs.c_ptr()); cnstrs.push_back(new_body);
new_body = m().mk_and(cnstrs.size(), cnstrs.c_ptr());
}
TRACE("purify_arith", TRACE("purify_arith",
tout << "num_vars: " << num_vars << "\n"; tout << "num_vars: " << num_vars << "\n";
tout << "body: " << mk_ismt2_pp(q->get_expr(), m()) << "\nnew_body: " << mk_ismt2_pp(new_body, m()) << "\n";); tout << "body: " << mk_ismt2_pp(q->get_expr(), m()) << "\nnew_body: " << mk_ismt2_pp(new_body, m()) << "\n";);
if (num_vars == 0) { if (num_vars == 0) {
result = m().update_quantifier(q, new_body); result = m().update_quantifier(q, new_body);
if (m_produce_proofs)
result_pr = m().mk_quant_intro(q, to_quantifier(result.get()), result_pr);
} }
else { else {
// Add new constraints // Add new constraints
@ -757,11 +757,12 @@ struct purify_arith_proc {
(*replacer)(new_body, new_body); (*replacer)(new_body, new_body);
new_body = m().mk_exists(num_vars, sorts.c_ptr(), names.c_ptr(), new_body, q->get_weight()); new_body = m().mk_exists(num_vars, sorts.c_ptr(), names.c_ptr(), new_body, q->get_weight());
result = m().update_quantifier(q, new_body); result = m().update_quantifier(q, new_body);
if (m_produce_proofs) { }
auto& cnstr_prs = r.cfg().m_new_cnstr_prs; if (m_produce_proofs) {
result_pr = m().mk_quant_intro(q, to_quantifier(result.get()), m().mk_rewrite_star(q->get_expr(), new_body, cnstr_prs.size(), cnstr_prs.c_ptr())); auto& cnstr_prs = r.cfg().m_new_cnstr_prs;
r.cfg().push_cnstr_pr(result_pr); result_pr = m().mk_rewrite_star(q->get_expr(), new_body, cnstr_prs.size(), cnstr_prs.c_ptr());
} result_pr = m().mk_quant_intro(q, to_quantifier(result.get()), result_pr);
r.cfg().push_cnstr_pr(result_pr);
} }
} }
@ -784,6 +785,7 @@ struct purify_arith_proc {
// add cnstraints // add cnstraints
sz = r.cfg().m_new_cnstrs.size(); sz = r.cfg().m_new_cnstrs.size();
TRACE("purify_arith", tout << r.cfg().m_new_cnstrs << "\n";); TRACE("purify_arith", tout << r.cfg().m_new_cnstrs << "\n";);
TRACE("purify_arith", tout << r.cfg().m_new_cnstr_prs << "\n";);
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
m_goal.assert_expr(r.cfg().m_new_cnstrs.get(i), m_produce_proofs ? r.cfg().m_new_cnstr_prs.get(i) : nullptr, nullptr); m_goal.assert_expr(r.cfg().m_new_cnstrs.get(i), m_produce_proofs ? r.cfg().m_new_cnstr_prs.get(i) : nullptr, nullptr);
} }

6
src/tactic/goal.cpp
View file

@ -591,9 +591,11 @@ bool goal::is_well_formed() const {
if (!::is_well_sorted(m(), t)) if (!::is_well_sorted(m(), t))
return false; return false;
#if 0 #if 0
SASSERT(m().get_fact(pr(i)) == form(i)); if (m().get_fact(pr(i)) != form(i)) {
if (m().get_fact(pr(i)) != form(i)) TRACE("tactic", tout << mk_ismt2_pp(pr(i), m()) << "\n" << mk_ismt2_pp(form(i), m()) << "\n";);
SASSERT(m().get_fact(pr(i)) == form(i));
return false; return false;
}
#endif #endif
} }
return true; return true;