Skip to content

Commit bdee518

Browse files
shigoelclaude
shigoel
and
claude
authored
Use globally unique bound variable names in SMT encoding (#681)
## Summary - Always generate `$__bv{N}` names for quantifier-bound variables instead of reusing user-provided names - This guarantees globally unique bound variable names across all quantifiers. By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 41ae0c1 commit bdee518

2 files changed

Lines changed: 22 additions & 20 deletions

File tree

‎Strata/Languages/Core/SMTEncoder.lean‎

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -274,11 +274,7 @@ partial def toSMTTerm (E : Env) (bvs : BoundVars) (e : LExpr CoreLParams.mono) (
274274
-- Generate base name using global counter to ensure uniqueness across terms.
275275
-- The `$__` prefix is reserved for internal use and cannot appear in user
276276
-- identifiers (see `Strata.DL.Lambda.LState.EvalConfig.varPrefix`).
277-
let (baseName, startSuffix) :=
278-
if name.isEmpty then
279-
(s!"$__bv{ctx.bvCounter}", 1)
280-
else
281-
Encoder.breakDisambiguatedName name
277+
let (baseName, startSuffix) := (s!"$__bv{ctx.bvCounter}", 1)
282278
let ctx := { ctx with bvCounter := ctx.bvCounter + 1 }
283279
-- Check for clashes with existing bvars, fvars in ctx, and fvars in body
284280
let isUsed := fun candidate =>

‎StrataTest/Languages/Core/Tests/SMTEncoderTests.lean‎

Lines changed: 21 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -13,23 +13,25 @@ namespace Core
1313
open Lambda
1414
open Strata.SMT
1515

16-
/-- info: "(define-fun $__t.0 () Bool (forall ((n Int)) (exists ((m Int)) (= n m))))\n" -/
16+
/--
17+
info: "(define-fun $__t.0 () Bool (forall (($__bv0 Int)) (exists (($__bv1 Int)) (= $__bv0 $__bv1))))\n"
18+
-/
1719
#guard_msgs in
1820
#eval toSMTTermString
1921
(.quant () .all "n" (.some .int) (LExpr.noTrigger ())
2022
(.quant () .exist "m" (.some .int) (LExpr.noTrigger ())
2123
(.eq () (.bvar () 1) (.bvar () 0))))
2224

2325
/--
24-
info: "; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (exists ((i Int)) (= i x)))\n"
26+
info: "; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (exists (($__bv0 Int)) (= $__bv0 x)))\n"
2527
-/
2628
#guard_msgs in
2729
#eval toSMTTermString
2830
(.quant () .exist "i" (.some .int) (LExpr.noTrigger ())
2931
(.eq () (.bvar () 0) (.fvar () "x" (.some .int))))
3032

3133
/--
32-
info: "; f\n(declare-fun f (Int) Int)\n; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (exists ((i Int)) (! (= i x) :pattern ((f i)))))\n"
34+
info: "; f\n(declare-fun f (Int) Int)\n; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (exists (($__bv0 Int)) (! (= $__bv0 x) :pattern ((f $__bv0)))))\n"
3335
-/
3436
#guard_msgs in
3537
#eval toSMTTermString
@@ -38,7 +40,7 @@ info: "; f\n(declare-fun f (Int) Int)\n; x\n(declare-const x Int)\n(define-fun $
3840

3941

4042
/--
41-
info: "; f\n(declare-fun f (Int) Int)\n; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (exists ((i Int)) (! (= (f i) x) :pattern ((f i)))))\n"
43+
info: "; f\n(declare-fun f (Int) Int)\n; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (exists (($__bv0 Int)) (! (= (f $__bv0) x) :pattern ((f $__bv0)))))\n"
4244
-/
4345
#guard_msgs in
4446
#eval toSMTTermString
@@ -52,7 +54,7 @@ info: "; f\n(declare-fun f (Int) Int)\n; x\n(declare-const x Int)\n(define-fun $
5254
(.eq () (.app () (.fvar () "f" (.some (.arrow .int .int))) (.bvar () 0)) (.fvar () "x" (.some .int))))
5355

5456
/--
55-
info: "; f\n(declare-const f (arrow Int Int))\n; f\n(declare-fun f@1 (Int) Int)\n; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (exists ((i Int)) (! (= (f@1 i) x) :pattern (f))))\n"
57+
info: "; f\n(declare-const f (arrow Int Int))\n; f\n(declare-fun f@1 (Int) Int)\n; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (exists (($__bv0 Int)) (! (= (f@1 $__bv0) x) :pattern (f))))\n"
5658
-/
5759
#guard_msgs in
5860
#eval toSMTTermString
@@ -68,7 +70,7 @@ info: "; f\n(declare-const f (arrow Int Int))\n; f\n(declare-fun f@1 (Int) Int)\
6870
}})
6971

