Skip to content

Commit cdd2c12

Browse files
augustepoirouxaugustepoiroux
committed
Separate the solver runner logic from the TPTP data extraction
1 parent 0799347 commit cdd2c12

File tree

3 files changed

+140
-118
lines changed

3 files changed

+140
-118
lines changed

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

Lines changed: 29 additions & 117 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,14 @@
1-
import scala.concurrent.duration._
2-
import scala.concurrent.ExecutionContext.Implicits.global
3-
import scala.concurrent._
4-
import java.util.concurrent.CancellationException
51
import java.io.File
2+
import java.io.FileWriter
3+
4+
import scala.concurrent.duration._
65

6+
import lisa.utils.ProofsConverter.*
7+
import lisa.utils.RunSolver.*
78
import lisa.utils.tptp.*
89
import lisa.utils.tptp.KernelParser.*
9-
import lisa.utils.tptp.KernelParser.getProblemInfos
1010
import lisa.utils.tptp.ProblemGatherer.*
11-
import lisa.utils.ProofsConverter.*
1211
import lisa.kernel.proof.SCProof
13-
import java.io.FileWriter
1412
import lisa.kernel.proof.SequentCalculus.Sequent
1513

1614
object TPTPSolver extends lisa.Main {
@@ -26,75 +24,62 @@ object TPTPSolver extends lisa.Main {
2624
val probfiles = d.listFiles.filter(_.isFile)
2725

2826
// We limit the execution time to solve each problem
29-
val timeoutTableau = .2.second
30-
val timeoutTautology = .2.second
27+
val timeoutTableau = .1.second
28+
val timeoutTautology = .1.second
3129

32-
var problems = List[Problem]()
33-
var tableauProofs = List[SolverResult]()
34-
var tautologyProofs = List[SolverResult]()
30+
var nbProblemsExtracted = 0
31+
var nbProblemsSolvedByTableau = 0
32+
var nbProblemsSolvedByTautology = 0
3533

3634
for ((probfile, i) <- probfiles.zipWithIndex) {
3735
// Progress bar
3836
if ((i + 1) % 10 == 0 || i + 1 == probfiles.size) {
3937
val pbarLength = 30
4038
var pbarContent = "=" * (((i + 1) * pbarLength) / probfiles.size)
4139
pbarContent += " " * (pbarLength - pbarContent.length)
42-
print("[" + pbarContent + "]")
43-
print(" -- " + (i + 1) + "/" + probfiles.size + " processed files")
44-
print(" -- " + problems.size + " extracted problems")
45-
print(" -- Tableau: " + tableauProofs.count(_.isInstanceOf[Solved]) + " solved")
46-
println(" -- Tautology: " + tautologyProofs.count(_.isInstanceOf[Solved]) + " solved")
40+
print(s"[$pbarContent]")
41+
print(s" -- ${i + 1}/${probfiles.size} processed files")
42+
print(s" -- $nbProblemsExtracted extracted problems")
43+
print(s" -- Tableau: $nbProblemsSolvedByTableau solved")
44+
println(s" -- Tautology: $nbProblemsSolvedByTautology solved")
4745
}
4846

49-
// Try to extract the problem
47+
// Try to extract and solve the problem
5048
try {
5149
val md = getProblemInfos(probfile)
5250
if (md.spc.exists(spc.contains)) {
5351
val p = problemToKernel(probfile, md)
54-
problems = problems :+ p
5552
val seq = problemToSequent(p)
53+
nbProblemsExtracted += 1
5654

5755
// Attempting proof by Tableau
58-
tableauProofs = tableauProofs :+ solveProblem(p, timeoutTableau, Tableau.solve)
56+
proveSequent(seq, timeoutTableau, Tableau.solve) match {
57+
case Solved(proof) =>
58+
nbProblemsSolvedByTableau += 1
59+
// writeProof(p, proof, "examples/proofs/tableau/")
60+
case _ => ()
61+
}
5962

6063
// Attempting proof by Tautology
6164
def tautologySolver(s: lisa.utils.K.Sequent): Option[SCProof] = Tautology.solveSequent(s) match
6265
case Left(proof) => Some(proof)
6366
case _ => None
64-
tautologyProofs = tautologyProofs :+ solveProblem(p, timeoutTautology, tautologySolver)
67+
proveSequent(seq, timeoutTautology, tautologySolver) match {
68+
case Solved(proof) =>
69+
nbProblemsSolvedByTautology += 1
70+
// writeProof(p, proof, "examples/proofs/tautology/")
71+
case _ => ()
72+
}
6573
}
6674
} catch {
6775
case _ => ()
6876
}
69-
7077
}
7178
} catch {
7279
case error: NullPointerException => println("You can download the tptp library at http://www.tptp.org/ and put it in main/resources")
7380
}
7481
}
7582

