Skip to content
GitLab
Menu
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Software
COOL
Commits
18e54fbc
Unverified
Commit
18e54fbc
authored
May 17, 2022
by
Merlin
💧
Browse files
Refactoring and Dest2 > Dest3 for role
parent
4e809722
Pipeline
#14771
waiting for manual action with stages
Changes
1
Pipelines
2
Show whitespace changes
Inline
Sidebyside
lib/src/CoAlgLogics.ml
View file @
18e54fbc
...
...
@@ 573,28 +573,25 @@ let mkRule_Fusion sort bs focus sl : stateExpander =
let
oneStepSat_MultiModalK
(
u
:
bset
list
)
sv
=
let
(
sort
,
v
)
=
sv
in
(*Filter for relations*)
let
boxargsForRels
=
(*List of Tuples, where first arg is relation and second are all formulae under a box of that kind*)
let
boxes
=
(
bsetFilter
v
(
fun
lf
>
(
lfGetType
sort
lf
)
=
AxF
))
in
let
boxRels
=
Array
.
to_list
(
bsetMap
(
lfGetDest2
sort
)
boxes
)
in
let
getRelBoxargsTupleForOneRel
rel
=
rel
,
(
bsetFilter
boxes
(
fun
r
>
(
lfGetDest2
sort
r
)
=
rel
))
in
let
res
=
List
.
map
getRelBoxargsTupleForOneRel
boxRels
in
res
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
in
(*Make reduced U for each relation, thus List of tupels of relation and reduced U*)
let
red
ucedU
=
List
.
map
(
fun
(
rel
,
boxargs
)
>
(
rel
,
List
.
filter
(
fun
bs
>
bsetIsSubOrEqual
box
args
bs
)
u
))
boxargsForRels
in
(*Make List of tupels of diamond formulae and their respective relation*)
let
diamonds
=
bsetFilter
v
(
fun
lf
>
(
lfGetType
sort
lf
)
=
ExF
)
in
let
diaRels
=
Array
.
to_list
(
bsetMap
(
lfGetDest2
sort
)
diamonds
)
in
let
diaargs
=
Array
.
to_list
(
bsetMap
(
lfGetDest1
sort
)
diamonds
)
in
let
diaTuples
=
List
.
combine
diaRels
diaargs
in
(*check if redU contains formula for every diamond per relation*)
let
existsInU
(
rel
,
lf
)
=
List
.
exists
(
fun
bs
>
bsetMem
bs
lf
)
(
List
.
assoc
rel
reducedU
)
in
let
res
=
List
.
for_all
existsInU
diaTuples
in
re
s
let
red
U
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
in
List
.
exists
(
fun
bs
>
bsetMem
bs
lf
)
cands
in
Array
.
for_all
(
fun
lf
>
existsInU
(
lfGetDest3
sort
lf
)
(
lfGetDest1
sort
lf
))
diamond
s
let
rec
oneStepGMLRec
counters
sort
v
currentU
=
let
isExceedingBox
lf
=
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment