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

reset model converter between rounds to elim-unconstrained.

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-18 15:16:04 -08:00
parent 0daa05aab2
commit 13be3c3fbb
3 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/converters/generic_model_converter.h
View file

@ -68,6 +68,8 @@ public:
void get_units(obj_map<expr, bool>& units) override; void get_units(obj_map<expr, bool>& units) override;
vector<entry> const& entries() const { return m_entries; } vector<entry> const& entries() const { return m_entries; }
void reset() { m_entries.reset(); }
}; };
typedef ref<generic_model_converter> generic_model_converter_ref; typedef ref<generic_model_converter> generic_model_converter_ref;

1
src/ast/rewriter/bv_rewriter.cpp
View file

@ -555,7 +555,6 @@ br_status bv_rewriter::mk_leq_core(bool is_signed, expr * a, expr * b, expr_ref
result = m.mk_and(result, m_util.mk_ule(m_util.mk_numeral(r1-r2, sz), a2)); result = m.mk_and(result, m_util.mk_ule(m_util.mk_numeral(r1-r2, sz), a2));
else if (r1 < r2) else if (r1 < r2)
result = m.mk_or(result, m_util.mk_ule(m_util.mk_numeral(r1-r2, sz), a2)); result = m.mk_or(result, m_util.mk_ule(m_util.mk_numeral(r1-r2, sz), a2));
verbose_stream() << result << "\n";
return BR_REWRITE2; return BR_REWRITE2;
} }

3
src/ast/simplifiers/elim_unconstrained.cpp
View file

@ -426,7 +426,7 @@ void elim_unconstrained::reduce() {
generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained"); generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained");
m_inverter.set_model_converter(mc.get()); m_inverter.set_model_converter(mc.get());
m_created_compound = true; m_created_compound = true;
for (unsigned rounds = 0; m_created_compound && rounds < 1; ++rounds) { for (unsigned rounds = 0; m_created_compound && rounds < 3; ++rounds) {
m_created_compound = false; m_created_compound = false;
init_nodes(); init_nodes();
eliminate(); eliminate();
@ -434,6 +434,7 @@ void elim_unconstrained::reduce() {
vector<dependent_expr> old_fmls; vector<dependent_expr> old_fmls;
assert_normalized(old_fmls); assert_normalized(old_fmls);
update_model_trail(*mc, old_fmls); update_model_trail(*mc, old_fmls);
mc->reset();
} }
} }