Merge pull request kind2-mc#1062 from daniel-larraz/analyze-slicing

Slice in IC3IA only if sys was not modified

src/ic3ia/IC3IA.ml

@@ -934,17 +934,20 @@ let main_ic3ia fwd prop in_sys param sys =
 
    SMTSolver.delete_instance solver
 
-let main fwd prop in_sys param sys =
+let main fwd slice_to_prop prop in_sys param sys =
 
   let param = Analysis.param_clone param in
 
   let sys =
-    (* Only slice if the property does not contain instantiated variables *)
-    (* The current slicing procedure works on the input system, not the transition system *)
-    match prop.Property.prop_source with
-    | Assumption _ -> sys (* An instantiated var is also involved, local sofar var *)
-    | Instantiated _ -> sys
-    | _ -> fst (InputSystem.trans_sys_of_analysis ~slice_to_prop:prop in_sys param)
+    if slice_to_prop then (
+      (* Only slice if the property does not contain instantiated variables *)
+      (* The current slicing procedure works on the input system, not the transition system *)
+      match prop.Property.prop_source with
+      | Assumption _ -> sys (* An instantiated var is also involved, local sofar var *)
+      | Instantiated _ -> sys
+      | _ -> fst (InputSystem.trans_sys_of_analysis ~slice_to_prop:prop in_sys param)
+    )
+    else sys
   in
   (*Format.printf "%a" (TransSys.pp_print_subsystems true) sys;*)
 

src/ic3ia/IC3IA.mli

@@ -30,7 +30,7 @@
 exception UnsupportedFeature of string
 
 (** Entry point *)
-val main : bool -> Property.t -> 'a InputSystem.t -> Analysis.param -> TransSys.t -> unit
+val main : bool -> bool -> Property.t -> 'a InputSystem.t -> Analysis.param -> TransSys.t -> unit
 
 (** Cleanup before exit *)
 val on_exit : TransSys.t option -> unit

src/invarManager.ml

