mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-01 00:43:18 +00:00
Code Activity

na

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-07-05 19:43:31 -07:00
parent 3e57a9ce1e
commit 52533130f9
2 changed files with 42 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

77
src/ast/sls/sls_arith_int.cpp
View file

@ -330,7 +330,6 @@ namespace sls {
vi.m_value = new_value; vi.m_value = new_value;
for (auto idx : vi.m_muls) { for (auto idx : vi.m_muls) {
auto const& [v, monomial] = m_muls[idx]; auto const& [v, monomial] = m_muls[idx];
num_t prod(1); num_t prod(1);
for (auto w : monomial) for (auto w : monomial)
prod *= value(w); prod *= value(w);
@ -348,7 +347,7 @@ namespace sls {
m_vars_to_update.push_back({ v, sum }); m_vars_to_update.push_back({ v, sum });
} }
if (vi.m_add_idx != UINT_MAX || vi.m_mul_idx != UINT_MAX) if (vi.m_add_idx != UINT_MAX || vi.m_mul_idx != UINT_MAX)
// add repair actions for additions. // add repair actions for additions and multiplications
m_defs_to_update.push_back(v); m_defs_to_update.push_back(v);
} }
@ -389,28 +388,21 @@ namespace sls {
template<typename num_t> template<typename num_t>
void arith_plugin<num_t>::add_args(linear_term& term, expr* e, num_t const& coeff) { void arith_plugin<num_t>::add_args(linear_term& term, expr* e, num_t const& coeff) {
auto v = m_expr2var.get(e->get_id(), UINT_MAX); auto v = m_expr2var.get(e->get_id(), UINT_MAX);
if (v != UINT_MAX) {
add_arg(term, coeff, v);
return;
}
expr* x, * y; expr* x, * y;
num_t i; num_t i;
if (is_num(e, i)) { if (v != UINT_MAX)
term.m_coeff += coeff * i; add_arg(term, coeff, v);
return; else if (is_num(e, i))
} term.m_coeff += coeff * i;
if (a.is_add(e)) { else if (a.is_add(e)) {
for (expr* arg : *to_app(e)) for (expr* arg : *to_app(e))
add_args(term, arg, coeff); add_args(term, arg, coeff);
return;
} }
if (a.is_sub(e, x, y)) { else if (a.is_sub(e, x, y)) {
add_args(term, x, coeff); add_args(term, x, coeff);
add_args(term, y, -coeff); add_args(term, y, -coeff);
return;
} }
else if (a.is_mul(e)) {
if (a.is_mul(e)) {
unsigned_vector m; unsigned_vector m;
num_t c = coeff; num_t c = coeff;
for (expr* arg : *to_app(e)) for (expr* arg : *to_app(e))
@ -426,7 +418,7 @@ namespace sls {
add_arg(term, c, m[0]); add_arg(term, c, m[0]);
break; break;
default: { default: {
auto v = mk_var(e); v = mk_var(e);
unsigned idx = m_muls.size(); unsigned idx = m_muls.size();
m_muls.push_back({ v, m }); m_muls.push_back({ v, m });
num_t prod(1); num_t prod(1);
@ -438,20 +430,13 @@ namespace sls {
break; break;
} }
} }
return;
} }
if (a.is_uminus(e, x)) { else if (a.is_uminus(e, x))
add_args(term, x, -coeff); add_args(term, x, -coeff);
return; else if (is_uninterp(e))
} add_arg(term, coeff, mk_var(e));
else
if (is_uninterp(e)) { NOT_IMPLEMENTED_YET();
auto v = mk_var(e);
add_arg(term, coeff, v);
return;
}
UNREACHABLE();
} }
template<typename num_t> template<typename num_t>
@ -555,17 +540,22 @@ namespace sls {
} }
template<typename num_t> template<typename num_t>
void arith_plugin<num_t>::propagate_updates() { void arith_plugin<num_t>::repair_defs_and_updates() {
while (!m_defs_to_update.empty() || !m_vars_to_update.empty()) { while (!m_defs_to_update.empty() || !m_vars_to_update.empty()) {
while (!m_vars_to_update.empty()) { repair_updates();
auto [w, new_value1] = m_vars_to_update.back();
m_vars_to_update.pop_back();
update(w, new_value1);
}
repair_defs(); repair_defs();
} }
} }
template<typename num_t>
void arith_plugin<num_t>::repair_updates() {
while (!m_vars_to_update.empty()) {
auto [w, new_value1] = m_vars_to_update.back();
m_vars_to_update.pop_back();
update(w, new_value1);
}
}
template<typename num_t> template<typename num_t>
void arith_plugin<num_t>::repair_defs() { void arith_plugin<num_t>::repair_defs() {
while (!m_defs_to_update.empty()) { while (!m_defs_to_update.empty()) {
@ -769,7 +759,7 @@ namespace sls {
for (sat::literal lit : ctx.root_literals()) for (sat::literal lit : ctx.root_literals())
repair(lit); repair(lit);
propagate_updates(); repair_defs_and_updates();
// update literal assignment based on current model // update literal assignment based on current model
for (unsigned v = 0; v < ctx.num_bool_vars(); ++v) for (unsigned v = 0; v < ctx.num_bool_vars(); ++v)
@ -816,6 +806,19 @@ namespace sls {
out << c << "@" << bv << " "; out << c << "@" << bv << " ";
out << "\n"; out << "\n";
} }
for (auto md : m_muls) {
out << "v" << md.m_var << " := ";
for (auto w : md.m_monomial)
out << "v" << w << " ";
out << "\n";
}
for (auto ad : m_adds) {
out << "v" << ad.m_var << " := ";
for (auto [c, w] : ad.m_args)
out << c << "* v" << w << " + ";
out << ad.m_coeff;
out << "\n";
}
return out; return out;
} }

3
src/ast/sls/sls_arith_int.h
View file

@ -123,8 +123,9 @@ namespace sls {
void repair_add(add_def const& ad); void repair_add(add_def const& ad);
unsigned_vector m_defs_to_update; unsigned_vector m_defs_to_update;
vector<std::pair<var_t, num_t>> m_vars_to_update; vector<std::pair<var_t, num_t>> m_vars_to_update;
void propagate_updates(); void repair_defs_and_updates();
void repair_defs(); void repair_defs();
void repair_updates();
void repair(sat::literal lit); void repair(sat::literal lit);
void repair(sat::literal lit, ineq const& ineq); void repair(sat::literal lit, ineq const& ineq);