diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt index aae8227e4c7..f966e49ea05 100644 --- a/src/ast/simplifiers/CMakeLists.txt +++ b/src/ast/simplifiers/CMakeLists.txt @@ -15,6 +15,7 @@ z3_add_component(simplifiers elim_unconstrained.cpp eliminate_predicates.cpp euf_completion.cpp + expand_records.cpp extract_eqs.cpp factor_simplifier.cpp fold_unfold.cpp @@ -39,6 +40,7 @@ z3_add_component(simplifiers blast_term_ite_simplifier.h elim_bounds.h elim_term_ite.h + expand_records.h pull_nested_quantifiers.h push_ite.h randomizer.h diff --git a/src/ast/simplifiers/expand_records.cpp b/src/ast/simplifiers/expand_records.cpp new file mode 100644 index 00000000000..850328e84f9 --- /dev/null +++ b/src/ast/simplifiers/expand_records.cpp @@ -0,0 +1,101 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + expand_records.cpp + +Abstract: + + See expand_records.h. + +Author: + + Lev Nachmanson 2026-05 + +--*/ + +#include "ast/ast_pp.h" +#include "ast/ast_util.h" +#include "ast/expr_substitution.h" +#include "ast/for_each_expr.h" +#include "ast/rewriter/expr_replacer.h" +#include "ast/simplifiers/expand_records.h" + + +void expand_records_simplifier::reduce() { + if (!m_enabled) + return; + + m_fmls.freeze_suffix(); + + // Collect candidate free constants. + obj_hashtable seen_vars; + ptr_vector vars; + expr_mark visited; + + auto visit = [&](expr* e) { + if (!is_uninterp_const(e)) + return; + if (seen_vars.contains(e)) + return; + if (!is_expandable(e->get_sort())) + return; + // Skip frozen symbols (e.g., introduced by other simplifiers, or + // symbols that other modules rely on being preserved verbatim). + if (m_fmls.frozen(to_app(e)->get_decl())) + return; + seen_vars.insert(e); + vars.push_back(to_app(e)); + }; + + for (unsigned i : indices()) { + for (expr* t : subterms::all(expr_ref(m_fmls[i].fml(), m), nullptr, &visited)) + visit(t); + } + + if (vars.empty()) + return; + + // Build the substitution v -> (c v!f1 ... v!fn). + scoped_ptr subst = alloc(expr_substitution, m); + expr_ref_vector pinned(m); + + for (app* v : vars) { + sort* s = v->get_sort(); + func_decl* ctor = m_dt.get_datatype_constructors(s)->get(0); + auto const* accs = m_dt.get_constructor_accessors(ctor); + expr_ref_vector args(m); + std::string base = v->get_decl()->get_name().str(); + for (func_decl* acc : *accs) { + std::string nm = base + "!" + acc->get_name().str(); + app* fresh = m.mk_fresh_const(nm.c_str(), acc->get_range()); + args.push_back(fresh); + } + expr_ref new_val(m.mk_app(ctor, args.size(), args.data()), m); + pinned.push_back(new_val); + subst->insert(v, new_val); + TRACE(expand_records, + tout << mk_pp(v, m) << " -> " << mk_pp(new_val, m) << "\n";); + } + + // Apply the substitution and rewrite. + scoped_ptr rp = mk_default_expr_replacer(m, false); + rp->set_substitution(subst.get()); + + vector old_fmls; + for (unsigned i : indices()) { + auto [f, p, d] = m_fmls[i](); + auto [g, dep2] = rp->replace_with_dep(f); + expr_ref tmp(m); + m_rewriter(g, tmp); + if (tmp == f) + continue; + expr_dependency_ref new_dep(m.mk_join(d, dep2), m); + old_fmls.push_back(m_fmls[i]); + m_fmls.update(i, dependent_expr(m, tmp, nullptr, new_dep)); + } + + if (!old_fmls.empty()) + m_fmls.model_trail().push(subst.detach(), old_fmls, false); +} diff --git a/src/ast/simplifiers/expand_records.h b/src/ast/simplifiers/expand_records.h new file mode 100644 index 00000000000..fcb8236abfd --- /dev/null +++ b/src/ast/simplifiers/expand_records.h @@ -0,0 +1,63 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + expand_records.h + +Abstract: + + Expand free constants of single-constructor algebraic datatype sort + (a.k.a. records) into applications of that constructor over fresh + variables. For a free constant v : T where T has the single + constructor c(f1:T1, ..., fn:Tn), introduce fresh constants + v!f1 : T1, ..., v!fn : Tn and substitute v -> (c v!f1 ... v!fn). + + After the substitution, every accessor application (fi v) collapses + via standard datatype simplification to v!fi. This enables solve-eqs + and arithmetic preprocessing to operate on the field variables + directly, which in turn enables more aggressive constant folding. + +Author: + + Lev Nachmanson 2026-05 + +--*/ +#pragma once + +#include "ast/datatype_decl_plugin.h" +#include "ast/rewriter/th_rewriter.h" +#include "ast/simplifiers/dependent_expr_state.h" + + +class expand_records_simplifier : public dependent_expr_simplifier { + datatype_util m_dt; + th_rewriter m_rewriter; + bool m_enabled = true; + + bool is_expandable(sort* s) { + if (!m_dt.is_datatype(s)) + return false; + if (m_dt.is_recursive(s)) + return false; + auto const* ctors = m_dt.get_datatype_constructors(s); + return ctors && ctors->size() == 1; + } + +public: + expand_records_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls): + dependent_expr_simplifier(m, fmls), m_dt(m), m_rewriter(m, p) {} + + char const* name() const override { return "expand-records"; } + + void reduce() override; + + void updt_params(params_ref const& p) override { + m_rewriter.updt_params(p); + m_enabled = p.get_bool("expand_records", true); + } +}; + +/* + ADD_SIMPLIFIER("expand-records", "expand single-constructor datatype constants.", "alloc(expand_records_simplifier, m, p, s)") +*/ diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp index 32b8bb9b65f..6165ed4ee83 100644 --- a/src/solver/assertions/asserted_formulas.cpp +++ b/src/solver/assertions/asserted_formulas.cpp @@ -19,6 +19,7 @@ Revision History: #include "util/warning.h" #include "ast/ast_ll_pp.h" #include "ast/ast_pp.h" +#include "ast/datatype_decl_plugin.h" #include "ast/for_each_expr.h" #include "ast/well_sorted.h" #include "ast/rewriter/rewriter_def.h" @@ -281,6 +282,8 @@ void asserted_formulas::reduce() { IF_VERBOSE(10, verbose_stream() << "(smt.simplify-begin :num-exprs " << get_total_size() << ")\n";); set_eliminate_and(false); // do not eliminate and before nnf. + expand_records(); + if (inconsistent()) return; if (!invoke(m_propagate_values)) return; if (!invoke(m_find_macros)) return; if (!invoke(m_nnf_cnf)) return; @@ -535,6 +538,70 @@ void asserted_formulas::commit(unsigned new_qhead) { m_qhead = new_qhead; } +void asserted_formulas::expand_records() { + if (m.proofs_enabled()) + return; + if (inconsistent()) + return; + + datatype_util dt(m); + obj_hashtable seen; + ptr_vector vars; + expr_mark visited; + + auto is_expandable = [&](sort* s) { + if (!dt.is_datatype(s)) + return false; + if (dt.is_recursive(s)) + return false; + auto const* ctors = dt.get_datatype_constructors(s); + return ctors && ctors->size() == 1; + }; + + for (unsigned i = m_qhead; i < m_formulas.size(); ++i) { + for (expr* t : subterms::all(expr_ref(m_formulas[i].fml(), m), nullptr, &visited)) { + if (!is_uninterp_const(t)) + continue; + if (seen.contains(t)) + continue; + if (!is_expandable(t->get_sort())) + continue; + seen.insert(t); + vars.push_back(to_app(t)); + } + } + + if (vars.empty()) + return; + + flush_cache(); + expr_ref_vector pinned(m); + expr_ref_vector defining_eqs(m); + for (app* v : vars) { + sort* s = v->get_sort(); + func_decl* ctor = dt.get_datatype_constructors(s)->get(0); + auto const* accs = dt.get_constructor_accessors(ctor); + expr_ref_vector args(m); + std::string base = v->get_decl()->get_name().str(); + for (func_decl* acc : *accs) { + std::string nm = base + "!" + acc->get_name().str(); + args.push_back(m.mk_fresh_const(nm.c_str(), acc->get_range())); + } + expr_ref new_val(m.mk_app(ctor, args.size(), args.data()), m); + pinned.push_back(new_val); + TRACE(expand_records, + tout << mk_pp(v, m) << " -> " << mk_pp(new_val, m) << "\n";); + m_scoped_substitution.insert(v, new_val, nullptr); + defining_eqs.push_back(m.mk_eq(v, new_val)); + } + + // Apply the substitution to existing assertions. + if (!invoke(m_reduce_asserted_formulas)) + return; + (void)defining_eqs; + flush_cache(); +} + void asserted_formulas::propagate_values() { if (m.proofs_enabled()) return; diff --git a/src/solver/assertions/asserted_formulas.h b/src/solver/assertions/asserted_formulas.h index 262499ff44a..205e76fcac4 100644 --- a/src/solver/assertions/asserted_formulas.h +++ b/src/solver/assertions/asserted_formulas.h @@ -228,6 +228,8 @@ class asserted_formulas { void force_push(); void push_scope_core(); + void expand_records(); + bool invoke(simplify_fmls& s); void swap_asserted_formulas(vector& new_fmls); void push_assertion(expr * e, proof * pr, vector& result); diff --git a/src/solver/solver_preprocess.cpp b/src/solver/solver_preprocess.cpp index e91c63d79c1..f6be2350fc5 100644 --- a/src/solver/solver_preprocess.cpp +++ b/src/solver/solver_preprocess.cpp @@ -30,6 +30,7 @@ Module Name: #include "ast/simplifiers/bv_slice.h" #include "ast/simplifiers/eliminate_predicates.h" #include "ast/simplifiers/elim_unconstrained.h" +#include "ast/simplifiers/expand_records.h" #include "ast/simplifiers/pull_nested_quantifiers.h" #include "ast/simplifiers/distribute_forall.h" #include "ast/simplifiers/refine_inj_axiom.h" @@ -60,6 +61,7 @@ void init_preprocess(ast_manager& m, params_ref const& p, then_simplifier& s, de }; smt_params smtp(p); s.add_simplifier(alloc(rewriter_simplifier, m, p, st)); + s.add_simplifier(alloc(expand_records_simplifier, m, p, st)); if (smtp.m_propagate_values) s.add_simplifier(alloc(propagate_values, m, p, st)); if (smtp.m_solve_eqs) s.add_simplifier(alloc(euf::solve_eqs, m, st)); if (smtp.m_elim_unconstrained) s.add_simplifier(alloc(elim_unconstrained, m, st)); diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index 02e62aec0db..8d4a02585c3 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -34,6 +34,7 @@ z3_add_component(core_tactics elim_uncnstr_tactic.h elim_uncnstr2_tactic.h eliminate_predicates_tactic.h + expand_records_tactic.h fold_unfold_tactic.h injectivity_tactic.h nnf_tactic.h diff --git a/src/tactic/core/expand_records_tactic.h b/src/tactic/core/expand_records_tactic.h new file mode 100644 index 00000000000..002b3561f33 --- /dev/null +++ b/src/tactic/core/expand_records_tactic.h @@ -0,0 +1,47 @@ +/*++ +Copyright (c) 2026 Microsoft Corporation + +Module Name: + + expand_records_tactic.h + +Author: + + Lev Nachmanson 2026-05 + +Tactic Documentation: + +## Tactic expand-records + +### Short Description + +Replace every free constant of a single-constructor algebraic datatype +sort with the corresponding constructor applied to fresh field +variables. For example, `(declare-fun p () Pair)` with the single +constructor `mk-pair(first:Int, second:Int)` is replaced by the +substitution `p -> (mk-pair p!first p!second)` for fresh `p!first` and +`p!second`. + +After the rewrite, accessor applications `(first p)`, `(second p)` +collapse to the corresponding field variables, allowing subsequent +solve-eqs and arithmetic simplification to make better use of constant +folding. + +--*/ +#pragma once + +#include "util/params.h" +#include "tactic/tactic.h" +#include "tactic/dependent_expr_state_tactic.h" +#include "ast/simplifiers/expand_records.h" + +inline tactic * mk_expand_records_tactic(ast_manager & m, params_ref const & p = params_ref()) { + return alloc(dependent_expr_state_tactic, m, p, + [](auto& mm, auto& pp, auto &ss) -> dependent_expr_simplifier* { + return alloc(expand_records_simplifier, mm, pp, ss); + }); +} + +/* + ADD_TACTIC("expand-records", "expand single-constructor datatype constants.", "mk_expand_records_tactic(m, p)") +*/ diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index 883cacdab6c..f620d912165 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -17,6 +17,7 @@ Module Name: --*/ #include "tactic/portfolio/default_tactic.h" +#include "tactic/core/expand_records_tactic.h" #include "tactic/core/simplify_tactic.h" #include "tactic/smtlogics/qfbv_tactic.h" #include "tactic/smtlogics/qflia_tactic.h" @@ -35,6 +36,8 @@ Module Name: tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params(and_then(mk_simplify_tactic(m, p), + mk_expand_records_tactic(m, p), + mk_simplify_tactic(m, p), cond(mk_and(mk_is_propositional_probe(), mk_not(mk_produce_proofs_probe())), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_fd_tactic(m, p); }), cond(mk_is_qfbv_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfbv_tactic(m, p); }), diff --git a/src/util/trace_tags.def b/src/util/trace_tags.def index 67adb62c986..2fc215fb590 100644 --- a/src/util/trace_tags.def +++ b/src/util/trace_tags.def @@ -70,6 +70,8 @@ X(eq_der, top_sort, "top sort") X(expr_substitution_simplifier, expr_substitution_simplifier, "expr substitution simplifier") X(expr_substitution_simplifier, propagate_values, "propagate values") +X(expand_records, expand_records, "expand records simplifier") + X(finite_set, finite_set, "finite set") X(fm_model_converter, fm_model_converter, "fm model converter")