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 11:20:58 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      let oldi = config.Ata.round in
  40      Html.trace (T.preorder tree node) i oldi
  41        "node: %i<br/>%s<br/>sat: %a<br/>unsat: %a<br/>todo: %around: %i<br/>"
  42        ((T.preorder tree node):>int)
  43        msg
  44        StateSet.print config.Ata.sat
  45        StateSet.print config.Ata.unsat
  46        (Ata.TransList.print ~sep:"<br/>") config.Ata.todo oldi
  47
  48
  49   let get c t n = Cache.N1.find c (T.preorder t n)
  50
  51   let set c t n v i =
  52     v.Ata.Config.node.Ata.round <- i;
  53     Cache.N1.add c (T.preorder t n) v
  54
  55
  56   type run = { config : Ata.Config.t Cache.N1.t;
  57                unstable : Bitvector.t;
  58                mutable redo : bool;
  59                mutable pass : int;
  60              }
  61
  62
  63   let top_down_run auto tree node run =
  64     let cache = run.config in
  65     let unstable = run.unstable in
  66     let _i = run.pass in
  67     let rec loop node =
  68       if node == T.nil then false else begin
  69         let parent = T.parent tree node in
  70         let fc = T.first_child tree node in
  71         let ns = T.next_sibling tree node in
  72         let tag = T.tag tree node in
  73         let config0 =
  74           let c = get cache tree node in
  75           if c == Cache.N1.dummy cache then
  76             Ata.Config.make
  77               { c.Ata.Config.node with
  78                 Ata.todo = Ata.get_trans auto tag auto.Ata.states;
  79                 summary = Ata.node_summary
  80                   (node == T.first_child tree parent) (* is_left *)
  81                   (node == T.next_sibling tree parent) (* is_right *)
  82                   (fc != T.nil) (* has_left *)
  83                   (ns != T.nil) (* has_right *)
  84                   (T.kind tree node) (* kind *)
  85               }
  86           else c
  87         in
  88
  89         TRACE(html tree node _i config0 "Entering node");
  90
  91         let ps = get cache tree parent in
  92         let fcs = get cache tree fc in
  93         let nss = get cache tree ns in
  94         let config1 = Ata.eval_trans auto fcs nss ps config0 in
  95
  96         TRACE(html tree node _i config1 "Updating transitions");
  97
  98         if config0 != config1 then set cache tree node config1 _i;
  99         let old_unstable_left = Bitvector.unsafe_get unstable (T.preorder tree fc) in
 100         let unstable_left = old_unstable_left && loop fc in
 101         let fcs1 = get cache tree fc in
 102         let config2 = Ata.eval_trans auto fcs1 nss ps config1 in
 103
 104         TRACE(html tree node _i config2 "Updating transitions (after first-child)");
 105
 106         if config1 != config2 then set cache tree node config2 _i;
 107         let old_unstable_right = Bitvector.unsafe_get unstable (T.preorder tree ns) in
 108         let unstable_right = old_unstable_right && loop ns in
 109         let nss1 = get cache tree ns 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 set cache tree node config3 _i;
 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 (T.preorder tree node) unstable_self;
 121         unstable_self
 122       end
 123     in
 124     loop node
 125
 126   let get_results auto tree node cache =
 127     let rec loop node acc =
 128       if node == T.nil then acc
 129       else
 130         let acc0 = loop (T.next_sibling tree node) acc in
 131         let acc1 = loop (T.first_child tree node) acc0 in
 132
 133         if StateSet.intersect
 134           (get cache tree node).Ata.Config.node.Ata.sat
 135           auto.Ata.selection_states then node::acc1
 136         else acc1
 137     in
 138     loop node []
 139
 140
 141   let stats run =
 142     let count = ref 0 in
 143     let len = Bitvector.length run.unstable in
 144     for i = 0 to len - 1 do
 145       if not (Bitvector.unsafe_get run.unstable i) then
 146         incr count
 147     done;
 148     eprintf "@[STATS: %i nodes over %i were skipped in iteration %i (%.2f %%), redo is: %b@]@."
 149       !count len run.pass (100. *. (float !count /. float len))
 150       run.redo
 151
 152
 153   let eval auto tree node =
 154     let run = { config = Cache.N1.create
 155         Ata.(Config.make { sat = StateSet.empty;
 156                            unsat = StateSet.empty;
 157                            todo = TransList.nil;
 158                            summary = dummy_summary;
 159                            round = ~-1
 160                          });
 161                 unstable = Bitvector.create ~init:true (T.size tree);
 162                 redo = true;
 163                 pass = 0
 164               }
 165     in
 166     while run.redo do
 167       run.redo <- false;
 168       Ata.reset auto; (* prevents the .cache2 and .cache4 memoization tables from growing too much *)
 169       run.redo <- top_down_run auto tree node run;
 170       stats run;
 171       run.pass <- run.pass + 1;
 172     done;
 173     at_exit (fun () -> eprintf "@[STATS: %i iterations@]@." run.pass);
 174     at_exit (fun () -> stats run);
 175     let r = get_results auto tree node run.config in
 176
 177     TRACE(Html.gen_trace (module T : Tree.S with type t = T.t) (tree));
 178
 179     r
 180
 181 end