-
Notifications
You must be signed in to change notification settings - Fork 19
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
b92ae33
commit 91ee02b
Showing
1 changed file
with
121 additions
and
0 deletions.
There are no files selected for viewing
121 changes: 121 additions & 0 deletions
121
lisa-sets2/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,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.")) | ||
|
||
|
||
} | ||
|
||
} |