- let sat, unsat, removed, kept, todo =
- Ata.TransList.fold
- (fun trs acc ->
- let q, lab, phi = Ata.Transition.node trs in
- let a_sat, a_unsat, a_rem, a_kept, a_todo = acc in
- if StateSet.mem q a_sat || StateSet.mem q a_unsat then acc else
- let new_phi =
- eval_form phi fcs nss ps old_config old_summary
- in
- if Ata.Formula.is_true new_phi then
- StateSet.add q a_sat, a_unsat, StateSet.add q a_rem, a_kept, a_todo
- else if Ata.Formula.is_false new_phi then
- a_sat, StateSet.add q a_unsat, StateSet.add q a_rem, a_kept, a_todo
- else
- let new_tr = Ata.Transition.make (q, lab, new_phi) in
- (a_sat, a_unsat, a_rem, StateSet.add q a_kept, (Ata.TransList.cons new_tr a_todo))
- ) old_todo (old_sat, old_unsat, StateSet.empty, StateSet.empty, Ata.TransList.nil)
+ let sat, todo =
+ StateSet.fold (fun q ((a_sat, a_todo) as acc) ->
+ let phi =
+ get_form cache2 auto tag q
+ in
+ let v = eval_form phi fcs nss ps old_status old_summary in
+ match v with
+ True -> StateSet.add q a_sat, a_todo
+ | False -> acc
+ | Unknown -> a_sat, StateSet.add q a_todo
+ ) old_todo (old_sat, StateSet.empty)