-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)