From 4b1f940ee93e62382c49e251c2561589ea50de11 Mon Sep 17 00:00:00 2001
From: Georgy Lukyanov <mail@geo2a.info>
Date: Thu, 1 Aug 2024 18:16:47 +0200
Subject: [PATCH] Emit more logs from evaluatePattern'

---
 .../library/Booster/Pattern/ApplyEquations.hs | 22 ++++++++++++++-----
 1 file changed, 16 insertions(+), 6 deletions(-)

diff --git a/booster/library/Booster/Pattern/ApplyEquations.hs b/booster/library/Booster/Pattern/ApplyEquations.hs
index 258a158046..760648a245 100644
--- a/booster/library/Booster/Pattern/ApplyEquations.hs
+++ b/booster/library/Booster/Pattern/ApplyEquations.hs
@@ -436,17 +436,24 @@ evaluatePattern' ::
 evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
     solver <- (.smtSolver) <$> getConfig
     -- check initial constraints for consistency, reporting an error if they are Bottom
-    SMT.isSat solver pat.constraints >>= \case
+    withContext CtxConstraint
+        . withContext CtxDetail
+        . withTermContext (coerce $ collapseAndBools pat.constraints)
+        $ pure ()
+    consistent <- withContext CtxConstraint $ SMT.isSat solver pat.constraints
+    withContext CtxConstraint $ do
+        logMessage $
+            "Constraints consistency check returns: " <> show consistent
+
+    case consistent of
         Right False -> do
-            let collapseAndBools :: Set Predicate -> Predicate
-                collapseAndBools = undefined
             -- the constraints are unsatisfiable, which means that the patten is Bottom
             throw . SideConditionFalse . collapseAndBools $ pat.constraints
-        Left unknwon@SMT.SMTSolverUnknown{} -> do
+        Left SMT.SMTSolverUnknown{} -> do
             -- unlikely case of an Unknown response to a consistency check.
             -- What to do here? continue for now to preserver the old behaviour.
-            withPatternContext pat . logWarn . Text.pack $
-                "Constraints consistency check returns: " <> show unknwon
+            withContext CtxConstraint . logWarn . Text.pack $
+                "Constraints consistency UNKNOWN: " <> show consistent
             continue
         Left other ->
             -- fail hard on SMT error other than @SMT.SMTSolverUnknown@
@@ -475,6 +482,9 @@ evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
             pure partialResult
         err -> throw err
 
+    collapseAndBools :: Set Predicate -> Predicate
+    collapseAndBools = coerce . foldAndBool . map coerce . Set.toList
+
 -- evaluate the given predicate assuming all others
 simplifyAssumedPredicate :: LoggerMIO io => Predicate -> EquationT io ()
 simplifyAssumedPredicate p = do