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.

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 test depends on generated names.

Fixes cvc5/cvc5#12912.

🤖 Generated with Claude Code