setting up test configuration

Auto/EvaluateAuto/TestCode.lean

@@ -27,18 +27,38 @@ instance : ToMessageData Result where
   | .typeUnequal     => "Result.typeUnequal"
   | .autoException e => m!"Result.autoException ::\n{e.toMessageData}"
 
+inductive SolverConfig where
+  | native
+  | leanSmt
+  | smt (solverName : Solver.SMT.SolverName)
+  | tptp (solverName : Solver.TPTP.SolverName) (path : String)
+
+instance : ToString SolverConfig where
+  toString : SolverConfig → String
+  | .native       => "native"
+  | .leanSmt      => "leanSmt"
+  | .smt sn       => s!"smt {sn}"
+  | .tptp sn path => s!"tptp {sn} {path}"
+
 structure EvalConfig where
+  /-- Timeout for native prover, e.g. Duper and Lean-smt -/
   maxHeartbeats : Nat           := 65536
+  /-- Timeout for external provers, i.e. TPTP solvers and SMT solvers -/
+  timeout       : Nat           := 10
+  /-- Solver configuration -/
+  solverConfig  : SolverConfig
+  /-- Optional logfile for saving the result of the evaluation -/
   logFile       : Option String := .none
 
 instance : ToString EvalConfig where
   toString : EvalConfig → String
-  | ⟨maxHeartbeats, logFile⟩ =>
+  | ⟨maxHeartbeats, timeout, solverConfig, logFile⟩ =>
     let logFileStr :=
       match logFile with
       | .some logFile => s!", logFile := {logFile}"
       | .none => ""
-    s!"\{maxHeartbeats := {maxHeartbeats}{logFileStr}}"
+    s!"\{maxHeartbeats := {maxHeartbeats}, timeout := {timeout}, " ++
+    s!"solverConfig = {solverConfig}{logFileStr}}"
 
 /--
   Run `Lean-auto` on `lem.type`, using premises collected from `lem.proof`
@@ -91,6 +111,12 @@ def runAutoOnConst (name : Name) : CoreM Result := do
   let lemmaV := {lemmaPre with proof := v}
   runAutoOnAutoLemma (.some name) lemmaV
 
+def disableAllSolvers (o : Options) : Options :=
+  let o := auto.native.set o false
+  let o := auto.smt.set o false
+  let o := auto.tptp.set o false
+  o
+
 def runAutoOnConsts (config : EvalConfig) (names : Array Name) : CoreM Unit := do
   let logFileHandle : Option IO.FS.Handle ← config.logFile.mapM (fun fname => IO.FS.Handle.mk fname .write)
   trace[auto.eval.printConfig] m!"Config = {config}"
@@ -102,10 +128,35 @@ def runAutoOnConsts (config : EvalConfig) (names : Array Name) : CoreM Unit := d
     if let .some fhandle := logFileHandle then
       fhandle.putStrLn ""
       fhandle.putStrLn s!"Testing || {name} : {← (Lean.Meta.ppExpr ci.type).run'}"
-    let result ←
-      withReader (fun ctx => {ctx with maxHeartbeats := config.maxHeartbeats * 1000}) <|
-        withCurrHeartbeats <| do
-          runAutoOnConst name
+    let result : Result ←
+      match config.solverConfig with
+      | .native    =>
+        withOptions (fun o =>
+          let o := disableAllSolvers o
+          let o := auto.native.set o true
+          o) <|
+          withReader (fun ctx => {ctx with maxHeartbeats := config.maxHeartbeats * 1000}) <|
+            withCurrHeartbeats <| runAutoOnConst name
+      | .leanSmt  =>
+        throwError "Lean-SMT is currently not supported"
+      | .smt sn   =>
+        withOptions (fun o =>
+          let o := disableAllSolvers o
+          let o := auto.smt.set o true
+          let o := auto.smt.solver.name.set o sn
+          let o := auto.smt.trust.set o true
+          o) <| runAutoOnConst name
+      | .tptp sn path =>
+        withOptions (fun o =>
+          let o := disableAllSolvers o
+          let o := auto.tptp.set o true
+          let o := auto.tptp.solver.name.set o sn
+          match sn with
+          | .zipperposition => auto.tptp.zipperposition.path.set o path
+          | .zeport _       => auto.tptp.eproverHo.path.set o path
+          | .eproverHo      => auto.tptp.zeport.path.set o path
+          | .vampire        => auto.tptp.vampire.path.set o path) <|
+            runAutoOnConst name
     trace[auto.eval.printResult] m!"{result}"
     if let .some fhandle := logFileHandle then
       fhandle.putStrLn (toString (← MessageData.format m!"{result}"))

Auto/Solver/SMT.lean

