From fdcb21ad65d6b03edae527d3958f0f44fff2c5dd Mon Sep 17 00:00:00 2001
From: ana-pantilie <ana.pantilie95@gmail.com>
Date: Wed, 21 Jul 2021 16:24:54 +0300
Subject: [PATCH 1/3] Overhaul Predicate simplifier: In simplifier

---
 kore/src/Kore/Simplify/Predicate.hs       | 12 ++++++++++
 kore/test/Test/Kore/Simplify/Predicate.hs | 29 +++++++++++++++++++++++
 2 files changed, 41 insertions(+)

diff --git a/kore/src/Kore/Simplify/Predicate.hs b/kore/src/Kore/Simplify/Predicate.hs
index f821d63259..139da75ce8 100644
--- a/kore/src/Kore/Simplify/Predicate.hs
+++ b/kore/src/Kore/Simplify/Predicate.hs
@@ -56,6 +56,7 @@ import Kore.Rewrite.RewritingVariable (
     RewritingVariableName,
  )
 import qualified Kore.Simplify.Ceil as Ceil
+import qualified Kore.Simplify.In as In
 import qualified Kore.Simplify.Not as Not
 import Kore.Simplify.Simplify
 import Kore.Substitute
@@ -72,6 +73,7 @@ import Kore.Syntax (
     Or (..),
     SomeVariableName,
     Top (..),
+    In (..),
     variableName,
  )
 import qualified Kore.Syntax.Exists as Exists
@@ -178,6 +180,8 @@ simplify sideCondition original =
                 ForallF forallF ->
                     traverse worker (Forall.refreshForall avoid forallF)
                         >>= simplifyForall sideCondition
+                InF inF ->
+                    simplifyIn sideCondition =<< traverse simplifyTerm inF
                 _ -> simplifyPredicateTODO sideCondition predicate & MultiOr.observeAllT
       where
         _ :< predicateF = Recursive.project predicate
@@ -522,3 +526,11 @@ extractFirstAssignment someVariableName predicates =
         guard (TermLike.isFunctionPattern termLike)
         (guard . not) (someVariableName `occursIn` termLike)
         pure termLike
+
+simplifyIn ::
+    MonadSimplify simplifier =>
+    SideCondition RewritingVariableName ->
+    In sort (OrPattern RewritingVariableName) ->
+    simplifier NormalForm
+simplifyIn sideCondition =
+    In.simplify sideCondition >=> return . MultiOr.map (from @(Condition _))
diff --git a/kore/test/Test/Kore/Simplify/Predicate.hs b/kore/test/Test/Kore/Simplify/Predicate.hs
index d24477e891..412d5b1f7b 100644
--- a/kore/test/Test/Kore/Simplify/Predicate.hs
+++ b/kore/test/Test/Kore/Simplify/Predicate.hs
@@ -20,6 +20,7 @@ import Kore.Internal.TermLike (
     TermLike,
     mkAnd,
     mkBottom,
+    mkCeil,
     mkElemVar,
     mkEquals,
     mkNot,
@@ -328,6 +329,34 @@ test_simplify =
             (fromEquals_ (mkElemVar x) (mkElemVar y))
             [[fromEquals_ (mkElemVar x) (mkElemVar y)]]
         ]
+    , testGroup
+        "\\in"
+        [ test
+            "\\top"
+            (fromIn_ Mock.a Mock.a)
+            [[]]
+        , test
+            "\\bottom"
+            (fromIn_ Mock.a Mock.b)
+            []
+        , test
+            "\\ceil"
+            (fromIn_ fa fa)
+            [[faCeil]]
+        , test
+            "\\or"
+            (fromIn_ (mkElemVar Mock.xConfig) (mkOr fa fb))
+            [ [faCeil, fromEquals_ (mkElemVar Mock.xConfig) fa]
+            , [fbCeil, fromEquals_ (mkElemVar Mock.xConfig) fb]
+            ]
+        , test
+            "Predicates"
+            (fromIn_
+                (mkEquals Mock.testSort (mkElemVar Mock.xConfig) fb)
+                (mkCeil Mock.testSort fa)
+            )
+            [[fromEquals_ (mkElemVar Mock.xConfig ) fb, faCeil, fbCeil]]
+        ]
     , testGroup
         "Other"
         [ test

From 441730335acb7df62f2a6577c62a96b71c92ef00 Mon Sep 17 00:00:00 2001
From: github-actions <github-actions@github.com>
Date: Wed, 21 Jul 2021 13:26:50 +0000
Subject: [PATCH 2/3] Format with fourmolu

---
 kore/src/Kore/Simplify/Predicate.hs       | 2 +-
 kore/test/Test/Kore/Simplify/Predicate.hs | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/kore/src/Kore/Simplify/Predicate.hs b/kore/src/Kore/Simplify/Predicate.hs
index 139da75ce8..73b35d72b6 100644
--- a/kore/src/Kore/Simplify/Predicate.hs
+++ b/kore/src/Kore/Simplify/Predicate.hs
@@ -69,11 +69,11 @@ import Kore.Syntax (
     Forall (Forall),
     Iff (..),
     Implies (..),
+    In (..),
     Not (..),
     Or (..),
     SomeVariableName,
     Top (..),
-    In (..),
     variableName,
  )
 import qualified Kore.Syntax.Exists as Exists
diff --git a/kore/test/Test/Kore/Simplify/Predicate.hs b/kore/test/Test/Kore/Simplify/Predicate.hs
index 412d5b1f7b..b0727e2326 100644
--- a/kore/test/Test/Kore/Simplify/Predicate.hs
+++ b/kore/test/Test/Kore/Simplify/Predicate.hs
@@ -351,11 +351,11 @@ test_simplify =
             ]
         , test
             "Predicates"
-            (fromIn_
+            ( fromIn_
                 (mkEquals Mock.testSort (mkElemVar Mock.xConfig) fb)
                 (mkCeil Mock.testSort fa)
             )
-            [[fromEquals_ (mkElemVar Mock.xConfig ) fb, faCeil, fbCeil]]
+            [[fromEquals_ (mkElemVar Mock.xConfig) fb, faCeil, fbCeil]]
         ]
     , testGroup
         "Other"

From 2abc1c41e10332a7089e01a0b38a464a8e6feab8 Mon Sep 17 00:00:00 2001
From: ana-pantilie <ana.pantilie95@gmail.com>
Date: Fri, 23 Jul 2021 12:29:47 +0300
Subject: [PATCH 3/3] Retrigger workflows