mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-07 11:41:22 +00:00
Code Activity

remove coefficient from multiplication definition

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-25 15:23:59 -07:00
parent 2bcb56fb13
commit fa6091dc16
2 changed files with 24 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -645,8 +645,8 @@ namespace sls {
// check for overflow // check for overflow
try { try {
for (auto idx : vi.m_muls) { for (auto idx : vi.m_muls) {
auto const& [w, coeff, monomial] = m_muls[idx]; auto const& [w, monomial] = m_muls[idx];
num_t prod(coeff); num_t prod(1);
for (auto [w, p] : monomial) for (auto [w, p] : monomial)
prod *= power_of(v == w ? new_value : value(w), p); prod *= power_of(v == w ? new_value : value(w), p);
} }
@ -690,8 +690,8 @@ namespace sls {
ctx.new_value_eh(m_vars[m_adds[idx].m_var].m_expr); ctx.new_value_eh(m_vars[m_adds[idx].m_var].m_expr);
for (auto idx : vi.m_muls) { for (auto idx : vi.m_muls) {
auto const& [w, coeff, monomial] = m_muls[idx]; auto const& [w, monomial] = m_muls[idx];
num_t prod(coeff); num_t prod(1);
try { try {
for (auto [w, p] : monomial) for (auto [w, p] : monomial)
prod *= power_of(value(w), p); prod *= power_of(value(w), p);
@ -737,8 +737,8 @@ namespace sls {
auto v = m_update_trail[i]; auto v = m_update_trail[i];
auto& vi = m_vars[v]; auto& vi = m_vars[v];
for (auto idx : vi.m_muls) { for (auto idx : vi.m_muls) {
auto const& [w, coeff, monomial] = m_muls[idx]; auto const& [w, monomial] = m_muls[idx];
num_t prod(coeff); num_t prod(1);
try { try {
for (auto [w, p] : monomial) for (auto [w, p] : monomial)
prod *= power_of(get_update_value(w), p); prod *= power_of(get_update_value(w), p);
@ -865,16 +865,15 @@ namespace sls {
} }
else if (a.is_mul(e)) { else if (a.is_mul(e)) {
unsigned_vector ms; unsigned_vector ms;
num_t c(1);
for (expr* arg : *to_app(e)) for (expr* arg : *to_app(e))
ms.push_back(mk_term(arg)); ms.push_back(mk_term(arg));
switch (ms.size()) { switch (ms.size()) {
case 0: case 0:
term.m_coeff += c*coeff; term.m_coeff += coeff;
break; break;
case 1: case 1:
add_arg(term, c*coeff, ms[0]); add_arg(term, coeff, ms[0]);
break; break;
default: { default: {
v = mk_var(e); v = mk_var(e);
@ -888,8 +887,8 @@ namespace sls {
++p, ++i; ++p, ++i;
mp.push_back({ w, p }); mp.push_back({ w, p });
} }
m_muls.push_back({ v, c, mp }); m_muls.push_back({ v, mp });
num_t prod(c); num_t prod(1);
for (auto [w, p] : mp) for (auto [w, p] : mp)
m_vars[w].m_muls.push_back(idx), prod *= power_of(value(w), p); m_vars[w].m_muls.push_back(idx), prod *= power_of(value(w), p);
m_vars[v].m_def_idx = idx; m_vars[v].m_def_idx = idx;
@ -1065,7 +1064,7 @@ namespace sls {
m_vars[v].m_bool_vars.push_back({ coeff, bv }); m_vars[v].m_bool_vars.push_back({ coeff, bv });
i.m_args_value += coeff * value(v); i.m_args_value += coeff * value(v);
if (is_mul(v)) { if (is_mul(v)) {
auto const& [w, c, monomial] = get_mul(v); auto const& [w, monomial] = get_mul(v);
for (auto [w, p] : monomial) for (auto [w, p] : monomial)
i.m_nonlinear.push_back({ w, { {v, coeff, p} } }); i.m_nonlinear.push_back({ w, { {v, coeff, p} } });
i.m_is_linear = false; i.m_is_linear = false;
@ -1164,8 +1163,8 @@ namespace sls {
break; break;
} }
case OP_MUL: { case OP_MUL: {
auto const& [w, coeff, monomial] = m_muls[vi.m_def_idx]; auto const& [w, monomial] = m_muls[vi.m_def_idx];
new_value = coeff; new_value = num_t(1);
for (auto [w, p] : monomial) for (auto [w, p] : monomial)
new_value *= power_of(value(w), p); new_value *= power_of(value(w), p);
break; break;
@ -1294,8 +1293,8 @@ namespace sls {
} }
} }
if (is_mul(v)) { if (is_mul(v)) {
auto const& [w, c, monomial] = get_mul(v); auto const& [w, monomial] = get_mul(v);
num_t lo(c), hi(c); num_t lo(1), hi(1);
bool lo_valid = true, hi_valid = true; bool lo_valid = true, hi_valid = true;
bool lo_strict = false, hi_strict = false; bool lo_strict = false, hi_strict = false;
for (auto [w, p] : monomial) { for (auto [w, p] : monomial) {
@ -1521,8 +1520,8 @@ namespace sls {
template<typename num_t> template<typename num_t>
bool arith_base<num_t>::repair_mul(mul_def const& md) { bool arith_base<num_t>::repair_mul(mul_def const& md) {
auto const& [v, coeff, monomial] = md; auto const& [v, monomial] = md;
num_t product(coeff); num_t product(1);
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);
@ -1702,9 +1701,9 @@ namespace sls {
template<typename num_t> template<typename num_t>
num_t arith_base<num_t>::mul_value_without(var_t m, var_t x) { num_t arith_base<num_t>::mul_value_without(var_t m, var_t x) {
auto const& vi = m_vars[m]; auto const& vi = m_vars[m];
auto const& [w, coeff, monomial] = m_muls[vi.m_def_idx]; auto const& [w, monomial] = m_muls[vi.m_def_idx];
SASSERT(m == w); SASSERT(m == w);
num_t r(coeff); num_t r(1);
for (auto [y, p] : monomial) for (auto [y, p] : monomial)
if (x != y) if (x != y)
r *= power_of(value(y), p); r *= power_of(value(y), p);
@ -1776,7 +1775,7 @@ namespace sls {
if (is_fixed(x)) if (is_fixed(x))
return; return;
if (is_mul(x)) { if (is_mul(x)) {
auto const& [w1, c, monomial] = get_mul(x); auto const& [w1, monomial] = get_mul(x);
for (auto [w1, p] : monomial) for (auto [w1, p] : monomial)
add_reset_update(w1); add_reset_update(w1);
} }
@ -1997,10 +1996,8 @@ namespace sls {
template<typename num_t> template<typename num_t>
std::ostream& arith_base<num_t>::display(std::ostream& out, mul_def const& md) const { std::ostream& arith_base<num_t>::display(std::ostream& out, mul_def const& md) const {
auto const& [w, coeff, monomial] = md; auto const& [w, monomial] = md;
bool first = true; bool first = true;
if (coeff != 1)
out << coeff, first = false;
for (auto [v, p] : monomial) { for (auto [v, p] : monomial) {
if (!first) if (!first)
out << " * "; out << " * ";
@ -2135,7 +2132,7 @@ namespace sls {
} }
case arith_op_kind::OP_MUL: { case arith_op_kind::OP_MUL: {
auto md = m_muls[vi.m_def_idx]; auto md = m_muls[vi.m_def_idx];
num_t prod(md.m_coeff); num_t prod(1);
for (auto [w, p] : md.m_monomial) for (auto [w, p] : md.m_monomial)
prod *= power_of(value(w), p); prod *= power_of(value(w), p);
return prod == value(v); return prod == value(v);
@ -2199,12 +2196,11 @@ namespace sls {
out << mk_bounded_pp(m_vars[v].m_expr, m) << "\n"; out << mk_bounded_pp(m_vars[v].m_expr, m) << "\n";
if (is_mul(v)) { if (is_mul(v)) {
auto const& [w, coeff, monomial] = get_mul(v); auto const& [w, monomial] = get_mul(v);
num_t prod(coeff); num_t prod(1);
for (auto [v, p] : monomial) for (auto [v, p] : monomial)
prod *= power_of(value(v), p); prod *= power_of(value(v), p);
out << "product " << prod << " value " << value(w) << "\n"; out << "product " << prod << " value " << value(w) << "\n";
out << "coeff " << coeff << "\n";
out << "v" << w << " := "; out << "v" << w << " := ";
for (auto [w, p] : monomial) { for (auto [w, p] : monomial) {
out << "(v" << w; out << "(v" << w;

1
src/ast/sls/sls_arith_base.h
View file

@ -120,7 +120,6 @@ namespace sls {
struct mul_def { struct mul_def {
unsigned m_var; unsigned m_var;
num_t m_coeff;
svector<std::pair<unsigned, unsigned>> m_monomial; svector<std::pair<unsigned, unsigned>> m_monomial;
}; };