de.uka.ilkd.key.util

Class SideProofUtil

java.lang.Object

de.uka.ilkd.key.util.SideProofUtil

public final class SideProofUtil
extends java.lang.Object

Constructor Summary

Constructors

Modifier	Constructor and Description
private	SideProofUtil() Forbid instances.

Method Summary

Modifier and Type	Method and Description
static ImmutableSet<Choice>	activateChoice(ImmutableSet<Choice> choices, Choice choiceToActivate) removes all choices with the same category as choiceToActivate from choices and adds choiceToActivate to the set
static ProofEnvironment	cloneProofEnvironmentWithOwnOneStepSimplifier(Proof source, Choice... enableChoices) Creates a copy of the ProofEnvironment of the given Proof which has his own OneStepSimplifier instance.
static ProofStarter	createSideProof(ProofEnvironment sideProofEnvironment, Sequent sequentToProve, java.lang.String proofName) Creates a new ProofStarter which contains a new site proof of the given Proof.

Methods inherited from class java.lang.Object

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

Constructor Detail

SideProofUtil

private SideProofUtil()

Forbid instances.

Method Detail

cloneProofEnvironmentWithOwnOneStepSimplifier

public static ProofEnvironment cloneProofEnvironmentWithOwnOneStepSimplifier(Proof source,
                                                                             Choice... enableChoices)

Creates a copy of the ProofEnvironment of the given Proof which has his own OneStepSimplifier instance. Such copies are required for instance during parallel usage of site proofs because OneStepSimplifier has an internal state.

Parameters:

source - The Proof to copy its ProofEnvironment.

enableChoices - The Choices that should be changed w.r.t. those derived from Proof.getInitConfig()

Returns:

The created ProofEnvironment which is a copy of the environment of the given Proof but with its own OneStepSimplifier instance.

activateChoice

public static ImmutableSet<Choice> activateChoice(ImmutableSet<Choice> choices,
                                                  Choice choiceToActivate)

removes all choices with the same category as choiceToActivate from choices and adds choiceToActivate to the set

Parameters:

choices - the currently active choices

choiceToActivate - the Choice to activate

Returns:

the set of choices with choiceToActivate added (i.e., choices.contains(choiceToActivate) will return true) and all other choices of the same category removed

createSideProof

public static ProofStarter createSideProof(ProofEnvironment sideProofEnvironment,
                                           Sequent sequentToProve,
                                           java.lang.String proofName)
                                    throws ProofInputException

Creates a new ProofStarter which contains a new site proof of the given Proof.

Parameters:

sideProofEnvironment - The given ProofEnvironment of the side proof.

sequentToProve - The Sequent to proof in a new site proof.

proofName - An optional name for the newly created Proof.

Returns:

The created ProofStarter with the site proof.

Throws:

ProofInputException - Occurred Exception.