From a6830f90ab365e14ccb7ca31201de37f8c1e978c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Fri, 20 Sep 2024 13:47:35 +0200 Subject: [PATCH] chore: basic cleanups for bv_decide (#5408) --- .../Tactic/BVDecide/Frontend/BVDecide.lean | 20 +++++++++---------- .../Elab/Tactic/BVDecide/Frontend/LRAT.lean | 5 +++-- .../BVDecide/Bitblast/BVExpr/Basic.lean | 6 +++--- 3 files changed, 16 insertions(+), 15 deletions(-) diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean index 3e1214ab9bb4..8b455b8ecd19 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean @@ -35,7 +35,7 @@ Reconstruct bit by bit which value expression must have had which `BitVec` value expression - pair values. -/ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Array (Bool × Nat)) - (aigSize : Nat) (atomsAssignment : Std.HashMap Nat Expr) : + (aigSize : Nat) (atomsAssignment : Std.HashMap Nat (Nat × Expr)) : Array (Expr × BVExpr.PackedBitVec) := Id.run do let mut sparseMap : Std.HashMap Nat (RBMap Nat Bool Ord.compare) := {} for (bitVar, cnfVar) in var2Cnf.toArray do @@ -70,7 +70,7 @@ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Ar if bitValue then value := value ||| (1 <<< currentBit) currentBit := currentBit + 1 - let atomExpr := atomsAssignment.get! bitVecVar + let atomExpr := atomsAssignment.get! bitVecVar |>.snd finalMap := finalMap.push (atomExpr, ⟨BitVec.ofNat currentBit value⟩) return finalMap @@ -83,14 +83,14 @@ structure UnsatProver.Result where proof : Expr lratCert : LratCert -abbrev UnsatProver := ReflectionResult → Std.HashMap Nat Expr → MetaM UnsatProver.Result +abbrev UnsatProver := ReflectionResult → Std.HashMap Nat (Nat × Expr) → MetaM UnsatProver.Result /-- Contains values that will be used to diagnose spurious counter examples. -/ structure DiagnosisInput where unusedHypotheses : Std.HashSet FVarId - atomsAssignment : Std.HashMap Nat Expr + atomsAssignment : Std.HashMap Nat (Nat × Expr) /-- The result of a spurious counter example diagnosis. @@ -104,14 +104,14 @@ abbrev DiagnosisM : Type → Type := ReaderT DiagnosisInput <| StateRefT Diagnos namespace DiagnosisM def run (x : DiagnosisM Unit) (unusedHypotheses : Std.HashSet FVarId) - (atomsAssignment : Std.HashMap Nat Expr) : MetaM Diagnosis := do + (atomsAssignment : Std.HashMap Nat (Nat × Expr)) : MetaM Diagnosis := do let (_, issues) ← ReaderT.run x { unusedHypotheses, atomsAssignment } |>.run {} return issues def unusedHyps : DiagnosisM (Std.HashSet FVarId) := do return (← read).unusedHypotheses -def atomsAssignment : DiagnosisM (Std.HashMap Nat Expr) := do +def atomsAssignment : DiagnosisM (Std.HashMap Nat (Nat × Expr)) := do return (← read).atomsAssignment def addUninterpretedSymbol (e : Expr) : DiagnosisM Unit := @@ -131,7 +131,7 @@ Diagnose spurious counter examples, currently this checks: - Whether all hypotheses which contain any variable that was bitblasted were included -/ def diagnose : DiagnosisM Unit := do - for (_, expr) in ← atomsAssignment do + for (_, (_, expr)) in ← atomsAssignment do match_expr expr with | BitVec.ofBool x => match x with @@ -158,7 +158,7 @@ def explainers : List (Diagnosis → Option MessageData) := [uninterpretedExplainer, unusedRelevantHypothesesExplainer] def explainCounterExampleQuality (unusedHypotheses : Std.HashSet FVarId) - (atomsAssignment : Std.HashMap Nat Expr) : MetaM MessageData := do + (atomsAssignment : Std.HashMap Nat (Nat × Expr)) : MetaM MessageData := do let diagnosis ← DiagnosisM.run DiagnosisM.diagnose unusedHypotheses atomsAssignment let folder acc explainer := if let some m := explainer diagnosis then acc.push m else acc let explanations := explainers.foldl (init := #[]) folder @@ -172,7 +172,7 @@ def explainCounterExampleQuality (unusedHypotheses : Std.HashSet FVarId) return err def lratBitblaster (cfg : TacticContext) (reflectionResult : ReflectionResult) - (atomsAssignment : Std.HashMap Nat Expr) : + (atomsAssignment : Std.HashMap Nat (Nat × Expr)) : MetaM UnsatProver.Result := do let bvExpr := reflectionResult.bvExpr let entry ← @@ -242,7 +242,7 @@ def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) : reflectBV g trace[Meta.Tactic.bv] "Reflected bv logical expression: {reflectionResult.bvExpr}" - let atomsPairs := (← getThe State).atoms.toList.map (fun (expr, _, ident) => (ident, expr)) + let atomsPairs := (← getThe State).atoms.toList.map (fun (expr, ⟨width, ident⟩) => (ident, (width, expr))) let atomsAssignment := Std.HashMap.ofList atomsPairs let ⟨bvExprUnsat, cert⟩ ← unsatProver reflectionResult atomsAssignment let proveFalse ← reflectionResult.proveFalse bvExprUnsat diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean index 8bc6b1ae4a79..4a262b9a8c9d 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/LRAT.lean @@ -141,10 +141,11 @@ This will obtain an `LratCert` if the formula is UNSAT and throw errors otherwis def runExternal (cnf : CNF Nat) (solver : System.FilePath) (lratPath : System.FilePath) (trimProofs : Bool) (timeout : Nat) (binaryProofs : Bool) : MetaM (Except (Array (Bool × Nat)) LratCert) := do - IO.FS.withTempFile fun _ cnfPath => do + IO.FS.withTempFile fun cnfHandle cnfPath => do withTraceNode `sat (fun _ => return "Serializing SAT problem to DIMACS file") do -- lazyPure to prevent compiler lifting - IO.FS.writeFile cnfPath (← IO.lazyPure (fun _ => cnf.dimacs)) + cnfHandle.putStr (← IO.lazyPure (fun _ => cnf.dimacs)) + cnfHandle.flush let res ← withTraceNode `sat (fun _ => return "Running SAT solver") do diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean index baa49040ce0f..bec9884cdd93 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean @@ -142,8 +142,8 @@ def toString : BVUnOp → String | not => "~" | shiftLeftConst n => s!"<< {n}" | shiftRightConst n => s!">> {n}" - | rotateLeft n => s! "rotL {n}" - | rotateRight n => s! "rotR {n}" + | rotateLeft n => s!"rotL {n}" + | rotateRight n => s!"rotR {n}" | arithShiftRightConst n => s!">>a {n}" instance : ToString BVUnOp := ⟨toString⟩ @@ -238,7 +238,7 @@ def toString : BVExpr w → String | .var idx => s!"var{idx}" | .const val => ToString.toString val | .zeroExtend v expr => s!"(zext {v} {expr.toString})" - | .extract hi lo expr => s!"{expr.toString}[{hi}:{lo}]" + | .extract start len expr => s!"{expr.toString}[{start}, {len}]" | .bin lhs op rhs => s!"({lhs.toString} {op.toString} {rhs.toString})" | .un op operand => s!"({op.toString} {toString operand})" | .append lhs rhs => s!"({toString lhs} ++ {toString rhs})"