de.uka.ilkd.key.strategy.feature

Class AbstractMonomialSmallerThanFeature

java.lang.Object

de.uka.ilkd.key.strategy.feature.BinaryFeature

de.uka.ilkd.key.strategy.feature.BinaryTacletAppFeature

de.uka.ilkd.key.strategy.feature.SmallerThanFeature

de.uka.ilkd.key.strategy.feature.AbstractMonomialSmallerThanFeature

All Implemented Interfaces:

Feature

Direct Known Subclasses:

AtomsSmallerThanFeature, MonomialsSmallerThanFeature

public abstract class AbstractMonomialSmallerThanFeature
extends SmallerThanFeature

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	AbstractMonomialSmallerThanFeature.AtomCollector

Nested classes/interfaces inherited from class de.uka.ilkd.key.strategy.feature.SmallerThanFeature

SmallerThanFeature.Collector

Field Summary

Fields

Modifier and Type	Field and Description
private Function	add
private Function	mul
private static Name	newSymRuleSetName
private Function	Z

Fields inherited from class de.uka.ilkd.key.strategy.feature.BinaryFeature

TOP_COST, ZERO_COST

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	AbstractMonomialSmallerThanFeature(IntegerLDT numbers)

Method Summary

Modifier and Type	Method and Description
protected ImmutableList<Term>	collectAtoms(Term t)
private boolean	inNewSmallSymRuleSet(TacletApp tapp)
private boolean	introducesSkolemSymbol(TacletApp tapp, Operator op)
protected int	introductionTime(Operator op, Goal goal)
private int	introductionTimeHelp(Operator op, Goal goal)

Methods inherited from class de.uka.ilkd.key.strategy.feature.SmallerThanFeature

compare, lessThan, lessThan

Methods inherited from class de.uka.ilkd.key.strategy.feature.BinaryTacletAppFeature

filter, filter

Methods inherited from class de.uka.ilkd.key.strategy.feature.BinaryFeature

computeCost

Methods inherited from class java.lang.Object

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

Field Detail

newSymRuleSetName

private static final Name newSymRuleSetName

add

private final Function add

mul

private final Function mul

Z

private final Function Z

Constructor Detail

AbstractMonomialSmallerThanFeature

protected AbstractMonomialSmallerThanFeature(IntegerLDT numbers)

Method Detail

introductionTime

protected int introductionTime(Operator op,
                               Goal goal)

introductionTimeHelp

private int introductionTimeHelp(Operator op,
                                 Goal goal)

introducesSkolemSymbol

private boolean introducesSkolemSymbol(TacletApp tapp,
                                       Operator op)

inNewSmallSymRuleSet

private boolean inNewSmallSymRuleSet(TacletApp tapp)

collectAtoms

protected ImmutableList<Term> collectAtoms(Term t)