7072
/--
71-
info: "; f\n(declare-fun f (Int Int) Int)\n; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (forall ((m Int) (n Int)) (! (= (f n m) x) :pattern ((f n m)))))\n"
73+
info: "; f\n(declare-fun f (Int Int) Int)\n; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (forall (($__bv0 Int) ($__bv1 Int)) (! (= (f $__bv1 $__bv0) x) :pattern ((f $__bv1 $__bv0)))))\n"
7274
-/
7375
#guard_msgs in
7476
#eval toSMTTermString
@@ -86,7 +88,7 @@ info: "; f\n(declare-fun f (Int Int) Int)\n; x\n(declare-const x Int)\n(define-f
8688

8789

8890
/--
89-
info: "; f\n(declare-fun f (Int Int) Int)\n; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (forall ((m Int) (n Int)) (= (f n m) x)))\n"
91+
info: "; f\n(declare-fun f (Int Int) Int)\n; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (forall (($__bv0 Int) ($__bv1 Int)) (= (f $__bv1 $__bv0) x)))\n"
9092
-/
9193
#guard_msgs in -- No valid trigger
9294
#eval toSMTTermString
@@ -180,26 +182,28 @@ info: "; m\n(declare-const m (Array Int Int))\n(define-fun $__t.0 () (Array Int
180182
}
181183
}})
182184

183-
-- Test empty string falls back to generated names
185+
-- Test that all bound variables get globally unique generated names
184186
/-- info: "(define-fun $__t.0 () Bool (forall (($__bv0 Int)) (exists (($__bv1 Int)) (= $__bv0 $__bv1))))\n" -/
185187
#guard_msgs in
186188
#eval toSMTTermString
187189
(.quant () .all "" (.some .int) (LExpr.noTrigger ())
188190
(.quant () .exist "" (.some .int) (LExpr.noTrigger ())
189191
(.eq () (.bvar () 1) (.bvar () 0))))
190192

191-
-- Test name clash between two nested quantifiers with same name
192-
-- Expected: Inner x should be disambiguated to x@1
193-
/-- info: "(define-fun $__t.0 () Bool (forall ((x Int)) (exists ((x@1 Int)) (= x x@1))))\n" -/
193+
-- Test nested quantifiers with same user name both get unique $__bv names
194+
/--
195+
info: "(define-fun $__t.0 () Bool (forall (($__bv0 Int)) (exists (($__bv1 Int)) (= $__bv0 $__bv1))))\n"
196+
-/
194197
#guard_msgs in
195198
#eval toSMTTermString
196199
(.quant () .all "x" (.some .int) (LExpr.noTrigger ())
197200
(.quant () .exist "x" (.some .int) (LExpr.noTrigger ())
198201
(.eq () (.bvar () 1) (.bvar () 0))))
199202

200-
-- Test x, x, x@1 scenario: nested quantifiers both named "x", then bvar named "x@1"
201-
-- Expected: outer x stays x, inner x becomes x@1, bvar "x@1" becomes x@2
202-
/-- info: "(define-fun $__t.0 () Bool (forall ((x Int) (x@1 Int) (x@2 Int)) (= x@2 x)))\n" -/
203+
-- Test triply nested quantifiers all get distinct $__bv names regardless of user names
204+
/--
205+
info: "(define-fun $__t.0 () Bool (forall (($__bv0 Int) ($__bv1 Int) ($__bv2 Int)) (= $__bv2 $__bv0)))\n"
206+
-/
203207
#guard_msgs in
204208
#eval toSMTTermString
205209
(.quant () .all "x" (.some .int) (LExpr.noTrigger ())
@@ -208,7 +212,9 @@ info: "; m\n(declare-const m (Array Int Int))\n(define-fun $__t.0 () (Array Int
208212
(.eq () (.bvar () 0) (.bvar () 2)))))
209213

210214

211-
/-- info: "; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (forall ((x@1 Int)) (= x@1 x)))\n" -/
215+
/--
216+
info: "; x\n(declare-const x Int)\n(define-fun $__t.0 () Bool (forall (($__bv0 Int)) (= $__bv0 x)))\n"
217+
-/
212218
#guard_msgs in
213219
#eval toSMTTermString
214220
(.quant () .all "x" (.some .int) (LExpr.noTrigger ())

0 commit comments

Comments
 (0)