Skip to content

Commit d66088a

Browse files
goodlyrottenapplegeo2a
authored andcommitted
implment isSat
1 parent 6fdb95b commit d66088a

File tree

1 file changed

+63
-0
lines changed

1 file changed

+63
-0
lines changed

booster/library/Booster/SMT/Interface.hs

Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ module Booster.SMT.Interface (
1515
finaliseSolver,
1616
getModelFor,
1717
checkPredicates,
18+
isSat,
1819
hardResetSolver,
1920
) where
2021

@@ -493,3 +494,65 @@ checkPredicates ctxt givenPs givenSubst psToCheck
493494
"Given ∧ P and Given ∧ !P interpreted as "
494495
<> pack (show (positive', negative'))
495496
pure (positive', negative')
497+
498+
isSat ::
499+
forall io.
500+
Log.LoggerMIO io =>
501+
SMT.SMTContext ->
502+
Set Predicate ->
503+
io (Either SMTError Bool)
504+
isSat ctxt psToCheck
505+
| null psToCheck = pure . Right $ True
506+
| Left errMsg <- translated = Log.withContext Log.CtxSMT $ do
507+
Log.withContext Log.CtxAbort $ Log.logMessage $ "SMT translation error: " <> errMsg
508+
pure . Left . SMTTranslationError $ errMsg
509+
| Right (smtToCheck, transState) <- translated = Log.withContext Log.CtxSMT $ do
510+
evalSMT ctxt . runExceptT $ solve smtToCheck transState
511+
where
512+
translated :: Either Text ([DeclareCommand], TranslationState)
513+
translated =
514+
SMT.runTranslator $
515+
mapM (\(Predicate p) -> Assert (mkComment p) <$> SMT.translateTerm p) $
516+
Set.toList psToCheck
517+
518+
solve smtToCheck transState = solve'
519+
where
520+
solve' = do
521+
lift $ hardResetSolver ctxt.options
522+
Log.getPrettyModifiers >>= \case
523+
ModifiersRep (_ :: FromModifiersT mods => Proxy mods) ->
524+
Log.logMessage . Pretty.renderOneLineText $
525+
hsep ("Predicates to check:" : map (pretty' @mods) (Set.toList psToCheck))
526+
lift $ declareVariables transState
527+
mapM_ smtRun smtToCheck
528+
smtRun CheckSat >>= \case
529+
Sat -> pure True
530+
Unsat -> pure False
531+
Unknown _ -> retry
532+
other -> do
533+
let msg = "Unexpected result while calling 'check-sat': " <> show other
534+
Log.withContext Log.CtxAbort $ Log.logMessage $ Text.pack msg
535+
throwSMT' msg
536+
537+
retry = do
538+
opts <- lift . SMT $ gets (.options)
539+
case opts.retryLimit of
540+
Just x | x > 0 -> do
541+
let newOpts = opts{timeout = 2 * opts.timeout, retryLimit = Just $ x - 1}
542+
lift $ hardResetSolver newOpts
543+
Log.logMessage ("Retrying with higher timeout" :: Text)
544+
solve'
545+
_ -> failBecauseUnknown
546+
547+
failBecauseUnknown :: ExceptT SMTError (SMT io) Bool
548+
failBecauseUnknown =
549+
smtRun GetReasonUnknown >>= \case
550+
Unknown reason -> do
551+
Log.withContext Log.CtxAbort $
552+
Log.logMessage $
553+
"Returned Unknown. Reason: " <> fromMaybe "UNKNOWN" reason
554+
throwE $ SMTSolverUnknown reason mempty psToCheck
555+
other -> do
556+
let msg = "Unexpected result while calling ':reason-unknown': " <> show other
557+
Log.withContext Log.CtxAbort $ Log.logMessage $ Text.pack msg
558+
throwSMT' msg

0 commit comments

Comments
 (0)