Remove Kore.Internal.SideCondition.andCondition

kore/src/Kore/Internal/SideCondition.hs

@@ -162,11 +162,12 @@ andCondition
     -> Condition variable
     -> SideCondition variable
 andCondition SideCondition {assumedTrue} newCondition =
-    SideCondition
+    assert (isNormalized result) result
+  where
+    result = SideCondition
         { representation = toRepresentationCondition merged
         , assumedTrue = merged
         }
-  where
     merged = assumedTrue `Condition.andCondition` newCondition
 
 assumeTrueCondition

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

@@ -27,6 +27,9 @@ import qualified Kore.Internal.SideCondition as SideCondition
     ( andCondition
     , topTODO
     )
+import Kore.Internal.Substitution
+    ( toMap
+    )
 import Kore.Internal.TermLike
     ( pattern Exists_
     )
@@ -36,6 +39,9 @@ import Kore.Step.Simplification.Simplify
     , simplifyCondition
     , simplifyConditionalTermToOr
     )
+import Kore.Substitute
+    ( substitute
+    )
 
 {-| Simplifies the pattern without a side-condition (i.e. it's top)
 and removes the exists quantifiers at the top.
@@ -68,9 +74,10 @@ simplify sideCondition pattern' =
         withSimplifiedCondition <- simplifyCondition sideCondition pattern'
         let (term, simplifiedCondition) =
                 Conditional.splitTerm withSimplifiedCondition
+            term' = substitute (toMap $ substitution simplifiedCondition) term
             termSideCondition =
                 sideCondition `SideCondition.andCondition` simplifiedCondition
-        orSimplifiedTerms <- simplifyConditionalTermToOr termSideCondition term
+        orSimplifiedTerms <- simplifyConditionalTermToOr termSideCondition term'
         simplifiedTerm <- Branch.scatter orSimplifiedTerms
         simplifyCondition
             sideCondition

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

@@ -74,8 +74,7 @@ import Kore.Internal.SideCondition
     ( SideCondition
     )
 import qualified Kore.Internal.SideCondition as SideCondition
-    ( andCondition
-    , toRepresentation
+    ( toRepresentation
     , topTODO
     )
 import Kore.Internal.Substitution
@@ -195,9 +194,7 @@ simplifyAnds MakeAnd { makeAnd } (NonEmpty.sort -> patterns) =
             AndF And { andFirst, andSecond } ->
                 foldM simplifyAnds' intermediate [andFirst, andSecond]
             _ -> do
-                let sideCondition =
-                        SideCondition.topTODO
-                        `SideCondition.andCondition` intermediateCondition
+                let sideCondition = SideCondition.topTODO
                 simplified <-
                     makeAnd
                         intermediateTerm

kore/src/Kore/Unification/Procedure.hs

@@ -26,9 +26,6 @@ import qualified Kore.Internal.Pattern as Conditional
 import Kore.Internal.SideCondition
     ( SideCondition
     )
-import qualified Kore.Internal.SideCondition as SideCondition
-    ( andCondition
-    )
 import Kore.Internal.TermLike
 import Kore.Log.InfoAttemptUnification
     ( infoAttemptUnification
@@ -75,9 +72,7 @@ unificationProcedureWorker sideCondition p1 p2
     pat <- termUnification Not.notSimplifier p1 p2
     TopBottom.guardAgainstBottom pat
     let (term, conditions) = Conditional.splitTerm pat
-        mergedSideCondition =
-            sideCondition `SideCondition.andCondition` conditions
-    orCeil <- Ceil.makeEvaluateTerm mergedSideCondition term
+    orCeil <- Ceil.makeEvaluateTerm sideCondition term
     ceil' <- Monad.Unify.scatter orCeil
     BranchT.alternate . simplifyCondition sideCondition
         $ Conditional.andCondition ceil' conditions

kore/test/Test/Kore/Strategies/OnePath/Step.hs

@@ -80,6 +80,7 @@ import Kore.Syntax.Module
 import Kore.Syntax.Variable
     ( Variable (..)
     )
+import Kore.Variables.UnifiedVariable
 
 import qualified Test.Kore.Step.MockSymbols as Mock
 import Test.Kore.Step.Simplification
@@ -749,34 +750,37 @@ test_onePathStrategy =
         -- Coinductive axiom: -
         -- Normal axiom: -
         -- Expected: stuck, since the terms unify but the conditions do not
-        let goal =
-                makeOnePathRuleFromPatterns
-                    ( Conditional
-                        { term = TermLike.mkElemVar Mock.x
-                        , predicate =
-                            makeEqualsPredicate Mock.testSort
-                                (TermLike.mkElemVar Mock.x)
-                                Mock.a
-                        , substitution = mempty
-                        }
+        let left =
+                Pattern.withCondition
+                    (TermLike.mkElemVar Mock.x)
+                    (Condition.fromPredicate
+                        (makeEqualsPredicate Mock.testSort
+                            (TermLike.mkElemVar Mock.x)
+                            Mock.a
+                        )
                     )
-                    ( Conditional
-                        { term = TermLike.mkElemVar Mock.x
-                        , predicate =
-                            makeNotPredicate
-                                $ makeEqualsPredicate Mock.testSort
-                                    (TermLike.mkElemVar Mock.x)
-                                    Mock.a
-                        , substitution = mempty
-                        }
+            left' =
+                Pattern.withCondition
+                    Mock.a
+                    (Condition.assign (ElemVar Mock.x) Mock.a)
+            right =
+                Pattern.withCondition
+                    (TermLike.mkElemVar Mock.x)
+                    (Condition.fromPredicate $ makeNotPredicate
+                        (makeEqualsPredicate Mock.testSort
+                            (TermLike.mkElemVar Mock.x)
+                            Mock.a
+                        )
                     )
+            original = makeOnePathRuleFromPatterns left right
+            expect = makeOnePathRuleFromPatterns left' right
         [ _actual ] <- runOnePathSteps
             Unlimited
             (Limit 1)
-            goal
+            original
             []
             []
-        assertEqual "" (ProofState.GoalStuck goal) _actual
+        assertEqual "" (ProofState.GoalStuck expect) _actual
     ]
 
 simpleRewrite
@@ -847,7 +851,11 @@ runSteps breadthLimit graphFilter picker configuration strategy' =
         give metadataTools
             $ declareSMTLemmas
             $ indexedModuleWithDefaultImports (ModuleName "TestModule") Nothing
-        runStrategy breadthLimit transitionRule strategy' (ProofState.Goal configuration)
+        runStrategy
+            breadthLimit
+            transitionRule
+            strategy'
+            (ProofState.Goal configuration)
   where
     mockEnv = Mock.env
     Env {metadataTools} = mockEnv