Give the given constants bottom status.
Set the status of the given constants to the top value (as free as possible)
List all constants whose status is different in
Determine whether the formula
lc1 - lc2 = 0 & phi is shielded
Given a constraint from which all shielded parts have been removed, determine which constants have to be considered as non-free
Only used for runtime assertion purposes
c is a formula of the shape
a*x + t = 0 & phi , where
a != 0 and
x is a quasi-universal constant that is maximal in
a*x + t = 0 .
Determine the (disjunctively connected) unshielded part of a formula