From 64eec65e2b85b0c08f7744e2ce5936587c6ba934 Mon Sep 17 00:00:00 2001
From: github-actions <github-actions@github.com>
Date: Mon, 19 Aug 2024 07:45:35 +0000
Subject: [PATCH] Format with fourmolu

---
 booster/library/Booster/SMT/Interface.hs |  6 +++---
 kore/src/Kore/Rewrite/SMT/Evaluator.hs   | 17 ++++++++++------
 kore/src/SMT/Utils.hs                    | 26 +++++++++++++-----------
 3 files changed, 28 insertions(+), 21 deletions(-)

diff --git a/booster/library/Booster/SMT/Interface.hs b/booster/library/Booster/SMT/Interface.hs
index 100c45f1f0..65acca1faa 100644
--- a/booster/library/Booster/SMT/Interface.hs
+++ b/booster/library/Booster/SMT/Interface.hs
@@ -515,6 +515,6 @@ closureOver atoms exprs = loop mempty exprs atoms
     loop acc exprs' currentAtoms =
         let (addedExprs, rest) = Set.partition (Set.null . Set.intersection currentAtoms . smtVars) exprs'
             newAtoms = Set.unions $ Set.map smtVars addedExprs
-        in if Set.null addedExprs
-               then acc
-               else loop (acc <> addedExprs) rest newAtoms
+         in if Set.null addedExprs
+                then acc
+                else loop (acc <> addedExprs) rest newAtoms
diff --git a/kore/src/Kore/Rewrite/SMT/Evaluator.hs b/kore/src/Kore/Rewrite/SMT/Evaluator.hs
index 792977d507..9419fa4d42 100644
--- a/kore/src/Kore/Rewrite/SMT/Evaluator.hs
+++ b/kore/src/Kore/Rewrite/SMT/Evaluator.hs
@@ -112,7 +112,11 @@ evalPredicate onUnknown predicate sideConditionM = case predicate of
         Nothing ->
             decidePredicate onUnknown SideCondition.top [] predicate
         Just sideCondition ->
-            decidePredicate onUnknown sideCondition (Predicate.getMultiAndPredicate $ from @_ @(Predicate _) sideCondition) predicate
+            decidePredicate
+                onUnknown
+                sideCondition
+                (Predicate.getMultiAndPredicate $ from @_ @(Predicate _) sideCondition)
+                predicate
 
 {- | Attempt to evaluate the 'Conditional' argument with an optional side
  condition using an external SMT solver.
@@ -193,11 +197,12 @@ decidePredicate onUnknown sideCondition sideConditionPredicates predicate =
     query = onErrorUnknown $ SMT.withSolver . evalTranslator $ do
         tools <- Simplifier.askMetadataTools
         Morph.hoist SMT.liftSMT $ do
-            sideConditionPredicates' <- concatMap SMT.splitAnd <$>
-                traverse
-                    (translatePredicate sideCondition tools)
-                    sideConditionPredicates
-            predicate' <- SMT.splitAnd <$> translatePredicate sideCondition tools predicate 
+            sideConditionPredicates' <-
+                concatMap SMT.splitAnd
+                    <$> traverse
+                        (translatePredicate sideCondition tools)
+                        sideConditionPredicates
+            predicate' <- SMT.splitAnd <$> translatePredicate sideCondition tools predicate
             let predicates' = SMT.transitiveClosure (Set.fromList predicate') $ Set.fromList sideConditionPredicates'
             -- when (Set.fromList predicate' /= predicates') $ liftIO $ do
             --     putStrLn $ "predicate: " <> show (Set.fromList predicate')
diff --git a/kore/src/SMT/Utils.hs b/kore/src/SMT/Utils.hs
index 96047a8352..cb3d5b53b3 100644
--- a/kore/src/SMT/Utils.hs
+++ b/kore/src/SMT/Utils.hs
@@ -1,4 +1,5 @@
 module SMT.Utils (module SMT.Utils) where
+
 import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Text (Text, isPrefixOf, isSuffixOf)
@@ -8,21 +9,22 @@ import SMT qualified
 
 splitAnd :: SMT.SExpr -> [SMT.SExpr]
 splitAnd = \case
-  SMT.List (SMT.Atom "and": xs) -> concatMap splitAnd xs
-  other -> [other]
+    SMT.List (SMT.Atom "and" : xs) -> concatMap splitAnd xs
+    other -> [other]
 
 varAtoms :: SMT.SExpr -> Set Text
 varAtoms = \case
-  SMT.Atom a
-    | "<" `isPrefixOf` a && ">" `isSuffixOf` a -> Set.singleton a
-    | otherwise -> mempty
-  SMT.List xs -> mconcat $ map varAtoms xs
-  _ -> mempty
+    SMT.Atom a
+        | "<" `isPrefixOf` a && ">" `isSuffixOf` a -> Set.singleton a
+        | otherwise -> mempty
+    SMT.List xs -> mconcat $ map varAtoms xs
+    _ -> mempty
 
-transitiveClosure :: Set SMT.SExpr ->  Set SMT.SExpr ->  Set SMT.SExpr
+transitiveClosure :: Set SMT.SExpr -> Set SMT.SExpr -> Set SMT.SExpr
 transitiveClosure cl' rest' = loop (Set.unions (Set.map varAtoms cl')) cl' rest'
   where
-    loop clVars cl rest = 
-      let (nonCommon, common) = Set.partition (null . Set.intersection clVars . varAtoms) rest in
-        if null common then cl else 
-          loop (clVars <> Set.unions (Set.map varAtoms common)) (cl <> common) nonCommon
\ No newline at end of file
+    loop clVars cl rest =
+        let (nonCommon, common) = Set.partition (null . Set.intersection clVars . varAtoms) rest
+         in if null common
+                then cl
+                else loop (clVars <> Set.unions (Set.map varAtoms common)) (cl <> common) nonCommon