Rule consistency or duplications

Here are the background types and functions we can use to represent the obligations and artifacts in these examples.

In [1]:
type obligations = {
  sing_a_song: bool;
  do_a_dance: bool;
}

type employee = {
  name : string;
  arrival_time : int;
  obligations : obligations;
}

type state = {
  emp: employee;
  meeting_time: int;
}

let on_time st =
  st.emp.arrival_time <= st.meeting_time

let is_late st =
  not (on_time st)
Out[1]:
type obligations = { sing_a_song : bool; do_a_dance : bool; }
type employee = {
  name : string;
  arrival_time : Z.t;
  obligations : obligations;
}
type state = { emp : employee; meeting_time : Z.t; }
val on_time : state -> bool = <fun>
val is_late : state -> bool = <fun>

Now for a particular rules we can represent this modules, which have a common structure.

In [2]:
(* Employee E must sing a song
   if E is late for a meeting for n minutes
   and n is greater than 3*)

module Rule0 = struct

 let c1 st =
  is_late st

 let c2 st =
  st.emp.arrival_time - st.meeting_time > 3

 let cs st =
  c1 st && c2 st

 let s st =
  st.emp.obligations.sing_a_song

 let rule st =
  s st <== cs st

end
Out[2]:
module Rule0 :
  sig
    val c1 : state -> bool
    val c2 : state -> bool
    val cs : state -> bool
    val s : state -> bool
    val rule : state -> bool
  end
In [3]:
(*
  Employee E must sing a song
  if E is late for a meeting for n minutes
  and n is greater than 1
*)

module Rule1 = struct

 let c1 st =
  is_late st

 let c2 st =
  st.emp.arrival_time - st.meeting_time > 1

 let cs st =
  c1 st && c2 st

 let s st =
  st.emp.obligations.sing_a_song

 let rule st =
  s st <== cs st

end
Out[3]:
module Rule1 :
  sig
    val c1 : state -> bool
    val c2 : state -> bool
    val cs : state -> bool
    val s : state -> bool
    val rule : state -> bool
  end

We can ask questions about these rules such as if the statements overlap using Imandra's instance mechanism:

In [4]:
(* Do Rule0's and Rule1's conditions overlap? *)

instance (fun st -> (Rule0.c1 st) && (Rule1.c1 st))
Out[4]:
- : state -> bool = <fun>
module CX : sig val st : state end
Instance (after 0 steps, 0.019s):
let st : state =
  {emp =
   {name = "!0!"; arrival_time = 0;
    obligations = {sing_a_song = false; do_a_dance = false}};
   meeting_time = (-1)}
