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), so 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. With pruning on (~prune:true or |>> prune), regions proved empty are removed, and each region proved feasible carries a witness, a concrete input usable for test-case generation and exploration. A region whose feasibility check fails (on a timeout, for example) is kept without a witness and may still be empty. Without pruning, regions are not checked and may be empty.

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 four regions:

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 used 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, as a region with the wrong invariant or a missing region.

In this section

• Basics: using top, ~assuming, ~basis, and reading the results
• Composition: composing decompositions with operators
• Refiners: pruning, combining, and enumerating regions
• Applications: test generation, compliance, analysis