Check consistency of constraints before evaluating a pattern

booster/library/Booster/JsonRpc.hs

@@ -155,33 +155,51 @@ respond stateVar request =
 
                         solver <- maybe (SMT.noSolver) (SMT.initSolver def) mSMTOptions
 
-                        logger <- getLogger
-                        prettyModifiers <- getPrettyModifiers
-                        let rewriteConfig =
-                                RewriteConfig
-                                    { definition = def
-                                    , llvmApi = mLlvmLibrary
-                                    , smtSolver = solver
-                                    , varsToAvoid = substVars
-                                    , doTracing
-                                    , logger
-                                    , prettyModifiers
-                                    , mbMaxDepth = mbDepth
-                                    , mbSimplify = rewriteOpts.interimSimplification
-                                    , cutLabels = cutPoints
-                                    , terminalLabels = terminals
-                                    }
-                        result <-
-                            performRewrite rewriteConfig substPat
-                        SMT.finaliseSolver solver
-                        stop <- liftIO $ getTime Monotonic
-                        let duration =
-                                if fromMaybe False req.logTiming
-                                    then
-                                        Just $
-                                            fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9
-                                    else Nothing
-                        pure $ execResponse duration req result substitution unsupported
+                        -- check input pattern's consistency before starting rewriting
+                        evaluatedInitialPattern <-
+                            ApplyEquations.evaluatePattern
+                                def
+                                mLlvmLibrary
+                                solver
+                                mempty
+                                substPat
+
+                        case evaluatedInitialPattern of
+                            (Left ApplyEquations.SideConditionFalse{}, _) -> do
+                                -- input pattern's constraints are Bottom, return Vacuous
+                                stop <- liftIO $ getTime Monotonic
+                                pure $
+                                    execResponse
+                                        (duration req.logTiming start stop)
+                                        req
+                                        (0, mempty, RewriteTrivial substPat)
+                                        substitution
+                                        unsupported
+                            (Left other, _) ->
+                                pure . Left . RpcError.backendError $ RpcError.Aborted (Text.pack . constructorName $ other)
+                            (Right newPattern, simplifierCache) -> do
+                                logger <- getLogger
+                                prettyModifiers <- getPrettyModifiers
+                                let rewriteConfig =
+                                        RewriteConfig
+                                            { definition = def
+                                            , llvmApi = mLlvmLibrary
+                                            , smtSolver = solver
+                                            , varsToAvoid = substVars
+                                            , doTracing
+                                            , logger
+                                            , prettyModifiers
+                                            , mbMaxDepth = mbDepth
+                                            , mbSimplify = rewriteOpts.interimSimplification
+                                            , cutLabels = cutPoints
+                                            , terminalLabels = terminals
+                                            }
+
+                                result <-
+                                    performRewrite rewriteConfig simplifierCache newPattern
+                                SMT.finaliseSolver solver
+                                stop <- liftIO $ getTime Monotonic
+                                pure $ execResponse (duration req.logTiming start stop) req result substitution unsupported
             RpcTypes.AddModule RpcTypes.AddModuleRequest{_module, nameAsId = nameAsId'} -> Booster.Log.withContext CtxAddModule $ runExceptT $ do
                 -- block other request executions while modifying the server state
                 state <- liftIO $ takeMVar stateVar
@@ -247,9 +265,9 @@ respond stateVar request =
                 start <- liftIO $ getTime Monotonic
                 let internalised =
                         runExcept $ internaliseTermOrPredicate DisallowAlias CheckSubsorts Nothing def req.state.term
-                let mkTraces duration
+                let mkTraces durationLog
                         | Just True <- req.logTiming =
-                            Just [ProcessingTime (Just Booster) duration]
+                            Just [ProcessingTime (Just Booster) durationLog]
                         | otherwise =
                             Nothing
 
@@ -327,11 +345,11 @@ respond stateVar request =
                 SMT.finaliseSolver solver
                 stop <- liftIO $ getTime Monotonic
 
-                let duration =
+                let durationLog =
                         fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9
                     mkSimplifyResponse state =
                         RpcTypes.Simplify
-                            RpcTypes.SimplifyResult{state, logs = mkTraces duration}
+                            RpcTypes.SimplifyResult{state, logs = mkTraces durationLog}
                 pure $ second mkSimplifyResponse result
             RpcTypes.GetModel req -> withModule req._module $ \case
                 (_, _, Nothing, _) -> do
@@ -567,6 +585,13 @@ respond stateVar request =
                             , logs = Nothing
                             }
 
