HOTFIX re-introduce indeterminate result for checkPredicates instead of exceptions (#3908)

* Re-introduces the 'indeterminate' result for checkPredicates, and
returns that on inconsistent ground truth.
* In the rewrite, aborts on `SMTSolverUnknown` when checking requires
clauses, but throws actual exceptions (terminating the request) on other
SMT errors (translation error, general error).

Follow-up to #3907

Author: jberthold

booster/library/Booster/Pattern/Rewrite.hs

@@ -18,6 +18,7 @@ module Booster.Pattern.Rewrite (
 ) where
 
 import Control.Applicative ((<|>))
+import Control.Exception qualified as Exception (throw)
 import Control.Monad
 import Control.Monad.Extra (whenJust)
 import Control.Monad.IO.Class (MonadIO (..))
@@ -354,29 +355,30 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
     -- check unclear requires-clauses in the context of known constraints (prior)
     mbSolver <- lift $ RewriteT $ (.smtSolver) <$> ask
 
+    let smtUnclear = do
+            withContext "abort" . logMessage . renderOneLineText $
+                "Uncertain about condition(s) in a rule:" <+> pretty unclearRequires
+            failRewrite $
+                RuleConditionUnclear rule . coerce . foldl1 AndTerm $
+                    map coerce unclearRequires
     case mbSolver of
         Just solver -> do
-            checkAllRequires <- SMT.checkPredicates solver prior mempty (Set.fromList unclearRequires)
+            checkAllRequires <-
+                SMT.checkPredicates solver prior mempty (Set.fromList unclearRequires)
 
             case checkAllRequires of
-                Left _ -> do
-                    -- TODO: we could process SMTError here
-                    -- unclear even with the prior
-                    withContext "abort" $
-                        logMessage $
-                            renderOneLineText $
-                                "Uncertain about a condition(s) in rule:" <+> pretty unclearRequires
-                    failRewrite $
-                        RuleConditionUnclear rule . coerce $
-                            foldl1 AndTerm $
-                                map coerce unclearRequires
-                Right False -> do
+                Left SMT.SMTSolverUnknown{} ->
+                    smtUnclear -- abort rewrite if a solver result was Unknown
+                Left other ->
+                    liftIO $ Exception.throw other -- fail hard on other SMT errors
+                Right (Just False) -> do
                     -- requires is actually false given the prior
                     withContext "failure" $ logMessage ("Required clauses evaluated to #Bottom." :: Text)
                     RewriteRuleAppT $ pure NotApplied
-                Right True ->
-                    -- can proceed
-                    pure ()
+                Right (Just True) ->
+                    pure () -- can proceed
+                Right Nothing ->
+                    smtUnclear -- no implication could be determined
         Nothing ->
             unless (null unclearRequires) $ do
                 withContext "abort" $
@@ -398,10 +400,15 @@ applyRule pat@Pattern{ceilConditions} rule = withRuleContext rule $ runRewriteRu
     -- check all new constraints together with the known side constraints
     whenJust mbSolver $ \solver ->
         (lift $ SMT.checkPredicates solver prior mempty (Set.fromList newConstraints)) >>= \case
-            Right False -> do
+            Right (Just False) -> do
                 withContext "success" $ logMessage ("New constraints evaluated to #Bottom." :: Text)
                 RewriteRuleAppT $ pure Trivial
-            _other -> pure ()
+            Right _other ->
+                pure ()
+            Left SMT.SMTSolverUnknown{} ->
+                pure ()
+            Left other ->
+                liftIO $ Exception.throw other
 
     -- existential variables may be present in rule.rhs and rule.ensures,
     -- need to strip prefixes and freshen their names with respect to variables already

booster/library/Booster/SMT/Interface.hs

@@ -263,9 +263,9 @@ checkPredicates ::
     Set Predicate ->
     Map Variable Term ->
     Set Predicate ->
-    io (Either SMTError Bool)
+    io (Either SMTError (Maybe Bool))
 checkPredicates ctxt givenPs givenSubst psToCheck
-    | null psToCheck = pure $ Right True
+    | null psToCheck = pure . Right $ Just True
     | Left errMsg <- translated = Log.withContext "smt" $ do
         Log.logErrorNS "booster" $ "SMT translation error: " <> errMsg
         Log.logMessage $ "SMT translation error: " <> errMsg
@@ -297,34 +297,35 @@ checkPredicates ctxt givenPs givenSubst psToCheck
         mapM_ smtRun smtGiven
 
         consistent <- smtRun CheckSat
-        when (consistent /= Sat) $ do
-            void $ smtRun Pop
+        unless (consistent == Sat) $ do
             let errMsg = ("Inconsistent ground truth, check returns Nothing" :: Text)
             Log.logMessage errMsg
-            throwE $ GeneralSMTError errMsg
+        let ifConsistent check = if (consistent == Sat) then check else pure Unsat
 
         -- save ground truth for 2nd check
         smtRun_ Push
 
         -- run check for K ∧ P and then for K ∧ !P
         let allToCheck = SMT.List (Atom "and" : sexprsToCheck)
 
-        smtRun_ $ Assert "P" allToCheck
-        positive <- smtRun CheckSat
+        positive <- ifConsistent $ do
+            smtRun_ $ Assert "P" allToCheck
+            smtRun CheckSat
+        smtRun_ Pop
+        negative <- ifConsistent $ do
+            smtRun_ $ Assert "not P" (SMT.smtnot allToCheck)
+            smtRun CheckSat
         smtRun_ Pop
-        smtRun_ $ Assert "not P" (SMT.smtnot allToCheck)
-        negative <- smtRun CheckSat
-        void $ smtRun Pop
 
         Log.logMessage $
             "Check of Given ∧ P and Given ∧ !P produced "
                 <> pack (show (positive, negative))
 
         case (positive, negative) of
-            (Unsat, Unsat) -> throwSMT "Inconsistent ground truth: should have been caught above"
-            (Sat, Sat) -> throwE $ GeneralSMTError "Implication not determined"
-            (Sat, Unsat) -> pure True
-            (Unsat, Sat) -> pure False
+            (Unsat, Unsat) -> pure Nothing -- defensive choice for inconsistent ground truth
+            (Sat, Sat) -> pure Nothing -- implication not determined
+            (Sat, Unsat) -> pure $ Just True
+            (Unsat, Sat) -> pure $ Just False
             (Unknown, _) -> do
                 smtRun GetReasonUnknown >>= \case
                     ReasonUnknown reason -> throwE $ SMTSolverUnknown reason givenPs psToCheck