public class MergeRuleUtils
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
static class |
MergeRuleUtils.Option<T>
A simple Scala-like option type: Either Some(value) or None.
|
Constructor and Description |
---|
MergeRuleUtils() |
Modifier and Type | Method and Description |
---|---|
static Term |
allClosure(Term term,
Services services)
Universally closes all logical and location variables in the given term.
|
static void |
assertEquivalent(Term term1,
Term term2,
Services services,
int timeout)
Tries to prove the equivalence of term1 and term2 and throws a
RuntimeException if the proof fails. |
static void |
clearSemisequent(Goal goal,
boolean antec)
Deletes all formulae of the succedent / antecedent.
|
static void |
closeMergePartnerGoal(Node mergeNodeParent,
Goal mergePartner,
PosInOccurrence pio,
SymbolicExecutionState mergeState,
SymbolicExecutionState mergePartnerState,
Term pc,
java.util.Set<Name> newNames)
Closes the given partner goal, using the
CloseAfterMerge rule. |
static int |
countAtoms(Term term)
Counts the atoms in a formula.
|
static int |
countDisjunctions(Term term,
boolean negated)
Counts the disjunctions in a formula.
|
static Term |
createSimplifiedDisjunctivePathCondition(Term cond1,
Term cond2,
Services services,
int simplificationTimeout)
Creates a path condition that is equivalent to the disjunction of the two
supplied formulae, but possibly simpler.
|
static boolean |
equalsModBranchUniqueRenaming(SourceElement se1,
SourceElement se2,
Node node,
Services services)
An equals method that, before the comparison, replaces all program
locations in the supplied arguments by their branch-unique versions.
|
static Term |
exClosure(Term term,
Services services)
Existentially closes all logical and location variables in the given
term.
|
static LocationVariable |
getBranchUniqueLocVar(LocationVariable var,
Node startLeaf)
Find a location variable for the given one that is unique for the branch
corresponding to the given goal, but not necessarily globally unique.
|
static java.util.ArrayList<Term> |
getConjunctiveElementsFor(Term term)
Dissects a conjunction into its conjunctive elements.
|
static MergeRuleUtils.Option<Pair<Term,Term>> |
getDistinguishingFormula(java.util.ArrayList<Term> conjElemsPathCond1,
java.util.ArrayList<Term> conjElemsPathCond2,
Services services) |
static MergeRuleUtils.Option<Pair<Term,Term>> |
getDistinguishingFormula(Term pathCondition1,
Term pathCondition2,
Services services)
Computes a formula that implies pathCondition1 and, if pathCondition1 and
pathCondition2 are contradicting, does not imply pathCondition2.
|
static java.util.LinkedList<Term> |
getElementaryUpdates(Term u)
Returns all elementary updates of a parallel update.
|
static LocationVariable |
getFreshLocVariableForPrefix(java.lang.String prefix,
Sort sort,
Services services)
Computes and registers a fresh location variable with the given prefix in
its name of the given sort.
|
static LogicVariable |
getFreshVariableForPrefix(java.lang.String prefix,
Sort sort,
Services services)
Computes and registers a fresh variable with the given prefix in its name
of the given sort.
|
static Node |
getIntroducingNodeforLocVar(LocationVariable var,
Node node)
Finds the node, from the given leaf on, where the variable was
introduced.
|
static JavaBlock |
getJavaBlockRecursive(Term term)
Returns the first Java block in the given term that can be found by
recursive search, or the empty block if there is no non-empty Java block
in the term.
|
static ImmutableSet<LocationVariable> |
getLocationVariables(Term term,
Services services)
Returns all program variables in the given term.
|
static java.util.HashSet<LocationVariable> |
getLocationVariablesHashSet(Sequent sequent,
Services services)
Returns all program variables in the given sequent.
|
static java.util.HashSet<LocationVariable> |
getLocationVariablesHashSet(Term term,
Services services)
Returns all program variables in the given term.
|
static Function |
getNewSkolemConstantForPrefix(java.lang.String prefix,
Sort sort,
Services services)
Computes and registers a new Skolem constant with the given prefix in its
name of the given sort.
|
static java.util.HashSet<Function> |
getSkolemConstants(Term term)
Returns all Skolem constants in the given term.
|
static ImmutableSet<LocationVariable> |
getUpdateLeftSideLocations(Term u) |
static Term |
getUpdateRightSideFor(Term update,
LocationVariable leftSide)
Returns the right side for a given location variable in an update (in
normal form).
|
static MergeRuleUtils.Option<Term> |
getUpdateRightSideForSafe(Term update,
LocationVariable leftSide)
Returns the right side for a given location variable in an update (in
normal form).
|
static Pair<SymbolicExecutionState,SymbolicExecutionState> |
handleNameClashes(SymbolicExecutionState mergeState,
SymbolicExecutionState mergePartnerState,
Services services)
Due to the introduction of local namespaces, we run into trouble when
applying state merging in the presence of locally introduced symbols.
|
static int |
intPow(int a,
int b)
Power function for integers.
|
static boolean |
isProvable(Sequent toProve,
Services services,
int timeout)
Tries to prove the given formula without splitting and returns whether
the prove could be closed.
|
static boolean |
isProvable(Term toProve,
Services services,
int timeout)
Tries to prove the given formula without splitting and returns whether
the prove could be closed.
|
static boolean |
isProvableWithSplitting(Sequent toProve,
Services services,
int timeout)
Tries to prove the given formula with splitting and returns whether the
prove could be closed.
|
static boolean |
isProvableWithSplitting(Term toProve,
Services services,
int timeout)
Tries to prove the given formula with splitting and returns whether the
prove could be closed.
|
static boolean |
isUpdateNormalForm(Term u)
Checks if an update is of the form { x := v || ...
|
static Pair<Sort,Name> |
parsePlaceholder(java.lang.String input,
boolean registerInNamespaces,
Services services)
Parses a declaration of the type "<SORT> <NAME>", where
<SORT> must be a sort known to the proof and <NAME> must be a
fresh name.
|
static Pair<Sort,Name> |
parsePlaceholder(java.lang.String input,
Services services)
Parses a declaration of the type "<SORT> <NAME>", where
<SORT> must be a sort known to the proof and <NAME> must be a
fresh name.
|
static AbstractionPredicate |
parsePredicate(java.lang.String input,
java.util.ArrayList<Pair<Sort,Name>> registeredPlaceholders,
NamespaceSet localNamespaces,
Services services)
Parses an abstraction predicate.
|
static boolean |
pathConditionsAreDistinguishable(Term pathCondition1,
Term pathCondition2,
Services services)
Checks if two given path conditions are distinguishable.
|
static ImmutableList<SymbolicExecutionState> |
sequentsToSEPairs(java.lang.Iterable<MergePartner> sequentInfos)
Convenience method for converting a whole list of goal-pio combinations
to symbolic execution states; relies on
sequentToSETriple(Node, PosInOccurrence, Services) . |
static SymbolicExecutionState |
sequentToSEPair(Node node,
PosInOccurrence pio,
Services services)
Converts a sequent (given by goal & pos in occurrence) to an SE state
(U,C).
|
static SymbolicExecutionStateWithProgCnt |
sequentToSETriple(Node node,
PosInOccurrence pio,
Services services)
Converts a sequent (given by goal & pos in occurrence) to an SE state
(U,C,p).
|
static <T> java.util.ArrayList<T> |
singletonArrayList(T elem)
Creates an
ArrayList containing exactly the given element. |
static java.lang.String |
stripIndex(java.lang.String name)
For Strings "xxx_i", this method returns "xxx".
|
static Term |
substConstantsByFreshVars(Term term,
java.util.HashMap<Function,LogicVariable> replMap,
Services services)
Substitutes all constants in the given term by fresh variables.
|
static Term |
substConstantsByFreshVars(Term term,
java.util.HashSet<Function> restrictTo,
java.util.HashMap<Function,LogicVariable> replMap,
Services services)
Substitutes all constants in the given term that are contained in the set
restrictTo by fresh variables.
|
static Term |
translateToFormula(Services services,
java.lang.String toTranslate)
Translates a String into a formula or to null if not applicable.
|
static Term |
trySimplify(Proof parentProof,
Term term,
boolean countDisjunctions,
int timeout)
Tries to simplifies the given
Term in a side proof with splits. |
static <T> MergeRuleUtils.Option<T> |
wrapOption(T obj)
Wraps the given object s.th.
|
public static <T> MergeRuleUtils.Option<T> wrapOption(T obj)
obj
- The object to wrap.public static java.lang.String stripIndex(java.lang.String name)
name
- Name to remove the index from.public static int intPow(int a, int b)
a
- The base.b
- The exponent.public static <T> java.util.ArrayList<T> singletonArrayList(T elem)
ArrayList
containing exactly the given element.elem
- Element that is contained in the returned list.ArrayList
containing exactly the given element.public static Term translateToFormula(Services services, java.lang.String toTranslate)
services
- The services object.toTranslate
- The formula to be translated.public static ImmutableSet<LocationVariable> getUpdateLeftSideLocations(Term u)
u
- The update (in normal form) to extract program locations from.public static java.util.LinkedList<Term> getElementaryUpdates(Term u)
u
- Parallel update to get elementary updates from.public static ImmutableSet<LocationVariable> getLocationVariables(Term term, Services services)
term
- The term to extract program variables from.public static java.util.HashSet<LocationVariable> getLocationVariablesHashSet(Sequent sequent, Services services)
sequent
- The sequent to extract program variables from.public static java.util.HashSet<LocationVariable> getLocationVariablesHashSet(Term term, Services services)
term
- The term to extract program variables from.public static java.util.HashSet<Function> getSkolemConstants(Term term)
term
- The term to extract Skolem constants from.public static MergeRuleUtils.Option<Term> getUpdateRightSideForSafe(Term update, LocationVariable leftSide)
update
- Update term to search.leftSide
- Left side to find the right side for.public static Term getUpdateRightSideFor(Term update, LocationVariable leftSide)
update
- Update term to search.leftSide
- Left side to find the right side for.public static int countAtoms(Term term)
term
- Formula to count atoms for.java.lang.IllegalArgumentException
- if the supplied term is not a formulapublic static int countDisjunctions(Term term, boolean negated)
term
- Formula to count disjunctions for.negated
- Set to true iff the current subformula is in the scope of a
negation; in this case, "and" junctors have the role of "or"
junctors considering the disjunctive complexity.java.lang.IllegalArgumentException
- if the supplied term is not a formulapublic static Function getNewSkolemConstantForPrefix(java.lang.String prefix, Sort sort, Services services)
prefix
- Prefix for the name of the constant.sort
- Sort of the constant.services
- The services object.public static LogicVariable getFreshVariableForPrefix(java.lang.String prefix, Sort sort, Services services)
prefix
- Prefix for the name of the variable.sort
- Sort of the variable.services
- The services object.public static LocationVariable getFreshLocVariableForPrefix(java.lang.String prefix, Sort sort, Services services)
prefix
- Prefix for the name of the variable.sort
- Sort of the variable.services
- The services object.public static Term substConstantsByFreshVars(Term term, java.util.HashMap<Function,LogicVariable> replMap, Services services)
term
- Term in which to substitute constants by variables.replMap
- Map from constants to variables in order to remember
substitutions of one constant.public static Term substConstantsByFreshVars(Term term, java.util.HashSet<Function> restrictTo, java.util.HashMap<Function,LogicVariable> replMap, Services services)
term
- Term in which to substitute constants by variables.restrictTo
- Set of constants to replace. If null, all constants are
replaced.replMap
- Map from constants to variables in order to remember
substitutions of one constant.public static Term exClosure(Term term, Services services)
term
- Term to existentially close.services
- The services object.public static Term allClosure(Term term, Services services)
term
- Term to universally close.services
- The services object.public static boolean isUpdateNormalForm(Term u)
u
- Update to check.public static java.util.ArrayList<Term> getConjunctiveElementsFor(Term term)
term
- Conjunctive formula to dissect (may be a conjunction of one
element, i.e. no "real" conjunction). In this case, the
resulting list will contain exactly the supplied formula.public static LocationVariable getBranchUniqueLocVar(LocationVariable var, Node startLeaf)
var
- Variable to get a branch-unique correspondent for.startLeaf
- The leaf of the branch.public static Node getIntroducingNodeforLocVar(LocationVariable var, Node node)
var
- Variable to find introducing node for.node
- Leaf to start from.public static JavaBlock getJavaBlockRecursive(Term term)
term
- The term to extract Java blocks for.public static boolean isProvable(Term toProve, Services services, int timeout)
toProve
- Formula to prove.services
- The services object.timeout
- Time in milliseconds after which the side proof is aborted.public static boolean isProvableWithSplitting(Term toProve, Services services, int timeout)
toProve
- Formula to prove.services
- The services object.timeout
- Time in milliseconds after which the side proof is aborted.public static boolean isProvable(Sequent toProve, Services services, int timeout)
toProve
- Sequent to prove.services
- The services object.timeout
- Time in milliseconds after which the side proof is aborted.public static boolean isProvableWithSplitting(Sequent toProve, Services services, int timeout)
toProve
- Sequent to prove.services
- The services object.timeout
- Time in milliseconds after which the side proof is aborted.public static void assertEquivalent(Term term1, Term term2, Services services, int timeout)
RuntimeException
if the proof fails.term1
- First term to check.term2
- Second term to check.services
- The services object.timeout
- Time in milliseconds after which the side proof is aborted.java.lang.RuntimeException
- iff proving the equivalence of term1 and term2 fails.public static Term trySimplify(Proof parentProof, Term term, boolean countDisjunctions, int timeout)
Term
in a side proof with splits.
If this attempt is successful, i.e. the number of atoms in the simplified
formula is lower (and, if requested, also the number of disjunctions),
the simplified formula is returned; otherwise, the original formula is
returned.
Please note that using this method can consume a great amount of time!
parentProof
- The parent Proof
.term
- The Term
to simplify.countDisjunctions
- If set to true, the method also takes the number of
disjunctions (in addition to the number of atoms) into account
when judging about the complexity of the "simplified" formula.timeout
- Time in milliseconds after which the side proof is aborted.Term
or the original term, if
simplification was not successful.#simplify(Proof, Term)
,
SymbolicExecutionUtil#simplify(Proof, Term)
public static void clearSemisequent(Goal goal, boolean antec)
goal
- Goal to delete formulae from.antec
- If true, antecedent formulae are deleted, else succedent
formulae.public static boolean equalsModBranchUniqueRenaming(SourceElement se1, SourceElement se2, Node node, Services services)
se1
- First element to check equality (mod renaming) for.se2
- Second element to check equality (mod renaming) for.goal
- The goal of the current branch (for getting branch-unique
names).services
- The Services object.public static Term createSimplifiedDisjunctivePathCondition(Term cond1, Term cond2, Services services, int simplificationTimeout)
The underlying idea is based upon the observation that many path
conditions that should be merged are conjunctions of mostly the same
elements and, in addition, formulae phi and !phi that vanish after
creating the disjunction of the path conditions. The corresponding valid
formula is (phi & psi) | (phi & !psi) <-> phi
For formulae that cannot be simplified by this law, the method performs
two additional steps:
(1) it applies, if possible, distributivity to simplify the result
(2) it checks whether the disjunction is already equivalent to the common
parts of the formulae only. This often happens when merging all branches
that occur in symbolic execution.
cond1
- First path condition to merge.cond2
- Second path condition to merge.services
- The services object.timeout
- Time in milliseconds after which the side proof is aborted.public static MergeRuleUtils.Option<Pair<Term,Term>> getDistinguishingFormula(Term pathCondition1, Term pathCondition2, Services services)
pathCondition1
- The first formula to compute a distinguishing formula for.pathCondition2
- The second formula to compute a distinguishing formula for.services
- The services object.public static MergeRuleUtils.Option<Pair<Term,Term>> getDistinguishingFormula(java.util.ArrayList<Term> conjElemsPathCond1, java.util.ArrayList<Term> conjElemsPathCond2, Services services)
public static boolean pathConditionsAreDistinguishable(Term pathCondition1, Term pathCondition2, Services services)
pathCondition1
- First path condition to check.pathCondition2
- Second path condition to check.services
- The services object.public static void closeMergePartnerGoal(Node mergeNodeParent, Goal mergePartner, PosInOccurrence pio, SymbolicExecutionState mergeState, SymbolicExecutionState mergePartnerState, Term pc, java.util.Set<Name> newNames)
CloseAfterMerge
rule.mergeNodeParent
- Parent of remaining join node.mergePartner
- Partner goal to close.newNames
- The set of new names (of Skolem constants) introduced in the
merge.public static SymbolicExecutionState sequentToSEPair(Node node, PosInOccurrence pio, Services services)
goal
- Current goal.pio
- Position of update-program counter formula in goal.services
- The services object.#sequentToSETriple(Goal, PosInOccurrence, Services)
public static SymbolicExecutionStateWithProgCnt sequentToSETriple(Node node, PosInOccurrence pio, Services services)
The problem which makes this renaming necessary is the fact that when
executing a program like int x; x = ...
, the variable x is
renamed to x_1, x_2 and so on in different branches, which makes a
"normal" merging impossible. Branch unique names are tracked in the
LocationVariables when they are renamed in InnerVariableNamer. Soundness
is not effected by the switch to branch-unique names. However, merged
nodes are then of course potentially different from their predecessors
concerning the involved local variable symbols.
goal
- Current goal.pio
- Position of update-program counter formula in goal.services
- The services object.public static ImmutableList<SymbolicExecutionState> sequentsToSEPairs(java.lang.Iterable<MergePartner> sequentInfos)
sequentToSETriple(Node, PosInOccurrence, Services)
.sequentInfos
- Goals and PosInOccurrences specifying merge partners and the
positions of the program counter-post condition formulae in
the goals.public static Pair<SymbolicExecutionState,SymbolicExecutionState> handleNameClashes(SymbolicExecutionState mergeState, SymbolicExecutionState mergePartnerState, Services services)
SymbolicExecutionState
state.mergeState
- The SymbolicExecutionState
in which the partners
should be merged.mergePartnerState
- The SymbolicExecutionState
of the second merge
partner.services
- The Services
object.SymbolicExecutionState
of the second merge
partner.public static Pair<Sort,Name> parsePlaceholder(java.lang.String input, Services services)
input
- Input to parse.Services
- The services object.NameAlreadyBoundException
- If the given placeholder is already known to the system.SortNotKnownException
- If the given sort is not known to the system.public static Pair<Sort,Name> parsePlaceholder(java.lang.String input, boolean registerInNamespaces, Services services)
input
- Input to parse.registerInNamespaces
- Flag to indicate whether the parsed placeholder should be
registered in the namespaces.Services
- The services object.NameAlreadyBoundException
- If the given placeholder is already known to the system.SortNotKnownException
- If the given sort is not known to the system.public static AbstractionPredicate parsePredicate(java.lang.String input, java.util.ArrayList<Pair<Sort,Name>> registeredPlaceholders, NamespaceSet localNamespaces, Services services) throws ParserException
input
- The predicate to parse (contains exactly one placeholder).localNamespaces
- The local NamespaceSet
.AbstractionPredicate
.ParserException
- If there is a syntax error.Copyright © 2003-2019 The KeY-Project.