in
loop phi
- type trivalent = False | True | Unknown
-
- let or_ t1 t2 = match t1 with
- False -> t2
- | True -> True
- | Unknown -> if t2 == True then True else Unknown
-
- let and_ t1 t2 = match t1 with
- False -> False
- | True -> t2
- | Unknown -> if t2 == False then False else Unknown
- let of_bool = function false -> False | true -> True
-
- let eval_form phi fcs nss ps ss summary =
- let open Ata in
- let rec loop phi =
- begin match Formula.expr phi with
- | Boolean.False -> False
- | Boolean.True -> True
- | Boolean.Atom (a, b) ->
- begin
- let open NodeSummary in
- match a.Atom.node with
- | Move (m, q) ->
- let sum = match m with
- `First_child -> fcs
- | `Next_sibling -> nss
- | `Parent | `Previous_sibling -> ps
- | `Stay -> ss
- in
- if StateSet.mem q sum.NodeStatus.node.sat then of_bool b
- else if StateSet.mem q sum.NodeStatus.node.unsat then of_bool (not b)
- else Unknown
- | Is_first_child -> of_bool (b == is_left summary)
- | Is_next_sibling -> of_bool (b == is_right summary)
- | Is k -> of_bool (b == (k == kind summary))
- | Has_first_child -> of_bool (b == has_left summary)
- | Has_next_sibling -> of_bool (b == has_right summary)
- end
- | Boolean.And(phi1, phi2) -> and_ (loop phi1) (loop phi2)
- | Boolean.Or (phi1, phi2) -> or_ (loop phi1) (loop phi2)
- end
- in
- loop phi
-
let eval_trans_aux cache4 fcs nss ps ss old_config =
let { sat = old_sat;
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 phi_val =
+ let new_phi =
eval_form phi fcs nss ps old_config old_summary
in
- match phi_val with
- | False -> a_sat, StateSet.add q a_unsat, StateSet.add q a_rem, a_kept, a_todo
- | True -> StateSet.add q a_sat, a_unsat, StateSet.add q a_rem, a_kept, a_todo
- | Unknown ->
- (a_sat, a_unsat, a_rem, StateSet.add q a_kept, (Ata.TransList.cons trs a_todo))
+ 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)
in
(* States that have been removed from the todo list and not kept are now