public class QuanEliminationAnalyser
extends java.lang.Object
Constructor and Description |
---|
QuanEliminationAnalyser() |
Modifier and Type | Method and Description |
---|---|
int |
eliminableDefinition(Term definition,
PosInOccurrence envPIO) |
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) |
public int eliminableDefinition(Term definition, PosInOccurrence envPIO)
definition
- Integer.MAX_VALUE
if the subformula is not an
eliminable definitionpublic 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)Copyright © 2003-2019 The KeY-Project.