public class QuanEliminationAnalyser
extends java.lang.Object
Constructor and Description |
---|
QuanEliminationAnalyser() |
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) |
public int eliminableDefinition(Term definition, PosInOccurrence envPIO)
definition
- Integer.MAX_VALUE
if the subformula is not an
eliminable definitionprivate boolean hasDefinitionShape(Term t, boolean ex)
private PosInOccurrence walkUpMatrix(PosInOccurrence pio)
public boolean isEliminableVariableSomePaths(QuantifiableVariable var, Term matrix, boolean ex)
var
is either eliminable or does not occur on
all conjunctive/disjunctive paths through matrix
(depending on whether ex
is true/false)public boolean isEliminableVariableAllPaths(QuantifiableVariable var, Term matrix, boolean ex)
var
is eliminable on all
conjunctive/disjunctive paths through matrix
(depending on
whether ex
is true/false)private boolean isDefinition(Term t, QuantifiableVariable var, boolean ex)
private boolean isDefinitionEx(Term t, QuantifiableVariable var)
private boolean isDefiningEquationAll(Term t, QuantifiableVariable var)
private boolean isDefiningEquationEx(Term t, QuantifiableVariable var)
private boolean isDefiningEquation(Term t, QuantifiableVariable var)