DOES NOT WORK AT ALL

1 files changed, 142 insertions, 135 deletions

diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index bc0755b..65255ca 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -501,150 +501,156 @@ end = struct
 
           let qc = ref None in
 
-          (* put true or false conditions into location definition *)
-          Hashtbl.iter
-            (fun q (loc : location) ->
-              let rec iter () =
-                try
-                  let cond, _ = List.find
-                    (fun (c, _) ->
-                      is_bot (apply_cl loc.v (conslist_of_f c))
-                      || is_bot (apply_cl loc.v (conslist_of_f (BNot c))))
-                    (ternary_conds loc.f)
-                  in
-                  let tr =
-                    if is_bot (apply_cl loc.v (conslist_of_f cond))
-                    then BNot cond
-                    else cond
-                  in
-                  loc.def <- apply_cl loc.def (conslist_of_f tr);
-                  loc.f <- simplify_k [tr] loc.f;
-                  loc.f <- simplify_k (get_root_true loc.f) loc.f;
-                  loc.cl <- conslist_of_f loc.f;
-                  iter()
-                with Not_found -> ()
-              in iter ())
-            e.loc;
-
-          (* find splitting condition *)
-          let voi = List.map (fun (a, b, c) -> c) e.guarantees in
-
-          Hashtbl.iter
-            (fun q (loc:location) ->
-              if loc.depth < e.opt.max_dp_depth then
-              let cs = ternary_conds loc.f in
-              List.iter
-                (fun (c, exprs) ->
-                  let cases_t = apply_cl_all_cases (top e) (conslist_of_f c) in
-                  let cases_f = apply_cl_all_cases (top e) (conslist_of_f (BNot c)) in
-                  let cases = List.mapi (fun i c -> i, c) (cases_t @ cases_f) in
-                  if
-                    List.length 
-                      (List.filter
-                        (fun (_, case) -> not (is_bot (meet loc.v case)))
-                        cases)
-                      >= 2
-                  then
-                    (* calculate which transitions qi -> q stay or are destroyed (approximation) *)
-                    let in_tc =
-                      List.flatten @@ List.map
-                        (fun qi ->
-                          let loci = Hashtbl.find e.loc qi in
-                          let v = apply_cl
-                            (meet (pass_cycle e.ve loci.v) loc.def)
-                            loc.cl in
-                          List.map
-                            (fun (ci, case) -> qi, ci, not (is_bot (meet v case)))
-                            cases)
-                        loc.in_t
+          if Hashtbl.length e.loc < e.opt.max_dp_width then begin
+            (* put true or false conditions into location definition *)
+            Hashtbl.iter
+              (fun q (loc : location) ->
+                let rec iter () =
+                  try
+                    let cond, _ = List.find
+                      (fun (c, _) ->
+                        is_bot (apply_cl loc.v (conslist_of_f c))
+                        || is_bot (apply_cl loc.v (conslist_of_f (BNot c))))
+                      (ternary_conds loc.f)
                     in
-                    (* calculate which transitions q -> qo stay or are destroyed (approximation) *)
-                    let out_tc =
-                      List.flatten @@ List.map
-                        (fun (ci, case) ->
-                          let v = meet loc.v case in
-                          List.map
-                            (fun qo ->
-                                let loco = Hashtbl.find e.loc qo in
-                                let w = apply_cl
-                                  (meet (pass_cycle e.ve v) loco.def)
-                                  loco.cl
-                                in qo, ci, not (is_bot w))
-                            loc.out_t)
-                        cases
+                    let tr =
+                      if is_bot (apply_cl loc.v (conslist_of_f cond))
+                      then BNot cond
+                      else cond
                     in
-                    (* calculate which cases have a good number of disappearing transitions *)
-                    let fa =
-                      let cs_sc =
-                        List.map
+                    loc.def <- apply_cl loc.def (conslist_of_f tr);
+                    loc.f <- simplify_k [tr] loc.f;
+                    loc.f <- simplify_k (get_root_true loc.f) loc.f;
+                    loc.cl <- conslist_of_f loc.f;
+                    iter()
+                  with Not_found -> ()
+                in iter ())
+              e.loc;
+
+            (* find splitting condition *)
+            let voi = List.map (fun (a, b, c) -> c) e.guarantees in
+
+            Hashtbl.iter
+              (fun q (loc:location) ->
+                if loc.depth < e.opt.max_dp_depth then
+                let cs = ternary_conds loc.f in
+                List.iter
+                  (fun (c, exprs) ->
+                    let cases_t = apply_cl_all_cases (top e) (conslist_of_f c) in
+                    let cases_f = apply_cl_all_cases (top e) (conslist_of_f (BNot c)) in
+                    let cases = List.mapi (fun i c -> i, c) (cases_t @ cases_f) in
+                    if
+                      List.length 
+                        (List.filter
+                          (fun (_, case) -> not (is_bot (meet loc.v case)))
+                          cases)
+                        >= 2
+                    then
+                      (* calculate which transitions qi -> q stay or are destroyed (approximation) *)
+                      let in_tc =
+                        List.flatten @@ List.map
+                          (fun qi ->
+                            let loci = Hashtbl.find e.loc qi in
+                            let v = apply_cl
+                              (meet (pass_cycle e.ve loci.v) loc.def)
+                              loc.cl in
+                            List.map
+                              (fun (ci, case) -> qi, ci, not (is_bot (meet v case)))
+                              cases)
+                          loc.in_t
+                      in
+                      (* calculate which transitions q -> qo stay or are destroyed (approximation) *)
+                      let out_tc =
+                        List.flatten @@ List.map
                           (fun (ci, case) ->
-                            let a = 
-                              List.length
-                                (List.filter (fun (qi, c, a) -> not a && c = ci) in_tc)
-                            in
-                            let b =
-                              List.length
-                                (List.filter (fun (qo, c, a) -> not a && c = ci) out_tc)
-                            in
-                            a + b + a * b)
+                            let v = meet loc.v case in
+                            List.map
+                              (fun qo ->
+                                  let loco = Hashtbl.find e.loc qo in
+                                  let w = apply_cl
+                                    (meet (pass_cycle e.ve v) loco.def)
+                                    loco.cl
+                                  in qo, ci, not (is_bot w))
+                              loc.out_t)
                           cases
                       in
-                      5 * List.fold_left max 0 cs_sc
-                    in
-                    (* calculate which states become inaccessible *)
-                    let fb =
-                      if fa = 0 || List.for_all (fun (_, _, a) -> a) out_tc
-                      then 0
-                      else
-                        let ff id =   (* transition function for new graph *)
-                          if id >= 1000000 then
-                            let case = id - 1000000 in
-                            List.map (fun (qo, _, _) -> qo)
-                              (List.filter (fun (_, c, a) -> c = case && a) out_tc)
+                      (* calculate which cases have a good number of disappearing transitions *)
+                      let fa =
+                        let cs_sc =
+                          List.map
+                            (fun (ci, case) ->
+                              let a = 
+                                List.length
+                                  (List.filter (fun (qi, c, a) -> not a && c = ci) in_tc)
+                              in
+                              let b =
+                                List.length
+                                  (List.filter (fun (qo, c, a) -> not a && c = ci) out_tc)
+                              in
+                              a * b + (if a + b > 0 then 1 else 0))
+                            cases
+                        in
+                        let a = List.fold_left max 0 cs_sc in
+                        let b = 5 * a in
+                        if a > 0 && b = 0 then 1 else b
+                      in
+                      if fa <> 0 then begin
+                        (* calculate which states become inaccessible *)
+                        let fb =
+                          if List.for_all (fun (_, _, a) -> a) out_tc
+                          then 0
                           else
-                            let out_t = (Hashtbl.find e.loc id).out_t in
-                            if List.mem loc.id out_t then
-                              (List.map (fun (_, c, _) -> c + 1000000)
-                                (List.filter (fun (qi, _, a) -> qi = id && a) in_tc))
-                              @ (List.filter ((<>) id) out_t)
-                            else out_t
+                            let ff id =   (* transition function for new graph *)
+                              if id >= 1000000 then
+                                let case = id - 1000000 in
+                                List.map (fun (qo, _, _) -> qo)
+                                  (List.filter (fun (_, c, a) -> c = case && a) out_tc)
+                              else
+                                let out_t = (Hashtbl.find e.loc id).out_t in
+                                if List.mem loc.id out_t then
+                                  (List.map (fun (_, c, _) -> c + 1000000)
+                                    (List.filter (fun (qi, _, a) -> qi = id && a) in_tc))
+                                  @ (List.filter ((<>) id) out_t)
+                                else out_t
+                            in
+                            let memo = Hashtbl.create 12 in
+                            let rec do_x id =
+                              if not (Hashtbl.mem memo id) then begin
+                                Hashtbl.add memo id ();
+                                List.iter do_x (ff id)
+                              end
+                            in
+                            Hashtbl.iter (fun i loc2 -> if loc2.is_init && i <> loc.id then do_x i) e.loc;
+                            if loc.is_init then List.iter (fun (ci, _) -> do_x (ci+1000000)) cases;
+                            let disappear_count = (Hashtbl.length e.loc + List.length cases) - (Hashtbl.length memo) in
+                            21 * disappear_count
                         in
-                        let memo = Hashtbl.create 12 in
-                        let rec do_x id =
-                          if not (Hashtbl.mem memo id) then begin
-                            Hashtbl.add memo id ();
-                            List.iter do_x (ff id)
-                          end
+                        (* calculate in/out count, weighted by changing guarantees *)
+                        let fc =
+                          0 * (2 * List.length loc.out_t + List.length loc.in_t)
                         in
-                        Hashtbl.iter (fun i loc2 -> if loc2.is_init && i <> loc.id then do_x i) e.loc;
-                        if loc.is_init then List.iter (fun (ci, _) -> do_x (ci+1000000)) cases;
-                        let disappear_count = (Hashtbl.length e.loc + List.length cases) - (Hashtbl.length memo) in
-                        21 * disappear_count
-                    in
-                    (* calculate number of VOI (variables of interest) that are affected *)
-                    let fc =
-                      let vlist = refd_evars_of_f exprs in
-                      10 * List.length
-                      (List.filter (fun v -> List.mem v vlist) voi) in
-                    (* give score to split *)
-                    let fd = 2 * List.length loc.out_t + List.length loc.in_t in
-                    let score =
-                      if fa = 0 then 0 else
-                        fa + fb + fc + fd
-                    in
-                    Format.printf " %5d + %5d + %5d + %5d = %5d  (q%d)@." fa fb fc fd score loc.id;
-                    if score > 0 &&
-                      match !qc with
-                      | None -> true
-                      | Some (s, _, _, _, _) -> score >= s
-                    then
-                      qc := Some(score, q, c, cases_t, cases_f)
-                  )
-                cs
-            )
-            e.loc;
+                        (* calculate number of VOI (variables of interest) that are affected *)
+                        let fd =
+                          let vlist = refd_evars_of_f exprs in
+                          3 * List.length
+                          (List.filter (fun v -> List.mem v vlist) voi) in
+                        (* give score to split *)
+                        let score =
+                          if fa = 0 then 0 else
+                            fa + fb + fc + fd
+                        in
+                        Format.printf " %5d + %5d + %5d + %5d = %5d  (q%d)@." fa fb fc fd score loc.id;
+                        if score > 0 &&
+                          match !qc with
+                          | None -> true
+                          | Some (s, _, _, _, _) -> score >= s
+                        then
+                          qc := Some(score, q, c, cases_t, cases_f)
+                      end)
+                  cs
+              )
+              e.loc;
 
-          if Hashtbl.length e.loc < e.opt.max_dp_width then
             match !qc with
             | None ->
               Format.printf "@.Found no more possible refinement.@.@."
@@ -673,6 +679,7 @@ end = struct
                 List.iter (handle_case (BNot c)) cases_f;
                           
               iter (n+1)
+          end
         in iter 0;
 
         (* Check guarantees *)