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

[levnach]

Fixes #9171.

Problem

Issue #9171 ships an SMT-LIB2 benchmark that declares a single-constructor Rat algebraic datatype and asserts a pile of non-linear Int constraints over the selectors (num x)/(den x). The problem is unsatisfiable just by literal-by-literal arithmetic constant folding, but Z3 was diverging — and for some random seeds it diverged even on builds from early March.

Root causes:

1. solve-eqs only substitutes uninterpreted constants. In extract_eqs.cpp / solve_eqs.cpp the predicate can_be_var(e) requires is_uninterp_const(e). Selector applications like (num x) are not uninterpreted constants, so equalities like (= (num x) 7) were never propagated. The variables of interest were hidden behind datatype selectors and the existing constant folding machinery never saw them as raw integer variables.
2. Tactic dispatch saw the un-simplified syntax. default_tactic.cpp picks a sub-tactic based on probes over the original formula. Because the formula mentions a datatype (Rat), the dispatcher chose the heavyweight smt sub-tactic (theory_arith + nlsat), which loops on this nonlinear input. The trivial qfnia-tactic (bit-blast) would have solved it instantly, but the dispatcher never saw the QF_NIA-shaped formula.

Fix

Introduces an expand-records preprocessing step that rewrites every free constant whose sort is a non-recursive single-constructor algebraic datatype into the constructor applied to fresh field constants, e.g.

x : Rat   ->   x  :=  (mk-rat x!num x!den)

Subsequent simplification rewrites (num (mk-rat x!num x!den)) to x!num, etc. After the rewrite, the formula no longer mentions the datatype at all — it is pure non-linear integer arithmetic over the fresh field constants, and the existing arithmetic rewriter and solve-eqs finish the job immediately.

Guards: only non-recursive single-constructor datatypes are expanded (prevents infinite expansion on lists, trees, etc.).

Model preservation: the substitution is pushed onto the model trail so models for the original datatype-typed constant can be reconstructed.

Wiring

The transformation is wired into all three preprocessing entry points so it applies regardless of which path the user takes:

• init_preprocess (src/solver/solver_preprocess.cpp) — modern simplifier_solver path (e.g. when (set-simplifier …) is used).
• asserted_formulas::reduce (src/solver/assertions/asserted_formulas.{h,cpp}) — legacy SMT context path.
• default_tactic (src/tactic/portfolio/default_tactic.cpp) — inserted into the and_then(...) chain before the logic-class cond probes, so the dispatcher sees the post-expansion formula and routes to qfnia-tactic. This is the critical piece for the user-visible (check-sat) path.

Files

New:

• src/ast/simplifiers/expand_records.{h,cpp} — the dependent_expr_simplifier.
• src/tactic/core/expand_records_tactic.h — thin dependent_expr_state_tactic wrapper registered as expand-records.

Modified:

• src/ast/simplifiers/CMakeLists.txt, src/tactic/core/CMakeLists.txt — register new sources/headers.
• src/solver/solver_preprocess.cpp — hook into init_preprocess.
• src/solver/assertions/asserted_formulas.{h,cpp} — expand_records() step at the start of reduce().
• src/tactic/portfolio/default_tactic.cpp — insert expand-records + simplify before the logic-class probes.
• src/util/trace_tags.def — register expand_records trace tag (needed for the debug build's TRACE(...) macro check).

Verification

• Original benchmark from Regression in a constant-folding example #9171: now solves as unsat in ~0.14s on the release build (previously diverged).
• Unit tests: 89/90 pass on both release and debug builds. The single failing test, tptp, fails identically on unmodified master — pre-existing, unrelated to this change.

cc @NikolajBjorner — could you review please?