Not simplifier dependency inversion

kore/src/Kore/Builtin/KEqual.hs

@@ -147,7 +147,8 @@ evalKEq true (valid :< app) =
 
         defined1 <- Ceil.makeEvaluate sideCondition pattern1
         defined2 <- Ceil.makeEvaluate sideCondition pattern2
-        defined <- And.simplifyEvaluated sideCondition defined1 defined2
+        defined <-
+            And.simplifyEvaluated Not.notSimplifier sideCondition defined1 defined2
 
         equalTerms <-
             Equals.makeEvaluateTermsToPredicate
@@ -162,7 +163,8 @@ evalKEq true (valid :< app) =
             falsePatterns = Pattern.withCondition falseTerm <$> notEqualTerms
 
         let undefinedResults = Or.simplifyEvaluated truePatterns falsePatterns
-        results <- And.simplifyEvaluated sideCondition defined undefinedResults
+        results <-
+            And.simplifyEvaluated Not.notSimplifier sideCondition defined undefinedResults
         pure $ Applied AttemptedAxiomResults
             { results
             , remainders = OrPattern.bottom

kore/src/Kore/Repl/Data.hs

@@ -88,8 +88,9 @@ import Kore.Profiler.Data
     ( MonadProfiler
     )
 import Kore.Step.Simplification.Data
-    ( MonadSimplify
+    ( MonadSimplify (..)
     )
+import qualified Kore.Step.Simplification.Not as Not
 import qualified Kore.Step.Strategy as Strategy
 import Kore.Strategies.Goal
 import Kore.Strategies.Verification
@@ -494,14 +495,24 @@ deriving instance MonadSMT m => MonadSMT (UnifierWithExplanation m)
 
 deriving instance MonadProfiler m => MonadProfiler (UnifierWithExplanation m)
 
+instance MonadTrans UnifierWithExplanation where
+    lift = UnifierWithExplanation . lift . lift
+    {-# INLINE lift #-}
+
 instance MonadLog m => MonadLog (UnifierWithExplanation m) where
     logEntry entry = UnifierWithExplanation $ logEntry entry
     {-# INLINE logEntry #-}
     logWhile entry ma =
         UnifierWithExplanation $ logWhile entry (getUnifierWithExplanation ma)
     {-# INLINE logWhile #-}
 
-deriving instance MonadSimplify m => MonadSimplify (UnifierWithExplanation m)
+instance MonadSimplify m => MonadSimplify (UnifierWithExplanation m) where
+    localSimplifierTermLike locally (UnifierWithExplanation unifierT) =
+        UnifierWithExplanation
+        $ localSimplifierTermLike locally unifierT
+    localSimplifierAxioms locally (UnifierWithExplanation unifierT) =
+        UnifierWithExplanation
+        $ localSimplifierAxioms locally unifierT
 
 instance MonadSimplify m => MonadUnify (UnifierWithExplanation m) where
     throwUnificationError =
@@ -570,7 +581,7 @@ runUnifierWithExplanation (UnifierWithExplanation unifier) =
     unificationResults =
         fmap (\(r, ex) -> flip (,) ex <$> r)
         . flip runAccumT mempty
-        . Monad.Unify.runUnifierT
+        . Monad.Unify.runUnifierT Not.notSimplifier
         $ unifier
     explainError = Left . makeAuxReplOutput . show . Pretty.pretty
     failWithExplanation

kore/src/Kore/Step/Search.hs

@@ -55,6 +55,7 @@ import qualified Kore.Internal.Pattern as Conditional
 import Kore.Internal.SideCondition
     ( SideCondition
     )
+import qualified Kore.Step.Simplification.Not as Not
 import Kore.Step.Simplification.Simplify
 import qualified Kore.Step.SMT.Evaluator as SMT.Evaluator
     ( evaluate
@@ -138,7 +139,7 @@ matchWith
     -> MaybeT m (OrCondition variable)
 matchWith sideCondition e1 e2 = do
     eitherUnifiers <-
-        lift $ Unifier.runUnifierT
+        lift $ Unifier.runUnifierT Not.notSimplifier
         $ unificationProcedureWorker sideCondition t1 t2
     let
         maybeUnifiers :: Maybe [Condition variable]

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

@@ -19,8 +19,7 @@ module Kore.Step.Simplification.And
 import Prelude.Kore
 
 import Control.Error
-    ( fromMaybe
-    , runMaybeT
+    ( runMaybeT
     )
 import Control.Monad
     ( foldM
@@ -111,13 +110,12 @@ import qualified Kore.Internal.TermLike as TermLike
 import Kore.Step.Simplification.AndTerms
     ( maybeTermAnd
     )
+import Kore.Step.Simplification.NotSimplifier
 import Kore.Step.Simplification.Simplify
 import qualified Kore.Step.Substitution as Substitution
 import Kore.Unification.UnifierT
-    ( runUnifierT
-    )
-import Kore.Unification.Unify
-    ( MonadUnify
+    ( UnifierT (..)
+    , runUnifierT
     )
 import Kore.Unparser
     ( unparse
@@ -164,12 +162,14 @@ Also, we have
     the same for two string literals and two chars
 -}
 simplify
-    :: (InternalVariable variable, MonadSimplify simplifier)
-    => SideCondition variable
+    :: InternalVariable variable
+    => MonadSimplify simplifier
+    => NotSimplifier (UnifierT simplifier)
+    -> SideCondition variable
     -> And Sort (OrPattern variable)
     -> simplifier (OrPattern variable)
-simplify sideCondition And { andFirst = first, andSecond = second } =
-    simplifyEvaluated sideCondition first second
+simplify notSimplifier sideCondition And { andFirst = first, andSecond = second } =
+    simplifyEvaluated notSimplifier sideCondition first second
 
 {-| simplifies an And given its two 'OrPattern' children.
 
@@ -189,12 +189,14 @@ to carry around.
 
 -}
 simplifyEvaluated
-    :: (InternalVariable variable, MonadSimplify simplifier)
-    => SideCondition variable
+    :: InternalVariable variable
+    => MonadSimplify simplifier
+    => NotSimplifier (UnifierT simplifier)
+    -> SideCondition variable
     -> OrPattern variable
     -> OrPattern variable
     -> simplifier (OrPattern variable)
-simplifyEvaluated sideCondition first second
+simplifyEvaluated notSimplifier sideCondition first second
   | OrPattern.isFalse first  = return OrPattern.bottom
   | OrPattern.isFalse second = return OrPattern.bottom
   | OrPattern.isTrue first   = return second
@@ -204,17 +206,19 @@ simplifyEvaluated sideCondition first second
         gather $ do
             first1 <- scatter first
             second1 <- scatter second
-            makeEvaluate sideCondition first1 second1
+            makeEvaluate notSimplifier sideCondition first1 second1
     return (OrPattern.fromPatterns result)
 
 simplifyEvaluatedMultiple
-    :: (InternalVariable variable, MonadSimplify simplifier)
-    => SideCondition variable
+    :: InternalVariable variable
+    => MonadSimplify simplifier
+    => NotSimplifier (UnifierT simplifier)
+    -> SideCondition variable
     -> [OrPattern variable]
     -> simplifier (OrPattern variable)
-simplifyEvaluatedMultiple _ [] = return OrPattern.top
-simplifyEvaluatedMultiple sideCondition (pat : patterns) =
-    foldM (simplifyEvaluated sideCondition) pat patterns
+simplifyEvaluatedMultiple _ _ [] = return OrPattern.top
+simplifyEvaluatedMultiple notSimplifier sideCondition (pat : patterns) =
+    foldM (simplifyEvaluated notSimplifier sideCondition) pat patterns
 
 {-|'makeEvaluate' simplifies an 'And' of 'Pattern's.
 
@@ -225,31 +229,34 @@ makeEvaluate
         , HasCallStack
         , MonadSimplify simplifier
         )
-    => SideCondition variable
+    => NotSimplifier (UnifierT simplifier)
+    -> SideCondition variable
     -> Pattern variable
     -> Pattern variable
     -> BranchT simplifier (Pattern variable)
-makeEvaluate sideCondition first second
+makeEvaluate notSimplifier sideCondition first second
   | Pattern.isBottom first || Pattern.isBottom second = empty
   | Pattern.isTop first = return second
   | Pattern.isTop second = return first
-  | otherwise = makeEvaluateNonBool sideCondition first second
+  | otherwise = makeEvaluateNonBool notSimplifier sideCondition first second
 
 makeEvaluateNonBool
     ::  ( InternalVariable variable
         , HasCallStack
         , MonadSimplify simplifier
         )
-    => SideCondition variable
+    => NotSimplifier (UnifierT simplifier)
+    -> SideCondition variable
     -> Pattern variable
     -> Pattern variable
     -> BranchT simplifier (Pattern variable)
 makeEvaluateNonBool
+    notSimplifier
     sideCondition
     first@Conditional { term = firstTerm }
     second@Conditional { term = secondTerm }
   = do
-    terms <- termAnd firstTerm secondTerm
+    terms <- termAnd notSimplifier firstTerm secondTerm
     let firstCondition = Conditional.withoutTerm first
         secondCondition = Conditional.withoutTerm second
         initialConditions = firstCondition <> secondCondition
@@ -433,23 +440,24 @@ The comment for 'simplify' describes all the special cases handled by this.
 -}
 termAnd
     :: forall variable simplifier
-    .  (InternalVariable variable, MonadSimplify simplifier)
+    .  InternalVariable variable
+    => MonadSimplify simplifier
     => HasCallStack
-    => TermLike variable
+    => NotSimplifier (UnifierT simplifier)
+    -> TermLike variable
     -> TermLike variable
     -> BranchT simplifier (Pattern variable)
-termAnd p1 p2 =
+termAnd notSimplifier p1 p2 =
     either (const andTerm) BranchT.scatter
-    =<< (lift . runUnifierT) (termAndWorker p1 p2)
+    =<< (lift . runUnifierT notSimplifier) (termAndWorker p1 p2)
   where
     andTerm = return $ Pattern.fromTermLike (mkAnd p1 p2)
     termAndWorker
-        :: MonadUnify unifier
-        => TermLike variable
+        :: TermLike variable
         -> TermLike variable
-        -> unifier (Pattern variable)
+        -> UnifierT simplifier (Pattern variable)
     termAndWorker first second = do
-        let maybeTermAnd' = maybeTermAnd termAndWorker first second
+        let maybeTermAnd' = maybeTermAnd notSimplifier termAndWorker first second
         patt <- runMaybeT maybeTermAnd'
         return $ fromMaybe andPattern patt
       where

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

@@ -68,6 +68,7 @@ import Kore.Step.Simplification.ExpandAlias
     )
 import Kore.Step.Simplification.InjSimplifier
 import Kore.Step.Simplification.NoConfusion
+import Kore.Step.Simplification.NotSimplifier
 import Kore.Step.Simplification.Overloading
 import Kore.Step.Simplification.SimplificationType
     ( SimplificationType
@@ -114,10 +115,11 @@ termUnification
     .  InternalVariable variable
     => MonadUnify unifier
     => HasCallStack
-    => TermLike variable
+    => NotSimplifier unifier
+    -> TermLike variable
     -> TermLike variable
     -> unifier (Pattern variable)
-termUnification =
+termUnification notSimplifier =
     termUnificationWorker
   where
     termUnificationWorker
@@ -127,7 +129,8 @@ termUnification =
     termUnificationWorker pat1 pat2 = do
         let
             maybeTermUnification :: MaybeT unifier (Pattern variable)
-            maybeTermUnification = maybeTermAnd termUnificationWorker pat1 pat2
+            maybeTermUnification =
+                maybeTermAnd notSimplifier termUnificationWorker pat1 pat2
             unsupportedPatternsError =
                 throwUnificationError
                     (unsupportedPatterns
@@ -141,32 +144,38 @@ maybeTermEquals
     :: InternalVariable variable
     => MonadUnify unifier
     => HasCallStack
-    => TermSimplifier variable unifier
+    => NotSimplifier unifier
+    -> TermSimplifier variable unifier
     -- ^ Used to simplify subterm "and".
     -> TermLike variable
     -> TermLike variable
     -> MaybeT unifier (Pattern variable)
-maybeTermEquals = maybeTransformTerm equalsFunctions
+maybeTermEquals notSimplifier =
+    maybeTransformTerm (equalsFunctions notSimplifier)
 
 maybeTermAnd
     :: InternalVariable variable
     => MonadUnify unifier
     => HasCallStack
-    => TermSimplifier variable unifier
+    => NotSimplifier unifier
+    -> TermSimplifier variable unifier
     -- ^ Used to simplify subterm "and".
     -> TermLike variable
     -> TermLike variable
     -> MaybeT unifier (Pattern variable)
-maybeTermAnd = maybeTransformTerm andFunctions
+maybeTermAnd notSimplifier =
+    maybeTransformTerm (andFunctions notSimplifier)
 
 andFunctions
     :: forall variable unifier
     .  InternalVariable variable
     => MonadUnify unifier
     => HasCallStack
-    => [TermTransformationOld variable unifier]
-andFunctions =
-    map (forAnd . snd) (filter appliesToAnd andEqualsFunctions)
+    => NotSimplifier unifier
+    -> [TermTransformationOld variable unifier]
+andFunctions notSimplifier =
+    forAnd . snd
+    <$> filter appliesToAnd (andEqualsFunctions notSimplifier)
   where
     appliesToAnd :: (SimplificationTarget, a) -> Bool
     appliesToAnd (AndT, _) = True
@@ -183,9 +192,11 @@ equalsFunctions
     .  InternalVariable variable
     => MonadUnify unifier
     => HasCallStack
-    => [TermTransformationOld variable unifier]
-equalsFunctions =
-    map (forEquals . snd) (filter appliesToEquals andEqualsFunctions)
+    => NotSimplifier unifier
+    -> [TermTransformationOld variable unifier]
+equalsFunctions notSimplifier =
+    forEquals . snd
+    <$> filter appliesToEquals (andEqualsFunctions notSimplifier)
   where
     appliesToEquals :: (SimplificationTarget, a) -> Bool
     appliesToEquals (AndT, _) = False
@@ -202,9 +213,10 @@ andEqualsFunctions
     .  InternalVariable variable
     => MonadUnify unifier
     => HasCallStack
-    => [(SimplificationTarget, TermTransformation variable unifier)]
-andEqualsFunctions = fmap mapEqualsFunctions
-    [ (AndT,    \_ _ s -> expandAlias (maybeTermAnd s), "expandAlias")
+    => NotSimplifier unifier
+    -> [(SimplificationTarget, TermTransformation variable unifier)]
+andEqualsFunctions notSimplifier = fmap mapEqualsFunctions
+    [ (AndT,    \_ _ s -> expandAlias (maybeTermAnd notSimplifier s), "expandAlias")
     , (AndT,    \_ _ _ -> boolAnd, "boolAnd")
     , (BothT,   \_ _ _ -> equalAndEquals, "equalAndEquals")
     , (BothT,   \_ _ _ -> bytesDifferent, "bytesDifferent")