Make SideCondition a MultiAnd of Predicate (#2282)

Co-authored-by: Thomas Tuegel <[email protected]> Co-authored-by: Thomas Tuegel <[email protected]>
runtimeverification · Nov 25, 2020 · 6a07860 · 6a07860
1 parent 6f89cee
commit 6a07860
Show file tree

Hide file tree

Showing 5 changed files with 92 additions and 123 deletions.
diff --git a/kore/src/Kore/Internal/MultiAnd.hs b/kore/src/Kore/Internal/MultiAnd.hs
@@ -38,8 +38,14 @@ import qualified Data.Traversable as Traversable
 import qualified Generics.SOP as SOP
 import qualified GHC.Exts as GHC
 import qualified GHC.Generics as GHC
+import Kore.Attribute.Pattern.FreeVariables
+    ( HasFreeVariables (..)
+    )
 
 import Debug
+import Kore.Internal.Condition
+    ( Condition
+    )
 import Kore.Internal.Predicate
     ( Predicate
     , getMultiAndPredicate
@@ -83,6 +89,11 @@ instance TopBottom child => TopBottom (MultiAnd child) where
     isBottom (MultiAnd [child]) = isBottom child
     isBottom _ = False
 
+instance (Ord variable, HasFreeVariables a variable) =>
+    HasFreeVariables (MultiAnd a) variable
+  where
+    freeVariables = foldMap' freeVariables
+
 instance Debug child => Debug (MultiAnd child)
 
 instance (Debug child, Diff child) => Diff (MultiAnd child)
@@ -109,6 +120,13 @@ instance
     from = fromPredicate
     {-# INLINE from #-}
 
+instance
+    InternalVariable variable
+    => From (Condition variable) (MultiAnd (Predicate variable))
+  where
+    from = fromPredicate . from @_ @(Predicate _)
+    {-# INLINE from #-}
+
 instance
     InternalVariable variable
     => From (TermLike variable) (MultiAnd (TermLike variable))

diff --git a/kore/src/Kore/Internal/SideCondition.hs b/kore/src/Kore/Internal/SideCondition.hs
@@ -17,7 +17,6 @@ module Kore.Internal.SideCondition
     , top
     , topTODO
     , toPredicate
-    , isNormalized
     , toRepresentation
     ) where
 
@@ -37,10 +36,14 @@ import Kore.Internal.Condition
     ( Condition
     )
 import qualified Kore.Internal.Condition as Condition
-import qualified Kore.Internal.Conditional as Conditional
+import Kore.Internal.MultiAnd
+    ( MultiAnd
+    )
+import qualified Kore.Internal.MultiAnd as MultiAnd
 import Kore.Internal.Predicate
     ( Predicate
     )
+import qualified Kore.Internal.Predicate as Predicate
 import Kore.Internal.SideCondition.SideCondition as SideCondition
 import Kore.Internal.Variable
     ( InternalVariable
@@ -65,10 +68,11 @@ other purposes, say, to remove redundant parts of the result predicate.
 -}
 newtype SideCondition variable =
     SideCondition
-        { assumedTrue :: Condition variable
+        { assumedTrue :: MultiAnd (Predicate variable)
         }
     deriving (Eq, Ord, Show)
     deriving (GHC.Generic)
+    deriving newtype (Semigroup, Monoid)
     deriving anyclass (Hashable, NFData)
     deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
     deriving anyclass (Debug)
@@ -91,97 +95,112 @@ instance TopBottom (SideCondition variable) where
       where
         SideCondition {assumedTrue} = sideCondition
 
-instance InternalVariable variable
-    => HasFreeVariables (SideCondition variable) variable
+instance Ord variable => HasFreeVariables (SideCondition variable) variable
   where
-    freeVariables sideCondition@(SideCondition _) =
-        freeVariables assumedTrue
-      where
-        SideCondition {assumedTrue} = sideCondition
+    freeVariables (SideCondition multiAnd) =
+        freeVariables multiAnd
 
 instance InternalVariable variable => Unparse (SideCondition variable) where
-    unparse sideCondition@(SideCondition _) =
-        unparse assumedTrue
-      where
-        SideCondition {assumedTrue} = sideCondition
-
-    unparse2 sideCondition@(SideCondition _) =
-        unparse2 assumedTrue
-      where
-        SideCondition {assumedTrue} = sideCondition
+    unparse = unparse . toPredicate
+    unparse2 = unparse2 . toPredicate
 
-instance From (Condition variable) (SideCondition variable)
+instance From (SideCondition variable) (MultiAnd (Predicate variable))
   where
-      from = SideCondition
+    from condition@(SideCondition _) = assumedTrue condition
+    {-# INLINE from #-}
 
-instance From (SideCondition variable) (Condition variable) where
-    from = assumedTrue
+instance From (MultiAnd (Predicate variable)) (SideCondition variable)
+  where
+    from = SideCondition
     {-# INLINE from #-}
 
 instance
     InternalVariable variable
     => From (SideCondition variable) (Predicate variable)
   where
-    from = from @(Condition variable) . from @(SideCondition variable)
+    from = toPredicate
     {-# INLINE from #-}
 
 instance
     InternalVariable variable
     => From (Predicate variable) (SideCondition variable)
   where
-    from = from @(Condition variable) . from @(Predicate variable)
+    from = fromPredicate
+    {-# INLINE from #-}
+
+instance InternalVariable variable =>
+    From (Condition variable) (SideCondition variable)
+  where
+    from = fromCondition
+    {-# INLINE from #-}
+
+instance InternalVariable variable =>
+    From (SideCondition variable) (Condition variable)
+  where
+    from = Condition.fromPredicate . toPredicate
     {-# INLINE from #-}
 
-top :: InternalVariable variable => SideCondition variable
-top = fromCondition Condition.top
+top :: SideCondition variable
+top = SideCondition MultiAnd.top
 
 -- | A 'top' 'Condition' for refactoring which should eventually be removed.
-topTODO :: InternalVariable variable => SideCondition variable
+topTODO :: SideCondition variable
 topTODO = top
 
 andCondition
     :: InternalVariable variable
     => SideCondition variable
     -> Condition variable
     -> SideCondition variable
-andCondition SideCondition { assumedTrue } newCondition =
-    SideCondition merged
-  where
-    merged = assumedTrue `Condition.andCondition` newCondition
+andCondition
+    sideCondition
+    (from @(Condition _) @(SideCondition _) -> newSideCondition)
+  =
+    newSideCondition <> sideCondition
 
-assumeTrueCondition :: Condition variable -> SideCondition variable
+assumeTrueCondition
+    :: InternalVariable variable
+    => Condition variable
+    -> SideCondition variable
 assumeTrueCondition = fromCondition
 
 assumeTruePredicate
-    :: InternalVariable variable => Predicate variable -> SideCondition variable
-assumeTruePredicate predicate =
-    assumeTrueCondition (Condition.fromPredicate predicate)
+    :: InternalVariable variable
+    => Predicate variable
+    -> SideCondition variable
+assumeTruePredicate = fromPredicate
 
 toPredicate
     :: InternalVariable variable
     => SideCondition variable
     -> Predicate variable
 toPredicate condition@(SideCondition _) =
-    Condition.toPredicate assumedTrue
+    MultiAnd.toPredicate assumedTrue
   where
     SideCondition { assumedTrue } = condition
 
+fromPredicate
+    :: InternalVariable variable
+    => Predicate variable
+    -> SideCondition variable
+fromPredicate = SideCondition . MultiAnd.fromPredicate
+
 mapVariables
     :: (InternalVariable variable1, InternalVariable variable2)
     => AdjSomeVariableName (variable1 -> variable2)
     -> SideCondition variable1
     -> SideCondition variable2
 mapVariables adj condition@(SideCondition _) =
-    fromCondition (Condition.mapVariables adj assumedTrue)
+    MultiAnd.map (Predicate.mapVariables adj) assumedTrue
+    & SideCondition
   where
     SideCondition { assumedTrue } = condition
 
-fromCondition :: Condition variable -> SideCondition variable
-fromCondition = from
-
-fromPredicate
-    :: InternalVariable variable => Predicate variable -> SideCondition variable
-fromPredicate = fromCondition . from
+fromCondition
+    :: InternalVariable variable
+    => Condition variable
+    -> SideCondition variable
+fromCondition = fromPredicate . Condition.toPredicate
 
 toRepresentation
     :: InternalVariable variable
@@ -190,6 +209,3 @@ toRepresentation
 toRepresentation =
     mkRepresentation
     . mapVariables @_ @VariableName (pure toVariableName)
-
-isNormalized :: forall variable. Ord variable => SideCondition variable -> Bool
-isNormalized = Conditional.isNormalized . from @_ @(Condition variable)
diff --git a/kore/test/Test/Kore/Step/Rule/Simplify.hs b/kore/test/Test/Kore/Step/Rule/Simplify.hs
@@ -8,9 +8,6 @@ import Prelude.Kore
 
 import Test.Tasty
 
-import Control.Applicative
-    ( ZipList (..)
-    )
 import qualified Control.Lens as Lens
 import Control.Monad.Morph
     ( MFunctor (..)
@@ -28,11 +25,8 @@ import Data.Generics.Product
 
 import Kore.Internal.Condition
     ( Condition
-    , Conditional (..)
     )
 import qualified Kore.Internal.Condition as Condition
-import qualified Kore.Internal.MultiAnd as MultiAnd
-import qualified Kore.Internal.MultiOr as MultiOr
 import qualified Kore.Internal.OrPattern as OrPattern
 import qualified Kore.Internal.Pattern as Pattern
 import Kore.Internal.Predicate
@@ -45,7 +39,6 @@ import Kore.Internal.Predicate
     )
 import qualified Kore.Internal.Predicate as Predicate
 import qualified Kore.Internal.SideCondition as SideCondition
-import qualified Kore.Internal.Substitution as Substitution
 import Kore.Internal.TermLike
     ( AdjSomeVariableName
     , InternalVariable
@@ -65,9 +58,6 @@ import Kore.Rewriting.RewritingVariable
     ( RewritingVariableName
     , getRewritingVariable
     )
-import Kore.Sort
-    ( predicateSort
-    )
 import Kore.Step.ClaimPattern
     ( ClaimPattern (..)
     , mkClaimPattern
@@ -465,13 +455,7 @@ test_simplifyClaimRule =
         -- Test simplifyClaimRule through the OnePathClaim instance.
         testCase name $ do
             actual <- run (simplifyRuleLhs input) & fmap toList
-            -- Equivalent under associativity of \\and
-            let checkEquivalence
-                    (fmap getOnePathClaim -> claims1)
-                    (fmap getOnePathClaim -> claims2)
-                  =
-                    and (areEquivalent <$> ZipList claims1 <*> ZipList claims2)
-            assertEqual "" True (checkEquivalence expect actual)
+            assertEqual "" expect actual
       where
         run =
             runSimplifierSMT env
@@ -517,15 +501,9 @@ instance MonadSimplify m => MonadSimplify (TestSimplifierT m) where
                     (Condition.toPredicate requires)
                     (makeCeilPredicate sort leftTerm)
                 & liftPredicate
-                & Predicate.coerceSort predicateSort
                 & Condition.fromPredicate
                 & SideCondition.fromCondition
-            -- Equivalent under associativity of \\and
-            checkEquivalence cond1 cond2 =
-                (==)
-                    (cond1 & SideCondition.toPredicate & MultiAnd.fromPredicate)
-                    (cond2 & SideCondition.toPredicate & MultiAnd.fromPredicate)
-            satisfied = checkEquivalence sideCondition expectSideCondition
+            satisfied = sideCondition == expectSideCondition
         return
             . OrPattern.fromTermLike
             . (if satisfied then applyReplacements replacements else id)
@@ -569,46 +547,3 @@ instance MonadSimplify m => MonadSimplify (TestSimplifierT m) where
             => AdjSomeVariableName (RewritingVariableName -> variable)
         liftRewritingVariable =
             pure (.) <*> pure fromVariableName <*> getRewritingVariable
-
--- | The terms of the implication are equivalent in respect to
--- the associativity, commutativity, and idempotence of \\and.
---
--- Warning: this should only be used when the distinction between the
--- predicate and substitution of a pattern is not of importance.
-areEquivalent
-    :: ClaimPattern
-    -> ClaimPattern
-    -> Bool
-areEquivalent
-    ClaimPattern
-        { left = left1
-        , right = right1
-        , existentials = existentials1
-        , attributes = attributes1
-        }
-    ClaimPattern
-        { left = left2
-        , right = right2
-        , existentials = existentials2
-        , attributes = attributes2
-        }
-  =
-    let leftsAreEquivalent =
-            toConjunctionOfTerms left1
-            == toConjunctionOfTerms left2
-        rightsAreEquivalent =
-            MultiOr.map toConjunctionOfTerms right1
-            == MultiOr.map toConjunctionOfTerms right2
-     in leftsAreEquivalent
-        && rightsAreEquivalent
-        && existentials1 == existentials2
-        && attributes1 == attributes2
-  where
-    toConjunctionOfTerms Conditional { term, predicate, substitution } =
-        MultiAnd.fromTermLike term
-        <> MultiAnd.fromTermLike (Predicate.unwrapPredicate predicate)
-        <> MultiAnd.fromTermLike
-            ( Predicate.unwrapPredicate
-            . Substitution.toPredicate
-            $ substitution
-            )
diff --git a/test/issue-1872/1.test.out.golden b/test/issue-1872/1.test.out.golden
@@ -1,7 +1,7 @@
     #Not ( {
-      1
-    #Equals
       'QuesUnds'0 %Int 2
+    #Equals
+      1
     } )
   #And
     <generatedTop>
@@ -23,7 +23,7 @@
     </generatedTop>
   #And
     {
-      1
-    #Equals
       'QuesUnds'0 %Int 2
+    #Equals
+      1
     }