From 05394431cf5cbe0e8f23e2582730c97071c0aa18 Mon Sep 17 00:00:00 2001
From: Thomas Tuegel <ttuegel@mailbox.org>
Date: Wed, 16 Jun 2021 11:21:05 -0500
Subject: [PATCH 1/2] [REF] simplifyPredicatesWithAssumptions: Return MultiAnd

---
 kore/src/Kore/Step/Simplification/Condition.hs | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/kore/src/Kore/Step/Simplification/Condition.hs b/kore/src/Kore/Step/Simplification/Condition.hs
index ed7ec60e32..f714b99170 100644
--- a/kore/src/Kore/Step/Simplification/Condition.hs
+++ b/kore/src/Kore/Step/Simplification/Condition.hs
@@ -137,12 +137,11 @@ simplifyPredicates sideCondition original = do
     let predicates =
             SideCondition.simplifyConjunctionByAssumption original
                 & fst . extract
-    simplified <-
+    simplifiedPredicates <-
         simplifyPredicatesWithAssumptions
             sideCondition
             (toList predicates)
-    let simplifiedPredicates =
-            from @(Condition _) @(MultiAnd (Predicate _)) simplified
+    let simplified = foldMap mkCondition simplifiedPredicates
     if original == simplifiedPredicates
         then return (Condition.markSimplified simplified)
         else simplifyPredicates sideCondition simplifiedPredicates
@@ -157,8 +156,8 @@ simplifyPredicatesWithAssumptions ::
     [Predicate RewritingVariableName] ->
     LogicT
         simplifier
-        (Condition RewritingVariableName)
-simplifyPredicatesWithAssumptions _ [] = return Condition.top
+        (MultiAnd (Predicate RewritingVariableName))
+simplifyPredicatesWithAssumptions _ [] = return MultiAnd.top
 simplifyPredicatesWithAssumptions sideCondition predicates@(_ : rest) = do
     let predicatesWithUnsimplified =
             zip predicates $
@@ -169,7 +168,6 @@ simplifyPredicatesWithAssumptions sideCondition predicates@(_ : rest) = do
             predicatesWithUnsimplified
         )
         MultiAnd.top
-        & fmap (foldMap mkCondition)
   where
     simplifyWithAssumptions ::
         ( Predicate RewritingVariableName

From f82bd6773db0e960d29d472d49d59738da821545 Mon Sep 17 00:00:00 2001
From: Thomas Tuegel <ttuegel@mailbox.org>
Date: Wed, 16 Jun 2021 15:00:59 -0500
Subject: [PATCH 2/2] Clean up simplifyPredicatesWithAssumptions

---
 .../src/Kore/Step/Simplification/Condition.hs | 36 ++++++++++---------
 1 file changed, 19 insertions(+), 17 deletions(-)

diff --git a/kore/src/Kore/Step/Simplification/Condition.hs b/kore/src/Kore/Step/Simplification/Condition.hs
index f714b99170..ddf6ac61e2 100644
--- a/kore/src/Kore/Step/Simplification/Condition.hs
+++ b/kore/src/Kore/Step/Simplification/Condition.hs
@@ -159,15 +159,11 @@ simplifyPredicatesWithAssumptions ::
         (MultiAnd (Predicate RewritingVariableName))
 simplifyPredicatesWithAssumptions _ [] = return MultiAnd.top
 simplifyPredicatesWithAssumptions sideCondition predicates@(_ : rest) = do
-    let predicatesWithUnsimplified =
-            zip predicates $
-                scanr ((<>) . MultiAnd.singleton) MultiAnd.top rest
-    State.execStateT
-        ( traverse_
-            simplifyWithAssumptions
-            predicatesWithUnsimplified
-        )
-        MultiAnd.top
+    let unsimplifieds =
+            map MultiAnd.singleton rest
+                & scanr (<>) MultiAnd.top
+    traverse_ simplifyWithAssumptions (zip predicates unsimplifieds)
+        & flip State.execStateT MultiAnd.top
   where
     simplifyWithAssumptions ::
         ( Predicate RewritingVariableName
@@ -178,15 +174,21 @@ simplifyPredicatesWithAssumptions sideCondition predicates@(_ : rest) = do
             (LogicT simplifier)
             ()
     simplifyWithAssumptions (predicate, unsimplifiedSideCond) = do
+        sideCondition' <- getSideCondition unsimplifiedSideCond
+        result <- simplifyPredicate sideCondition' predicate
+        putSimplifiedResult result
+
+    getSideCondition unsimplifiedSideCond = do
         simplifiedSideCond <- State.get
-        let otherSideConds =
-                SideCondition.addAssumptions
-                    (simplifiedSideCond <> unsimplifiedSideCond)
-                    sideCondition
-        result <-
-            Predicate.simplify otherSideConds predicate >>= Logic.scatter
-                & lift
-        State.put (simplifiedSideCond <> result)
+        SideCondition.addAssumptions
+            (simplifiedSideCond <> unsimplifiedSideCond)
+            sideCondition
+            & return
+
+    putSimplifiedResult result = State.modify' (<> result)
+
+    simplifyPredicate sideCondition' predicate =
+        Predicate.simplify sideCondition' predicate >>= Logic.scatter & lift
 
 mkCondition ::
     InternalVariable variable =>