Enable assumption generation

src/flags.ml

@@ -1243,7 +1243,7 @@ module Contracts = struct
 
   let assumption_gen_default = false
   let assumption_gen = ref assumption_gen_default
-  (*let _ = add_spec
+  let _ = add_spec
     "--assumption_gen"
     (bool_arg assumption_gen)
     (fun fmt ->
@@ -1254,7 +1254,7 @@ module Contracts = struct
         Default: %a\
       @]"
       fmt_bool assumption_gen_default
-    )*)
+    )
   let assumption_gen () = !assumption_gen
 
   (*let assump_include_outputs_default = true
@@ -1275,7 +1275,7 @@ module Contracts = struct
 
   let two_state_assumption_default = false
   let two_state_assumption = ref two_state_assumption_default
-  (*let _ = add_spec
+  let _ = add_spec
     "--two_state_assumption"
     (bool_arg two_state_assumption)
     (fun fmt ->
@@ -1286,12 +1286,12 @@ module Contracts = struct
         Default: %a\
       @]"
       fmt_bool two_state_assumption_default
-    )*)
+    )
   let two_state_assumption () = !two_state_assumption
 
   let assumption_gen_iter_default = 1
   let assumption_gen_iter = ref assumption_gen_iter_default
-  (*let _ = add_spec
+  let _ = add_spec
     "--assumption_gen_iter"
     (Arg.Int (fun n -> assumption_gen_iter := n))
     (fun fmt ->
@@ -1302,7 +1302,7 @@ module Contracts = struct
         Default: %d\
       @]"
       assumption_gen_iter_default
-    )*)
+    )
   let assumption_gen_iter () = !assumption_gen_iter
 
 

src/lustre/assumption.ml

@@ -908,10 +908,22 @@ let satisfy_input_requirements in_sys param top =
 
 let generate_assumption ?(one_state=false) analyze in_sys param sys =
 
-  match TSys.get_split_properties sys with
-  | _, [], [] -> Success { init = Term.t_true; trans = Term.t_true }
-  | _, [], _ -> Unknown
-  | _, invalid, _ -> (
+  let valid, invalid, unknown = TSys.get_split_properties sys in
+  let invalid_inv =
+    List.filter (fun p -> p.Property.prop_kind = Invariant) invalid
+  in
+  match invalid_inv, unknown with
+  | [], [] -> Success { init = Term.t_true; trans = Term.t_true }
+  | [], _ -> Unknown
+  | invalid, _ -> (
+
+    let sys =
+      let valid =
+        List.filter (fun p -> p.Property.prop_kind = Invariant) valid
+      in
+      let props = valid @ invalid in
+      TSys.set_subsystem_properties sys (TSys.scope_of_trans_sys sys) props
+    in
 
     let get_min_k props =
       let k_list =

src/postAnalysis.ml

@@ -212,18 +212,34 @@ module RunAssumptionGen: PostAnalysis = struct
     last_result results top
     |> Res.chain (fun { Analysis.sys } ->
       (* Check all properties are valid. *)
-      match TSys.get_split_properties sys with
-      | [], [], [] -> error (
-        fun fmt ->
-          Format.fprintf fmt
-            "No properties, assumption generation disabled."
+      let valid, invalid, unknown = TSys.get_split_properties sys in
+      let valid_rch =
+        valid |> List.filter (fun p ->
+          match p.Property.prop_kind with Reachable _ -> true | _ -> false)
+      in
+      let invalid_inv =
+        List.filter (fun p -> p.Property.prop_kind = Invariant) invalid
+      in
+      match unknown with
+      | [] -> (
+        match invalid_inv, valid_rch with
+        | [], _ -> error (
+          fun fmt ->
+            Format.fprintf fmt
+              "No invalid properties, assumption generation disabled."
+        )
+        | _, [] -> Ok sys
+        | _ -> error (
+          fun fmt ->
+            Format.fprintf fmt
+              "Unreachable property detected, assumption generation disabled."
+        )
       )
-      | _, [], _ -> error (
+      | _ -> error (
         fun fmt ->
           Format.fprintf fmt
-            "No invalid properties, assumption generation disabled."
+            "Unknown property detected, assumption generation disabled."
       )
-      | _ -> Ok sys
     )
     |> Res.chain (fun sys ->
       try (