| java.lang.Object de.uka.ilkd.key.strategy.quantifierHeuristics.QuanEliminationAnalyser
QuanEliminationAnalyser | public class QuanEliminationAnalyser (Code) | | |
eliminableDefinition | public int eliminableDefinition(Term definition, PosInOccurrence envPIO)(Code) | | Parameters: definitionPIO - the distance to the quantifier that can be eliminated;Integer.MAX_VALUE if the subformula is not aneliminable definition |
isEliminableVariableAllPaths | public boolean isEliminableVariableAllPaths(QuantifiableVariable var, Term matrix, boolean ex)(Code) | | The variable var is eliminable on all
conjunctive/disjunctive paths through matrix (depending on
whether ex is true/false)
|
isEliminableVariableSomePaths | public boolean isEliminableVariableSomePaths(QuantifiableVariable var, Term matrix, boolean ex)(Code) | | The variable var is either eliminable or does not occur on
all conjunctive/disjunctive paths through matrix
(depending on whether ex is true/false)
|
|
|