mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

try pushing gcd over ite

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-12-02 13:34:32 -08:00
parent e6feb8423a
commit bd5d388f15
6 changed files with 61 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

29
src/ast/rewriter/arith_rewriter.cpp
View file

@ -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());

1
src/ast/rewriter/arith_rewriter.h
View file

@ -67,6 +67,7 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
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);

1
src/ast/rewriter/poly_rewriter.h
View file

@ -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);

20
src/ast/rewriter/poly_rewriter_def.h
View file

@ -442,6 +442,26 @@ inline expr * poly_rewriter<Config>::get_power_product(expr * t, numeral & a) {
a = numeral(1);
return t;
}
template<typename Config>
bool poly_rewriter<Config>::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<typename Config>
bool poly_rewriter<Config>::is_mul(expr * t, numeral & c, expr * & pp) const {

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

@ -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:

11
src/ast/sls/sls_seq_plugin.cpp
View file

@ -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) {