mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix #3919

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-11 12:30:03 -07:00
parent ec0cd644f1
commit 6ca039c855
2 changed files with 22 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/ast/fpa/fpa2bv_rewriter.cpp
View file

@ -186,12 +186,13 @@ bool fpa2bv_rewriter_cfg::pre_visit(expr * t)
}
bool fpa2bv_rewriter_cfg::reduce_quantifier(quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
bool fpa2bv_rewriter_cfg::reduce_quantifier(
quantifier * old_q,
expr * new_body,
expr * const * new_patterns,
expr * const * new_no_patterns,
expr_ref & result,
proof_ref & result_pr) {
if (is_lambda(old_q)) {
return false;
}
@ -228,6 +229,9 @@ bool fpa2bv_rewriter_cfg::reduce_quantifier(quantifier * old_q,
new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(),
old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns);
result_pr = nullptr;
if (m().proofs_enabled()) {
result_pr = m().mk_rewrite(old_q, result);
}
m_bindings.shrink(old_sz);
TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " <<
mk_ismt2_pp(old_q->get_expr(), m()) << std::endl <<

30
src/tactic/fpa/fpa2bv_tactic.cpp
View file

@ -29,17 +29,10 @@ class fpa2bv_tactic : public tactic {
fpa2bv_rewriter m_rw;
unsigned m_num_steps;
bool m_proofs_enabled;
bool m_produce_models;
bool m_produce_unsat_cores;
imp(ast_manager & _m, params_ref const & p):
m(_m),
m_conv(m),
m_rw(m, m_conv, p),
m_proofs_enabled(false),
m_produce_models(false),
m_produce_unsat_cores(false) {
m_rw(m, m_conv, p) {
}
void updt_params(params_ref const & p) {
@ -48,15 +41,12 @@ class fpa2bv_tactic : public tactic {
void operator()(goal_ref const & g,
goal_ref_buffer & result) {
m_proofs_enabled = g->proofs_enabled();
m_produce_models = g->models_enabled();
m_produce_unsat_cores = g->unsat_core_enabled();
bool proofs_enabled = g->proofs_enabled();
result.reset();
tactic_report report("fpa2bv", *g);
m_rw.reset();
TRACE("fpa2bv", tout << "BEFORE: " << std::endl; g->display(tout););
TRACE("fpa2bv", g->display(tout << "BEFORE: " << std::endl););
if (g->inconsistent()) {
result.push_back(g.get());
@ -73,7 +63,7 @@ class fpa2bv_tactic : public tactic {
expr * curr = g->form(idx);
m_rw(curr, new_curr, new_pr);
m_num_steps += m_rw.get_num_steps();
if (m_proofs_enabled) {
if (proofs_enabled) {
proof * pr = g->pr(idx);
new_pr = m.mk_modus_ponens(pr, new_pr);
}
@ -101,11 +91,15 @@ class fpa2bv_tactic : public tactic {
g->inc_depth();
result.push_back(g.get());
for (unsigned i = 0; i < m_conv.m_extra_assertions.size(); i++)
result.back()->assert_expr(m_conv.m_extra_assertions[i].get());
for (expr* e : m_conv.m_extra_assertions) {
proof* pr = nullptr;
if (proofs_enabled)
pr = m.mk_asserted(e);
result.back()->assert_expr(e, pr);
}
TRACE("fpa2bv", tout << "AFTER: " << std::endl; g->display(tout);
if (g->mc()) g->mc()->display(tout); tout << std::endl; );
TRACE("fpa2bv", g->display(tout << "AFTER:\n");
if (g->mc()) g->mc()->display(tout); tout << std::endl; );
}
};