-
Notifications
You must be signed in to change notification settings - Fork 18
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Support for Goéland and SC-TPTP (#211)
This adds support for Goéland as a proof tactic, and for parsing of proofs in SC-TPTP format.
- Loading branch information
1 parent
73bc04b
commit 0e2b6b7
Showing
16 changed files
with
801 additions
and
122 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
119 changes: 119 additions & 0 deletions
119
lisa-sets/src/main/scala/lisa/automation/atp/Goeland.scala
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,119 @@ | ||
| package lisa.automation.atp | ||
| import lisa.utils.tptp.* | ||
| import ProofParser.* | ||
| import KernelParser.* | ||
|
|
||
| import lisa.prooflib.ProofTacticLib.* | ||
| import lisa.fol.FOL as F | ||
| import lisa.prooflib.Library | ||
| import lisa.utils.K | ||
|
|
||
| import java.io.* | ||
| import sys.process._ | ||
| import scala.io.Source | ||
| import scala.util.{Try, Success, Failure} | ||
| import lisa.prooflib.OutputManager | ||
|
|
||
| /** | ||
| * 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.Term(K.VariableLabel(K.Identifier("X"+x.id.name, x.id.no)), Seq())).toMap | ||
|
|
||
| val backMap = freevars.map{ | ||
| case (x: K.VariableLabel, K.Term(xx: K.VariableLabel, _)) => xx -> K.LambdaTermTerm(Seq(), K.Term(x, Seq())) | ||
| 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.")) | ||
|
|
||
|
|
||
| } | ||
|
|
||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.