Make fresh names unique across sorts

[daniel-larraz]

next_fresh checked (name, sort) against ctx.vars and only advanced its counter on a collision, so a name counted as free as long as no constant of that same sort held it. Two FreshConst calls at different sorts could therefore be handed the same name:

a = FreshConst(Float16())   # c0
b = FreshConst(Float16())   # c1, after colliding on (c0, Float16)
c = FreshConst(Float32())   # c1 again -- (c1, Float32) is not in vars

The terms stay distinct, so solving is unaffected, but a name is all that identifies a constant once printed. sexpr() renders b and c alike, and the result is not merely ambiguous — c1 appears applied at both Float16 and Float32, so no set of declarations could make it parse back:

(and (fp.isNormal c0) (fp.isNormal c1) (fp.isSubnormal c1) (fp.isNormal (fp.add ... c1)))

This tracks the names in use in ctx.var_names and checks that instead, and advances the counter on every call so a number is never handed out twice. The same script now prints:

(and (fp.isNormal c0) (fp.isNormal c1) (fp.isSubnormal c2) (fp.isNormal (fp.add ... c2)))

FreshBool, FreshInt, FreshReal and FreshFunction were affected the same way and are covered by the same fix.

The sort argument is gone from next_fresh and its callers. It was doing no work in FreshFunction either, which passed a raw cvc5 Sort where the others passed a SortRef, so that lookup could never have matched a vars entry keyed the other way.

Test

test/pgms/fresh.py covers the report and the helpers around it. Every line of its output but one changes without the fix:

 c0 c1 c2            ->  c0 c1 c1     # the report
 b3 x4 b5 c6         ->  b1 x1 b1 c1  # FreshBool/FreshInt/FreshReal/FreshConst
 freshfn7            ->  freshfn1
 test8 test9         ->  test1 test2
 b11                 ->  b2

FreshBool and FreshReal both default to the "b" prefix, so only the counter separates them — hence the two b1s on the second line. The last line checks that a name held by a declared constant is skipped even when the fresh constant is asked for at a different sort.

One behavioral note for reviewers: the counter is shared across prefixes, so mixing them now skips numbers — FreshBool() after two FreshConst() calls gives b2, not b0. z3 behaves the same way, and no existing test depends on generated names.

Fixes cvc5/cvc5#12912.

🤖 Generated with Claude Code

[alex-ozdemir]

LGTM