Refiners

Refiners transform region decompositions — pruning infeasible regions, enumerating concrete instances, or merging related regions. They are applied using the |>> pipe operator within a [@@decomp ...] attribute.

prune

Remove infeasible regions — regions whose constraints are unsatisfiable:

let d = f
[@@decomp top () |>> prune]

Pruning uses decision procedures to check satisfiability of each region's constraints. Regions with contradictory constraints are removed.

enumerate

Generate a concrete representative instance for each region:

let d = f
[@@decomp top () |>> enumerate]

Each region gets a representative input value satisfying its constraints. This is the basis for automated test generation: one test per region gives complete behavioral coverage.

enumerate_all

Like enumerate, but generates multiple instances per region:

let d = f
[@@decomp top () |>> enumerate_all]

Both enumerate and enumerate_all support style options: Additive or Multiplicative.

merge_

Merge adjacent regions that share the same invariant:

let d = f
[@@decomp top () |>> merge_]

This simplifies the decomposition by combining regions that differ only in their constraints but produce the same output. This is the underlying refiner used by the << operator.

compound_merge_

A more aggressive merging strategy that considers constraint subsumption:

let d = f
[@@decomp top () |>> compound_merge_]

This is the underlying refiner used by the <|< operator.

Rule specifications

Functions annotated with [@@rw] and [@@imandra_rule_spec] serve as background axioms during decomposition, enabling rewriting and forward-chaining:

let map_recons len f x = ...
[@@rw] [@@imandra_rule_spec]
 
let map_cons_eval f x y = ...
[@@rw] [@@imandra_rule_spec]

These are referenced via ~rule_specs:[ [%id map_recons]; [%id map_cons_eval] ] in the top call. Rule specifications are advanced features used when the default decomposition needs customization for domain-specific analysis.

Chaining refiners

Refiners can be chained:

let d = f
[@@decomp top () |>> prune |>> enumerate]

This first prunes infeasible regions, then generates concrete instances for each surviving region.