Skip to content

Commit

Permalink
3902 use smt solver for equations (#3904)
Browse files Browse the repository at this point in the history 
This PR adds the SMT solver to the equation application function.

Unclear side conditions for equations (those that could not be
simplified to values in isolation) are checked (two-sided) using the SMT
solver in context of the known path condition.
This should reduce the amount of unclear conditions, and thereby enable
more simplificaitons in boooster.

Fixes #3902

---------

Co-authored-by: github-actions <github-actions@github.com>
  • Loading branch information
@jberthold
jberthold and github-actions authored Jul 16, 2024
1 parent c71e5da commit abf81e9
Show file tree
Hide file tree
Showing 18 changed files with 4,120 additions and 541 deletions.
69 changes: 58 additions & 11 deletions booster/library/Booster/Pattern/ApplyEquations.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,6 +26,7 @@ module Booster.Pattern.ApplyEquations (
evaluateConstraints,
) where

import Control.Exception qualified as Exception (throw)
import Control.Monad
import Control.Monad.Extra (fromMaybeM, whenJust)
import Control.Monad.IO.Class (MonadIO (..))
Expand All @@ -39,7 +40,7 @@ import Data.ByteString.Char8 qualified as BS
import Data.Coerce (coerce)
import Data.Data (Data, Proxy)
import Data.Foldable (toList, traverse_)
import Data.List (intersperse, partition)
import Data.List (foldl1', intersperse, partition)
import Data.List.NonEmpty qualified as NonEmpty
import Data.Map (Map)
import Data.Map qualified as Map
Expand Down Expand Up @@ -817,17 +818,45 @@ applyEquation term rule =
-- could now be syntactically present in the path constraints, filter again
stillUnclear <- lift $ filterOutKnownConstraints knownPredicates unclearConditions

-- abort if any of the conditions is still unclear at that point
mbSolver :: Maybe SMT.SMTContext <- (.smtSolver) <$> lift getConfig

-- check any conditions that are still unclear with the SMT solver
-- (or abort if no solver is being used), abort if still unclear after
unless (null stillUnclear) $
throwE
( \ctxt ->
ctxt $
logMessage $
renderOneLineText $
"Uncertain about a condition(s) in rule:"
<+> hsep (intersperse "," $ map (pretty' @mods) unclearConditions)
, IndeterminateCondition unclearConditions
)
let checkWithSmt :: SMT.SMTContext -> EquationT io (Maybe Bool)
checkWithSmt smt =
SMT.checkPredicates smt knownPredicates mempty (Set.fromList stillUnclear) >>= \case
Left SMT.SMTSolverUnknown{} -> do
pure Nothing
Left other ->
liftIO $ Exception.throw other
Right result ->
pure result
in maybe (pure Nothing) (lift . checkWithSmt) mbSolver >>= \case
Nothing -> do
-- no solver or still unclear: abort
throwE
( \ctx ->
ctx . logMessage $
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
renderOneLineText
( "Uncertain about conditions in rule: " <+> hsep (intersperse "," $ map (pretty' @mods) stillUnclear)
)
, IndeterminateCondition stillUnclear
)
Just False -> do
-- actually false given path condition: fail
let failedP = Predicate $ foldl1' AndTerm $ map coerce stillUnclear
throwE
( \ctx ->
ctx . logMessage $
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) stillUnclear]) $
renderOneLineText ("Required condition found to be false: " <> pretty' @mods failedP)
, ConditionFalse failedP
)
Just True -> do
-- can proceed
pure ()

-- check ensured conditions, filter any
-- true ones, prune if any is false
Expand All @@ -842,6 +871,24 @@ applyEquation term rule =
( checkConstraint $ \p -> (\ctxt -> ctxt $ logMessage ("Ensures clause simplified to #Bottom." :: Text), EnsuresFalse p)
)
ensured
-- check all ensured conditions together with the path condition
whenJust mbSolver $ \solver -> do
lift (SMT.checkPredicates solver knownPredicates mempty $ Set.fromList ensuredConditions) >>= \case
Right (Just False) -> do
let falseEnsures = Predicate $ foldl1' AndTerm $ map coerce ensuredConditions
throwE
( \ctx ->
ctx . logMessage $
WithJsonMessage (object ["conditions" .= map (externaliseTerm . coerce) ensuredConditions]) $
renderOneLineText ("Ensured conditions found to be false: " <> pretty' @mods falseEnsures)
, EnsuresFalse falseEnsures
)
Right _other ->
pure ()
Left SMT.SMTSolverUnknown{} ->
pure ()
Left other ->
liftIO $ Exception.throw other
lift $ pushConstraints $ Set.fromList ensuredConditions
pure $ substituteInTerm subst rule.rhs
where
Expand Down
37 changes: 37 additions & 0 deletions booster/test/rpc-integration/resources/simplify-smt.k
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
module SIMPLIFY-SMT-SYNTAX
imports INT
imports BOOL
imports STRING

// testing SMT solver use during equation application

syntax Thing ::= unevaluated ( Int, Int ) [function, symbol("unevaluated")]
| evaluated ( String ) [symbol("evaluated")]
endmodule

module SIMPLIFY-SMT
imports INT
imports BOOL
imports SIMPLIFY-SMT-SYNTAX

// contradicting requires clauses: unclear in isolation, false when checked together
rule [bad-requires]:
unevaluated(A, B) => evaluated("contradicting requires clause")
requires A *Int B <=Int 0 andBool A <Int B andBool B <Int A // should never apply
[priority(10), preserves-definedness]
// unclear without SMT solver, aborting function evaluation)

// Should apply with the right path conditions about A and B.
rule [good-requires]:
unevaluated(A, B) => evaluated("A and B have the same sign and are not zero")
requires 0 <Int A *Int B
[priority(20), preserves-definedness]

// contradicting ensures clauses: unclear in isolation, false when checked together
rule [bad-ensures]:
unevaluated(A, B) => evaluated("contradicting ensures clause")
ensures A <Int B andBool B <Int A // should terminate the evaluation
[priority(30), preserves-definedness]
// would be added to the path condition without SMT solver

endmodule
Loading

0 comments on commit abf81e9

Please sign in to comment.