Extend Unknown type, abort on unsafe unknown ensures

Author: geo2a

booster/library/Booster/JsonRpc.hs

@@ -365,7 +365,7 @@ respond stateVar request =
                                         withContext CtxGetModel $
                                             withContext CtxSMT $
                                                 logMessage ("No predicates or substitutions given, returning Unknown" :: Text)
-                                        pure $ SMT.IsUnknown "No predicates or substitutions given"
+                                        pure $ SMT.IsUnknown (SMT.SMTUnknownReason "No predicates or substitutions given")
                                     else do
                                         solver <- SMT.initSolver def smtOptions
                                         result <- SMT.getModelFor solver boolPs suppliedSubst
@@ -409,7 +409,7 @@ respond stateVar request =
                                             , substitution = Nothing
                                             }
                                 SMT.IsUnknown reason -> do
-                                    logMessage $ "SMT result: Unknown - " <> reason
+                                    logMessage $ "SMT result: Unknown - " <> show reason
                                     pure . Right . RpcTypes.GetModel $
                                         RpcTypes.GetModelResult
                                             { satisfiable = RpcTypes.Unknown

booster/library/Booster/Pattern/Rewrite.hs

@@ -307,7 +307,7 @@ applyRule pat@Pattern{ceilConditions} rule =
                         MatchSuccess matchingSubstitution -> do
                             -- existential variables may be present in rule.rhs and rule.ensures,
                             -- need to strip prefixes and freshen their names with respect to variables already
-                            -- present in the input pattern and in the unification substitution
+                            -- present in the input pattern and in the matching substitution
                             varsFromInput <- lift . RewriteT $ asks (.varsToAvoid)
                             let varsFromPattern = freeVariables pat.term <> (Set.unions $ Set.map (freeVariables . coerce) pat.constraints)
                                 varsFromSubst = Set.unions . map freeVariables . Map.elems $ matchingSubstitution
@@ -498,18 +498,11 @@ applyRule pat@Pattern{ceilConditions} rule =
 
         -- check unclear requires-clauses in the context of known constraints (priorKnowledge)
         solver <- lift $ RewriteT $ (.smtSolver) <$> ask
-        let smtUnclear = do
-                withContext CtxConstraint . withContext CtxAbort . logMessage $
-                    WithJsonMessage (object ["conditions" .= (externaliseTerm . coerce <$> stillUnclear)]) $
-                        renderOneLineText $
-                            "Uncertain about condition(s) in a rule:"
-                                <+> (hsep . punctuate comma . map (pretty' @mods) $ stillUnclear)
-                failRewrite $
-                    RuleConditionUnclear rule . coerce . foldl1 AndTerm $
-                        map coerce stillUnclear
         SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList stillUnclear) >>= \case
-            SMT.IsUnknown{} ->
-                smtUnclear -- abort rewrite if a solver result was Unknown
+            SMT.IsUnknown reason -> do
+                -- abort rewrite if a solver result was Unknown
+                withContext CtxAbort $ logMessage reason
+                smtUnclear stillUnclear
             SMT.IsInvalid -> do
                 -- requires is actually false given the prior
                 withContext CtxFailure $ logMessage ("Required clauses evaluated to #Bottom." :: Text)
@@ -534,15 +527,38 @@ applyRule pat@Pattern{ceilConditions} rule =
 
         -- check all new constraints together with the known side constraints
         solver <- lift $ RewriteT $ (.smtSolver) <$> ask
+        -- TODO it is probably enough to establish satisfiablity (rather than validity) of the ensured conditions.
+        -- For now, we check validity to be safe and admit indeterminate result (i.e. (P, not P) is (Sat, Sat)).
         (lift $ SMT.checkPredicates solver pat.constraints pat.substitution (Set.fromList newConstraints)) >>= \case
+            SMT.IsUnknown SMT.ImplicationIndeterminate -> do
+                pure ()
+            SMT.IsUnknown SMT.InconsistentGroundTruth -> do
+                withContext CtxWarn $ logMessage ("Ground truth is #Bottom." :: Text)
+                RewriteRuleAppT $ pure Trivial
             SMT.IsInvalid -> do
                 withContext CtxSuccess $ logMessage ("New constraints evaluated to #Bottom." :: Text)
                 RewriteRuleAppT $ pure Trivial
+            SMT.IsUnknown reason -> do
+                -- abort rewrite if a solver result was Unknown for reason other then SMT.ImplicationIndeterminate
+                withContext CtxAbort $ logMessage reason
+                smtUnclear newConstraints
             _other ->
                 pure ()
 
         pure newConstraints
 
+    smtUnclear :: [Predicate] -> RewriteRuleAppT (RewriteT io) ()
+    smtUnclear predicates = do
+        ModifiersRep (_ :: FromModifiersT mods => Proxy mods) <- getPrettyModifiers
+        withContext CtxConstraint . withContext CtxAbort . logMessage $
+            WithJsonMessage (object ["conditions" .= (externaliseTerm . coerce <$> predicates)]) $
+                renderOneLineText $
+                    "Uncertain about condition(s) in a rule:"
+                        <+> (hsep . punctuate comma . map (pretty' @mods) $ predicates)
+        failRewrite $
+            RuleConditionUnclear rule . coerce . foldl1 AndTerm $
+                map coerce predicates
+
 {- | Reason why a rewrite did not produce a result. Contains additional
    information for logging what happened during the rewrite.
 -}

booster/library/Booster/SMT/Interface.hs

@@ -12,6 +12,7 @@ module Booster.SMT.Interface (
     SMTOptions (..), -- re-export
     defaultSMTOptions, -- re-export
     SMTError (..),
+    UnkwnonReason (..),
     initSolver,
     noSolver,
     finaliseSolver,
@@ -33,6 +34,7 @@ import Control.Monad
 import Control.Monad.IO.Class
 import Control.Monad.Trans.State
 import Data.Aeson (object, (.=))
+import Data.Aeson.Types (FromJSON (..), ToJSON (..))
 import Data.ByteString.Char8 qualified as BS
 import Data.Coerce
 import Data.Data (Proxy)
@@ -44,6 +46,14 @@ import Data.Map qualified as Map
 import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Text as Text (Text, pack, unlines, unwords)
+import Deriving.Aeson (
+    CamelToKebab,
+    CustomJSON (..),
+    FieldLabelModifier,
+    OmitNothingFields,
+    StripPrefix,
+ )
+import GHC.Generics (Generic)
 import Prettyprinter (Pretty, backslash, hsep, punctuate, slash, (<+>))
 import SMTLIB.Backends.Process qualified as Backend
 
@@ -188,12 +198,28 @@ finaliseSolver ctxt = do
     Log.logMessage ("Closing SMT solver" :: Text)
     destroyContext ctxt
 
-pattern IsUnknown :: unknown -> Either unknown b
+data UnkwnonReason
+    = -- | SMT prelude is UNSAT
+      InconsistentGroundTruth
+    | -- | (P, not P) is (SAT, SAT)
+      ImplicationIndeterminate
+    | -- | SMT solver returned unknown
+      SMTUnknownReason Text
+    deriving (Show, Eq, Generic)
+    deriving
+        (FromJSON, ToJSON)
+        via CustomJSON '[OmitNothingFields, FieldLabelModifier '[CamelToKebab, StripPrefix "_"]] UnkwnonReason
+
+instance Log.ToLogFormat UnkwnonReason where
+    toTextualLog = pack . show
+    toJSONLog = toJSON
+
+pattern IsUnknown :: UnkwnonReason -> Either UnkwnonReason b
 pattern IsUnknown u = Left u
 
 newtype IsSat' a = IsSat' (Maybe a) deriving (Functor)
 
-type IsSatResult a = Either Text (IsSat' a)
+type IsSatResult a = Either UnkwnonReason (IsSat' a)
 
 pattern IsSat :: a -> IsSatResult a
 pattern IsSat a = Right (IsSat' (Just a))
@@ -243,7 +269,7 @@ isSatReturnTransState ctxt ps subst
         SMT.runCmd CheckSat >>= \case
             Sat -> pure $ IsSat transState
             Unsat -> pure IsUnsat
-            Unknown reason -> retry (solve smtToCheck transState) (pure $ IsUnknown reason)
+            Unknown reason -> retry (solve smtToCheck transState) (pure $ IsUnknown (SMTUnknownReason reason))
             other -> do
                 let msg = "Unexpected result while calling 'check-sat': " <> show other
                 Log.withContext Log.CtxAbort $ Log.logMessage $ Text.pack msg
@@ -347,7 +373,7 @@ mkComment = BS.pack . Pretty.renderDefault . pretty' @'[Decoded]
 
 newtype IsValid' = IsValid' Bool
 
-type IsValidResult = Either (Maybe Text) IsValid'
+type IsValidResult = Either UnkwnonReason IsValid'
 
 pattern IsValid, IsInvalid :: IsValidResult
 pattern IsValid = Right (IsValid' True)
@@ -418,14 +444,14 @@ checkPredicates ctxt givenPs givenSubst psToCheck
                     hsep ("Predicates to check:" : map (pretty' @mods) (Set.toList psToCheck))
         result <- interactWithSolver smtGiven sexprsToCheck
         case result of
-            (Unsat, Unsat) -> pure $ IsUnknown Nothing -- defensive choice for inconsistent ground truth
+            (Unsat, Unsat) -> pure $ IsUnknown InconsistentGroundTruth
             (Sat, Sat) -> do
                 Log.logMessage ("Implication not determined" :: Text)
-                pure $ IsUnknown Nothing
+                pure $ IsUnknown ImplicationIndeterminate
             (Sat, Unsat) -> pure IsValid
             (Unsat, Sat) -> pure IsInvalid
-            (Unknown reason, _) -> retry (solve smtGiven sexprsToCheck transState) (pure $ IsUnknown $ Just reason)
-            (_, Unknown reason) -> retry (solve smtGiven sexprsToCheck transState) (pure $ IsUnknown $ Just reason)
+            (Unknown reason, _) -> retry (solve smtGiven sexprsToCheck transState) (pure . IsUnknown . SMTUnknownReason $ reason)
+            (_, Unknown reason) -> retry (solve smtGiven sexprsToCheck transState) (pure . IsUnknown . SMTUnknownReason $ reason)
             other ->
                 throwSMT $
                     "Unexpected result while checking a condition: " <> Text.pack (show other)