Support unsat-core and counter-examples.

Author: abdoo8080

.github/workflows/ci.yml

@@ -30,6 +30,6 @@ jobs:
     - name: Build and Test Lean-SMT
       run: |
         lake update
-        lake build Smt Smt.Auto Smt.Rat Smt.Real
+        lake build Smt Smt.Rat Smt.Real
         lake run test
       shell: bash

Smt/Options.lean

@@ -14,6 +14,7 @@ open Lean
 initialize
   registerTraceClass `smt
   registerTraceClass `smt.attr
+  registerTraceClass `smt.preprocess
   registerTraceClass `smt.translate
   registerTraceClass `smt.translate.expr
   registerTraceClass `smt.translate.query

Smt/Preprocess.lean

@@ -6,3 +6,5 @@ Authors: Abdalrhman Mohamed, Tomaz Gomes Mascarenhas
 -/
 
 import Smt.Preprocess.Iff
+import Smt.Preprocess.Mono
+import Smt.Preprocess.PushHintsToCtx

Smt/Preprocess/Basic.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2021-2024 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Abdalrhman Mohamed
+-/
+
+import Lean.Meta.Basic
+import Lean.Meta.InferType
+
+namespace Smt.Preprocess
+
+open Lean
+
+structure Result where
+  map : Std.HashMap Expr (Array Expr)
+  hs : Array Expr
+  mv : MVarId
+
+/-- Return all propositions in the local context. -/
+def getPropHyps : MetaM (Array FVarId) := do
+  let mut result := #[]
+  for localDecl in (← getLCtx) do
+    unless localDecl.isImplementationDetail do
+      if ← pure !(isNonEmpty localDecl.type) <&&> Meta.isProp localDecl.type then
+        result := result.push localDecl.fvarId
+  return result
+where
+  isNonEmpty (e : Expr) : Bool :=
+  match_expr e with
+  | Nonempty _ => true
+  | _ => false
+
+end Smt.Preprocess

Smt/Preprocess/Iff.lean

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Abdalrhman Mohamed, Tomaz Gomes Mascarenhas
 -/
 
-import Lean
+import Smt.Preprocess.Basic
 import Qq
 
 namespace Smt.Preprocess
@@ -27,43 +27,46 @@ def replaceIff (e : Expr) : MetaM Expr :=
 def containsIff (e : Expr) : Bool :=
   (Expr.const ``Iff []).occurs e
 
-def elimIff (mv : MVarId) (hs : List Expr) : MetaM (List Expr × MVarId) := mv.withContext do
+def elimIff (mv : MVarId) (hs : Array Expr) : MetaM Result := mv.withContext do
   let t ← instantiateMVars (← mv.getType)
   let ts ← hs.mapM (Meta.inferType · >>= instantiateMVars)
   if !(containsIff t || ts.any containsIff) then
-    return (hs, mv)
+    return { map := Std.HashMap.insertMany ∅ (hs.zip (hs.map .singleton)), hs, mv }
   let simpTheorems ← #[``eq_self, ``iff_eq_eq].foldlM (·.addConst ·) ({} : Meta.SimpTheorems)
   let simpTheorems := #[simpTheorems]
   let congrTheorems ← Meta.getSimpCongrTheorems
   let ctx ← Meta.Simp.mkContext {} simpTheorems congrTheorems
