- type node_status = {
- sat : StateSet.t; (* States that are satisfied at the current node *)
- todo : StateSet.t; (* States that remain to be proven *)
- (* For every node_status and automaton a:
- a.states - (sat U todo) = unsat *)
- summary : NodeSummary.t; (* Summary of the shape of the node *)
- }
-(* Describe what is kept at each node for a run *)
-
- module NodeStatus =
- struct
- include Hcons.Make(struct
- type t = node_status
- let equal c d =
- c == d ||
- c.sat == d.sat &&
- c.todo == d.todo &&
- c.summary == d.summary
-
- let hash c =
- HASHINT3((c.sat.StateSet.id :> int),
- (c.todo.StateSet.id :> int),
- c.summary)
- end
- )
- let print ppf s =
- fprintf ppf
- "{ sat: %a; todo: %a; summary: _ }"
- StateSet.print s.node.sat
- StateSet.print s.node.todo
- end
-
- let dummy_status =
- NodeStatus.make { sat = StateSet.empty;
- todo = StateSet.empty;
- summary = NodeSummary.dummy;
- }
-
-