- if b1 then
- let b2,rl2,rr2 = eval (f2,sets) in
- if b2 then (true,rl1||rl2,rr1||rr2) else (false,false,false)
- else (false,false,false)
- )
- in
- eval (f,sets)
-
-
- 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_formlist ?(memo=true) s1 s2 fl =
- let sets = (s1,s2) in
- let eval = MemoFormlist.make_rec (
- fun eval (fl,_) ->
- if Formlist.is_empty fl
- then StateSet.empty,false,false,false,false
- else
- let f,fll = Formlist.uncons fl in
- 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 = eval (fll,sets) in
- if b then (StateSet.add q s, b, b1'||b1,b2'||b2,mark||amark)
- else s,b',b1',b2',amark )
- in eval (fl,sets)
-
+ if b1 then
+ let b2,rl2,rr2 = eval (f2,sets) in
+ if b2 then (true,rl1||rl2,rr1||rr2) else (false,false,false)
+ else (false,false,false)
+ )
+
+*) *)
+module F = Formula
+
+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
+ | 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 = 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 =
+ 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