runtimeverification · ana-pantilie · Mar 2, 2021 · Feb 8, 2021 · Feb 8, 2021 · Feb 10, 2021
diff --git a/kore/src/Kore/Equation/Simplification.hs b/kore/src/Kore/Equation/Simplification.hs
@@ -37,9 +37,6 @@ import Kore.Internal.Pattern
     )
 import qualified Kore.Internal.Pattern as Pattern
 import qualified Kore.Internal.Predicate as Predicate
-import qualified Kore.Internal.SideCondition as SideCondition
-    ( top
-    )
 import qualified Kore.Internal.Substitution as Substitution
 import qualified Kore.Internal.TermLike as TermLike
 import qualified Kore.Step.Simplification.Pattern as Pattern
@@ -134,4 +131,4 @@ simplifyPattern
     -> simplifier (OrPattern variable)
 simplifyPattern patt =
     Simplifier.localSimplifierAxioms (const mempty)
-    $ Pattern.simplify SideCondition.top patt
+    $ Pattern.simplify patt
diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs
@@ -92,9 +92,6 @@ import Kore.Internal.Predicate
     , makeMultipleOrPredicate
     )
 import qualified Kore.Internal.SideCondition as SideCondition
-    ( top
-    , topTODO
-    )
 import Kore.Internal.TermLike
 import Kore.Log.ErrorRewriteLoop
     ( errorRewriteLoop
@@ -224,8 +221,7 @@ exec depthLimit breadthLimit verifiedModule strategy initialTerm =
         finals <-
             getFinalConfigsOf $ do
                 initialConfig <-
-                    Pattern.simplify SideCondition.top
-                        (Pattern.fromTermLike initialTerm)
+                    Pattern.simplify (Pattern.fromTermLike initialTerm)
                     >>= Logic.scatter
                 let
                     updateQueue = \as ->
@@ -372,8 +368,7 @@ search depthLimit breadthLimit verifiedModule termLike searchPattern searchConfi
         initialized <- initializeAndSimplify verifiedModule
         let Initialized { rewriteRules } = initialized
         simplifiedPatterns <-
-            Pattern.simplify SideCondition.top
-            $ Pattern.fromTermLike termLike
+            Pattern.simplify $ Pattern.fromTermLike termLike
         let
             initialPattern =
                 case toList simplifiedPatterns of
@@ -401,7 +396,7 @@ search depthLimit breadthLimit verifiedModule termLike searchPattern searchConfi
             searchGraph
                 searchConfig
                 (match
-                    SideCondition.topTODO
+                    SideCondition.top
                     (mkRewritingPattern searchPattern)
                 )
                 executionGraph

diff --git a/kore/src/Kore/Reachability/Claim.hs b/kore/src/Kore/Reachability/Claim.hs
@@ -130,9 +130,6 @@ import Kore.Step.Simplification.Data
     )
 import qualified Kore.Step.Simplification.Exists as Exists
 import qualified Kore.Step.Simplification.Not as Not
-import Kore.Step.Simplification.OrPattern
-    ( simplifyConditionsWithSmt
-    )
 import Kore.Step.Simplification.Pattern
     ( simplifyTopConfiguration
     )
@@ -521,9 +518,9 @@ checkImplicationWorker (ClaimPattern.refreshExistentials -> claimPattern) =
                 $ from $ makeCeilPredicate leftTerm
         let configs' = MultiOr.map (definedConfig <*) removal
         stuck <-
-            simplifyConditionsWithSmt sideCondition configs'
-            >>= Logic.scatter
-            >>= Pattern.simplify sideCondition
+            Logic.scatter configs'
+            >>= Pattern.simplify
+            >>= SMT.Evaluator.filterMultiOr
             >>= Logic.scatter
         pure (examine anyUnified stuck)
     & elseImplied
@@ -552,12 +549,12 @@ checkImplicationWorker (ClaimPattern.refreshExistentials -> claimPattern) =
             unified <-
                 mkIn sort leftTerm rightTerm
                 & Pattern.fromTermLike
-                & Pattern.simplify sideCondition
+                & Pattern.simplify
                 & (>>= Logic.scatter)
             didUnify
             removed <-
                 Pattern.andCondition unified rightCondition
