From 4803bab8fe6c44792807bd7d90654d99a962dba4 Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed Date: Sat, 16 Nov 2024 19:33:05 -0800 Subject: [PATCH] Update toolchain to 4.13. (#143) * Update toolchain to 4.13. * Remove precompileModules config. * Update CI. --- .github/workflows/ci.yml | 5 +--- Smt/Attribute.lean | 6 ++--- Smt/Data/Graph.lean | 24 +++++++++--------- Smt/Dsl/Sexp.lean | 4 ++- Smt/Reconstruct.lean | 24 ++++++++++-------- Smt/Reconstruct/BitVec.lean | 4 +-- Smt/Reconstruct/BitVec/Bitblast.lean | 11 +++----- Smt/Reconstruct/Builtin.lean | 2 +- Smt/Reconstruct/Int.lean | 24 +++++++++--------- Smt/Reconstruct/Int/Polynorm.lean | 12 ++++----- Smt/Reconstruct/Int/Rewrites.lean | 4 +-- Smt/Reconstruct/Rat.lean | 26 ++++++++++--------- Smt/Reconstruct/Rat/Lemmas.lean | 4 +-- Smt/Reconstruct/Real.lean | 22 ++++++++-------- Smt/Reconstruct/Rewrite.lean | 4 +-- Smt/Reconstruct/UF.lean | 2 +- Smt/Tactic/EqnDef.lean | 6 ++--- Smt/Tactic/Smt.lean | 4 +-- Smt/Tactic/WHNFConfigurable.lean | 6 ++--- Smt/Tactic/WHNFSmt.lean | 12 ++++----- Smt/Translate.lean | 21 ++++++++-------- Smt/Translate/Bool.lean | 4 +++ Smt/Translate/Query.lean | 12 ++++----- Smt/Util.lean | 4 +-- Test/BitVec/Add.lean | 3 --- Test/BitVec/Shift.expected | 4 +-- Test/BitVec/XorComm.expected | 2 +- Test/Bool/Assoc.expected | 4 +-- Test/Bool/Comm.expected | 4 +-- Test/Bool/Cong.expected | 2 +- Test/Bool/HypotheticalSyllogism.expected | 2 +- Test/Bool/ModusPonens'.expected | 2 +- Test/Bool/ModusPonens.expected | 2 +- Test/Bool/ModusTollens.expected | 2 +- Test/Bool/PropExt.expected | 2 +- Test/Bool/Trans.expected | 4 +-- Test/EUF/Issue100.expected | 6 ++--- Test/Int/Binders.expected | 4 +-- Test/Int/DefineSort.expected | 2 +- Test/Int/Dvd.expected | 2 +- Test/Int/DvdTimeout.expected | 2 +- Test/Int/Let.expected | 2 +- Test/Nat/Cong.expected | 6 ++--- Test/Nat/Max.expected | 8 +++--- Test/Nat/ZeroSub'.expected | 2 +- Test/String/Contains.expected | 2 +- Test/String/Length.expected | 2 +- Test/linarith.expected | 24 ++++++++++++++++++ lake-manifest.json | 32 ++++++++++++++++-------- lakefile.lean | 20 ++++++--------- lean-toolchain | 2 +- 51 files changed, 214 insertions(+), 182 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a62910e4..9c7e2721 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -23,9 +23,6 @@ jobs: - name: Build lean-smt run: | lake update - lake build - lake build +Smt:dynlib - lake build +Smt.Rat:dynlib - lake build +Smt.Real:dynlib + lake build Smt Smt.Rat Smt.Real - name: Test lean-smt run: lake run test diff --git a/Smt/Attribute.lean b/Smt/Attribute.lean index 993e4876..34788231 100644 --- a/Smt/Attribute.lean +++ b/Smt/Attribute.lean @@ -14,12 +14,12 @@ open Lean /-- An extension to Lean's runtime environment to support SMT attributes. Maintains a set of function declarations for the `smt` tactic to utilize while generating the SMT query. -/ -abbrev SmtExtension := SimpleScopedEnvExtension (Name × Name) (HashMap Name (HashSet Name)) +abbrev SmtExtension := SimpleScopedEnvExtension (Name × Name) (Std.HashMap Name (Std.HashSet Name)) /-- Adds a declaration to the set of function declarations maintained by the SMT environment extension. -/ -def addSmtEntry (d : HashMap Name (HashSet Name)) (e : (Name × Name)) := - d.insert e.fst ((d.findD e.fst {}).insert e.snd) +def addSmtEntry (d : Std.HashMap Name (Std.HashSet Name)) (e : (Name × Name)) := + d.insert e.fst ((d.getD e.fst {}).insert e.snd) initialize smtExt : SmtExtension ← registerSimpleScopedEnvExtension { name := `SmtExt diff --git a/Smt/Data/Graph.lean b/Smt/Data/Graph.lean index f01e76c2..2ba5c032 100644 --- a/Smt/Data/Graph.lean +++ b/Smt/Data/Graph.lean @@ -9,37 +9,37 @@ import Lean.Data.HashMap import Lean.Data.HashSet import Lean.Message -open Lean Std +open Lean -def Graph (α) (β) [BEq α] [Hashable α] := Lean.HashMap α (Lean.HashMap α β) +abbrev Graph (α) (β) [BEq α] [Hashable α] := Std.HashMap α (Std.HashMap α β) namespace Graph variable {α} {β} [BEq α] [Hashable α] (g : Graph α β) (v u : α) (e : β) -def empty : Graph α β := HashMap.empty +def empty : Graph α β := {} def vertices : List α := g.fold (fun a v _ => v :: a) [] def neighbors? : Option (List α) := - g.find? v >>= fun es => some (es.fold (fun a v _ => v :: a) []) + g[v]? >>= fun es => some (es.fold (fun a v _ => v :: a) []) def neighbors! : List α := match (g.neighbors? v) with | some ns => ns | none => panic! "vertex is not in the graph" -def addVertex : Graph α β := g.insert v HashMap.empty +def addVertex : Graph α β := g.insert v {} -def addEdge : Graph α β := g.insert v ((g.find! v).insert u e) +def addEdge : Graph α β := g.insert v ((g[v]!).insert u e) -def weight? : Option β := g.find? v >>= fun es => es.find? u +def weight? : Option β := g[v]? >>= fun es => es[u]? partial def dfs [Monad m] (f : α → m Unit) : m Unit := - StateT.run' (s := HashSet.empty) do + StateT.run' (s := {}) do for v in g.vertices do visitVertex v where - visitVertex (v : α) : StateT (Lean.HashSet α) m Unit := do + visitVertex (v : α) : StateT (Std.HashSet α) m Unit := do let vs ← get if vs.contains v then return @@ -49,11 +49,11 @@ where f v partial def orderedDfs [Monad m] (vs : List α) (f : α → m Unit) : m Unit := - StateT.run' (s := HashSet.empty) do + StateT.run' (s := {}) do for v in vs do visitVertex v where - visitVertex (v : α) : StateT (Lean.HashSet α) m Unit := do + visitVertex (v : α) : StateT (Std.HashSet α) m Unit := do let vs ← get if vs.contains v then return @@ -62,7 +62,7 @@ where visitVertex u f v -open Format in +open Std.Format in protected def format [ToFormat α] [ToFormat β] : Format := bracket "{" (joinSep (g.vertices.map formatVertex) ("," ++ line)) "}" where diff --git a/Smt/Dsl/Sexp.lean b/Smt/Dsl/Sexp.lean index fd36d96b..042e84ef 100644 --- a/Smt/Dsl/Sexp.lean +++ b/Smt/Dsl/Sexp.lean @@ -4,7 +4,9 @@ institutional affiliations. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Wojciech Nawrocki -/ -import Lean.Parser + +import Lean.PrettyPrinter.Formatter +import Lean.PrettyPrinter.Parenthesizer import Smt.Data.Sexp diff --git a/Smt/Reconstruct.lean b/Smt/Reconstruct.lean index 837bfbc5..aa3c309c 100644 --- a/Smt/Reconstruct.lean +++ b/Smt/Reconstruct.lean @@ -16,9 +16,9 @@ open Lean open Attribute structure Reconstruct.state where - userNames : HashMap String FVarId - termCache : HashMap cvc5.Term Expr - proofCache : HashMap cvc5.Proof Expr + userNames : Std.HashMap String FVarId + termCache : Std.HashMap cvc5.Term Expr + proofCache : Std.HashMap cvc5.Proof Expr count : Nat currAssums : Array Expr skippedGoals : Array MVarId @@ -35,7 +35,7 @@ namespace Reconstruct private unsafe def getReconstructorsUnsafe (n : Name) (rcons : Type) : MetaM (List (rcons × Name)) := do let env ← getEnv - let names := ((smtExt.getState env).findD n {}).toList + let names := ((smtExt.getState env).getD n {}).toList let mut reconstructors := [] for name in names do let fn ← IO.ofExcept <| Id.run <| ExceptT.run <| @@ -75,7 +75,7 @@ def reconstructTerm : cvc5.Term → ReconstructM Expr := withTermCache fun t => go rs t where withTermCache (r : cvc5.Term → ReconstructM Expr) (t : cvc5.Term) : ReconstructM Expr := do - match (← get).termCache.find? t with + match (← get).termCache[t]? with -- TODO: cvc5's global bound variables mess up the cache. Find a better fix. | some e => return e | none => reconstruct r t @@ -98,7 +98,7 @@ def withNewProofCache (k : ReconstructM α) : ReconstructM α := do return r def withProofCache (r : cvc5.Proof → ReconstructM Expr) (pf : cvc5.Proof) : ReconstructM Expr := do - match (← get).proofCache.find? pf with + match (← get).proofCache[pf]? with | some e => return e | none => reconstruct r pf where @@ -181,11 +181,15 @@ def traceReconstructProof (r : Except Exception (Expr × Expr × List MVarId)) : | _ => m!"{bombEmoji}" open Qq in -partial def reconstructProof (pf : cvc5.Proof) (fvNames : HashMap String FVarId) : MetaM (Expr × Expr × List MVarId) := do +partial def reconstructProof (pf : cvc5.Proof) (fvNames : Std.HashMap String FVarId) : MetaM (Expr × Expr × List MVarId) := do withTraceNode `smt.reconstruct.proof traceReconstructProof do let Prod.mk (p : Q(Prop)) state ← (Reconstruct.reconstructTerm (pf.getResult)).run ⟨fvNames, {}, {}, 0, #[], #[]⟩ - let Prod.mk (h : Q(True → $p)) (.mk _ _ _ _ _ mvs) ← (Reconstruct.reconstructProof pf).run state - return (p, q($h trivial), mvs.toList) + let (h, .mk _ _ _ _ _ mvs) ← (Reconstruct.reconstructProof pf).run state + if pf.getArguments.isEmpty then + let h : Q(True → $p) ← pure h + return (p, q($h trivial), mvs.toList) + else + return (p, h, mvs.toList) open cvc5 in def traceSolve (r : Except Exception (Except SolverError Proof)) : MetaM MessageData := @@ -233,7 +237,7 @@ open Lean.Elab Tactic in let (_, mv) ← mv.intro1 replaceMainGoal (mv :: mvs) where - getFVarNames : MetaM (HashMap String FVarId) := do + getFVarNames : MetaM (Std.HashMap String FVarId) := do let lCtx ← getLCtx return lCtx.getFVarIds.foldl (init := {}) fun m fvarId => m.insert (lCtx.getRoundtrippingUserName? fvarId).get!.toString fvarId diff --git a/Smt/Reconstruct/BitVec.lean b/Smt/Reconstruct/BitVec.lean index 6670a140..71e6343d 100644 --- a/Smt/Reconstruct/BitVec.lean +++ b/Smt/Reconstruct/BitVec.lean @@ -51,7 +51,7 @@ partial def synthDecidableInst (t : cvc5.Term) : ReconstructM Expr := do match t let w : Nat := t[0]!.getSort.getBitVectorSize.val let x : Q(BitVec $w) ← reconstructTerm t[0]! let i : Nat := t.getOp[0]!.getIntegerValue.toNat - return q(instDecidableEqBool («$x».getLsb $i) true) + return q(instDecidableEqBool («$x».getLsbD $i) true) | _ => let p : Q(Prop) ← reconstructTerm t Meta.synthInstance q(Decidable $p) @@ -229,7 +229,7 @@ where let w : Nat := t[0]!.getSort.getBitVectorSize.val let x : Q(BitVec $w) ← reconstructTerm t[0]! let i : Nat := t.getOp[0]!.getIntegerValue.toNat - return q(«$x».getLsb $i = true) + return q(«$x».getLsbD $i = true) | _ => return none where leftAssocOp (op : Expr) (t : cvc5.Term) : ReconstructM Expr := do diff --git a/Smt/Reconstruct/BitVec/Bitblast.lean b/Smt/Reconstruct/BitVec/Bitblast.lean index 379c61b4..76eaa1c7 100644 --- a/Smt/Reconstruct/BitVec/Bitblast.lean +++ b/Smt/Reconstruct/BitVec/Bitblast.lean @@ -7,12 +7,10 @@ Authors: Abdalrhman Mohamed import Lean -import Smt.Reconstruct.Prop.Core - namespace BitVec def bb (x : BitVec w) : BitVec w := - (iunfoldr (fun i _ => ((), x.getLsb i)) ()).snd + (iunfoldr (fun i _ => ((), x.getLsbD i)) ()).snd def self_eq_bb (x : BitVec w) : x = x.bb := sorry @@ -29,8 +27,8 @@ def beq (x : BitVec w) (y : BitVec w) : Bool := go (w - 1) where go : Nat → Bool - | 0 => x.getLsb (w - 1) == y.getLsb (w - 1) - | i + 1 => x.getLsb ((w - 1) - (i + 1)) == y.getLsb ((w - 1) - (i + 1)) && go i + | 0 => x.getLsbD (w - 1) == y.getLsbD (w - 1) + | i + 1 => x.getLsbD ((w - 1) - (i + 1)) == y.getLsbD ((w - 1) - (i + 1)) && go i def eq_eq_beq (x : BitVec w) (y : BitVec w) : (x = y) = x.beq y := sorry @@ -44,12 +42,11 @@ theorem adcb_eq_adcb' : adcb = adcb' := by /-- Bitwise addition implemented via a ripple carry adder. -/ def adc' (x y : BitVec w) : Bool → Bool × BitVec w := - iunfoldr fun (i : Fin w) c => adcb' (x.getLsb i) (y.getLsb i) c + iunfoldr fun (i : Fin w) c => adcb' (x.getLsbD i) (y.getLsbD i) c theorem adc_eq_adc' : @adc = @adc' := by funext x y c rw [adc, adc', adcb_eq_adcb'] - rfl theorem add_eq_adc' (x y : BitVec w) : x + y = (adc' x y false).snd := by rw [add_eq_adc, adc_eq_adc'] diff --git a/Smt/Reconstruct/Builtin.lean b/Smt/Reconstruct/Builtin.lean index c9f20ae8..ac6b0731 100644 --- a/Smt/Reconstruct/Builtin.lean +++ b/Smt/Reconstruct/Builtin.lean @@ -30,7 +30,7 @@ def getFVarExpr! (n : Name) : MetaM Expr := do | none => throwError "unknown free variable '{n}'" def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do - match (← get).userNames.find? n with + match (← get).userNames[n]? with | some fv => return .fvar fv | none => match (← getLCtx).findFromUserName? n.toName with | some d => return d.toExpr diff --git a/Smt/Reconstruct/Int.lean b/Smt/Reconstruct/Int.lean index 0c1dc251..7409ae62 100644 --- a/Smt/Reconstruct/Int.lean +++ b/Smt/Reconstruct/Int.lean @@ -289,7 +289,7 @@ def reconstructSumUB (pf : cvc5.Proof) : ReconstructM (Option Expr) := do def reconstructMulSign (pf : cvc5.Proof) : ReconstructM (Option Expr) := do let ts := pf.getResult[0]!.getChildren let mut hs : Array (Name × (Array Expr → ReconstructM Expr)) := #[] - let mut map : HashMap cvc5.Term Nat := {} + let mut map : Std.HashMap cvc5.Term Nat := {} for h : i in [0:ts.size] do let t := ts[i]'(h.right) let p : Q(Prop) ← reconstructTerm t @@ -303,43 +303,43 @@ def reconstructMulSign (pf : cvc5.Proof) : ReconstructM (Option Expr) := do let ps : Q(List Prop) ← ts.foldrM f q([]) let q : Q(Prop) ← reconstructTerm t let h : Q(impliesN $ps $q) ← Meta.withLocalDeclsD hs fun hs => do - let h : Q($q) ← if ts[map.find! vs[0]!]!.getKind == .NOT then + let h : Q($q) ← if ts[map[vs[0]!]!]!.getKind == .NOT then let a : Q(Int) ← reconstructTerm vs[0]! - let ha : Q($a ≠ 0) := hs[map.find! vs[0]!]! + let ha : Q($a ≠ 0) := hs[map[vs[0]!]!]! go vs ts hs map .GT q($a * $a) q(Int.mul_sign₀ $ha) 2 else let a : Q(Int) ← reconstructTerm vs[0]! - go vs ts hs map ts[map.find! vs[0]!]!.getKind a hs[map.find! vs[0]!]! 1 + go vs ts hs map ts[map[vs[0]!]!]!.getKind a hs[map[vs[0]!]!]! 1 Meta.mkLambdaFVars hs h addThm q(andN $ps → $q) q(Builtin.scopes $h) where go vs ts hs map ka (a : Q(Int)) (ha : Expr) i : ReconstructM Expr := do if hi : i < vs.size then let b : Q(Int) ← reconstructTerm vs[i] - let k := ts[map.find! vs[i]]!.getKind + let k := ts[map[vs[i]]!]!.getKind if ka == .LT && k == .LT then let ha : Q($a < 0) := ha - let hb : Q($b < 0) := hs[map.find! vs[i]]! + let hb : Q($b < 0) := hs[map[vs[i]]!]! go vs ts hs map .GT q($a * $b) q(Int.mul_sign₁ $ha $hb) (i + 1) else if ka == .LT && k == .NOT then let ha : Q($a < 0) := ha - let hb : Q($b ≠ 0) := hs[map.find! vs[i]]! + let hb : Q($b ≠ 0) := hs[map[vs[i]]!]! go vs ts hs map .LT q($a * $b * $b) q(Int.mul_sign₂ $ha $hb) (i + 2) else if ka == .LT && k == .GT then let ha : Q($a < 0) := ha - let hb : Q($b > 0) := hs[map.find! vs[i]]! + let hb : Q($b > 0) := hs[map[vs[i]]!]! go vs ts hs map .LT q($a * $b) q(Int.mul_sign₃ $ha $hb) (i + 1) else if ka == .GT && k == .LT then let ha : Q($a > 0) := ha - let hb : Q($b < 0) := hs[map.find! vs[i]]! + let hb : Q($b < 0) := hs[map[vs[i]]!]! go vs ts hs map .LT q($a * $b) q(Int.mul_sign₄ $ha $hb) (i + 1) else if ka == .GT && k == .NOT then let ha : Q($a > 0) := ha - let hb : Q($b ≠ 0) := hs[map.find! vs[i]]! + let hb : Q($b ≠ 0) := hs[map[vs[i]]!]! go vs ts hs map .GT q($a * $b * $b) q(Int.mul_sign₅ $ha $hb) (i + 2) else if ka == .GT && k == .GT then let ha : Q($a > 0) := ha - let hb : Q($b > 0) := hs[map.find! vs[i]]! + let hb : Q($b > 0) := hs[map[vs[i]]!]! go vs ts hs map .GT q($a * $b) q(Int.mul_sign₆ $ha $hb) (i + 1) else throwError "[mul_sign]: invalid kinds: {ka}, {k}" @@ -400,7 +400,7 @@ where if !pf.getResult[0]!.getSort.isInteger then return none let a : Q(Int) ← reconstructTerm pf.getResult[0]! let b : Q(Int) ← reconstructTerm pf.getResult[1]! - addTac q($a = $b) Int.polyNorm + addTac q($a = $b) Int.nativePolyNorm | .ARITH_POLY_NORM_REL => if !pf.getResult[0]![0]!.getSort.isInteger then return none let cx : Int := pf.getChildren[0]!.getResult[0]![0]!.getIntegerValue diff --git a/Smt/Reconstruct/Int/Polynorm.lean b/Smt/Reconstruct/Int/Polynorm.lean index c44de280..4c756144 100644 --- a/Smt/Reconstruct/Int/Polynorm.lean +++ b/Smt/Reconstruct/Int/Polynorm.lean @@ -303,12 +303,12 @@ end PolyNorm.Expr open Lean Qq -partial def genCtx (e : Q(Int)) : StateT (Array Q(Int) × HashSet Q(Int)) MetaM Unit := do +partial def genCtx (e : Q(Int)) : StateT (Array Q(Int) × Std.HashSet Q(Int)) MetaM Unit := do if !(← get).snd.contains e then go modify fun (es, cache) => (es, cache.insert e) where - go : StateT (Array Q(Int) × HashSet Q(Int)) MetaM Unit := do + go : StateT (Array Q(Int) × Std.HashSet Q(Int)) MetaM Unit := do match e with | ~q(OfNat.ofNat $x) => pure () | ~q(-$x) => genCtx x @@ -317,15 +317,15 @@ where | ~q($x * $y) => genCtx x >>= fun _ => genCtx y | _ => if !(← get).fst.contains e then modify fun (es, cache) => (es.push e, cache) -partial def toQPolyNormExpr (ctx : Q(PolyNorm.Context)) (es : Array Q(Int)) (e : Q(Int)) (cache : HashMap Expr (Expr × Expr)) : - MetaM (HashMap Expr (Expr × Expr) × (o : Q(PolyNorm.Expr)) × Q(«$o».denote $ctx = $e)) := do - match cache.find? e with +partial def toQPolyNormExpr (ctx : Q(PolyNorm.Context)) (es : Array Q(Int)) (e : Q(Int)) (cache : Std.HashMap Expr (Expr × Expr)) : + MetaM (Std.HashMap Expr (Expr × Expr) × (o : Q(PolyNorm.Expr)) × Q(«$o».denote $ctx = $e)) := do + match cache.get? e with | some (e, h) => return ⟨cache, e, h⟩ | none => let ⟨cache, o, h⟩ ← go return ⟨cache.insert e (o, h), o, h⟩ where - go : MetaM (HashMap Expr (Expr × Expr) × (o : Q(PolyNorm.Expr)) × Q(«$o».denote $ctx = $e)) := do match e with + go : MetaM (Std.HashMap Expr (Expr × Expr) × (o : Q(PolyNorm.Expr)) × Q(«$o».denote $ctx = $e)) := do match e with | ~q(OfNat.ofNat $x) => pure ⟨cache, q(.val (@OfNat.ofNat Int $x _)), q(rfl)⟩ | ~q(-$x) => diff --git a/Smt/Reconstruct/Int/Rewrites.lean b/Smt/Reconstruct/Int/Rewrites.lean index bae255aa..6a4745ba 100644 --- a/Smt/Reconstruct/Int/Rewrites.lean +++ b/Smt/Reconstruct/Int/Rewrites.lean @@ -49,9 +49,9 @@ theorem elim_gt : (t > s) = ¬(t ≤ s) := theorem elim_lt : (t < s) = ¬(t ≥ s) := propext Int.not_le.symm theorem elim_int_gt {t s : Int} : (t > s) = (t ≥ s + 1) := - propext (Int.lt_iff_add_one_le s t) + propext Int.lt_iff_add_one_le theorem elim_int_lt {t s : Int} : (t < s) = (s ≥ t + 1) := - propext (Int.lt_iff_add_one_le t s) + propext Int.lt_iff_add_one_le theorem elim_leq : (t ≤ s) = (s ≥ t) := propext ge_iff_le diff --git a/Smt/Reconstruct/Rat.lean b/Smt/Reconstruct/Rat.lean index 295c18e7..eace39a7 100644 --- a/Smt/Reconstruct/Rat.lean +++ b/Smt/Reconstruct/Rat.lean @@ -271,7 +271,7 @@ def reconstructSumUB (pf : cvc5.Proof) : ReconstructM (Option Expr) := do def reconstructMulSign (pf : cvc5.Proof) : ReconstructM (Option Expr) := do let ts := pf.getResult[0]!.getChildren let mut hs : Array (Name × (Array Expr → ReconstructM Expr)) := #[] - let mut map : HashMap cvc5.Term Nat := {} + let mut map : Std.HashMap cvc5.Term Nat := {} for h : i in [0:ts.size] do let t := ts[i]'(h.right) let p : Q(Prop) ← reconstructTerm t @@ -285,43 +285,43 @@ def reconstructMulSign (pf : cvc5.Proof) : ReconstructM (Option Expr) := do let ps : Q(List Prop) ← ts.foldrM f q([]) let q : Q(Prop) ← reconstructTerm t let h : Q(impliesN $ps $q) ← Meta.withLocalDeclsD hs fun hs => do - let h : Q($q) ← if ts[map.find! vs[0]!]!.getKind == .NOT then + let h : Q($q) ← if ts[map[vs[0]!]!]!.getKind == .NOT then let a : Q(Rat) ← reconstructTerm vs[0]! - let ha : Q($a ≠ 0) := hs[map.find! vs[0]!]! + let ha : Q($a ≠ 0) := hs[map[vs[0]!]!]! go vs ts hs map .GT q($a * $a) q(Rat.mul_sign₀ $ha) 2 else let a : Q(Rat) ← reconstructTerm vs[0]! - go vs ts hs map ts[map.find! vs[0]!]!.getKind a hs[map.find! vs[0]!]! 1 + go vs ts hs map ts[map[vs[0]!]!]!.getKind a hs[map[vs[0]!]!]! 1 Meta.mkLambdaFVars hs h addThm q(andN $ps → $q) q(Builtin.scopes $h) where go vs ts hs map ka (a : Q(Rat)) (ha : Expr) i : ReconstructM Expr := do if hi : i < vs.size then let b : Q(Rat) ← reconstructTerm vs[i] - let k := ts[map.find! vs[i]]!.getKind + let k := ts[map[vs[i]]!]!.getKind if ka == .LT && k == .LT then let ha : Q($a < 0) := ha - let hb : Q($b < 0) := hs[map.find! vs[i]]! + let hb : Q($b < 0) := hs[map[vs[i]]!]! go vs ts hs map .GT q($a * $b) q(Rat.mul_sign₁ $ha $hb) (i + 1) else if ka == .LT && k == .NOT then let ha : Q($a < 0) := ha - let hb : Q($b ≠ 0) := hs[map.find! vs[i]]! + let hb : Q($b ≠ 0) := hs[map[vs[i]]!]! go vs ts hs map .LT q($a * $b * $b) q(Rat.mul_sign₂ $ha $hb) (i + 2) else if ka == .LT && k == .GT then let ha : Q($a < 0) := ha - let hb : Q($b > 0) := hs[map.find! vs[i]]! + let hb : Q($b > 0) := hs[map[vs[i]]!]! go vs ts hs map .LT q($a * $b) q(Rat.mul_sign₃ $ha $hb) (i + 1) else if ka == .GT && k == .LT then let ha : Q($a > 0) := ha - let hb : Q($b < 0) := hs[map.find! vs[i]]! + let hb : Q($b < 0) := hs[map[vs[i]]!]! go vs ts hs map .LT q($a * $b) q(Rat.mul_sign₄ $ha $hb) (i + 1) else if ka == .GT && k == .NOT then let ha : Q($a > 0) := ha - let hb : Q($b ≠ 0) := hs[map.find! vs[i]]! + let hb : Q($b ≠ 0) := hs[map[vs[i]]!]! go vs ts hs map .GT q($a * $b * $b) q(Rat.mul_sign₅ $ha $hb) (i + 2) else if ka == .GT && k == .GT then let ha : Q($a > 0) := ha - let hb : Q($b > 0) := hs[map.find! vs[i]]! + let hb : Q($b > 0) := hs[map[vs[i]]!]! go vs ts hs map .GT q($a * $b) q(Rat.mul_sign₆ $ha $hb) (i + 1) else throwError "[mul_sign]: invalid kinds: {ka}, {k}" @@ -335,6 +335,8 @@ where if pf.getResult[0]!.getSort.isInteger then return none reconstructSumUB pf | .INT_TIGHT_UB => + logInfo + m!"rule : {pf.getRule}\npremises : {pf.getChildren.map (·.getResult)}\nargs : {pf.getArguments}\nconclusion : {pf.getResult}" let i : Q(Int) ← reconstructTerm pf.getChildren[0]!.getResult[0]! let c : Q(Rat) ← reconstructTerm pf.getChildren[0]!.getResult[1]! let h : Q($i < $c) ← reconstructProof pf.getChildren[0]! @@ -380,7 +382,7 @@ where if pf.getResult[0]!.getSort.isInteger then return none let a : Q(Rat) ← reconstructTerm pf.getResult[0]! let b : Q(Rat) ← reconstructTerm pf.getResult[1]! - addTac q($a = $b) Rat.polyNorm + addTac q($a = $b) Rat.nativePolyNorm | .ARITH_POLY_NORM_REL => if pf.getResult[0]![0]!.getSort.isInteger then return none let lcx : Lean.Rat := pf.getChildren[0]!.getResult[0]![0]!.getRationalValue diff --git a/Smt/Reconstruct/Rat/Lemmas.lean b/Smt/Reconstruct/Rat/Lemmas.lean index 1c4bdc6d..b82f7de4 100644 --- a/Smt/Reconstruct/Rat/Lemmas.lean +++ b/Smt/Reconstruct/Rat/Lemmas.lean @@ -58,10 +58,10 @@ theorem neg_lt_neg (h : a < b) : -a > -b := by theorem neg_le_neg (h : a ≤ b) : -a ≥ -b := by sorry -theorem int_tight_ub {i : Int} (h : i < c) : i ≤ c.floor := by +theorem int_tight_ub (h : i < c) : i ≤ c.floor := by sorry -theorem int_tight_lb {i : Int} (h : i > c) : i ≥ c.ceil := by +theorem int_tight_lb (h : i > c) : i ≥ c.ceil := by sorry theorem trichotomy₁ (h₁ : a ≤ b) (h₂ : a ≠ b) : a < b := by diff --git a/Smt/Reconstruct/Real.lean b/Smt/Reconstruct/Real.lean index ea499d44..949d4fa0 100644 --- a/Smt/Reconstruct/Real.lean +++ b/Smt/Reconstruct/Real.lean @@ -291,7 +291,7 @@ def reconstructSumUB (pf : cvc5.Proof) : ReconstructM (Option Expr) := do def reconstructMulSign (pf : cvc5.Proof) : ReconstructM (Option Expr) := do let ts := pf.getResult[0]!.getChildren let mut hs : Array (Name × (Array Expr → ReconstructM Expr)) := #[] - let mut map : HashMap cvc5.Term Nat := {} + let mut map : Std.HashMap cvc5.Term Nat := {} for h : i in [0:ts.size] do let t := ts[i]'(h.right) let p : Q(Prop) ← reconstructTerm t @@ -305,43 +305,43 @@ def reconstructMulSign (pf : cvc5.Proof) : ReconstructM (Option Expr) := do let ps : Q(List Prop) ← ts.foldrM f q([]) let q : Q(Prop) ← reconstructTerm t let h : Q(impliesN $ps $q) ← Meta.withLocalDeclsD hs fun hs => do - let h : Q($q) ← if ts[map.find! vs[0]!]!.getKind == .NOT then + let h : Q($q) ← if ts[map[vs[0]!]!]!.getKind == .NOT then let a : Q(Real) ← reconstructTerm vs[0]! - let ha : Q($a ≠ 0) := hs[map.find! vs[0]!]! + let ha : Q($a ≠ 0) := hs[map[vs[0]!]!]! go vs ts hs map .GT q($a * $a) q(Real.mul_sign₀ $ha) 2 else let a : Q(Real) ← reconstructTerm vs[0]! - go vs ts hs map ts[map.find! vs[0]!]!.getKind a hs[map.find! vs[0]!]! 1 + go vs ts hs map ts[map[vs[0]!]!]!.getKind a hs[map[vs[0]!]!]! 1 Meta.mkLambdaFVars hs h addThm q(andN $ps → $q) q(Builtin.scopes $h) where go vs ts hs map ka (a : Q(Real)) (ha : Expr) i : ReconstructM Expr := do if hi : i < vs.size then let b : Q(Real) ← reconstructTerm vs[i] - let k := ts[map.find! vs[i]]!.getKind + let k := ts[map[vs[i]]!]!.getKind if ka == .LT && k == .LT then let ha : Q($a < 0) := ha - let hb : Q($b < 0) := hs[map.find! vs[i]]! + let hb : Q($b < 0) := hs[map[vs[i]]!]! go vs ts hs map .GT q($a * $b) q(Real.mul_sign₁ $ha $hb) (i + 1) else if ka == .LT && k == .NOT then let ha : Q($a < 0) := ha - let hb : Q($b ≠ 0) := hs[map.find! vs[i]]! + let hb : Q($b ≠ 0) := hs[map[vs[i]]!]! go vs ts hs map .LT q($a * $b * $b) q(Real.mul_sign₂ $ha $hb) (i + 2) else if ka == .LT && k == .GT then let ha : Q($a < 0) := ha - let hb : Q($b > 0) := hs[map.find! vs[i]]! + let hb : Q($b > 0) := hs[map[vs[i]]!]! go vs ts hs map .LT q($a * $b) q(Real.mul_sign₃ $ha $hb) (i + 1) else if ka == .GT && k == .LT then let ha : Q($a > 0) := ha - let hb : Q($b < 0) := hs[map.find! vs[i]]! + let hb : Q($b < 0) := hs[map[vs[i]]!]! go vs ts hs map .LT q($a * $b) q(Real.mul_sign₄ $ha $hb) (i + 1) else if ka == .GT && k == .NOT then let ha : Q($a > 0) := ha - let hb : Q($b ≠ 0) := hs[map.find! vs[i]]! + let hb : Q($b ≠ 0) := hs[map[vs[i]]!]! go vs ts hs map .GT q($a * $b * $b) q(Real.mul_sign₅ $ha $hb) (i + 2) else if ka == .GT && k == .GT then let ha : Q($a > 0) := ha - let hb : Q($b > 0) := hs[map.find! vs[i]]! + let hb : Q($b > 0) := hs[map[vs[i]]!]! go vs ts hs map .GT q($a * $b) q(Real.mul_sign₆ $ha $hb) (i + 1) else throwError "[mul_sign]: invalid kinds: {ka}, {k}" diff --git a/Smt/Reconstruct/Rewrite.lean b/Smt/Reconstruct/Rewrite.lean index ef592c3d..7563f49e 100644 --- a/Smt/Reconstruct/Rewrite.lean +++ b/Smt/Reconstruct/Rewrite.lean @@ -33,8 +33,8 @@ def smtRw (mv : MVarId) (op : Expr) (id : Expr) (rr : Expr) (xss : Array (Array let lvl ← Meta.getLevel α let h₁ ← Meta.mkFreshExprMVar (mkApp3 (.const ``Eq [lvl]) α l ml) let h₃ ← Meta.mkFreshExprMVar (mkApp3 (.const ``Eq [lvl]) α mr r) - Meta.AC.rewriteUnnormalized h₁.mvarId! - Meta.AC.rewriteUnnormalized h₃.mvarId! + Meta.AC.rewriteUnnormalizedRefl h₁.mvarId! + Meta.AC.rewriteUnnormalizedRefl h₃.mvarId! mv.assign (mkApp8 (.const ``Eq.trans₂ [lvl]) α l ml mr r h₁ h₂ h₃) syntax inner := "[" term,* "]" diff --git a/Smt/Reconstruct/UF.lean b/Smt/Reconstruct/UF.lean index e23fb4ee..bb33145a 100644 --- a/Smt/Reconstruct/UF.lean +++ b/Smt/Reconstruct/UF.lean @@ -14,7 +14,7 @@ namespace Smt.Reconstruct.UF open Lean Qq def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do - match (← get).userNames.find? n with + match (← get).userNames[n]? with | some fv => return .fvar fv | none => match (← getLCtx).findFromUserName? n.toName with | some d => return d.toExpr diff --git a/Smt/Tactic/EqnDef.lean b/Smt/Tactic/EqnDef.lean index 07464a1a..c4c843f7 100644 --- a/Smt/Tactic/EqnDef.lean +++ b/Smt/Tactic/EqnDef.lean @@ -131,7 +131,7 @@ elab "extract_def" i:ident : tactic => do let _ ← addEqnDefForConst nm /-- Specialize an equational definition via partial evaluation. See `specialize_def`. -/ -def specializeEqnDef (x : FVarId) (args : Array Expr) (opaqueConsts : HashSet Name := {}) +def specializeEqnDef (x : FVarId) (args : Array Expr) (opaqueConsts : Std.HashSet Name := {}) : TacticM FVarId := do withMainContext do let eqn ← inferType (mkFVar x) @@ -193,14 +193,14 @@ open Lean Meta Elab Tactic in | `(tactic|specialize_def $i [ $ts,* ]) => go i ts {} | `(tactic|specialize_def $i [ $ts,* ] blocking [ $bs,* ]) => withMainContext do - let opaqueConsts ← bs.getElems.foldlM (init := HashSet.empty) fun cs b => do + let opaqueConsts ← bs.getElems.foldlM (init := {}) fun cs b => do match ← elabTerm b none with | .const nm _ => return cs.insert nm | .fvar fv => return cs.insert (← fv.getDecl).userName | _ => throwError "expected a (local) constant, got{indentD b}" go i ts opaqueConsts | stx => throwError "unexpected syntax {stx}" -where go (i : TSyntax `ident) (ts : TSyntaxArray `term) (opaqueConsts : HashSet Name) : TacticM Unit := +where go (i : TSyntax `ident) (ts : TSyntaxArray `term) (opaqueConsts : Std.HashSet Name) : TacticM Unit := withMainContext do let nm := i.getId let ld ← getLocalDeclFromUserName (eqnDefName nm) diff --git a/Smt/Tactic/Smt.lean b/Smt/Tactic/Smt.lean index de30697f..a5d4865d 100644 --- a/Smt/Tactic/Smt.lean +++ b/Smt/Tactic/Smt.lean @@ -20,7 +20,7 @@ open Lean hiding Command open Elab Tactic Qq open Smt Translate Query Reconstruct Util -def genUniqueFVarNames : MetaM (HashMap FVarId String × HashMap String FVarId) := do +def genUniqueFVarNames : MetaM (Std.HashMap FVarId String × Std.HashMap String FVarId) := do let lCtx ← getLCtx let st : NameSanitizerState := { options := {}} let (lCtx, _) := (lCtx.sanitizeNames st).run @@ -29,7 +29,7 @@ def genUniqueFVarNames : MetaM (HashMap FVarId String × HashMap String FVarId) let m₂ := m₂.insert (lCtx.getRoundtrippingUserName? fvarId).get!.toString fvarId (m₁, m₂) -def prepareSmtQuery (hs : List Expr) (goalType : Expr) (fvNames : HashMap FVarId String) : MetaM (List Command) := do +def prepareSmtQuery (hs : List Expr) (goalType : Expr) (fvNames : Std.HashMap FVarId String) : MetaM (List Command) := do let goalId ← Lean.mkFreshMVarId Lean.Meta.withLocalDeclD goalId.name (mkNot goalType) fun g => Query.generateQuery g hs fvNames diff --git a/Smt/Tactic/WHNFConfigurable.lean b/Smt/Tactic/WHNFConfigurable.lean index e8a04728..418865cc 100644 --- a/Smt/Tactic/WHNFConfigurable.lean +++ b/Smt/Tactic/WHNFConfigurable.lean @@ -239,7 +239,7 @@ private def reduceRec (recVal : RecursorVal) (recLvls : List Level) (recArgs : A =========================== -/ /-- Auxiliary function for reducing `Quot.lift` and `Quot.ind` applications. -/ -private def reduceQuotRec (recVal : QuotVal) (recLvls : List Level) (recArgs : Array Expr) +private def reduceQuotRec (recVal : QuotVal) (recArgs : Array Expr) (failK : Unit → ReductionM α) (successK : Expr → ReductionM α) : ReductionM α := let process (majorPos argPos : Nat) : ReductionM α := @@ -583,7 +583,7 @@ where matchConstAux f (fun _ => return e) fun cinfo lvls => match cinfo with | ConstantInfo.recInfo rec => reduceRec rec lvls revArgs.reverse (fun _ => return e) go - | ConstantInfo.quotInfo rec => reduceQuotRec rec lvls revArgs.reverse (fun _ => return e) go + | ConstantInfo.quotInfo rec => reduceQuotRec rec revArgs.reverse (fun _ => return e) go | c@(ConstantInfo.defnInfo _) => do if (← isAuxDef c.name) then deltaBetaDefinition c lvls revArgs (fun _ => return e) go @@ -850,7 +850,7 @@ def reduceRecMatcher? (e : Expr) : ReductionM (Option Expr) := do | _ => matchConstAux e.getAppFn (fun _ => pure none) fun cinfo lvls => do match cinfo with | ConstantInfo.recInfo «rec» => reduceRec «rec» lvls e.getAppArgs (fun _ => pure none) (fun e => pure (some e)) - | ConstantInfo.quotInfo «rec» => reduceQuotRec «rec» lvls e.getAppArgs (fun _ => pure none) (fun e => pure (some e)) + | ConstantInfo.quotInfo «rec» => reduceQuotRec «rec» e.getAppArgs (fun _ => pure none) (fun e => pure (some e)) | c@(ConstantInfo.defnInfo _) => if (← isAuxDef c.name) then deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => pure none) (fun e => pure (some e)) diff --git a/Smt/Tactic/WHNFSmt.lean b/Smt/Tactic/WHNFSmt.lean index d535be48..04801b7c 100644 --- a/Smt/Tactic/WHNFSmt.lean +++ b/Smt/Tactic/WHNFSmt.lean @@ -13,8 +13,8 @@ namespace Smt open Lean /-- Constants which SMT knows about and we thus don't want to unfold. -/ -def smtConsts : HashSet Name := - List.foldr (fun c s => s.insert c) HashSet.empty +def smtConsts : Std.HashSet Name := + List.foldr (fun c s => s.insert c) {} [ ``Eq, ``BEq.beq, @@ -94,22 +94,22 @@ def smtConsts : HashSet Name := ``UInt32.shiftRight ] -def opaquePred (opaqueConsts : HashSet Name) (_ : Meta.Config) (ci : ConstantInfo) : CoreM Bool := do +def opaquePred (opaqueConsts : Std.HashSet Name) (_ : Meta.Config) (ci : ConstantInfo) : CoreM Bool := do if smtConsts.contains ci.name || opaqueConsts.contains ci.name then return false return true /-- Runs type-theoretic reduction, but never unfolding SMT builtins and with extra rules -to let-lift `let-opaque` bindings. This can produce linearly-sized terms in certain cases. +to let-lift `let-opaque` bindings. This can produce linearly-sized terms in certain cases. Constants with names in `opaqueConsts` are also not unfolded. -/ -def smtOpaqueReduce (e : Expr) (opaqueConsts : HashSet Name := {}) : MetaM Expr := +def smtOpaqueReduce (e : Expr) (opaqueConsts : Std.HashSet Name := {}) : MetaM Expr := withTheReader Meta.Context (fun ctx => { ctx with canUnfold? := some (opaquePred opaqueConsts) }) do Smt.reduce (skipTypes := false) e |>.run { letPushElim := true } - + open Parser in syntax (name := «let_opaque») withPosition("let_opaque " letDecl) optional(";") term : term diff --git a/Smt/Translate.lean b/Smt/Translate.lean index ce16d699..e72c00f0 100644 --- a/Smt/Translate.lean +++ b/Smt/Translate.lean @@ -9,7 +9,6 @@ import Lean import Smt.Attribute import Smt.Translate.Term -import Smt.Util /-- Return true iff `e` contains a free variable which satisfies `p`. -/ @[inline] private def Lean.Expr.hasAnyFVar' [Monad m] (e : Expr) (p : FVarId → m Bool) : m Bool := @@ -33,20 +32,20 @@ open Attribute Term structure TranslationM.State where /-- Constants that the translated result depends on. We propagate these upwards during translation in order to build a dependency graph. The value is reset at the `translateExpr` entry point. -/ - depConstants : NameSet := .empty + depConstants : NameSet := {} /-- Free variables that the translated result depends on. We propagate these upwards during translation in order to build a dependency graph. The value is reset at the `translateExpr` entry point. -/ - depFVars : FVarIdSet := .empty + depFVars : FVarIdSet := {} /-- Free variables introduced during translation (from binder expressions). Those should NOT be propegated upwards during translation. -/ - localFVars : FVarIdSet := .empty + localFVars : FVarIdSet := {} /-- Memoizes `applyTranslators?` calls together with what they add to `depConstants` and `depFVars`. -/ - cache : HashMap Expr (Option (Term × NameSet × FVarIdSet)) := .empty + cache : Std.HashMap Expr (Option (Term × NameSet × FVarIdSet)) := {} /-- A mapping from a scopped name to a suffix index that makes it unique. This field does not handle scopping, which should be handled by `withScopedName` -/ - scopedNames : HashMap Name Nat := .empty + scopedNames : Std.HashMap Name Nat := {} /-- A mapping from fvars to unique names. -/ - uniqueFVarNames : HashMap FVarId String := .empty + uniqueFVarNames : Std.HashMap FVarId String := {} abbrev TranslationM := StateT TranslationM.State MetaM @@ -63,7 +62,7 @@ namespace Translator private unsafe def getTranslatorsUnsafe : MetaM (List (Translator × Name)) := do let env ← getEnv - let names := ((smtExt.getState env).findD ``Translator {}).toList + let names := ((smtExt.getState env).getD ``Translator {}).toList -- trace[smt.attr] "Translators: {names}" let mut translators := [] for name in names do @@ -79,7 +78,7 @@ opaque getTranslators : MetaM (List (Translator × Name)) /-- Return a cached translation of `e` if found, otherwise run `k e` and cache the result. -/ def withCache (k : Translator) (e : Expr) : TranslationM (Option Term) := do - match (← get).cache.find? e with + match (← get).cache[e]? with | some (some (tm, depConsts, depFVars)) => modify fun st => { st with depConstants := st.depConstants.union depConsts @@ -105,7 +104,7 @@ def withScopedName (n : Name) (b : Expr) (k : Name → TranslationM α) : Transl let mut n' := n let mut scopedNames := state.scopedNames while ← b.hasAnyFVar' (·.getUserName >>= (return · == n')) do - let i := scopedNames.findD n 1 + let i := scopedNames.getD n 1 n' := n.appendIndexAfter i scopedNames := scopedNames.insert n (i + 1) set { state with scopedNames := scopedNames } @@ -143,7 +142,7 @@ partial def applyTranslators? : Translator := withCache fun e => do return symbolT (← fv.getUserName).toString else modify fun st => { st with depFVars := st.depFVars.insert fv } - match (← get).uniqueFVarNames.find? fv with + match (← get).uniqueFVarNames[fv]? with | some n => return symbolT n | none => return symbolT (← fv.getUserName).toString | const nm _ => diff --git a/Smt/Translate/Bool.lean b/Smt/Translate/Bool.lean index 4520e107..f6c508ae 100644 --- a/Smt/Translate/Bool.lean +++ b/Smt/Translate/Bool.lean @@ -21,8 +21,12 @@ open Translator Term @[smt_translate] def translateBool : Translator := fun (e : Q(Bool)) => match e with | ~q(true) => return symbolT "true" | ~q(false) => return symbolT "false" + | ~q(!$x) => return appT (symbolT "not") (← applyTranslators! x) | ~q(($x : Bool) == $y) => return mkApp2 (symbolT "=") (← applyTranslators! x) (← applyTranslators! y) | ~q(($x : Bool) != $y) => return mkApp2 (symbolT "distinct") (← applyTranslators! x) (← applyTranslators! y) + | ~q($x && $y) => return mkApp2 (symbolT "and") (← applyTranslators! x) (← applyTranslators! y) + | ~q($x || $y) => return mkApp2 (symbolT "or") (← applyTranslators! x) (← applyTranslators! y) + | ~q($x ^^ $y) => return mkApp2 (symbolT "xor") (← applyTranslators! x) (← applyTranslators! y) | _ => return none @[smt_translate] def translateProp : Translator := fun (e : Q(Prop)) => match e with diff --git a/Smt/Translate/Query.lean b/Smt/Translate/Query.lean index b0314920..1e417d36 100644 --- a/Smt/Translate/Query.lean +++ b/Smt/Translate/Query.lean @@ -26,8 +26,8 @@ structure QueryBuilderM.Config where toDefine : List Expr := [] structure QueryBuilderM.State where - graph : Graph Expr Unit := .empty - commands : HashMap Expr Command := .empty + graph : Graph Expr Unit := {} + commands : Std.HashMap Expr Command := {} abbrev QueryBuilderM := ReaderT QueryBuilderM.Config <| StateT QueryBuilderM.State TranslationM @@ -159,7 +159,7 @@ def addCommandFor (e tp : Expr) : QueryBuilderM (Array Expr) := do -- Otherwise it is a local/global declaration with name `nm`. let nm ← match e with | fvar id .. => - match (← (get : TranslationM _)).uniqueFVarNames.find? id with + match (← (get : TranslationM _)).uniqueFVarNames[id]? with | some nm => pure nm | none => pure (← id.getUserName).toString | const n .. => pure n.toString @@ -251,12 +251,12 @@ def addCommand (cmd : Command) (cmds : List Command) : MetaM (List Command) := d | _ => pure () return cmds -def emitVertex (cmds : HashMap Expr Command) (e : Expr) : StateT (List Command) MetaM Unit := do +def emitVertex (cmds : Std.HashMap Expr Command) (e : Expr) : StateT (List Command) MetaM Unit := do trace[smt.translate.query] "emitting {e}" - let some cmd := cmds.find? e | throwError "no command was computed for {e}" + let some cmd := cmds[e]? | throwError "no command was computed for {e}" set (← addCommand cmd (← get)) -def generateQuery (goal : Expr) (hs : List Expr) (fvNames : HashMap FVarId String) : MetaM (List Command) := +def generateQuery (goal : Expr) (hs : List Expr) (fvNames : Std.HashMap FVarId String) : MetaM (List Command) := withTraceNode `smt.translate.query (fun _ => pure .nil) do trace[smt.translate.query] "Goal: {← inferType goal}" trace[smt.translate.query] "Provided Hints: {hs}" diff --git a/Smt/Util.lean b/Smt/Util.lean index 9c5ab4c2..cec045ee 100644 --- a/Smt/Util.lean +++ b/Smt/Util.lean @@ -54,8 +54,8 @@ def countConst (e : Expr) (c : Name) : Nat := visit e /-- Set of constants defined by SMT-LIB. -/ -def smtConsts : HashSet String := - List.foldr (fun c s => s.insert c) HashSet.empty +def smtConsts : Std.HashSet String := + List.foldr (fun c s => s.insert c) Std.HashSet.empty [ "=", "distinct", diff --git a/Test/BitVec/Add.lean b/Test/BitVec/Add.lean index d60e8f8d..2a7eb7a4 100644 --- a/Test/BitVec/Add.lean +++ b/Test/BitVec/Add.lean @@ -4,12 +4,9 @@ open BitVec example {x y : BitVec 4} : ¬(x = 11#4 ∧ y = 11#4 ∧ x + y = 15#4) := by smt - all_goals simp example {x y : BitVec 8} : ¬(x = 11#8 ∧ y = 11#8 ∧ x + y = 15#8) := by smt - all_goals simp example {x y : BitVec 16} : ¬(x = 11#16 ∧ y = 11#16 ∧ x + y = 15#16) := by smt - all_goals simp diff --git a/Test/BitVec/Shift.expected b/Test/BitVec/Shift.expected index 9d781ffb..88005d8d 100644 --- a/Test/BitVec/Shift.expected +++ b/Test/BitVec/Shift.expected @@ -1,16 +1,16 @@ goal: x ++ y = zeroExtend 4 x <<< 2#2 ||| zeroExtend 4 y query: -(declare-const y (_ BitVec 2)) (declare-const x (_ BitVec 2)) +(declare-const y (_ BitVec 2)) (assert (distinct (concat x y) (bvor (bvshl ((_ zero_extend 2) x) #b10) ((_ zero_extend 2) y)))) (check-sat) Test/BitVec/Shift.lean:5:8: warning: declaration uses 'sorry' goal: x ++ y = zeroExtend 6 x <<< 3#2 ||| zeroExtend 6 y query: -(declare-const y (_ BitVec 3)) (declare-const x (_ BitVec 3)) +(declare-const y (_ BitVec 3)) (assert (distinct (concat x y) (bvor (bvshl ((_ zero_extend 3) x) #b11) ((_ zero_extend 3) y)))) (check-sat) Test/BitVec/Shift.lean:10:8: warning: declaration uses 'sorry' diff --git a/Test/BitVec/XorComm.expected b/Test/BitVec/XorComm.expected index 6cd4a967..9d49feaf 100644 --- a/Test/BitVec/XorComm.expected +++ b/Test/BitVec/XorComm.expected @@ -1,8 +1,8 @@ goal: x ^^^ y = y ^^^ x query: -(declare-const y (_ BitVec 2)) (declare-const x (_ BitVec 2)) +(declare-const y (_ BitVec 2)) (assert (distinct (bvxor x y) (bvxor y x))) (check-sat) Test/BitVec/XorComm.lean:3:8: warning: declaration uses 'sorry' diff --git a/Test/Bool/Assoc.expected b/Test/Bool/Assoc.expected index 1934db2a..739b06a4 100644 --- a/Test/Bool/Assoc.expected +++ b/Test/Bool/Assoc.expected @@ -1,10 +1,10 @@ goal: (f p (f q r) == f (f p q) r) = true query: +(declare-const r Bool) +(declare-fun f (Bool Bool) Bool) (declare-const p Bool) (declare-const q Bool) -(declare-fun f (Bool Bool) Bool) -(declare-const r Bool) (assert (distinct (= (f p (f q r)) (f (f p q) r)) true)) (check-sat) Test/Bool/Assoc.lean:3:8: warning: declaration uses 'sorry' diff --git a/Test/Bool/Comm.expected b/Test/Bool/Comm.expected index 368f1f85..2bed275c 100644 --- a/Test/Bool/Comm.expected +++ b/Test/Bool/Comm.expected @@ -1,9 +1,9 @@ goal: (f p q == f q p) = true query: -(declare-const p Bool) -(declare-const q Bool) (declare-fun f (Bool Bool) Bool) +(declare-const q Bool) +(declare-const p Bool) (assert (distinct (= (f p q) (f q p)) true)) (check-sat) Test/Bool/Comm.lean:3:0: warning: declaration uses 'sorry' diff --git a/Test/Bool/Cong.expected b/Test/Bool/Cong.expected index f97fc612..c9a355fe 100644 --- a/Test/Bool/Cong.expected +++ b/Test/Bool/Cong.expected @@ -2,7 +2,7 @@ goal: (p == q) = true → (f p == f q) = true query: (declare-const p Bool) -(declare-fun f (Bool) Bool) (declare-const q Bool) +(declare-fun f (Bool) Bool) (assert (not (=> (= (= p q) true) (= (= (f p) (f q)) true)))) (check-sat) diff --git a/Test/Bool/HypotheticalSyllogism.expected b/Test/Bool/HypotheticalSyllogism.expected index 01b899e6..e9311b80 100644 --- a/Test/Bool/HypotheticalSyllogism.expected +++ b/Test/Bool/HypotheticalSyllogism.expected @@ -1,8 +1,8 @@ goal: (p = true → q = true) → (q = true → r = true) → p = true → r = true query: -(declare-const r Bool) (declare-const p Bool) +(declare-const r Bool) (declare-const q Bool) (assert (not (=> (=> (= p true) (= q true)) (=> (=> (= q true) (= r true)) (=> (= p true) (= r true)))))) (check-sat) diff --git a/Test/Bool/ModusPonens'.expected b/Test/Bool/ModusPonens'.expected index 12a42b63..26589d77 100644 --- a/Test/Bool/ModusPonens'.expected +++ b/Test/Bool/ModusPonens'.expected @@ -1,8 +1,8 @@ goal: q = true query: -(declare-const p Bool) (declare-const q Bool) +(declare-const p Bool) (assert (=> (= p true) (= q true))) (assert (= p true)) (assert (distinct q true)) diff --git a/Test/Bool/ModusPonens.expected b/Test/Bool/ModusPonens.expected index 5a811051..29ca7539 100644 --- a/Test/Bool/ModusPonens.expected +++ b/Test/Bool/ModusPonens.expected @@ -1,7 +1,7 @@ goal: p = true → (p = true → q = true) → q = true query: -(declare-const p Bool) (declare-const q Bool) +(declare-const p Bool) (assert (not (=> (= p true) (=> (=> (= p true) (= q true)) (= q true))))) (check-sat) diff --git a/Test/Bool/ModusTollens.expected b/Test/Bool/ModusTollens.expected index 4949c3f9..a6af2644 100644 --- a/Test/Bool/ModusTollens.expected +++ b/Test/Bool/ModusTollens.expected @@ -1,7 +1,7 @@ goal: (!q) = true → (p = true → q = true) → (!p) = true query: -(declare-const p Bool) (declare-const q Bool) +(declare-const p Bool) (assert (not (=> (= (not q) true) (=> (=> (= p true) (= q true)) (= (not p) true))))) (check-sat) diff --git a/Test/Bool/PropExt.expected b/Test/Bool/PropExt.expected index 1b077583..0869af7c 100644 --- a/Test/Bool/PropExt.expected +++ b/Test/Bool/PropExt.expected @@ -1,7 +1,7 @@ goal: (p = true) = (q = true) → (p == q) = true query: -(declare-const p Bool) (declare-const q Bool) +(declare-const p Bool) (assert (not (=> (= (= p true) (= q true)) (= (= p q) true)))) (check-sat) diff --git a/Test/Bool/Trans.expected b/Test/Bool/Trans.expected index 07da80d1..e329b3cb 100644 --- a/Test/Bool/Trans.expected +++ b/Test/Bool/Trans.expected @@ -1,8 +1,8 @@ goal: (p == q) = true → (q == r) = true → (p == r) = true query: -(declare-const q Bool) -(declare-const p Bool) (declare-const r Bool) +(declare-const p Bool) +(declare-const q Bool) (assert (not (=> (= (= p q) true) (=> (= (= q r) true) (= (= p r) true))))) (check-sat) diff --git a/Test/EUF/Issue100.expected b/Test/EUF/Issue100.expected index 89933759..70efa2e7 100644 --- a/Test/EUF/Issue100.expected +++ b/Test/EUF/Issue100.expected @@ -2,11 +2,11 @@ [smt] query: (set-logic ALL) - (declare-sort node 0) - (declare-sort round 0) (declare-sort value 0) - (declare-fun rel (node round round value) Bool) + (declare-sort round 0) + (declare-sort node 0) (declare-fun upd_rel (node round round value) Bool) + (declare-fun rel (node round round value) Bool) (assert (forall ((x node)) (forall ((x_1 round)) (forall ((x_2 round)) (forall ((x_3 value)) (= (upd_rel x x_1 x_2 x_3) (rel x x_1 x_2 x_3))))))) (assert (not true)) (check-sat) diff --git a/Test/Int/Binders.expected b/Test/Int/Binders.expected index 329a9ff7..151a05d0 100644 --- a/Test/Int/Binders.expected +++ b/Test/Int/Binders.expected @@ -19,7 +19,7 @@ Test/Int/Binders.lean:11:0: warning: declaration uses 'sorry' goal: partCurryAdd' a b = partCurryAdd' b a query: -(define-fun |partCurryAdd'| ((a Int) (a._@.Init.Prelude._hyg.2495 Int)) Int (+ a a._@.Init.Prelude._hyg.2495)) +(define-fun |partCurryAdd'| ((a Int) (a._@.Init.Prelude._hyg.2519 Int)) Int (+ a a._@.Init.Prelude._hyg.2519)) (declare-const a Int) (declare-const b Int) (assert (distinct (+ a b) (+ b a))) @@ -29,8 +29,8 @@ goal: mismatchNamesAdd a b = mismatchNamesAdd b a query: (define-fun mismatchNamesAdd ((a Int) (b Int)) Int (+ a b)) -(declare-const a Int) (declare-const b Int) +(declare-const a Int) (assert (distinct (mismatchNamesAdd a b) (mismatchNamesAdd b a))) (check-sat) Test/Int/Binders.lean:25:0: warning: declaration uses 'sorry' diff --git a/Test/Int/DefineSort.expected b/Test/Int/DefineSort.expected index 15e6649e..9c64cdd6 100644 --- a/Test/Int/DefineSort.expected +++ b/Test/Int/DefineSort.expected @@ -3,8 +3,8 @@ goal: a.add b = b.add a query: (define-sort MyInt () Int) (define-fun MyInt.add ((a MyInt) (b MyInt)) MyInt (+ a b)) -(declare-const a MyInt) (declare-const b MyInt) +(declare-const a MyInt) (assert (distinct (MyInt.add a b) (MyInt.add b a))) (check-sat) Test/Int/DefineSort.lean:6:0: warning: declaration uses 'sorry' diff --git a/Test/Int/Dvd.expected b/Test/Int/Dvd.expected index 3eee65e4..0c13c88d 100644 --- a/Test/Int/Dvd.expected +++ b/Test/Int/Dvd.expected @@ -3,8 +3,8 @@ goal: dvd a c = true query: (declare-fun dvd (Int Int) Bool) (assert (forall ((x Int)) (forall ((y Int)) (forall ((z Int)) (=> (= (dvd x y) true) (=> (= (dvd y z) true) (= (dvd x z) true))))))) -(declare-const b Int) (declare-const c Int) +(declare-const b Int) (assert (= (dvd b c) true)) (declare-const a Int) (assert (= (dvd a b) true)) diff --git a/Test/Int/DvdTimeout.expected b/Test/Int/DvdTimeout.expected index a78b96be..10b15bcf 100644 --- a/Test/Int/DvdTimeout.expected +++ b/Test/Int/DvdTimeout.expected @@ -1,9 +1,9 @@ goal: dvd a (b + c + d) = true query: -(declare-fun dvd (Int Int) Bool) (declare-const a Int) (declare-const d Int) +(declare-fun dvd (Int Int) Bool) (assert (= (dvd a d) true)) (declare-const c Int) (assert (= (dvd a c) true)) diff --git a/Test/Int/Let.expected b/Test/Int/Let.expected index cd2a1eac..b67f096c 100644 --- a/Test/Int/Let.expected +++ b/Test/Int/Let.expected @@ -19,7 +19,7 @@ goal: z 3 = 10 query: (declare-fun f (Int) Int) -(define-fun z ((x._@.Test.Int.Let._hyg.300 Int)) Int (f 10)) +(define-fun z ((x._@.Test.Int.Let._hyg.292 Int)) Int (f 10)) (assert (= (f 10) 10)) (assert (distinct (z 3) 10)) (check-sat) diff --git a/Test/Nat/Cong.expected b/Test/Nat/Cong.expected index e6bb14e7..e378911e 100644 --- a/Test/Nat/Cong.expected +++ b/Test/Nat/Cong.expected @@ -3,10 +3,10 @@ goal: x = y → f x = f y query: (define-sort Nat () Int) (declare-fun f (Nat) Nat) -(assert (forall ((_uniq.1004 Nat)) (=> (>= _uniq.1004 0) (>= (f _uniq.1004) 0)))) -(declare-const x Nat) -(assert (>= x 0)) +(assert (forall ((_uniq.965 Nat)) (=> (>= _uniq.965 0) (>= (f _uniq.965) 0)))) (declare-const y Nat) (assert (>= y 0)) +(declare-const x Nat) +(assert (>= x 0)) (assert (not (=> (= x y) (= (f x) (f y))))) (check-sat) diff --git a/Test/Nat/Max.expected b/Test/Nat/Max.expected index 968d9188..d65a6ede 100644 --- a/Test/Nat/Max.expected +++ b/Test/Nat/Max.expected @@ -2,12 +2,12 @@ goal: x ≤ x.max' y ∧ y ≤ x.max' y query: (define-sort Nat () Int) -(declare-const x Nat) -(assert (>= x 0)) (declare-fun |Nat.max'| (Nat Nat) Nat) -(assert (forall ((_uniq.1222 Nat)) (=> (>= _uniq.1222 0) (forall ((_uniq.1223 Nat)) (=> (>= _uniq.1223 0) (>= (|Nat.max'| _uniq.1222 _uniq.1223) 0)))))) +(assert (forall ((_uniq.1382 Nat)) (=> (>= _uniq.1382 0) (forall ((_uniq.1383 Nat)) (=> (>= _uniq.1383 0) (>= (|Nat.max'| _uniq.1382 _uniq.1383) 0)))))) (declare-const y Nat) (assert (>= y 0)) +(declare-const x Nat) +(assert (>= x 0)) (assert (not (and (<= x (|Nat.max'| x y)) (<= y (|Nat.max'| x y))))) (check-sat) goal: x ≤ x.max' y ∧ y ≤ x.max' y @@ -15,7 +15,7 @@ goal: x ≤ x.max' y ∧ y ≤ x.max' y query: (define-sort Nat () Int) (define-fun |Nat.max'| ((x Nat) (y Nat)) Nat (ite (<= x y) y x)) -(assert (forall ((_uniq.2539 Nat)) (=> (>= _uniq.2539 0) (forall ((_uniq.2540 Nat)) (=> (>= _uniq.2540 0) (>= (|Nat.max'| _uniq.2539 _uniq.2540) 0)))))) +(assert (forall ((_uniq.2960 Nat)) (=> (>= _uniq.2960 0) (forall ((_uniq.2961 Nat)) (=> (>= _uniq.2961 0) (>= (|Nat.max'| _uniq.2960 _uniq.2961) 0)))))) (declare-const x Nat) (assert (>= x 0)) (declare-const y Nat) diff --git a/Test/Nat/ZeroSub'.expected b/Test/Nat/ZeroSub'.expected index b0b6a7d2..28e17705 100644 --- a/Test/Nat/ZeroSub'.expected +++ b/Test/Nat/ZeroSub'.expected @@ -1,6 +1,6 @@ Test/Nat/ZeroSub'.lean:6:12: error: tactic 'assumption' failed case zero -_uniq✝⁴³⁸⁻⁰ : ¬Smt.Reconstruct.Builtin.distinct [0, 0] +_uniq✝⁴¹⁷⁻⁰ : ¬Smt.Reconstruct.Builtin.distinct [0, 0] ⊢ ¬Smt.Reconstruct.andN' [] ¬0 - 0 = 0 Test/Nat/ZeroSub'.lean:7:17: error: application type mismatch HAdd.hAdd x diff --git a/Test/String/Contains.expected b/Test/String/Contains.expected index c01ed4a5..6dc788ec 100644 --- a/Test/String/Contains.expected +++ b/Test/String/Contains.expected @@ -2,9 +2,9 @@ goal: "a".contains 'a' = true query: (declare-sort Char 0) +(declare-fun String.contains (String Char) Bool) (define-sort Nat () Int) (declare-fun Char.ofNat (Nat) Char) -(declare-fun String.contains (String Char) Bool) (assert (distinct (String.contains "a" (Char.ofNat (+ 96 1))) true)) (check-sat) Test/String/Contains.lean:3:8: warning: declaration uses 'sorry' diff --git a/Test/String/Length.expected b/Test/String/Length.expected index 2a63582b..b332e098 100644 --- a/Test/String/Length.expected +++ b/Test/String/Length.expected @@ -3,6 +3,6 @@ goal: "a".length = 1 query: (define-sort Nat () Int) (declare-fun String.length (String) Nat) -(assert (forall ((_uniq.805 String)) (>= (String.length _uniq.805) 0))) +(assert (forall ((_uniq.786 String)) (>= (String.length _uniq.786) 0))) (assert (distinct (String.length "a") 1)) (check-sat) diff --git a/Test/linarith.expected b/Test/linarith.expected index 45481b77..cf024286 100644 --- a/Test/linarith.expected +++ b/Test/linarith.expected @@ -1,3 +1,21 @@ +Test/linarith.lean:10:0: error: application type mismatch + @Smt.Reconstruct.Real.int_tight_ub 1 +argument has type + ℤ +but function has type + ∀ {c : ℝ} {i : ℤ}, ↑i < c → i ≤ ⌊c⌋ +Test/linarith.lean:19:0: error: application type mismatch + @Smt.Reconstruct.Real.int_tight_ub 0 +argument has type + ℤ +but function has type + ∀ {c : ℝ} {i : ℤ}, ↑i < c → i ≤ ⌊c⌋ +Test/linarith.lean:22:0: error: application type mismatch + @Smt.Reconstruct.Real.int_tight_ub 0 +argument has type + ℤ +but function has type + ∀ {c : ℝ} {i : ℤ}, ↑i < c → i ≤ ⌊c⌋ Test/linarith.lean:34:9: warning: unused variable `e` note: this linter can be disabled with `set_option linter.unusedVariables false` Test/linarith.lean:53:0: warning: declaration uses 'sorry' @@ -19,3 +37,9 @@ Test/linarith.lean:168:34: warning: unused variable `z` note: this linter can be disabled with `set_option linter.unusedVariables false` Test/linarith.lean:169:5: warning: unused variable `h5` note: this linter can be disabled with `set_option linter.unusedVariables false` +Test/linarith.lean:173:0: error: application type mismatch + @Smt.Reconstruct.Real.int_tight_ub 0 +argument has type + ℤ +but function has type + ∀ {c : ℝ} {i : ℤ}, ↑i < c → i ≤ ⌊c⌋ diff --git a/lake-manifest.json b/lake-manifest.json index 87888d6c..64ecf4f2 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,17 +15,17 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4756e0fc48acce0cc808df0ad149de5973240df6", + "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9", + "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "28fa80508edc97d96ed6342c9a771a67189e0baa", + "rev": "5f934891e11d70a1b86e302fdf9cecfc21e8de46", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -45,16 +45,16 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c", + "rev": "23268f52d3505955de3c26a42032702c25cfcbf8", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.42", + "inputRev": "v0.0.44", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "scope": "", + "scope": "leanprover", "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0", "name": "Cli", "manifestFile": "lake-manifest.json", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1", + "rev": "984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -75,20 +75,30 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2ba60fa2c384a94735454db11a2d523612eaabff", + "rev": "7bedaed1ef024add1e171cc17706b012a9a37802", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "d212dd74414e997653cd3484921f4159c955ccca", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", - "rev": "809c3fb3b5c8f5d7dace56e200b426187516535a", + "rev": "d7317655e2826dc1f1de9a0c138db2775c4bb841", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.12.0", + "inputRev": "v4.13.0", "inherited": false, "configFile": "lakefile.lean"}], "name": "smt", diff --git a/lakefile.lean b/lakefile.lean index cc23bc9a..fc11d19e 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -6,7 +6,7 @@ require cvc5 from git "https://github.com/abdoo8080/lean-cvc5.git" @ "c97ff4cfc218c11af8c1598b8225a6fcc094f5cd" require mathlib from - git "https://github.com/leanprover-community/mathlib4.git" @ "v4.12.0" + git "https://github.com/leanprover-community/mathlib4.git" @ "v4.13.0" def libcpp : String := if System.Platform.isWindows then "libstdc++-6.dll" @@ -14,7 +14,6 @@ def libcpp : String := else "libstdc++.so.6" package smt where - precompileModules := true moreLeanArgs := #[s!"--load-dynlib={libcpp}"] moreGlobalServerArgs := #[s!"--load-dynlib={libcpp}"] @@ -72,11 +71,10 @@ script test do where runTest (test : FilePath) (expected : FilePath) : ScriptM UInt32 := do IO.println s!"Start : {test}" - let imports ← Lean.parseImports' (← IO.FS.readFile test) test.fileName.get! - let modules ← imports.filterMapM (findModule? ·.module) + let some cvc5 ← findModule? ``cvc5 | return 2 let out ← IO.Process.output { cmd := (← getLean).toString - args := #[s!"--load-dynlib={libcpp}"] ++ modules.map (s!"--load-dynlib={·.dynlibFile}") ++ #[test.toString] + args := #[s!"--load-dynlib={libcpp}", s!"--load-dynlib={cvc5.dynlibFile}"] ++ #[test.toString] env := ← getAugmentedEnv } let expected ← IO.FS.readFile expected @@ -116,11 +114,10 @@ where updateTest (test : FilePath) : ScriptM UInt32 := do let expected := test.withExtension "expected" IO.println s!"Start : {test}" - let imports ← Lean.parseImports' (← IO.FS.readFile test) test.fileName.get! - let modules ← imports.filterMapM (findModule? ·.module) + let some cvc5 ← findModule? ``cvc5 | return 2 let out ← IO.Process.output { cmd := (← getLean).toString - args := #[s!"--load-dynlib={libcpp}"] ++ modules.map (s!"--load-dynlib={·.dynlibFile}") ++ #[test.toString] + args := #[s!"--load-dynlib={libcpp}", s!"--load-dynlib={cvc5.dynlibFile}"] ++ #[test.toString] env := ← getAugmentedEnv } IO.FS.writeFile expected out.stdout @@ -137,12 +134,11 @@ Use Firefox Profiler UI to view profiling information. script profile args do let file : FilePath := args[0]! let log : FilePath := args[1]! - let imports ← Lean.parseImports' (← IO.FS.readFile file) file.fileName.get! - let modules ← imports.filterMapM (findModule? ·.module) + let some cvc5 ← findModule? ``cvc5 | return 2 let s ← IO.Process.run { cmd := (← getLean).toString - args := #[s!"--load-dynlib={libcpp}"] ++ modules.map (s!"--load-dynlib={·.dynlibFile}") ++ - #["-Dtrace.profiler=true", s!"-Dtrace.profiler.output={log}"] ++ #[file.toString] + args := #[s!"--load-dynlib={libcpp}", s!"--load-dynlib={cvc5.dynlibFile}", + "-Dtrace.profiler=true", s!"-Dtrace.profiler.output={log}", file.toString] env := ← getAugmentedEnv } IO.println s diff --git a/lean-toolchain b/lean-toolchain index 89985206..4f86f953 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.12.0 +leanprover/lean4:v4.13.0