CristalCaveGem » LustreC

                Location.dummy_loc

                (Expr_const

                   (Const_real

            else if Z3.Arithmetic.is_int ze then

              mkexpr

                Location.dummy_loc

    Format.eprintf "After simplify: %a@." (pp_guard_list pp_elem) l; 

    Format.eprintf "@[<v 2>Z3 check sat: [%a]@ " (pp_guard_list pp_elem)l;

  );

  let solver = Z3.Solver.mk_simple_solver !ctx in

  try (

    let zl =

  (* Filtering out trivial cases. More semantics ones would have to be

     addressed later *)

  let check_sat e = (* temp function before we clean the original one *)

    let ok, _ = check_sat e in

    ok

  in

  let implies (e1,pn1) (e2,pn2) =

    (* Rewrite the expression expr, replacing any occurence of a variable

   by its definition.

     *)

  let rewrite = rewrite defs in

  let res =

    match expr.expr_desc with

    | Expr_appl (id, args, None) ->

       let args = rewrite args in

       List.map (fun (guards, e) ->

         ) args 

    | Expr_const _  -> [[], Expr expr]

    | Expr_ident id ->

                    fun accu (gl, minituple) ->

                    let is_compat, guard_comb = combine_guards g gl in

                    if is_compat then

                      new_gt::accu

                    else

                      accu

         gtuples

    | Expr_fby _

      | Expr_appl _

      -> Format.eprintf "Pb expr: %a@.@?" Printers.pp_expr expr; assert false

    | Expr_array _ | Expr_access _ | Expr_power _

                                                (* Arrays not handled here yet *)

   *   (Utils.fprintf_list ~sep:"@ "

   *        pp_guard_expr) res; *)

  res

and add_def defs vid expr =

  (* Format.eprintf "Add_def: %s = %a@."

   *   vid

  (* Format.eprintf "-> @[<v 0>%a@]@."

   *   (Utils.fprintf_list ~sep:"@ "

   *      (pp_guard_expr pp_elem)) vid_defs;   *)

(* Takes a list of guarded exprs (ge) and a guard

returns the same list of ge splited into the ones where the guard is true and the ones where it is false. In both lists the associated ge do not mention that guard anymore.

      (* Special cases to avoid useless computations: true, false conditions *)

      match elem.expr_desc with

      (*| Expr_ident "true"  ->   build_switch_sys pos prefix *)

        ->   build_switch_sys pos prefix

      (*| Expr_ident "false" ->   build_switch_sys neg prefix *)

        ->   build_switch_sys neg prefix

      | _ -> (* Regular case *)

         (* let _ = (

    List.iter (fun c -> Hashtbl.add const_defs c.const_id c.const_value) consts

  in

  (* Registering node equations: identifying mem definitions and

     storing others in the "defs" hashtbl.

               | Expr_pre def_m ->

                  report ~level:3 (fun fmt ->

                      Format.fprintf fmt "Preparing mem %s@." vid);

               | _ -> assert false

             ) 

           else if List.exists (fun v -> v.var_id = vid) nd.node_outputs then (

             report ~level:3 (fun fmt ->

                 Format.fprintf fmt "Output variable %s@." vid);

           )

           else

             (

               report ~level:3 (fun fmt ->

                   Format.fprintf fmt "Registering variable %s@." vid);

               accu_mems, accu_outputs

             )

        | _ -> assert false (* should have been removed by normalization *)

  if !seal_debug then Format.eprintf "Map: %i elements@ " (UpMap.cardinal map);

  UpMap.fold (fun up (common, disj) accu ->

      if !seal_debug then

          "Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@."

          Guards.pp_short common

          (fprintf_list ~sep:";@ " Guards.pp_long) disj

      let disj = clean_disj disj in

      let guard_expr = (gl_as_expr common)@disj in

let is_eq_elem elem elem' =

  match elem, elem' with

  | IsInit, IsInit -> true

  | _ -> false

let select_elem elem (gelem, _) =

        machines; 

      exit 1

    )

  in

  let m = Machine_code_common.get_machine machines node_name in

  let nd = m.mname in

  let msch = Utils.desome m.msch in

  (* Format.eprintf "graph: %a@." Causality.pp_dep_graph deps; *)

  let sliced_nd = slice_node (mems@nd.node_outputs) msch nd in

  report ~level:3 (fun fmt -> Format.fprintf fmt "Node sliced@.");

  let consts = Corelang.(List.map const_of_top (get_consts prog)) in

  report ~level:1 (fun fmt ->

      (*let pp_res = pp_res (fun fmt e -> Format.fprintf fmt "%i" e.Lustre_types.expr_tag)  in*)

       let pp_res = pp_res Printers.pp_expr in

        pp_res  sw_init;

      Format.fprintf fmt "@[<v 3>Step:@ %a@]@]@ "

        pp_res  sw_sys

    );

  let _ = match !seal_export with

    | Some "lustre" | Some "lus" ->

       Seal_export.to_lustre basename prog m sw_init sw_sys init_out update_out  

      ]

    let activate () =

      active := true;

    let is_active () = !active

    let run = seal_run

  (* Used to print boolean constants *)

let horn_tag_to_expr t =

    Z3.Boolean.mk_true !ctx

    Z3.Boolean.mk_false !ctx

  else

    (* Finding the associated sort *)

let rec horn_const_to_expr c =

  match c with

    | Const_int i    -> Z3.Arithmetic.Integer.mk_numeral_i !ctx i

    | Const_tag t    -> horn_tag_to_expr t

    | _              -> assert false

       (val_to_expr v1)

       (val_to_expr v2)

  (* | _, [v1; v2] ->      Z3.Boolean.mk_and