Region Decomposition

The term Region Decomposition refers to a (geometrically inspired) "slicing" of an algorithm’s state-space into distinct regions where the behavior of the algorithm is invariant, i.e., where it behaves "the same."

Each "slice" or region of the state-space describes a family of inputs and the output of the algorithm upon them, both of which may be symbolic and represent (potentially infinitely) many concrete instances.

The entrypoint to decomposition is the Modular_decomp.top function, here's a quick basic example of how it can be used:

In [1]:
let target x =
  if x > 0 then
    1
  else
    -1
;;

let d = Modular_decomp.top "target" [@@program]
Out[1]:
val target : Z.t -> Z.t = <fun>
val d : Modular_decomp_intf.decomp_ref = <abstr>
Regions details

No group selected.

  • Concrete regions are numbered
  • Unnumbered regions are groups whose children share a particular constraint
  • Click on a region to view its details
  • Double click on a region to zoom in on it
  • Shift+double click to zoom out
  • Hit escape to reset back to the top
decomp of (target x
Reg_idConstraintsInvariant
1
  • not (x > 0)
(-1)
0
  • x > 0
1

Imandra decomposed the function target into 2 regions: the first region tells us that whenever the input argument x is less than or equal to 0, then the value returned by the function will be -1, the second region tells us that whenever x is positive, the output will be 1.

Aside: Voronoi diagrams

When performing a region decomposition in a Jupyter notebook, the Imandra plugin will render the result as a Voronoi diagram.

To render a Voronoi diagram from the REPL, use Imandra_voronoi.Voronoi.print:

# let target x = if x > 0 then 1 else -1;;
val target : int -> int = <fun>

# let d = Modular_decomp.top "target" [@@program];;
- Beginning modular decomposition of target.
* Computing fresh modular decomposition for target
- Computed 2 regions.
- Target modular decomposition of target complete (2 regions).
- Integration complete in 0 rounds (2 regions).
val d : Top_result.modular_decomposition =
  {Imandra_interactive.Modular_decomp.MD.ipynb_session = 1i;
   md_f =
    {Imandra_surface.Uid.name = "target"; id = <abstr>;
     special_tag = <abstr>; namespace = <abstr>;
     chash = Some IJllFgjXGBXdmGllO51yKe2dFt1V0i4n85B2RT8f5B0;
     depth = (3i, 1i)};
   md_args = [(x : int)]; md_regions = <abstr>}

# Imandra_voronoi.Voronoi.print () Format.std_formatter d;;
Open: file:////var/folders/y2/bzjbz5bj0s91lz0mx42q_jd80000gn/T/voronoi_822f8d.html
- : unit = ()

Then open the temporary file in your browser.

Alternatively, you can install the Voronoi printer to generate a diagram for every decomposition:

# let pp_voronoi = Imandra_voronoi.Voronoi.print () [@@program];;
val pp_voronoi : Format.formatter -> Top_result.modular_decomposition -> unit =
  <fun>

# #install_printer pp_voronoi;;

# let target x = if x > 0 then 1 else -1;;
val target : int -> int = <fun>

# Modular_decomp.top "target";;
- Beginning modular decomposition of target.
* Computing fresh modular decomposition for target
- Computed 2 regions.
- Target modular decomposition of target complete (2 regions).
- Integration complete in 0 rounds (2 regions).
- : Top_result.modular_decomposition =
Open: file:////var/folders/y2/bzjbz5bj0s91lz0mx42q_jd80000gn/T/voronoi_8710d3.html

Api

At its very core, modular decomposition allows us to "splice" the state space of a function into (possibly infeasible) regions of behavior.

In [2]:
let f x = if x > 0 then if x * x < 0 then x else x + 1 else x;;
let d = Modular_decomp.top "f" [@@program];;
Out[2]:
val f : Z.t -> Z.t = <fun>
val d : Modular_decomp_intf.decomp_ref = <abstr>
Regions details

No group selected.

  • Concrete regions are numbered
  • Unnumbered regions are groups whose children share a particular constraint
  • Click on a region to view its details
  • Double click on a region to zoom in on it
  • Shift+double click to zoom out
  • Hit escape to reset back to the top
decomp of (f x
Reg_idConstraintsInvariant
2
  • not (x > 0)
x
1
  • not (x * x < 0)
  • x > 0
x + 1
0
  • x * x < 0
  • x > 0
x

A side condition can be specified to inject extra constraints about the target function, this can be used to constrain and/or partition the explored state space

In [3]:
let g x = x < 0;;
let d1 = Modular_decomp.top ~assuming:"g" "f" [@@program];;

let h x = x < 0 && (x > -5 || x < -6);;
let d2 = Modular_decomp.top ~assuming:"h" "f" [@@program];;
Out[3]:
val g : Z.t -> bool = <fun>
val d1 : Modular_decomp_intf.decomp_ref = <abstr>
val h : Z.t -> bool = <fun>
val d2 : Modular_decomp_intf.decomp_ref = <abstr>
Regions details

No group selected.

  • Concrete regions are numbered
  • Unnumbered regions are groups whose children share a particular constraint
  • Click on a region to view its details
  • Double click on a region to zoom in on it
  • Shift+double click to zoom out
  • Hit escape to reset back to the top
decomp of (f x
Reg_idConstraintsInvariant
0
  • x < 0
  • not (x > 0)
x
Regions details

No group selected.

  • Concrete regions are numbered
  • Unnumbered regions are groups whose children share a particular constraint
  • Click on a region to view its details
  • Double click on a region to zoom in on it
  • Shift+double click to zoom out
  • Hit escape to reset back to the top
decomp of (f x
Reg_idConstraintsInvariant
1
  • x < 0
  • not (x > (-5))
  • x < (-6)
  • not (x > 0)
x
0
  • x < 0
  • x > (-5)
  • not (x > 0)
x

Pruning instructs modular decomposition to solve all the regions for feasibility using unrolling and throw away infeasible ones

In [4]:
let d = Modular_decomp.top ~prune:true "f" [@@program];;
Out[4]:
val d : Modular_decomp_intf.decomp_ref = <abstr>
Regions details

No group selected.

  • Concrete regions are numbered
  • Unnumbered regions are groups whose children share a particular constraint
  • Click on a region to view its details
  • Double click on a region to zoom in on it
  • Shift+double click to zoom out
  • Hit escape to reset back to the top
decomp of (f x
Reg_idConstraintsInvariant
2
  • not (x > 0)
x
1
  • not (x * x < 0)
  • x > 0
x + 1
0
  • x * x < 0
  • x > 0
x

In some cases feasibility is not known via unrolling, so pruning may return regions of unknown feasibility

In [5]:
let i (x : int list) = if (x = List.rev @@ List.rev x) then 1 else 2;;

let d = Modular_decomp.top ~prune:true "i" [@@program];;

d |> Modular_decomp.get_concrete_regions |> CCList.map (fun r -> r, Modular_region.(show_status @@ status r));;
Out[5]:
val i : Z.t list -> Z.t = <fun>
val d : Modular_decomp_intf.decomp_ref = <abstr>
- : (Top_result.modular_region * string) list =
[({Constraints:
     [not (x = List.rev (List.rev x))]
   Invariant:
     2},
  "Feasibility_status.Unknown");
 ({Constraints:
     [x = List.rev (List.rev x)]
   Invariant:
     1},
  "Feasibility_status.Unknown")]
Regions details

No group selected.

  • Concrete regions are numbered
  • Unnumbered regions are groups whose children share a particular constraint
  • Click on a region to view its details
  • Double click on a region to zoom in on it
  • Shift+double click to zoom out
  • Hit escape to reset back to the top
decomp of (i x
Reg_idConstraintsInvariant
1
  • x = List.rev (List.rev x)
1
0
  • not (x = List.rev (List.rev x))
2

Recursive functions are not expanded, nor functions belonging to the "basis" (but pruning can still unroll them when solving for feasibility)

In [6]:
let j x = if f x = x then 1 else 2;;
let d = Modular_decomp.top ~prune:true ~basis:["f"] "j" [@@program];;
Out[6]:
val j : Z.t -> Z.t = <fun>
val d : Modular_decomp_intf.decomp_ref = <abstr>
Regions details

No group selected.

  • Concrete regions are numbered
  • Unnumbered regions are groups whose children share a particular constraint
  • Click on a region to view its details
  • Double click on a region to zoom in on it
  • Shift+double click to zoom out
  • Hit escape to reset back to the top
decomp of (j x
Reg_idConstraintsInvariant
1
  • not (f x = x)
2
0
  • f x = x
1

A model satisfying the region constraints can be extracted for feasible regions

In [7]:
Modular_decomp.(d |> get_regions |> CCList.map get_model);;
Out[7]:
- : Top_result.model list =
[{Imandra_surface.Term.Model.tys = []; consts = [((x : int), 0)]; funs = [];
  representable = true};
 {Imandra_surface.Term.Model.tys = []; consts = [((x : int), 1)]; funs = [];
  representable = true}]

The model can be turned into a computable value by generating an extractor for the target function

In [8]:
Extract.eval ~signature:(Event.DB.fun_id_of_str (db()) "j") ~quiet:true ();;
Modular_decomp.(d |> get_regions |> CCList.map (get_model %> Mex.of_model));;
Out[8]:
- : unit = ()
- : Mex.extract_type list = [{Mex.x = 0};{Mex.x = 1}]

Regions can be manually refined with terms in order to add extra constraints (refining automatically prunes)

In [9]:
let d1 = Modular_decomp.(top ~prune:true "f" |> get_regions |> CCList.filter_map (fun r -> refine r [Term.false_])) [@@program];;

let d2 = Modular_decomp.(
    let d = top ~prune:true "f" in
    let arg = Remote_ref.get_shared_block d |> Modular_decomposition.args |> List.hd |> Term.var in
    d
    |> get_regions
    |> CCList.filter_map
         (fun r ->
           refine r
             (* x = 1 *)
             [Term.eq ~ty:Type.int arg (Term.int 1)])) [@@program];;
Out[9]:
val d1 : Modular_decomp_intf.region_ref list = []
val d2 : Modular_decomp_intf.region_ref list = [<abstr>]
Regions details

No group selected.

  • Concrete regions are numbered
  • Unnumbered regions are groups whose children share a particular constraint
  • Click on a region to view its details
  • Double click on a region to zoom in on it
  • Shift+double click to zoom out
  • Hit escape to reset back to the top
decomp of (f x
Reg_idConstraintsInvariant
2
  • not (x > 0)
x
1
  • not (x * x < 0)
  • x > 0
x + 1
0
  • x * x < 0
  • x > 0
x
Regions details

No group selected.

  • Concrete regions are numbered
  • Unnumbered regions are groups whose children share a particular constraint
  • Click on a region to view its details
  • Double click on a region to zoom in on it
  • Shift+double click to zoom out
  • Hit escape to reset back to the top
decomp of (f x
Reg_idConstraintsInvariant
2
  • not (x > 0)
x
1
  • not (x * x < 0)
  • x > 0
x + 1
0
  • x * x < 0
  • x > 0
x