From ebfcc36a5a879182244b6cb404e8f2e99b725360 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Mon, 26 Jul 2021 15:18:57 +0300 Subject: [PATCH 1/4] Overhaul Predicate simplifier: Equals, v2 --- kore/src/Kore/Simplify/Equals.hs | 2 +- kore/src/Kore/Simplify/Predicate.hs | 14 ++++++++++++++ 2 files changed, 15 insertions(+), 1 deletion(-) diff --git a/kore/src/Kore/Simplify/Equals.hs b/kore/src/Kore/Simplify/Equals.hs index 79eac812a6..e02f5984cd 100644 --- a/kore/src/Kore/Simplify/Equals.hs +++ b/kore/src/Kore/Simplify/Equals.hs @@ -159,7 +159,7 @@ Equals(a and b, b and a) will not be evaluated to Top. simplify :: MonadSimplify simplifier => SideCondition RewritingVariableName -> - Equals Sort (OrPattern RewritingVariableName) -> + Equals sort (OrPattern RewritingVariableName) -> simplifier (OrCondition RewritingVariableName) simplify sideCondition Equals{equalsFirst = first, equalsSecond = second} = simplifyEvaluated sideCondition first' second' diff --git a/kore/src/Kore/Simplify/Predicate.hs b/kore/src/Kore/Simplify/Predicate.hs index f821d63259..e745ef73b3 100644 --- a/kore/src/Kore/Simplify/Predicate.hs +++ b/kore/src/Kore/Simplify/Predicate.hs @@ -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.Not as Not import Kore.Simplify.Simplify import Kore.Substitute @@ -63,6 +64,7 @@ import Kore.Syntax ( And (..), Bottom (..), Ceil (..), + Equals (..), Exists (..), Floor (..), Forall (Forall), @@ -178,6 +180,8 @@ simplify sideCondition original = ForallF forallF -> traverse worker (Forall.refreshForall avoid forallF) >>= simplifyForall sideCondition + EqualsF equalsF -> + simplifyEquals sideCondition =<< traverse simplifyTerm equalsF _ -> simplifyPredicateTODO sideCondition predicate & MultiOr.observeAllT where _ :< predicateF = Recursive.project predicate @@ -522,3 +526,13 @@ extractFirstAssignment someVariableName predicates = guard (TermLike.isFunctionPattern termLike) (guard . not) (someVariableName `occursIn` termLike) pure termLike + +simplifyEquals :: + forall simplifier sort. + MonadSimplify simplifier => + SideCondition RewritingVariableName -> + Equals sort (OrPattern RewritingVariableName) -> + simplifier NormalForm +simplifyEquals sideCondition = + Equals.simplify sideCondition + >=> return . MultiOr.map (from @(Condition _)) From e3f6c5aaa4418282bdbf8e25b069122f9dd1c550 Mon Sep 17 00:00:00 2001 From: github-actions Date: Mon, 26 Jul 2021 12:21:20 +0000 Subject: [PATCH 2/4] Format with fourmolu --- kore/src/Kore/Simplify/Predicate.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/src/Kore/Simplify/Predicate.hs b/kore/src/Kore/Simplify/Predicate.hs index e745ef73b3..66d68f7ef1 100644 --- a/kore/src/Kore/Simplify/Predicate.hs +++ b/kore/src/Kore/Simplify/Predicate.hs @@ -535,4 +535,4 @@ simplifyEquals :: simplifier NormalForm simplifyEquals sideCondition = Equals.simplify sideCondition - >=> return . MultiOr.map (from @(Condition _)) + >=> return . MultiOr.map (from @(Condition _)) From 609eed00baeeef33b218fe61c1e3e9e176892e7b Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Wed, 28 Jul 2021 12:36:33 +0300 Subject: [PATCH 3/4] Add sort info to simplifyEquals --- kore/src/Kore/Simplify/Equals.hs | 2 +- kore/src/Kore/Simplify/Predicate.hs | 24 ++++++++++++++++++------ 2 files changed, 19 insertions(+), 7 deletions(-) diff --git a/kore/src/Kore/Simplify/Equals.hs b/kore/src/Kore/Simplify/Equals.hs index e02f5984cd..79eac812a6 100644 --- a/kore/src/Kore/Simplify/Equals.hs +++ b/kore/src/Kore/Simplify/Equals.hs @@ -159,7 +159,7 @@ Equals(a and b, b and a) will not be evaluated to Top. simplify :: MonadSimplify simplifier => SideCondition RewritingVariableName -> - Equals sort (OrPattern RewritingVariableName) -> + Equals Sort (OrPattern RewritingVariableName) -> simplifier (OrCondition RewritingVariableName) simplify sideCondition Equals{equalsFirst = first, equalsSecond = second} = simplifyEvaluated sideCondition first' second' diff --git a/kore/src/Kore/Simplify/Predicate.hs b/kore/src/Kore/Simplify/Predicate.hs index 66d68f7ef1..41d1e9406d 100644 --- a/kore/src/Kore/Simplify/Predicate.hs +++ b/kore/src/Kore/Simplify/Predicate.hs @@ -47,7 +47,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, @@ -73,6 +76,7 @@ import Kore.Syntax ( Not (..), Or (..), SomeVariableName, + Sort, Top (..), variableName, ) @@ -180,8 +184,9 @@ simplify sideCondition original = ForallF forallF -> traverse worker (Forall.refreshForall avoid forallF) >>= simplifyForall sideCondition - EqualsF equalsF -> - simplifyEquals sideCondition =<< traverse simplifyTerm equalsF + EqualsF equalsF@(Equals _ _ term _) -> + simplifyEquals sideCondition (termLikeSort term) + =<< traverse simplifyTerm equalsF _ -> simplifyPredicateTODO sideCondition predicate & MultiOr.observeAllT where _ :< predicateF = Recursive.project predicate @@ -531,8 +536,15 @@ simplifyEquals :: forall simplifier sort. MonadSimplify simplifier => SideCondition RewritingVariableName -> + Sort -> Equals sort (OrPattern RewritingVariableName) -> simplifier NormalForm -simplifyEquals sideCondition = - Equals.simplify sideCondition - >=> return . MultiOr.map (from @(Condition _)) +simplifyEquals sideCondition sort equals = + Equals.simplify sideCondition equals' + >>= return . MultiOr.map (from @(Condition _)) + where + equals' = + equals + { equalsOperandSort = sort + , equalsResultSort = sort + } From 9ebc57d504a23ea58ad0616443400e6f0e85d9b1 Mon Sep 17 00:00:00 2001 From: ana-pantilie Date: Thu, 29 Jul 2021 10:44:27 +0300 Subject: [PATCH 4/4] Address review comment --- kore/src/Kore/Simplify/Predicate.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/src/Kore/Simplify/Predicate.hs b/kore/src/Kore/Simplify/Predicate.hs index 9e5e492e19..453948ff73 100644 --- a/kore/src/Kore/Simplify/Predicate.hs +++ b/kore/src/Kore/Simplify/Predicate.hs @@ -506,7 +506,7 @@ simplifyEquals :: simplifier NormalForm simplifyEquals sideCondition sort equals = Equals.simplify sideCondition equals' - >>= return . MultiOr.map (from @(Condition _)) + <&> MultiOr.map (from @(Condition _)) where equals' = equals