From a1af82ee639c4b90c00863a8c6ae9882c366f119 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 12 Mar 2026 04:16:04 +0000 Subject: [PATCH 1/5] Initial plan From c303b56f04329a89b5d72928fb1a01961e5eed7b Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 12 Mar 2026 04:37:17 +0000 Subject: [PATCH 2/5] Add injectivity_simplifier and register injectivity2 tactic + injectivity simplifier Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/simplifiers/injectivity_simplifier.h | 190 +++++++++++++++++++ src/tactic/core/injectivity_tactic.h | 11 ++ 2 files changed, 201 insertions(+) create mode 100644 src/ast/simplifiers/injectivity_simplifier.h diff --git a/src/ast/simplifiers/injectivity_simplifier.h b/src/ast/simplifiers/injectivity_simplifier.h new file mode 100644 index 000000000..05b5e69ec --- /dev/null +++ b/src/ast/simplifiers/injectivity_simplifier.h @@ -0,0 +1,190 @@ +/*++ +Copyright (c) 2017 Microsoft Corporation + +Module Name: + + injectivity_simplifier.h + +Abstract: + + Dependent expression simplifier for injectivity rewriting. + + - Discover axioms of the form `forall x. (= (g (f x)) x)` + Mark `f` as injective + + - Rewrite (sub)terms of the form `(= (f x) (f y))` to `(= x y)` whenever `f` is injective. + +Author: + + Nicolas Braud-Santoni (t-nibrau) 2017-08-10 + Ported to simplifier by Nikolaj Bjorner (nbjorner) 2023 + +Notes: + * does not support cores nor proofs + +--*/ + +#pragma once + +#include "ast/simplifiers/dependent_expr_state.h" +#include "ast/rewriter/rewriter_def.h" + +class injectivity_simplifier : public dependent_expr_simplifier { + + struct inj_map : public obj_map*> { + ast_manager& m; + + inj_map(ast_manager& m) : m(m) {} + + ~inj_map() { + for (auto& kv : *this) { + for (func_decl* f : *kv.get_value()) + m.dec_ref(f); + m.dec_ref(kv.m_key); + dealloc(kv.m_value); + } + } + + void insert(func_decl* f, func_decl* g) { + obj_hashtable* inverses; + if (!obj_map::find(f, inverses)) { + m.inc_ref(f); + inverses = alloc(obj_hashtable); + obj_map::insert(f, inverses); + } + if (!inverses->contains(g)) { + m.inc_ref(g); + inverses->insert(g); + } + } + }; + + struct rw_cfg : public default_rewriter_cfg { + ast_manager& m; + inj_map& m_map; + + rw_cfg(ast_manager& m, inj_map& map) : m(m), m_map(map) {} + + br_status reduce_app(func_decl* f, unsigned num, expr* const* args, + expr_ref& result, proof_ref& result_pr) { + if (num != 2 || !m.is_eq(f)) + return BR_FAILED; + + if (!is_app(args[0]) || !is_app(args[1])) + return BR_FAILED; + + app* a = to_app(args[0]); + app* b = to_app(args[1]); + + if (a->get_decl() != b->get_decl()) + return BR_FAILED; + + if (a->get_num_args() != 1 || b->get_num_args() != 1) + return BR_FAILED; + + if (!m_map.contains(a->get_decl())) + return BR_FAILED; + + SASSERT(a->get_arg(0)->get_sort() == b->get_arg(0)->get_sort()); + result = m.mk_eq(a->get_arg(0), b->get_arg(0)); + result_pr = nullptr; + return BR_DONE; + } + }; + + struct rw : public rewriter_tpl { + rw_cfg m_cfg; + + rw(ast_manager& m, inj_map& map) : + rewriter_tpl(m, false, m_cfg), + m_cfg(m, map) {} + }; + + inj_map m_map; + rw m_rw; + + bool is_axiom(expr* n, func_decl*& f, func_decl*& g) { + if (!is_forall(n)) + return false; + + quantifier* q = to_quantifier(n); + if (q->get_num_decls() != 1) + return false; + + expr* body = q->get_expr(); + if (!m.is_eq(body)) + return false; + + app* body_a = to_app(body); + if (body_a->get_num_args() != 2) + return false; + + expr* a = body_a->get_arg(0); + expr* b = body_a->get_arg(1); + + if (is_app(a) && is_var(b)) { + // keep a, b as-is + } + else if (is_app(b) && is_var(a)) { + std::swap(a, b); + } + else + return false; + + app* a_app = to_app(a); + var* b_var = to_var(b); + + if (b_var->get_idx() != 0) + return false; + + if (a_app->get_num_args() != 1) + return false; + + g = a_app->get_decl(); + expr* a_body = a_app->get_arg(0); + + if (!is_app(a_body)) + return false; + + app* a_body_app = to_app(a_body); + if (a_body_app->get_num_args() != 1) + return false; + + f = a_body_app->get_decl(); + expr* a_body_body = a_body_app->get_arg(0); + + if (a_body_body != b_var) + return false; + + return true; + } + +public: + injectivity_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s) : + dependent_expr_simplifier(m, s), m_map(m), m_rw(m, m_map) {} + + char const* name() const override { return "injectivity"; } + + void reduce() override { + // Phase 1: Scan for injectivity axioms + for (unsigned idx : indices()) { + auto const& d = m_fmls[idx]; + func_decl* fn = nullptr; + func_decl* inv = nullptr; + if (is_axiom(d.fml(), fn, inv)) { + TRACE("injectivity", tout << "Marking " << fn->get_name() << " as injective\n";); + m_map.insert(fn, inv); + } + } + + // Phase 2: Rewrite using injectivity + expr_ref new_fml(m); + proof_ref new_pr(m); + for (unsigned idx : indices()) { + auto const& d = m_fmls[idx]; + m_rw(d.fml(), new_fml, new_pr); + if (new_fml != d.fml()) + m_fmls.update(idx, dependent_expr(m, new_fml, nullptr, d.dep())); + } + } +}; diff --git a/src/tactic/core/injectivity_tactic.h b/src/tactic/core/injectivity_tactic.h index 78310909a..d0bdfa283 100644 --- a/src/tactic/core/injectivity_tactic.h +++ b/src/tactic/core/injectivity_tactic.h @@ -45,12 +45,23 @@ Tactic Documentation: #pragma once #include "util/params.h" +#include "tactic/dependent_expr_state_tactic.h" +#include "ast/simplifiers/injectivity_simplifier.h" class ast_manager; class tactic; tactic * mk_injectivity_tactic(ast_manager & m, params_ref const & p = params_ref()); +inline tactic* mk_injectivity2_tactic(ast_manager& m, params_ref const& p = params_ref()) { + return alloc(dependent_expr_state_tactic, m, p, + [](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* { + return alloc(injectivity_simplifier, m, p, s); + }); +} + /* ADD_TACTIC("injectivity", "Identifies and applies injectivity axioms.", "mk_injectivity_tactic(m, p)") + ADD_TACTIC("injectivity2", "Identifies and applies injectivity axioms.", "mk_injectivity2_tactic(m, p)") + ADD_SIMPLIFIER("injectivity", "Identifies and applies injectivity axioms.", "alloc(injectivity_simplifier, m, p, s)") */ From 995e0e1f145fcf19384b08b437905a12cafc8a2c Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 12 Mar 2026 05:32:32 +0000 Subject: [PATCH 3/5] Deprecate injectivity_tactic.cpp: forward mk_injectivity_tactic to simplifier-based impl Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/tactic/core/CMakeLists.txt | 1 - src/tactic/core/injectivity_tactic.h | 5 +---- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index 69c60bc7d..8ab41f155 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -6,7 +6,6 @@ z3_add_component(core_tactics ctx_simplify_tactic.cpp elim_term_ite_tactic.cpp elim_uncnstr_tactic.cpp - injectivity_tactic.cpp nnf_tactic.cpp occf_tactic.cpp pb_preprocess_tactic.cpp diff --git a/src/tactic/core/injectivity_tactic.h b/src/tactic/core/injectivity_tactic.h index d0bdfa283..06a841fe6 100644 --- a/src/tactic/core/injectivity_tactic.h +++ b/src/tactic/core/injectivity_tactic.h @@ -50,9 +50,7 @@ Tactic Documentation: class ast_manager; class tactic; -tactic * mk_injectivity_tactic(ast_manager & m, params_ref const & p = params_ref()); - -inline tactic* mk_injectivity2_tactic(ast_manager& m, params_ref const& p = params_ref()) { +inline tactic* mk_injectivity_tactic(ast_manager& m, params_ref const& p = params_ref()) { return alloc(dependent_expr_state_tactic, m, p, [](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* { return alloc(injectivity_simplifier, m, p, s); @@ -61,7 +59,6 @@ inline tactic* mk_injectivity2_tactic(ast_manager& m, params_ref const& p = para /* ADD_TACTIC("injectivity", "Identifies and applies injectivity axioms.", "mk_injectivity_tactic(m, p)") - ADD_TACTIC("injectivity2", "Identifies and applies injectivity axioms.", "mk_injectivity2_tactic(m, p)") ADD_SIMPLIFIER("injectivity", "Identifies and applies injectivity axioms.", "alloc(injectivity_simplifier, m, p, s)") */ From 7692dfc7d6d3309a03b14acdcb79b10763a77c18 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 12 Mar 2026 16:25:04 +0000 Subject: [PATCH 4/5] Delete injectivity_tactic.cpp (deprecated, replaced by injectivity_simplifier.h) Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/tactic/core/injectivity_tactic.cpp | 281 ------------------------- 1 file changed, 281 deletions(-) delete mode 100644 src/tactic/core/injectivity_tactic.cpp diff --git a/src/tactic/core/injectivity_tactic.cpp b/src/tactic/core/injectivity_tactic.cpp deleted file mode 100644 index eb6470ace..000000000 --- a/src/tactic/core/injectivity_tactic.cpp +++ /dev/null @@ -1,281 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - injectivity_tactic.cpp - - -Author: - - Nicolas Braud-Santoni (t-nibrau) 2017-08-10 - ---*/ -#include -#include -#include "tactic/tactical.h" -#include "ast/rewriter/rewriter_def.h" -#include "tactic/core/injectivity_tactic.h" -#include "util/dec_ref_util.h" - - -class injectivity_tactic : public tactic { - - struct InjHelper : public obj_map*> { - ast_manager & m_manager; - - void insert(func_decl* const f, func_decl* const g) { - obj_hashtable *m; - if (! obj_map::find(f, m)) { - m_manager.inc_ref(f); - m = alloc(obj_hashtable); // TODO: Check we don't leak memory - obj_map::insert(f, m); - } - if (!m->contains(g)) { - m_manager.inc_ref(g); - m->insert(g); - } - } - - bool find(func_decl* const f, func_decl* const g) const { - obj_hashtable *m; - if(! obj_map::find(f, m)) - return false; - - return m->contains(g); - } - - InjHelper(ast_manager& m) : obj_map*>(), m_manager(m) {} - ~InjHelper() { - for(auto m : *this) { - for (func_decl* f : *m.get_value()) - m_manager.dec_ref(f); - - m_manager.dec_ref(m.m_key); - dealloc(m.m_value); - } - } - - }; - - struct finder { - ast_manager & m_manager; - InjHelper & inj_map; - - finder(ast_manager & m, InjHelper & map, params_ref const & p) : - m_manager(m), - inj_map(map) { - updt_params(p); - } - - ast_manager & m() const { return m_manager; } - - bool is_axiom(expr* n, func_decl* &f, func_decl* &g) { - if (!is_forall(n)) - return false; - - quantifier* const q = to_quantifier(n); - if (q->get_num_decls() != 1) - return false; - - const expr * const body = q->get_expr(); - - // n ~= forall x. body - - if (!m().is_eq(body)) - return false; - - const app * const body_a = to_app(body); - if (body_a->get_num_args() != 2) - return false; - - const expr* a = body_a->get_arg(0); - const expr* b = body_a->get_arg(1); - - // n ~= forall x. (= a b) - - if (is_app(a) && is_var(b)) { - // Do nothing - } - else if (is_app(b) && is_var(a)) { - std::swap(a, b); - } - else - return false; - - const app* const a_app = to_app(a); - const var* const b_var = to_var(b); - - if (b_var->get_idx() != 0) // idx is the De Bruijn's index - return false; - - if (a_app->get_num_args() != 1) - return false; - - g = a_app->get_decl(); - const expr* const a_body = a_app->get_arg(0); - - // n ~= forall x. (= (g a_body) x) - - if (!is_app(a_body)) - return false; - const app* const a_body_app = to_app(a_body); - if (a_body_app->get_num_args() != 1) // Maybe TODO: support multi-argument functions - return false; - - f = a_body_app->get_decl(); - const expr* const a_body_body = a_body_app->get_arg(0); - - // n ~= forall x. (= (g (f a_body_body)) x) - if (a_body_body != b_var) - return false; - - // n ~= forall x. (= (g (f x)) x) - - return true; - } - - void operator()(goal_ref const & goal, - goal_ref_buffer & result) { - tactic_report report("injectivity", *goal); - fail_if_unsat_core_generation("injectivity", goal); // TODO: Support UNSAT cores - fail_if_proof_generation("injectivity", goal); - - for (unsigned i = 0; i < goal->size(); ++i) { - func_decl *f, *g; - if (!is_axiom(goal->form(i), f, g)) continue; - TRACE(injectivity, tout << "Marking " << f->get_name() << " as injective" << std::endl;); - inj_map.insert(f, g); - // TODO: Record that g is f's pseudoinverse - } - } - - void updt_params(params_ref const & p) {} - }; - - struct rewriter_eq_cfg : public default_rewriter_cfg { - ast_manager & m_manager; - InjHelper & inj_map; - - ast_manager & m() const { return m_manager; } - - rewriter_eq_cfg(ast_manager & m, InjHelper & map, params_ref const & p) : m_manager(m), inj_map(map) { - } - - void cleanup_buffers() { - } - - void reset() { - } - - br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { - if (num != 2) - return BR_FAILED; - - if (!m().is_eq(f)) - return BR_FAILED; - - // We are rewriting (= a b) - if (!is_app(args[0]) || !is_app(args[1])) - return BR_FAILED; - - const app* const a = to_app(args[0]); - const app* const b = to_app(args[1]); - - // a and b are applications of the same function - if (a->get_decl() != b->get_decl()) - return BR_FAILED; - - // Maybe TODO: Generalize to multi-parameter functions ? - if (a->get_num_args() != 1 || b->get_num_args() != 1) - return BR_FAILED; - - if (!inj_map.contains(a->get_decl())) - return BR_FAILED; - - SASSERT(a->get_arg(0)->get_sort() == b->get_arg(0)->get_sort()); - TRACE(injectivity, tout << "Rewriting (= " << mk_ismt2_pp(args[0], m()) << - " " << mk_ismt2_pp(args[1], m()) << ")" << std::endl;); - result = m().mk_eq(a->get_arg(0), b->get_arg(0)); - result_pr = nullptr; - return BR_DONE; - } - - }; - - struct rewriter_eq : public rewriter_tpl { - rewriter_eq_cfg m_cfg; - rewriter_eq(ast_manager & m, InjHelper & map, params_ref const & p) : - rewriter_tpl(m, m.proofs_enabled(), m_cfg), - m_cfg(m, map, p) { - } - }; - - struct rewriter_inverse { }; - - finder * m_finder; - rewriter_eq * m_eq; - InjHelper * m_map; - params_ref m_params; - ast_manager & m_manager; - -public: - injectivity_tactic(ast_manager & m, params_ref const & p): - m_params(p), - m_manager(m) { - TRACE(injectivity, tout << "constructed new tactic" << std::endl;); - m_map = alloc(InjHelper, m); - m_finder = alloc(finder, m, *m_map, p); - m_eq = alloc(rewriter_eq, m, *m_map, p); - } - - tactic * translate(ast_manager & m) override { - return alloc(injectivity_tactic, m, m_params); - } - - ~injectivity_tactic() override { - dealloc(m_finder); - dealloc(m_eq); - dealloc(m_map); - } - - char const* name() const override { return "injectivity"; } - - void updt_params(params_ref const & p) override { - m_params.append(p); - m_finder->updt_params(m_params); - } - - void collect_param_descrs(param_descrs & r) override { - insert_max_memory(r); - insert_produce_models(r); - } - - void operator()(goal_ref const & g, - goal_ref_buffer & result) override { - (*m_finder)(g, result); - - for (unsigned i = 0; i < g->size(); ++i) { - expr* curr = g->form(i); - expr_ref rw(m_manager); - proof_ref pr(m_manager); - (*m_eq)(curr, rw, pr); - g->update(i, rw, pr, g->dep(i)); - } - result.push_back(g.get()); - } - - void cleanup() override { - InjHelper * m = alloc(InjHelper, m_manager); - finder * f = alloc(finder, m_manager, *m, m_params); - rewriter_eq * r = alloc(rewriter_eq, m_manager, *m, m_params); - std::swap(m, m_map), std::swap(f, m_finder), std::swap(r, m_eq); - dealloc(m), dealloc(f), dealloc(r); - } - - -}; - -tactic * mk_injectivity_tactic(ast_manager & m, params_ref const & p) { - return alloc(injectivity_tactic, m, p); -} From 56c88022e28e0023aa358ef9e97e2696cc2b2547 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 12 Mar 2026 18:27:36 +0000 Subject: [PATCH 5/5] Fix build: use unquoted TRACE tag identifier instead of string literal Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/simplifiers/injectivity_simplifier.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/simplifiers/injectivity_simplifier.h b/src/ast/simplifiers/injectivity_simplifier.h index 05b5e69ec..60d605165 100644 --- a/src/ast/simplifiers/injectivity_simplifier.h +++ b/src/ast/simplifiers/injectivity_simplifier.h @@ -172,7 +172,7 @@ public: func_decl* fn = nullptr; func_decl* inv = nullptr; if (is_axiom(d.fml(), fn, inv)) { - TRACE("injectivity", tout << "Marking " << fn->get_name() << " as injective\n";); + TRACE(injectivity, tout << "Marking " << fn->get_name() << " as injective\n";); m_map.insert(fn, inv); } }