Skip to content

Overhaul Predicate simplifier: Equals, v2 #2766

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 6 commits into from
Jul 29, 2021
Merged

Overhaul Predicate simplifier: Equals, v2 #2766

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
ebfcc36
Overhaul Predicate simplifier: Equals, v2
ana-pantilie Jul 26, 2021
e3f6c5a
Format with fourmolu
invalid-email-address Jul 26, 2021
609eed0
Add sort info to simplifyEquals
ana-pantilie Jul 28, 2021
d36de5a
Merge remote-tracking branch 'origin/master' into overhaul-predicate-…
ana-pantilie Jul 28, 2021
9ebc57d
Address review comment
ana-pantilie Jul 29, 2021
56adf0d
Merge branch 'master' into overhaul-predicate-equals-2
ana-pantilie Jul 29, 2021
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
67 changes: 27 additions & 40 deletions kore/src/Kore/Simplify/Predicate.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,6 @@ import Kore.Attribute.Pattern.FreeVariables (
freeVariableNames,
occursIn,
)
import qualified Kore.Internal.Conditional as Conditional
import Kore.Internal.From
import Kore.Internal.MultiAnd (
MultiAnd,
Expand All @@ -29,11 +28,9 @@ import qualified Kore.Internal.MultiOr as MultiOr
import Kore.Internal.OrPattern (
OrPattern,
)
import qualified Kore.Internal.OrPattern as OrPattern
import Kore.Internal.Pattern (
Condition,
)
import qualified Kore.Internal.Pattern as Pattern
import Kore.Internal.Predicate (
Predicate,
PredicateF (..),
Expand All @@ -47,7 +44,10 @@ import Kore.Internal.Substitution (
pattern UnorderedAssignment,
)
import qualified Kore.Internal.Substitution as Substitution
import Kore.Internal.TermLike (TermLike)
import Kore.Internal.TermLike (
TermLike,
termLikeSort,
)
import qualified Kore.Internal.TermLike as TermLike
import Kore.Log.WarnUnsimplifiedPredicate (
warnUnsimplifiedPredicate,
Expand All @@ -56,6 +56,7 @@ import Kore.Rewrite.RewritingVariable (
RewritingVariableName,
)
import qualified Kore.Simplify.Ceil as Ceil
import qualified Kore.Simplify.Equals as Equals
import qualified Kore.Simplify.In as In
import qualified Kore.Simplify.Not as Not
import Kore.Simplify.Simplify
Expand All @@ -64,6 +65,7 @@ import Kore.Syntax (
And (..),
Bottom (..),
Ceil (..),
Equals (..),
Exists (..),
Floor (..),
Forall (Forall),
Expand All @@ -73,47 +75,14 @@ import Kore.Syntax (
Not (..),
Or (..),
SomeVariableName,
Sort,
Top (..),
variableName,
)
import qualified Kore.Syntax.Exists as Exists
import qualified Kore.Syntax.Forall as Forall
import qualified Kore.TopBottom as TopBottom
import Kore.Unparser
import Logic
import Prelude.Kore
import qualified Pretty

{- | Simplify the 'Predicate' once.

@simplifyPredicate@ does not attempt to apply the resulting substitution and
re-simplify the result.

See also: 'simplify'
-}
simplifyPredicateTODO ::
( HasCallStack
, MonadSimplify simplifier
) =>
SideCondition RewritingVariableName ->
Predicate RewritingVariableName ->
LogicT simplifier (MultiAnd (Predicate RewritingVariableName))
simplifyPredicateTODO sideCondition predicate = do
patternOr <-
simplifyTermLike sideCondition (Predicate.fromPredicate_ predicate)
& lift
-- Despite using lift above, we do not need to
-- explicitly check for \bottom because patternOr is an OrPattern.
from @(Condition _) @(MultiAnd (Predicate _)) <$> scatter (OrPattern.map eraseTerm patternOr)
where
eraseTerm conditional
| TopBottom.isTop (Pattern.term conditional) =
Conditional.withoutTerm conditional
| otherwise =
(error . show . Pretty.vsep)
[ "Expecting a \\top term, but found:"
, unparse conditional
]

{- | @NormalForm@ is the normal form result of simplifying 'Predicate'.
The primary purpose of this form is to transmit to the external solver.
Expand All @@ -124,7 +93,6 @@ type NormalForm = MultiOr (MultiAnd (Predicate RewritingVariableName))

simplify ::
forall simplifier.
HasCallStack =>
MonadSimplify simplifier =>
SideCondition RewritingVariableName ->
Predicate RewritingVariableName ->
Expand Down Expand Up @@ -180,9 +148,11 @@ simplify sideCondition original =
ForallF forallF ->
traverse worker (Forall.refreshForall avoid forallF)
>>= simplifyForall sideCondition
EqualsF equalsF@(Equals _ _ term _) ->
simplifyEquals sideCondition (termLikeSort term)
=<< traverse simplifyTerm equalsF
InF inF ->
simplifyIn sideCondition =<< traverse simplifyTerm inF
_ -> simplifyPredicateTODO sideCondition predicate & MultiOr.observeAllT
where
_ :< predicateF = Recursive.project predicate
~avoid = freeVariableNames sideCondition
Copy link
Contributor

@JKTKops JKTKops Jul 28, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Aren't where bindings lazy by default? What is this ~ for?

This line wasn't changed, but asking anyway while we're here.

Copy link
Contributor Author

@ana-pantilie ana-pantilie Jul 29, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We have Strict on by default, maybe this changes the behavior? I don't know for certain, though.

Expand Down Expand Up @@ -527,6 +497,23 @@ extractFirstAssignment someVariableName predicates =
(guard . not) (someVariableName `occursIn` termLike)
pure termLike

simplifyEquals ::
forall simplifier sort.
MonadSimplify simplifier =>
SideCondition RewritingVariableName ->
Sort ->
Equals sort (OrPattern RewritingVariableName) ->
simplifier NormalForm
simplifyEquals sideCondition sort equals =
Equals.simplify sideCondition equals'
<&> MultiOr.map (from @(Condition _))
where
equals' =
equals
{ equalsOperandSort = sort
, equalsResultSort = sort
}

simplifyIn ::
MonadSimplify simplifier =>
SideCondition RewritingVariableName ->
Expand Down
2 changes: 0 additions & 2 deletions kore/src/Kore/Simplify/Predicate.hs-boot
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,6 @@ import Kore.Rewrite.RewritingVariable (
RewritingVariableName,
)
import Kore.Simplify.Simplify
import Prelude.Kore

-- TODO (thomas.tuegel): Remove this file when the TermLike simplifier no longer
-- depends on the Condition simplifier.
Expand All @@ -31,7 +30,6 @@ type NormalForm = MultiOr (MultiAnd (Predicate RewritingVariableName))

simplify ::
forall simplifier.
HasCallStack =>
MonadSimplify simplifier =>
SideCondition RewritingVariableName ->
Predicate RewritingVariableName ->
Expand Down