-                & Pattern.simplify sideCondition
+                & Pattern.simplify
                 & (>>= Logic.scatter)
             Exists.makeEvaluate sideCondition existentials removed
                 >>= Logic.scatter
@@ -626,7 +623,7 @@ simplifyRightHandSide lensClaimPattern sideCondition =
     Lens.traverseOf (lensClaimPattern . field @"right") $ \dest ->
         OrPattern.observeAllT
         $ Logic.scatter dest
-        >>= Pattern.simplify sideCondition . Pattern.requireDefined
+        >>= Pattern.makeEvaluate sideCondition . Pattern.requireDefined
         >>= SMT.Evaluator.filterMultiOr
         >>= Logic.scatter
 

diff --git a/kore/src/Kore/Step/Rule/Simplify.hs b/kore/src/Kore/Step/Rule/Simplify.hs
@@ -21,7 +21,6 @@ import Kore.Internal.MultiAnd
     ( MultiAnd
     )
 import qualified Kore.Internal.MultiAnd as MultiAnd
-import qualified Kore.Internal.OrPattern as OrPattern
 import Kore.Internal.Pattern
     ( Pattern
     )
@@ -38,7 +37,7 @@ import Kore.Rewriting.RewritingVariable
     ( RewritingVariableName
     )
 import Kore.Step.ClaimPattern
-    ( ClaimPattern (ClaimPattern)
+    ( ClaimPattern
     )
 import qualified Kore.Step.ClaimPattern as ClaimPattern
 import Kore.Step.RulePattern
@@ -100,37 +99,6 @@ instance InternalVariable variable => SimplifyRuleLHS (RulePattern variable)
                         makeAndPredicate predicate requires'
                     }
 
