From 91ee02bfe8362d025b094629dbfae7c18b428489 Mon Sep 17 00:00:00 2001 From: Simon Guilloud Date: Fri, 1 Nov 2024 15:01:56 +0100 Subject: [PATCH] add goeland files in sets2 --- .../scala/lisa/automation/atp/Goeland.scala | 121 ++++++++++++++++++ 1 file changed, 121 insertions(+) create mode 100644 lisa-sets2/src/main/scala/lisa/automation/atp/Goeland.scala diff --git a/lisa-sets2/src/main/scala/lisa/automation/atp/Goeland.scala b/lisa-sets2/src/main/scala/lisa/automation/atp/Goeland.scala new file mode 100644 index 00000000..2493399e --- /dev/null +++ b/lisa-sets2/src/main/scala/lisa/automation/atp/Goeland.scala @@ -0,0 +1,121 @@ +package lisa.automation.atp +import lisa.fol.FOL as F +import lisa.prooflib.Library +import lisa.prooflib.OutputManager +import lisa.prooflib.ProofTacticLib.* +import lisa.utils.K +import lisa.utils.tptp.* + +import java.io.* +import scala.io.Source +import scala.util.Failure +import scala.util.Success +import scala.util.Try + +import ProofParser.* +import KernelParser.* +import sys.process._ + +/** + * Goéland is an automated theorem prover. This tactic calls the Goéland prover to solve the current sequent. + * Goéland is only available on Linux yet, but proofs generated by Goéland should be kept in the library for future use. + * To ensure that proofs are published and can be replayed in any system, proofs from an ATPcan only be generated in draft mode. + * When in non-draft mode, the proof file should be given as an argument to the tactic (the exact file is provided by Lisa upon run without draft mode). + */ +object Goeland extends ProofTactic with ProofSequentTactic { + private var i : Int = 0 + + val goelandExec = "../bin/goeland_linux_release" + + class OsNotSupportedException(msg: String) extends Exception(msg) + + val foldername = "goeland/" + + /** + * Fetch a proof of a sequent that was previously proven by Goéland. + * The file must be in SC-TPTP format. + */ + def apply(using lib: Library, proof: lib.Proof)(file:String)(bot: F.Sequent): proof.ProofTacticJudgement = { + val outputname = proof.owningTheorem.fullName+"_sol" + try { + val scproof = reconstructProof(new File(foldername+outputname+".p"))(using ProofParser.mapAtom, ProofParser.mapTerm, ProofParser.mapVariable) + proof.ValidProofTactic(bot, scproof.steps, Seq()) + } catch { + case e: FileNotFoundException => + throw FileNotFoundException("The file "+foldername+outputname+".p was not found. To produce a proof, use `by Goeland`. ") + case e => throw e + } + } + + + /** + * Solve a sequent using the Goéland automated theorem prover. + * At the moment, this option is only available on Linux system. + * The proof is generated and saved in a file in the `Goeland` folder. + */ + def apply(using lib: Library, proof: lib.Proof)(bot: F.Sequent): proof.ProofTacticJudgement = { + + + solve(Seq(), bot, proof.owningTheorem.fullName, lib.isDraft) match { + case Success(value) => proof.ValidProofTactic(bot, value.steps, Seq()) + case Failure(e) => e match + case e: FileNotFoundException => throw new Exception("For compatibility reasons, external provers can't be called in non-draft mode" + + " unless all proofs have already been generated and be available in static files. You can enable draft mode by adding `draft()` at the top of your working file.") + case e: OsNotSupportedException => throw e + case e => + throw e + } + } + + inline def solve(axioms: Seq[F.Sequent], sequent: F.Sequent, source: String, generateProofs : Boolean): Try[K.SCProof] = + solveK(axioms.map(_.underlying), sequent.underlying, source, generateProofs) + + + /** + * Solve a sequent using the Goéland automated theorem prover, and return the kernel proof. + * At the moment, this option is only available on Linux systems. + */ + def solveK(using line: sourcecode.Line, file: sourcecode.File)(axioms: Seq[K.Sequent], sequent: K.Sequent, source:String, generateProofs : Boolean): Try[K.SCProof] = { + val filename = source + val outputname = source+"_sol" + val directory = File(foldername) + if (directory != null) && !directory.exists() then directory.mkdirs() + + val freevars = (sequent.left.flatMap(_.freeVariables) ++ sequent.right.flatMap(_.freeVariables) ).toSet.map(x => x -> K.Variable(K.Identifier("X"+x.id.name, x.id.no), x.sort) ).toMap + + val backMap = freevars.map{ + case (x: K.Variable, xx: K.Variable) => xx -> x + case _ => throw new Exception("This should not happen") + } + val r = problemToFile(foldername, filename, "question"+i, axioms, sequent, source) + i += 1 + + if generateProofs then + val OS = System.getProperty("os.name") + if OS.contains("nix") || OS.contains("nux") || OS.contains("aix") then + val ret = s"chmod u+x \"$goelandExec\"".! + val cmd = (s"$goelandExec -otptp -wlogs -no_id -quoted_pred -proof_file=$foldername$outputname $foldername$filename.p") + val res = try { + cmd.!! + } catch { + case e: Exception => + throw e + } + val proof = reconstructProof(new File(foldername+outputname+".p"))(using ProofParser.mapAtom, ProofParser.mapTerm, ProofParser.mapVariable) + Success(proof) + else if OS.contains("win") then + Failure(OsNotSupportedException("The Goeland automated theorem prover is not yet supported on Windows.")) + else + Failure(OsNotSupportedException("The Goeland automated theorem prover is only supported on Linux for now.")) + else + if File(foldername+outputname+".p").exists() then + val proof = reconstructProof(new File(foldername+outputname+".p"))(using ProofParser.mapAtom, ProofParser.mapTerm, ProofParser.mapVariable) + println(OutputManager.WARNING(s"WARNING: in ${file.value}:$line, For compatibility reasons, replace `by Goeland` with `by Goeland(\"$foldername$outputname\")`.")) + Success(proof) + + else Failure(Exception("For compatibility reasons, external provers can't be called in non-draft mode. You can enable draft mode by adding `draft()` at the top of your working file.")) + + + } + +} \ No newline at end of file