feat(SMT): avoid redundant reset, globally unique quantified var names, more smtReservedKeywords

Strata/DL/SMT/Encoder.lean

@@ -31,11 +31,11 @@ The encoding pipeline has two layers:
 2. **Encoder layer** (`EncoderM`): Sits on top of `SolverM` and manages
    A-normal form decomposition purely in the `Term` domain:
    - **Term → abbreviated Term cache** (`terms`): Maps each `Term` to its
-     abbreviated `Term.var` reference (e.g., a variable named `t0`, `t1`).
+     abbreviated `Term.var` reference (e.g., a variable named `$__t.0`, `$__t.1`).
      Large terms are broken into small `define-fun` definitions with short
      names, and the Solver handles all `Term → String` conversion.
    - **UF → abbreviated name cache** (`ufs`): Maps uninterpreted functions to
-     their abbreviated identifiers (e.g., `f0`, `f1`).
+     their abbreviated identifiers (e.g., `$__f.0`, `$__f.1`).
 
 The Encoder works purely with `Term` values. The `SolverM` layer handles all
 string conversion and caching when emitting commands.
@@ -72,10 +72,10 @@ open Solver
 public section
 
 structure EncoderState where
-  /-- Maps a `Term` to its abbreviated `Term` (a `Term.var` with name like `t0`).
+  /-- Maps a `Term` to its abbreviated `Term` (a `Term.var` with name like `$__t.0`).
       This is a cache after converting terms to A-Normal Form. -/
   terms : Std.HashMap Term Term
-  /-- Maps a `UF` to its abbreviated SMT identifier (e.g., `f0`, `f1`). -/
+  /-- Maps a `UF` to its abbreviated SMT identifier (e.g., `$__f.0`, `$__f.1`). -/
   ufs   : Std.HashMap UF String
 
 def EncoderState.init : EncoderState where
@@ -94,10 +94,23 @@ def smtReservedKeywords : List String :=
   -- SMT-LIB reserved words from the DDM parser
   let parserKeywords := _root_.Strata.reservedKeywords.map (·.2)
   -- Additional keywords not in the parser list
-  parserKeywords ++ ["select", "store", "and", "or", "not", "ite",
-   "true", "false", "Int", "Bool", "Real", "Array", "BitVec",
-   -- Theory function symbols that cvc5 disallows shadowing
-   "abs", "mod", "div", "to_real", "to_int", "is_int"]
+  parserKeywords ++
+   ["true", "false", "Int", "Bool", "Real", "Array", "BitVec",
+   -- Core theory symbols
+   "abs", "and", "distinct", "/", "=", ">", ">=", "ite", "=>",
+   "div", "is_int", "<", "<=", "-", "mod", "*", "not", "or", "+",
+   "to_int", "to_real", "xor",
+   -- String theory symbols
+   "str.at", "str.++", "str.contains", "str.from_code", "str.from_int",
+   "str.in_re", "str.indexof", "str.is_digit", "str.<=", "str.len",
+   "str.<", "str.prefixof", "str.replace", "str.substr", "str.suffixof",
+   "str.to_code", "str.to_int", "str.to_re",
+   -- Regex theory symbols
+   "re.*", "re.+", "re.opt", "re.++", "re.union", "re.inter", "re.diff",
+   "re.comp", "re.loop", "re.^", "re.range", "re.none", "re.all",
+   "re.allchar",
+   -- Array theory symbols
+   "select", "store"]
 
 /-- Generate a disambiguated name by appending @suffix -/
 def disambiguateName (baseName : String) (suffix : Nat) : String :=
