SMT encoder: opt-in define-fun-rec for recursive functions

[kondylidou]

Recursive functions are encoded as uninterpreted functions with per-constructor
axioms. Good for proving, but the solver cannot evaluate them during model
search, so a false obligation whose counterexample must be computed through
the function returns unknown.

This adds two options, both default off:

• VerifyOptions.recursiveFnsAsDefineFunRec: emit the body as define-fun-rec
  and skip the axioms. With cvc5's fmf-fun the solver then finds concrete
  constructor terms.
• VerifyOptions.obligationsToVerify: discharge only the listed obligations
  (no solver call, no result for the others). Lets a client re-query just the
  obligations a first pass left unknown, so the weaker proving mode never
  touches the rest. Mirrors proceduresToVerify, at discharge level.

Follow-up to #1432, which made define-fun-rec the default and was withdrawn.
Here the axiom encoding stays the default. The July comparison ran without
fmf-fun, which is why both encodings looked the same then.

Changes

• Term.IF.isRec, SMT.Context.recFnsAsDefineFunRec.
• Both encoders register the function name before encoding its body, so the
  self-call resolves to it instead of declaring an uninterpreted twin.
• AbstractSolver.defineFunRec, for IncrementalSolver and SolverM.
• Self-recursive only; mutual recursion under the option is an error.
• Obligation filter in the discharge loop of Core.verify.

Test (DefineFunRecTests.lean): binary nat, obligation
toInt(a) = 73 ∧ toInt(a + b) = 200 ⊢ toInt(b) = 0, false with b = 127.
11 obligations: 9 library proof obligations + the false one (assert, ensures).

encoding	proof obligations	false obligation
default	9 pass	unknown, candidate a=2 b=3
define-fun-rec	9 pass	timeout
define-fun-rec + fmf-fun	7 pass, 2 unknown	fail, a = 73, b = 127
same, obligationsToVerify = [b_is_zero]	skipped	fail, a = 73, b = 127

Row 2: the encoding alone does not regress proving. Row 3: fmf-fun weakens
proving, hence row 4 is the intended client pattern (Strata-Boole side, cvc5
only).

Default behaviour unchanged; full StrataTest passes.

🤖 Generated with Claude Code

[kondylidou]

@shigoel

[joscoh]

I understand why this is used for the define-fun-rec example, but is the intended use case that a user gets the unknown proof obligations, then calls strata again passing in those obligations by name? This does not seem like an ideal workflow.

[kondylidou]

The caller isn't a person, it's a dialect front-end: Boole's verify takes the
labels that came back unknown from the results it already has and re-runs only
those under a model-finding configuration. No label is typed by hand.

The objection still lands, the field is a mechanism with the policy left to
every caller, and a caller that gets it wrong is unsound. If you'd rather Strata
owned the loop, I'm happy to move it upstream; one constraint to know is that our
retry also substitutes a different nat encoding, so it re-verifies a different
program, not the same one under different options.

[kondylidou]

@shigoel @atomb can I get another approval here please? :D :D