From 7d765ddb6b4c1735e9df88a5062eea654756ee6a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Aug 2024 15:55:30 -0700 Subject: [PATCH] fixes Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_arith_base.cpp | 253 +++++-------------------------- src/ast/sls/sls_arith_base.h | 39 +---- src/ast/sls/sls_basic_plugin.cpp | 5 +- 3 files changed, 47 insertions(+), 250 deletions(-) diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp index ac5df6056..dd6b3571d 100644 --- a/src/ast/sls/sls_arith_base.cpp +++ b/src/ast/sls/sls_arith_base.cpp @@ -650,9 +650,13 @@ namespace sls { IF_VERBOSE(10, verbose_stream() << "new value eh " << mk_bounded_pp(e, m) << "\n"); + for (auto idx : vi.m_muls) + ctx.new_value_eh(m_vars[m_muls[idx].m_var].m_expr); + for (auto idx : vi.m_adds) + ctx.new_value_eh(m_vars[m_adds[idx].m_var].m_expr); + for (auto idx : vi.m_muls) { auto const& [w, coeff, monomial] = m_muls[idx]; - ctx.new_value_eh(m_vars[w].m_expr); num_t prod(coeff); try { for (auto [w, p] : monomial) @@ -669,7 +673,6 @@ namespace sls { for (auto idx : vi.m_adds) { auto const& ad = m_adds[idx]; auto w = ad.m_var; - ctx.new_value_eh(m_vars[w].m_expr); num_t sum(ad.m_coeff); for (auto const& [coeff, w] : ad.m_args) sum += coeff * value(w); @@ -948,7 +951,6 @@ namespace sls { template typename arith_base::var_t arith_base::mk_var(expr* e) { - SASSERT(!m.is_value(e)); var_t v = m_expr2var.get(e->get_id(), UINT_MAX); if (v == UINT_MAX) { v = m_vars.size(); @@ -1337,225 +1339,55 @@ namespace sls { return update(v, sum); } - template - bool arith_base::repair_power(mul_def const& md) { - auto const& [v, coeff, monomial] = md; - if (!is_int(v)) - return false; - for (auto [c, v, p] : monomial_iterator(md)) { - if (c == 0) - continue; - num_t val1 = div(value(v), c); - if (val1 < 0 && p % 2 == 0) - continue; - num_t root = root_of(p, val1); - if (in_bounds(v, -root) && (((p % 2 == 0) && ctx.rand(3) == 0) || val1 < 0)) - root = -root; - if (update(v, root)) - return true; - } - return false; - } - - // increment/decrement the value of one of the variables as long - // as it improves the repair distance. - template - bool arith_base::repair_mul_inc(mul_def const& md) { - num_t inc; - unsigned i = 0; - double sum_probs = 0; - unsigned sz = md.m_monomial.size(); - m_probs.reserve(sz); - for (auto [c, v, p] : monomial_iterator(md)) { - int r = -1; // repair_delta(v, inc); - auto prob = r <= 0 ? 0.1 : r; - sum_probs += prob; - m_probs[i++] = prob; - - } - i = sz; - double lim = sum_probs * ((double)ctx.rand() / random_gen().max_value()); - do { - lim -= m_probs[--i]; - } while (lim >= 0 && i > 0); - - return false; - } - - // update entries to +/- 1, except for one, which is set to be +/- value(v) - template - bool arith_base::repair_mul_ones(mul_def const& md) { - auto const& [v, coeff, monomial] = md; - auto val = value(v); - vector coeffs(monomial.size(), num_t(1)); - for (auto [c, v, p] : monomial_iterator(md)) { - if (c == 0) - continue; - auto new_value = root_of(p, abs(val)); - int sign = ctx.rand(2) == 0 ? 1 : -1; - if (sign == -1) - new_value = -new_value; - if (!in_bounds(v, new_value)) { - new_value = -new_value; - if (p % 2 != 0) - sign *= -1; - } - if (!in_bounds(v, new_value)) - continue; - - unsigned i = 0; - bool failed = false; - for (auto [w, q] : monomial) { - if (w == v) - coeffs[i] = new_value; - else if (q % 2 == 0) - coeffs[i] = num_t(ctx.rand(2) == 0 ? 1 : -1); - else { - auto sign1 = ctx.rand(2) == 0 ? 1 : -1; - coeffs[i] = num_t(sign1); - if (!in_bounds(w, coeffs[i])) { - sign1 = -sign1; - coeffs[i] = num_t(sign1); - } - if (!in_bounds(w, coeffs[i])) - failed = true; - sign *= sign1; - } - ++i; - } - if (failed) - continue; - - if ((sign == 1) != val > 0) { - bool fixed = false; - for (auto [w, q] : monomial) { - if (q % 2 == 1 && in_bounds(w, -coeffs[i])) { - coeffs[i] = -coeffs[i]; - fixed = true; - break; - } - } - if (!fixed) - continue; - } - i = 0; - for (auto [w, q] : monomial) { - if (!update(w, coeffs[i])) - return false; - ++i; - } - return true; - } - return false; - } - - // update one of the variables such that the product aligns with value(v) - template - bool arith_base::repair_mul_one(mul_def const& md) { - auto const& [v, coeff, monomial] = md; - if (!is_int(v)) - return false; - num_t val = value(v); - if (!divides(coeff, val)) - return false; - for (auto [c, v, p] : monomial_iterator(md)) { - if (c == 0 || !divides(c, val)) - continue; - auto val1 = div(val, c); - val1 = root_of(p, val); - if (update(v, val1)) - return true; - } - return false; - } - template bool arith_base::repair_mul(mul_def const& md) { auto const& [v, coeff, monomial] = md; num_t product(coeff); num_t val = value(v); - num_t new_value; for (auto [v, p]: monomial) 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) return true; - IF_VERBOSE(10, verbose_stream() << "repair mul " << mk_bounded_pp(m_vars[v].m_expr, m) << " := " << val << "(product: " << product << ")\n"); - unsigned sz = monomial.size(); - if (ctx.rand(20) == 0) - return update(v, product); - else if (val == 0) { - for (auto [c, v, p] : monomial_iterator(md)) - if (update(v, num_t(0))) - return true; - return false; + + + m_updates.reset(); + if (val == 0) { + for (auto [x, p] : monomial) + add_update(x, -value(x)); + } + else if (val == 1 || val == -1) { + for (auto [x, p] : monomial) { + add_update(x, num_t(1) - value(x)); + add_update(x, num_t(-1) - value(x)); + } } - else if (abs(val) == 1 && repair_mul_one(md)) - return true; - else if (repair_power(md)) - return true; - else if (ctx.rand(4) != 0 && repair_mul_one(md)) - return true; - else if (repair_mul_factors(md)) - return true; - else if (repair_mul_one(md)) - return true; else { - IF_VERBOSE(0, verbose_stream() << "repair mul " << mk_bounded_pp(m_vars[v].m_expr, m) << " := " << val << "(product: " << product << ")\n"); - - //NOT_IMPLEMENTED_YET(); - return false; - } - return false; - } - - template - bool arith_base::repair_mul_factors(mul_def const& md) { - auto const& [v, coeff, monomial] = md; - auto val = value(v); - if (!is_int(v)) - return false; - num_t n = div(val, coeff); - if (!divides(coeff, val) && ctx.rand(2) == 0) - n = div(val + coeff - 1, coeff); - if (n == 0) - return false; - auto const& fs = factor(abs(n)); - unsigned sz = monomial.size(); - vector coeffs(sz, num_t(1)); - vector gcds(sz, num_t(0)); - num_t sign(1); - for (auto c : coeffs) - sign *= c; - unsigned i = 0; - for (auto [w, p] : monomial) { - for (auto idx : m_vars[w].m_muls) { - auto const& [w1, coeff1, monomial1] = m_muls[idx]; - gcds[i] = gcd(gcds[i], abs(value(w1))); - } - auto const& vi = m_vars[w]; - if (vi.m_lo && vi.m_lo->value >= 0) - coeffs[i] = 1; - else if (vi.m_hi && vi.m_hi->value < 0) - coeffs[i] = -1; - else - coeffs[i] = num_t(ctx.rand(2) == 0 ? 1 : -1); - ++i; - } - for (auto f : fs) - coeffs[ctx.rand(sz)] *= f; - if ((sign == 0) != (n == 0)) - coeffs[ctx.rand(sz)] *= -1; - verbose_stream() << "value " << val << " coeff: " << coeff << " coeffs: " << coeffs << " factors: " << fs << "\n"; - i = 0; - for (auto [w, p] : monomial) { - if (!update(w, coeffs[i++])) { - verbose_stream() << "failed to update v" << w << " to " << coeffs[i - 1] << "\n"; - return false; + for (auto [x, p] : monomial) { + auto mx = mul_value_without(v, x); + // val / mx = x^p + if (mx == 0) + continue; + auto valmx = divide(x, val, mx); + auto r = root_of(p, valmx); + add_update(x, r - value(x)); + if (p % 2 == 0) + add_update(x, -r - value(x)); } } - verbose_stream() << "all updated for v" << v << " := " << value(v) << "\n"; - return true; - } + + if (apply_update()) + return eval_is_correct(v); + + m_updates.reset(); + for (auto [x, p] : monomial) + add_reset_update(x); + + if (apply_update()) + return eval_is_correct(v); + + return update(v, product); + } template bool arith_base::repair_rem(op_def const& od) { @@ -1687,8 +1519,7 @@ namespace sls { num_t r(coeff); for (auto [y, p] : monomial) if (x != y) - for (unsigned i = 0; i < p; ++i) - r *= value(y); + r *= power_of(value(y), p); return r; } diff --git a/src/ast/sls/sls_arith_base.h b/src/ast/sls/sls_arith_base.h index 515046d41..67fddfd0a 100644 --- a/src/ast/sls/sls_arith_base.h +++ b/src/ast/sls/sls_arith_base.h @@ -160,12 +160,7 @@ namespace sls { unsigned get_num_vars() const { return m_vars.size(); } - bool eval_is_correct(var_t v); - bool repair_mul_one(mul_def const& md); - bool repair_power(mul_def const& md); - bool repair_mul_factors(mul_def const& md); - bool repair_mul_ones(mul_def const& md); - bool repair_mul_inc(mul_def const& md); + bool eval_is_correct(var_t v); bool repair_mul(mul_def const& md); bool repair_add(add_def const& ad); bool repair_mod(op_def const& od); @@ -201,38 +196,6 @@ namespace sls { unsigned p; // power }; - struct monomial_iterator_base { - arith_base& a; - mul_def const& md; - unsigned m_seed = 0; - unsigned m_idx; - monomial_iterator_base(arith_base& a, mul_def const& md, unsigned idx, unsigned seed) : a(a), md(md), m_seed(seed), m_idx(idx) {} - monomial_elem operator*() { - auto [v, p] = md.m_monomial[(m_idx + m_seed) % md.m_monomial.size()]; - num_t prod(md.m_coeff); - for (auto [w, q] : md.m_monomial) - if (w != v) - prod *= a.power_of(a.value(w), q); - return { prod, v, p }; - } - monomial_iterator_base& operator++() { - ++m_idx; - return *this; - } - bool operator==(monomial_iterator_base const& other) const { return m_idx == other.m_idx; } - bool operator!=(monomial_iterator_base const& other) const { return m_idx != other.m_idx; } - }; - - struct monomials { - arith_base& a; - mul_def const& md; - monomials(arith_base & a, mul_def const& md) : a(a), md(md) {} - monomial_iterator_base begin() { return monomial_iterator_base(a, md, 0, a.ctx.rand()); } - monomial_iterator_base end() { return monomial_iterator_base(a, md, md.m_monomial.size(), 0); } - }; - - monomials monomial_iterator(mul_def const& md) { return monomials(*this, md); } - // double reward(sat::literal lit); bool sign(sat::bool_var v) const { return !ctx.is_true(sat::literal(v, false)); } diff --git a/src/ast/sls/sls_basic_plugin.cpp b/src/ast/sls/sls_basic_plugin.cpp index cbb77dad0..c55785c71 100644 --- a/src/ast/sls/sls_basic_plugin.cpp +++ b/src/ast/sls/sls_basic_plugin.cpp @@ -38,6 +38,8 @@ namespace sls { return false; if (m.is_distinct(e) && !m.is_bool(to_app(e)->get_arg(0))) return false; + if (m.is_not(e, x)) + return is_basic(x); return true; } @@ -50,7 +52,7 @@ namespace sls { } void basic_plugin::register_term(expr* e) { - if (is_basic(e)) + if (is_basic(e) && m.is_bool(e)) m_values.setx(e->get_id(), bval1(to_app(e)), false); } @@ -94,6 +96,7 @@ namespace sls { } bool basic_plugin::bval1(app* e) const { + verbose_stream() << mk_bounded_pp(e, m) << "\n"; if (m.is_not(e)) return bval1(to_app(e->get_arg(0))); SASSERT(m.is_bool(e));