D-SMALLEST : INFO

D-SMALLEST is a flag setting or other piece of information.
A setting for DEFAULT-OB.
The default next obligation in mtree is the deepest element of the
set of smallest obligations (i.e. given the set of all obligations with
the fewest possible literals, the first element of this set to be found
by depth-first search).

TPS documentation homepage


© 1988-99, Carnegie Mellon University.

TPS homepage