- let rec eval_aux f = match f.pos with
- | Atom(`Left,b,q,_) -> if b == (Ptset.mem q s1) then (true,res1) else false,TS.empty
- | Atom(`Right,b,q,_) -> if b == (Ptset.mem q s2) then (true,res2) else false,TS.empty
- | True -> true,(TS.union res1 res2)
- | False -> false,TS.empty
- | Or(f1,f2) ->
- let b1,r1 = eval_aux f1
- and b2,r2 = eval_aux f2
- in
- let r1 = if b1 then r1 else TS.empty
- and r2 = if b2 then r2 else TS.empty
- in (b1 || b2, TS.union r1 r2)
-
- | And(f1,f2) ->
- let b1,r1 = eval_aux f1
- and b2,r2 = eval_aux f2
- in
- if b1 && b2 then (true, TS.union r1 r2)
- else (false,TS.empty)
+ let hfeval = HFEval.create 4097
+
+
+ let eval_form_bool f s1 s2 =
+ let rec eval f = match f.pos with
+ | Atom((`Left|`LLeft),b,q) -> if b == (Ptset.mem q s1) then (true,true,false) else false,false,false
+ | Atom((`Right|`RRight),b,q) -> if b == (Ptset.mem q s2) then (true,false,true) else false,false,false
+ (* test some inlining *)
+ | True -> true,true,true
+ | False -> false,false,false
+ | _ ->
+ try
+ HFEval.find hfeval (f.fid,s1,s2)
+ with
+ | Not_found -> let r =
+ match f.pos with
+ | Or(f1,f2) ->
+ let b1,rl1,rr1 = eval f1
+ in
+ if b1 && rl1 && rr1 then (true,true,true)
+ else
+ let b2,rl2,rr2 = eval 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)
+ | And(f1,f2) ->
+ let b1,rl1,rr1 = eval f1 in
+ if b1 && rl1 && rr1 then (true,true,true)
+ else if b1
+ then let b2,rl2,rr2 = eval f2 in
+ if b2 then (true,rl1||rl2,rr1||rr2)
+ else (false,false,false)
+ else (false,false,false)
+ | _ -> assert false
+ in
+ HFEval.add hfeval (f.fid,s1,s2) r;
+ r
+ in eval f
+
+
+ let fstate_pool = Hashtbl.create 11
+
+ let merge_pred a b = match a,b with
+ | Some(f1), Some(f2) -> Some(fun x -> f1 x || f2 x)
+ | None,None -> None
+ | None,Some(_) -> b
+ | Some(_),None -> a
+
+ let acc_pred p l1 l2 = match p with
+ | `Left _ -> p::l1,l2
+ | `Right _ -> l1,p::l2
+ | _ -> l1,l2
+
+
+ let merge_trans t a tag q acc =
+ List.fold_left (fun (accf,accm,acchtrue) (ts,(m,f,pred)) ->
+ if TagSet.mem tag ts
+ then
+ let tmpf,hastrue =
+ if is_true f then
+ let newfinal =
+ try Hashtbl.find fstate_pool f.fid with
+ | Not_found -> let s = mk_state() in
+ a.states <- Ptset.add s a.states;
+ a.final <- Ptset.add s a.final;
+ Hashtbl.add fstate_pool f.fid s;s
+ in
+ (atom_ `Left true newfinal),true
+ else f,false in
+ (or_ tmpf accf,accm||m,acchtrue||hastrue)
+ else (accf,accm,acchtrue)
+ ) acc (try Hashtbl.find a.phi q with Not_found -> [])
+
+ let get_trans t a tag r =
+ try
+ let mark,f,predl,has_true =
+ HTagSet.find a.sigma (r,tag)
+ in f.st,f,mark,has_true,r
+ with
+ Not_found ->
+ let f,mark,has_true,accq =
+ Ptset.fold (fun q (accf,accm,acchtrue,accq) ->
+ let naccf,naccm,nacctrue =
+ merge_trans t a tag q (accf,accm,acchtrue )
+ in
+ if is_false naccf then (naccf,naccm,nacctrue,accq)
+ else (naccf,naccm,nacctrue,Ptset.add q accq)
+ )
+ r (false_,false,false,Ptset.empty)
+ in
+ HTagSet.add a.sigma (accq,tag) (mark,f,([],[]),has_true);
+ f.st,f,mark,has_true,accq
+
+ let h_union = Hashtbl.create 4097
+
+ let pt_cup s1 s2 =
+ let h = (Ptset.hash s1,Ptset.hash s2) in
+ try
+ Hashtbl.find h_union h
+ with
+ | Not_found -> let s = Ptset.union s1 s2
+ in
+ Hashtbl.add h_union h s;s