76-
sealed trait SolverResult
77-
case class Solved(proof: SCProof) extends SolverResult
78-
case object Unsolved extends SolverResult
79-
case object Timeout extends SolverResult
80-
case object Error extends SolverResult
81-
82-
def solveProblem(problem: Problem, timeout: FiniteDuration, solver: Sequent => Option[SCProof]): SolverResult = {
83-
val seq = problemToSequent(problem)
84-
val (futureSolver, cancelSolver) = Future.interruptibly { solver(seq) }
85-
try
86-
Await.result(futureSolver, timeout) match
87-
case Some(proof) => Solved(proof)
88-
case None => Unsolved
89-
catch
90-
case e: TimeoutException =>
91-
cancelSolver()
92-
Timeout
93-
case _ =>
94-
cancelSolver()
95-
Error
96-
}
97-
9883
def writeProof(problem: Problem, proof: SCProof, path: String): Unit = {
9984
// TODO
10085
val file = new File(path + problem.name + ".sc")
@@ -103,76 +88,3 @@ def writeProof(problem: Problem, proof: SCProof, path: String): Unit = {
10388
bw.write(proof.toString)
10489
bw.close()
10590
}
106-
107-
final class Interrupt extends (() => Boolean) {
108-
// We need a state-machine to track the progress.
109-
// It can have the following states:
110-
// a null reference means execution has not started.
111-
// a Thread reference means that the execution has started but is not done.
112-
// a this reference means that it is already cancelled or is already too late.
113-
private[this] final var state: AnyRef = null
114-
115-
/**
116-
* This is the signal to cancel the execution of the logic.
117-
* Returns whether the cancellation signal was successully issued or not.
118-
*/
119-
override final def apply(): Boolean = this.synchronized {
120-
state match {
121-
case null =>
122-
state = this
123-
true
124-
case _: this.type => false
125-
case t: Thread =>
126-
state = this
127-
// t.interrupt()
128-
t.stop()
129-
true
130-
}
131-
}
132-
133-
// Initializes right before execution of logic and
134-
// allows to not run the logic at all if already cancelled.
135-
private[this] final def enter(): Boolean =
136-
this.synchronized {
137-
state match {
138-
case _: this.type => false
139-
case null =>
140-
state = Thread.currentThread
141-
true
142-
}
143-
}
144-
145-
// Cleans up after the logic has executed
146-
// Prevents cancellation to occur "too late"
147-
private[this] final def exit(): Boolean =
148-
this.synchronized {
149-
state match {
150-
case _: this.type => false
151-
case t: Thread =>
152-
state = this
153-
true
154-
}
155-
}
156-
157-
/**
158-
* Executes the suplied block of logic and returns the result.
159-
* Throws CancellationException if the block was interrupted.
160-
*/
161-
def interruptibly[T](block: => T): T =
162-
if (enter()) {
163-
try block
164-
catch {
165-
case ie: InterruptedException => throw new CancellationException()
166-
} finally {
167-
if (!exit() && Thread.interrupted())
168-
() // If we were interrupted and flag was not cleared
169-
}
170-
} else throw new CancellationException()
171-
}
172-
173-
implicit class FutureInterrupt(val future: Future.type) extends AnyVal {
174-
def interruptibly[T](block: => T)(implicit ec: ExecutionContext): (Future[T], () => Boolean) = {
175-
val interrupt = new Interrupt()
176-
(Future(interrupt.interruptibly(block))(ec), interrupt)
177-
}
178-
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ import lisa.utils.KernelHelpers.lambda
99

1010
object ProofsConverter {
1111

12-
// TODO: fix printing of ∧ and ∨ with > 2 arguments, currently handled as recursive binary operators
12+
// TODO: fix printing of ∧ and ∨ with > 2 arguments, currently handled as recursive binary operators (see FOLHelpers.scala)
1313
// TODO: remove unnecessary variables "val s_..." in generated proofs -> need to keep track of which steps are used in other steps
1414
// TODO: generate more realistic variable names
1515
// TODO: handle automatic global variable declaration before theorems/proofs

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

Lines changed: 110 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,110 @@
1+
package lisa.utils
2+
3+
import scala.concurrent.duration._
4+
import scala.concurrent.ExecutionContext.Implicits.global
5+
import scala.concurrent._
6+
import java.util.concurrent.CancellationException
7+
8+
import lisa.kernel.proof.SCProof
9+
import lisa.kernel.proof.SequentCalculus.Sequent
10+
11+
object RunSolver {
12+
sealed trait SolverResult
13+
case class Solved(proof: SCProof) extends SolverResult
14+
case object Unsolved extends SolverResult
15+
case object Timeout extends SolverResult
16+
case class SolverException(e: Exception) extends SolverResult
17+
18+
def proveSequent(sequent: Sequent, timeout: Duration, solver: Sequent => Option[SCProof]): SolverResult = {
19+
val (futureSolver, cancelSolver) = Future.interruptibly { solver(sequent) }
20+
try
21+
Await.result(futureSolver, timeout) match
22+
case Some(proof) => Solved(proof)
23+
case None => Unsolved
24+
catch
25+
case _: TimeoutException =>
26+
cancelSolver()
27+
Timeout
28+
case e: Exception =>
29+
cancelSolver()
30+
SolverException(e)
31+
}
32+
33+
// Class to handle future cancellation
34+
// Source: https://viktorklang.com/blog/Futures-in-Scala-protips-6.html
35+
final class Interrupt extends (() => Boolean) {
36+
// We need a state-machine to track the progress.
37+
// It can have the following states:
38+
// a null reference means execution has not started.
39+
// a Thread reference means that the execution has started but is not done.
40+
// a this reference means that it is already cancelled or is already too late.
41+
private[this] final var state: AnyRef = null
42+
43+
/**
44+
* This is the signal to cancel the execution of the logic.
45+
* Returns whether the cancellation signal was successully issued or not.
46+
*/
47+
override final def apply(): Boolean = this.synchronized {
48+
state match {
49+
case null =>
50+
state = this
51+
true
52+
case _: this.type => false
53+
case t: Thread =>
54+
state = this
55+
// def kill = t.interrupt() // ask nicely for interruption, but this requires cooperation from the thread (involves checking isInterrupted() regularly)
56+
@annotation.nowarn
57+
def kill = t.stop() // brutally kill the thread without asking, more portable but less "safe". I believe it's safe here because we don't share any resources with the thread.
58+
kill
59+
true
60+
}
61+
}
62+
63+
// Initializes right before execution of logic and
64+
// allows to not run the logic at all if already cancelled.
65+
private[this] final def enter(): Boolean =
66+
this.synchronized {
67+
state match {
68+
case _: this.type => false
69+
case null =>
70+
state = Thread.currentThread
71+
true
72+
}
73+
}
74+
75+
// Cleans up after the logic has executed
76+
// Prevents cancellation to occur "too late"
77+
private[this] final def exit(): Boolean =
78+
this.synchronized {
79+
state match {
80+
case _: this.type => false
81+
case t: Thread =>
82+
state = this
83+
true
84+
}
85+
}
86+
87+
/**
88+
* Executes the suplied block of logic and returns the result.
89+
* Throws CancellationException if the block was interrupted.
90+
*/
91+
def interruptibly[T](block: => T): T =
92+
if (enter()) {
93+
try block
94+
catch {
95+
case ie: InterruptedException => throw new CancellationException()
96+
case td: ThreadDeath => throw new CancellationException()
97+
} finally {
98+
if (!exit() && Thread.interrupted())
99+
() // If we were interrupted and flag was not cleared
100+
}
101+
} else throw new CancellationException()
102+
}
103+
104+
implicit class FutureInterrupt(val future: Future.type) extends AnyVal {
105+
def interruptibly[T](block: => T)(implicit ec: ExecutionContext): (Future[T], () => Boolean) = {
106+
val interrupt = new Interrupt()
107+
(Future(interrupt.interruptibly(block))(ec), interrupt)
108+
}
109+
}
110+
}

0 commit comments

Comments
 (0)