Unverified Commit 2c8322c1 authored by Merlin's avatar Merlin 💧
Browse files


parent e58aece4
......@@ -575,22 +575,11 @@ let oneStepSat_MultiModalK (u: bset list) sv =
let (sort, v) = sv in
let boxes = bsetFilter v (fun lf -> (lfGetType sort lf) = AxF) in
let diamonds = bsetFilter v (fun lf -> (lfGetType sort lf) = ExF) in
let boxargsByRel = (*Array of Tuples, where first arg is relation and second are all formulae under a box of that kind*)
let boxRels = bsetMap (lfGetDest3 sort) boxes in
let boxargsForRel rel = bsetFilter boxes (fun r -> (lfGetDest3 sort r) = rel) in
Array.map (fun rel -> (rel, boxargsForRel rel)) boxRels
(*Make reduced U for each relation, thus List of tupels of relation and reduced U*)
(*Make reduced U. Will be applied for each relation*)
let redU args = List.filter (fun bs -> bsetIsSubOrEqual args bs) u in
let reducedU = Array.map (fun (rel, boxargs) -> (rel, redU boxargs)) boxargsByRel in
(*check if reducedU contains formula for every diamond per relation*)
let existsInU rel lf =
let cands = match List.assoc_opt rel (Array.to_list reducedU) with
| None -> u
| Some uc -> uc
List.exists (fun bs -> bsetMem bs lf) cands
let existsInU rel lf = List.exists (fun bs -> bsetMem bs lf) (redU (boxargsForRel rel)) in
bsetForall diamonds (fun lf -> existsInU (lfGetDest3 sort lf) (lfGetDest1 sort lf))
let rec oneStepGMLRec counters sort v currentU =
Supports Markdown
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