public final class SideProofUtil
extends java.lang.Object
Modifier | Constructor and Description |
---|---|
private |
SideProofUtil()
Forbid instances.
|
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 . |
public static ProofEnvironment cloneProofEnvironmentWithOwnOneStepSimplifier(Proof source, Choice... enableChoices)
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.source
- The Proof
to copy its ProofEnvironment
.enableChoices
- The Choice
s that should be changed w.r.t. those derived from Proof.getInitConfig()
ProofEnvironment
which is a copy of the environment of the given Proof
but with its own OneStepSimplifier
instance.public static ImmutableSet<Choice> activateChoice(ImmutableSet<Choice> choices, Choice choiceToActivate)
choiceToActivate
from
choices
and adds choiceToActivate
to the setchoices
- the currently active choiceschoiceToActivate
- the Choice
to activatechoiceToActivate
added (i.e.,
choices.contains(choiceToActivate)
will return true) and all
other choices of the same category removedpublic static ProofStarter createSideProof(ProofEnvironment sideProofEnvironment, Sequent sequentToProve, java.lang.String proofName) throws ProofInputException
ProofStarter
which contains a new site proof
of the given Proof
.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
.ProofStarter
with the site proof.ProofInputException
- Occurred Exception.