Overhaul predicate simplifier

kore/kore.cabal

@@ -444,6 +444,7 @@ library
     Kore.Step.Simplification.Overloading
     Kore.Step.Simplification.OverloadSimplifier
     Kore.Step.Simplification.Pattern
+    Kore.Step.Simplification.Predicate
     Kore.Step.Simplification.Rewrites
     Kore.Step.Simplification.Rule
     Kore.Step.Simplification.SetVariable
@@ -751,6 +752,7 @@ test-suite kore-test
     Test.Kore.Step.Simplification.Or
     Test.Kore.Step.Simplification.OrPattern
     Test.Kore.Step.Simplification.Overloading
+    Test.Kore.Step.Simplification.Predicate
     Test.Kore.Step.Simplification.Pattern
     Test.Kore.Step.Simplification.Rule
     Test.Kore.Step.Simplification.StringLiteral

kore/src/Kore/Equation/Application.hs

@@ -62,6 +62,9 @@ import Kore.Internal.Condition (
     Condition,
  )
 import qualified Kore.Internal.Condition as Condition
+import Kore.Internal.OrCondition (
+    OrCondition,
+ )
 import qualified Kore.Internal.OrCondition as OrCondition
 import Kore.Internal.OrPattern (
     OrPattern,
@@ -382,16 +385,17 @@ checkRequires sideCondition predicate requires =
   where
     simplifyCondition = Simplifier.simplifyCondition sideCondition
 
-    assertBottom orCondition
-        | isBottom orCondition = done
-        | otherwise = requiresNotMet
+    assertBottom negatedImplication
+        | isBottom negatedImplication = done
+        | otherwise = requiresNotMet negatedImplication
     done = return ()
-    requiresNotMet =
+    requiresNotMet negatedImplication =
         throwE
             CheckRequiresError
                 { matchPredicate = predicate
                 , equationRequires = requires
                 , sideCondition
+                , negatedImplication
                 }
 
     -- Pair a configuration with sideCondition for evaluation by the solver.
@@ -530,6 +534,7 @@ data CheckRequiresError variable = CheckRequiresError
     { matchPredicate :: !(Predicate variable)
     , equationRequires :: !(Predicate variable)
     , sideCondition :: !(SideCondition variable)
+    , negatedImplication :: !(OrCondition variable)
     }
     deriving stock (Eq, Ord, Show)
     deriving stock (GHC.Generic)
@@ -539,16 +544,22 @@ data CheckRequiresError variable = CheckRequiresError
 instance Pretty (CheckRequiresError RewritingVariableName) where
     pretty checkRequiresError =
         Pretty.vsep
-            [ "could not infer the equation requirement:"
+            [ "Could not infer the equation requirement:"
             , Pretty.indent 4 (pretty equationRequires)
             , "and the matching requirement:"
             , Pretty.indent 4 (pretty matchPredicate)
             , "from the side condition:"
             , Pretty.indent 4 (pretty sideCondition)
+            , "The negated implication is:"
+            , Pretty.indent 4 (pretty negatedImplication)
             ]
       where
-        CheckRequiresError{matchPredicate, equationRequires, sideCondition} =
-            checkRequiresError
+        CheckRequiresError
+            { matchPredicate
+            , equationRequires
+            , sideCondition
+            , negatedImplication
+            } = checkRequiresError
 
 -- * Logging
 

kore/src/Kore/Internal/MultiAnd.hs

@@ -20,6 +20,9 @@ module Kore.Internal.MultiAnd (
     singleton,
     map,
     traverse,
+    distributeAnd,
+    traverseOr,
+    traverseOrAnd,
 ) where
 
 import qualified Data.Functor.Foldable as Recursive
@@ -35,6 +38,10 @@ import Kore.Attribute.Pattern.FreeVariables (
 import Kore.Internal.Condition (
     Condition,
  )
+import Kore.Internal.MultiOr (
+    MultiOr,
+ )
+import qualified Kore.Internal.MultiOr as MultiOr
 import Kore.Internal.Predicate (
     Predicate,
     getMultiAndPredicate,
@@ -49,6 +56,7 @@ import Kore.Internal.Variable
 import Kore.TopBottom (
     TopBottom (..),
  )
+import qualified Logic
 import Prelude.Kore hiding (
     map,
     traverse,
@@ -251,3 +259,32 @@ traverse ::
     f (MultiAnd child2)
 traverse f = fmap make . Traversable.traverse f . toList
 {-# INLINE traverse #-}
+
+distributeAnd ::
+    Ord term =>
+    TopBottom term =>
+    MultiAnd (MultiOr term) ->
+    MultiOr (MultiAnd term)
+distributeAnd multiAnd =
+    MultiOr.observeAll $ traverse Logic.scatter multiAnd
+{-# INLINE distributeAnd #-}
+
+traverseOr ::
+    Ord child2 =>
+    TopBottom child2 =>
+    Applicative f =>
+    (child1 -> f (MultiOr child2)) ->
+    MultiAnd child1 ->
+    f (MultiOr (MultiAnd child2))
+traverseOr f = fmap distributeAnd . traverse f
+{-# INLINE traverseOr #-}
+
+traverseOrAnd ::
+    Ord child2 =>
+    TopBottom child2 =>
+    Applicative f =>
+    (child1 -> f (MultiOr (MultiAnd child2))) ->
+    MultiOr (MultiAnd child1) ->
+    f (MultiOr (MultiAnd child2))
+traverseOrAnd f = MultiOr.traverseOr (fmap (MultiOr.map fold) . traverseOr f)
+{-# INLINE traverseOrAnd #-}

kore/src/Kore/Internal/MultiOr.hs

@@ -15,7 +15,6 @@ module Kore.Internal.MultiOr (
     bottom,
     filterOr,
     flatten,
-    distributeAnd,
     distributeApplication,
     gather,
     observeAllT,
@@ -26,6 +25,7 @@ module Kore.Internal.MultiOr (
     singleton,
     map,
     traverse,
+    traverseOr,
 
     -- * Re-exports
     Alternative (..),
@@ -43,10 +43,6 @@ import GHC.Exts (
 import qualified GHC.Generics as GHC
 import qualified Generics.SOP as SOP
 import Kore.Debug
-import Kore.Internal.MultiAnd (
-    MultiAnd,
- )
-import qualified Kore.Internal.MultiAnd as MultiAnd
 import Kore.Syntax.Application (
     Application (..),
  )
@@ -162,17 +158,6 @@ singleton term
     | isBottom term = MultiOr []
     | otherwise = MultiOr [term]
 
-distributeAnd ::
-    Ord term =>
-    TopBottom term =>
-    MultiAnd (MultiOr term) ->
-    MultiOr (MultiAnd term)
-distributeAnd =
-    foldr (crossProductGeneric and') (singleton MultiAnd.top)
-  where
-    and' term ma =
-        MultiAnd.singleton term <> ma
-
 distributeApplication ::
     Ord head =>
     Ord term =>
@@ -343,3 +328,14 @@ traverse ::
     f (MultiOr child2)
 traverse f = fmap make . Traversable.traverse f . toList
 {-# INLINE traverse #-}
+
+-- | Traverse a @MultiOr@ using an action that returns a disjunction.
+traverseOr ::
+    Ord child2 =>
+    TopBottom child2 =>
+    Applicative f =>
+    (child1 -> f (MultiOr child2)) ->
+    MultiOr child1 ->
+    f (MultiOr child2)
+traverseOr f = fmap fold . traverse f
+{-# INLINE traverseOr #-}

kore/src/Kore/Internal/Predicate.hs

@@ -254,6 +254,10 @@ instance From (Iff () child) (PredicateF variable child) where
     from = IffF
     {-# INLINE from #-}
 
+instance From (Not () child) (PredicateF variable child) where
+    from = NotF
+    {-# INLINE from #-}
+
 newtype Predicate variable = Predicate
     { getPredicate ::
         Cofree (PredicateF variable) (PredicatePattern variable)

kore/src/Kore/Internal/Substitution.hs

@@ -13,6 +13,7 @@ module Kore.Internal.Substitution (
     assignedVariable,
     assignedTerm,
     mapAssignedTerm,
+    retractAssignment,
     singleSubstitutionToPredicate,
     UnwrappedSubstitution,
     mkUnwrappedSubstitution,
@@ -68,6 +69,7 @@ import qualified Kore.Attribute.Pattern.Simplified as Attribute (
 import Kore.Debug
 import Kore.Internal.Predicate (
     Predicate,
+    pattern PredicateEquals,
  )
 import qualified Kore.Internal.Predicate as Predicate
 import qualified Kore.Internal.SideCondition.SideCondition as SideCondition (
@@ -155,6 +157,20 @@ mkUnwrappedSubstitution ::
     [Assignment variable]
 mkUnwrappedSubstitution = fmap (uncurry assign)
 
+{- | Extract an 'Assignment' from a 'Predicate' of the proper form.
+
+Returns 'Nothing' if the 'Predicate' is not in the correct form.
+-}
+retractAssignment ::
+    InternalVariable variable =>
+    Predicate variable ->
+    Maybe (Assignment variable)
+retractAssignment (PredicateEquals (Var_ var) term) =
+    Just (assign var term)
+retractAssignment (PredicateEquals term (Var_ var)) =
+    Just (assign var term)
+retractAssignment _ = Nothing
+
 {- | @Substitution@ represents a collection @[xᵢ=φᵢ]@ of substitutions.
 
 Individual substitutions are a pair of type

kore/src/Kore/Step/SMT/Evaluator.hs

@@ -33,6 +33,7 @@ import qualified Kore.Attribute.Symbol as Attribute (
 import Kore.IndexedModule.MetadataTools (
     SmtMetadataTools,
  )
+import qualified Kore.Internal.Condition as Condition
 import Kore.Internal.Conditional (
     Conditional,
  )
@@ -120,7 +121,9 @@ instance
     where
     evaluate (sideCondition, conditional) =
         assert (Conditional.isNormalized conditional) $
-            evaluate (sideCondition, Conditional.predicate conditional)
+            evaluate (sideCondition, Condition.toPredicate condition)
+      where
+        condition = Conditional.withoutTerm conditional
 
 -- | Removes all branches refuted by an external SMT solver.
 filterBranch ::

kore/src/Kore/Step/Simplification/AndPredicates.hs

@@ -15,6 +15,7 @@ import qualified Kore.Internal.Condition as Condition
 import Kore.Internal.MultiAnd (
     MultiAnd,
  )
+import qualified Kore.Internal.MultiAnd as MultiAnd
 import qualified Kore.Internal.MultiOr as MultiOr
 import Kore.Internal.OrCondition (
     OrCondition,
@@ -38,10 +39,9 @@ simplifyEvaluatedMultiPredicate ::
     SideCondition RewritingVariableName ->
     MultiAnd (OrCondition RewritingVariableName) ->
     simplifier (OrCondition RewritingVariableName)
-simplifyEvaluatedMultiPredicate sideCondition predicates = do
-    let crossProduct = MultiOr.distributeAnd predicates
+simplifyEvaluatedMultiPredicate sideCondition predicates =
     MultiOr.observeAllT $ do
-        element <- LogicT.scatter crossProduct
+        element <- MultiAnd.traverse LogicT.scatter predicates
         andConditions element
   where
     andConditions predicates' =