mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

add ast-mark to make traversal feasible

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

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

@ -61,6 +61,7 @@ protected:
expr * get_power_product(expr * t); expr * get_power_product(expr * t);
expr * get_power_product(expr * t, numeral & a); expr * get_power_product(expr * t, numeral & a);
bool get_ite_gcd(expr* t, numeral& a); bool get_ite_gcd(expr* t, numeral& a);
bool get_ite_gcd(ast_mark& mark, expr* t, numeral& a);
br_status mk_flat_add_core(unsigned num_args, expr * const * args, expr_ref & result); 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); br_status mk_nflat_add_core(unsigned num_args, expr * const * args, expr_ref & result);

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

@ -444,21 +444,36 @@ inline expr * poly_rewriter<Config>::get_power_product(expr * t, numeral & a) {
} }
template<typename Config> template<typename Config>
bool poly_rewriter<Config>::get_ite_gcd(expr* t, numeral& a) { bool poly_rewriter<Config>::get_ite_gcd(expr* t, numeral& a) {
expr* th, *el, *cond; ast_mark mark;
//verbose_stream() << "gcd " << get_depth(t) << " " << mk_bounded_pp(t, M()) << "\n";
bool r = get_ite_gcd(mark, t, a);
//verbose_stream() << a << " " << r << "\n";
return r;
}
template<typename Config>
bool poly_rewriter<Config>::get_ite_gcd(ast_mark & mark, expr* t, numeral& a) {
if (mark.is_marked(t)) {
a = 0;
return true;
}
expr* th, * el, * cond;
rational b, c; rational b, c;
if (is_mul(t) && to_app(t)->get_num_args() == 2 && if (is_mul(t) && to_app(t)->get_num_args() == 2 &&
get_ite_gcd(to_app(t)->get_arg(1), a) && get_ite_gcd(to_app(t)->get_arg(1), a) &&
is_int_numeral(to_app(t)->get_arg(0), b) && abs(b) == 1) { is_int_numeral(to_app(t)->get_arg(0), b) && abs(b) == 1) {
return true; mark.mark(t, true);
return a != 1;
} }
if (M().is_ite(t, cond, th, el) && if (M().is_ite(t, cond, th, el) &&
(is_int_numeral(th, b) || get_ite_gcd(th, b)) && (is_int_numeral(th, b) || get_ite_gcd(th, b)) &&
(is_int_numeral(el, c) || get_ite_gcd(el, c))) { (is_int_numeral(el, c) || get_ite_gcd(el, c))) {
a = gcd(b, c); a = gcd(b, c);
return true; mark.mark(t, true);
return a != 1;
} }
// verbose_stream() << "not gcd " << mk_bounded_pp(t, M()) << "\n";
return false; return false;
} }