Commit f94f3d37 authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Invariant: use an array-based map instead of a balanced binary tree.

parent d495ea19
Pipeline #188747 passed with stages
in 2 minutes and 7 seconds
......@@ -47,6 +47,14 @@ let stack_height (node : Lr1.node) : int =
(* By the way, this least fixed point analysis remains the most costly
computation throughout this module. *)
(* Our keys are the nodes of the LR(1) automaton. *)
module Key = struct
type t = Lr1.node
let n = Lr1.n
let encode = Lr1.number
end
(* Vectors of sets of states. *)
module StateVector = struct
......@@ -117,12 +125,12 @@ end
(* Compute the least fixed point. *)
let stack_states : Lr1.node -> property option =
let module F =
Fix.DataFlow.Run
(Fix.Glue.PersistentMapsToImperativeMaps(Lr1.NodeMap))
(StateVector)
(G)
let module M =
Fix.Glue.InjectMinimalImperativeMaps
(Fix.Glue.ArraysAsImperativeMaps(Key))
(Key)
in
let module F = Fix.DataFlow.Run(M)(StateVector)(G) in
F.solution
(* If every state is reachable, then the least fixed point must be non-[None]
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment