From 224ac0517efb4c053cbcfd3e80a76497ef8667a8 Mon Sep 17 00:00:00 2001
From: dopamane <dwc1295@gmail.com>
Date: Mon, 21 Jun 2021 06:52:20 -0700
Subject: [PATCH 1/3] first draft, remove toPattern, replace with \and and
 \implies

---
 kore/src/Kore/Step/Simplification/Iff.hs | 20 ++++++++++++++++----
 1 file changed, 16 insertions(+), 4 deletions(-)

diff --git a/kore/src/Kore/Step/Simplification/Iff.hs b/kore/src/Kore/Step/Simplification/Iff.hs
index abd04e6f88..25a159ce06 100644
--- a/kore/src/Kore/Step/Simplification/Iff.hs
+++ b/kore/src/Kore/Step/Simplification/Iff.hs
@@ -13,6 +13,7 @@ module Kore.Step.Simplification.Iff (
     simplifyEvaluated,
 ) where
 
+import qualified Kore.Internal.MultiAnd as MultiAnd
 import Kore.Internal.OrPattern (
     OrPattern,
  )
@@ -30,8 +31,15 @@ import qualified Kore.Internal.TermLike as TermLike (
 import Kore.Rewriting.RewritingVariable (
     RewritingVariableName,
  )
+import qualified Kore.Step.Simplification.And as And (
+    makeEvaluate,
+ )
+import qualified Kore.Step.Simplification.Implies as Implies (
+    simplifyEvaluated,
+ )
 import qualified Kore.Step.Simplification.Not as Not (
     makeEvaluate,
+    notSimplifier,
     simplifyEvaluated,
  )
 import Kore.Step.Simplification.Simplify
@@ -86,10 +94,14 @@ simplifyEvaluated
         | otherwise =
             return $ case (firstPatterns, secondPatterns) of
                 ([firstP], [secondP]) -> makeEvaluate firstP secondP
-                _ ->
-                    makeEvaluate
-                        (OrPattern.toPattern first)
-                        (OrPattern.toPattern second)
+                _ -> do
+                    fwd <- Implies.simplifyEvaluated sideCondition first second
+                    bwd <- Implies.simplifyEvaluated sideCondition second first
+                    And.makeEvaluate
+                        Not.notSimplifier
+                        sideCondition
+                        (MultiAnd.make [fwd, bwd])
+                        & OrPattern.observeAllT
       where
         firstPatterns = toList first
         secondPatterns = toList second

From a70fb7d1bc95be3b430415c86dad6ca524a2c3d4 Mon Sep 17 00:00:00 2001
From: dopamane <dwc1295@gmail.com>
Date: Mon, 21 Jun 2021 11:06:51 -0700
Subject: [PATCH 2/3] typechecks, use And.simplify

---
 kore/src/Kore/Step/Simplification/Iff.hs | 22 ++++++++++------------
 1 file changed, 10 insertions(+), 12 deletions(-)

diff --git a/kore/src/Kore/Step/Simplification/Iff.hs b/kore/src/Kore/Step/Simplification/Iff.hs
index 25a159ce06..f9356fb4ef 100644
--- a/kore/src/Kore/Step/Simplification/Iff.hs
+++ b/kore/src/Kore/Step/Simplification/Iff.hs
@@ -32,7 +32,7 @@ import Kore.Rewriting.RewritingVariable (
     RewritingVariableName,
  )
 import qualified Kore.Step.Simplification.And as And (
-    makeEvaluate,
+    simplify,
  )
 import qualified Kore.Step.Simplification.Implies as Implies (
     simplifyEvaluated,
@@ -91,17 +91,15 @@ simplifyEvaluated
         | OrPattern.isFalse first = Not.simplifyEvaluated sideCondition second
         | OrPattern.isTrue second = return first
         | OrPattern.isFalse second = Not.simplifyEvaluated sideCondition first
-        | otherwise =
-            return $ case (firstPatterns, secondPatterns) of
-                ([firstP], [secondP]) -> makeEvaluate firstP secondP
-                _ -> do
-                    fwd <- Implies.simplifyEvaluated sideCondition first second
-                    bwd <- Implies.simplifyEvaluated sideCondition second first
-                    And.makeEvaluate
-                        Not.notSimplifier
-                        sideCondition
-                        (MultiAnd.make [fwd, bwd])
-                        & OrPattern.observeAllT
+        | otherwise = case (firstPatterns, secondPatterns) of
+            ([firstP], [secondP]) -> return $ makeEvaluate firstP secondP
+            _ -> do
+                fwd <- Implies.simplifyEvaluated sideCondition first second
+                bwd <- Implies.simplifyEvaluated sideCondition second first
+                And.simplify
+                    Not.notSimplifier
+                    sideCondition
+                    (MultiAnd.make [fwd, bwd])
       where
         firstPatterns = toList first
         secondPatterns = toList second

From 85c56856da1040db7a691454e218d2b3d1243cd1 Mon Sep 17 00:00:00 2001
From: dopamane <dwc1295@gmail.com>
Date: Tue, 22 Jun 2021 11:36:14 -0700
Subject: [PATCH 3/3] update Or-to-pattern test

---
 kore/test/Test/Kore/Step/Simplification/Integration.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/kore/test/Test/Kore/Step/Simplification/Integration.hs b/kore/test/Test/Kore/Step/Simplification/Integration.hs
index 4b6f8d4aee..1ef3f12c4b 100644
--- a/kore/test/Test/Kore/Step/Simplification/Integration.hs
+++ b/kore/test/Test/Kore/Step/Simplification/Integration.hs
@@ -558,7 +558,7 @@ test_simplificationIntegration =
                 )
                     [ [fromNot cfCeil, fromNot chCeil]
                     , [chCeil, cgCeil, cfCeil]
-                    , [chCeil, cfCeil]
+                    , [chCeil, cfCeil, fromNot cgCeil]
                     ]
             cfCeil = makeCeilPredicate Mock.cf
             cgCeil = makeCeilPredicate Mock.cg