public final class SymbolicExecutionSideProofUtil
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
protected static class |
SymbolicExecutionSideProofUtil.ContainsIrrelevantThingsVisitor
Utility class used by
QuerySideProofRule#containsIrrelevantThings(Services, SequentFormula, Set) . |
protected static class |
SymbolicExecutionSideProofUtil.ContainsModalityOrQueryVisitor
Utility method used by
QuerySideProofRule#containsModalityOrQuery(Term) . |
Modifier | Constructor and Description |
---|---|
private |
SymbolicExecutionSideProofUtil()
Forbid instances.
|
Modifier and Type | Method and Description |
---|---|
static void |
addNewNamesToNamespace(Services services,
Term term)
|
static ProofEnvironment |
cloneProofEnvironmentWithOwnOneStepSimplifier(InitConfig sourceInitConfig,
boolean useSimplifyTermProfile)
Creates a copy of the
ProofEnvironment of the given Proof
which has his own OneStepSimplifier instance. |
static ProofEnvironment |
cloneProofEnvironmentWithOwnOneStepSimplifier(Proof source,
boolean useSimplifyTermProfile)
Creates a copy of the
ProofEnvironment of the given Proof
which has his own OneStepSimplifier instance. |
static Sequent |
computeGeneralSequentToProve(Sequent goalSequent,
SequentFormula currentSF)
Computes a general
Sequent to prove in a side proof which
contains all SequentFormula of the original Sequent
except the given current SequentFormula and those which
contains modalities and queries. |
static java.util.List<Pair<Term,Node>> |
computeResults(Services services,
Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
TermLabel label,
java.lang.String description,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption,
boolean addNamesToServices)
Starts the side proof and extracts the result
Term . |
static java.util.List<Triple<Term,java.util.Set<Term>,Node>> |
computeResultsAndConditions(Services services,
Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
Operator operator,
java.lang.String description,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption,
boolean addNamesToServices)
Starts the side proof and extracts the result
Term and conditions. |
private static Term |
constructResultIfContained(Services services,
SequentFormula sf,
Operator operator) |
private static Term |
constructResultIfContained(Services services,
Term term,
Operator operator) |
static boolean |
containsIrrelevantThings(Services services,
SequentFormula sf,
java.util.Set<Operator> relevantThings)
Checks if the given
SequentFormula contains irrelevant things
(things which are not contained in the relevantThingsToProve and are no Java types) |
static boolean |
containsModalityOrQuery(SequentFormula sf)
Checks if the given
SequentFormula contains a modality or query. |
static boolean |
containsModalityOrQuery(Term term)
Checks if the given
Term contains a modality or query. |
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 . |
static void |
disposeOrStore(java.lang.String description,
ApplyStrategyInfo info)
|
static Term |
extractOperatorTerm(ApplyStrategyInfo info,
Operator operator)
Extracts the operator term for the formula with the given
Operator
from the site proof result (ApplyStrategyInfo ). |
static Term |
extractOperatorTerm(Goal goal,
Operator operator)
|
static Term |
extractOperatorTerm(Node node,
Operator operator)
|
static Term |
extractOperatorValue(Goal goal,
Operator operator)
|
static Term |
extractOperatorValue(Node node,
Operator operator)
|
static java.util.Set<Operator> |
extractRelevantThings(Services services,
Sequent sequentToProve)
|
static boolean |
isIrrelevantCondition(Services services,
Sequent initialSequent,
java.util.Set<Operator> relevantThingsInSequentToProve,
SequentFormula sf)
Checks if the given
SequentFormula is a relevant condition. |
private static boolean |
isOperatorASequentFormula(Sequent sequent,
Operator operator) |
protected static boolean |
isRelevantThing(Services services,
Term term)
Checks if the given
Term describes a relevant thing. |
static ApplyStrategyInfo |
startSideProof(Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve)
Starts a site proof for the given
Sequent . |
static ApplyStrategyInfo |
startSideProof(Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption)
Starts a site proof for the given
Sequent . |
static ApplyStrategyInfo |
startSideProof(Proof proof,
ProofStarter starter,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption)
Starts a site proof.
|
private SymbolicExecutionSideProofUtil()
public static Sequent computeGeneralSequentToProve(Sequent goalSequent, SequentFormula currentSF)
Sequent
to prove in a side proof which
contains all SequentFormula
of the original Sequent
except the given current SequentFormula
and those which
contains modalities and queries.goalSequent
- The original Sequent
of the current Goal
.currentSF
- The SequentFormula
to ignore.Sequent
.public static java.util.List<Pair<Term,Node>> computeResults(Services services, Proof proof, ProofEnvironment sideProofEnvironment, Sequent sequentToProve, TermLabel label, java.lang.String description, java.lang.String methodTreatment, java.lang.String loopTreatment, java.lang.String queryTreatment, java.lang.String splittingOption, boolean addNamesToServices) throws ProofInputException
Starts the side proof and extracts the result Term
.
New used names are automatically added to the Namespace
of the Services
.
services
- The Services
to use.proof
- The Proof
from on which the side proof si performed.sideProofEnvironment
- The given ProofEnvironment
of the side proof.sequentToProve
- The Sequent
to prove in a side proof.label
- The TermLabel
which is used to compute the result.description
- The side proof description.splittingOption
- The splitting options to use.addNamesToServices
- true
defines that used names in result and conditions are added to the namespace of the given Services
, false
means that names are not added.Term
and the conditions.ProofInputException
- Occurred Exception.public static java.util.List<Triple<Term,java.util.Set<Term>,Node>> computeResultsAndConditions(Services services, Proof proof, ProofEnvironment sideProofEnvironment, Sequent sequentToProve, Operator operator, java.lang.String description, java.lang.String methodTreatment, java.lang.String loopTreatment, java.lang.String queryTreatment, java.lang.String splittingOption, boolean addNamesToServices) throws ProofInputException
Starts the side proof and extracts the result Term
and conditions.
New used names are automatically added to the Namespace
of the Services
.
services
- The Services
to use.proof
- The Proof
from on which the side proof si performed.sideProofEnvironment
- The given ProofEnvironment
of the side proof.sequentToProve
- The Sequent
to prove in a side proof.operator
- The Operator
which is used to compute the result.description
- The side proof description.splittingOption
- The splitting options to use.addNamesToServices
- true
defines that used names in result and conditions are added to the namespace of the given Services
, false
means that names are not added.Term
and the conditions.ProofInputException
- Occurred Exception.private static Term constructResultIfContained(Services services, SequentFormula sf, Operator operator)
private static Term constructResultIfContained(Services services, Term term, Operator operator)
private static boolean isOperatorASequentFormula(Sequent sequent, Operator operator)
public static boolean containsModalityOrQuery(SequentFormula sf)
SequentFormula
contains a modality or query.sf
- The SequentFormula
to check.true
contains at least one modality or query, false
contains no modalities and no queries.public static boolean containsModalityOrQuery(Term term)
Term
contains a modality or query.term
- The Term
to check.true
contains at least one modality or query, false
contains no modalities and no queries.public static java.util.Set<Operator> extractRelevantThings(Services services, Sequent sequentToProve)
protected static boolean isRelevantThing(Services services, Term term)
Term
describes a relevant thing.
Relevant things are:
public static boolean isIrrelevantCondition(Services services, Sequent initialSequent, java.util.Set<Operator> relevantThingsInSequentToProve, SequentFormula sf)
SequentFormula
is a relevant condition.services
- The Services
to use.initialSequent
- The initial Sequent
of the side proof.relevantThingsInSequentToProve
- The relevant things found in the initial Sequent
.sf
- The SequentFormula
to check.true
SequentFormula
is relevant condition, false
SequentFormula
is not a relevant condition.public static boolean containsIrrelevantThings(Services services, SequentFormula sf, java.util.Set<Operator> relevantThings)
SequentFormula
contains irrelevant things
(things which are not contained in the relevantThingsToProve and are no Java types)services
- The Services
to use.sf
- The SequentFormula
to check.relevantThings
- The relevant things.true
The SequentFormula
contains irrelevant things, false
the SequentFormula
contains no irrelevant things.public static ApplyStrategyInfo startSideProof(Proof proof, ProofEnvironment sideProofEnvironment, Sequent sequentToProve) throws ProofInputException
Sequent
.proof
- The parent Proof
of the site proof to do.sideProofEnvironment
- The given ProofEnvironment
of the side proof.sequentToProve
- The Sequent
to prove.ApplyStrategyInfo
instance.ProofInputException
- Occurred Exceptionpublic static ApplyStrategyInfo startSideProof(Proof proof, ProofEnvironment sideProofEnvironment, Sequent sequentToProve, java.lang.String methodTreatment, java.lang.String loopTreatment, java.lang.String queryTreatment, java.lang.String splittingOption) throws ProofInputException
Sequent
.proof
- The parent Proof
of the site proof to do.sideProofEnvironment
- The given ProofEnvironment
of the side proof.sequentToProve
- The Sequent
to prove.ApplyStrategyInfo
instance.ProofInputException
- Occurred Exceptionpublic 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.public static ApplyStrategyInfo startSideProof(Proof proof, ProofStarter starter, java.lang.String methodTreatment, java.lang.String loopTreatment, java.lang.String queryTreatment, java.lang.String splittingOption)
proof
- The original Proof
.starter
- The ProofStarter
with the site proof.splittingOption
- The splitting option to use.public static Term extractOperatorTerm(ApplyStrategyInfo info, Operator operator) throws ProofInputException
Operator
from the site proof result (ApplyStrategyInfo
).info
- The site proof result.operator
- The Operator
for the formula which should be extracted.Operator
.ProofInputException
- Occurred Exception.public static ProofEnvironment cloneProofEnvironmentWithOwnOneStepSimplifier(Proof source, boolean useSimplifyTermProfile)
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
.ProofEnvironment
which is a copy of the environment of the given Proof
but with its own OneStepSimplifier
instance.public static ProofEnvironment cloneProofEnvironmentWithOwnOneStepSimplifier(InitConfig sourceInitConfig, boolean useSimplifyTermProfile)
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.sourceInitConfig
- The InitConfig
to copy its ProofEnvironment
.ProofEnvironment
which is a copy of the environment of the given Proof
but with its own OneStepSimplifier
instance.public static void disposeOrStore(java.lang.String description, ApplyStrategyInfo info)
Stores or disposes the Proof
of the ApplyStrategyInfo
in SideProofStore.DEFAULT_INSTANCE
.
This method should be called whenever a side proof is no longer needed and should be disposed or stored for debugging purposes.
description
- The description.info
- The ApplyStrategyInfo
to store or dispose its Proof
.