Fix #9171: add expand-records preprocessing to enable constant folding

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

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<expr> seen_vars;
+    ptr_vector<app>     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<expr_substitution> 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<expr_replacer> rp = mk_default_expr_replacer(m, false);
+    rp->set_substitution(subst.get());
+
+    vector<dependent_expr> 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);
+}

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)")
+*/

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<expr> seen;
+    ptr_vector<app> 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;

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<justified_expr>& new_fmls);
     void push_assertion(expr * e, proof * pr, vector<justified_expr>& result);

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));

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

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)")
+*/

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); }),

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")