@@ -119,7 +119,7 @@ let kill_useless_engines child_pids =
 
 let check_pending_processes run_process pending_processes sys child_pids =
   pending_processes := !pending_processes |> List.filter (function
-    | ProcessCall.IC3IA_Call (_, prop, _) -> (
+    | ProcessCall.IC3IA_Call (_, _, prop, _) -> (
       match TransSys.get_prop_status sys prop.prop_name with
       | PropUnknown | PropKTrue _ -> true
       | _ -> false

src/ivcMcs.ml

@@ -45,7 +45,7 @@ type 'a result =
 | Error of string
 
 type 'a analyze_func =
-    bool -> bool ->
+    bool -> bool -> bool ->
     Lib.kind_module list ->
     'a InputSystem.t ->
     Analysis.param ->
@@ -546,7 +546,7 @@ let make_ts_analyzer in_sys ?(stop_after_disprove=true) ?(no_copy=false) param a
   let param = Analysis.param_clone param in
   let sys = if no_copy then sys else TS.copy sys in
   let modules = Flags.enabled () in
-  sys, (fun sys -> analyze false stop_after_disprove modules in_sys param sys)
+  sys, (fun sys -> analyze false stop_after_disprove false modules in_sys param sys)
 
 let props_names props =
   List.map (fun { Property.prop_name = n } -> n) props

src/ivcMcs.mli

@@ -34,7 +34,7 @@ type 'a result =
 | Error of string
 
 type 'a analyze_func =
-    bool -> bool ->
+    bool -> bool -> bool ->
     Lib.kind_module list ->
     'a InputSystem.t ->
     Analysis.param ->

src/kind2Flow.ml

@@ -109,9 +109,9 @@ let main_of_process = function
     | `INVGENMACH | `INVGENMACHOS | `MCS | `CONTRACTCK
     | `Parser | `Certif -> ( fun _ _ _ -> () )
   )
-  | IC3IA_Call (fwd, prop, instance_name) ->
+  | IC3IA_Call (fwd, slice_to_prop, prop, instance_name) ->
     SMTLIBSolver.trace_suffix := instance_name ;
-    IC3IA.main fwd prop
+    IC3IA.main fwd slice_to_prop prop
 
 (** Cleanup function of the process *)
 let on_exit_of_process mdl =
@@ -516,7 +516,7 @@ let run_process in_sys param sys messaging_setup process =
     child_pids := (pid, kind_module) :: !child_pids
 
 
-let create_processes modules sys =
+let create_processes slice_to_prop modules sys =
   let ic3ia_module, other_modules = modules |> List.partition (
     function `IC3IA -> true | _ -> false)
   in
@@ -547,11 +547,11 @@ let create_processes modules sys =
             (fun acc p ->
               match Flags.Smt.itp_solver () with
               | `cvc5_QE | `Z3_QE when qe_itp_support_model ->
-                IC3IA_Call (false, p, fresh_ic3ia_instance_name ())
-                :: IC3IA_Call (true, p, fresh_ic3ia_instance_name ()) :: acc
+                IC3IA_Call (false, slice_to_prop, p, fresh_ic3ia_instance_name ())
+                :: IC3IA_Call (true, slice_to_prop, p, fresh_ic3ia_instance_name ()) :: acc
               | `cvc5_QE | `Z3_QE -> acc
               | _ ->
-                IC3IA_Call (false, p, fresh_ic3ia_instance_name ()) :: acc
+                IC3IA_Call (false, slice_to_prop, p, fresh_ic3ia_instance_name ()) :: acc
             )
             []
             (TSys.get_real_properties sys)
@@ -614,7 +614,7 @@ let process_ic3_modules (modules: Lib.kind_module list) : Lib.kind_module list =
     modules
 
 (** Performs an analysis. *)
-let analyze msg_setup save_results ignore_props stop_if_falsified modules in_sys param sys =
+let analyze msg_setup save_results ignore_props stop_if_falsified slice_to_prop modules in_sys param sys =
   Stat.start_timer Stat.analysis_time ;
 
   ( if TSys.has_real_properties sys |> not && not ignore_props then
@@ -642,7 +642,7 @@ let analyze msg_setup save_results ignore_props stop_if_falsified modules in_sys
       let modules = process_bmc_modules sys modules in
       let modules = process_ic3_modules modules in
 
-      let to_run, pending = create_processes modules sys in
+      let to_run, pending = create_processes slice_to_prop modules sys in
 
       (* Start all child processes. *)
       to_run |> List.iter (
@@ -946,7 +946,7 @@ let run in_sys =
 
         latest_trans_sys := Some sys ;
         (* Analyze... *)
-        analyze msg_setup true false false modules in_sys param sys ;
+        analyze msg_setup true false false true modules in_sys param sys ;
         (* ...and loop. *)
         loop ac ()
 

src/lustre/assumption.ml

@@ -229,7 +229,7 @@ let create_assumpion_trans fmt_assump sys solver vars fp prop =
 
 
 type 'a analyze_func =
-  bool -> bool -> 
+  bool -> bool -> bool ->
   Lib.kind_module list ->
   'a InputSystem.t ->
   Analysis.param ->
@@ -1027,7 +1027,7 @@ let generate_assumption ?(one_state=false) analyze in_sys param sys =
 
         Lib.set_log_level L_off ;
 
-        analyze false false modules in_sys param sys' ;
+        analyze false false false modules in_sys param sys' ;
 
         Lib.set_log_level old_log_level;
 

src/lustre/assumption.mli

@@ -73,7 +73,7 @@ val generate_assumption_vg:
   'a InputSystem.t -> TransSys.t -> 'a pair_of_filters -> Property.t -> response
 
 type 'a analyze_func =
-  bool -> bool -> 
+  bool -> bool -> bool -> 
   Lib.kind_module list ->
   'a InputSystem.t ->
   Analysis.param ->

src/postAnalysis.ml

@@ -59,7 +59,7 @@ module type PostAnalysis = sig
     Analysis.param ->
     (* A function running an analysis with some modules. *)
     (
-      bool -> bool -> Lib.kind_module list -> 'a ISys.t -> Analysis.param -> TSys.t -> unit
+      bool -> bool -> bool -> Lib.kind_module list -> 'a ISys.t -> Analysis.param -> TSys.t -> unit
     ) ->
     (* Results for the current system. *)
     Analysis.results
@@ -512,7 +512,7 @@ module RunContractGen: PostAnalysis = struct
           ) "@ "
         ) teks ;
         try
-          analyze true false
+          analyze true false false
             teks
             (* [
               `INVGEN ; `INVGENOS ;

src/postAnalysis.mli

@@ -39,7 +39,7 @@ module type PostAnalysis = sig
     Analysis.param ->
     (* A function running an analysis with some modules. *)
     (
-      bool -> bool -> Lib.kind_module list -> 'a InputSystem.t -> Analysis.param -> TransSys.t
+      bool -> bool -> bool -> Lib.kind_module list -> 'a InputSystem.t -> Analysis.param -> TransSys.t
       -> unit
     ) ->
     (* Results for the current system. *)
@@ -63,7 +63,7 @@ module RunMCS: PostAnalysis
     Analysis.param ->
     (* A function running an analysis with some modules. *)
     (
-      bool -> bool -> Lib.kind_module list -> 'a InputSystem.t -> Analysis.param -> TransSys.t
+      bool -> bool -> bool -> Lib.kind_module list -> 'a InputSystem.t -> Analysis.param -> TransSys.t
       -> unit
     ) ->
     TransSys.t
@@ -74,7 +74,7 @@ module RunMCS: PostAnalysis
 val run: 'a InputSystem.t -> Scope.t ->
     (* A function running an analysis with some modules. *)
     (
-      bool -> bool -> Lib.kind_module list -> 'a InputSystem.t -> Analysis.param -> TransSys.t
+      bool -> bool -> bool -> Lib.kind_module list -> 'a InputSystem.t -> Analysis.param -> TransSys.t
       -> unit
     ) ->
     Analysis.results -> unit

src/processCall.ml

@@ -18,8 +18,8 @@
 
 type t =
   | GenericCall of Lib.kind_module
-  | IC3IA_Call of bool * Property.t * string
+  | IC3IA_Call of bool * bool * Property.t * string
 
 let get_kind_module = function
   | GenericCall m -> m
-  | IC3IA_Call _ -> `IC3IA
+  | IC3IA_Call _ -> `IC3IA

src/processCall.mli

@@ -18,6 +18,6 @@
 
 type t =
   | GenericCall of Lib.kind_module
-  | IC3IA_Call of bool * Property.t * string
+  | IC3IA_Call of bool * bool * Property.t * string
 
-val get_kind_module : t -> Lib.kind_module
+val get_kind_module : t -> Lib.kind_module

src/realizability.ml

@@ -23,7 +23,7 @@ module ScMap = Scope.Map
 
 
 type 'a analyze_func =
-  Lib.kind_module list -> 'a InputSystem.t -> Analysis.param -> TransSys.t -> unit
+  bool -> Lib.kind_module list -> 'a InputSystem.t -> Analysis.param -> TransSys.t -> unit
 
 type unrealizable_result =
   | BaseCase of Term.t
@@ -633,20 +633,20 @@ let compute_dependent_conflict_and_deadlocking_trace
 let compute_deadlocking_trace_and_conflict
   analyze in_sys param sys controllable_vars_at_0 controllable_vars_at_1 u_result =
 
-  let sys =
+  let sys, slice_to_prop =
     let scope = (Analysis.info_of_param param).top in
     match InputSystem.get_lustre_node in_sys scope with
-    | None -> sys
+    | None -> sys, false
     | Some { LustreNode.is_function } ->
       if is_function && Flags.Contracts.enforce_func_congruence () then (
         (* Recompute transition system adding functional constraints *)
         let sys, _ =
           InputSystem.trans_sys_of_analysis
             ~add_functional_constraints:true in_sys param
         in
-        sys
+        sys, false
       )
-      else sys
+      else sys, true
   in
 
   let vr, cex, is_base, offset, contr_vars =
@@ -675,7 +675,7 @@ let compute_deadlocking_trace_and_conflict
       let old_log_level = Lib.get_log_level () in
       Lib.set_log_level L_off ;
 
-      analyze modules in_sys param sys ;
+      analyze slice_to_prop modules in_sys param sys ;
 
       Lib.set_log_level old_log_level;
 

src/realizability.mli

@@ -22,7 +22,7 @@
 *)
 
 type 'a analyze_func =
-  Lib.kind_module list -> 'a InputSystem.t -> Analysis.param -> TransSys.t -> unit
+  bool -> Lib.kind_module list -> 'a InputSystem.t -> Analysis.param -> TransSys.t -> unit
 
 type unrealizable_result