# 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 Decompose.top function, here's a quick basic example of how it can be used:

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

Decompose.top "f"

Out[1]:
val f : int -> Z.t = <fun>
- : Imandra_interactive.Decompose.t list = [<region>; <region>]

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
ConstraintsInvariant
• not (x <= 0)
1
• x <= 0
-1

Imandra decomposed the function "f" 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.

When using Region Decomposition from a REPL instead of from the jupyter notebook, we recommend installing the vornoi printer (producing the above diagram) via #install_printer Imandra_voronoi.Voronoi.print;;

In the rest of this article we'll go over various important flags and arguments accepted by Imandra's Decompose.top entrypoint into its Principal Region Decomposition machinery. As much as possible, we'll use concrete examples to clarify their behaviour.

# Assuming¶

The ~assuming flag is used to add extra axioms as a side-condition to the decomposition of target function. This usually has the effect that regions that don't satisfy the side-condition will be pruned away (although it is not always the case when in presence of non-interpreted functions, see aggressive_rec for a mitigation) but it can also cause constraints to be pruned away or new regions to be discovered when used in combination with ctx_asm_simp.

The side-condition function must be a boolean predicate accepting the same arguments as the target function.

Let's see how it works:

In [2]:
let f x y =
if x > 0 then
if x > y then
Some (x - y)
else
Some (y - x)
else
None

let g x (y : int) = x > 0

Out[2]:
val f : int -> int -> Z.t option = <fun>
val g : int -> int -> bool = <fun>


Let's assume we only care to decompose feasible paths of f when g holds (i.e. when x > 0):

In [3]:
Decompose.top ~assuming:"g" "f"

Out[3]:
- : Imandra_interactive.Decompose.t list = [<region>; <region>]

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
ConstraintsInvariant
• not (x <= 0)
• not (x <= y)
Some (x + -1 * y)
• not (x <= 0)
• x <= y
Some (y + -1 * x)

As we can see, the call to Decompose.top pruned away the region where g didn't hold.

# Compound¶

The ~compound flag instructs Imandra whether or not to expand compound logical statements in conditionals, such as conjunctions and disjunctions, into their constituent parts. With ~compound:true, the decomposition may in general be possible with fewer regions than otherwise, but region constraints and invariants may involve && and ||. This flag doesn't cause any constraints to be removed.

By default, ~compound:false is used.

Let's see how ~compound works in practice on a target function with a compound conditional:

In [4]:
let f x y =
if x > 10 || y < 20 then
1
else
2

Out[4]:
val f : int -> int -> Z.t = <fun>


If we decompose f with ~compound:false, we'll get 3 different regions:

In [5]:
Decompose.top ~compound:false "f"

Out[5]:
- : Imandra_interactive.Decompose.t list = [<region>; <region>; <region>]

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
ConstraintsInvariant
• x <= 10
• 20 <= y
2
• x <= 10
• not (20 <= y)
1
• not (x <= 10)
1

