Skip to content

Add SideCondition argument to simplifyAnds #1846

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
May 23, 2020
Merged

Add SideCondition argument to simplifyAnds #1846

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
0741a1b
Add SideCondition argument to simplifyAnds
andreiburdusa May 22, 2020
6882938
stylish
andreiburdusa May 22, 2020
2fad079
Addressed comments
andreiburdusa May 22, 2020
206ca8e
Merge branch 'master' into add-SideCondition-to-simplifyAnds
andreiburdusa May 23, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,6 @@ import Kore.Internal.SideCondition
)
import qualified Kore.Internal.SideCondition as SideCondition
( toRepresentation
, topTODO
)
import Kore.Internal.Substitution
( Assignment
Expand Down Expand Up @@ -180,9 +179,10 @@ simplifyAnds
, Monad monad
)
=> MakeAnd monad
-> SideCondition variable
-> NonEmpty (TermLike variable)
-> monad (Pattern variable)
simplifyAnds MakeAnd { makeAnd } (NonEmpty.sort -> patterns) =
simplifyAnds MakeAnd { makeAnd } sideCondition (NonEmpty.sort -> patterns) =
foldM simplifyAnds' Pattern.top patterns
where
simplifyAnds'
Expand All @@ -194,7 +194,6 @@ simplifyAnds MakeAnd { makeAnd } (NonEmpty.sort -> patterns) =
AndF And { andFirst, andSecond } ->
foldM simplifyAnds' intermediate [andFirst, andSecond]
_ -> do
let sideCondition = SideCondition.topTODO
simplified <-
makeAnd
intermediateTerm
Expand All @@ -211,12 +210,13 @@ deduplicateSubstitution
, Monad monad
)
=> MakeAnd monad
-> SideCondition variable
-> Substitution variable
-> monad
( Predicate variable
, Map (UnifiedVariable variable) (TermLike variable)
)
deduplicateSubstitution makeAnd' =
deduplicateSubstitution sideCondition makeAnd' =
worker Predicate.makeTruePredicate_ . checkSetVars . Substitution.toMultiMap
where
checkSetVars m
Expand All @@ -228,7 +228,7 @@ deduplicateSubstitution makeAnd' =
(\k v -> Any $ isSetVar k && isNotSingleton v)
isNotSingleton = isNothing . getSingleton

simplifyAnds' = simplifyAnds makeAnd'
simplifyAnds' = simplifyAnds sideCondition makeAnd'

worker
:: Predicate variable
Expand Down Expand Up @@ -373,7 +373,7 @@ simplifySubstitutionWorker sideCondition makeAnd' = \substitution -> do
(Map (UnifiedVariable variable) (TermLike variable))
deduplicate substitution = do
(predicate, substitution') <-
deduplicateSubstitution makeAnd' substitution
deduplicateSubstitution makeAnd' sideCondition substitution
& lift . lift
addPredicate predicate
return substitution'
Expand Down
1 change: 1 addition & 0 deletions kore/test/Test/Kore/Unification/Unifier.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -195,6 +195,7 @@ simplifyAnds
simplifyAnds =
SubstitutionSimplifier.simplifyAnds
(Unification.unificationMakeAnd Not.notSimplifier)
SideCondition.top

andSimplifySuccess
:: HasCallStack
Expand Down