From b3bc16f2b99681aedbfe895f5aa7afead9aaad4e Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Fri, 4 Sep 2026 16:40:38 -0500 Subject: [PATCH] Make fresh names unique across sorts next_fresh checked (name, sort) against ctx.vars and only advanced its counter on a collision, so a name was 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() then 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. Track the names in use in ctx.var_names and check that instead, and advance the counter on every call so a number is never handed out twice. Mixing prefixes now skips numbers, which is what z3 does. 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. The new test covers the report and the helpers around it. Every line of its output but one changes without the fix: the constants collide as above, and FreshBool and FreshReal are handed the same name too, since both default to the "b" prefix and only the counter separates them. Fixes cvc5/cvc5#12912. Co-Authored-By: Claude Opus 5 --- cvc5_pythonic_api/cvc5_pythonic.py | 28 +++++++++++++---------- test/pgm_outputs/fresh.py.out | 7 ++++++ test/pgms/fresh.py | 36 ++++++++++++++++++++++++++++++ 3 files changed, 59 insertions(+), 12 deletions(-) create mode 100644 test/pgm_outputs/fresh.py.out create mode 100644 test/pgms/fresh.py diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py index 3fda95b..18188e9 100644 --- a/cvc5_pythonic_api/cvc5_pythonic.py +++ b/cvc5_pythonic_api/cvc5_pythonic.py @@ -148,6 +148,9 @@ def __init__(self): self.tm = pc.TermManager() # Map from (name, sort) pairs to constant terms self.vars = {} + # The names of all constants created so far. Names are unique across + # sorts, since a name is all that identifies a constant when printing. + self.var_names = set() # An increasing identifier used to make fresh identifiers self.next_fresh_var = 0 @@ -164,16 +167,20 @@ def get_var(self, name, sort): """ if (name, sort) not in self.vars: self.vars[(name, sort)] = self.tm.mkConst(sort.ast, name) + self.var_names.add(name) return self.vars[(name, sort)] - def next_fresh(self, sort, prefix): - """Make a name such that (name, sort) is fresh. + def next_fresh(self, prefix): + """Make a name that no constant uses, prefixed by `prefix`. - The name will be prefixed by `prefix`""" + The name is fresh regardless of sort: two constants sharing a name are + indistinguishable once printed, even when their sorts differ.""" name = "{}{}".format(prefix, self.next_fresh_var) - while (name, sort) in self.vars: + while name in self.var_names: self.next_fresh_var += 1 name = "{}{}".format(prefix, self.next_fresh_var) + # Never hand out this number again, whatever sort the caller uses it at + self.next_fresh_var += 1 return name def __eq__(self, o): @@ -1127,7 +1134,7 @@ def FreshFunction(*sig): if debugging(): _assert(is_sort(rng), "SMT sort expected") ctx = rng.ctx - name = ctx.next_fresh(_to_function_sort(ctx, sig), "freshfn") + name = ctx.next_fresh("freshfn") return Function(name, *sig) @@ -1500,7 +1507,7 @@ def FreshConst(sort, prefix="c"): False """ ctx = sort.ctx - name = ctx.next_fresh(sort, prefix) + name = ctx.next_fresh(prefix) return Const(name, sort) @@ -1877,8 +1884,7 @@ def FreshBool(prefix="b", ctx=None): False """ ctx = _get_ctx(ctx) - sort = BoolSort(ctx) - name = ctx.next_fresh(sort, prefix) + name = ctx.next_fresh(prefix) return Bool(name, ctx) @@ -3867,8 +3873,7 @@ def FreshInt(prefix="x", ctx=None): Int """ ctx = _get_ctx(ctx) - sort = IntSort(ctx) - name = ctx.next_fresh(sort, prefix) + name = ctx.next_fresh(prefix) return Int(name, ctx) @@ -3927,8 +3932,7 @@ def FreshReal(prefix="b", ctx=None): Real """ ctx = _get_ctx(ctx) - sort = RealSort(ctx) - name = ctx.next_fresh(sort, prefix) + name = ctx.next_fresh(prefix) return Real(name, ctx) diff --git a/test/pgm_outputs/fresh.py.out b/test/pgm_outputs/fresh.py.out new file mode 100644 index 0000000..b705ea9 --- /dev/null +++ b/test/pgm_outputs/fresh.py.out @@ -0,0 +1,7 @@ +c0 c1 c2 +(and (fp.isNormal c0) (fp.isNormal c1) (fp.isSubnormal c2) (fp.isNormal (fp.add roundTowardZero (fp.mul roundTowardZero ((_ to_fp 8 24) roundTowardZero c0) ((_ to_fp 8 24) roundTowardZero c1)) c2))) +False False False +b3 x4 b5 c6 +freshfn7 +test8 test9 +b11 diff --git a/test/pgms/fresh.py b/test/pgms/fresh.py new file mode 100644 index 0000000..954014e --- /dev/null +++ b/test/pgms/fresh.py @@ -0,0 +1,36 @@ +from cvc5_pythonic_api import * + +# A fresh name is fresh across sorts, not just within one. Sharing a name +# with a constant of another sort would make the two indistinguishable once +# printed, and the assertions below unparseable: the name would appear +# applied at both sorts, which no set of declarations can typecheck. +a = FreshConst(Float16()) +b = FreshConst(Float16()) +c = FreshConst(Float32()) +print(a, b, c) + +s = Solver() +s.add(fpIsNormal(a)) +s.add(fpIsNormal(b)) +s.add(fpIsSubnormal(c)) +ab = fpMul(RTZ(), fpToFP(RTZ(), a, Float32()), fpToFP(RTZ(), b, Float32())) +s.add(fpIsNormal(fpAdd(RTZ(), ab, c))) +print(s.sexpr()) + +# Distinct terms, whatever they are called. +print(a.eq(b), a.eq(c), b.eq(c)) + +# The other Fresh* helpers draw from the same counter, so a name minted by +# one is never handed out by another. FreshBool and FreshReal both default +# to the "b" prefix, so nothing but the counter keeps them apart. +print(FreshBool(), FreshInt(), FreshReal(), FreshConst(IntSort())) +print(FreshFunction(IntSort(), IntSort())) + +# The prefix is honored, and a number is never reused within one either. +print(FreshConst(BoolSort(), prefix="test"), FreshConst(BoolSort(), prefix="test")) + +# A declared constant blocks its name for every sort, not just its own: the +# counter has reached 10 by now, so the fresh Bool below skips the name an +# Int already holds. +Int("b10") +print(FreshBool())