Region Decomposition Basics

Region decompositions are declared using the [@@decomp ...] attribute on a function definition. The primary entry point is top, which decomposes the entire input space into disjoint regions.

The [@@decomp top ()] attribute

let f x = if x = 1 || x = 2 then x + 1 else x - 1
[@@decomp top ()]

This decomposes the entire input space of f into disjoint regions, each with constraints and an invariant.

Example

let classify age =
  if age < 0 then "invalid"
  else if age < 13 then "child"
  else if age < 18 then "teenager"
  else if age < 65 then "adult"
  else "senior"
[@@decomp top ()]

This produces five regions:

  1. age < 0 → "invalid"
  2. 0 ≤ age < 13 → "child"
  3. 13 ≤ age < 18 → "teenager"
  4. 18 ≤ age < 65 → "adult"
  5. age ≥ 65 → "senior"

Optional parameters

~assuming — Side-conditions

Restrict the decomposition to inputs satisfying a given predicate. This yields all unique regions of behavior under the assumption that the side-condition holds. Use [%id ...] to reference the assumption function:

let asm x = x > 1
 
let g x = if x > 10 then x * 2 else x + 5
[@@decomp top ~assuming:[%id asm] ()]

This decomposes g only over inputs where asm holds (i.e., x > 1), potentially producing fewer regions. Side-conditions and basis are orthogonal — you can use them independently or together.

~basis — Abstraction boundaries

Every decomposition is performed with respect to a basis — a collection of function symbols treated as atomic concepts. Basis functions' definitions are not expanded and do not contribute case-splits during decomposition, but they are interpreted when deciding feasibility of purported regions. This means infeasible regions involving basis functions are still correctly pruned.

let g x = if f x > x then -1 else 1
[@@decomp top ~basis:[ [%id f] ] ()]

The decomposition of g will treat f as an opaque function, producing regions in terms of f x rather than expanding f's definition. You can later merge f's own decomposition in using the << operator (see Composition).

~ctx_simp — Contextual simplification

Enable contextual simplification (value propagation and rewriting) during decomposition:

let h x y = if x > 0 then x + y else y - x
[@@decomp top ~ctx_simp:true ()]

~prune — Prune infeasible regions

Attempt feasibility checking of each region's constraints and remove regions with unsatisfiable constraints:

let f x = if x > 0 && x < 0 then 1 else 2
[@@decomp top ~prune:true ()]

~rule_specs — Background axioms

Specify rule specifications (lemmas annotated with [@@rw] and [@@imandra_rule_spec]) to guide rewriting and forward-chaining during decomposition:

let map_recons len f x = ...
[@@rw] [@@imandra_rule_spec]
 
let map_cons_eval f x y = ...
[@@rw] [@@imandra_rule_spec]
 
let result = my_function
[@@decomp top ~rule_specs:[ [%id map_recons]; [%id map_cons_eval] ] ()]

Understanding the output

Each region in the decomposition contains:

  • Constraints (cs) — A conjunction of conditions on the input variables that define the region
  • Invariant (inv) — A symbolic expression describing the function's output in terms of the input variables

The regions satisfy:

  • Local correctness — For each region, if its constraints hold for an input, then the function's value equals its invariant
  • Coverage — The disjunction of all region constraints is a tautology (modulo background theories and any ~assuming side-condition). Every possible input belongs to at least one region
  • Feasibility — Every returned region is satisfiable — it has at least one concrete input satisfying its constraints. Concrete sample points (witnesses) can be synthesized on demand for test-case generation
  • Semantically meaningful — Each region corresponds to a distinct computational path through the function

Decompositions are first-class values — they can be printed, composed, refined, and serialized.

Recursive functions

Region decomposition works with recursive functions too. ImandraX unrolls the recursion and analyzes the resulting regions:

let rec gcd a b =
  if b = 0 then a
  else gcd b (a mod b)
[@@decomp top ()]

For recursive functions, the decomposition captures the distinct patterns of recursion depth and base-case behavior.

Previous← Region Decomposition
NextComposition →