| java.lang.Object
 de.uka.ilkd.key.strategy.termgenerator.RootsGenerator
| RootsGenerator | | public class RootsGenerator implements TermGenerator(Code) | | Term generator for infering the range of values that a variable can have from
a given non-linear (in)equation. The generator may only be called on formulas
of the form
v^n = l, v^n <= l, v^n >= l,
where v is an atomic term (does not start with
addition or multiplication) and l is a literal. The generator will
then produce at most one formula that describes the solutions of the formula
using linear (in)equations.
|
|
|