| java.lang.Object de.uka.ilkd.key.proof.mgt.QuantifierEliminator
QuantifierEliminator | public class QuantifierEliminator (Code) | | Pre-processor for MethodSpecTransformation .
Pull out quantifiers from a formula, only leaving over subformulas of the
shape all x. f@pre(...) = t (such subformulas are removed by
MethodSpecTransformation ).
|
getQuantifierFreeFormula | public Term getQuantifierFreeFormula()(Code) | | Returns the quantifierFreeFormula. |
getQuantifiers | public ListOfQuantifierPrefixEntry getQuantifiers()(Code) | | Returns the quantifiers. |
|
|