Though all regions are disjoint, we can see that two regions have the same invariant and could be logically collapsed into just one region with a disjunctive constraint. (Hint: click on a region in the Voronoi diagram to see the region's constraints and invariant.) This is where ~compound:true helps us:

In [6]:
Decompose.top ~compound:true "f"

Out[6]:
- : Imandra_interactive.Decompose.t list = [<region>; <region>]

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
ConstraintsInvariant
• x <= 10
• 20 <= y
2
• not (x <= 10) || not (20 <= y)
1

Note that ~compound:true doesn't simply operate on literal &&'s and ||'s in code, but is more general, taking the boolean meaning of nested if statements into account.

# Reduce symmetry¶

The flag ~reduce_symmetry is like ~compound in the sense that it is used to reduce the number of regions output by a decomposition, but through very different means.

This flag is only meaningful when used in combination with side-conditions (assuming), and behaves like a no-op when no-side conditions are present.

When side-conditions are present and reduce_symmetry is true, Imandra uses the information it has been given by the assuming function to find and merge symmetric regions. At a high level, symmetric regions are regions that share some control flow paths which, modulo the assumptions, can be seen to behave identically and thus can be merged.

This flag can cause constraints to be eliminated, so it should be used only when decomposing as means of finding possible behavioural regions rather than as a way to get at all the possible execution paths of a function.

Let's see how this works in practice:

In [7]:
let f x y =
if x + y = 10 then
1
else if x > y then
1
else
2

Out[7]:
val f : int -> int -> Z.t = <fun>


For this particular example (with no compound conditionals), the setting of ~compound is immaterial, so for the sake of demonstrating the behaviour of ~reduce_symmetry:true, we'll decompose with the default ~compound:false setting. Note that in general, with more complex target and side-condition functions than the ones we use here as examples, it is not in general true that ~compound:true subsumes ~reduce_symmetry:true.

If we try to decompose f, we see that we get 3 different regions, as expected, corresponding to the three different branches.

In [8]:
Decompose.top "f"

Out[8]:
- : Imandra_interactive.Decompose.t list = [<region>; <region>; <region>]

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
ConstraintsInvariant
• not (x + y = 10)
• not (x <= y)
1
• not (x + y = 10)
• x <= y
2
• x + y = 10
1

Let's now try to insert a side condition g that simply states that x is always bigger than y:

In [9]:
let g (x:int) y = x > y;;

Decompose.top ~assuming:"g" "f"

Out[9]:
val g : int -> int -> bool = <fun>
- : Imandra_interactive.Decompose.t list = [<region>; <region>]

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
ConstraintsInvariant
• not (x + y = 10)
• not (x <= y)
1
• x + y = 10
1

We've now excluded the third region, as we've asserted that it is never the case that x<=y.

However if we look carefully, we'll notice that both remaining regions have invariants that don't depend on the region constraints, thus if we're doing a decomposition just to analyze all the possible states our f can be in and not to get a concrete listing of all the possible paths through f, we'd like for this decomposition to collapse both regions into one.

In other words, we'd like imandra to understand that for our purposes, f could have been written instead like:

In [10]:
let f' x y =
if x <= y then
2
else
1

Out[10]:
val f' : int -> int -> Z.t = <fun>


This is where ~reduce_symmetry:true helps us:

In [11]:
Decompose.top ~assuming:"g" ~reduce_symmetry:true "f"

Out[11]:
- : Imandra_interactive.Decompose.t list = [<region>]

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
ConstraintsInvariant
1

As you can see, not only did ~reduce_symmetry:true collapse both regions into one, but it also figured out that there are actually no constraints to be held true for this regions's invariant to hold, since all possible values of x and y will cause f x y to evaluate to 1, as we've restricted the functions' domain in the side-condition.

For the curious, this is one of the big differencies between ~reduce_symmetry:true and ~compound:true in this case, as ~compound:true would've merged the two regions and had the constraints in a logical disjunction, but wouldn't have figured out that it could just as well remove the constraints altogether as they always hold true from the side-condition:

In [12]:
Decompose.top ~assuming:"g" ~compound:true "f"

Out[12]:
- : Imandra_interactive.Decompose.t list = [<region>; <region>]

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
ConstraintsInvariant
• not (x + y = 10)
• not (x <= y)
1
• x + y = 10
1

# Ctx_asm_simp¶

~ctx_asm_simp is yet another flag that deals with trying to reduce the number of regions and improve performance. It instructs Imandra whether or not to take the side-conditions into accound when doing a pre-processing step of contextually simplifying the target function. When no side condition is present this is equivalent to a no-op.

When set to true, this can help Imandra simplify some more state space away and make decomposition faster and produce less regions, however it is also possible that this will cause Imandra to spend a lot more time doing simplification and might even cause more regions to be produced, so careful consideration is needed before enabling this.

Let's see how this flag works in practice:

In [13]:
let f x (y:int) =
if y > 0 then
if x > y  then
1
else
2
else
if x < 0 then
3
else
2

Out[13]:
val f : int -> int -> Z.t = <fun>


If we decompose f we get all 4 regions, as expeted:

In [14]:
Decompose.top "f"

Out[14]:
- : Imandra_interactive.Decompose.t list =
[<region>; <region>; <region>; <region>]

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
ConstraintsInvariant
• not (y <= 0)
• not (x <= y)
1
• not (y <= 0)
• x <= y
2
• y <= 0
• not (0 <= x)
3
• y <= 0
• 0 <= x
2

If we then introduce a side-condition g making the first and third branches unreachable:

In [15]:
let g x y =
x + y = 1;;

Decompose.top ~assuming:"g" "f";;

Out[15]:
val g : Z.t -> Z.t -> bool = <fun>
- : Imandra_interactive.Decompose.t list = [<region>; <region>]

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
ConstraintsInvariant
• not (y <= 0)
• x <= y
2
• y <= 0
• 0 <= x
2

The 2 unreachable branches are correctly filtered out by the side-condition. However we notice that both feasabile paths have the same invariant and we would like to collapse them into a single region.

Let's see how ~ctx_asm_simp:true helps us here:

In [16]:
Decompose.top ~compound:false ~ctx_asm_simp:true ~assuming:"g" "f"

Out[16]:
- : Imandra_interactive.Decompose.t list = [<region>]

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
ConstraintsInvariant
2

By letting Imandra use the side-condition while doing simplification, it can then realize there is just one possible behaviour for f given the side-condition g, and collapse the two regions.

# Max_ctx_simp¶

~max_ctx_simp is a numeric value (defaults to 100) which tells Imandra how "deep" to simplify conditional statements into separate regions. A higher number will mean that Imandra will spend more time trying to "simplify" the target function, which can lead to faster or better decomposition, but a value too high might also make Imandra work too hard trying to simplify a target function that would be more easily decomposed with a less deep simplification.

In practice you'll very rarely need to tweak this flag.

# Basis¶

~basis is an optional list of functions that we want Imandra to leave opaque (i.e., disabled or uninterpreted). There are two main reasons for wanting to do this:

• Abstraction fence: Function symbols in the basis will give a logical vernacular for describing regions and invariants. This is very similar to the use of disabled function symbols in Imandra theorem proving.

A typical example: Consider a "date/time comparison" function Datetime.(<=) which is used in an IML model. If this comparison function is complex with many branches (comparing year, month, day, hour, minute, etc.), these constraints may pollute your decomposition with a huge number of regions ultimately describing "every possible way" one can have, e.g., Datetime.(x <= y) and this may obscure the meaning of the various regions. Instead, if we add Datetime.(<=) to the basis, then its definition will not be expanded and it can appear atomically in constraints and invariants. There are also ways to make use of Imandra rewrite rules and other lemmas, so that various exposed properties of the basis functions are respected (and contribute to simplification) during decomposition, culimatining in the use of interpret_basis (described below).

• Performance/region space: When the interpretation of a function is too expensive (many branches, lots of complex nonlinear arithmetic), we may want to tell imandra to avoid interpreting it

Note that putting certain functions in ~basis may actually cause a higher number of regions to be computed and much more deeply nested branches to be analyzed, thus also causing performance issues and having the exactly opposite effect than what desired, so be very careful and thoughtful about putting functions in ~basis. There are also correctness issues that can arise, see ~interpret-basis

Let's see how this flag works in practice:

In [17]:
type my_num = Real of real | Int of int | NaN

match x, y with
| Real f1, Real f2 -> Real (f1 +. f2)
| Int i1, Int i2 -> Int (i1 + i2)
| _, _ -> NaN

let is_pos x =
match x with
| Real f -> f >. 0.0
| Int i -> i > 0
| NaN -> false

let f x y =
if is_pos (add x y) then
1
else
2

Out[17]:
type my_num = Real of real | Int of int | NaN
val add : my_num -> my_num -> my_num = <fun>
val is_pos : my_num -> bool = <fun>
val f : my_num -> my_num -> Z.t = <fun>


Let's try to decompose f without anything in basis:

In [18]:
Decompose.top "f"

Out[18]:
- : Imandra_interactive.Decompose.t list =
[<region>; <region>; <region>; <region>; <region>; <region>; <region>]

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
ConstraintsInvariant
• not Is_a(Real, x)
• not Is_a(Int, x)
2
• not Is_a(Real, x)
• Is_a(Int, x)
• not Is_a(Int, y)
2
• not Is_a(Real, x)
• Is_a(Int, x)
• Is_a(Int, y)
• (Destruct(Int, 0, x) + Destruct(Int, 0, y)) <= 0
2
• not Is_a(Real, x)
• Is_a(Int, x)
• Is_a(Int, y)
• not ((Destruct(Int, 0, x) + Destruct(Int, 0, y)) <= 0)
1
• Is_a(Real, x)
• not Is_a(Real, y)
• not Is_a(Int, x)
2
• Is_a(Real, x)
• Is_a(Real, y)
• (Destruct(Real, 0, x) +. Destruct(Real, 0, y)) <=. 0
2
• Is_a(Real, x)
• Is_a(Real, y)
• not ((Destruct(Real, 0, x) +. Destruct(Real, 0, y)) <=. 0)
1

As we can see decomposition for our f explodes because of the branching in is_pos and add, we can imagine the number of regions getting much larger as we support summation between Float and Int for example.

Let's see how ~basis helps us here:

In [19]:
Decompose.top ~basis:["add";"is_pos"] "f"

Out[19]:
- : Imandra_interactive.Decompose.t list = [<region>; <region>]

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
ConstraintsInvariant
• not (is_pos (add x y))
2
• is_pos (add x y)
1

By putting add and is_pos in ~basis, we now only get the 2 "logical" regions of behaviour instead of a listing of all the possible code paths.

# Interpret basis¶

~interpret_basis is a flag which tells Imandra whether or not to take the interpretation of the functions in ~basis into account when lifting and when extracting sample values via the Mex module. It only has effect when ~basis is not empty.

Note that ~interpret_basis cannot be used with recursive functions in basis.

This flag has a strong effect on correctness when used in decompositions that have side-conditions that use functions in ~basis in branching points, as in the absence of side-conditions, setting this flag to false may cause unreachable regions to be output. Setting ~interpret_basis:false may have significant performance benefits, but could also cause a degradation in performance in certain cases; for those reasons we suggest to always set ~interpret_basis:true unless careful thought is given and the possible issues have been explored and are understood.

Let's see how this flag works in practice:

In [20]:
let gt (x : int) (y : int) = x > y;;

let f x y =
if gt x y then
if gt y x then
1 (* this is unreachable! *)
else
2
else
3

Out[20]:
val gt : int -> int -> bool = <fun>
val f : int -> int -> Z.t = <fun>


If we try to simply decompose f, we get 2 regions:

In [21]:
Decompose.top "f"

Out[21]:
- : Imandra_interactive.Decompose.t list = [<region>; <region>]

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
ConstraintsInvariant
• not (x <= y)
2
• x <= y
3

Imandra has correctly figured out that the region with invariant F=1 is not admissible, since it's never the case that x>y && y>x.

However, if we decide we need gt to be a basis function (for one of the reasions we've described earlier), Imandra doesn't have any visibility into what gt does and thus loses the ability to understand that if gt x y then not (gt y x), and we see that the unreachable region is output anyway:

In [22]:
Decompose.top ~basis:["gt"] "f"

Out[22]:
- : Imandra_interactive.Decompose.t list = [<region>; <region>; <region>]

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
ConstraintsInvariant
• not (gt x y)
3
• gt x y
• not (gt y x)
2
• gt x y
• gt y x
1

If however, we set ~interpret_basis:true, Imandra will have visibility into gt at "region feasibility checks" even though it will keep it atomic in the constraints, and thus will be able to prove that gt x y ==> not (gt y x) which is sufficient to exclude that region:

In [23]:
Decompose.top ~interpret_basis:true ~basis:["gt"] "f"

Out[23]:
- : Imandra_interactive.Decompose.t list = [<region>; <region>]

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
ConstraintsInvariant
• not (gt x y)
3
• gt x y
• not (gt y x)
2

# Aggressive Recursion¶

Sometimes, even ~interpret_basis:true won't be enough, and regions with falsifiable constraints will still be returned. This can be the case for a number of cases where it is not possible to provide an interpretation for a function, for example in the case of a recursive function that cannot be fully unrolled.

In those cases, ~aggressive_rec:true can help us by applying the full unrolling and simplification machinery used for theorem proving and verification to each region before returning it, this means that we can install theorems as rewrite rules or forward-chaining rules to aid in this process:

In [24]:
let rec f x = if x <= 0 then 23 else f (x - 1)

let g x = if f x = 23 then 1 else 2

Out[24]:
val f : int -> Z.t = <fun>
val g : int -> Z.t = <fun>

termination proof

### Termination proof

call f (x - 1) from f x
originalf x
subf (x - 1)
original ordinalOrdinal.Int (if x >= 0 then x else 0)
sub ordinalOrdinal.Int (if (x - 1) >= 0 then x - 1 else 0)
path[not (x <= 0)]
proof
detailed proof
ground_instances1
definitions0
inductions0
search_time
0.010s
details
Expand
smt_stats
 num checks 3 arith assert lower 8 arith pivots 2 rlimit count 1027 mk clause 4 datatype occurs check 2 mk bool var 20 arith assert upper 3 decisions 2 arith add rows 3 propagations 2 conflicts 2 arith fixed eqs 2 datatype accessor ax 2 arith conflicts 1 final checks 1 added eqs 6 del clause 4 arith eq adapter 2 memory 144.07 max memory 287.25 num allocs 4.87433e+10
Expand
• start[0.010s]
not (x <= 0)
&& (if x >= 0 then x else 0) >= 0
&& (if (x - 1) >= 0 then x - 1 else 0) >= 0
==> (x - 1) <= 0
|| Ordinal.( << ) (Ordinal.Int (if (x - 1) >= 0 then x - 1 else 0))
(Ordinal.Int (if x >= 0 then x else 0))
• ##### simplify
 into (not ((not (x <= 0) && (if x >= 0 then x else 0) >= 0) && (if x >= 1 then -1 + x else 0) >= 0) || x <= 1) || Ordinal.( << ) (Ordinal.Int (if x >= 1 then -1 + x else 0)) (Ordinal.Int (if x >= 0 then x else 0)) expansions [] rewrite_steps forward_chaining
• unroll
 expr (|Ordinal.<<_102| (|Ordinal.Int_93| (ite (>= x_1202 1) (+ (- 1) x_1202) 0)) (|Ordi… expansions
• ##### unsat
(let ((a!1 (not (= x_1202 (ite (>= x_1202 0) x_1202 0))))
(a!2 (+ x_1202 (* (- 1) (ite (>= x_1…

It's quite clear that the only live region of g is the one that returns 1, but if we try to decompose it we see that Imandra doesn't realize that:

In [25]:
Decompose.top "g";;

Out[25]:
- : Imandra_interactive.Decompose.t list = [<region>; <region>]

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
ConstraintsInvariant
• not (f x = 23)
2
• f x = 23
1

Let's prove that f x does indeed always return 23 and register the theorem as a rewrite rule:

In [26]:
theorem _ x = f x = 23 [@@induct functional f] [@@rw]

Out[26]:
val _anonymous_theorem_1 : int -> bool = <fun>
Goal:

f x = 23.

1 nontautological subgoal.

We shall induct according to a scheme derived from f.

Induction scheme:

(x <= 0 ==> φ x) && (not (x <= 0) && φ (x - 1) ==> φ x).

2 nontautological subgoals.

Subgoal 2:

H0. x <= 0
|---------------------------------------------------------------------------
f x = 23

But simplification reduces this to true, using the definition of f.

Subgoal 1:

H0. not (x <= 0)
H1. f (-1 + x) = 23
|---------------------------------------------------------------------------
f x = 23

But simplification reduces this to true, using the definition of f.

ⓘ  Rules:
(:def f)
(:induct f)


Proved
proof
 ground_instances 0 definitions 2 inductions 1 search_time 0.002s
Expand
• start[0.002s, "Goal"] f :var_0: = 23
• #### subproof

f x = 23
• start[0.002s, "1"] f x = 23
• induction on (functional f)
:scheme (x <= 0 ==> φ x) && (not (x <= 0) && φ (x - 1) ==> φ x)
• Split ((not (x <= 0) || f x = 23)
&& (not (not (x <= 0) && f (-1 + x) = 23) || f x = 23)
:cases [not (x <= 0) || f x = 23;
(x <= 0 || not (f (-1 + x) = 23)) || f x = 23])
• ##### subproof
(x <= 0 || not (f (-1 + x) = 23)) || f x = 23
• start[0.001s, "1"] (x <= 0 || not (f (-1 + x) = 23)) || f x = 23
• ###### simplify
 into true expansions f rewrite_steps forward_chaining
• ##### subproof
not (x <= 0) || f x = 23
• start[0.001s, "2"] not (x <= 0) || f x = 23
• ###### simplify
 into true expansions f rewrite_steps forward_chaining

That was easy. We can now decompose g using ~aggressive_rec:true and we obtain just one region, as Imandra is able to apply our rewrite rule during simplification:

In [27]:
Decompose.top "g" ~aggressive_rec:true

Out[27]:
- : Imandra_interactive.Decompose.t list = [<region>]

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
ConstraintsInvariant
1