-instance SimplifyRuleLHS ClaimPattern
-  where
-    simplifyRuleLhs rule@(ClaimPattern _ _ _ _) = do
-        simplifiedTerms <-
-            Pattern.simplifyTopConfiguration left
-        fullySimplified <-
-            SMT.Evaluator.filterMultiOr simplifiedTerms
-        let rules =
-                setRuleLeft rule
-                <$> OrPattern.toPatterns fullySimplified
-        return (MultiAnd.make rules)
-      where
-        ClaimPattern { left } = rule
-
-        setRuleLeft
-            :: ClaimPattern
-            -> Pattern RewritingVariableName
-            -> ClaimPattern
-        setRuleLeft
-            claimPattern@ClaimPattern { left = left' }
-            patt@Conditional { substitution }
-          =
-            ClaimPattern.applySubstitution
-                substitution
-                claimPattern
-                    { ClaimPattern.left =
-                        Condition.andCondition
-                            patt
-                            (Condition.eraseConditionalTerm left')
-                    }
-
 instance SimplifyRuleLHS (RewriteRule VariableName) where
     simplifyRuleLhs =
         fmap (MultiAnd.map RewriteRule)

diff --git a/kore/src/Kore/Step/Simplification/Exists.hs b/kore/src/Kore/Step/Simplification/Exists.hs
@@ -78,7 +78,7 @@ import qualified Kore.Step.Simplification.AndPredicates as And
     ( simplifyEvaluatedMultiPredicate
     )
 import qualified Kore.Step.Simplification.Pattern as Pattern
-    ( simplify
+    ( makeEvaluate
     )
 import Kore.Step.Simplification.Simplify
 import qualified Kore.TopBottom as TopBottom
@@ -303,7 +303,7 @@ makeEvaluateBoundLeft sideCondition variable boundTerm normalized
                         $ Conditional.predicate normalized
                     }
         orPattern <-
-            lift $ Pattern.simplify sideCondition substituted
+            lift $ Pattern.makeEvaluate sideCondition substituted
         Logic.scatter (toList orPattern)
   where
     someVariableName = inject (variableName variable)

diff --git a/kore/src/Kore/Step/Simplification/Pattern.hs b/kore/src/Kore/Step/Simplification/Pattern.hs
@@ -6,13 +6,24 @@ License     : NCSA
 module Kore.Step.Simplification.Pattern
     ( simplifyTopConfiguration
     , simplify
+    , makeEvaluate
+    -- For testing
+    , simplifySideCondition
     ) where
 
 import Prelude.Kore
 
+import Control.Monad.State.Strict
+    ( StateT
+    )
+import qualified Control.Monad.State.Strict as State
 
 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.OrPattern
     ( OrPattern
     )
@@ -21,12 +32,15 @@ import Kore.Internal.Pattern
     ( Conditional (..)
     , Pattern
     )
+import Kore.Internal.Predicate
+    ( Predicate
+    )
 import Kore.Internal.SideCondition
     ( SideCondition
     )
 import qualified Kore.Internal.SideCondition as SideCondition
     ( andCondition
-    , topTODO
+    , top
     )
 import Kore.Internal.Substitution
     ( toMap
@@ -43,6 +57,7 @@ import Kore.Step.Simplification.Simplify
 import Kore.Substitute
     ( substitute
     )
+import Logic
 
 {-| Simplifies the pattern without a side-condition (i.e. it's top)
 and removes the exists quantifiers at the top.
@@ -54,7 +69,7 @@ simplifyTopConfiguration
     => Pattern variable
     -> simplifier (OrPattern variable)
 simplifyTopConfiguration patt = do
-    simplified <- simplify SideCondition.topTODO patt
+    simplified <- simplify patt
     return (OrPattern.map removeTopExists simplified)
   where
     removeTopExists :: Pattern variable -> Pattern variable
@@ -65,12 +80,24 @@ simplifyTopConfiguration patt = do
 {-| Simplifies an 'Pattern', returning an 'OrPattern'.
 -}
 simplify
+    :: InternalVariable variable
+    => MonadSimplify simplifier
+    => Pattern variable
+    -> simplifier (OrPattern variable)
+simplify = makeEvaluate SideCondition.top
+
+{- | Simplifies a 'Pattern' with a custom 'SideCondition'.
+This should only be used when it's certain that the
+'SideCondition' was not created from the 'Condition' of
+the 'Pattern'.
+ -}
+makeEvaluate
     :: InternalVariable variable
     => MonadSimplify simplifier
     => SideCondition variable
     -> Pattern variable
     -> simplifier (OrPattern variable)
-simplify sideCondition pattern' =
+makeEvaluate sideCondition pattern' =
     OrPattern.observeAllT $ do
         withSimplifiedCondition <- simplifyCondition sideCondition pattern'
         let (term, simplifiedCondition) =
@@ -89,7 +116,36 @@ simplify sideCondition pattern' =
                 & Condition.fromPredicate
             termSideCondition =
                 sideCondition `SideCondition.andCondition` simplifiedCondition'
-        simplifiedTerm <- simplifyConditionalTerm termSideCondition term'
+        simplifiedSideCondition <-
+            simplifySideCondition termSideCondition
+        simplifiedTerm <- simplifyConditionalTerm simplifiedSideCondition term'
         let simplifiedPattern =
                 Conditional.andCondition simplifiedTerm simplifiedCondition
         simplifyCondition sideCondition simplifiedPattern
+
+-- | Simplify each condition in the 'SideCondition' with the assumption that
+-- the other conditions are true.
+simplifySideCondition
+    :: forall variable simplifier
+    .  InternalVariable variable
+    => MonadSimplify simplifier
+    => SideCondition variable
+    -> LogicT simplifier (SideCondition variable)
+simplifySideCondition (toList . from @_ @(MultiAnd _) -> predicates) =
+    State.execStateT (worker predicates) SideCondition.top
+  where
+    worker
+        :: [Predicate variable]
+        -> StateT
+            (SideCondition variable)
+            (LogicT simplifier)
+            ()
+    worker [] = return ()
+    worker (pred' : rest) = do
+        sideCondition <- State.get
+        let otherConds = sideCondition <> from (MultiAnd.make rest)
+        result <-
+            simplifyCondition otherConds (Condition.fromPredicate pred')
+            & lift
+        State.put (SideCondition.andCondition sideCondition result)
+        worker rest
diff --git a/kore/src/Kore/Step/Simplification/Rule.hs b/kore/src/Kore/Step/Simplification/Rule.hs
@@ -22,9 +22,6 @@ import Kore.Internal.Predicate
     ( pattern PredicateTrue
     )
 import qualified Kore.Internal.Predicate as Predicate
-import qualified Kore.Internal.SideCondition as SideCondition
-    ( topTODO
-    )
 import qualified Kore.Internal.Substitution as Substitution
 import Kore.Internal.TermLike
     ( TermLike
@@ -144,4 +141,4 @@ simplifyPattern
     -> simplifier (OrPattern variable)
 simplifyPattern termLike =
     Simplifier.localSimplifierAxioms (const mempty)
-    $ Pattern.simplify SideCondition.topTODO (Pattern.fromTermLike termLike)
+    $ Pattern.simplify (Pattern.fromTermLike termLike)
diff --git a/kore/test/Test/Kore/Step/Axiom/Registry.hs b/kore/test/Test/Kore/Step/Axiom/Registry.hs
@@ -46,9 +46,6 @@ import qualified Kore.IndexedModule.MetadataToolsBuilder as MetadataTools
     ( build
     )
 import Kore.Internal.Pattern as Pattern
-import qualified Kore.Internal.SideCondition as SideCondition
-    ( top
-    )
 import Kore.Internal.Symbol as Symbol
 import Kore.Internal.TermLike
 import qualified Kore.Step.Axiom.Identifier as AxiomIdentifier
@@ -449,15 +446,15 @@ test_functionRegistry =
         let expect = mkApplySymbol sHead []
         simplified <-
             runSimplifier testEnv
-            $ Pattern.simplify SideCondition.top
+            $ Pattern.simplify
             $ makePattern $ mkApplySymbol gHead []
         let actual = Pattern.term $ head $ toList simplified
         assertEqual "" expect actual
     , testCase "Checking that evaluator simplifies correctly" $ do
         let expect = mkApplySymbol tHead []
         simplified <-
             runSimplifier testEnv
-            $ Pattern.simplify SideCondition.top
+            $ Pattern.simplify
             $ makePattern $ mkApplySymbol pHead []
         let actual = Pattern.term $ head $ toList simplified
         assertEqual "" expect actual

diff --git a/kore/test/Test/Kore/Step/Simplification/Integration.hs b/kore/test/Test/Kore/Step/Simplification/Integration.hs
@@ -57,7 +57,7 @@ import Kore.Step.Axiom.Registry
     ( mkEvaluatorRegistry
     )
 import qualified Kore.Step.Simplification.Pattern as Pattern
-    ( simplify
+    ( makeEvaluate
     )
 import Kore.Step.Simplification.Simplify
 
@@ -1405,7 +1405,7 @@ evaluateConditionalWithAxioms
     -> TestPattern
     -> IO OrTestPattern
 evaluateConditionalWithAxioms axioms sideCondition =
-    runSimplifierSMT env . Pattern.simplify sideCondition
+    runSimplifierSMT env . Pattern.makeEvaluate sideCondition
   where
     env = Mock.env { simplifierAxioms }
     simplifierAxioms :: BuiltinAndAxiomSimplifierMap

diff --git a/kore/test/Test/Kore/Step/Simplification/IntegrationProperty.hs b/kore/test/Test/Kore/Step/Simplification/IntegrationProperty.hs
@@ -114,9 +114,7 @@ test_regressionGeneratedTerms =
                         )
                     )
         simplified <-
-            Pattern.simplify
-                SideCondition.top
-                (Pattern.fromTermLike term)
+            Pattern.simplify (Pattern.fromTermLike term)
             & runSimplifier Mock.env
         assertEqual "" True (OrPattern.isSimplified sideRepresentation simplified)
     ]
@@ -135,7 +133,7 @@ evaluateWithAxioms
     -> Pattern VariableName
     -> SMT.NoSMT (OrPattern VariableName)
 evaluateWithAxioms axioms =
-    Simplification.runSimplifier env . Pattern.simplify SideCondition.top
+    Simplification.runSimplifier env . Pattern.simplify
   where
     env = Mock.env { simplifierAxioms }
     simplifierAxioms :: BuiltinAndAxiomSimplifierMap