| java.lang.Object
 de.uka.ilkd.key.logic.DepthTermOrdering
All known Subclasses: de.uka.ilkd.key.logic.CascadeDepthTermOrdering,
| DepthTermOrdering | | public class DepthTermOrdering implements TermOrdering(Code) | | Term ordering, comparing the maximum depths of terms and contained
variables; following definition 5.14 in the script "Automatisches
Beweisen", Bernhard Beckert, Reiner Haehnle
|
| compare | | public int compare(Term p_a, Term p_b)(Code) | | Compare the two given terms
a number negative, zero or a number positive ifp_a is less than, equal, or greater thanp_b regarding the ordering given by theimplementing class |
| compareVars | | protected int compareVars(DepthCollector p_depthsA, DepthCollector p_depthsB)(Code) | | a negative number, if each variable collected byp_depthsA has also been collected byp_depthsB, and p_depthsB has alsofound a greater maximum depth for that variable; zero otherwise |
|
|