mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

perform lookahead update + nested mul

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-24 13:25:48 -07:00
parent 29aca5b1d6
commit c643672e9f
1 changed files with 14 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/ast/sls/sls_arith_base.cpp
View file

@ -519,7 +519,7 @@ namespace sls {
num_t new_value = value(v) + delta; num_t new_value = value(v) + delta;
IF_VERBOSE(10, verbose_stream() << "repair: v" << v << " := " << value(v) << " -> " << new_value << "\n");
if (update(v, new_value)) { if (update(v, new_value)) {
m_last_delta = delta; m_last_delta = delta;
m_stats.m_num_steps++; m_stats.m_num_steps++;
@ -642,7 +642,7 @@ namespace sls {
#if 0 #if 1
if (!check_update(v, new_value)) if (!check_update(v, new_value))
return false; return false;
apply_checked_update(); apply_checked_update();
@ -660,6 +660,7 @@ namespace sls {
ctx.flip(bv); ctx.flip(bv);
SASSERT(dtt(sign(bv), ineq) == 0); SASSERT(dtt(sign(bv), ineq) == 0);
} }
IF_VERBOSE(5, verbose_stream() << "repair: v" << v << " := " << old_value << " -> " << new_value << "\n");
vi.m_value = new_value; vi.m_value = new_value;
ctx.new_value_eh(e); ctx.new_value_eh(e);
m_last_var = v; m_last_var = v;
@ -843,13 +844,14 @@ namespace sls {
add_args(term, y, -coeff); add_args(term, y, -coeff);
} }
else if (a.is_mul(e)) { else if (a.is_mul(e)) {
unsigned_vector m; unsigned_vector ms;
num_t c(1); num_t c(1);
ptr_buffer<expr> muls; ptr_buffer<expr> muls;
muls.append(to_app(e)->get_num_args(), to_app(e)->get_args()); muls.append(to_app(e)->get_num_args(), to_app(e)->get_args());
for (unsigned j = 0; j < muls.size(); ++j) { for (unsigned j = 0; j < muls.size(); ++j) {
expr* arg = muls[j]; expr* arg = muls[j];
if (a.is_mul(arg)) { if (a.is_mul(arg)) {
//verbose_stream() << "nested " << mk_bounded_pp(arg, m) << "\n";
muls.append(to_app(arg)->get_num_args(), to_app(arg)->get_args()); muls.append(to_app(arg)->get_num_args(), to_app(arg)->get_args());
muls[j] = muls.back(); muls[j] = muls.back();
muls.pop_back(); muls.pop_back();
@ -858,25 +860,25 @@ namespace sls {
else if (is_num(arg, i)) else if (is_num(arg, i))
c *= i; c *= i;
else else
m.push_back(mk_term(arg)); ms.push_back(mk_term(arg));
} }
switch (m.size()) { switch (ms.size()) {
case 0: case 0:
term.m_coeff += c*coeff; term.m_coeff += c*coeff;
break; break;
case 1: case 1:
add_arg(term, c*coeff, m[0]); add_arg(term, c*coeff, ms[0]);
break; break;
default: { default: {
v = mk_var(e); v = mk_var(e);
unsigned idx = m_muls.size(); unsigned idx = m_muls.size();
std::stable_sort(m.begin(), m.end(), [&](unsigned a, unsigned b) { return a < b; }); std::stable_sort(ms.begin(), ms.end(), [&](unsigned a, unsigned b) { return a < b; });
svector<std::pair<unsigned, unsigned>> mp; svector<std::pair<unsigned, unsigned>> mp;
for (unsigned i = 0; i < m.size(); ++i) { for (unsigned i = 0; i < ms.size(); ++i) {
auto w = m[i]; auto w = ms[i];
auto p = 1; auto p = 1;
while (i + 1 < m.size() && m[i + 1] == w) while (i + 1 < ms.size() && ms[i + 1] == w)
++p, ++i; ++p, ++i;
mp.push_back({ w, p }); mp.push_back({ w, p });
} }
@ -1519,9 +1521,10 @@ namespace sls {
num_t val = value(v); num_t val = value(v);
for (auto [v, p]: monomial) for (auto [v, p]: monomial)
product *= power_of(value(v), p); product *= power_of(value(v), p);
IF_VERBOSE(10, verbose_stream() << "v" << v << " repair mul " << mk_bounded_pp(m_vars[v].m_expr, m) << " : = " << val << "(product : " << product << ")\n");
if (product == val) if (product == val)
return true; return true;
IF_VERBOSE(10, verbose_stream() << "v" << v << " repair mul " << mk_bounded_pp(m_vars[v].m_expr, m) << " : = " << val << " (product : " << product << ")\n");
m_updates.reset(); m_updates.reset();
if (val == 0) { if (val == 0) {