src/eval.ml

   1 (***********************************************************************)
   2 (*                                                                     *)
   3 (*                               TAToo                                 *)
   4 (*                                                                     *)
   5 (*                     Kim Nguyen, LRI UMR8623                         *)
   6 (*                   Université Paris-Sud & CNRS                       *)
   7 (*                                                                     *)
   8 (*  Copyright 2010-2013 Université Paris-Sud and Centre National de la *)
   9 (*  Recherche Scientifique. All rights reserved.  This file is         *)
  10 (*  distributed under the terms of the GNU Lesser General Public       *)
  11 (*  License, with the special exception on linking described in file   *)
  12 (*  ../LICENSE.                                                        *)
  13 (*                                                                     *)
  14 (***********************************************************************)
  15
  16 (*
  17   Time-stamp: <Last modified on 2013-04-25 17:22:15 CEST by Kim Nguyen>
  18 *)
  19
  20 INCLUDE "utils.ml"
  21 open Format
  22
  23 module Make (T : Tree.S) :
  24   sig
  25     val eval : Ata.t -> T.t -> T.node -> T.node list
  26   end
  27  = struct
  28
  29
  30 IFDEF HTMLTRACE
  31   THEN
  32 DEFINE TRACE(e) = (e)
  33   ELSE
  34 DEFINE TRACE(e) = ()
  35 END
  36
  37    let html tree node i config msg =
  38      let config = config.Ata.Config.node in
  39      Html.trace (T.preorder tree node) i
  40        "node: %i<br/>%s<br/>sat: %a<br/>unsat: %a<br/>todo: %around: %i<br/>"
  41        (T.preorder tree node)
  42        msg
  43        StateSet.print config.Ata.sat
  44        StateSet.print config.Ata.unsat
  45        (Ata.TransList.print ~sep:"<br/>") config.Ata.todo i
  46
  47
  48
  49   type run = { config : Ata.Config.t array;
  50                unstable : Bitvector.t;
  51                mutable redo : bool;
  52                mutable pass : int;
  53              }
  54
  55
  56
  57   let top_down_run auto tree node run =
  58     let module Array =
  59     struct
  60       include Array
  61       let get a i =
  62         if i < 0 then Ata.dummy_config else get a i
  63       let unsafe_get a i =
  64         if i < 0 then Ata.dummy_config else unsafe_get a i
  65     end
  66     in
  67     let cache = run.config in
  68     let unstable = run.unstable in
  69     let _i = run.pass in
  70     let rec loop node =
  71       let node_id = T.preorder tree node in
  72       if node == T.nil || not (Bitvector.get unstable node_id) then false else begin
  73         let parent = T.parent tree node in
  74         let fc = T.first_child tree node in
  75         let fc_id = T.preorder tree fc in
  76         let ns = T.next_sibling tree node in
  77         let ns_id = T.preorder tree ns in
  78         let tag = T.tag tree node in
  79         let config0 =
  80           let c = cache.(node_id) in
  81           if c == Ata.dummy_config then
  82             Ata.Config.make
  83               { c.Ata.Config.node with
  84                 Ata.todo = Ata.get_trans auto tag auto.Ata.states;
  85                 summary = Ata.node_summary
  86                   (node == T.first_child tree parent) (* is_left *)
  87                   (node == T.next_sibling tree parent) (* is_right *)
  88                   (fc != T.nil) (* has_left *)
  89                   (ns != T.nil) (* has_right *)
  90                   (T.kind tree node) (* kind *)
  91               }
  92           else c
  93         in
  94
  95         TRACE(html tree node _i config0 "Entering node");
  96
  97         let ps = cache.(T.preorder tree parent) in
  98         let fcs = cache.(fc_id) in
  99         let nss = cache.(ns_id) in
 100         let config1 = Ata.eval_trans auto fcs nss ps config0 in
 101
 102         TRACE(html tree node _i config1 "Updating transitions");
 103
 104         if config0 != config1 then cache.(node_id) <- config1;
 105         let unstable_left = loop fc in
 106         let fcs1 = cache.(fc_id) in
 107         let config2 = Ata.eval_trans auto fcs1 nss ps config1 in
 108
 109         TRACE(html tree node _i config2 "Updating transitions (after first-child)");
 110
 111         if config1 != config2 then cache.(node_id) <- config2;
 112         let unstable_right = loop ns in
 113         let nss1 = cache.(ns_id) in
 114         let config3 = Ata.eval_trans auto fcs1 nss1 ps config2 in
 115
 116         TRACE(html tree node _i config3 "Updating transitions (after next-sibling)");
 117
 118         if config2 != config3 then cache.(node_id) <- config3;
 119         let unstable_self =
 120           unstable_left
 121           || unstable_right
 122           || Ata.(TransList.nil != config3.Config.node.todo)
 123         in
 124         Bitvector.unsafe_set unstable node_id unstable_self;
 125         TRACE((if not unstable_self then
 126             Html.finalize_node
 127               node_id
 128               _i
 129               Ata.(StateSet.intersect config3.Config.node.sat auto.selection_states)));
 130         unstable_self
 131       end
 132     in
 133     loop node
 134
 135   let get_results auto tree node cache =
 136     let rec loop node acc =
 137       if node == T.nil then acc
 138       else
 139         let acc0 = loop (T.next_sibling tree node) acc in
 140         let acc1 = loop (T.first_child tree node) acc0 in
 141
 142         if Ata.(
 143           StateSet.intersect
 144             cache.(T.preorder tree node).Config.node.sat
 145             auto.selection_states) then node::acc1
 146         else acc1
 147     in
 148     loop node []
 149
 150
 151   let stats run =
 152     let count = ref 0 in
 153     let len = Bitvector.length run.unstable in
 154     for i = 0 to len - 1 do
 155       if not (Bitvector.unsafe_get run.unstable i) then
 156         incr count
 157     done;
 158     Logger.msg `STATS
 159       "%i nodes over %i were skipped in iteration %i (%.2f %%), redo is: %b"
 160       !count len run.pass (100. *. (float !count /. float len))
 161       run.redo
 162
 163
 164   let eval auto tree node =
 165     let len = T.size tree in
 166     let run = { config = Array.create len Ata.dummy_config;
 167                 unstable = Bitvector.create ~init:true len;
 168                 redo = true;
 169                 pass = 0
 170               }
 171     in
 172     while run.redo do
 173       run.redo <- false;
 174       Ata.reset auto; (* prevents the .cache2 and .cache4 memoization tables from growing too much *)
 175       run.redo <- top_down_run auto tree node run;
 176       stats run;
 177       run.pass <- run.pass + 1;
 178     done;
 179     at_exit (fun () -> Logger.msg `STATS "%i iterations" run.pass);
 180     at_exit (fun () -> stats run);
 181     let r = get_results auto tree node run.config in
 182
 183     TRACE(Html.gen_trace (module T : Tree.S with type t = T.t) (tree));
 184
 185     r
 186
 187 end