| java.lang.Object de.uka.ilkd.key.rule.AbstractIntegerRule
All known Subclasses: de.uka.ilkd.key.rule.CVC3IntegerRule, de.uka.ilkd.key.rule.SVCIntegerRule, de.uka.ilkd.key.rule.CVCLiteIntegerRule, de.uka.ilkd.key.rule.SmtTranslationIntegerRule, de.uka.ilkd.key.rule.ICSIntegerRule, de.uka.ilkd.key.rule.YicesIntegerRule, de.uka.ilkd.key.rule.SimplifyIntegerRule,
AbstractIntegerRule | abstract public class AbstractIntegerRule implements BuiltInRule(Code) | | Abstract base class for ICS and Simplify built-in rules.
|
showResults | final protected boolean showResults(Code) | | |
getDecisionProcedure | abstract protected AbstractDecisionProcedure getDecisionProcedure(Goal goal, Constraint userConstraint, Services services)(Code) | | Get the decision procedure invoked by this rule.
Parameters: goal - the goal on which the decision procedure should operate. Parameters: userConstraint - the user constraint the decision procedure |
isApplicable | public boolean isApplicable(Goal goal, PosInOccurrence pio, Constraint userConstraint)(Code) | | returns true iff a rule is applicable at the given
position. This does not necessary mean that a rule application
will change the goal (this decision is made due to performance
reasons)
|
|
|