public class MergeRuleUtils
extends java.lang.Object
Modifier and Type | Class and Description |
---|---|
private static class |
MergeRuleUtils.CollectLocationVariablesVisitor
Visitor for collecting program locations in a Java block.
|
private static class |
MergeRuleUtils.CollectLocationVariablesVisitorHashSet
Visitor for collecting program locations in a Java block.
|
private static class |
MergeRuleUtils.CommonAndSpecificSubformulasResult
TODO
|
private static class |
MergeRuleUtils.LocVarReplBranchUniqueMap
Map for renaming variables to their branch-unique names.
|
(package private) static class |
MergeRuleUtils.NameAlreadyBoundException
This exception is thrown by methods to indicate that a name for which it
is requested to register it is already known to the system.
|
static class |
MergeRuleUtils.Option<T>
A simple Scala-like option type: Either Some(value) or None.
|
(package private) static class |
MergeRuleUtils.SortNotKnownException
This exception is thrown by methods to indicate that a given KeY sort is
not known in the current situation.
|
(package private) static class |
MergeRuleUtils.TermWrapper
Simple term wrapper for comparing terms modulo renaming.
|
(package private) static class |
MergeRuleUtils.TermWrapperFactory
Creates
MergeRuleUtils.TermWrapper objects, thereby ensuring that equal term
wrappers also have equal hash codes. |
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.
|
private static Pair<Term,ImmutableSet<QuantifiableVariable>> |
anonymizeProgramVariables(Term term,
Services services)
Anonymizes all program variables occurring 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. |
private static MergeRuleUtils.CommonAndSpecificSubformulasResult |
commonAndSpecificSubformulas(java.util.ArrayList<Term> cond1,
java.util.ArrayList<Term> cond2,
Services services)
Returns the set of specific and common conjunctive subformulas of two
formulas.
|
private static MergeRuleUtils.CommonAndSpecificSubformulasResult |
commonAndSpecificSubformulas(Term cond1,
Term cond2,
Services services)
Returns the set of specific and common conjunctive subformulas of two
formulas.
|
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.
|
private static ImmutableSet<LocationVariable> |
getProgramLocations(Term programCounterTerm,
Services services)
Returns all used program locations in the given term.
|
private static java.util.HashSet<LocationVariable> |
getProgramLocationsHashSet(Term programCounterTerm,
Services services)
Returns all used program locations in the given term.
|
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.
|
private static boolean |
isProvable(Sequent toProve,
Services services,
boolean doSplit,
int timeout)
Tries to prove the given formula and returns whether the prove could be
closed.
|
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.
|
private static boolean |
isProvable(Term toProve,
Services services,
boolean doSplit,
int timeout)
Tries to prove the given formula 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.
|
private static boolean |
isUniqueInGlobals(java.lang.String name,
java.lang.Iterable<IProgramVariable> globals)
Tells whether a name is unique in the passed list of global variables.
|
static boolean |
isUpdateNormalForm(Term u)
Checks if an update is of the form { x := v || ... || z := q}.
|
private static Term |
joinConjuctiveElements(java.util.Collection<Term> elems,
Services services)
Joins a list of formulae to a conjunction.
|
private static Term |
joinListToAndTerm(ImmutableList<SequentFormula> formulae,
Services services)
Joins a list of sequent formulae to an and-connected term.
|
private static LocationVariable |
lookupVarInNS(java.lang.String name,
Services services)
Looks up a program variable by its name in the PV namespace.
|
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) . |
private static Term |
sequentToFormula(Sequent sequent,
Services services)
Converts a Sequent "Gamma ==> Delta" into a single formula equivalent to
"/\ Gamma -> \/ Delta"; however, the formulae in Gamma are shifted to the
succedent by the negation-left rule, so the result of this method is a
disjunction, not an implication.
|
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).
|
private static StrategyProperties |
setupStrategy()
creates the strategy configuration to be used for the side proof
|
private static Term |
simplify(Proof parentProof,
Term term,
int timeout)
Simplifies the given
Term in a side proof with splits. |
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. |
private static ApplyStrategyInfo |
tryToProve(Sequent toProve,
Services services,
boolean doSplit,
java.lang.String sideProofName,
int timeout)
Tries to prove the given formula and returns the result.
|
private static ApplyStrategyInfo |
tryToProve(Term toProve,
Services services,
boolean doSplit,
java.lang.String sideProofName,
int timeout)
Tries to prove the given formula and returns the result.
|
static <T> MergeRuleUtils.Option<T> |
wrapOption(T obj)
Wraps the given object s.th. if it is null, a None value is returned, and
a Some value wrapping the object is returned otherwise.
|
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.MergeRuleUtils.NameAlreadyBoundException
- If the given placeholder is already known to the system.MergeRuleUtils.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.MergeRuleUtils.NameAlreadyBoundException
- If the given placeholder is already known to the system.MergeRuleUtils.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.private static Pair<Term,ImmutableSet<QuantifiableVariable>> anonymizeProgramVariables(Term term, Services services)
{ ... || x := vx || ...} term
where vx is a fresh variable.
Returns all free variables of the new termin the second component of the
pair.term
- Term to anonymize.services
- The services object.{ ... || x := vx || ...} term
for
every PV x occurring in the term, where vx is a fresh variable.private static Term joinListToAndTerm(ImmutableList<SequentFormula> formulae, Services services)
formulae
- Formulae to join.services
- The services object.private static ImmutableSet<LocationVariable> getProgramLocations(Term programCounterTerm, Services services)
programCounterTerm
- The term (program counter) to extract locations from.services
- The Services object.private static java.util.HashSet<LocationVariable> getProgramLocationsHashSet(Term programCounterTerm, Services services)
programCounterTerm
- The term (program counter) to extract locations from.services
- The Services object.private static Term joinConjuctiveElements(java.util.Collection<Term> elems, Services services)
elems
- Formulae to join.services
- The services object.private static ApplyStrategyInfo tryToProve(Term toProve, Services services, boolean doSplit, java.lang.String sideProofName, int timeout)
toProve
- Formula to prove.services
- The services object.doSplit
- if true, splitting is allowed (normal mode).sideProofName
- name for the generated side proof.timeout
- A timeout for the proof in milliseconds.private static ApplyStrategyInfo tryToProve(Sequent toProve, Services services, boolean doSplit, java.lang.String sideProofName, int timeout)
toProve
- Sequent to prove.services
- The services object.doSplit
- if true, splitting is allowed (normal mode).sideProofName
- name for the generated side proof.timeout
- A timeout for the proof in milliseconds. Set to -1 for no
timeout.private static StrategyProperties setupStrategy()
private static boolean isProvable(Term toProve, Services services, boolean doSplit, int timeout)
toProve
- Formula to prove.services
- The services object.doSplit
- if true, splitting is allowed (normal mode).timeout
- Time in milliseconds after which the side proof is aborted.private static boolean isProvable(Sequent toProve, Services services, boolean doSplit, int timeout)
toProve
- Sequent to prove.services
- The services object.doSplit
- if true, splitting is allowed (normal mode).timeout
- Time in milliseconds after which the side proof is aborted.private static Term simplify(Proof parentProof, Term term, int timeout) throws ProofInputException
Term
in a side proof with splits. This code
has been copied from SymbolicExecutionUtil
and only been slightly
modified (to allow for splitting the proof).parentProof
- The parent Proof
.term
- The Term
to simplify.timeout
- Time in milliseconds after which the side proof is aborted.Term
.ProofInputException
- Occurred Exception.SymbolicExecutionUtil#simplify(Proof, Term)
private static Term sequentToFormula(Sequent sequent, Services services)
sequent
- The sequent to convert to a formula.services
- The services object.private static boolean isUniqueInGlobals(java.lang.String name, java.lang.Iterable<IProgramVariable> globals)
name
- The name to check uniqueness for.globals
- The global variables for the givan branch.VariableNamer#isUniqueInGlobals(String, Globals)
private static LocationVariable lookupVarInNS(java.lang.String name, Services services)
name
- Name to find a PV for.private static MergeRuleUtils.CommonAndSpecificSubformulasResult commonAndSpecificSubformulas(Term cond1, Term cond2, Services services)
cond1
- The conjunctive elements of the first formula.cond2
- The conjunctive elements of the second formula.services
- The Services
object.commonAndSpecificSubformulas(ArrayList, ArrayList, Services)
private static MergeRuleUtils.CommonAndSpecificSubformulasResult commonAndSpecificSubformulas(java.util.ArrayList<Term> cond1, java.util.ArrayList<Term> cond2, Services services)
cond1
- The first formula.cond2
- The second formula.services
- The Services
object.