sbv-13.4: Data/SBV/Control/Query.hs
-----------------------------------------------------------------------------
-- |
-- Module : Data.SBV.Control.Query
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Querying a solver interactively.
-----------------------------------------------------------------------------
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}
module Data.SBV.Control.Query (
send, ask, retrieveResponse
, CheckSatResult(..), checkSat, checkSatUsing, checkSatAssuming, checkSatAssumingWithUnsatisfiableSet
, getUnsatCore, getProof, getInterpolantMathSAT, getInterpolantZ3, getAbduct, getAbductNext, getAssignment, getOption
, push, pop, getAssertionStackDepth
, inNewAssertionStack, echo, caseSplit, resetAssertions, exit, getAssertions, getModel, getSMTResult
, getLexicographicOptResults, getIndependentOptResults, getParetoOptResults, getAllSatResult, getUnknownReason, getObservables, ensureSat
, SMTOption(..), SMTInfoFlag(..), SMTErrorBehavior(..), SMTReasonUnknown(..), SMTInfoResponse(..), getInfo
, Logic(..), Assignment(..)
, ignoreExitCode, timeout
, (|->)
, mkSMTResult
, io
) where
import Control.Monad (unless, when, zipWithM)
import Control.Monad.IO.Class (MonadIO)
import Data.IORef (readIORef)
import qualified Data.Map.Strict as M
import qualified Data.Text as T
import qualified Data.Foldable as F
import Data.Char (toLower)
import Data.List (intercalate, nubBy)
import Data.Maybe (fromMaybe)
import Data.Function (on)
import Data.SBV.Core.Data
import Data.SBV.Core.Symbolic (MonadQuery(..), State(..), incrementInternalCounter, getSV)
import Data.SBV.Utils.SExpr
import Data.SBV.Control.Types
import Data.SBV.Control.Utils
import Data.SBV.Utils.Lib (unBar)
import Data.SBV.Utils.PrettyNum (showNegativeNumber)
-- | An Assignment of a model binding
data Assignment = Assign SVal CV
-- Is this a string? If so, return it, otherwise fail in the Maybe monad.
fromECon :: SExpr -> Maybe String
fromECon (ECon s) = Just s
fromECon _ = Nothing
-- Collect strings appearing, used in 'getOption' only
stringsOf :: SExpr -> [String]
stringsOf (ECon s) = [s]
stringsOf (ENum (i, _, _)) = [show i]
stringsOf (EReal r) = [show r]
stringsOf (EFloat f) = [show f]
stringsOf (EFloatingPoint f) = [show f]
stringsOf (EDouble d) = [show d]
stringsOf (EApp ss) = concatMap stringsOf ss
-- Sort of a light-hearted show for SExprs, for better consumption at the user level.
serialize :: Bool -> SExpr -> String
serialize removeQuotes = go
where go (ECon s) = if removeQuotes then unQuote s else s
go (ENum (i, _, _)) = showNegativeNumber i
go (EReal r) = showNegativeNumber r
go (EFloat f) = showNegativeNumber f
go (EDouble d) = showNegativeNumber d
go (EFloatingPoint f) = show f
go (EApp [x]) = go x
go (EApp ss) = "(" ++ unwords (map go ss) ++ ")"
-- | Generalization of 'Data.SBV.Control.getInfo'
getInfo :: (MonadIO m, MonadQuery m) => SMTInfoFlag -> m SMTInfoResponse
getInfo flag = do
let cmd = "(get-info " ++ show flag ++ ")"
bad = unexpected "getInfo" cmd "a valid get-info response" Nothing
isAllStatistics AllStatistics = True
isAllStatistics _ = False
isAllStat = isAllStatistics flag
grabAllStat k v = (render k, render v)
-- we're trying to do our best to get key-value pairs here, but this
-- is necessarily a half-hearted attempt.
grabAllStats (EApp xs) = walk xs
where walk [] = []
walk [t] = [grabAllStat t (ECon "")]
walk (t : v : rest) = grabAllStat t v : walk rest
grabAllStats o = [grabAllStat o (ECon "")]
r <- ask cmd
parse r bad $ \pe ->
if isAllStat
then return $ Resp_AllStatistics $ grabAllStats pe
else case pe of
ECon "unsupported" -> return Resp_Unsupported
EApp [ECon ":assertion-stack-levels", ENum (i, _, _)] -> return $ Resp_AssertionStackLevels i
EApp (ECon ":authors" : ns) -> return $ Resp_Authors (map render ns)
EApp [ECon ":error-behavior", ECon "immediate-exit"] -> return $ Resp_Error ErrorImmediateExit
EApp [ECon ":error-behavior", ECon "continued-execution"] -> return $ Resp_Error ErrorContinuedExecution
EApp (ECon ":name" : o) -> return $ Resp_Name (render (EApp o))
EApp (ECon ":reason-unknown" : o) -> return $ Resp_ReasonUnknown (unk o)
EApp (ECon ":version" : o) -> return $ Resp_Version (render (EApp o))
EApp (ECon s : o) -> return $ Resp_InfoKeyword s (map render o)
_ -> bad r Nothing
where render = serialize True
unk [ECon s] | Just d <- getUR s = d
unk o = UnknownOther (render (EApp o))
getUR s = map toLower (unQuote s) `lookup` [(map toLower k, d) | (k, d) <- unknownReasons]
-- As specified in Section 4.1 of the SMTLib document. Note that we're adding the
-- extra timeout as it is useful in this context.
unknownReasons = [ ("memout", UnknownMemOut)
, ("incomplete", UnknownIncomplete)
, ("timeout", UnknownTimeOut)
]
-- | Generalization of 'Data.SBV.Control.getOption'
getOption :: (MonadIO m, MonadQuery m) => (a -> SMTOption) -> m (Maybe SMTOption)
getOption f = case f undefined of
DiagnosticOutputChannel{} -> askFor "DiagnosticOutputChannel" ":diagnostic-output-channel" $ string DiagnosticOutputChannel
ProduceAssertions{} -> askFor "ProduceAssertions" ":produce-assertions" $ bool ProduceAssertions
ProduceAssignments{} -> askFor "ProduceAssignments" ":produce-assignments" $ bool ProduceAssignments
ProduceProofs{} -> askFor "ProduceProofs" ":produce-proofs" $ bool ProduceProofs
ProduceInterpolants{} -> askFor "ProduceInterpolants" ":produce-interpolants" $ bool ProduceInterpolants
ProduceUnsatAssumptions{} -> askFor "ProduceUnsatAssumptions" ":produce-unsat-assumptions" $ bool ProduceUnsatAssumptions
ProduceUnsatCores{} -> askFor "ProduceUnsatCores" ":produce-unsat-cores" $ bool ProduceUnsatCores
ProduceAbducts{} -> askFor "ProduceAbducts" ":produce-abducts" $ bool ProduceAbducts
RandomSeed{} -> askFor "RandomSeed" ":random-seed" $ integer RandomSeed
ReproducibleResourceLimit{} -> askFor "ReproducibleResourceLimit" ":reproducible-resource-limit" $ integer ReproducibleResourceLimit
SMTVerbosity{} -> askFor "SMTVerbosity" ":verbosity" $ integer SMTVerbosity
OptionKeyword nm _ -> askFor ("OptionKeyword" ++ nm) nm $ stringList (OptionKeyword nm)
SetLogic{} -> error "Data.SBV.Query: SMTLib does not allow querying the value of logic!"
SetTimeOut{} -> error "Data.SBV.Query: SMTLib does not allow querying the timeout value!"
-- Not to be confused by getInfo, which is totally irrelevant!
SetInfo{} -> error "Data.SBV.Query: SMTLib does not allow querying value of meta-info!"
where askFor sbvName smtLibName continue = do
let cmd = "(get-option " ++ smtLibName ++ ")"
bad = unexpected ("getOption " ++ sbvName) cmd "a valid option value" Nothing
r <- ask cmd
parse r bad $ \case ECon "unsupported" -> return Nothing
e -> continue e (bad r)
string c (ECon s) _ = return $ Just $ c s
string _ e k = k $ Just ["Expected string, but got: " ++ show (serialize False e)]
bool c (ENum (0, _, True)) _ = return $ Just $ c False
bool c (ENum (1, _, True)) _ = return $ Just $ c True
bool _ e k = k $ Just ["Expected boolean, but got: " ++ show (serialize False e)]
integer c (ENum (i, _, _)) _ = return $ Just $ c i
integer _ e k = k $ Just ["Expected integer, but got: " ++ show (serialize False e)]
-- free format, really
stringList c e _ = return $ Just $ c $ stringsOf e
-- | Generalization of 'Data.SBV.Control.getUnknownReason'
getUnknownReason :: (MonadIO m, MonadQuery m) => m SMTReasonUnknown
getUnknownReason = do ru <- getInfo ReasonUnknown
case ru of
Resp_Unsupported -> return $ UnknownOther "Solver responded: Unsupported."
Resp_ReasonUnknown r -> return r
-- Shouldn't happen, but just in case:
_ -> error $ "Unexpected reason value received: " ++ show ru
-- | Generalization of 'Data.SBV.Control.ensureSat'
ensureSat :: (MonadIO m, MonadQuery m) => m ()
ensureSat = do cfg <- getConfig
cs <- checkSatUsing $ satCmd cfg
case cs of
Sat -> return ()
DSat{} -> return ()
Unk -> do s <- getUnknownReason
error $ unlines [ ""
, "*** Data.SBV.ensureSat: Solver reported Unknown!"
, "*** Reason: " ++ show s
]
Unsat -> error "Data.SBV.ensureSat: Solver reported Unsat!"
-- | Generalization of 'Data.SBV.Control.getSMTResult'
getSMTResult :: (MonadIO m, MonadQuery m) => m SMTResult
getSMTResult = do cfg <- getConfig
cs <- checkSat
case cs of
Unsat -> Unsatisfiable cfg <$> getUnsatCoreIfRequested
Sat -> Satisfiable cfg <$> getModel
DSat p -> DeltaSat cfg p <$> getModel
Unk -> Unknown cfg <$> getUnknownReason
-- | Classify a model based on whether it has unbound objectives or not.
classifyModel :: SMTConfig -> SMTModel -> SMTResult
classifyModel cfg m
| any isExt (modelObjectives m) = SatExtField cfg m
| True = Satisfiable cfg m
where isExt (_, v) = not $ isRegularCV v
-- | Generalization of 'Data.SBV.Control.getLexicographicOptResults'
getLexicographicOptResults :: (MonadIO m, MonadQuery m) => m SMTResult
getLexicographicOptResults = do cfg <- getConfig
cs <- checkSat
case cs of
Unsat -> Unsatisfiable cfg <$> getUnsatCoreIfRequested
Sat -> classifyModel cfg <$> getModelWithObjectives
DSat{} -> classifyModel cfg <$> getModelWithObjectives
Unk -> Unknown cfg <$> getUnknownReason
where getModelWithObjectives = do objectiveValues <- getObjectiveValues
m <- getModel
return m {modelObjectives = objectiveValues}
-- | Generalization of 'Data.SBV.Control.getIndependentOptResults'
getIndependentOptResults :: forall m. (MonadIO m, MonadQuery m) => [String] -> m [(String, SMTResult)]
getIndependentOptResults objNames = do cfg <- getConfig
cs <- checkSat
case cs of
Unsat -> getUnsatCoreIfRequested >>= \mbUC -> return [(nm, Unsatisfiable cfg mbUC) | nm <- objNames]
Sat -> continue (classifyModel cfg)
DSat{} -> continue (classifyModel cfg)
Unk -> do ur <- Unknown cfg <$> getUnknownReason
return [(nm, ur) | nm <- objNames]
where continue classify = do objectiveValues <- getObjectiveValues
nms <- zipWithM getIndependentResult [0..] objNames
return [(n, classify (m {modelObjectives = objectiveValues})) | (n, m) <- nms]
getIndependentResult :: Int -> String -> m (String, SMTModel)
getIndependentResult i s = do m <- getModelAtIndex (Just i)
return (s, m)
-- | Generalization of 'Data.SBV.Control.getParetoOptResults'
getParetoOptResults :: (MonadIO m, MonadQuery m) => Maybe Int -> m (Bool, [SMTResult])
getParetoOptResults (Just i)
| i <= 0 = return (True, [])
getParetoOptResults mbN = do cfg <- getConfig
cs <- checkSat
case cs of
Unsat -> return (False, [])
Sat -> continue (classifyModel cfg)
DSat{} -> continue (classifyModel cfg)
Unk -> do ur <- getUnknownReason
return (False, [ProofError cfg [show ur] Nothing])
where continue classify = do m <- getModel
(limReached, fronts) <- getParetoFronts (subtract 1 <$> mbN) [m]
return (limReached, reverse (map classify fronts))
getParetoFronts :: (MonadIO m, MonadQuery m) => Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
getParetoFronts (Just i) sofar | i <= 0 = return (True, sofar)
getParetoFronts mbi sofar = do cs <- checkSat
let more = getModel >>= \m -> getParetoFronts (subtract 1 <$> mbi) (m : sofar)
case cs of
Unsat -> return (False, sofar)
Sat -> more
DSat{} -> more
Unk -> more
-- | Generalization of 'Data.SBV.Control.checkSatAssuming'
checkSatAssuming :: (MonadIO m, MonadQuery m) => [SBool] -> m CheckSatResult
checkSatAssuming sBools = fst <$> checkSatAssumingHelper False sBools
-- | Generalization of 'Data.SBV.Control.checkSatAssumingWithUnsatisfiableSet'
checkSatAssumingWithUnsatisfiableSet :: (MonadIO m, MonadQuery m) => [SBool] -> m (CheckSatResult, Maybe [SBool])
checkSatAssumingWithUnsatisfiableSet = checkSatAssumingHelper True
-- | Helper for the two variants of checkSatAssuming we have. Internal only.
checkSatAssumingHelper :: (MonadIO m, MonadQuery m) => Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
checkSatAssumingHelper getAssumptions sBools = do
-- sigh.. SMT-Lib requires the values to be literals only. So, create proxies.
let mkAssumption st = do swsOriginal <- mapM (\sb -> do sv <- sbvToSV st sb
return (sv, sb)) sBools
-- drop duplicates and trues
let swbs = [p | p@(sv, _) <- nubBy ((==) `on` fst) swsOriginal, sv /= trueSV]
-- get a unique proxy name for each
uniqueSWBs <- mapM (\(sv, sb) -> do unique <- incrementInternalCounter st
return (sv, (unique, sb))) swbs
let translate (sv, (unique, sb)) = (nm, decls, (proxy, sb))
where nm = show sv
proxy = "__assumption_proxy_" ++ nm ++ "_" ++ show unique
decls = [ "(declare-const " ++ proxy ++ " Bool)"
, "(assert (= " ++ proxy ++ " " ++ nm ++ "))"
]
return $ map translate uniqueSWBs
assumptions <- inNewContext mkAssumption
let (origNames, declss, proxyMap) = unzip3 assumptions
let cmd = "(check-sat-assuming (" ++ unwords (map fst proxyMap) ++ "))"
bad = unexpected "checkSatAssuming" cmd "one of sat/unsat/unknown"
$ Just [ "Make sure you use:"
, ""
, " setOption $ ProduceUnsatAssumptions True"
, ""
, "to tell the solver to produce unsat assumptions."
]
mapM_ (send True) $ concat declss
r <- ask cmd
let grabUnsat
| getAssumptions = do as <- getUnsatAssumptions origNames proxyMap
return (Unsat, Just as)
| True = return (Unsat, Nothing)
parse r bad $ \case ECon "sat" -> return (Sat, Nothing)
ECon "unsat" -> grabUnsat
ECon "unknown" -> return (Unk, Nothing)
_ -> bad r Nothing
-- | Generalization of 'Data.SBV.Control.getAssertionStackDepth'
getAssertionStackDepth :: (MonadIO m, MonadQuery m) => m Int
getAssertionStackDepth = queryAssertionStackDepth <$> getQueryState
-- | Upon a pop, we need to restore all arrays and tables. See: http://github.com/LeventErkok/sbv/issues/374
restoreTablesAndArrays :: (MonadIO m, MonadQuery m) => m ()
restoreTablesAndArrays = do st <- queryState
tCount <- M.size <$> (io . readIORef) (rtblMap st)
let inits = [ "table" ++ show i ++ "_initializer" | i <- [0 .. tCount - 1]]
case inits of
[] -> return () -- Nothing to do
[x] -> send True $ "(assert " ++ x ++ ")"
xs -> send True $ "(assert (and " ++ unwords xs ++ "))"
-- | Generalization of 'Data.SBV.Control.inNewAssertionStack'
inNewAssertionStack :: (MonadIO m, MonadQuery m) => m a -> m a
inNewAssertionStack q = do push 1
r <- q
pop 1
return r
-- | Generalization of 'Data.SBV.Control.push'
push :: (MonadIO m, MonadQuery m) => Int -> m ()
push i
| i <= 0 = error $ "Data.SBV: push requires a strictly positive level argument, received: " ++ show i
| True = do depth <- getAssertionStackDepth
send True $ "(push " ++ show i ++ ")"
modifyQueryState $ \s -> s{queryAssertionStackDepth = depth + i}
-- | Generalization of 'Data.SBV.Control.pop'
pop :: (MonadIO m, MonadQuery m) => Int -> m ()
pop i
| i <= 0 = error $ "Data.SBV: pop requires a strictly positive level argument, received: " ++ show i
| True = do depth <- getAssertionStackDepth
if i > depth
then error $ "Data.SBV: Illegally trying to pop " ++ shl i ++ ", at current level: " ++ show depth
else do QueryState{queryConfig} <- getQueryState
if not (supportsGlobalDecls (capabilities (solver queryConfig)))
then error $ unlines [ ""
, "*** Data.SBV: Backend solver does not support global-declarations."
, "*** Hence, calls to 'pop' are not supported."
, "***"
, "*** Request this as a feature for the underlying solver!"
]
else do send True $ "(pop " ++ show i ++ ")"
restoreTablesAndArrays
modifyQueryState $ \s -> s{queryAssertionStackDepth = depth - i}
where shl 1 = "one level"
shl n = show n ++ " levels"
-- | Generalization of 'Data.SBV.Control.caseSplit'
caseSplit :: (MonadIO m, MonadQuery m) => Bool -> [(String, SBool)] -> m (Maybe (String, SMTResult))
caseSplit printCases cases = do cfg <- getConfig
go cfg (cases ++ [("Coverage", sNot (sOr (map snd cases)))])
where msg = when printCases . io . putStrLn
go _ [] = return Nothing
go cfg ((n,c):ncs) = do let notify s = msg $ "Case " ++ n ++ ": " ++ s
notify "Starting"
r <- checkSatAssuming [c]
case r of
Unsat -> do notify "Unsatisfiable"
go cfg ncs
Sat -> do notify "Satisfiable"
res <- Satisfiable cfg <$> getModel
return $ Just (n, res)
DSat mbP -> do notify $ "Delta satisfiable" ++ maybe "" (" (precision: " ++) mbP
res <- DeltaSat cfg mbP <$> getModel
return $ Just (n, res)
Unk -> do notify "Unknown"
res <- Unknown cfg <$> getUnknownReason
return $ Just (n, res)
-- | Generalization of 'Data.SBV.Control.resetAssertions'
resetAssertions :: (MonadIO m, MonadQuery m) => m ()
resetAssertions = do send True "(reset-assertions)"
modifyQueryState $ \s -> s{ queryAssertionStackDepth = 0 }
-- Make sure we restore tables and arrays after resetAssertions: See: https://github.com/LeventErkok/sbv/issues/535
restoreTablesAndArrays
-- | Generalization of 'Data.SBV.Control.echo'
echo :: (MonadIO m, MonadQuery m) => String -> m ()
echo s = do let cmd = "(echo \"" ++ concatMap sanitize s ++ "\")"
-- we send the command, but otherwise ignore the response
-- note that 'send True/False' would be incorrect here. 'send True' would
-- require a success response. 'send False' would fail to consume the
-- output. But 'ask' does the right thing! It gets "some" response,
-- and forgets about it immediately.
_ <- ask cmd
return ()
where sanitize '"' = "\"\"" -- quotes need to be duplicated
sanitize c = [c]
-- | Generalization of 'Data.SBV.Control.exit'
exit :: (MonadIO m, MonadQuery m) => m ()
exit = do send True "(exit)"
modifyQueryState $ \s -> s{queryAssertionStackDepth = 0}
-- | Generalization of 'Data.SBV.Control.getUnsatCore'
getUnsatCore :: (MonadIO m, MonadQuery m) => m [String]
getUnsatCore = do
let cmd = "(get-unsat-core)"
bad = unexpected "getUnsatCore" cmd "an unsat-core response"
$ Just [ "Make sure you use:"
, ""
, " setOption $ ProduceUnsatCores True"
, ""
, "so the solver will be ready to compute unsat cores,"
, "and that there is a model by first issuing a 'checkSat' call."
, ""
, "If using z3, you might also optionally want to set:"
, ""
, " setOption $ OptionKeyword \":smt.core.minimize\" [\"true\"]"
, ""
, "to make sure the unsat core doesn't have irrelevant entries,"
, "though this might incur a performance penalty."
]
r <- ask cmd
parse r bad $ \case
EApp es | Just xs <- mapM fromECon es -> return $ map unBar xs
_ -> bad r Nothing
-- | Retrieve the unsat core if it was asked for in the configuration
getUnsatCoreIfRequested :: (MonadIO m, MonadQuery m) => m (Maybe [String])
getUnsatCoreIfRequested = do
cfg <- getConfig
if or [b | ProduceUnsatCores b <- solverSetOptions cfg]
then Just <$> getUnsatCore
else return Nothing
-- | Generalization of 'Data.SBV.Control.getProof'
getProof :: (MonadIO m, MonadQuery m) => m String
getProof = do
let cmd = "(get-proof)"
bad = unexpected "getProof" cmd "a get-proof response"
$ Just [ "Make sure you use:"
, ""
, " setOption $ ProduceProofs True"
, ""
, "to make sure the solver is ready for producing proofs,"
, "and that there is a proof by first issuing a 'checkSat' call."
]
r <- ask cmd
-- we only care about the fact that we can parse the output, so the
-- result of parsing is ignored.
parse r bad $ \_ -> return r
-- | Generalization of 'Data.SBV.Control.getInterpolantMathSAT'. Use this version with MathSAT.
getInterpolantMathSAT :: (MonadIO m, MonadQuery m) => [String] -> m String
getInterpolantMathSAT fs
| null fs
= error "SBV.getInterpolantMathSAT requires at least one marked constraint, received none!"
| True
= do let bar s = '|' : s ++ "|"
cmd = "(get-interpolant (" ++ unwords (map bar fs) ++ "))"
bad = unexpected "getInterpolant" cmd "a get-interpolant response"
$ Just [ "Make sure you use:"
, ""
, " setOption $ ProduceInterpolants True"
, ""
, "to make sure the solver is ready for producing interpolants,"
, "and that you have used the proper attributes using the"
, "constrainWithAttribute function."
]
r <- ask cmd
parse r bad $ \e -> return $ serialize False e
-- | Generalization of 'Data.SBV.Control.getAbduct'.
getAbduct :: (SolverContext m, MonadIO m, MonadQuery m) => Maybe String -> String -> SBool -> m String
getAbduct mbGrammar defName b = do
s <- inNewContext (`sbvToSV` b)
let cmd = "(get-abduct " ++ defName ++ " " ++ show s ++ fromMaybe "" mbGrammar ++ ")"
bad = unexpected "getAbduct" cmd "a get-abduct response" Nothing
r <- ask cmd
parse r bad $ \e -> return $ serialize False e
-- | Generalization of 'Data.SBV.Control.getAbductNext'.
getAbductNext :: (MonadIO m, MonadQuery m) => m String
getAbductNext = do
let cmd = "(get-abduct-next)"
bad = unexpected "getAbductNext" cmd "a get-abduct-next response" Nothing
r <- ask cmd
parse r bad $ \e -> return $ serialize False e
-- | Generalization of 'Data.SBV.Control.getInterpolantZ3'. Use this version with Z3.
getInterpolantZ3 :: (MonadIO m, MonadQuery m) => [SBool] -> m String
getInterpolantZ3 fs
| length fs < 2
= error $ "SBV.getInterpolantZ3 requires at least two booleans, received: " ++ show fs
| True
= do ss <- let fAll [] sofar = return $ reverse sofar
fAll (b:bs) sofar = do sv <- inNewContext (`sbvToSV` b)
fAll bs (sv : sofar)
in fAll fs []
let cmd = "(get-interpolant " ++ unwords (map show ss) ++ ")"
bad = unexpected "getInterpolant" cmd "a get-interpolant response" Nothing
r <- ask cmd
parse r bad $ \e -> return $ serialize False e
-- | Generalization of 'Data.SBV.Control.getAssertions'
getAssertions :: (MonadIO m, MonadQuery m) => m [String]
getAssertions = do
let cmd = "(get-assertions)"
bad = unexpected "getAssertions" cmd "a get-assertions response"
$ Just [ "Make sure you use:"
, ""
, " setOption $ ProduceAssertions True"
, ""
, "to make sure the solver is ready for producing assertions."
]
render = serialize False
r <- ask cmd
parse r bad $ \pe -> case pe of
EApp xs -> return $ map render xs
_ -> return [render pe]
-- | Generalization of 'Data.SBV.Control.getAssignment'
getAssignment :: (MonadIO m, MonadQuery m) => m [(String, Bool)]
getAssignment = do
let cmd = "(get-assignment)"
bad = unexpected "getAssignment" cmd "a get-assignment response"
$ Just [ "Make sure you use:"
, ""
, " setOption $ ProduceAssignments True"
, ""
, "to make sure the solver is ready for producing assignments,"
, "and that there is a model by first issuing a 'checkSat' call."
]
-- we're expecting boolean assignment to labels, essentially
grab (EApp [ECon s, ENum (0, _, _)]) = Just (unQuote s, False)
grab (EApp [ECon s, ENum (1, _, _)]) = Just (unQuote s, True)
grab _ = Nothing
r <- ask cmd
parse r bad $ \case EApp ps | Just vs <- mapM grab ps -> return vs
_ -> bad r Nothing
-- | Make an assignment. The type 'Assignment' is abstract, the result is typically passed
-- to 'mkSMTResult':
--
-- @ mkSMTResult [ a |-> 332
-- , b |-> 2.3
-- , c |-> True
-- ]
-- @
--
-- End users should use 'getModel' for automatically constructing models from the current solver state.
-- However, an explicit 'Assignment' might be handy in complex scenarios where a model needs to be
-- created manually.
infix 1 |->
(|->) :: SymVal a => SBV a -> a -> Assignment
SBV a |-> v = case literal v of
SBV (SVal _ (Left cv)) -> Assign a cv
r -> error $ "Data.SBV: Impossible happened in |->: Cannot construct a CV with literal: " ++ show r
-- | Generalization of 'Data.SBV.Control.mkSMTResult'
-- NB. This function does not allow users to create interpretations for UI-Funs. But that's
-- probably not a good idea anyhow. Also, if you use the 'validateModel' or 'optimizeValidateConstraints' features, SBV will
-- fail on models returned via this function.
mkSMTResult :: (MonadIO m, MonadQuery m) => [Assignment] -> m SMTResult
mkSMTResult asgns = do
QueryState{queryConfig} <- getQueryState
inps <- F.toList <$> getTopLevelInputs
let grabValues st = do let extract (Assign s n) = sbvToSV st (SBV s) >>= \sv -> return (sv, n)
modelAssignment <- mapM extract asgns
-- sanity checks
-- - All existentials should be given a value
-- - No duplicates
-- - No bindings to vars that are not inputs
let userSS = map fst modelAssignment
missing, extra, dup :: [String]
missing = [T.unpack n | NamedSymVar s n <- inps, s `notElem` userSS]
extra = [show s | s <- userSS, s `notElem` map getSV inps]
dup = let walk [] = []
walk (n:ns)
| n `elem` ns = show n : walk (filter (/= n) ns)
| True = walk ns
in walk userSS
unless (null (missing ++ extra ++ dup)) $ do
let misTag = "*** Missing inputs"
dupTag = "*** Duplicate bindings"
extTag = "*** Extra bindings"
maxLen = maximum $ 0
: [length misTag | not (null missing)]
++ [length extTag | not (null extra)]
++ [length dupTag | not (null dup)]
align s = s ++ replicate (maxLen - length s) ' ' ++ ": "
error $ unlines $ [""
, "*** Data.SBV: Query model construction has a faulty assignment."
, "***"
]
++ [ align misTag ++ intercalate ", " missing | not (null missing)]
++ [ align extTag ++ intercalate ", " extra | not (null extra) ]
++ [ align dupTag ++ intercalate ", " dup | not (null dup) ]
++ [ "***"
, "*** Data.SBV: Check your query result construction!"
]
let findName s = case [T.unpack nm | NamedSymVar i nm <- inps, s == i] of
[nm] -> nm
[] -> error "*** Data.SBV: Impossible happened: Cannot find " ++ show s ++ " in the input list"
nms -> error $ unlines [ ""
, "*** Data.SBV: Impossible happened: Multiple matches for: " ++ show s
, "*** Candidates: " ++ unwords nms
]
return [(findName s, n) | (s, n) <- modelAssignment]
assocs <- inNewContext grabValues
let m = SMTModel { modelObjectives = []
, modelBindings = Nothing
, modelAssocs = assocs
, modelUIFuns = []
}
return $ Satisfiable queryConfig m