@@ -133,8 +146,12 @@ def findUniqueName (baseName : String) (startSuffix : Nat) (isUsed : String →
     omega
   loop (if startSuffix == 1 then baseName else disambiguateName baseName (startSuffix - 1)) startSuffix limit
 
-def termId (n : Nat)                    : String := s!"t{n}"
-def ufId (n : Nat)                      : String := s!"f{n}"
+/-- The `$__` prefix is reserved for internal use and cannot appear in user
+    identifiers (see `Strata.DL.Lambda.LState.EvalConfig.varPrefix`).
+    The `.` after `t`/`f` prevents collision with Lambda-generated names
+    like `$__t0` (variable `t`, index 0). -/
+def termId (n : Nat)                    : String := s!"$__t.{n}"
+def ufId (n : Nat)                      : String := s!"$__f.{n}"
 
 def termNum : EncoderM Nat := do return (← get).terms.size
 def ufNum   : EncoderM Nat := do return (← get).ufs.size
@@ -325,11 +342,8 @@ Then you can run any `SolverM` action `act` with `act |>.run solver`, where
 `solver` is a `Solver` instance you can construct using functions in
 Solver.lean.
 
-Note that `encode` itself first resets the solver in order to define datatypes
-etc.
 -/
 def encode (ts : List Term) : SolverM Unit := do
-  Solver.reset
   Solver.setLogic "ALL"
   Solver.declareDatatype "Option" ["X"]
     [⟨"none", []⟩, ⟨"some", [("val", .constr "X" [])]⟩]

Strata/Languages/B3/Verifier/Program.lean

@@ -176,11 +176,8 @@ Workflow:
    - If failed, automatically diagnose to find root cause
 3. Report all results with diagnosis
 
-The solver is reset at the beginning to ensure clean state.
 -/
 def programToSMT (prog : Strata.B3AST.Program SourceRange) (solver : Solver) : IO (List ProcedureReport) := do
-  -- Reset solver to clean state
-  let _ ← (Solver.reset).run solver
   let state ← buildProgramState prog solver
   let mut reportsRev := []
 

Strata/Languages/Core/SMTEncoder.lean

@@ -43,6 +43,8 @@ structure SMT.Context where
   typeFactory : @Lambda.TypeFactory CoreLParams.IDMeta := #[]
   seenDatatypes : Std.HashSet String := {}
   datatypeFuns : Map String (Op.DatatypeFuncs × LConstr CoreLParams.IDMeta) := Map.empty
+  /-- Global counter for generating unique bound variable names across all terms. -/
+  bvCounter : Nat := 0
 deriving Repr, Inhabited
 
 def SMT.Context.default : SMT.Context := {}
@@ -269,12 +271,15 @@ partial def toSMTTerm (E : Env) (bvs : BoundVars) (e : LExpr CoreLParams.mono) (
   | .quant _ _ _ .none _ _ => .error f!"Cannot encode untyped quantifier {e}"
   | .quant _ qk name (.some ty) tr e =>
     let fvarNames := (e.collectFvarNames.map (·.name)).toArray
-    -- Generate base name and extract any existing suffix
+    -- Generate base name using global counter to ensure uniqueness across terms.
+    -- The `$__` prefix is reserved for internal use and cannot appear in user
+    -- identifiers (see `Strata.DL.Lambda.LState.EvalConfig.varPrefix`).
     let (baseName, startSuffix) :=
       if name.isEmpty then
-        (s!"$__bv{bvs.length}", 1)
+        (s!"$__bv{ctx.bvCounter}", 1)
       else
         Encoder.breakDisambiguatedName name
+    let ctx := { ctx with bvCounter := ctx.bvCounter + 1 }
     -- Check for clashes with existing bvars, fvars in ctx, and fvars in body
     let isUsed := fun candidate =>
       bvs.any (fun (n, _) => n == candidate) ||

Strata/Languages/Core/Verifier.lean

@@ -47,7 +47,6 @@ def encodeCore (ctx : Core.SMT.Context) (prelude : SolverM Unit)
     (md : Imperative.MetaData Core.Expression)
     (satisfiabilityCheck validityCheck : Bool) :
     SolverM (List String × EncoderState) := do
-  Solver.reset
   Solver.setLogic "ALL"
   prelude
   let _ ← ctx.sorts.mapM (fun s => Solver.declareSort s.name s.arity)

StrataTest/DL/Imperative/SMTEncoder.lean

@@ -71,7 +71,6 @@ def ProofObligation.toSMTTerms (E : Env) (d : Imperative.ProofObligation Arith.P
   .ok (assumptions_terms ++ [obligation_term])
 
 def encodeArithToSMTTerms (ts : List Term) : SolverM (List String × EncoderState) := do
-  Solver.reset
   Solver.setLogic "ALL"
   let estate := EncoderState.init
   let (termEncs, estate) ← ts.mapM (Strata.SMT.Encoder.encodeTerm False) |>.run estate

StrataTest/Languages/Core/Tests/SMTEncoderDatatypeTest.lean

@@ -114,7 +114,7 @@ info: (declare-datatype TestOption (par (α) (
   (Some (TestOption..val |α|)))))
 ; x
 (declare-const x (TestOption Int))
-(define-fun t0 () (TestOption Int) x)
+(define-fun $__t.0 () (TestOption Int) x)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -128,7 +128,7 @@ info: (declare-datatype TestList (par (α) (
   (Cons (TestList..head |α|) (TestList..tail (TestList |α|))))))
 ; xs
 (declare-const xs (TestList Int))
-(define-fun t0 () (TestList Int) xs)
+(define-fun $__t.0 () (TestList Int) xs)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -142,7 +142,7 @@ info: (declare-datatype TestTree (par (α) (
   (Node (TestTree..value |α|) (TestTree..left (TestTree |α|)) (TestTree..right (TestTree |α|))))))
 ; tree
 (declare-const tree (TestTree Bool))
-(define-fun t0 () (TestTree Bool) tree)
+(define-fun $__t.0 () (TestTree Bool) tree)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -156,7 +156,7 @@ info: (declare-datatype TestList (par (α) (
   (Cons (TestList..head |α|) (TestList..tail (TestList |α|))))))
 ; intList
 (declare-const intList (TestList Int))
-(define-fun t0 () (TestList Int) intList)
+(define-fun $__t.0 () (TestList Int) intList)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -170,7 +170,7 @@ info: (declare-datatype TestList (par (α) (
   (Cons (TestList..head |α|) (TestList..tail (TestList |α|))))))
 ; boolList
 (declare-const boolList (TestList Bool))
-(define-fun t0 () (TestList Bool) boolList)
+(define-fun $__t.0 () (TestList Bool) boolList)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -184,7 +184,7 @@ info: (declare-datatype TestTree (par (α) (
   (Node (TestTree..value |α|) (TestTree..left (TestTree |α|)) (TestTree..right (TestTree |α|))))))
 ; intTree
 (declare-const intTree (TestTree Int))
-(define-fun t0 () (TestTree Int) intTree)
+(define-fun $__t.0 () (TestTree Int) intTree)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -201,7 +201,7 @@ info: (declare-datatype TestOption (par (α) (
   (Cons (TestList..head |α|) (TestList..tail (TestList |α|))))))
 ; listOfOption
 (declare-const listOfOption (TestList (TestOption Int)))
-(define-fun t0 () (TestList (TestOption Int)) listOfOption)
+(define-fun $__t.0 () (TestList (TestOption Int)) listOfOption)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -215,7 +215,7 @@ info: (declare-datatype TestOption (par (α) (
 info: (declare-datatype TestOption (par (α) (
   (None)
   (Some (TestOption..val |α|)))))
-(define-fun t0 () (TestOption Int) (as None (TestOption Int)))
+(define-fun $__t.0 () (TestOption Int) (as None (TestOption Int)))
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -227,7 +227,7 @@ info: (declare-datatype TestOption (par (α) (
 info: (declare-datatype TestOption (par (α) (
   (None)
   (Some (TestOption..val |α|)))))
-(define-fun t0 () (TestOption Int) ((as Some (TestOption Int)) 42))
+(define-fun $__t.0 () (TestOption Int) ((as Some (TestOption Int)) 42))
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -239,8 +239,8 @@ info: (declare-datatype TestOption (par (α) (
 info: (declare-datatype TestList (par (α) (
   (Nil)
   (Cons (TestList..head |α|) (TestList..tail (TestList |α|))))))
-(define-fun t0 () (TestList Int) (as Nil (TestList Int)))
-(define-fun t1 () (TestList Int) ((as Cons (TestList Int)) 1 t0))
+(define-fun $__t.0 () (TestList Int) (as Nil (TestList Int)))
+(define-fun $__t.1 () (TestList Int) ((as Cons (TestList Int)) 1 $__t.0))
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -259,8 +259,8 @@ info: (declare-datatype TestOption (par (α) (
   (Some (TestOption..val |α|)))))
 ; x
 (declare-const x (TestOption Int))
-(define-fun t0 () (TestOption Int) x)
-(define-fun t1 () Bool (|is-None| t0))
+(define-fun $__t.0 () (TestOption Int) x)
+(define-fun $__t.1 () Bool (|is-None| $__t.0))
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -275,8 +275,8 @@ info: (declare-datatype TestList (par (α) (
   (Cons (TestList..head |α|) (TestList..tail (TestList |α|))))))
 ; xs
 (declare-const xs (TestList Int))
-(define-fun t0 () (TestList Int) xs)
-(define-fun t1 () Bool (|is-Cons| t0))
+(define-fun $__t.0 () (TestList Int) xs)
+(define-fun $__t.1 () Bool (|is-Cons| $__t.0))
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -293,8 +293,8 @@ info: (declare-datatype TestOption (par (α) (
   (Some (TestOption..val |α|)))))
 ; x
 (declare-const x (TestOption Int))
-(define-fun t0 () (TestOption Int) x)
-(define-fun t1 () Int (TestOption..val t0))
+(define-fun $__t.0 () (TestOption Int) x)
+(define-fun $__t.1 () Int (TestOption..val $__t.0))
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -309,8 +309,8 @@ info: (declare-datatype TestList (par (α) (
   (Cons (TestList..head |α|) (TestList..tail (TestList |α|))))))
 ; xs
 (declare-const xs (TestList Int))
-(define-fun t0 () (TestList Int) xs)
-(define-fun t1 () Int (TestList..head t0))
+(define-fun $__t.0 () (TestList Int) xs)
+(define-fun $__t.1 () Int (TestList..head $__t.0))
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -325,8 +325,8 @@ info: (declare-datatype TestList (par (α) (
   (Cons (TestList..head |α|) (TestList..tail (TestList |α|))))))
 ; xs
 (declare-const xs (TestList Int))
-(define-fun t0 () (TestList Int) xs)
-(define-fun t1 () (TestList Int) (TestList..tail t0))
+(define-fun $__t.0 () (TestList Int) xs)
+(define-fun $__t.1 () (TestList Int) (TestList..tail $__t.0))
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -391,7 +391,7 @@ info: (declare-datatype Root (
   (DiamondValue (Diamond..left Left) (Diamond..right Right))))
 ; diamondVar
 (declare-const diamondVar Diamond)
-(define-fun t0 () Diamond diamondVar)
+(define-fun $__t.0 () Diamond diamondVar)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypes
@@ -432,7 +432,7 @@ info: (declare-datatypes ((RoseTree 1) (Forest 1))
   (par (α) ((FNil) (FCons (Forest..hd (RoseTree |α|)) (Forest..tl (Forest |α|)))))))
 ; tree
 (declare-const tree (RoseTree Int))
-(define-fun t0 () (RoseTree Int) tree)
+(define-fun $__t.0 () (RoseTree Int) tree)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypeBlocks
@@ -450,7 +450,7 @@ info: (declare-datatype TestOption (par (α) (
   (par (α) ((FNil) (FCons (Forest..hd (RoseTree |α|)) (Forest..tl (Forest |α|)))))))
 ; optionTree
 (declare-const optionTree (TestOption (RoseTree Int)))
-(define-fun t0 () (TestOption (RoseTree Int)) optionTree)
+(define-fun $__t.0 () (TestOption (RoseTree Int)) optionTree)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithDatatypeBlocks
@@ -525,12 +525,12 @@ info: (declare-datatype IntList (
   (Cons (IntList..hd Int) (IntList..tl IntList))))
 ; listLen
 (declare-fun listLen (IntList) Int)
-(define-fun t0 () IntList (as Nil IntList))
-(define-fun t1 () Int (listLen t0))
-(define-fun t2 () Bool (= t1 0))
-(define-fun t3 () Bool (forall (($__bv0 Int) ($__bv1 IntList)) (! (= (listLen ((as Cons IntList) $__bv0 $__bv1)) (+ 1 (listLen $__bv1))) :pattern ((listLen ((as Cons IntList) $__bv0 $__bv1))))))
-(assert t2)
-(assert t3)
+(define-fun $__t.0 () IntList (as Nil IntList))
+(define-fun $__t.1 () Int (listLen $__t.0))
+(define-fun $__t.2 () Bool (= $__t.1 0))
+(define-fun $__t.3 () Bool (forall (($__bv0 Int) ($__bv1 IntList)) (! (= (listLen ((as Cons IntList) $__bv0 $__bv1)) (+ 1 (listLen $__bv1))) :pattern ((listLen ((as Cons IntList) $__bv0 $__bv1))))))
+(assert $__t.2)
+(assert $__t.3)
 -/
 #guard_msgs in
 #eval format <$> toSMTStringWithRecFunc