-  let (hs, mv) ← elimIffLocalDecls mv hs ctx
-  let mv ← elimIffTarget mv ctx
-  return (hs, mv)
+  let (hs', mv') ← elimIffLocalDecls mv hs.toList ctx #[]
+  let mv' ← elimIffTarget mv' ctx
+  return { map := Std.HashMap.insertMany ∅ (hs'.zip (hs.map .singleton)), hs := hs', mv := mv' }
 where
-  elimIffLocalDecls mv hs ctx := mv.withContext do
-    let mut newHs := []
-    let mut toAssert := #[]
-    for h in hs do
+  elimIffLocalDecls mv hs ctx hs' := do match hs with
+    | [] => return (hs', mv)
+    | h :: hs =>
       let type ← Meta.inferType h
       let eq ← replaceIff (← instantiateMVars type)
       let (_, l, r) := eq.eq?.get!
       if l == r then
-        newHs := h :: newHs
+        elimIffLocalDecls mv hs ctx (hs'.push h)
       else
-        let userName ← if h.isFVar then h.fvarId!.getUserName else Lean.mkFreshId
-        let type := r
-        let (r, _) ←  Meta.simp eq ctx
-        let value ←  Meta.mkAppM ``eq_resolve #[h, ← Meta.mkOfEqTrue (← r.getProof)]
-        toAssert := toAssert.push { userName, type, value }
-    let (fvs, mv) ← mv.assertHypotheses toAssert
-    newHs := newHs.reverse ++ (fvs.map (.fvar ·)).toList
-    return (newHs, mv)
+        let (res, _) ← Meta.simp eq ctx
+        let h' := mkApp4 (.const ``eq_resolve []) l r h (mkOfEqTrue eq (← res.getProof))
+        if let .some fv := h.fvarId? then
+          let res ← mv.replace fv h' (.some r)
+          let hs' := hs'.map res.subst.apply
+          let hs := hs.map res.subst.apply
+          res.mvarId.withContext (elimIffLocalDecls res.mvarId hs ctx (hs'.push (.fvar res.fvarId)))
+        else
+          elimIffLocalDecls mv hs ctx (hs'.push h')
+      termination_by hs.length
   elimIffTarget mv ctx := mv.withContext do
     let eq ← replaceIff (← instantiateMVars (← mv.getType))
-    let (r, _) ←  Meta.simp eq ctx
-    if r.expr.isTrue then
-      mv.replaceTargetEq eq.appArg! (← Meta.mkOfEqTrue (← r.getProof))
+    let (res, _) ← Meta.simp eq ctx
+    if res.expr.isTrue then
+      mv.replaceTargetEq eq.appArg! (mkOfEqTrue eq (← res.getProof))
     else
       return mv
+  mkOfEqTrue p hpt :=
+    mkApp2 (.const ``of_eq_true []) p hpt
 
 end Smt.Preprocess

Smt/Auto.lean Smt/Preprocess/Mono.leanSmt/Auto.lean renamed to Smt/Preprocess/Mono.lean

@@ -6,11 +6,18 @@ Authors: Abdalrhman Mohamed
 -/
 
 import Auto.Tactic
+import Smt.Preprocess.Basic
 
 namespace Auto
 
 open Lean Elab Embedding.Lam
 
+def DTr.contains (self : DTr) (other : DTr) : Bool :=
+  if self == other then true
+  else match self with
+    | .leaf _ => false
+    | .node _ dtrs => dtrs.attach.any fun ⟨dtr, _⟩ => dtr.contains other
+
 structure InputHints' where
   lemmas   : Array Lemma := #[]
   lemdbs   : Array Name  := #[]
@@ -147,7 +154,7 @@ def mono' (declName? : Option Name) (mv : MVarId) (hints : InputHints') (unfoldI
       let f (acc : MessageData) (dtr : FVarId × DTr) :=
         acc ++ m!"\n<{Expr.fvar dtr.fst}> = <{ToString.toString dtr.snd}>"
       let message : MessageData := dtrs.foldl f m!""
-      trace[smt] "dtrs: {message}"
+      trace[smt.preprocess] "dtrs: {message}"
       let (_, mv) ← mvarId.assertHypotheses hs
       absurd.assign proof
       return (mv, dtrs)
@@ -182,3 +189,40 @@ open Lean Elab Tactic in
   | _ => throwUnsupportedSyntax
 
 end Auto.Tactic
+
+namespace Smt.Preprocess
+
+open Lean
+
+open Auto in
+def hintsToAutoHints (hs : Array Expr) : MetaM (Std.HashMap DTr Expr × InputHints' × Array Prep.ConstUnfoldInfo × Array Name) := do
+  let lemmas ← hs.mapM inferLemma
+  let map := .ofList (lemmas.map (fun l => (l.deriv, l.proof))).toList
+  return (map, ⟨lemmas, #[], false⟩, #[], #[])
+where
+  inferLemma (e : Expr) : MetaM Lemma := do
+    let paramNames ← getLevelParamNames e
+    return Lemma.mk ⟨e, ← Meta.inferType e, (.node "smtHint" #[.leaf s!"{e}"])⟩ paramNames
+  getLevelParamNames {ω : Type} {m} [STWorld ω m] [MonadLiftT (ST ω) m] [Monad m] (e : Expr) : m (Array Name) := do
+    let ((), names) ← (e.forEach getLevelParamName).run (m := m) {}
+    return names.toArray
+  getLevelParamName {m} [Monad m] (e : Expr) : StateT (Std.HashSet Name) m Unit := do
+    match e with
+    | .const _ lvls =>
+      let names := lvls.filterMap fun lvl => do
+        let .param name := lvl | none
+        some name
+      modify fun s => s.insertMany names
+    | _ => return
+
+def mono (mv : MVarId) (hs : Array Expr) : MetaM Result := do
+  let (invMap, hints, unfoldInfos, defeqNames) ← hintsToAutoHints hs
+  let (mv, dtrs) ← Auto.mono' `smt mv hints unfoldInfos defeqNames
+  let map := dtrs.foldl (init := {}) fun map (fv, dtr) =>
+    let usedHints := invMap.filter (fun k _ => dtr.contains k)
+    map.insert (.fvar fv) usedHints.valuesArray
+  let hs ← mv.withContext (return (← getPropHyps).map Expr.fvar)
+  trace[smt.preprocess] "goal: {mv}"
+  return { map, hs, mv }
+
+end Smt.Preprocess

Smt/Preprocess/PushHintsToCtx.lean

@@ -0,0 +1,27 @@
+/-
+Copyright (c) 2021-2024 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Abdalrhman Mohamed
+-/
+
+import Smt.Preprocess.Basic
+import Lean.Meta.Tactic.Assert
+
+namespace Smt.Preprocess
+
+open Lean
+
+def pushHintsToCtx (mv : MVarId) (hs : Array Expr) : MetaM Result := do
+  hs.foldrM pushHint { map := {}, hs := #[], mv }
+where
+  pushHint (h : Expr) (r : Result) : MetaM Result := do
+    if h.isFVar || h.isConst then
+      return { r with map := r.map.insert h #[h], hs := r.hs.push h }
+    else
+      let mv' ← r.mv.assert (← mkFreshId) (← Meta.inferType h) h
+      let ⟨fv, mv'⟩ ← mv'.intro1
+      let h' := .fvar fv
+      return { map := r.map.insert h' #[h], hs := r.hs.push h', mv := mv' }
+
+end Smt.Preprocess

Smt/Reconstruct.lean

@@ -215,35 +215,51 @@ partial def reconstructProof (pf : cvc5.Proof) (ctx : Reconstruct.Context) :
   else
     return (dfns, ps, p, h, mvs.toList)
 
+inductive cvc5Result where
+  | sat (model : Array (cvc5.Term × cvc5.Term))
+  | unsat (pf : cvc5.Proof) (uc : Array cvc5.Term)
+  | unknown (reason : cvc5.UnknownExplanation)
+
 open cvc5 in
-def traceSolve (r : Except Exception (Except SolverError Proof)) : MetaM MessageData :=
+def traceSolve (r : Except Exception (Except Error cvc5Result)) : MetaM MessageData :=
   return match r with
   | .ok (.ok _) => m!"{checkEmoji}"
   | _           => m!"{bombEmoji}"
 
 open cvc5 in
-def solve (query : String) (timeout : Option Nat) : MetaM (Except Error cvc5.Proof) :=
-  profileitM Exception "simp" {} do
+def solve (query : String) (timeout : Option Nat) : MetaM (Except cvc5.Error cvc5Result) :=
+  profileitM Exception "smt" {} do
   withTraceNode `smt.solve traceSolve do Solver.run (← TermManager.new) do
     if let .some timeout := timeout then
       Solver.setOption "tlimit" (toString (1000*timeout))
     Solver.setOption "dag-thresh" "0"
     Solver.setOption "simplification" "none"
     Solver.setOption "enum-inst" "true"
+    Solver.setOption "enum-inst-interleave" "true"
     Solver.setOption "cegqi-midpoint" "true"
     Solver.setOption "produce-models" "true"
     Solver.setOption "produce-proofs" "true"
     Solver.setOption "proof-elim-subtypes" "true"
     Solver.setOption "proof-granularity" "dsl-rewrite"
-    Solver.parseCommands query
-    let r ← Solver.checkSat
-    trace[smt.solve] m!"result: {r}"
-    if r.isUnsat then
+    let vs ← Solver.parseCommands query
+    let res ← Solver.checkSat
+    trace[smt.solve] m!"result: {res}"
+    if res.isSat then
+      let ts ← Solver.getValues vs
+      trace[smt.solve] "unsat-core:\n{vs.zip ts}"
+      return .sat (vs.zip ts)
+    else if res.isUnsat then
       let ps ← Solver.getProof
+      let uc ← Solver.getUnsatCore
       if h : 0 < ps.size then
         trace[smt.solve] "proof:\n{← Solver.proofToString ps[0]}"
-        return ps[0]
-    throw (self := instMonadExceptOfMonadExceptOf _ _) (Error.error s!"Expected unsat, got {r}")
+        trace[smt.solve] "unsat-core:\n{uc}"
+        return .unsat ps[0] uc
+    else if res.isUnknown then
+      let reason := res.getUnknownExplanation
+      trace[smt.solve] "unknown-reason:\n{reason}"
+      return .unknown reason
+    throwError s!"unexpected check-sat result {res}"
 
 syntax (name := reconstruct) "reconstruct" str : tactic
 
@@ -253,8 +269,10 @@ open Lean.Elab Tactic in
     let some query := stx[1].isStrLit? | throwError "expected string"
     let r ← solve query none
     match r with
-      | .error e => logInfo (repr e)
-      | .ok pf =>
+      | .error e => throwError e.toString
+      | .ok (.sat _) => throwError "expected unsat result"
+      | .ok (.unknown r) => logInfo (repr r)
+      | .ok (.unsat pf _) =>
         let (_, _, p, hp, mvs) ← reconstructProof pf ⟨(← getUserNames), false⟩
         let mv ← Tactic.getMainGoal
         let mv ← mv.assert (Name.num `s 0) p hp

Smt/Reconstruct/Builtin.lean

@@ -63,7 +63,8 @@ where
   | .ITE =>
     let (u, (α : Q(Sort u))) ← reconstructSortLevelAndSort t.getSort
     let c : Q(Prop) ← reconstructTerm t[0]!
-    let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c)
+    let oh : Option Q(Decidable $c) ← Meta.synthInstance? q(Decidable $c)
+    let h : Q(Decidable $c) := oh.getD q(Classical.propDecidable $c)
     let x : Q($α) ← reconstructTerm t[1]!
     let y : Q($α) ← reconstructTerm t[2]!
     return q(@ite $α $c $h $x $y)