Grounder avoids additional names in cases like the Bool simulation.
When all terms of a given sort occur only in literals like (t = n) and (t = x), but not nested or in terms like (t = t'), no additional names are needed for splitting. The prototypical case is when we simulate relations with functions of sort Bool and use two names TRUE and FALSE. Then we don't want to split over a third value.
Loading
Please register or sign in to comment