-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
13 changed files
with
359 additions
and
179 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,104 +1,105 @@ | ||
module NFA = LevNFA | ||
module Make (NFA : NFA.NFA_t) = struct | ||
|
||
module NFAStateSetSet = struct | ||
include Set.Make(NFA.StateSet) | ||
module NFAStateSetSet = struct | ||
include Set.Make(NFA.StateSet) | ||
|
||
let pp_states_set ppf s = | ||
Format.fprintf ppf "{@[%a@]}" | ||
(Format.pp_print_list ~pp_sep:NFA.StateSet.pp_comma NFA.StateSet.pp_states) (to_seq s |> List.of_seq) | ||
end | ||
let pp_states_set ppf s = | ||
Format.fprintf ppf "{@[%a@]}" | ||
(Format.pp_print_list ~pp_sep:NFA.StateSet.pp_comma NFA.StateSet.pp_states) (to_seq s |> List.of_seq) | ||
end | ||
|
||
module NFAStateSetMap = struct | ||
include Map.Make(NFA.StateSet) | ||
module NFAStateSetMap = struct | ||
include Map.Make(NFA.StateSet) | ||
|
||
let pp_kv_pair ~pp_val ppf (k,v) = | ||
Format.fprintf ppf "@[%a ->@ %a@]" NFA.StateSet.pp_states k pp_val v | ||
let pp_kv_pair ~pp_val ppf (k,v) = | ||
Format.fprintf ppf "@[%a ->@ %a@]" NFA.StateSet.pp_states k pp_val v | ||
|
||
let pp_map ~pp_val ppf map = | ||
Format.fprintf ppf "{@[%a@]}" | ||
(Format.pp_print_list ~pp_sep:NFA.StateSet.pp_comma (pp_kv_pair ~pp_val)) (to_seq map |> List.of_seq) | ||
end | ||
let pp_map ~pp_val ppf map = | ||
Format.fprintf ppf "{@[%a@]}" | ||
(Format.pp_print_list ~pp_sep:NFA.StateSet.pp_comma (pp_kv_pair ~pp_val)) (to_seq map |> List.of_seq) | ||
end | ||
|
||
module Transitions = struct | ||
include Map.Make(BitVec) | ||
module Transitions = struct | ||
include Map.Make(BitVec) | ||
|
||
let pp_kv_pair ~pp_val ppf (k,v) = | ||
Format.fprintf ppf "@[%a ->@ %a@]" BitVec.pp_bv k pp_val v | ||
let pp_kv_pair ~pp_val ppf (k,v) = | ||
Format.fprintf ppf "@[%a ->@ %a@]" BitVec.pp_bv k pp_val v | ||
|
||
let pp_map ~pp_val ppf map = | ||
Format.fprintf ppf "[@[%a@]]" | ||
(Format.pp_print_list ~pp_sep:NFA.StateSet.pp_comma (pp_kv_pair ~pp_val)) (to_seq map |> List.of_seq) | ||
end | ||
let pp_map ~pp_val ppf map = | ||
Format.fprintf ppf "[@[%a@]]" | ||
(Format.pp_print_list ~pp_sep:NFA.StateSet.pp_comma (pp_kv_pair ~pp_val)) (to_seq map |> List.of_seq) | ||
end | ||
|
||
module DFA = struct | ||
module DFA = struct | ||
|
||
type dfa = (NFA.StateSet.t Transitions.t) NFAStateSetMap.t | ||
type dfa = (NFA.StateSet.t Transitions.t) NFAStateSetMap.t | ||
|
||
let add_key ~from:(from : NFA.StateSet.t) ~dfa:(dfa : dfa) : dfa = | ||
match NFAStateSetMap.find_opt from dfa with | ||
| None -> NFAStateSetMap.add from (Transitions.empty) dfa | ||
| Some _ -> dfa | ||
|
||
let add_transition ~from:(from : NFA.StateSet.t) (bv : BitVec.t) ~to_:(to_ : NFA.StateSet.t) ~dfa:(dfa : dfa) : dfa = | ||
let dfa = | ||
let add_key ~from:(from : NFA.StateSet.t) ~dfa:(dfa : dfa) : dfa = | ||
match NFAStateSetMap.find_opt from dfa with | ||
| None -> NFAStateSetMap.add from (Transitions.singleton bv to_) dfa | ||
| Some trans -> NFAStateSetMap.add from (Transitions.add bv to_ trans) dfa | ||
in | ||
(* make sure the to_ is in the set of keys*) | ||
add_key ~from:to_ ~dfa | ||
|
||
type dula_build = | ||
{ marked : NFAStateSetSet.t | ||
; unmarked : NFAStateSetSet.t | ||
; k : int | ||
; dfa : dfa | ||
} | ||
|
||
let build_transitions (dula : dula_build) ~t = | ||
let rec build_transitions ({marked; unmarked; k; dfa} as dula) t n max = | ||
let from = t in | ||
let bv = (BitVec.Bits n) in | ||
let transition : NFA.StateSet.t = NFA.Transitions.all_transitions t bv ~k in | ||
let dfa = add_transition ~from bv ~to_:transition ~dfa in | ||
let unmarked = | ||
if NFAStateSetSet.mem transition marked || NFAStateSetSet.mem transition unmarked then | ||
unmarked | ||
| None -> NFAStateSetMap.add from (Transitions.empty) dfa | ||
| Some _ -> dfa | ||
|
||
let add_transition ~from:(from : NFA.StateSet.t) (bv : BitVec.t) ~to_:(to_ : NFA.StateSet.t) ~dfa:(dfa : dfa) : dfa = | ||
let dfa = | ||
match NFAStateSetMap.find_opt from dfa with | ||
| None -> NFAStateSetMap.add from (Transitions.singleton bv to_) dfa | ||
| Some trans -> NFAStateSetMap.add from (Transitions.add bv to_ trans) dfa | ||
in | ||
(* make sure the to_ is in the set of keys*) | ||
add_key ~from:to_ ~dfa | ||
|
||
type dula_build = | ||
{ marked : NFAStateSetSet.t | ||
; unmarked : NFAStateSetSet.t | ||
; k : int | ||
; dfa : dfa | ||
} | ||
|
||
let build_transitions (dula : dula_build) ~t = | ||
let rec build_transitions ({marked; unmarked; k; dfa} as dula) t n max = | ||
let from = t in | ||
let bv = (BitVec.Bits n) in | ||
let transition : NFA.StateSet.t = NFA.Transitions.all_transitions t bv ~k in | ||
let dfa = add_transition ~from bv ~to_:transition ~dfa in | ||
let unmarked = | ||
if NFAStateSetSet.mem transition marked || NFAStateSetSet.mem transition unmarked then | ||
unmarked | ||
else | ||
NFAStateSetSet.add transition unmarked | ||
in | ||
let dula = { dula with dfa; unmarked } in | ||
if n = max then | ||
dula | ||
else | ||
NFAStateSetSet.add transition unmarked | ||
build_transitions dula t (n + 1) max | ||
in | ||
let dula = { dula with dfa; unmarked } in | ||
if n = max then | ||
dula | ||
else | ||
build_transitions dula t (n + 1) max | ||
in | ||
let BitVec.(Bits max) = | ||
BitVec.ones ~m:(dula.k * 2 + 1) | ||
in | ||
build_transitions dula t 0 max | ||
|
||
let rec build_dfa ({marked; unmarked; k = _; dfa = _} as dula) = | ||
match NFAStateSetSet.max_elt_opt unmarked with | ||
| None -> dula | ||
| Some t -> | ||
let marked = NFAStateSetSet.add t marked in | ||
let unmarked = NFAStateSetSet.remove t unmarked in | ||
let dula = | ||
build_transitions { dula with marked; unmarked } ~t | ||
let BitVec.(Bits max) = | ||
BitVec.ones ~m:(dula.k * 2 + 1) | ||
in | ||
build_dfa dula | ||
|
||
let start = NFAStateSetSet.of_list [NFA.StateSet.singleton (Lane 0, Err 0);NFA.StateSet.empty] | ||
|
||
let build_dula ~k = | ||
if (k < 1) || k > 3 then | ||
failwith "build_dula can only be called with 1 <= k <= 3" | ||
else | ||
build_dfa { marked = NFAStateSetSet.empty; unmarked = start; k; dfa = NFAStateSetMap.empty } | ||
build_transitions dula t 0 max | ||
|
||
let rec build_dfa ({marked; unmarked; k = _; dfa = _} as dula) = | ||
match NFAStateSetSet.max_elt_opt unmarked with | ||
| None -> dula | ||
| Some t -> | ||
let marked = NFAStateSetSet.add t marked in | ||
let unmarked = NFAStateSetSet.remove t unmarked in | ||
let dula = | ||
build_transitions { dula with marked; unmarked } ~t | ||
in | ||
build_dfa dula | ||
|
||
let start = NFAStateSetSet.of_list [NFA.StateSet.start;NFA.StateSet.err] | ||
|
||
let build_dula ~k = | ||
if (k < 1) || k > 3 then | ||
failwith "build_dula can only be called with 1 <= k <= 3" | ||
else | ||
build_dfa { marked = NFAStateSetSet.empty; unmarked = start; k; dfa = NFAStateSetMap.empty } | ||
|
||
let build_and_print_dula ~k = | ||
let {dfa;_} = build_dula ~k in | ||
NFAStateSetMap.pp_map ~pp_val:(Transitions.pp_map ~pp_val:NFA.StateSet.pp_states) Format.std_formatter dfa; | ||
Format.pp_print_newline Format.std_formatter () | ||
let build_and_print_dula ~k = | ||
let {dfa;_} = build_dula ~k in | ||
NFAStateSetMap.pp_map ~pp_val:(Transitions.pp_map ~pp_val:NFA.StateSet.pp_states) Format.std_formatter dfa; | ||
Format.pp_print_newline Format.std_formatter () | ||
end | ||
end |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,63 @@ | ||
module BV = BitVec | ||
|
||
type states = States of (BV.t array) * (BV.t array) | ||
|
||
module StateSet = struct | ||
type t = states | ||
|
||
let start ~k : t = | ||
let arr = Array.make (k + 1) BV.zero in | ||
(* Using k + 1 just to keep things simple *) | ||
let trans = Array.make (k + 1) BV.zero in | ||
let init = BV.snoc_zeros ~m:k (BV.one) in | ||
arr.(0) <- init; | ||
States (arr, trans) | ||
|
||
let _find_index ~f arr : int option = | ||
let rec find_index f arr n len = | ||
if n < len then | ||
begin if f arr.(n) then | ||
Some n | ||
else | ||
find_index f arr (n + 1) len | ||
end | ||
else | ||
None | ||
in | ||
find_index f arr 0 (Array.length arr) | ||
|
||
let min_cost_opt (States (arr,_)) : int option = | ||
_find_index ~f:(fun bv -> BV.non_zero bv) arr | ||
|
||
|
||
let pp_states ppf (States (arr,trans)) = | ||
Format.fprintf ppf | ||
"@[states@ @[%a@]@ transpose @[%a@]@]" | ||
(Format.pp_print_list ~pp_sep:(fun ppf () -> Format.pp_print_char ppf '|') BV.pp_bv) (Array.to_list arr) | ||
(Format.pp_print_list ~pp_sep:(fun ppf () -> Format.pp_print_char ppf '|') BV.pp_bv) (Array.to_list trans) | ||
end | ||
|
||
module Transitions = struct | ||
|
||
let all_transitions (States (input, trans) : StateSet.t) bv ~k : StateSet.t = | ||
let output = Array.make (k + 1) BV.zero in | ||
let out_trans = Array.make (k + 1) BV.zero in | ||
let del_mask = ref BV.zero in | ||
let prev = ref BV.zero in | ||
for i = 0 to k do | ||
let prev_bv = !prev in | ||
let ins_subs = (BV.logor (BV.shift_left prev_bv 1) prev_bv) in | ||
let dels = BV.logand bv !del_mask in | ||
let transpose_transitions = BV.shift_right_logical (BV.logand bv trans.(i)) 1 in | ||
let prev_transitions = BV.logor ins_subs dels in | ||
let self_transitions = BV.logand bv input.(i) in | ||
let transitions = BV.logor (BV.logor prev_transitions self_transitions) transpose_transitions in | ||
let transpose_intermediate = BV.shift_left (BV.logand bv (BV.shift_right_logical prev_bv 1)) 2 in | ||
del_mask := BV.logor (BV.shift_right_logical input.(i) 1) (BV.shift_right_logical !del_mask 1); | ||
prev := input.(i); | ||
out_trans.(i) <- transpose_intermediate; | ||
output.(i) <- transitions | ||
done; | ||
States (output, out_trans) | ||
|
||
end |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,51 @@ | ||
module BV = BitVec | ||
|
||
type states = States of (BV.t array) [@@unboxed] | ||
|
||
module StateSet = struct | ||
type t = states | ||
|
||
let start ~k : t = | ||
let arr = Array.make (k + 1) BV.zero in | ||
let init = BV.snoc_zeros ~m:k (BV.one) in | ||
arr.(0) <- init; | ||
States arr | ||
|
||
let _find_index ~f arr : int option = | ||
let rec find_index f arr n len = | ||
if n < len then | ||
begin if f arr.(n) then | ||
Some n | ||
else | ||
find_index f arr (n + 1) len | ||
end | ||
else | ||
None | ||
in | ||
find_index f arr 0 (Array.length arr) | ||
|
||
let min_cost_opt (States arr) : int option = | ||
_find_index ~f:(fun bv -> BV.non_zero bv) arr | ||
|
||
end | ||
|
||
module Transitions = struct | ||
|
||
let all_transitions (States input : StateSet.t) bv ~k : StateSet.t = | ||
let output = Array.make (k + 1) BV.zero in | ||
let del_mask = ref BV.zero in | ||
let prev = ref BV.zero in | ||
for i = 0 to k do | ||
let prev_bv = !prev in | ||
let ins_subs = (BV.logor (BV.shift_left prev_bv 1) prev_bv) in | ||
let dels = BV.logand bv !del_mask in | ||
let prev_transitions = BV.logor ins_subs dels in | ||
let self_transitions = BV.logand bv input.(i) in | ||
let transitions = BV.logor prev_transitions self_transitions in | ||
del_mask := BV.logor (BV.shift_right_logical input.(i) 1) (BV.shift_right_logical !del_mask 1); | ||
prev := input.(i); | ||
output.(i) <- transitions | ||
done; | ||
States output | ||
|
||
end |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,18 @@ | ||
module type NFA_t = sig | ||
module State : sig | ||
type t | ||
val compare : t -> t -> int | ||
end | ||
module StateSet : sig | ||
include Set.S with type elt = State.t | ||
|
||
val start : t | ||
val err : t | ||
|
||
val pp_comma : Format.formatter -> unit -> unit | ||
val pp_states : Format.formatter -> t -> unit | ||
end | ||
module Transitions : sig | ||
val all_transitions : StateSet.t -> BitVec.t -> k:int -> StateSet.t | ||
end | ||
end |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.