From 8c44f0c291abdef2442dd747c8c65fcd382c468e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 2 Dec 2024 14:38:34 -0800
Subject: [PATCH] add ast-mark to make traversal feasible
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/rewriter/poly_rewriter.h | 3 ++-
src/ast/rewriter/poly_rewriter_def.h | 25 ++++++++++++++++++++-----
2 files changed, 22 insertions(+), 6 deletions(-)
diff --git a/src/ast/rewriter/poly_rewriter.h b/src/ast/rewriter/poly_rewriter.h
index cc3a5d292..5a88bee30 100644
--- a/src/ast/rewriter/poly_rewriter.h
+++ b/src/ast/rewriter/poly_rewriter.h
@@ -60,7 +60,8 @@ protected:
expr * get_power_product(expr * t);
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_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 0be71ab94..a23f26fb0 100644
--- a/src/ast/rewriter/poly_rewriter_def.h
+++ b/src/ast/rewriter/poly_rewriter_def.h
@@ -444,21 +444,36 @@ inline expr * poly_rewriter<Config>::get_power_product(expr * t, numeral & a) {
}
template<typename Config>
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;
+
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;
+ mark.mark(t, true);
+ return a != 1;
}
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))) {
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;
}