diff --git a/build.sbt b/build.sbt index 5b1996c9..9a25d67a 100644 --- a/build.sbt +++ b/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") diff --git a/lisa-examples/src/main/scala/TPTPSolver.scala b/lisa-examples/src/main/scala/TPTPSolver.scala index 57615b68..a20ef722 100644 --- a/lisa-examples/src/main/scala/TPTPSolver.scala +++ b/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() + } diff --git a/lisa-utils/src/main/scala/lisa/utils/ProofsConverter.scala b/lisa-utils/src/main/scala/lisa/utils/ProofsConverter.scala index f53aee0a..44edc084 100644 --- a/lisa-utils/src/main/scala/lisa/utils/ProofsConverter.scala +++ b/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 diff --git a/lisa-utils/src/main/scala/lisa/utils/RunSolver.scala b/lisa-utils/src/main/scala/lisa/utils/RunSolver.scala index 29be3fc7..b0fb2ec8 100644 --- a/lisa-utils/src/main/scala/lisa/utils/RunSolver.scala +++ b/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 =>