Add proof checks in TPTPSolver

Author: augustepoiroux

lisa-examples/src/main/scala/TPTPSolver.scala

@@ -10,6 +10,7 @@ import lisa.utils.tptp.KernelParser.*
 import lisa.utils.tptp.ProblemGatherer.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.Sequent
+import lisa.kernel.proof.SCProofChecker.checkSCProof
 
 object TPTPSolver extends lisa.Main {
   try {
@@ -55,8 +56,10 @@ object TPTPSolver extends lisa.Main {
           // Attempting proof by Tableau
           proveSequent(seq, timeoutTableau, Tableau.solve) match {
             case Solved(proof) =>
-              nbProblemsSolvedByTableau += 1
-            // writeProof(p, proof, "examples/proofs/tableau/")
+              if (checkSCProof(proof).isValid)
+                nbProblemsSolvedByTableau += 1
+                // writeProof(p, proof, "examples/proofs/tableau/")
+              else throw new Exception("Tableau proof is not valid")
             case _ => ()
           }
 
@@ -66,13 +69,15 @@ object TPTPSolver extends lisa.Main {
             case _ => None
           proveSequent(seq, timeoutTautology, tautologySolver) match {
             case Solved(proof) =>
-              nbProblemsSolvedByTautology += 1
-            // writeProof(p, proof, "examples/proofs/tautology/")
+              if (checkSCProof(proof).isValid)
+                nbProblemsSolvedByTautology += 1
+                // writeProof(p, proof, "examples/proofs/tautology/")
+              else throw new Exception("Tautology proof is not valid")
             case _ => ()
           }
         }
       } catch {
-        case _ => ()
+        case e => println(s"Error while processing $probfile: $e")
       }
     }
   } catch {

lisa-utils/src/main/scala/lisa/utils/RunSolver.scala

@@ -13,7 +13,7 @@ object RunSolver {
   case class Solved(proof: SCProof) extends SolverResult
   case object Unsolved extends SolverResult
   case object Timeout extends SolverResult
-  case class SolverException(e: Exception) extends SolverResult
+  case class SolverThrow(t: Throwable) extends SolverResult
 
   def proveSequent(sequent: Sequent, timeout: Duration, solver: Sequent => Option[SCProof]): SolverResult = {
     val (futureSolver, cancelSolver) = Future.interruptibly { solver(sequent) }
@@ -25,9 +25,9 @@ object RunSolver {
       case _: TimeoutException =>
         cancelSolver()
         Timeout
-      case e: Exception =>
+      case t: Throwable =>
         cancelSolver()
-        SolverException(e)
+        SolverThrow(t)
   }
 
   // Class to handle future cancellation
@@ -94,6 +94,7 @@ object RunSolver {
         catch {
           case ie: InterruptedException => throw new CancellationException()
           case td: ThreadDeath => throw new CancellationException()
+          case t: Throwable => throw t
         } finally {
           if (!exit() && Thread.interrupted())
             () // If we were interrupted and flag was not cleared