Modifying TPTPParser to pass on information regarding whether facts a…

…re from the goal

Duper/TPTPParser/PrattParser.lean

@@ -34,10 +34,10 @@ def tokens := [
   "~", ",", "(", ")", "*", "!", "?", "^", ":", "[", "]", "!>", ".", "*"
 ] -- TODO: Add ?? and !!
 
-def tokenHashMap : HashSet String := 
+def tokenHashMap : HashSet String :=
   HashSet.empty.insertMany tokens
 
-def tokenPrefixes : HashSet String := 
+def tokenPrefixes : HashSet String :=
   HashSet.empty.insertMany $ tokens.bind (fun t => Id.run do
     let mut res := []
     let mut pref := ""
@@ -60,13 +60,13 @@ def addToCurrToken (char : Char) : TokenizerM Unit := do
 
 def getCurrToken : TokenizerM String := do
   return (← get).currToken
-  
+
 def addCurrToken : TokenizerM Unit := do
-  modify fun (s : State) => 
-    {s with 
+  modify fun (s : State) =>
+    {s with
       res := s.res.push $
-        match s.status with 
-        | .default => .op s.currToken 
+        match s.status with
+        | .default => .op s.currToken
         | .ident => .ident s.currToken
         | .string => .ident s.currToken
         | .comment => panic! s!"Cannot add comment as token"
@@ -76,7 +76,7 @@ def addCurrToken : TokenizerM Unit := do
 def finalizeToken : TokenizerM Unit := do
   if (← getStatus) == .string || (← getCurrToken) != "" then
     match ← getStatus with
-    | .default => 
+    | .default =>
       if tokenHashMap.contains (← getCurrToken)
       then addCurrToken
       else throw $ IO.userError s!"Invalid token: {(← getCurrToken)}"
@@ -124,9 +124,9 @@ def tokenizeAux (str : String) : TokenizerM Unit := do
     | .comment =>
       if char == '\n' then
         setStatus .default
-          
-          
-  
+
+
+
   finalizeToken
 
   def tokenize (s : String) : IO (Array Token) := do
@@ -155,7 +155,7 @@ def peek : ParserM Token := do
   return ts[i]!
 
 def peek? : ParserM (Option Token) := do
-  if ← isEOF then return none else return ← peek 
+  if ← isEOF then return none else return ← peek
 
 def next : ParserM Token := do
   let c ← peek
@@ -204,8 +204,8 @@ partial def parseSep (sep : Token) (p : ParserM α) : ParserM (List α) := do
     return [t]
 
 mutual
-partial def parseTerm (minbp : Nat := 0) : ParserM Term := do        
-  let lhs ← parseLhs 
+partial def parseTerm (minbp : Nat := 0) : ParserM Term := do
+  let lhs ← parseLhs
   let res ← addOpAndRhs lhs minbp
   return res
 
@@ -226,7 +226,7 @@ partial def parseLhs : ParserM Term := do
       let p ← next
       parseToken (.op ")")
       return ⟨p, []⟩
-    else      
+    else
     let lhs ← parseTerm 0
     parseToken (.op ")")
     return lhs
@@ -307,7 +307,7 @@ def parseCommand : ParserM Command := do
 
 
 partial def parseFile : ParserM (List Command) := do
-  if ← isEOF 
+  if ← isEOF
   then return []
   else
     let c ← parseCommand
@@ -375,19 +375,19 @@ partial def toLeanExpr (t : Parser.Term) : MetaM Expr := do
   | ⟨.op "!=", []⟩  => pure $ mkConst `Ne
   | ⟨.op "=", []⟩   => pure $ mkConst `Eq
   | ⟨.op "~|", []⟩  => pure $ mkLambda `x .default (mkSort levelZero) $
-                         mkLambda `y .default (mkSort levelZero) $ 
+                         mkLambda `y .default (mkSort levelZero) $
                            mkAppN (mkConst ``Not) #[mkAppN (mkConst ``Or) #[.bvar 1, .bvar 0]]
   | ⟨.op "~&", []⟩  => pure $ mkLambda `x .default (mkSort levelZero) $
-                         mkLambda `y .default (mkSort levelZero) $ 
+                         mkLambda `y .default (mkSort levelZero) $
                            mkAppN (mkConst ``Not) #[mkAppN (mkConst ``And) #[.bvar 1, .bvar 0]]
   | ⟨.op "<~>", []⟩  => pure $ mkLambda `x .default (mkSort levelZero) $
-                         mkLambda `y .default (mkSort levelZero) $ 
+                         mkLambda `y .default (mkSort levelZero) $
                            mkAppN (mkConst ``Not) #[mkAppN (mkConst ``Iff) #[.bvar 1, .bvar 0]]
   | ⟨.op "=>", []⟩  => pure $ mkLambda `x .default (mkSort levelZero) $
-                         mkLambda `y .default (mkSort levelZero) $ 
+                         mkLambda `y .default (mkSort levelZero) $
                            Lean.mkForall `i BinderInfo.default (.bvar 1) (.bvar 1)
   | ⟨.op "<=", []⟩  => pure $ mkLambda `x .default (mkSort levelZero) $
-                         mkLambda `y .default (mkSort levelZero) $ 
+                         mkLambda `y .default (mkSort levelZero) $
                            Lean.mkForall `i BinderInfo.default (.bvar 0) (.bvar 2)
 
   | ⟨.op ">", [⟨.op "*", [a, b]⟩, c]⟩   => toLeanExpr ⟨.op ">", [a, ⟨.op ">", [b, c]⟩]⟩
@@ -446,25 +446,29 @@ partial def resolveIncludes (cmds : List Parser.Command) (dir : System.FilePath)
       let cmds' ← resolveIncludes cmds' dir
       for cmd' in cmds' do
         res := res.push cmd'
-    | _ => res := res.push cmd   
+    | _ => res := res.push cmd
   return res.toList
 
-abbrev Formulas := Array (Expr × Expr × Array Name)
+/-- First argument is the Prop itself, second argument is the proof of the Prop, third argument is an array of
+    paramNames, and the final argument is a bool which indicates if of kind "conjecture" (i.e. whether the facts
+    come from the goal) -/
+abbrev Formulas := Array (Expr × Expr × Array Name × Bool)
 
 def compileCmds (cmds : List Parser.Command) (acc : Formulas) (k : Formulas → MetaM α): MetaM α := do
   match cmds with
   | ⟨cmd, args⟩ :: cs =>
     match cmd with
-    | "thf" | "tff" | "cnf" | "fof" => 
+    | "thf" | "tff" | "cnf" | "fof" =>
       match args with
       | [_, ⟨.ident "type", _⟩, ⟨.ident id, [ty]⟩]  =>
         withLocalDeclD id (← ty.toLeanExpr) fun _ => do
           compileCmds cs acc k
       | [⟨.ident name, []⟩, ⟨.ident kind, _⟩, val] =>
         let val ← val.toLeanExpr
         let val := if kind == "conjecture" then ← mkAppM ``Not #[val] else val
+        let isFromGoal := kind == "conjecture"
         withLocalDeclD ("H_" ++ name) val fun x => do
-          let acc := acc.push (val, x, #[])
+          let acc := acc.push (val, x, #[], isFromGoal)
           compileCmds cs acc k
       | _ => throwError "Unknown declaration kind: {args.map repr}"
     | "include" => throwError "includes should have been unfolded first: {args.map repr}"
@@ -477,26 +481,26 @@ partial def collectConstantsOfCmd (topLevel : Bool) (acc : HashMap String Expr)
   | ⟨.ident n, as⟩ => do
     let acc ← as.foldlM (collectConstantsOfCmd false) acc
     if n.data[0]!.isLower && n.data[0]! != '$' && !acc.contains n
-    then 
-      let ty ← as.foldlM 
+    then
+      let ty ← as.foldlM
         (fun acc _ => mkArrow (mkConst `Iota) acc)
         (if topLevel then mkSort levelZero else mkConst `Iota)
       let acc := acc.insert n ty
       return acc
-    else 
+    else
       return acc
   | ⟨.op "!", body :: _⟩ | ⟨.op "?", body :: _⟩ =>
     collectConstantsOfCmd topLevel acc body
   | ⟨.op "~", as⟩
   | ⟨.op "|", as⟩
   | ⟨.op "&", as⟩
-  | ⟨.op "<=>", as⟩ 
-  | ⟨.op "=>", as⟩ | ⟨.op "<=", as⟩ 
-  | ⟨.op "~|", as⟩ 
-  | ⟨.op "~&", as⟩  
-  | ⟨.op "<~>", as⟩ => 
+  | ⟨.op "<=>", as⟩
+  | ⟨.op "=>", as⟩ | ⟨.op "<=", as⟩
+  | ⟨.op "~|", as⟩
+  | ⟨.op "~&", as⟩
+  | ⟨.op "<~>", as⟩ =>
     as.foldlM (collectConstantsOfCmd topLevel) acc
-  | ⟨.op "!=", as⟩ 
+  | ⟨.op "!=", as⟩
   | ⟨.op "=", as⟩ =>
     as.foldlM (collectConstantsOfCmd false) acc
   | _ => throwError "Failed to collect constants: {repr t}"
@@ -548,4 +552,4 @@ set_option trace.Meta.debug true
 #eval toLeanExpr "$true & $true"
 #eval toLeanExpr "(<=)"
 
-end TPTP
+end TPTP

Main.lean

@@ -8,8 +8,32 @@ open Lean.Elab.Tactic
 open Duper
 open ProverM
 
-def run (path : String) (github : Bool) : MetaM Unit := do
+/-- Entry point for calling a single instance of duper using the options determined by (← getOptions).
+
+    Formulas should consist of lemmas supplied by the user (to see how to obtain formulas from duper's input syntax, see `collectAssumptions`).
+    InstanceMaxHeartbeats should indicate how many heartbeats duper should run for before timing out (if instanceMaxHeartbeats is set to 0,
+    then duper will run until it is timed out by the Core `maxHeartbeats` option). If Duper succeeds in deriving a contradiction and constructing
+    a proof for it, then `runDuper` returns that proof as an expression. Otherwise, Duper will throw an error. -/
+def runDuperOnTPTP (fileName : String) (formulas : List (Expr × Expr × Array Name × Bool)) (instanceMaxHeartbeats : Nat) : MetaM Unit := do
+  let state ←
+    withNewMCtxDepth do
+      let formulas ← unfoldDefinitions formulas
+      /- `collectAssumptions` should not be wrapped by `withoutModifyingCoreEnv` because new definitional equations might be
+          generated during `collectAssumptions` -/
+      withoutModifyingCoreEnv <| do
+        -- Add the constant `skolemSorry` to the environment
+        let skSorryName ← addSkolemSorry
+        let (_, state) ←
+          ProverM.runWithExprs (ctx := {}) (s := {instanceMaxHeartbeats := instanceMaxHeartbeats, skolemSorryName := skSorryName})
+            ProverM.saturateNoPreprocessingClausification
+            formulas
+        pure state
+  match state.result with
+  | Result.contradiction => IO.println s!"SZS status Theorem for {fileName}"
+  | Result.saturated => IO.println s!"SZS status GaveUp for {fileName}"
+  | Result.unknown => IO.println s!"SZS status Timeout for {fileName}"
 
+def run (path : String) (github : Bool) : MetaM Unit := do
   let env ← getEnv
   let prop := mkSort levelZero
   let type := mkSort levelOne
@@ -48,31 +72,20 @@ def run (path : String) (github : Bool) : MetaM Unit := do
 
   TPTP.compileFile path fun formulas => do
     let formulas := Array.toList formulas
-    /- Adding `isFromGoal := false` to each formula as a placeholder.
-       TODO: Update TPTP.compileFile to distinguish between lemmas/axioms and the goal. -/
-    let formulas := formulas.map (fun (e, proof, paramNames) => (e, proof, paramNames, false))
-    let formulas ← unfoldDefinitions formulas
-    let skSorryName ← addSkolemSorry
-    let (_, state) ←
-      ProverM.runWithExprs (ctx := {}) (s := {skolemSorryName := skSorryName})
-        ProverM.saturateNoPreprocessingClausification
-        formulas
     let fileName := (path : System.FilePath).fileName.get!
-    match state.result with
-    | Result.contradiction => do
-      trace[TPTP_Testing] "Final Active Set: {state.activeSet.toArray}"
-      try
-        IO.println s!"SZS status Theorem for {fileName}"
-        if !github then
-          IO.println s!"SZS output start Proof for {fileName}"
-          printProof state
-          IO.println s!"SZS output end Proof for {fileName}"
-      catch
-      | _ => IO.println s!"SZS status Error for {fileName}"
-    | Result.saturated =>
-      IO.println s!"SZS status GaveUp for {fileName}"
-    | Result.unknown =>
-      IO.println s!"SZS status Timeout for {fileName}"
+    /- Going to try without Auto's preprocessing first. Although Duper performs better with Auto's preprocessing generally speaking, it's very plausible that Auto's preprocessing
+       won't be particularly helpful for TPTP problems (though I should test it both ways, because it's possible that the preprocessing steps Auto performs aside from monomorphization
+       are still helpful) -/
+
+    /- Using the options from Duper instance 9:
+       - preprocessing = no_preprocessing
+       - inhabitationReasoning = false
+       - selFunction = 4 (which corresponds to Zipperposition's default selection function)
+       - includeExpensiveRules = false
+
+       Additionally, we set maxHeartbeats to 0 so that Duper will run until the bash script terminates Duper -/
+    withOptions (fun o => (((o.set `inhabitationReasoning false).set `selFunction 4).set `includeExpensiveRules false).set `maxHeartbeats 0) $
+      runDuperOnTPTP fileName formulas 0
 
 def main : List String → IO UInt32 := fun args => do
   if args.length == 0 then