Simplify return type of int domain comparison predicates

[sim642]

This is like #1906 but for all the int domains.

This makes the implementations of the domains slightly nicer. But it also makes most usages of these predicates easier by not having to always use ID.to_bool around them.

It also avoids strange inconsistencies that previously existed between the domains, where some returned an abstraction of just 0 or 1, but others returned top int. Now this is defined once and for all in base which has the only non-to_bool usage of these comparisons.

TODO

• Use [0,1] interval for normal evaluation result.

[Copilot]

Pull request overview

This PR updates all integer value domains so comparison predicates (lt, gt, le, ge, eq, ne) return bool option instead of an int-domain value, simplifying domain implementations and downstream uses (eliminating most to_bool wrappers and standardizing “unknown” results).

Changes:

• Change the IntDomain predicate signatures to bool option and update domain implementations accordingly.
• Adapt analyses/utilities which consume comparisons (e.g., base evaluation, OOB checks) to handle bool option directly (and reintroduce [0,1] when an int result is required).
• Update unit tests and property-based tests for the new predicate return type.

Reviewed changes

Copilot reviewed 16 out of 16 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
tests/unit/cdomains/intDomainTest.ml	Adjusts assertions to expect bool option results from comparisons.
src/domains/intDomainProperties.ml	Updates IntegerSet-based properties to aggregate bool option predicate results and adapts validity checks.
src/cdomain/value/cdomains/offset.ml	Removes Idx.to_bool wrapper since Idx.eq now returns bool option.
src/cdomain/value/cdomains/intDomain_intf.ml	Changes predicate signatures in the int-domain interfaces to bool option.
src/cdomain/value/cdomains/intDomain0.ml	Updates lifted int-domain predicate plumbing to return bool option.
src/cdomain/value/cdomains/int/intervalSetDomain.ml	Converts comparison implementations to return bool option and simplifies boolean negation handling.
src/cdomain/value/cdomains/int/intervalDomain.ml	Converts interval comparisons to bool option.
src/cdomain/value/cdomains/int/intDomTuple.ml	Adapts tuple domain to map/merge bool option predicate results across subdomains.
src/cdomain/value/cdomains/int/enumsDomain.ml	Converts comparisons to bool option and updates ne accordingly.
src/cdomain/value/cdomains/int/defExcDomain.ml	Converts equality predicates to bool option and adjusts logical-not handling.
src/cdomain/value/cdomains/int/congruenceDomain.ml	Converts comparisons to bool option and updates tracing pretty-printers.
src/cdomain/value/cdomains/int/bitfieldDomain.ml	Converts comparisons to bool option and simplifies ne.
src/cdomain/value/cdomains/arrayDomain.ml	Uses bool option comparisons directly for array OOB checks.
src/analyses/memOutOfBounds.ml	Removes to_bool wrapper around predicate results and handles bool option directly.
src/analyses/baseInvariant.ml	Updates sign checks to compare predicate results directly to Some true.
src/analyses/base.ml	Introduces helper to convert bool option predicate results back into [0,1] int intervals where needed by expression evaluation.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.