Format.fprintf ppf "%s\n%!" (String.make (maxt+maxh+3) '_')
+module FormTable = Hashtbl.Make(struct
+ type t = Formula.t*StateSet.t*StateSet.t
+ let equal (f1,s1,t1) (f2,s2,t2) =
+ Formula.equal f1 f2 && StateSet.equal s1 s2 && StateSet.equal t1 t2
+ let hash (f,s,t) =
+ HASHINT3(Formula.uid f ,StateSet.uid s,StateSet.uid t)
+ end)
+(* Too slow
module MemoForm = Memoizer.Make(
- Hashtbl.Make(struct
- type t = Formula.t*(StateSet.t*StateSet.t)
- let equal (f1,(s1,t1)) (f2,(s2,t2)) =
- Formula.equal f1 f2 && StateSet.equal s1 s2 && StateSet.equal t1 t2
- let hash (f,(s,t)) =
- HASHINT3(Formula.uid f ,StateSet.uid s,StateSet.uid t)
- end))
-
-module F = Formula
+module F = Formula
+(*
let eval_form_bool =
MemoForm.make_rec(
fun eval (f, ((s1,s2) as sets)) ->
else (false,false,false)
)
-let eval_form_bool f s1 s2 = eval_form_bool (f,(s1,s2))
-
+*) *)
+module F = Formula
-module MemoFormlist = Memoizer.Make(
- Hashtbl.Make(struct
- type t = Formlist.t*(StateSet.t*StateSet.t)
- let equal (f1,(s1,t1)) (f2,(s2,t2)) =
- Formlist.equal f1 f2 && StateSet.equal s1 s2 && StateSet.equal t1 t2
- let hash (f,(s,t)) =
- HASHINT3(Formlist.uid f ,StateSet.uid s,StateSet.uid t)
- end))
+let eval_form_bool =
+ let h_f = FormTable.create BIG_H_SIZE in
+ fun f s1 s2 ->
+ let rec loop f =
+ match F.expr f with
+ | F.True -> true,true,true
+ | F.False -> false,false,false
+ | F.Atom((`Left|`LLeft),b,q) ->
+ if b == (StateSet.mem q s1)
+ then (true,true,false)
+ else false,false,false
+ | F.Atom(_,b,q) ->
+ if b == (StateSet.mem q s2)
+ then (true,false,true)
+ else false,false,false
+ | f' ->
+ try FormTable.find h_f (f,s1,s2)
+ with Not_found -> let r =
+ match f' with
+ | F.Or(f1,f2) ->
+ let b1,rl1,rr1 = loop f1
+ in
+ if b1 && rl1 && rr1 then (true,true,true) else
+ let b2,rl2,rr2 = loop f2 in
+ let rl1,rr1 = if b1 then rl1,rr1 else false,false
+ and rl2,rr2 = if b2 then rl2,rr2 else false,false
+ in (b1 || b2, rl1||rl2,rr1||rr2)
+
+ | F.And(f1,f2) ->
+ let b1,rl1,rr1 = loop f1 in
+ if b1 && rl1 && rr1 then (true,true,true) else
+ if b1 then
+ let b2,rl2,rr2 = loop f2 in
+ if b2 then (true,rl1||rl2,rr1||rr2) else (false,false,false)
+ else (false,false,false)
+ | _ -> assert false
+ in FormTable.add h_f (f,s1,s2) r;r
+ in loop f
+
+module FTable = Hashtbl.Make(
+ struct
+ type t = Formlist.t*StateSet.t*StateSet.t
+ let equal (f1,s1,t1) (f2,s2,t2) =
+ Formlist.equal f1 f2 && StateSet.equal s1 s2 && StateSet.equal t1 t2;;
+ let hash (f,s,t) = HASHINT3(Formlist.uid f ,StateSet.uid s,StateSet.uid t);;
+ end)
+
+(*
+module MemoFormlist = Memoizer.Make(FTable)
-
-
+ Too slow
let eval_formlist = MemoFormlist.make_rec (
fun eval (fl,((s1,s2)as sets)) ->
match Formlist.node fl with
let s,b',b1',b2',amark = eval (fll,sets) in
if b then (StateSet.add q s, b, b1'||b1,b2'||b2,mark||amark)
else s,b',b1',b2',amark )
-
- let eval_formlist ?(memo=true) s1 s2 fl =
- eval_formlist (fl,(s1,s2))
-
+*)
+
+
+
+ let eval_formlist =
+ let h_f = FTable.create BIG_H_SIZE in
+ fun s1 s2 fl ->
+ let rec loop fl =
+ let key = (fl,s1,s2) in
+ try
+ FTable.find h_f key
+ with
+ | Not_found ->
+ match Formlist.node fl with
+ | Formlist.Nil -> StateSet.empty,false,false,false,false
+ | Formlist.Cons(f,fll) ->
+ let q,mark,f,_ = Transition.node f in
+ let b,b1,b2 = eval_form_bool f s1 s2 in
+ let s,b',b1',b2',amark = loop fll in
+ let r = if b then (StateSet.add q s, b, b1'||b1,b2'||b2,mark||amark)
+ else s,b',b1',b2',amark
+ in FTable.add h_f key r;r
+ in loop fl
let tags_of_state a q =
Hashtbl.fold
if Tree.is_nil t then null_result()
else
let tag = Tree.tag t in
- let fl_list,llist,rlist,first,next = get_trans slist tag a t in
+ let fl_list,llist,_,first,next = get_trans slist tag a t in
let sl1,res1 = loop (first t) llist t in
let sl2,res2 = null_result() in
let res = eval_fold2_slist fl_list sl1 sl2 res1 res2 t