From cb789f6ca8abb33fdc546452729732047ca337c0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 24 Nov 2022 23:44:35 +0700 Subject: [PATCH] add arithmetical macros Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/eliminate_predicates.cpp | 111 ++++++++++++++++++- src/ast/simplifiers/eliminate_predicates.h | 1 - src/ast/simplifiers/propagate_values.cpp | 3 +- 3 files changed, 109 insertions(+), 6 deletions(-) diff --git a/src/ast/simplifiers/eliminate_predicates.cpp b/src/ast/simplifiers/eliminate_predicates.cpp index 052a44397..afa07a3a3 100644 --- a/src/ast/simplifiers/eliminate_predicates.cpp +++ b/src/ast/simplifiers/eliminate_predicates.cpp @@ -52,6 +52,8 @@ forbidden from macros vs forbidden from elimination #include "ast/ast_util.h" #include "ast/for_each_ast.h" #include "ast/recfun_decl_plugin.h" +#include "ast/bv_decl_plugin.h" +#include "ast/arith_decl_plugin.h" #include "ast/occurs.h" #include "ast/array_decl_plugin.h" #include "ast/rewriter/var_subst.h" @@ -331,9 +333,11 @@ void eliminate_predicates::try_find_macro(clause& cl) { insert_macro(f, def, cl.m_dep); cl.m_alive = false; fml = m.mk_not(m.mk_eq(k, t)); - init_clause(fml, cl.m_dep, UINT_MAX); - + clause* new_cl = init_clause(fml, cl.m_dep, UINT_MAX); + add_use_list(*new_cl); + m_clauses.push_back(new_cl); }; + if (cl.is_unit() && !cl.sign(0) && m.is_iff(cl.atom(0), x, y)) { expr* z, * u; if (m.is_eq(x, z, u) && can_be_conditioned(z, u, y)) { @@ -357,10 +361,111 @@ void eliminate_predicates::try_find_macro(clause& cl) { // // other macros handled by macro_finder: // - // arithmetic/bit-vectors // (= (+ (f x) s) t) // becomes (= (f x) (- t s)) + // + // TBD: + // (= (+ (* -1 (f x)) x) t) + // becomes (= (f x) (- (- t s))) + + bv_util bv(m); + arith_util a(m); + auto is_add = [&](expr * e) { + rational n; + return a.is_add(e) || bv.is_bv_add(e); + }; + + auto sub = [&](expr* t, expr* s) { + if (a.is_int_real(t)) + return expr_ref(a.mk_sub(t, s), m); + else + return expr_ref(bv.mk_bv_sub(t, s), m); + }; + + auto subtract = [&](expr* t, app* s, unsigned i) { + expr_ref result(t, m); + unsigned j = 0; + for (expr* arg : *s) { + ++j; + if (i != j) + result = sub(result, arg); + } + return result; + }; + + auto uminus = [&](expr* t) { + if (a.is_int_real(t)) + return expr_ref(a.mk_uminus(t), m); + else + return expr_ref(bv.mk_bv_neg(t), m); + }; + + auto is_inverse = [&](expr*& t) { + expr* x, * y; + rational n; + if (a.is_mul(t, x, y) && a.is_numeral(x, n) && n == -1) { + t = y; + return true; + } + if (bv.is_bv_mul(t, x, y) && bv.is_numeral(x, n) && n + 1 == rational::power_of_two(bv.get_bv_size(t))) { + t = y; + return true; + } + return false; + }; + + auto find_arith_macro = [&](expr* x, expr* y) { + if (!is_add(x)) + return false; + + if (!is_macro_safe(y)) + return false; + + unsigned i = 0; + for (expr* arg : *to_app(x)) { + ++i; + bool inv = is_inverse(arg); + if (!can_be_macro_head(arg, cl.m_bound.size())) + continue; + app* head = to_app(arg); + func_decl* f = head->get_decl(); + if (head->get_num_args() != cl.m_bound.size()) + continue; + if (occurs(f, y)) + continue; + unsigned j = 0; + for (expr* arg2 : *head) { + ++j; + if (i == j) + continue; + if (occurs(f, arg2)) + goto next; + if (!is_macro_safe(arg2)) + goto next; + } + { + // arg = y - x - arg; + expr_ref y1 = subtract(y, to_app(x), i); + if (inv) + y1 = uminus(y1); + insert_macro(to_app(arg), y1, cl.m_dep); + cl.m_alive = false; + return true; + } + next: + ; + } + return false; + }; + + if (cl.is_unit() && !cl.sign(0) && m.is_eq(cl.atom(0), x, y)) { + if (find_arith_macro(x, y)) + return; + if (find_arith_macro(y, x)) + return; + } + // // macro_finder also has: diff --git a/src/ast/simplifiers/eliminate_predicates.h b/src/ast/simplifiers/eliminate_predicates.h index f5d1cab96..6afd0886a 100644 --- a/src/ast/simplifiers/eliminate_predicates.h +++ b/src/ast/simplifiers/eliminate_predicates.h @@ -107,7 +107,6 @@ private: bool try_find_binary_definition(func_decl* p, app_ref& head, expr_ref& def, expr_dependency_ref& dep); void try_resolve_definition(func_decl* p); void insert_macro(app* head, expr* def, expr_dependency* dep); - bool has_macro(func_decl* p, app_ref& head, expr_ref& def, expr_dependency_ref& dep); expr_ref bind_free_variables_in_def(clause& cl, app* head, expr* def); bool can_be_macro_head(expr* head, unsigned num_bound); bool is_macro_safe(expr* e); diff --git a/src/ast/simplifiers/propagate_values.cpp b/src/ast/simplifiers/propagate_values.cpp index b7bd6eb37..6a179674b 100644 --- a/src/ast/simplifiers/propagate_values.cpp +++ b/src/ast/simplifiers/propagate_values.cpp @@ -96,7 +96,6 @@ void propagate_values::reduce() { m_rewriter.set_substitution(nullptr); m_rewriter.reset(); - advance_qhead(m_fmls.size()); } @@ -113,4 +112,4 @@ void propagate_values::updt_params(params_ref const& p) { void propagate_values::collect_param_descrs(param_descrs& r) { th_rewriter::get_param_descrs(r); r.insert("max_rounds", CPK_UINT, "(default: 4) maximum number of rounds."); -} \ No newline at end of file +}