Export proofs extracted from TPTP to JSON

build.sbt

@@ -16,9 +16,6 @@ ThisBuild / semanticdbEnabled := true
 ThisBuild / semanticdbVersion := scalafixSemanticdb.revision
 ThisBuild / scalafixDependencies += "com.github.liancheng" %% "organize-imports" % "0.6.0"
 
-
-
-
 val commonSettings = Seq(
   crossScalaVersions := Seq("2.12.13", "2.13.4", "3.0.1", "3.2.0"),
   run / fork := true
@@ -41,6 +38,7 @@ val commonSettings3 = commonSettings ++ Seq(
   ),
   libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.10" % "test",
   libraryDependencies += "com.lihaoyi" %% "sourcecode" % "0.3.0",
+  libraryDependencies += "com.lihaoyi" %% "ujson" % "3.1.0",
   // libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "2.1.1",
   libraryDependencies += ("io.github.uuverifiers" %% "princess" % "2023-06-19").cross(CrossVersion.for3Use2_13),
   Test / parallelExecution := false
@@ -102,7 +100,6 @@ ThisBuild / assemblyMergeStrategy := {
     oldStrategy(x)
 }
 
-
 lazy val examples = Project(
   id = "lisa-examples",
   base = file("lisa-examples")

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

@@ -7,88 +7,126 @@ import lisa.utils.ProofsConverter.*
 import lisa.utils.RunSolver.*
 import lisa.utils.tptp.*
 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
+import lisa.utils.ProofsShrink.optimizeProofIteratively
 
 object TPTPSolver extends lisa.Main {
-  try {
-    val spc = Seq("PRP", "FOF") // type of problems we want to extract and solve
-    // val spc = Seq("PRP", "FOF", "CNF") // almost no CNF problems are solved by Tableau, TODO: investigate why
-
-    // val d = new File(TPTPProblemPath)
-    // val libraries = d.listFiles.filter(_.isDirectory)
-    // val probfiles = libraries.flatMap(_.listFiles).filter(_.isFile)
-
-    val d = new File(TPTPProblemPath + "SYN/")
-    val probfiles = d.listFiles.filter(_.isFile)
-
-    // We limit the execution time to solve each problem
-    val timeoutTableau = .1.second
-    val timeoutTautology = .1.second
-
-    var nbProblemsExtracted = 0
-    var nbProblemsSolvedByTableau = 0
-    var nbProblemsSolvedByTautology = 0
-
-    for ((probfile, i) <- probfiles.zipWithIndex) {
-      // Progress bar
-      if ((i + 1) % 10 == 0 || i + 1 == probfiles.size) {
-        val pbarLength = 30
-        var pbarContent = "=" * (((i + 1) * pbarLength) / probfiles.size)
-        pbarContent += " " * (pbarLength - pbarContent.length)
-        print(s"[$pbarContent]")
-        print(s" -- ${i + 1}/${probfiles.size} processed files")
-        print(s" -- $nbProblemsExtracted extracted problems")
-        print(s" -- Tableau: $nbProblemsSolvedByTableau solved")
-        println(s" -- Tautology: $nbProblemsSolvedByTautology solved")
-      }
+  sealed trait ProofType
+  case object BySolver extends ProofType
+  case object Kernel extends ProofType
+  case object KernelOptimized extends ProofType
+
+  class ProblemSolverResults(val problem: Problem, val solverName: String, val solverStatus: String, val proofCode: String, val proofType: ProofType)
+
+  val exportOnlySolvedProblems = true
+  val exportOptimizedProofs = true
+  val exportBySolverProofs = true
+
+  val jsonResultsPath: String = "/home/auguste/Documents/EPFL/PhD/Projects/lisa/lisa-examples/src/main/resources/TPTPResults.json"
+  val TPTPProblemPath: String = "/home/auguste/Documents/EPFL/PhD/Projects/TPTP-v8.2.0/Problems/"
+
+  val spc = Seq("PRP", "FOF") // type of problems we want to extract and solve
+  // val spc = Seq("CNF") // almost no CNF problems are solved by Tableau, TODO: investigate why
+
+  // val d = new File(TPTPProblemPath)
+  // val libraries = d.listFiles.filter(_.isDirectory)
+  // val probfiles = libraries.flatMap(_.listFiles).filter(_.isFile)
+
+  val d = new File(TPTPProblemPath + "SYN/")
+  val probfiles = d.listFiles.filter(_.isFile)
+
+  // We limit the execution time to solve each problem
+  val timeoutTableau = .1.second
+  val timeoutTautology = .1.second
 
-      // Try to extract and solve the problem
-      try {
-        val md = getProblemInfos(probfile)
+  var nbProblemsExtracted = 0
+  var nbProblemsSolved = Map("Tableau" -> 0, "Tautology" -> 0)
+  var nbInvalidProofs = Map("Tableau" -> 0, "Tautology" -> 0)
+  var results = Seq.empty[ProblemSolverResults]
+
+  for ((probfile, i) <- probfiles.zipWithIndex) {
+    // Progress bar
+    if ((i + 1) % 10 == 0 || i + 1 == probfiles.size) {
+      val pbarLength = 20
+      var pbarContent = "=" * (((i + 1) * pbarLength) / probfiles.size)
+      pbarContent += " " * (pbarLength - pbarContent.length)
+      print(s"[$pbarContent]")
+      print(s" -- ${i + 1}/${probfiles.size} processed files")
+      print(s" -- $nbProblemsExtracted extracted problems")
+      print(s" -- Tableau: ${nbProblemsSolved("Tableau")} solved + ${nbInvalidProofs("Tableau")} invalid")
+      println(s" -- Tautology: ${nbProblemsSolved("Tautology")} solved + ${nbInvalidProofs("Tautology")} invalid")
+    }
+
+    // Try to extract and solve the problem
+    try {
+      val md = getProblemInfos(probfile)
+      if (!(md.spc.contains("SAT"))) {
         if (md.spc.exists(spc.contains)) {
-          val p = problemToKernel(probfile, md)
-          val seq = problemToSequent(p)
+          val problem = problemToKernel(probfile, md)
+          val seq = problemToSequent(problem)
           nbProblemsExtracted += 1
 
+          def exportResults(problem: Problem, solverName: String, solverResult: SolverResult): Unit =
+            val solverStatus = solverResult.getClass.getSimpleName.stripSuffix("$")
+            solverResult match
+              case Solved(proof) =>
+                nbProblemsSolved += (solverName -> (nbProblemsSolved(solverName) + 1))
+                results :+= new ProblemSolverResults(problem, solverName, solverStatus, generateStandaloneTheoremFileContent(problem.name, proof), Kernel)
+                if (exportOptimizedProofs)
+                  results :+= new ProblemSolverResults(problem, solverName, solverStatus, generateStandaloneTheoremFileContent(problem.name, optimizeProofIteratively(proof)), KernelOptimized)
+                if (exportBySolverProofs)
+                  val statementString = any2code(seq)
+                  val proofCode = s"have(thesis) by $solverName"
+                  val symbolDeclarations = generateSymbolDeclarationCode(Set(K.sequentToFormula(seq)), "private")
+                  results :+= new ProblemSolverResults(problem, solverName, solverStatus, generateStandaloneTheoremFileContent(problem.name, statementString, proofCode, symbolDeclarations), BySolver)
+              case InvalidProof(proof) =>
+                nbInvalidProofs += (solverName -> (nbInvalidProofs(solverName) + 1))
+                if (!exportOnlySolvedProblems)
+                  results :+= new ProblemSolverResults(problem, solverName, solverStatus, generateStandaloneTheoremFileContent(problem.name, proof), Kernel)
+              case _ =>
+                if (!exportOnlySolvedProblems)
+                  results :+= new ProblemSolverResults(problem, solverName, solverStatus, "", Kernel)
+
           // Attempting proof by Tableau
-          proveSequent(seq, timeoutTableau, Tableau.solve) match {
-            case Solved(proof) =>
-              if (checkSCProof(proof).isValid)
-                nbProblemsSolvedByTableau += 1
-                // writeProof(p, proof, "examples/proofs/tableau/")
-              else throw new Exception("Tableau proof is not valid")
-            case _ => ()
-          }
+          val tableauResult = proveSequent(seq, timeoutTableau, Tableau.solve)
+          exportResults(problem, "Tableau", tableauResult)
 
           // Attempting proof by Tautology
           def tautologySolver(s: lisa.utils.K.Sequent): Option[SCProof] = Tautology.solveSequent(s) match
             case Left(proof) => Some(proof)
             case _ => None
-          proveSequent(seq, timeoutTautology, tautologySolver) match {
-            case Solved(proof) =>
-              if (checkSCProof(proof).isValid)
-                nbProblemsSolvedByTautology += 1
-                // writeProof(p, proof, "examples/proofs/tautology/")
-              else throw new Exception("Tautology proof is not valid")
-            case _ => ()
-          }
+          val tautologyResult = proveSequent(seq, timeoutTautology, tautologySolver)
+          exportResults(problem, "Tautology", tautologyResult)
         }
-      } catch {
-        case e => println(s"Error while processing $probfile: $e")
+        // } else println(s"Problem $probfile not extracted because of its type: ${md.spc.mkString(",")}")
       }
-    }
-  } catch {
-    case error: NullPointerException => println("You can download the tptp library at http://www.tptp.org/ and put it in main/resources")
+    } catch case e => println(s"Error while processing $probfile (index $i): $e")
   }
-}
 
-def writeProof(problem: Problem, proof: SCProof, path: String): Unit = {
-  val file = new File(path + problem.name + ".sc")
-  val bw = new FileWriter(file)
-  val fileContent = generateStandaloneTheoremFileContent(problem.name, proof)
-  bw.write(fileContent)
-  bw.close()
+  // Write results to a JSON file
+  val jsonResultsFile = new File(jsonResultsPath)
+  if (!jsonResultsFile.getParentFile.exists())
+    jsonResultsFile.getParentFile.mkdirs()
+  val jsonWriter = new java.io.PrintWriter(jsonResultsPath)
+  ujson.writeTo(
+    results.map(r =>
+      ujson.Obj(
+        "problemName" -> r.problem.name,
+        "problemDomain" -> r.problem.domain,
+        "problemStatus" -> r.problem.status,
+        "problemSPC" -> r.problem.spc.mkString(","),
+        "problemSequent" -> any2code(problemToSequent(r.problem)),
+        "problemFile" -> r.problem.file,
+        "solver" -> r.solverName,
+        "solverStatus" -> r.solverStatus,
+        "solverProofCode" -> r.proofCode,
+        "proofType" -> r.proofType.getClass.getSimpleName.stripSuffix("$")
+      )
+    ),
+    jsonWriter,
+    indent = 2
+  )
+  jsonWriter.close()
+
 }

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

@@ -166,7 +166,7 @@ object ProofsConverter {
    *
    * @return Scala code representing the variables in string format
    */
-  private def generateVariablesCode(formulas: Set[K.Formula], accessibility: String): String =
+  def generateSymbolDeclarationCode(formulas: Set[K.Formula], accessibility: String): String =
     val (variableSet, functionSet, formulaVariableSet, predicateSet, connectorSet) = extractSymbols(formulas)
     val access = if accessibility != "" then accessibility.strip() + " " else ""
     (variableSet.map(v => access + s"val ${v.id} = variable").toList.sorted ++
@@ -184,8 +184,8 @@ object ProofsConverter {
    *
    * @return Scala code representing the variables in string format
    */
-  def generateVariablesCode(proof: K.SCProof, accessibility: String = "private"): String =
-    generateVariablesCode(extractFormulasFromProof(proof), accessibility)
+  def generateSymbolDeclarationCode(proof: K.SCProof, accessibility: String = "private"): String =
+    generateSymbolDeclarationCode(extractFormulasFromProof(proof), accessibility)
 
   /**
    * Generates a valid Scala/Lisa code of a theorem and its proof
@@ -195,13 +195,13 @@ object ProofsConverter {
    *
    * @return Scala code representing the theorem in string format
    */
-  private def generateTheoremCode(name: String, proof: K.SCProof): String = {
+  def generateTheoremCode(name: String, statementString: String, proofCode: String): String = {
     // lowercase and underscore-separated version of the theorem name
     val filteredName = "[A-Za-z0-9]+".r.findAllIn(name).mkString("_").toLowerCase
     s"val $filteredName = Theorem(\n" +
-      indent(any2code(proof.conclusion)) +
+      indent(statementString) +
       s"\n) {\n" +
-      indent(scproof2code(proof)) +
+      indent(proofCode) +
       s"\n}"
   }
 
@@ -210,20 +210,32 @@ object ProofsConverter {
    * The theorem and its proof must be self-contained, i.e. no dependencies to other theorems, axioms, definitions, etc.
    *
    * @param name name of the theorem
-   * @param proof proof of the theorem
+   * @param proofCode code of the proof of the theorem
    *
    * @return Scala code representing the theorem in string format
    */
-  def generateStandaloneTheoremFileContent(name: String, proof: K.SCProof): String =
+  def generateStandaloneTheoremFileContent(name: String, statementString: String, proofCode: String, symbolDeclarations: String): String =
     val camelName = "[A-Za-z0-9]+".r.findAllIn(name).map(_.capitalize).mkString
     s"object $camelName extends lisa.Main {\n\n" +
       indent(
-        generateVariablesCode(proof) +
+        symbolDeclarations +
           "\n\n" +
-          generateTheoremCode(name, proof)
+          generateTheoremCode(name, statementString, proofCode)
       ) +
       "\n}"
 
+  /**
+   * Generates a valid Scala/Lisa code of a theorem and its proof in a standalone file, including the necessary variables declarations.
+   * The theorem and its proof must be self-contained, i.e. no dependencies to other theorems, axioms, definitions, etc.
+   *
+   * @param name name of the theorem
+   * @param proof proof of the theorem
+   *
+   * @return Scala code representing the theorem in string format
+   */
+  def generateStandaloneTheoremFileContent(name: String, proof: K.SCProof): String =
+    generateStandaloneTheoremFileContent(name, any2code(proof.conclusion), scproof2code(proof), generateSymbolDeclarationCode(proof))
+
   /**
    * Parse and check that a generated theorem file is valid, i.e. that it compiles and the theorem is proven
    * @param fileContent content of the generated file

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

@@ -7,10 +7,12 @@ import java.util.concurrent.CancellationException
 
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.Sequent
+import lisa.kernel.proof.SCProofChecker.checkSCProof
 
 object RunSolver {
   sealed trait SolverResult
   case class Solved(proof: SCProof) extends SolverResult
+  case class InvalidProof(proof: SCProof) extends SolverResult
   case object Unsolved extends SolverResult
   case object Timeout extends SolverResult
   case class SolverThrow(t: Throwable) extends SolverResult
@@ -19,7 +21,9 @@ object RunSolver {
     val (futureSolver, cancelSolver) = Future.interruptibly { solver(sequent) }
     try
       Await.result(futureSolver, timeout) match
-        case Some(proof) => Solved(proof)
+        case Some(proof) =>
+          if (checkSCProof(proof).isValid) Solved(proof)
+          else InvalidProof(proof)
         case None => Unsolved
     catch
       case _: TimeoutException =>