@@ -52,9 +52,6 @@ register_option auto.smt.rconsProof : Bool := {
 
 namespace Auto
 
-open IR.SMT
-open Parser.SMTSexp
-
 namespace Solver.SMT
 
 inductive SolverName where
@@ -80,11 +77,19 @@ instance : Lean.KVMap.Value SolverName where
   | "cvc5" => some .cvc5
   | _      => none
 
+end Auto.Solver.SMT
+
+open Auto.Solver.SMT in
 register_option auto.smt.solver.name : SolverName := {
   defValue := SolverName.z3
   descr := "Name of the designated SMT solver. Use `none` to disable solver querying."
 }
 
+namespace Auto.Solver.SMT
+
+open IR.SMT
+open Parser.SMTSexp
+
 abbrev SolverProc := IO.Process.Child ⟨.piped, .piped, .piped⟩
 
 private def emitCommand (p : SolverProc) (c : IR.SMT.Command) : IO Unit := do

Auto/Solver/TPTP.lean

@@ -43,6 +43,7 @@ inductive SolverName where
   | zeport (zept : ZEPortType)
   -- E prover, higher-order version
   | eproverHo
+  | vampire
 deriving BEq, Hashable, Inhabited
 
 instance : ToString SolverName where
@@ -53,6 +54,7 @@ instance : ToString SolverName where
     | .fo => "zeport-fo"
     | .lams => "zeport-lams"
   | .eproverHo => "eprover-ho"
+  | .vampire => "vampire"
 
 instance : Lean.KVMap.Value SolverName where
   toDataValue n := toString n
@@ -61,8 +63,12 @@ instance : Lean.KVMap.Value SolverName where
   | "zeport-fo" => some (.zeport .fo)
   | "zeport-lams" => some (.zeport .lams)
   | "eprover-ho" => some .eproverHo
+  | "vampire" => some .vampire
   | _ => none
 
+end Auto.Solver.TPTP
+
+open Auto.Solver.TPTP in
 register_option auto.tptp.solver.name : SolverName := {
   defValue := SolverName.zipperposition
   descr := "Name of the designated TPTP solver"
@@ -73,16 +79,23 @@ register_option auto.tptp.zipperposition.path : String := {
   descr := "Path to zipperposition, defaults to \"zipperposition\""
 }
 
+register_option auto.tptp.zeport.path : String := {
+  defValue := "zeport"
+  descr := "Path to the zipperposition-E portfolio"
+}
+
 register_option auto.tptp.eproverHo.path : String := {
   defValue := "eprover-ho"
   descr := "Path to higher-order version of E theorem prover"
 }
 
-register_option auto.tptp.zeport.path : String := {
-  defValue := "zeport"
-  descr := "Path to the zipperposition-E portfolio"
+register_option auto.tptp.vampire.path : String := {
+  defValue := "vampire"
+  descr := "Path to vampire prover"
 }
 
+namespace Auto.Solver.TPTP
+
 abbrev SolverProc := IO.Process.Child ⟨.piped, .piped, .piped⟩
 
 private def createAux (path : String) (args : Array String) : MetaM SolverProc :=
@@ -147,14 +160,27 @@ def queryE (query : String) : MetaM String := do
   solver.kill
   return stdout
 
+def queryVampire (query : String) : MetaM String := do
+  let path := auto.tptp.vampire.path.get (← getOptions)
+  let tlim := auto.tptp.timeout.get (← getOptions)
+  let solver ← createAux path #["--mode", "casc", "--time_limit", s!"{tlim}"]
+  solver.stdin.putStr s!"{query}\n"
+  let (_, solver) ← solver.takeStdin
+  let stdout ← solver.stdout.readToEnd
+  let stderr ← solver.stderr.readToEnd
+  trace[auto.tptp.result] "Result: \nstderr:\n{stderr}\nstdout:\n{stdout}"
+  solver.kill
+  return stdout
+
 def querySolver (query : String) : MetaM (Array Parser.TPTP.Command) := do
   if !(auto.tptp.get (← getOptions)) then
     throwError "{decl_name%} :: Unexpected error"
   let stdout ← (do
     match auto.tptp.solver.name.get (← getOptions) with
     | .zipperposition => queryZipperposition query
-    | .zeport zept => queryZEPort zept query
-    | .eproverHo => queryE query)
+    | .zeport zept    => queryZEPort zept query
+    | .eproverHo      => queryE query
+    | .vampire        => queryVampire query)
   return ← Parser.TPTP.parse stdout
 
 end Solver.TPTP

Auto/Tactic.lean

@@ -254,10 +254,6 @@ def collectAllLemmas
   return (lctxLemmas ++ userLemmas ++ defeqLemmas, inhFacts)
 
 open Embedding.Lam in
-/--
-  If TPTP succeeds, return unsat core
-  If TPTP fails, return none
--/
 def queryTPTP (exportFacts : Array REntry) : LamReif.ReifM (Array Embedding.Lam.REntry) := do
     let lamVarTy := (← LamReif.getVarVal).map Prod.snd
     let lamEVarTy ← LamReif.getLamEVarTy

Auto/Translation/LamFOL2SMT.lean

@@ -319,7 +319,7 @@ private def lamBaseTerm2STerm_Arity1 (sni : SMTNamingInfo) (arg : STerm) : LamBa
 | t               => throwError "{decl_name%} :: The arity of {repr t} is not 1"
 where
   solverName : MetaM Solver.SMT.SolverName := do
-    return Solver.SMT.auto.smt.solver.name.get (← getOptions)
+    return auto.smt.solver.name.get (← getOptions)
   mkSMTMsbExpr (n : Nat) (arg : STerm) : STerm :=
     let andExpr := .qStrApp "bvand" #[arg, .qStrApp "bvshl" #[bitVec2STerm n 1, bitVec2STerm n (n - 1)]]
     .qStrApp "not" #[.qStrApp "=" #[andExpr, bitVec2STerm n 0]]