public abstract class AbstractMonomialSmallerThanFeature extends SmallerThanFeature
Modifier and Type | Class and Description |
---|---|
private class |
AbstractMonomialSmallerThanFeature.AtomCollector |
SmallerThanFeature.Collector
Modifier and Type | Field and Description |
---|---|
private Function |
add |
private Goal |
currentGoal |
private Function |
mul |
private static Name |
newSymRuleSetName |
private Function |
Z |
TOP_COST, ZERO_COST
Modifier | Constructor and Description |
---|---|
protected |
AbstractMonomialSmallerThanFeature(IntegerLDT numbers) |
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<Term> |
collectAtoms(Term t) |
protected Goal |
getCurrentGoal() |
private boolean |
inNewSmallSymRuleSet(TacletApp tapp) |
private boolean |
introducesSkolemSymbol(TacletApp tapp,
Operator op) |
protected int |
introductionTime(Operator op,
ServiceCaches caches) |
private int |
introductionTimeHelp(Operator op) |
protected void |
setCurrentGoal(Goal currentGoal) |
compare, lessThan, lessThan
filter, filter
computeCost
private static final Name newSymRuleSetName
private final Function add
private final Function mul
private final Function Z
private Goal currentGoal
protected AbstractMonomialSmallerThanFeature(IntegerLDT numbers)
protected int introductionTime(Operator op, ServiceCaches caches)
private int introductionTimeHelp(Operator op)
private boolean inNewSmallSymRuleSet(TacletApp tapp)
protected ImmutableList<Term> collectAtoms(Term t)
protected void setCurrentGoal(Goal currentGoal)
currentGoal
- The currentGoal to set.protected Goal getCurrentGoal()