mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
filter fresh constants from models
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
601cb43f78
commit
4732e03259
|
@ -25,6 +25,7 @@ Notes:
|
|||
#include"bv_decl_plugin.h"
|
||||
#include"expr_replacer.h"
|
||||
#include"extension_model_converter.h"
|
||||
#include"filter_model_converter.h"
|
||||
#include"ast_smt2_pp.h"
|
||||
|
||||
class bv_size_reduction_tactic : public tactic {
|
||||
|
@ -60,6 +61,7 @@ struct bv_size_reduction_tactic::imp {
|
|||
obj_map<app, numeral> m_unsigned_lowers;
|
||||
obj_map<app, numeral> m_unsigned_uppers;
|
||||
ref<bv_size_reduction_mc> m_mc;
|
||||
ref<filter_model_converter> m_fmc;
|
||||
scoped_ptr<expr_replacer> m_replacer;
|
||||
bool m_produce_models;
|
||||
volatile bool m_cancel;
|
||||
|
@ -196,6 +198,7 @@ struct bv_size_reduction_tactic::imp {
|
|||
numeral u = m_util.norm(entry->get_data().m_value, bv_sz, true);
|
||||
TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << "\n";);
|
||||
expr * new_def = 0;
|
||||
app * new_const = 0;
|
||||
if (l > u) {
|
||||
g.assert_expr(m.mk_false());
|
||||
return;
|
||||
|
@ -208,15 +211,19 @@ struct bv_size_reduction_tactic::imp {
|
|||
if (l.is_neg()) {
|
||||
unsigned i_nb = (u - l).get_num_bits();
|
||||
unsigned v_nb = m_util.get_bv_size(v);
|
||||
if (i_nb < v_nb)
|
||||
new_def = m_util.mk_sign_extend(v_nb - i_nb, m.mk_fresh_const(0, m_util.mk_sort(i_nb)));
|
||||
if (i_nb < v_nb) {
|
||||
new_const = m.mk_fresh_const(0, m_util.mk_sort(i_nb));
|
||||
new_def = m_util.mk_sign_extend(v_nb - i_nb, new_const);
|
||||
}
|
||||
}
|
||||
else {
|
||||
// 0 <= l <= v <= u
|
||||
unsigned u_nb = u.get_num_bits();
|
||||
unsigned v_nb = m_util.get_bv_size(v);
|
||||
if (u_nb < v_nb)
|
||||
new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), m.mk_fresh_const(0, m_util.mk_sort(u_nb)));
|
||||
if (u_nb < v_nb) {
|
||||
new_const = m.mk_fresh_const(0, m_util.mk_sort(u_nb));
|
||||
new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -226,6 +233,10 @@ struct bv_size_reduction_tactic::imp {
|
|||
if (!m_mc)
|
||||
m_mc = alloc(bv_size_reduction_mc, m);
|
||||
m_mc->insert(v->get_decl(), new_def);
|
||||
if (!m_fmc && new_const)
|
||||
m_fmc = alloc(filter_model_converter, m);
|
||||
if (new_const)
|
||||
m_fmc->insert(new_const->get_decl());
|
||||
}
|
||||
num_reduced++;
|
||||
}
|
||||
|
@ -264,6 +275,7 @@ struct bv_size_reduction_tactic::imp {
|
|||
|
||||
TRACE("bv_size_reduction", tout << l << " <= " << v->get_decl()->get_name() << " <= " << u << "\n";);
|
||||
expr * new_def = 0;
|
||||
app * new_const = 0;
|
||||
if (l > u) {
|
||||
g.assert_expr(m.mk_false());
|
||||
return;
|
||||
|
@ -275,8 +287,10 @@ struct bv_size_reduction_tactic::imp {
|
|||
// 0 <= l <= v <= u
|
||||
unsigned u_nb = u.get_num_bits();
|
||||
unsigned v_nb = m_util.get_bv_size(v);
|
||||
if (u_nb < v_nb)
|
||||
new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), m.mk_fresh_const(0, m_util.mk_sort(u_nb)));
|
||||
if (u_nb < v_nb) {
|
||||
new_def = m_util.mk_concat(m_util.mk_numeral(numeral(0), v_nb - u_nb), new_const);
|
||||
new_const = m.mk_fresh_const(0, m_util.mk_sort(u_nb));
|
||||
}
|
||||
}
|
||||
|
||||
if (new_def) {
|
||||
|
@ -285,6 +299,10 @@ struct bv_size_reduction_tactic::imp {
|
|||
if (!m_mc)
|
||||
m_mc = alloc(bv_size_reduction_mc, m);
|
||||
m_mc->insert(v->get_decl(), new_def);
|
||||
if (!m_fmc && new_const)
|
||||
m_fmc = alloc(filter_model_converter, m);
|
||||
if (new_const)
|
||||
m_fmc->insert(new_const->get_decl());
|
||||
}
|
||||
num_reduced++;
|
||||
TRACE("bv_size_reduction", tout << "New definition = " << mk_ismt2_pp(new_def, m) << "\n";);
|
||||
|
@ -309,7 +327,11 @@ struct bv_size_reduction_tactic::imp {
|
|||
g.update(i, new_f);
|
||||
}
|
||||
mc = m_mc.get();
|
||||
if (m_fmc) {
|
||||
mc = concat(m_fmc.get(), mc.get());
|
||||
}
|
||||
m_mc = 0;
|
||||
m_fmc = 0;
|
||||
}
|
||||
report_tactic_progress(":bv-reduced", num_reduced);
|
||||
TRACE("after_bv_size_reduction", g.display(tout); if (m_mc) m_mc->display(tout););
|
||||
|
|
Loading…
Reference in a new issue