+    duration mLogTiming start stop =
+        if fromMaybe False mLogTiming
+            then
+                Just $
+                    fromIntegral (toNanoSecs (diffTimeSpec stop start)) / 1e9
+            else Nothing
+
 handleSmtError :: JsonRpcHandler
 handleSmtError = JsonRpcHandler $ \case
     SMT.GeneralSMTError err -> runtimeError "problem" err

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -439,7 +439,11 @@ evaluateTerm' ::
 evaluateTerm' direction = iterateEquations direction PreferFunctions
 
 {- | Simplify a Pattern, processing its constraints independently.
-     Returns either the first failure or the new pattern if no failure was encountered
+
+     Before evaluating the term of the pattern,
+     the constraints of the pattern are checked for consistency with an SMT solver.
+
+     Returns either the first failure or the new pattern if no failure was encountered.
 -}
 evaluatePattern ::
     LoggerMIO io =>
@@ -457,10 +461,36 @@ evaluatePattern' ::
     LoggerMIO io =>
     Pattern ->
     EquationT io Pattern
-evaluatePattern' pat@Pattern{term, ceilConditions} = withPatternContext pat $ do
+evaluatePattern' pat@Pattern{term, constraints, ceilConditions} = withPatternContext pat $ do
+    solver <- (.smtSolver) <$> getConfig
+    -- check the pattern's constraints for satisfiability to ensure they are consistent
+    consistent <-
+        withContext CtxConstraint $ do
+            withContext CtxDetail . withTermContext (coerce $ collapseAndBools constraints) $ pure ()
+            consistent <- SMT.isSat solver constraints
+            withContext CtxConstraint $
+                logMessage $
+                    "Constraints consistency check returns: " <> show consistent
+            pure consistent
+    case consistent of
+        Right False -> do
+            -- the constraints are unsatisfiable, which means that the patten is Bottom
+            throw . SideConditionFalse . collapseAndBools $ constraints
+        Left SMT.SMTSolverUnknown{} -> do
+            -- unlikely case of an Unknown response to a consistency check.
+            -- continue to preserver the old behaviour.
+            withContext CtxConstraint . logWarn . Text.pack $
+                "Constraints consistency UNKNOWN: " <> show consistent
+            pure ()
+        Left other ->
+            -- fail hard on SMT error other than @SMT.SMTSolverUnknown@
+            liftIO $ Exception.throw other
+        Right True ->
+            -- constraints are consistent, continue
+            pure ()
+
     newTerm <- withTermContext term $ evaluateTerm' BottomUp term `catch_` keepTopLevelResults
-    -- after evaluating the term, evaluate all (existing and
-    -- newly-acquired) constraints, once
+    -- after evaluating the term, evaluate all (existing and newly-acquired) constraints, once
     traverse_ simplifyAssumedPredicate . predicates =<< getState
     -- this may yield additional new constraints, left unevaluated
     evaluatedConstraints <- predicates <$> getState
@@ -477,6 +507,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

booster/library/Booster/Pattern/Rewrite.hs

@@ -704,9 +704,10 @@ performRewrite ::
     forall io.
     LoggerMIO io =>
     RewriteConfig ->
+    SimplifierCache ->
     Pattern ->
     io (Natural, Seq (RewriteTrace ()), RewriteResult Pattern)
-performRewrite rewriteConfig pat = do
+performRewrite rewriteConfig initialCache pat = do
     (rr, RewriteStepsState{counter, traces}) <-
         flip runStateT rewriteStart $ doSteps False pat
     pure (counter, traces, rr)
@@ -722,6 +723,14 @@ performRewrite rewriteConfig pat = do
         , terminalLabels
         } = rewriteConfig
 
+    rewriteStart :: RewriteStepsState
+    rewriteStart =
+        RewriteStepsState
+            { counter = 0
+            , traces = mempty
+            , simplifierCache = initialCache
+            }
+
     logDepth = withContext CtxDepth . logMessage
 
     depthReached n = maybe False (n >=) mbMaxDepth
@@ -919,11 +928,3 @@ data RewriteStepsState = RewriteStepsState
     , traces :: !(Seq (RewriteTrace ()))
     , simplifierCache :: SimplifierCache
     }
-
-rewriteStart :: RewriteStepsState
-rewriteStart =
-    RewriteStepsState
-        { counter = 0
-        , traces = mempty
-        , simplifierCache = mempty
-        }