Skip to content

Fix SMT interaction in Booster #3987

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 8 commits into from
Jul 18, 2024
Merged

Fix SMT interaction in Booster #3987

Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
4794c3a
De-duplicate SMT result log message
geo2a Jul 17, 2024
a96660f
Do not proceed if the SMT ground truth is not Sat
geo2a Jul 17, 2024
6817a38
Post-process results to eliminate Unknowns
geo2a Jul 17, 2024
8ab9ad4
Log ground truth when it is SMT-unknown
geo2a Jul 18, 2024
2c53590
Use /\ instead of , to separate conjuncts
geo2a Jul 18, 2024
5bc66fb
Update booster/library/Booster/SMT/Interface.hs
geo2a Jul 18, 2024
a7514b0
Format with fourmolu
invalid-email-address Jul 18, 2024
590c324
Fix check
geo2a Jul 18, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
82 changes: 51 additions & 31 deletions booster/library/Booster/SMT/Interface.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ import Control.Monad.IO.Class
import Control.Monad.Trans.Class
import Control.Monad.Trans.Except
import Control.Monad.Trans.State
import Data.Aeson (object, (.=))
import Data.ByteString.Char8 qualified as BS
import Data.Coerce
import Data.Data (Proxy)
Expand All @@ -34,7 +35,7 @@ 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 Prettyprinter (Pretty, hsep)
import Prettyprinter (Pretty, backslash, hsep, punctuate, slash, (<+>))
import SMTLIB.Backends.Process qualified as Backend

import Booster.Definition.Base
Expand All @@ -46,6 +47,7 @@ import Booster.Prettyprinter qualified as Pretty
import Booster.SMT.Base as SMT
import Booster.SMT.Runner as SMT
import Booster.SMT.Translate as SMT
import Booster.Syntax.Json.Externalise (externaliseTerm)

data SMTError
= GeneralSMTError Text
Expand Down Expand Up @@ -370,10 +372,6 @@ checkPredicates ctxt givenPs givenSubst psToCheck
Log.logMessage . Pretty.renderOneLineText $
hsep ("Predicates to check:" : map (pretty' @mods) (Set.toList psToCheck))
result <- interactWithSolver smtGiven sexprsToCheck
Log.logMessage $
"Check of Given ∧ P and Given ∧ !P produced "
<> (Text.pack $ show result)

case result of
(Unsat, Unsat) -> pure Nothing -- defensive choice for inconsistent ground truth
(Sat, Sat) -> do
Expand Down Expand Up @@ -435,29 +433,51 @@ checkPredicates ctxt givenPs givenSubst psToCheck
-- assert ground truth
mapM_ smtRun smtGiven

consistent <- smtRun CheckSat
unless (consistent == Sat) $ do
let errMsg = ("Inconsistent ground truth, check returns Nothing" :: Text)
Log.logMessage 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)

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

Log.logMessage $
"Check of Given ∧ P and Given ∧ !P produced "
<> pack (show (positive, negative))

pure (positive, negative)
groundTruthCheckSmtResult <- smtRun CheckSat
Log.logMessage ("Ground truth check returned: " <> show groundTruthCheckSmtResult)
case groundTruthCheckSmtResult of
Unsat -> do
Log.logMessage ("Inconsistent ground truth" :: Text)
pure (Unsat, Unsat)
Unknown -> do
Log.getPrettyModifiers >>= \case
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) -> do
Log.withContext Log.CtxDetail
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe log in the context that these conditions actually cause an "Abort"?

Suggested change
Log.withContext Log.CtxDetail
Log.withContext Log.CtxAbort
$ Log.withContext Log.CtxDetail

$ Log.logMessage
$ Log.WithJsonMessage
(object ["conditions" .= (map (externaliseTerm . coerce) . Set.toList $ givenPs)])
$ Pretty.renderOneLineText
$ "Unknown ground truth: "
<+> (hsep . punctuate (slash <> backslash) . map (pretty' @mods) . Set.toList $ givenPs)
pure (Unknown, Unknown)
_ -> do
-- 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)

positive <- do
smtRun_ $ Assert "P" allToCheck
smtRun CheckSat
smtRun_ Pop

negative <- do
smtRun_ $ Assert "not P" (SMT.smtnot allToCheck)
smtRun CheckSat
smtRun_ Pop

Log.logMessage $
"Check of Given ∧ P and Given ∧ !P produced "
<> pack (show (positive, negative))

let (positive', negative') =
case (positive, negative) of
(Unsat, _) -> (Unsat, Sat)
(_, Unsat) -> (Sat, Unsat)
_ -> (positive, negative)
unless ((positive, negative) == (positive', negative')) $
Log.logMessage $
"Given ∧ P and Given ∧ !P interpreted as "
<> pack (show (positive', negative'))
pure (positive', negative')
Loading