Region Decomposition

Region decomposition is one of ImandraX's most distinctive and powerful capabilities. Given a function, it exhaustively decomposes the input space into disjoint regions, each characterized by a set of constraints and an invariant describing the function's behavior in that region.

Think of it as an X-ray of your function: instead of testing individual inputs, you see every possible behavior at once.

What is a region?

A region is a subset of the input space defined by a conjunction of constraints (cs), together with an invariant (inv) — a symbolic expression describing the function's output in that region.

Given a function f, decomposition produces a collection of regions [{cs_0, inv_0}, {cs_1, inv_1}, ..., {cs_m, inv_m}] satisfying two key properties:

1. Local correctness — For each region i, if the constraints cs_i hold for an input, then the function's value equals the invariant: cs_i(x) ==> f(x) = inv_i(x).
2. Coverage — The disjunction of all region constraints is a tautology (modulo background theories): every input belongs to at least one region.

Crucially, the function is equal to the union of all its regions — this is not a sequential if-then-else chain, but a collection of independently valid local descriptions that together cover the entire input space. All returned regions are guaranteed to be feasible — each has at least one satisfying input, and concrete sample points (witnesses) can be synthesized on demand for test-case generation and exploration.

Decompositions are always performed with respect to a basis — the collection of function symbols treated as atomic concepts during decomposition. Basis functions' definitions are not expanded or used to generate case-splits, but they are interpreted for deciding feasibility of purported regions. Separately, a side-condition (~assuming) can restrict the decomposition to inputs where a given predicate holds, yielding all unique regions of behavior under that assumption. See Basics for details on both.

For example, given:

let f x =
  if x > 99 then 100
  else if x > 20 then x + 9
  else if x > -2 then 103
  else 99
[@@decomp top ()]

Region decomposition produces:

Each region is locally correct (if its constraints hold, the invariant is true), and together the regions provide complete coverage of the input space. Each invariant is a proved fact about the function's behavior in that region.

Why region decomposition matters

Region decomposition is invaluable for:

• Test generation — Automatically generate test cases covering every behavioral region. One test per region gives complete behavioral coverage.
• Coverage analysis — Understand exactly how many distinct behaviors a function has. Compare this against your specification to find missing cases.
• Regulatory compliance — In financial services and safety-critical systems, regulators require evidence of exhaustive analysis. Region decomposition provides mathematically rigorous coverage.
• Specification discovery — Understand complex functions you didn't write. Region decomposition reveals the implicit specification embedded in the code.
• Debugging — When a function has unexpected behavior, its region decomposition often makes the bug obvious — a region with the wrong invariant, or a missing region.

In this section

• Basics — Using top, ~assuming, ~basis, and interpreting results
• Composition — Composing decompositions with operators
• Refiners — Pruning, enumerating, and merging regions
• Applications — Real-world uses: test generation, compliance, analysis