Instance
proof attempt
ground_instances:0
definitions:0
inductions:0
search_time:
0.019s
details:
Expand
smt_stats:
num checks:1
arith assert lower:1
arith tableau max rows:1
arith tableau max columns:4
arith pivots:1
rlimit count:331
mk clause:16
datatype occurs check:1
mk bool var:22
decisions:2
seq num reductions:1
propagations:2
datatype accessor ax:4
arith num rows:1
datatype constructor ax:4
num allocs:6850118
final checks:1
added eqs:23
del clause:8
time:0.009000
memory:16.290000
max memory:16.690000
Expand
  • start[0.019s]
      let (_x_0 : bool)
          = not (( :var_0: ).emp.arrival_time <= ( :var_0: ).meeting_time)
      in _x_0 && _x_0
  • simplify

    into:
    not (( :var_0: ).emp.arrival_time <= ( :var_0: ).meeting_time)
    expansions:
    []
    rewrite_steps:
      forward_chaining:
      • Sat (Some let st : state = {emp = {name = "!0!"; arrival_time = (Z.of_nativeint (0n)); obligations = {sing_a_song = false; do_a_dance = false}}; meeting_time = (Z.of_nativeint (-1n))} )
      In [5]:
      (* Employee E must sing a song
         if E is late for a meeting for n minutes
         and n is less than 3*)
      
      module Rule2 = struct
      
       let c1 st =
        is_late st
      
       let c2 st =
        st.emp.arrival_time - st.meeting_time < 3
      
       let cs st =
        c1 st && c2 st
      
       let s st =
        st.emp.obligations.sing_a_song
      
       let rule st =
        s st <== cs st
      
      end
      
      Out[5]:
      module Rule2 :
        sig
          val c1 : state -> bool
          val c2 : state -> bool
          val cs : state -> bool
          val s : state -> bool
          val rule : state -> bool
        end
      
      In [6]:
      (* Employee E must do a dance
         if E is late for a meeting for n minutes
         and n is greater than 3*)
      
      module Rule3 = struct
      
       let c1 st =
        is_late st
      
       let c2 st =
        st.emp.arrival_time - st.meeting_time > 3
      
       let cs st =
        c1 st && c2 st
      
       let s st =
        st.emp.obligations.do_a_dance
      
       let rule st =
        s st <== cs st
      
      end
      
      Out[6]:
      module Rule3 :
        sig
          val c1 : state -> bool
          val c2 : state -> bool
          val cs : state -> bool
          val s : state -> bool
          val rule : state -> bool
        end
      
      In [7]:
      (* Employee E must NOT sing a song
         if E is late for a meeting for n minutes
         and n is greater than 1 *)
      
      module Rule3 = struct
      
       let c1 st =
        is_late st
      
       let c2 st =
        st.emp.arrival_time - st.meeting_time > 1
      
       let cs st =
        c1 st && c2 st
      
       let s st =
        not (st.emp.obligations.sing_a_song)
      
       let rule st =
        s st <== cs st
      
      end
      
      Out[7]:
      module Rule3 :
        sig
          val c1 : state -> bool
          val c2 : state -> bool
          val cs : state -> bool
          val s : state -> bool
          val rule : state -> bool
        end
      
      In [8]:
      (* Employee E must not sing a song
         if E is late for a meeting for n minutes
         and n is greater than 3 *)
      
      module Rule4 = struct
      
       let c1 st =
        is_late st
      
       let c2 st =
        st.emp.arrival_time - st.meeting_time > 3
      
       let cs st =
        c1 st && c2 st
      
       let s st =
        not (st.emp.obligations.sing_a_song)
      
       let rule st =
        s st <== cs st
      
      end
      
      Out[8]:
      module Rule4 :
        sig
          val c1 : state -> bool
          val c2 : state -> bool
          val cs : state -> bool
          val s : state -> bool
          val rule : state -> bool
        end
      
      In [9]:
      (* Employee E must do a dance
         if E is late for a meeting for n minutes
         and n is greater than 3 *)
      
      module Rule5 = struct
      
       let c1 st =
        is_late st
      
       let c2 st =
        st.emp.arrival_time - st.meeting_time > 1
      
       let cs st =
        c1 st && c2 st
      
       let s st =
        st.emp.obligations.do_a_dance
      
       let rule st =
        s st <== cs st
      
      end
      
      Out[9]:
      module Rule5 :
        sig
          val c1 : state -> bool
          val c2 : state -> bool
          val cs : state -> bool
          val s : state -> bool
          val rule : state -> bool
        end
      
      In [10]:
      (* Employee E must sing a song
         if E is late for a meeting for n minutes
         and n is less than 3 *)
      
      module Rule6 = struct
      
       let c1 st =
        is_late st
      
       let c2 st =
        st.emp.arrival_time - st.meeting_time < 3
      
       let cs st =
        c1 st && c2 st
      
       let s st =
        st.emp.obligations.sing_a_song
      
       let rule st =
        s st <== cs st
      
      end
      
      Out[10]:
      module Rule6 :
        sig
          val c1 : state -> bool
          val c2 : state -> bool
          val cs : state -> bool
          val s : state -> bool
          val rule : state -> bool
        end
      
      In [11]:
      (* Employee E must not sing a song
         if E is late for a meeting for n minutes
         and n is greater than 1 *)
      
      module Rule7 = struct
      
       let c1 st =
        is_late st
      
       let c2 st =
        st.emp.arrival_time - st.meeting_time > 1
      
       let cs st =
        c1 st && c2 st
      
       let s st =
        not (st.emp.obligations.sing_a_song)
      
       let rule st =
        s st <== cs st
      
      end
      
      Out[11]:
      module Rule7 :
        sig
          val c1 : state -> bool
          val c2 : state -> bool
          val cs : state -> bool
          val s : state -> bool
          val rule : state -> bool
        end
      
      In [12]:
      (* Employee E must not sing a song
         if E is late for a meeting for n minutes
         and n is less than 3 *)
      
      module Rule8 = struct
      
       let c1 st =
        is_late st
      
       let c2 st =
        st.emp.arrival_time - st.meeting_time < 3
      
       let cs st =
        c1 st && c2 st
      
       let s st =
        not (st.emp.obligations.sing_a_song)
      
       let rule st =
        s st <== cs st
      
      end
      
      Out[12]:
      module Rule8 :
        sig
          val c1 : state -> bool
          val c2 : state -> bool
          val cs : state -> bool
          val s : state -> bool
          val rule : state -> bool
        end
      

      Let's pose some queries about the relationships of these rules

      In [13]:
      (* Do the conditions of rules 0 and 1 overlap? *)
      
      instance (fun st -> Rule0.cs st && Rule1.cs st)
      
      Out[13]:
      - : state -> bool = <fun>
      module CX : sig val st : state end
      
      Instance (after 0 steps, 0.018s):
      let st : state =
        {emp =
         {name = "!0!"; arrival_time = 0;
          obligations = {sing_a_song = false; do_a_dance = false}};
         meeting_time = (-4)}
      
      Instance
      proof attempt
      ground_instances:0
      definitions:0
      inductions:0
      search_time:
      0.018s
      details:
      Expand
      smt_stats:
      num checks:1
      arith assert lower:3
      arith tableau max rows:1
      arith tableau max columns:4
      arith pivots:1
      rlimit count:577
      mk clause:16
      datatype occurs check:1
      mk bool var:24
      decisions:2
      seq num reductions:1
      propagations:2
      datatype accessor ax:4
      arith num rows:1
      datatype constructor ax:4
      num allocs:14642280
      final checks:1
      added eqs:23
      del clause:8
      time:0.008000
      memory:17.880000
      max memory:18.260000
      Expand
      • start[0.018s]
          let (_x_0 : int) = ( :var_0: ).emp.arrival_time in
          let (_x_1 : int) = ( :var_0: ).meeting_time in
          let (_x_2 : bool) = not (_x_0 <= _x_1) in
          let (_x_3 : int) = _x_0 - _x_1 in
          _x_2 && (_x_3 > 3) && (_x_2 && (_x_3 > 1))
      • simplify

        into:
        let (_x_0 : int) = ( :var_0: ).emp.arrival_time in
        let (_x_1 : int) = ( :var_0: ).meeting_time in
        let (_x_2 : int) = _x_0 + (-1) * _x_1 in
        not (_x_0 <= _x_1) && not (_x_2 <= 3) && not (_x_2 <= 1)
        expansions:
        []
        rewrite_steps:
          forward_chaining:
          • Sat (Some let st : state = {emp = {name = "!0!"; arrival_time = (Z.of_nativeint (0n)); obligations = {sing_a_song = false; do_a_dance = false}}; meeting_time = (Z.of_nativeint (-4n))} )
          In [14]:
          (* Do the statements of rules 0 and 1 overlap? *)
          
          instance (fun st -> Rule0.s st && Rule1.s st)
          
          Out[14]:
          - : state -> bool = <fun>
          module CX : sig val st : state end
          
          Instance (after 0 steps, 0.017s):
          let st : state =
            {emp =
             {name = ""; arrival_time = 0;
              obligations = {sing_a_song = true; do_a_dance = false}};
             meeting_time = 0}
          
          Instance
          proof attempt
          ground_instances:0
          definitions:0
          inductions:0
          search_time:
          0.017s
          details:
          Expand
          smt_stats:
          num checks:1
          rlimit count:119
          mk bool var:1
          eliminated applications:3
          num allocs:22838437
          final checks:1
          time:0.008000
          memory:18.020000
          max memory:18.270000
          Expand
          • start[0.017s]
              let (_x_0 : bool) = ( :var_0: ).emp.obligations.sing_a_song in _x_0 && _x_0
          • simplify

            into:
            ( :var_0: ).emp.obligations.sing_a_song
            expansions:
            []
            rewrite_steps:
              forward_chaining:
              • Sat (Some let st : state = {emp = {name = ""; arrival_time = (Z.of_nativeint (0n)); obligations = {sing_a_song = true; do_a_dance = false}}; meeting_time = (Z.of_nativeint (0n))} )
              In [15]:
              (* We can encode these as checks on rules.
                 We prefix with `v` if `verify` should be used, else with `i` if `instance` should be used. *)
              
              let v_check_1 r1_cs r1_s r2_cs r2_s st =
                r1_s st = r2_s st && r1_cs st = r2_cs st
              
              Out[15]:
              val v_check_1 :
                ('a -> 'b) -> ('a -> 'c) -> ('a -> 'b) -> ('a -> 'c) -> 'a -> bool = <fun>
              
              In [16]:
              (* For example, we can do check1 for Rule0 and Rule0 *)
              
              verify (fun st -> v_check_1 Rule0.cs Rule0.s Rule0.cs Rule0.s st)
              
              Out[16]:
              - : state -> bool = <fun>
              
              Proved
              proof
              ground_instances:0
              definitions:0
              inductions:0
              search_time:
              0.016s
              details:
              Expand
              smt_stats:
              rlimit count:7
              num allocs:32625989
              time:0.007000
              memory:18.420000
              max memory:18.420000
              Expand
              • start[0.016s] true
              • Unsat
              In [17]:
              (* And similarly for Rule0 and Rule1 *)
              
              verify (fun st -> v_check_1 Rule0.cs Rule0.s Rule1.cs Rule1.s st)
              
              Out[17]:
              - : state -> bool = <fun>
              module CX : sig val st : state end
              
              Counterexample (after 0 steps, 0.019s):
              let st : state =
                {emp =
                 {name = "!0!"; arrival_time = 0;
                  obligations = {sing_a_song = false; do_a_dance = false}};
                 meeting_time = (-2)}
              
              Refuted
              proof attempt
              ground_instances:0
              definitions:0
              inductions:0
              search_time:
              0.019s
              details:
              Expand
              smt_stats:
              num checks:1
              arith assert lower:2
              arith tableau max rows:1
              arith tableau max columns:4
              arith pivots:1
              rlimit count:733
              mk clause:26
              datatype occurs check:1
              mk bool var:26
              arith assert upper:1
              decisions:3
              seq num reductions:1
              propagations:10
              conflicts:1
              datatype accessor ax:4
              arith num rows:1
              datatype constructor ax:4
              num allocs:45617351
              final checks:1
              added eqs:23
              del clause:8
              time:0.010000
              memory:18.660000
              max memory:19.020000
              Expand
              • start[0.019s]
                  let (_x_0 : int) = ( :var_0: ).emp.arrival_time in
                  let (_x_1 : int) = ( :var_0: ).meeting_time in
                  let (_x_2 : bool) = not (_x_0 <= _x_1) in
                  let (_x_3 : int) = _x_0 - _x_1 in
                  (_x_2 && (_x_3 > 3)) = (_x_2 && (_x_3 > 1))
              • simplify

                into:
                let (_x_0 : int) = ( :var_0: ).emp.arrival_time in
                let (_x_1 : int) = ( :var_0: ).meeting_time in
                let (_x_2 : bool) = not (_x_0 <= _x_1) in
                let (_x_3 : int) = _x_0 + (-1) * _x_1 in
                (_x_2 && not (_x_3 <= 3)) = (_x_2 && not (_x_3 <= 1))
                expansions:
                []
                rewrite_steps:
                  forward_chaining:
                  • Sat (Some let st : state = {emp = {name = "!0!"; arrival_time = (Z.of_nativeint (0n)); obligations = {sing_a_song = false; do_a_dance = false}}; meeting_time = (Z.of_nativeint (-2n))} )
                  In [18]:
                  (* Now let's consider check2: statements the same but conditions different (overlapping) *)
                  (* We do this with two checks, one universal and one existential: *)
                  
                  let v_check2 r1_cs r1_s r2_cs r2_s st =
                   r1_s st = r2_s st
                  
                  let i_check2 r1_cs r1_s r2_cs r2_s st =
                   r1_cs st && r2_cs st
                  
                  Out[18]:
                  val v_check2 : 'a -> ('b -> 'c) -> 'd -> ('b -> 'c) -> 'b -> bool = <fun>
                  val i_check2 : ('a -> bool) -> 'b -> ('a -> bool) -> 'c -> 'a -> bool = <fun>
                  
                  In [19]:
                  (* Let's check condition 2 for Rule0 and Rule1 -- we see it holds! *)
                  
                  verify (fun st -> v_check2 Rule0.cs Rule0.s Rule1.cs Rule2.s st)
                  instance (fun st -> i_check2 Rule0.cs Rule0.s Rule1.cs Rule2.s st)
                  
                  Out[19]:
                  - : state -> bool = <fun>
                  - : state -> bool = <fun>
                  module CX : sig val st : state end
                  
                  Proved
                  proof
                  ground_instances:0
                  definitions:0
                  inductions:0
                  search_time:
                  0.016s
                  details:
                  Expand
                  smt_stats:
                  rlimit count:32
                  num allocs:59668086
                  time:0.008000
                  memory:19.160000
                  max memory:19.160000
                  Expand
                  • start[0.016s] true
                  • simplify

                    into:
                    true
                    expansions:
                    []
                    rewrite_steps:
                      forward_chaining:
                      • Unsat
                      Instance (after 0 steps, 0.018s):
                      let st : state =
                        {emp =
                         {name = "!0!"; arrival_time = 0;
                          obligations = {sing_a_song = false; do_a_dance = false}};
                         meeting_time = (-4)}
                      
                      Instance
                      proof attempt
                      ground_instances:0
                      definitions:0
                      inductions:0
                      search_time:
                      0.018s
                      details:
                      Expand
                      smt_stats:
                      num checks:1
                      arith assert lower:3
                      arith tableau max rows:1
                      arith tableau max columns:4
                      arith pivots:1
                      rlimit count:583
                      mk clause:16
                      datatype occurs check:1
                      mk bool var:24
                      decisions:2
                      seq num reductions:1
                      propagations:2
                      datatype accessor ax:4
                      arith num rows:1
                      datatype constructor ax:4
                      num allocs:77404793
                      final checks:1
                      added eqs:23
                      del clause:8
                      time:0.009000
                      memory:19.360000
                      max memory:19.760000
                      Expand
                      • start[0.018s]
                          let (_x_0 : int) = ( :var_0: ).emp.arrival_time in
                          let (_x_1 : int) = ( :var_0: ).meeting_time in
                          let (_x_2 : bool) = not (_x_0 <= _x_1) in
                          let (_x_3 : int) = _x_0 - _x_1 in
                          _x_2 && (_x_3 > 3) && (_x_2 && (_x_3 > 1))
                      • simplify

                        into:
                        let (_x_0 : int) = ( :var_0: ).emp.arrival_time in
                        let (_x_1 : int) = ( :var_0: ).meeting_time in
                        let (_x_2 : int) = _x_0 + (-1) * _x_1 in
                        not (_x_0 <= _x_1) && not (_x_2 <= 3) && not (_x_2 <= 1)
                        expansions:
                        []
                        rewrite_steps:
                          forward_chaining:
                          • Sat (Some let st : state = {emp = {name = "!0!"; arrival_time = (Z.of_nativeint (0n)); obligations = {sing_a_song = false; do_a_dance = false}}; meeting_time = (Z.of_nativeint (-4n))} )
                          In [20]:
                          (* Let's check condition 2 for Rule0 and Rule2 -- we see it does not hold! *)
                          
                          verify (fun st -> v_check2 Rule0.cs Rule0.s Rule2.cs Rule2.s st)
                          instance (fun st -> i_check2 Rule0.cs Rule0.s Rule2.cs Rule2.s st)
                          
                          Out[20]:
                          - : state -> bool = <fun>
                          - : state -> bool = <fun>
                          
                          Proved
                          proof
                          ground_instances:0
                          definitions:0
                          inductions:0
                          search_time:
                          0.016s
                          details:
                          Expand
                          smt_stats:
                          rlimit count:32
                          num allocs:94505637
                          time:0.007000
                          memory:19.560000
                          max memory:19.760000
                          Expand
                          • start[0.016s] true
                          • simplify

                            into:
                            true
                            expansions:
                            []
                            rewrite_steps:
                              forward_chaining:
                              • Unsat
                              Unsatisfiable
                              proof
                              ground_instances:0
                              definitions:0
                              inductions:0
                              search_time:
                              0.018s
                              details:
                              Expand
                              smt_stats:
                              num checks:1
                              arith assert lower:2
                              arith tableau max rows:1
                              arith tableau max columns:4
                              rlimit count:508
                              mk clause:16
                              mk bool var:24
                              arith assert upper:1
                              seq num reductions:1
                              conflicts:1
                              datatype accessor ax:4
                              arith conflicts:1
                              arith num rows:1
                              datatype constructor ax:4
                              num allocs:116639780
                              added eqs:15
                              time:0.009000
                              memory:19.740000
                              max memory:20.160000
                              Expand
                              • start[0.018s]
                                  let (_x_0 : int) = ( :var_0: ).emp.arrival_time in
                                  let (_x_1 : int) = ( :var_0: ).meeting_time in
                                  let (_x_2 : bool) = not (_x_0 <= _x_1) in
                                  let (_x_3 : int) = _x_0 - _x_1 in
                                  _x_2 && (_x_3 > 3) && (_x_2 && (_x_3 < 3))
                              • simplify

                                into:
                                let (_x_0 : int) = ( :var_0: ).emp.arrival_time in
                                let (_x_1 : int) = ( :var_0: ).meeting_time in
                                let (_x_2 : int) = _x_0 + (-1) * _x_1 in
                                not (_x_0 <= _x_1) && not (_x_2 <= 3) && not (3 <= _x_2)
                                expansions:
                                []
                                rewrite_steps:
                                  forward_chaining:
                                  • Unsat
                                  In [21]:
                                  (* Now let's do check 7: contrary statements with same conditions *)
                                  
                                  let v_check7 r1_cs r1_s r2_cs r2_s st =
                                   (r1_s st <==> not(r2_s st)) && (r1_cs st = r2_cs st)
                                  
                                  Out[21]:
                                  val v_check7 :
                                    ('a -> 'b) -> ('a -> bool) -> ('a -> 'b) -> ('a -> bool) -> 'a -> bool =
                                    <fun>
                                  
                                  In [22]:
                                  (* We'll check this for Rule0 and Rule 4 *)
                                  
                                  verify (fun st -> v_check7 Rule0.cs Rule0.s Rule4.cs Rule4.s st)
                                  
                                  Out[22]:
                                  - : state -> bool = <fun>
                                  
                                  Proved
                                  proof
                                  ground_instances:0
                                  definitions:0
                                  inductions:0
                                  search_time:
                                  0.017s
                                  details:
                                  Expand
                                  smt_stats:
                                  rlimit count:126
                                  num allocs:138364849
                                  time:0.008000
                                  memory:20.120000
                                  max memory:20.160000
                                  Expand
                                  • start[0.017s] true
                                  • simplify

                                    into:
                                    true
                                    expansions:
                                    []
                                    rewrite_steps:
                                      forward_chaining:
                                      • Unsat
                                      In [23]:
                                      (* Now let's check it for Rule0 and Rule5 -- we see it's not true! *)
                                      
                                      verify (fun st -> v_check7 Rule0.cs Rule0.s Rule5.cs Rule5.s st)
                                      
                                      Out[23]:
                                      - : state -> bool = <fun>
                                      module CX : sig val st : state end
                                      
                                      Counterexample (after 0 steps, 0.020s):
                                      let st : state =
                                        {emp =
                                         {name = "!0!"; arrival_time = 0;
                                          obligations = {sing_a_song = false; do_a_dance = false}};
                                         meeting_time = 38}
                                      
                                      Refuted
                                      proof attempt
                                      ground_instances:0
                                      definitions:0
                                      inductions:0
                                      search_time:
                                      0.020s
                                      details:
                                      Expand
                                      smt_stats:
                                      num checks:1
                                      arith tableau max rows:1
                                      arith tableau max columns:4
                                      rlimit count:989
                                      mk clause:33
                                      datatype occurs check:1
                                      mk bool var:28
                                      decisions:3
                                      seq num reductions:1
                                      propagations:8
                                      datatype accessor ax:4
                                      arith num rows:1
                                      datatype constructor ax:4
                                      num allocs:164455119
                                      final checks:1
                                      added eqs:23
                                      del clause:8
                                      time:0.010000
                                      memory:20.350000
                                      max memory:20.710000
                                      Expand
                                      • start[0.020s]
                                          let (_x_0 : employee) = ( :var_0: ).emp in
                                          let (_x_1 : obligations) = _x_0.obligations in
                                          let (_x_2 : int) = _x_0.arrival_time in
                                          let (_x_3 : int) = ( :var_0: ).meeting_time in
                                          let (_x_4 : bool) = not (_x_2 <= _x_3) in
                                          let (_x_5 : int) = _x_2 - _x_3 in
                                          (_x_1.sing_a_song = not _x_1.do_a_dance)
                                          && ((_x_4 && (_x_5 > 3)) = (_x_4 && (_x_5 > 1)))
                                      • simplify

                                        into:
                                        let (_x_0 : employee) = ( :var_0: ).emp in
                                        let (_x_1 : obligations) = _x_0.obligations in
                                        let (_x_2 : int) = _x_0.arrival_time in
                                        let (_x_3 : int) = ( :var_0: ).meeting_time in
                                        let (_x_4 : bool) = not (_x_2 <= _x_3) in
                                        let (_x_5 : int) = _x_2 + (-1) * _x_3 in
                                        (_x_1.sing_a_song = not _x_1.do_a_dance)
                                        && ((_x_4 && not (_x_5 <= 3)) = (_x_4 && not (_x_5 <= 1)))
                                        expansions:
                                        []
                                        rewrite_steps:
                                          forward_chaining:
                                          • Sat (Some let st : state = {emp = {name = "!0!"; arrival_time = (Z.of_nativeint (0n)); obligations = {sing_a_song = false; do_a_dance = false}}; meeting_time = (Z.of_nativeint (38n))} )

                                          Let's look at a region decomp of a particular rule to get examples of its distinct behaviours.

                                          In [24]:
                                          let rule5 = Rule5.rule;;
                                          
                                          Out[24]:
                                          val rule5 : state -> bool = <fun>
                                          
                                          In [25]:
                                          Modular_decomp.top "rule5";;
                                          
                                          Out[25]:
                                          - : 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 (rule5 st
                                          Reg_idConstraintsInvariant
                                          2
                                          • st.emp.arrival_time <= st.meeting_time
                                          true
                                          1
                                          • not (st.emp.arrival_time <= st.meeting_time)
                                          • not (st.emp.arrival_time - st.meeting_time > 1)
                                          true
                                          0
                                          • not (st.emp.arrival_time <= st.meeting_time)
                                          • st.emp.arrival_time - st.meeting_time > 1
                                          st.emp.obligations.do_a_dance