Make fresh names unique across sorts

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)
 
 

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

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())