CristalCaveGem » LustreC

   that the system is properly defined and check that the property is valid.

   expressed as a sequence of input values. *)

let idx_0 = Z3.Arithmetic.Integer.mk_numeral_i !ctx 0

let uid_0 = Z3.Z3List.nil uid_sort

let check machines node =

  let main_output = rename_machine_list node_id machine.mstep.step_outputs in

  let main_input = rename_machine_list node_id machine.mstep.step_inputs in

  let main_input_dummy =

  in

    main_input

    @ rename_next_list

        (* machine.mname.node_id *)

        (full_memory_vars machines machine)

    @ main_output

    main_input_dummy

    @ rename_current_list

        (* machine.mname.node_id *)

        (full_memory_vars machines machine)

    @ main_output_dummy

  (* TODO: push/pop? donner un nom different par instance pour les garder dans

     le buffer ? Faut-il declarer les "rel" dans la hashtbl ? *)

    decl_rel ~no_additional_vars:true (main_name node_id)

      (int_sort :: List.map (fun v -> type_to_sort v.var_type) main_memory_next)

  in

  let horn_head =

    Z3.Expr.mk_app !ctx decl_main

      (idx_0 :: (* uid_0:: *)

                List.map horn_var_to_expr main_memory_next)

      (* Initial set: One Step(m,x)  -- Stateless node  *)

      (* rule => (INIT_STATE and step(mid, next)) MAIN(next) *)

      (* Note that vars here contains main_memory_next *)

      let vars = step_vars_m_x machines machine in

      (* Re-declaring variables *)

      let _ = List.map decl_var vars in

      let horn_body =

        Z3.Boolean.mk_and !ctx

          [

            Z3.Expr.mk_app !ctx decl_init [];

            Z3.Expr.mk_app !ctx

              (get_fdecl (machine_stateless_name node))

              (idx_0 :: uid_0 :: List.map horn_var_to_expr vars);

          ]

      in

      add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)

      (* Initial set: Reset(c,m) + One Step(m,x) @. *)

      (* Re-declaring variables *)

      let vars_reset = reset_vars machines machine in

      let vars_step = step_vars_m_x machines machine in

      let vars_step_all = step_vars_c_m_x machines machine in

      let _ = List.map decl_var (vars_reset @ vars_step @ vars_step_all) in

      (* rule => (INIT_STATE and reset(mid) and step(mid, next)) MAIN(next) *)

      let horn_body =

        Z3.Boolean.mk_and !ctx

          [

            Z3.Expr.mk_app !ctx decl_init [];

            Z3.Expr.mk_app !ctx

              (get_fdecl (machine_reset_name node))

              (idx_0

               ::

               uid_0 :: List.map horn_var_to_expr (reset_vars machines machine));

            Z3.Expr.mk_app !ctx

              (get_fdecl (machine_step_name node))

              (idx_0

               ::

               uid_0

               :: List.map horn_var_to_expr (step_vars_m_x machines machine));

          ]

      in

      (* Vars contains all vars: in_out, current, mid, neXt memories *)

      let vars = step_vars_c_m_x machines machine in

      add_rule vars (Z3.Boolean.mk_implies !ctx horn_body horn_head)

  let step_name =

    if Machine_code_common.is_stateless machine then machine_stateless_name

    else machine_step_name

  (* ; Inductive def@. *)

  (* (Utils.fprintf_list ~sep:" " (fun fmt v -> fprintf fmt "%a@." pp_decl_var

     v)) fmt main_output_dummy; *)

  (* "@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN

     %a)@]@.))@.@." *)

  (* (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) (step_vars machines

     machine) *)

  let k =

    Corelang.dummy_var_decl "k" Type_predef.type_int

    (*Corelang.mktyp Location.dummy_loc Types.type_int*)

  in

  let horn_head =

    Z3.Expr.mk_app !ctx decl_main

      (Z3.Arithmetic.mk_add !ctx

         [ k_var; Z3.Arithmetic.Integer.mk_numeral_i !ctx 1 ]

       :: List.map horn_var_to_expr main_memory_next)

        Z3.Expr.mk_app !ctx decl_main

          (k_var :: List.map horn_var_to_expr main_memory_current);

        Z3.Expr.mk_app !ctx

          (get_fdecl (step_name node))

          (k_var

           :: uid_0 :: List.map horn_var_to_expr (step_vars machines machine));

  let vars =

    step_vars_c_m_x machines machine @ main_output_dummy @ main_input_dummy

  in

    add_rule ~dont_touch:[ decl_main ] (k :: vars)

      (Z3.Boolean.mk_implies !ctx horn_body horn_head)

  let prop = Z3.Boolean.mk_and !ctx (List.map horn_var_to_expr main_output) in

  let not_prop = Z3.Boolean.mk_not !ctx prop in

  add_rule

    (*~dont_touch:[decl_main;decl_err]*)

    (k :: main_memory_next)

    (Z3.Boolean.mk_implies !ctx

       (Z3.Boolean.mk_and !ctx

          [

            not_prop;

            Z3.Expr.mk_app !ctx decl_main

              (k_var :: List.map horn_var_to_expr main_memory_next);

          ])

       (Z3.Expr.mk_app !ctx decl_err []));

  (* fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>(not %a)@ (MAIN %a)@])@

     ERR))@." *)

  (*   (pp_conj (pp_horn_var machine)) main_output *)

  (*   (Utils.fprintf_list ~sep:" " (pp_horn_var machine)) main_memory_next *)

  (*   ; *)

  (*  if !Options.horn_query then fprintf fmt "(query ERR)@." *)

  (* Debug instructions *)

      (Utils.fprintf_list ~sep:"@ " (fun fmt e ->

           Format.pp_print_string fmt (Z3.Expr.to_string e)))

    let res_status = Z3.Fixedpoint.query_r !fp [ decl_err ] in

    | Z3.Solver.SATISFIABLE ->

      Zustre_cex.build_cex machine machines decl_err

    | Z3.Solver.UNSATISFIABLE -> (

      (*build_inv*)

      | None ->

        if !debug then Format.eprintf "Unsat No feedback@."

      | Some e ->

        if !debug then Format.eprintf "Unsat Result: %s@." (Z3.Expr.to_string e)

      )

    | Z3.Solver.UNKNOWN ->

      ()

  with Z3.Error msg ->

    Format.eprintf "Z3 failure: %s@." msg;

    ()