mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 05:11:21 +00:00
Code Activity

#4923 - eq2bv

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-01-08 16:38:07 -08:00
parent 690bc51b7f
commit ffd57bef24
1 changed files with 28 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

58
src/tactic/arith/eq2bv_tactic.cpp
View file

@ -151,7 +151,7 @@ public:
expr_ref_vector m_trail; expr_ref_vector m_trail;
bound_manager m_bounds; bound_manager m_bounds;
obj_map<expr, expr*> m_fd; obj_map<expr, expr*> m_fd;
obj_map<expr, unsigned> m_max; obj_map<expr, rational> m_max;
expr_mark m_nonfd; expr_mark m_nonfd;
expr_mark m_has_eq; expr_mark m_has_eq;
ptr_vector<expr> m_todo; ptr_vector<expr> m_todo;
@ -278,32 +278,34 @@ public:
void cleanup_fd(ref<bvmc>& mc) { void cleanup_fd(ref<bvmc>& mc) {
SASSERT(m_fd.empty()); SASSERT(m_fd.empty());
ptr_vector<expr> rm; ptr_vector<expr> rm;
for (auto& kv : m_max)
if (m_nonfd.is_marked(kv.m_key))
rm.push_back(kv.m_key);
for (expr* r : rm)
m_max.erase(r);
for (auto& kv : m_max) { for (auto& kv : m_max) {
expr* key = kv.m_key;
rational& value = kv.m_value;
if (m_nonfd.is_marked(key)) {
rm.push_back(key);
continue;
}
// ensure there are enough elements. // ensure there are enough elements.
bool strict; bool strict;
rational val; rational bound;
if (m_bounds.has_upper(kv.m_key, val, strict)) {
SASSERT(!strict); if (m_bounds.has_upper(key, bound, strict))
if (val.get_unsigned() > kv.m_value) kv.m_value = val.get_unsigned(); value = std::max(value, bound);
} else
else { ++value;
++kv.m_value;
} if (m_bounds.has_lower(key, bound, strict))
if (m_bounds.has_lower(kv.m_key, val, strict)) { value = std::max(value, bound);
SASSERT(!strict);
if (val.get_unsigned() > kv.m_value) kv.m_value = val.get_unsigned(); ++value;
} }
unsigned p = next_power_of_two(kv.m_value); for (expr* r : rm)
m_max.erase(r);
for (auto& kv : m_max) {
unsigned p = kv.m_value.get_num_bits();
if (p <= 1) p = 2; if (p <= 1) p = 2;
if (kv.m_value == p) p *= 2; app* z = m.mk_fresh_const("z", bv.mk_sort(p));
unsigned n = log2(p);
SASSERT(p >= kv.m_value);
app* z = m.mk_fresh_const("z", bv.mk_sort(n));
m_trail.push_back(z); m_trail.push_back(z);
m_fd.insert(kv.m_key, z); m_fd.insert(kv.m_key, z);
mc->insert(z->get_decl(), to_app(kv.m_key)->get_decl()); mc->insert(z->get_decl(), to_app(kv.m_key)->get_decl());
@ -385,20 +387,16 @@ public:
} }
bool is_fd(expr* v, expr* c) { bool is_fd(expr* v, expr* c) {
unsigned val;
rational r; rational r;
if (is_uninterp_const(v) && a.is_numeral(c, r) && !m_nonfd.is_marked(v) && a.is_int(v) && r.is_unsigned()) { if (is_uninterp_const(v) && a.is_numeral(c, r) && !m_nonfd.is_marked(v) && a.is_int(v) && r.is_unsigned()) {
val = r.get_unsigned(); add_fd(v, r);
if (val > UINT_MAX/4)
return false;
add_fd(v, val);
return true; return true;
} }
return false; return false;
} }
void add_fd(expr* c, unsigned val) { void add_fd(expr* c, rational val) {
unsigned val2; rational val2;
if (!m_max.find(c, val2) || val2 < val) { if (!m_max.find(c, val2) || val2 < val) {
m_max.insert(c, val); m_max.insert(c, val);
} }