[Termtools] termination competition changes

[Lars Noschinski]

* Johannes Waldmann <waldmann at imn.htwk-leipzig.de> [09-02-25 16:02]:
> PS: I think Booleans do not belong into Integer. SMT-LIB of course
> avoids this problem because they have truth values "for free".

If we do not do a module system allowing stacking, we need Booleans in
the Integer module - perhaps we could avoid the Boolean operations, but
not the boolean constants.

As a low-tech solution, the user could just introduce conversion rules
like

    toBoolean(Integer.True) -> True
    toBoolean(Bitvectors.True) -> True

and use these for inter-module boolean stuff. I think, together with
arbitrary prefixes, this would be a 'good enough' solution.