de.uka.ilkd.key.strategy.quantifierHeuristics

Class QuanEliminationAnalyser

java.lang.Object

de.uka.ilkd.key.strategy.quantifierHeuristics.QuanEliminationAnalyser

public class QuanEliminationAnalyser
extends java.lang.Object

Constructor Summary

Constructors

Constructor and Description
QuanEliminationAnalyser()

Method Summary

Modifier and Type	Method and Description
int	eliminableDefinition(Term definition, PosInOccurrence envPIO)
private boolean	hasDefinitionShape(Term t, boolean ex)
private boolean	isBelowOr(Term t, Term env)
private boolean	isDefiningEquation(Term t, QuantifiableVariable var)
private boolean	isDefiningEquationAll(Term t, QuantifiableVariable var)
private boolean	isDefiningEquationEx(Term t, QuantifiableVariable var)
private boolean	isDefinition(Term t, QuantifiableVariable var, boolean ex)
private boolean	isDefinitionCandidate(Term t, Term env, boolean ex)
private boolean	isDefinitionEx(Term t, QuantifiableVariable var)
boolean	isEliminableVariableAllPaths(QuantifiableVariable var, Term matrix, boolean ex) The variable var is eliminable on all conjunctive/disjunctive paths through matrix (depending on whether ex is true/false)
boolean	isEliminableVariableSomePaths(QuantifiableVariable var, Term matrix, boolean ex) The variable var is either eliminable or does not occur on all conjunctive/disjunctive paths through matrix (depending on whether ex is true/false)
private PosInOccurrence	walkUpMatrix(PosInOccurrence pio)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

QuanEliminationAnalyser

public QuanEliminationAnalyser()

Method Detail

eliminableDefinition

public int eliminableDefinition(Term definition,
                                PosInOccurrence envPIO)

Parameters:

definition -

Returns:

the distance to the quantifier that can be eliminated; Integer.MAX_VALUE if the subformula is not an eliminable definition

isDefinitionCandidate

private boolean isDefinitionCandidate(Term t,
                                      Term env,
                                      boolean ex)

isBelowOr

private boolean isBelowOr(Term t,
                          Term env)

hasDefinitionShape

private boolean hasDefinitionShape(Term t,
                                   boolean ex)

walkUpMatrix

private PosInOccurrence walkUpMatrix(PosInOccurrence pio)

isEliminableVariableSomePaths

public boolean isEliminableVariableSomePaths(QuantifiableVariable var,
                                             Term matrix,
                                             boolean ex)

The variable var is either eliminable or does not occur on all conjunctive/disjunctive paths through matrix (depending on whether ex is true/false)

isEliminableVariableAllPaths

public boolean isEliminableVariableAllPaths(QuantifiableVariable var,
                                            Term matrix,
                                            boolean ex)

The variable var is eliminable on all conjunctive/disjunctive paths through matrix (depending on whether ex is true/false)

isDefinition

private boolean isDefinition(Term t,
                             QuantifiableVariable var,
                             boolean ex)

isDefinitionEx

private boolean isDefinitionEx(Term t,
                               QuantifiableVariable var)

isDefiningEquationAll

private boolean isDefiningEquationAll(Term t,
                                      QuantifiableVariable var)

isDefiningEquationEx

private boolean isDefiningEquationEx(Term t,
                                     QuantifiableVariable var)

isDefiningEquation

private boolean isDefiningEquation(Term t,
                                   QuantifiableVariable var)