de.uka.ilkd.key.taclettranslation.lemma

Class AutomaticProver

java.lang.Object

de.uka.ilkd.key.taclettranslation.lemma.AutomaticProver

public class AutomaticProver
extends java.lang.Object

A very simple type of prover, but it is sufficient for the automatic lemmata handling: Normally there is a mechanism for choosing the next goal in a cyclic way if for the currently chosen goal no rules are left that could be applied. This is not done within this automatic prover, because it is not necessary: Either the proof can be closed or not.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	AutomaticProver.Worker The core of the automatic prover runs in an own thread.

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.concurrent.locks.ReentrantLock	awaitShutdown
private java.util.concurrent.locks.ReentrantLock	lock
private java.util.concurrent.locks.Condition	sleepCondition

Constructor Summary

Constructors

Constructor and Description
AutomaticProver()

Method Summary

Modifier and Type	Method and Description
void	start(Proof proof, int maxNumberOfRules, long timeout) Starts the prover with the following parameters.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

lock

private java.util.concurrent.locks.ReentrantLock lock

sleepCondition

private java.util.concurrent.locks.Condition sleepCondition

awaitShutdown

private java.util.concurrent.locks.ReentrantLock awaitShutdown

Constructor Detail

AutomaticProver

public AutomaticProver()

Method Detail

start

public void start(Proof proof,
                  int maxNumberOfRules,
                  long timeout)
           throws java.lang.InterruptedException

Starts the prover with the following parameters.

Parameters:

proof -

maxNumberOfRules -

timeout -

Throws:

java.lang.InterruptedException - If the prover is interrupted by the user, this exception is thrown