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