CristalCaveGem » LustreC

(* Switched system extraction: expression are memoized *)

(*let expr_mem = Hashtbl.create 13*)

  | Expr e -> Format.fprintf fmt "%a" Printers.pp_expr e 

  | Expr e, Expr e' -> e = e' (*

     Corelang.is_eq_expr e e' *)

(* Set of hash to support memoization *)

let expr_hash: (expr * Utils.tag) list ref = ref []

let ze_hash: (Z3.Expr.expr, Utils.tag) Hashtbl.t = Hashtbl.create 13

let e_hash: (Utils.tag, Z3.Expr.expr) Hashtbl.t = Hashtbl.create 13

let pp_hash pp_key pp_v fmt h = Hashtbl.iter (fun key v -> Format.fprintf fmt "%a -> %a@ " pp_key key pp_v v) h

let pp_e_map fmt = List.iter (fun (e,t) -> Format.fprintf fmt "%i -> %a@ " t Printers.pp_expr e) !expr_hash

let pp_ze_hash fmt = pp_hash

                      (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))

                      Format.pp_print_int

                      fmt

                      ze_hash

let pp_e_hash fmt = pp_hash

                      Format.pp_print_int

                      (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))

                      fmt

                      e_hash                              

let mem_expr e =

  (* Format.eprintf "Searching for %a in map: @[<v 0>%t@]"

   *   Printers.pp_expr e

   *   pp_e_map; *)

  let res = List.exists (fun (e',_) -> Corelang.is_eq_expr e e') !expr_hash in

  (* Format.eprintf "found?%b@." res; *)

  res

let mem_zexpr ze =

  Hashtbl.mem ze_hash ze

let get_zexpr e =

  let eref, uid = List.find (fun (e',_) -> Corelang.is_eq_expr e e') !expr_hash in

  (* Format.eprintf "found expr=%a id=%i@." Printers.pp_expr eref eref.expr_tag; *)

  Hashtbl.find e_hash uid

let get_expr ze =

  let uid = Hashtbl.find ze_hash ze in

  let e,_ = List.find (fun (e,t) -> t = uid) !expr_hash in

  e

let neg_ze z3e = Z3.Boolean.mk_not !ctx z3e 

let is_init_z3e =

  Z3.Expr.mk_const_s !ctx is_init_name  Zustre_common.bool_sort 

let get_zid (ze:Z3.Expr.expr) : Utils.tag = 

  try

    if Z3.Expr.equal ze is_init_z3e then -1 else

      if Z3.Expr.equal ze (neg_ze is_init_z3e) then -2 else

    Hashtbl.find ze_hash ze

  with _ -> (Format.eprintf "Looking for ze %s in Hash %a"

               (Z3.Expr.to_string ze)

               (fun fmt hash -> Hashtbl.iter (fun ze uid -> Format.fprintf fmt "%s -> %i@ " (Z3.Expr.to_string ze) uid) hash ) ze_hash;

             assert false)

let add_expr =

  let cpt = ref 0 in

  fun e ze ->

  incr cpt;

  let uid = !cpt in

  expr_hash := (e, uid)::!expr_hash;

  Hashtbl.add e_hash uid ze;

  Hashtbl.add ze_hash ze uid

  (* let hash = ref [] in

   * let comp_expr e (e', _) = Corelang.is_eq_expr e e' in

   * let comp_zexpr ze (_, ze') = Z3.Expr.equal ze ze' in *)

(*

  zexpr_to_guard_list ze

  *)

let implies =

  let ze_implies_hash : ((Utils.tag * Utils.tag), bool) Hashtbl.t  = Hashtbl.create 13 in

  fun ze1 ze2 ->

  let ze1_uid = get_zid ze1 in

  let ze2_uid = get_zid ze2 in

  if Hashtbl.mem ze_implies_hash (ze1_uid, ze2_uid) then

    Hashtbl.find ze_implies_hash (ze1_uid, ze2_uid)

  else

    begin

       Format.eprintf "Checking implication: %s => %s? "

        (Z3.Expr.to_string ze1) (Z3.Expr.to_string ze2)

        ; 

      let solver = Z3.Solver.mk_simple_solver !ctx in

      let tgt = Z3.Boolean.mk_not !ctx (Z3.Boolean.mk_implies !ctx ze1 ze2) in

      let res =

        try

          let status_res = Z3.Solver.check solver [tgt] in

          match status_res with

          | Z3.Solver.UNSATISFIABLE -> Format.eprintf "Valid!@."; 

             true

          | _ -> Format.eprintf "not proved valid@."; 

             false

        with Zustre_common.UnknownFunction(id, msg) -> (

          report ~level:1 msg;

          false

        )

      in

      Hashtbl.add ze_implies_hash (ze1_uid,ze2_uid) res ;

      res

    end

    (* Forall e in tl, checking whether hd => e or e => hd, to keep hd

  if false then

    Format.eprintf "Before simplify: %a@." pp_guard_list l; 

  if false then (

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

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

  );

    if false then Format.eprintf "Z3 exprs1: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; 

        if false then Format.eprintf "Z3 exprs2: [%a]@ " (fprintf_list ~sep:",@ " (fun fmt e -> Format.fprintf fmt "%s" (Z3.Expr.to_string e))) zl; 

     if false then Format.eprintf "Z3 status: %s@ @]@. " (Z3.Solver.string_of_status status_res); 

        (* TODO: may be reactivate but it may create new expressions *)

        (* let l = goal_simplify zl in *)

        let l = List.fold_left

                  (fun accu ze -> accu @ (zexpr_to_guard_list ze))

                  []

                  zl

        in

(* Most costly function: has the be efficiently implemented.  All

   registered guards are initially produced by the call to

   combine_guards. We csan normalize the guards to ease the

   comparisons.

   We assume that gl1 and gl2 are already both satisfiable and in a

   kind of reduced form. Let lshort and llong be the short and long

   list of gl1, gl2. We check whether each element elong of llong is

   satisfiable with lshort. If no, stop. If yes, we search to reduce

   the list. If elong => eshort_i, we can remove eshort_i from

   lshort. we can continue with this lshort shortened, lshort'; it is

   not necessary to add yet elong in lshort' since we already know

   rthat elong is somehow reduced with respect to other elements of

   llong. If eshort_i => elong, then we keep ehosrt_i in lshort and do

   not store elong.

   After iterating through llong, we have a shortened version of

   lshort + some elements of llong that have to be remembered. We add

   them to this new consolidated list. 

 *)

(* combine_guards ~fresh:Some(e,b) gl1 gl2 returns ok, gl with ok=true

   when (e=b) ang gl1 and gl2 is satisfiable and gl is a consilidated

   version of it.  *)

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

    let ok, _ = check_sat e in

    ok

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

    let e2z e pn =

      match e with

        | IsInit -> if pn then is_init_z3e else neg_ze is_init_z3e

        | Expr e -> expr_to_z3_expr (if pn then e else (Corelang.push_negations ~neg:true e))

      in

    implies (e2z e1 pn1) (e2z e2 pn2)

  in

  let lshort, llong =

    if List.length gl1 > List.length gl2 then gl2, gl1 else gl1, gl2

  in

  let merge long short =

    let short, long_sel, ok = 

    List.fold_left (fun (short,long_sel, ok) long_e ->

        if not ok then

          [],[], false (* Propagating unsat case *)

        else if check_sat (long_e::short) then

          let short, keep_long_e =

            List.fold_left (fun (accu_short, keep_long_e) eshort_i ->

                if not keep_long_e then (* shorten the algo *)

                  eshort_i :: accu_short, false

                else (* keep_long_e = true in the following *)

                  if implies eshort_i long_e then

                    (* First case is trying to remove long_e!

                     Since short is already normalized, we can remove

                     long_e. If later long_e is stronger than another

                     element of short, then necessarily eshort_i =>

                     long_e ->

                     that_other_element_of_short. Contradiction. *)

                    eshort_i::accu_short, false

                  else if implies long_e eshort_i then 

                    (* removing eshort_i, keeping long_e. *)

                    accu_short, true

                  else (* Not comparable, keeping both *)

                    eshort_i::accu_short, true

              )

              ([],true) (* Initially we assume that we will keep long_e *)

              short

          in

          if keep_long_e then

            short, long_e::long_sel, true

          else

            short, long_sel, true

          [],[],false

      ) (short, [], true) long

    in

    ok, long_sel@short

  let ok, l = match fresh with

    | None -> true, []

    | Some g -> merge [g] []

  in

  if not ok then

  else

    let ok, lshort = merge lshort l in

    if not ok then

      false, []

    else

      merge llong lshort

  let l, all_invalid =

    List.fold_left (

        fun (accu, all_invalid) (g2,e2) ->

        List.fold_left (

            fun (accu, all_invalid) (g1,e1) ->

            (* Format.eprintf "@[<v 2>Combining guards: (%a=%b) AND [%a] AND [%a]@ "

             *  pp_elem e1

             *  posneg

             *  pp_guard_list g1

             *  pp_guard_list g2; *)

            let ok, gl = combine_guards ~fresh:(Some(e1,posneg)) g1 g2 in

            (* Format.eprintf "@]@ Result is [%a]@ "

             *   pp_guard_list gl; *)

            if ok then

              (gl, e2)::accu, false

            else (

              accu, all_invalid

            )

          ) (accu, all_invalid) gel1

      ) ([], true) gel2

  in

  not all_invalid, l

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

   by its definition.

*)

       let ok_then, g_then = concatenate_ge g true e1 in

       let ok_else, g_else = concatenate_ge g false e2 in

       (if ok_then then g_then else [])@

         (if ok_else then g_else else [])

(* Previous version of the function: way too costly 

let pick_guard mem_defs : expr option =  

   *)

(* Returning the first non empty guard expression *)

let rec pick_guard mem_defs : expr option =

  match mem_defs with

  | [] -> None

  | (_, gel)::tl -> (

    let found =

      List.fold_left (fun found (g,_) ->

          if found = None then

            match g with

            | [] -> None

            | (Expr e, _)::_ -> Some e

            | (IsInit, _)::_ -> assert false (* should be removed already *)

          else

            found

        ) None gel

    in

    if found = None then pick_guard tl else found

  )

         Format.eprintf "Pos_prefix: %a@.Neg_prefix: %a@."

           pp_guard_list (List.map (fun (e,b) -> Expr e ,b) pos_prefix)

           pp_guard_list (List.map (fun (e,b) -> Expr e ,b) neg_prefix);

         let ok_pos, pos_prefix = clean pos_prefix in         

         Format.eprintf "Pos_prefix: %b %a@.Neg_prefix: %b %a@."

           ok_pos pp_guard_list (List.map (fun (e,b) -> Expr e ,b) pos_prefix)

           ok_neg pp_guard_list (List.map (fun (e,b) -> Expr e ,b) neg_prefix);

     storing others in the "defs" hashtbl.

     Each assign is stored in a hash tbl as list of guarded

     expressions. The memory definition is also "rewritten" as such a

     list of guarded assigns.  *)