diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index b67e873c0..d66601678 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -118,12 +118,14 @@ void arith_rewriter::get_coeffs_gcd(expr * t, numeral & g, bool & first, unsigne continue; } if (first) { - get_power_product(arg, g); + if (!get_ite_gcd(arg, g)) + get_power_product(arg, g); SASSERT(g.is_int()); first = false; } else { - get_power_product(arg, a); + if (!get_ite_gcd(arg, a)) + get_power_product(arg, a); SASSERT(a.is_int()); g = gcd(abs(a), g); } @@ -132,6 +134,23 @@ void arith_rewriter::get_coeffs_gcd(expr * t, numeral & g, bool & first, unsigne } } +expr_ref arith_rewriter::div_ite(expr* t, numeral const& g) { + if (g == 1) + return expr_ref(t, m); + expr* th, *el, *c; + numeral n; + bool is_int = false; + if (m.is_ite(t, c, th, el)) + return expr_ref(m.mk_ite(c, div_ite(th, g), div_ite(el, g)), m); + if (m_util.is_mul(t, th, el)) { + return expr_ref(m_util.mk_mul(th, div_ite(el, g)), m); + } + VERIFY(m_util.is_numeral(t, n, is_int)); + if (n == 0) + return expr_ref(t, m); + return expr_ref(m_util.mk_numeral(n / g, is_int), m); +} + bool arith_rewriter::div_polynomial(expr * t, numeral const & g, const_treatment ct, expr_ref & result) { SASSERT(m_util.is_int(t)); SASSERT(!g.is_one()); @@ -159,6 +178,12 @@ bool arith_rewriter::div_polynomial(expr * t, numeral const & g, const_treatment new_args.push_back(m_util.mk_numeral(a, true)); continue; } + if (get_ite_gcd(arg, a)) { + a /= g; + if (!a.is_zero()) + new_args.push_back(div_ite(arg, g)); + continue; + } expr * pp = get_power_product(arg, a); a /= g; SASSERT(a.is_int()); diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index a1aadfa7f..a99477975 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -67,6 +67,7 @@ class arith_rewriter : public poly_rewriter { void get_coeffs_gcd(expr * t, numeral & g, bool & first, unsigned & num_consts); enum const_treatment { CT_FLOOR, CT_CEIL, CT_FALSE }; bool div_polynomial(expr * t, numeral const & g, const_treatment ct, expr_ref & result); + expr_ref div_ite(expr* t, numeral const& g); enum op_kind { LE, GE, EQ }; static op_kind inv(op_kind k) { return k == LE ? GE : (k == GE ? LE : EQ); } bool is_bound(expr * arg1, expr * arg2, op_kind kind, expr_ref & result); diff --git a/src/ast/rewriter/poly_rewriter.h b/src/ast/rewriter/poly_rewriter.h index 6880f7e23..cc3a5d292 100644 --- a/src/ast/rewriter/poly_rewriter.h +++ b/src/ast/rewriter/poly_rewriter.h @@ -60,6 +60,7 @@ protected: expr * get_power_product(expr * t); expr * get_power_product(expr * t, numeral & a); + bool get_ite_gcd(expr* t, numeral& a); br_status mk_flat_add_core(unsigned num_args, expr * const * args, expr_ref & result); br_status mk_nflat_add_core(unsigned num_args, expr * const * args, expr_ref & result); diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index f739579e6..0be71ab94 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -442,6 +442,26 @@ inline expr * poly_rewriter::get_power_product(expr * t, numeral & a) { a = numeral(1); return t; } +template +bool poly_rewriter::get_ite_gcd(expr* t, numeral& a) { + expr* th, *el, *cond; + rational b, c; + if (is_mul(t) && to_app(t)->get_num_args() == 2 && + get_ite_gcd(to_app(t)->get_arg(1), a) && + is_int_numeral(to_app(t)->get_arg(0), b) && abs(b) == 1) { + return true; + } + + if (M().is_ite(t, cond, th, el) && + (is_int_numeral(th, b) || get_ite_gcd(th, b)) && + (is_int_numeral(el, c) || get_ite_gcd(el, c))) { + a = gcd(b, c); + return true; + } + // verbose_stream() << "not gcd " << mk_bounded_pp(t, M()) << "\n"; + return false; +} + template bool poly_rewriter::is_mul(expr * t, numeral & c, expr * & pp) const { diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp index 590c4c6df..a31304831 100644 --- a/src/ast/sls/sls_arith_base.cpp +++ b/src/ast/sls/sls_arith_base.cpp @@ -2191,7 +2191,7 @@ namespace sls { auto const& vi = m_vars[v]; if (vi.m_def_idx == UINT_MAX) return true; - IF_VERBOSE(2, verbose_stream() << " repair def " << mk_bounded_pp(vi.m_expr, m) << "\n"); + IF_VERBOSE(4, verbose_stream() << vi.m_op << " repair def " << mk_bounded_pp(vi.m_expr, m) << "\n"); TRACE("sls", tout << "repair def " << mk_bounded_pp(vi.m_expr, m) << "\n"); switch (vi.m_op) { case arith_op_kind::LAST_ARITH_OP: diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp index d8e42d234..1f7d927e2 100644 --- a/src/ast/sls/sls_seq_plugin.cpp +++ b/src/ast/sls/sls_seq_plugin.cpp @@ -605,11 +605,15 @@ namespace sls { zstring ch(m_chars[ctx.rand(m_chars.size())]); m_str_updates.push_back({ x, strval1(y) + ch, 1 }); m_str_updates.push_back({ x, ch + strval1(y), 1 }); + m_str_updates.push_back({ x, ch, 1 }); + m_str_updates.push_back({ x, zstring(), 1 }); } if (!is_value(y) && !m_chars.empty()) { zstring ch(m_chars[ctx.rand(m_chars.size())]); m_str_updates.push_back({ y, strval1(x) + ch, 1 }); m_str_updates.push_back({ y, ch + strval1(x), 1 }); + m_str_updates.push_back({ x, ch, 1 }); + m_str_updates.push_back({ x, zstring(), 1}); } } return apply_update(); @@ -826,6 +830,7 @@ namespace sls { expr* x, * y; VERIFY(seq.str.is_at(e, x, y)); zstring se = strval0(e); + verbose_stream() << "repair down at " << mk_pp(e, m) << " " << se << "\n"; if (se.length() > 1) return false; zstring sx = strval0(x); @@ -886,6 +891,12 @@ namespace sls { if (offset_r.is_unsigned()) offset_u = offset_r.get_unsigned(); + // set to not a member: + if (value == -1) { + m_str_updates.push_back({ y, zstring(m_chars[ctx.rand(m_chars.size())]), 1 }); + if (lenx > 0) + m_str_updates.push_back({ x, zstring(), 1 }); + } // change x: // insert y into x at offset if (offset_r.is_unsigned() && 0 <= value && offset_u + value <= lenx && leny > 0) {