Skip to content

Latest commit

 

History

History
198 lines (145 loc) · 5.02 KB

scheduler.md

File metadata and controls

198 lines (145 loc) · 5.02 KB

leo3ltb.scheduler

leo3ltb.scheduler.scheduler

Implementation of a fully customizeable prove scheduler.

ProveScheduler

ProveScheduler(self, *, threads, schedulerProcessClass, batch, overallTimeout, problemTimeout=None, withCASCStdout=True)

Args:

  • threads: number of concurrent threads(and external processes) to use
  • batch: batch environment containing:
    • batch.definiton.problems: problems to prove by the Scheduler in this batch
    • file = batch.createTempfile(name) to create a temp file
    • ..
  • schedulerProcessClass: use you class implementing SchedulerProcess. If you are using Leo-III you may use 'Leo3SchedulerProcess'

status

ProveScheduler.status(self)

Get the complex status of the Scheduler as human readable string.

scheduledProblemVariants

ProveScheduler.scheduledProblemVariants(self)

Get all problem variants which are enqueued.

activeProblemVariants

ProveScheduler.activeProblemVariants(self)

Get all problem variants which are enqueued.

runningProblemVariants

ProveScheduler.runningProblemVariants(self)

Get all problem variants where proves are currently running.

prove

ProveScheduler.prove(self, problemVariant, *, timeout)

Enqueus a problemVariant to prove.

terminate

ProveScheduler.terminate(self, problemVariant)

Terminate the prove of the 'problemVariant'.

terminateProblemVariants

ProveScheduler.terminateProblemVariants(self, problem)

Terminate the prove of all problemVariant of 'problem'.

getProblemTimeUsed

ProveScheduler.getProblemTimeUsed(self, problem)

Returns:

  • The time the problem has used for running overall.

getProblemTimeLeft

ProveScheduler.getProblemTimeLeft(self, problem)

Returns:

  • The time the problem has left for running.

onSuccess

ProveScheduler.onSuccess(self, problemVariant, overallTimeleft, problemTimeleft)

Called if a proverall is terminated with a success-szs-status.

Args:

  • problemVariant: terminated problem variant
  • overallTimeleft time left to prove the batch
  • problemTimeleft time left to prove the problem

Needs to be overwritten.

onNoSuccess

ProveScheduler.onNoSuccess(self, problemVariant, overallTimeleft, problemTimeleft)

Called if a prove call is terminated with a nosuccess-szs-status.

Args:

  • problemVariant: terminated problem variant
  • overallTimeleft time left to prove the batch
  • problemTimeleft time left to prove the problem

Needs to be overwritten.

onTimeout

ProveScheduler.onTimeout(self, problemVariant, overallTimeleft, problemTimeleft)

Called if a prove call is either:

  1. terminated with the szs-status 'Timeout', then:
    • problemVariant.schedulerStatus == 'ProcessTimeout'
  2. the process run into a timeout is was killed by python, then:
    • problemVariant.schedulerStatus == 'Completed'

Args:

  • problemVariant: terminated problem variant
  • overallTimeleft time left to prove the batch
  • problemTimeleft time left to prove the problem

Needs to be overwritten.

onUserForced

ProveScheduler.onUserForced(self, problemVariant, overallTimeleft, problemTimeleft)

Called if a prove call is terminated by the scheduler, using one of

  • terminate(problemVariant)
  • terminateProblemVariants(problem)

Args:

  • problemVariant: terminated problem variant
  • overallTimeleft time left to prove the batch
  • problemTimeleft time left to prove the problem

Needs to be overwritten.

onStart

ProveScheduler.onStart(self, problemVariant, overallTimeleft, problemTimeleft)

Called if a prove call is started by the scheduler.

Args:

  • problemVariant: terminated problem variant
  • overallTimeleft time left to prove the batch
  • problemTimeleft time left to prove the problem

Needs to be overwritten.

Leo3SchedulerProcess

Leo3SchedulerProcess(self, problemVariant, problemFile, *, timeout, withCASCStdout)

If you are using the Leo-III theorem prover using the default shell command 'leo3' use this implementation. Otherwise use a custom implementation of 'ProveSchedulerProcess'

ProveSchedulerProcess

ProveSchedulerProcess(self, problemVariant, problemFile, *, timeout, withCASCStdout)

Process runned by the Scheduler to prove a problemVariant.

generateProverCall

ProveSchedulerProcess.generateProverCall(self, problemFile, timeout)

Function returning the shell command to call the underlaying prover given a set of call parameter.

Needs to be overwritten s.t. an appropriate commandline call is provided.

Args:

  • problemFile: the problem that should be used
  • timeout: the timeout in seconds when the process should be finished, if exceeded, the process is killed

Returns:

  • the cmd command to run the prover on the given problem

Example:

  1. Using the Leo-III theorem prover Leo-III Usage. If the shell command 'leo3' calls Leo-III. You should implement the method with return
['leo3', problemFile, '-t', timeout]