sbv-14.0: Data/SBV/Control/Utils.hs
-----------------------------------------------------------------------------
-- |
-- Module : Data.SBV.Control.Utils
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Query related utils.
-----------------------------------------------------------------------------
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}
module Data.SBV.Control.Utils (
io
, ask, send, getValue, getFunction
, getValueCV, getUICVal, getUIFunCVAssoc, getUnsatAssumptions
, SMTFunction(..), getQueryState, modifyQueryState, getConfig, getObjectives, getUIs
, getSBVAssertions, getSBVPgm, getObservables
, checkSat, checkSatUsing, getAllSatResult
, inNewContext, freshVar, freshVar_
, getTopLevelInputs, parse, unexpected
, timeout, queryDebug, retrieveResponse, recoverKindedValue, runProofOn, executeQuery
, startOptimizer, getObjectiveValues, getModel, getModelAtIndex
) where
import Data.List (sortBy, sortOn, partition, groupBy, tails, intercalate, isPrefixOf, isSuffixOf)
import Data.Char (isPunctuation, isSpace, isDigit)
import Data.Function (on)
import Data.Bifunctor (first)
import Data.Proxy
import qualified Data.Foldable as F (toList)
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set (empty, fromList, toAscList)
import qualified Data.Sequence as S
import qualified Data.Text as T
import Control.Monad (join, unless, zipWithM, when, replicateM, forM_)
import Control.Monad.IO.Class (MonadIO, liftIO)
import Control.Monad.Trans (lift)
import Control.Monad.Reader (runReaderT)
import Data.Maybe (isNothing, isJust, catMaybes, listToMaybe)
import Data.IORef (readIORef, writeIORef, IORef, newIORef, modifyIORef')
import Data.Time (getZonedTime)
import Data.Ratio
import Data.SBV.Core.Data ( SV(..), trueSV, falseSV, CV(..), trueCV, falseCV, SBV, sbvToSV, kindOf, Kind(..)
, HasKind(..), mkConstCV, CVal(..), SMTResult(..)
, NamedSymVar, SMTConfig(..), SMTModel(..)
, QueryState(..), SVal(..), cache
, newExpr, SBVExpr(..), Op(..), FPOp(..), SBV(..)
, SolverContext(..), SBool, Objective(..), SolverCapabilities(..), capabilities
, Result(..), SMTProblem(..), trueSV, SymVal(..), SBVPgm(..), SMTSolver(..), SBVRunMode(..)
, SBVType(..), forceSVArg, RoundingMode(RoundNearestTiesToEven), (.=>)
, RCSet(..), QuantifiedBool(..), ArrayModel(..), SInfo(..), getSInfo
, OptimizeStyle(..), GeneralizedCV(..), ExtCV(..)
)
import Data.SBV.Core.Symbolic ( IncState(..), withNewIncState, State(..), svToSV, symbolicEnv, SymbolicT
, MonadQuery(..), QueryContext(..), VarContext(..)
, registerLabel, svMkSymVar, validationRequested
, isSafetyCheckingIStage, isSetupIStage, isRunIStage, IStage(..), QueryT(..)
, extractSymbolicSimulationState, MonadSymbolic(..)
, UserInputs, getSV, NamedSymVar(..), lookupInput, getUserName'
, Name, CnstMap, Inputs(..), ProgInfo(..)
, mustIgnoreVar, newInternalVariable, Penalty(..)
)
import Data.SBV.Core.AlgReals (mergeAlgReals, AlgReal(..), RealPoint(..))
import Data.SBV.Core.SizedFloats (fpZero, fpFromInteger, fpFromFloat, fpFromDouble)
import Data.SBV.Core.Kind (smtType, hasUninterpretedSorts, expandKinds, isSomeKindOfFloat, substituteADTVars)
import Data.SBV.Core.Operations (svNot, svNotEqual, svOr, svEqual)
import Data.SBV.SMT.SMT (showModel, parseCVs, SatModel, AllSatResult(..), OptimizeResult(..))
import Data.SBV.SMT.SMTLib (toIncSMTLib, toSMTLib)
import Data.SBV.SMT.SMTLib2 (setSMTOption)
import Data.SBV.SMT.Utils ( showTimeoutValue, addAnnotations, alignPlain, debug
, mergeSExpr, SBVException(..), recordTranscript, TranscriptMsg(..)
)
import Data.SBV.Utils.ExtractIO
import Data.SBV.Utils.Lib (qfsToString, unBar)
import Data.SBV.Utils.SExpr
import Data.SBV.Utils.PrettyNum (cvToSMTLib)
import Data.SBV.Control.Types
import qualified Control.Exception as C
import GHC.Stack
-- | 'Data.SBV.Trans.Control.QueryT' as a 'SolverContext'.
instance MonadIO m => SolverContext (QueryT m) where
constrain = addQueryConstraint False [] . quantifiedBool
softConstrain = addQueryConstraint True [] . quantifiedBool
namedConstraint nm = addQueryConstraint False [(":named", nm)] . quantifiedBool
constrainWithAttribute attr = addQueryConstraint False attr . quantifiedBool
contextState = queryState
internalVariable :: forall a. Kind -> QueryT m (SBV a)
internalVariable k = contextState >>= \st -> liftIO $ do
sv <- newInternalVariable st k
pure $ SBV $ SVal k (Right (cache (const (pure sv))))
setOption o
| isStartModeOption o = error $ unlines [ ""
, "*** Data.SBV: '" ++ show o ++ "' can only be set at start-up time."
, "*** Hint: Move the call to 'setOption' before the query."
]
| True = do State{stCfg} <- contextState
send True $ T.unpack $ setSMTOption stCfg o
-- | Adding a constraint, possibly with attributes and possibly soft. Only used internally.
-- Use 'constrain' and 'namedConstraint' from user programs.
addQueryConstraint :: (MonadIO m, MonadQuery m) => Bool -> [(String, String)] -> SBool -> m ()
addQueryConstraint isSoft atts b = do sv <- inNewContext (\st -> liftIO $ do mapM_ (registerLabel "Constraint" st) [nm | (":named", nm) <- atts]
sbvToSV st b)
unless (null atts && sv == trueSV) $
send True $ "(" ++ asrt ++ " " ++ T.unpack (addAnnotations atts (T.pack (show sv))) ++ ")"
where asrt | isSoft = "assert-soft"
| True = "assert"
-- | Get the current configuration
getConfig :: (MonadIO m, MonadQuery m) => m SMTConfig
getConfig = queryConfig <$> getQueryState
-- | Get the objectives
getObjectives :: (MonadIO m, MonadQuery m) => m [Objective (SV, SV)]
getObjectives = do State{rOptGoals} <- queryState
io $ reverse <$> readIORef rOptGoals
-- | Get the program
getSBVPgm :: (MonadIO m, MonadQuery m) => m SBVPgm
getSBVPgm = do State{spgm} <- queryState
io $ readIORef spgm
-- | Get the assertions put in via 'Data.SBV.sAssert'
getSBVAssertions :: (MonadIO m, MonadQuery m) => m [(String, Maybe CallStack, SV)]
getSBVAssertions = do State{rAsserts} <- queryState
io $ reverse <$> readIORef rAsserts
-- | Generalization of 'Data.SBV.Control.io'
io :: MonadIO m => IO a -> m a
io = liftIO
-- | Sync-up the external solver with new context we have generated
syncUpSolver :: (MonadIO m, MonadQuery m) => ProgInfo -> IORef CnstMap -> IncState -> m ()
syncUpSolver progInfo rGlobalConsts is = do
cfg <- getConfig
-- update global consts to have the new ones
(newConsts, allConsts) <- liftIO $ do nc <- readIORef (rNewConsts is)
oc <- readIORef rGlobalConsts
let !allConsts = Map.union nc oc
writeIORef rGlobalConsts allConsts
pure (nc, allConsts)
ls <- io $ do let swap (a, b) = (b, a)
cmp (a, _) (b, _) = a `compare` b
arrange (i, (at, rt, es)) = ((i, at, rt), es)
inps <- reverse <$> readIORef (rNewInps is)
ks <- readIORef (rNewKinds is)
tbls <- map arrange . sortBy cmp . map swap . Map.toList <$> readIORef (rNewTbls is)
uis <- Map.toAscList <$> readIORef (rNewUIs is)
as <- readIORef (rNewAsgns is)
constraints <- readIORef (rNewConstraints is)
let cnsts = sortBy cmp . map swap . Map.toList $ newConsts
return $ map T.unpack $ toIncSMTLib cfg progInfo inps ks (allConsts, cnsts) tbls uis as constraints cfg
mapM_ (send True) $ mergeSExpr ls
-- | Retrieve the query context
getQueryState :: (MonadIO m, MonadQuery m) => m QueryState
getQueryState = do state <- queryState
mbQS <- io $ readIORef (rQueryState state)
case mbQS of
Nothing -> error $ unlines [ ""
, "*** Data.SBV: Impossible happened: Query context required in a non-query mode."
, "Please report this as a bug!"
]
Just qs -> return qs
-- | Generalization of 'Data.SBV.Control.modifyQueryState'
modifyQueryState :: (MonadIO m, MonadQuery m) => (QueryState -> QueryState) -> m ()
modifyQueryState f = do state <- queryState
mbQS <- io $ readIORef (rQueryState state)
case mbQS of
Nothing -> error $ unlines [ ""
, "*** Data.SBV: Impossible happened: Query context required in a non-query mode."
, "Please report this as a bug!"
]
Just qs -> let fqs = f qs
in fqs `seq` io $ writeIORef (rQueryState state) $ Just fqs
-- | Generalization of 'Data.SBV.Control.inNewContext'
inNewContext :: (MonadIO m, MonadQuery m) => (State -> IO a) -> m a
inNewContext act = do st@State{rconstMap, rProgInfo} <- queryState
(is, r) <- io $ withNewIncState st act
progInfo <- io $ readIORef rProgInfo
syncUpSolver progInfo rconstMap is
return r
-- | Generalization of 'Data.SBV.Control.freshVar_'
freshVar_ :: forall a m. (MonadIO m, MonadQuery m, SymVal a) => m (SBV a)
freshVar_ = inNewContext $ fmap SBV . svMkSymVar QueryVar k Nothing
where k = kindOf (Proxy @a)
-- | Generalization of 'Data.SBV.Control.freshVar'
freshVar :: forall a m. (MonadIO m, MonadQuery m, SymVal a) => String -> m (SBV a)
freshVar nm = inNewContext $ fmap SBV . svMkSymVar QueryVar k (Just nm)
where k = kindOf (Proxy @a)
-- | Generalization of 'Data.SBV.Control.queryDebug'
queryDebug :: (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug msgs = do QueryState{queryConfig} <- getQueryState
io $ do debug queryConfig msgs
-- If we're doing a transcript, record it there too
recordTranscript (transcript queryConfig) (DebugMsg (unlines msgs))
-- | We need to track sent asserts/check-sat calls so we can issue an extra check-sat call if needed
trackAsserts :: (MonadIO m, MonadQuery m) => String -> m ()
trackAsserts s
| isCheckSat || isAssert
= do State{rOutstandingAsserts} <- queryState
liftIO $ writeIORef rOutstandingAsserts isAssert
| True
= pure ()
where trimmedS = dropWhile isSpace s
isCheckSat = "(check-sat" `isPrefixOf` trimmedS
isAssert = "(assert" `isPrefixOf` trimmedS
-- | Generalization of 'Data.SBV.Control.ask'
ask :: (MonadIO m, MonadQuery m) => String -> m String
ask s = askIgnoring s []
-- | Send a string to the solver, and return the response. Except, if the response
-- is one of the "ignore" ones, keep querying.
askIgnoring :: (MonadIO m, MonadQuery m) => String -> [String] -> m String
askIgnoring s ignoreList = do
trackAsserts s
QueryState{queryAsk, queryRetrieveResponse, queryTimeOutValue} <- getQueryState
case queryTimeOutValue of
Nothing -> queryDebug ["[SEND] " `alignPlain` s]
Just i -> queryDebug ["[SEND, TimeOut: " ++ showTimeoutValue i ++ "] " `alignPlain` s]
r <- io $ queryAsk queryTimeOutValue s
queryDebug ["[RECV] " `alignPlain` r]
let loop currentResponse
| currentResponse `notElem` ignoreList
= return currentResponse
| True
= do queryDebug ["[WARN] Previous response is explicitly ignored, beware!"]
newResponse <- io $ queryRetrieveResponse queryTimeOutValue
queryDebug ["[RECV] " `alignPlain` newResponse]
loop newResponse
loop r
-- | Generalization of 'Data.SBV.Control.send'
send :: (MonadIO m, MonadQuery m) => Bool -> String -> m ()
send requireSuccess s = do
trackAsserts s
QueryState{queryAsk, querySend, queryConfig, queryTimeOutValue} <- getQueryState
if requireSuccess && supportsCustomQueries (capabilities (solver queryConfig))
then do r <- io $ queryAsk queryTimeOutValue s
case words r of
["success"] -> queryDebug ["[GOOD] " `alignPlain` s]
_ -> do case queryTimeOutValue of
Nothing -> queryDebug ["[FAIL] " `alignPlain` s]
Just i -> queryDebug [("[FAIL, TimeOut: " ++ showTimeoutValue i ++ "] ") `alignPlain` s]
let cmd = case words (dropWhile (\c -> isSpace c || isPunctuation c) s) of
(c:_) -> c
_ -> "Command"
unexpected cmd s "success" Nothing r Nothing
else do -- fire and forget. if you use this, you're on your own!
queryDebug ["[FIRE] " `alignPlain` s]
io $ querySend queryTimeOutValue s
-- | Generalization of 'Data.SBV.Control.retrieveResponse'
retrieveResponse :: (MonadIO m, MonadQuery m) => String -> Maybe Int -> m [String]
retrieveResponse userTag mbTo = do
ts <- io (show <$> getZonedTime)
let synchTag = show $ userTag ++ " (at: " ++ ts ++ ")"
cmd = "(echo " ++ synchTag ++ ")"
queryDebug ["[SYNC] Attempting to synchronize with tag: " ++ synchTag]
send False cmd
QueryState{queryRetrieveResponse} <- getQueryState
let loop sofar = do
s <- io $ queryRetrieveResponse mbTo
-- strictly speaking SMTLib requires solvers to print quotes around
-- echo'ed strings, but they don't always do. Accommodate for that
-- here, though I wish we didn't have to.
if s == synchTag || show s == synchTag
then do queryDebug ["[SYNC] Synchronization achieved using tag: " ++ synchTag]
return $ reverse sofar
else do queryDebug ["[RECV] " `alignPlain` s]
loop (s : sofar)
loop []
-- | Generalization of 'Data.SBV.Control.getValue'
getValue :: (MonadIO m, MonadQuery m, SymVal a) => SBV a -> m a
getValue s = do
sv <- inNewContext (`sbvToSV` s)
-- If we're issuing get-value, we gotta make sure there are no outstanding asserts
-- This can happen if we sent some ourselves. See https://github.com/LeventErkok/sbv/issues/682
outstandingAsserts <- do State{rOutstandingAsserts} <- queryState
liftIO $ readIORef rOutstandingAsserts
when outstandingAsserts $ do
queryDebug ["[NOTE] getValue: There are outstanding asserts. Ensuring we're still sat."]
r <- checkSat
let bad = unexpected "checkSat" "check-sat" "one of sat/unsat/unknown" Nothing (show r) Nothing
case r of
Sat -> pure ()
DSat{} -> pure ()
Unk -> bad
Unsat -> bad
-- Are we in an optimization context? If so, we must ensure that the model is not in an extended field
objs <- getObjectives
unless (null objs) $ do
ovs <- getObjectiveValues
case [() | (_, ExtendedCV _) <- ovs] of
[] -> pure () -- We're good, all objectives are within the domain
_ -> do cfg <- getConfig
m <- getModel
ov <- getObjectiveValues
let mdl = LexicographicResult (SatExtField cfg m{modelObjectives = ov})
align "" = "***"
align l = "*** " ++ l
error $ unlines $ "" : map align ([
"Data.SBV.getValue: The current solver state is satisfiable in an extension field."
, "That is, the optimized values assume epsilon/infinity values."
, ""
, "Calls to getValue is not supported in this context. Instead, use the 'optimize' method"
, "directly and inspect the objective values explicitly."
, ""
, "The current model is:"
, ""
] ++ map (" " ++) (lines (show mdl)))
cv <- getValueCV Nothing sv
return $ fromCV cv
-- | A class which allows for sexpr-conversion to functions
class (HasKind r, SatModel r) => SMTFunction fun a r | fun -> a r where
sexprToArg :: (MonadIO m, SolverContext m) => fun -> [SExpr] -> m (Maybe a)
smtFunName :: (MonadIO m, SolverContext m) => fun -> m ((String, Maybe [String]), Bool)
smtFunSaturate :: fun -> SBV r
smtFunType :: fun -> SBVType
smtFunDefault :: fun -> Maybe r
sexprToFun :: (MonadIO m, SolverContext m, MonadQuery m, MonadSymbolic m, SymVal r) => fun -> (String, SExpr) -> m (Either String ([(a, r)], r))
{-# MINIMAL sexprToArg, smtFunSaturate, smtFunType #-}
-- Given the function, figure out a default "return value"
smtFunDefault _
| let v = defaultKindedValue (kindOf (Proxy @r)), Just (res, []) <- parseCVs [v]
= Just res
| True
= Nothing
-- Given the function, determine what its name is and do some sanity checks
smtFunName f = do st@State{rUIMap} <- contextState
uiMap <- liftIO $ readIORef rUIMap
nm <- findName st uiMap
-- Read the uiMap again here. Why? Because the act of finding the name might've
-- introduced it as an uninterperted name!
newUIMap <- liftIO $ readIORef rUIMap
case nm `Map.lookup` newUIMap of
Nothing -> cantFind newUIMap
Just (isCurried, mbArgs, _) -> pure ((nm, mbArgs), isCurried)
where cantFind uiMap = error $ unlines $ [ ""
, "*** Data.SBV.getFunction: Must be called on an uninterpreted function!"
, "***"
, "*** Expected to receive a function created by \"uninterpret\""
]
++ tag
++ [ "***"
, "*** Make sure to call getFunction on uninterpreted functions only!"
, "*** If that is already the case, please report this as a bug."
]
where tag = case map fst (Map.toList uiMap) of
[] -> [ "*** But, there are no matching uninterpreted functions in the context." ]
[x] -> [ "*** The only possible candidate is: " ++ x ]
cands -> [ "*** Candidates are:"
, "*** " ++ intercalate ", " cands
]
findName st@State{spgm} uiMap = do
r <- liftIO $ sbvToSV st (smtFunSaturate f)
liftIO $ forceSVArg r
SBVPgm asgns <- liftIO $ readIORef spgm
case S.findIndexR ((== r) . fst) asgns of
Nothing -> cantFind uiMap
Just i -> case asgns `S.index` i of
(sv, SBVApp (Uninterpreted nm) _) | r == sv -> return nm
_ -> cantFind uiMap
sexprToFun f (s, e) = do nm <- fst . fst <$> smtFunName f
si <- contextState >>= getSInfo
mbRes <- case parseSExprFunction e of
Just (Left nm') -> case (nm == nm', smtFunDefault f) of
(True, Just v) -> return $ Just ([], v)
_ -> bailOut nm
Just (Right v) -> convert si v
Nothing -> do mbPVS <- pointWiseExtract nm (smtFunType f)
case mbPVS of
Nothing -> pure Nothing
Just pts -> convert si pts
pure $ maybe (Left s) Right mbRes
where convert st (vs, d) = do ps <- mapM (sexprPoint st) vs
pure $ (,) <$> sequenceA ps <*> sexprToVal st d
sexprPoint st (as, v) = do mbA <- sexprToArg f as
pure $ (,) <$> mbA <*> sexprToVal st v
bailOut nm = error $ unlines [ ""
, "*** Data.SBV.getFunction: Unable to extract an interpretation for function " ++ show nm
, "***"
, "*** Failed while trying to extract a pointwise interpretation."
, "***"
, "*** This could be a bug with SBV or the backend solver. Please report!"
]
-- | Pointwise function value extraction. If we get unlucky and can't parse z3's output (happens
-- when we have all booleans and z3 decides to spit out an expression), just brute force our
-- way out of it. Note that we only do this if we have a pure boolean type, as otherwise we'd blow
-- up. And I think it'll only be necessary then, I haven't seen z3 try anything smarter in other scenarios.
pointWiseExtract :: forall m. (MonadIO m, MonadQuery m) => String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
pointWiseExtract nm typ = tryPointWise
where trueSExpr = ENum (1, Nothing, True)
falseSExpr = ENum (0, Nothing, True)
isTrueSExpr (ENum (1, Nothing, True)) = True
isTrueSExpr (ENum (0, Nothing, True)) = False
isTrueSExpr s = error $ "Data.SBV.pointWiseExtract: Impossible happened: Received: " ++ show s
(nArgs, isBoolFunc) = case typ of
SBVType ts -> (length ts - 1, all (== KBool) ts)
getBVal :: [SExpr] -> m ([SExpr], SExpr)
getBVal args = do let shc c | isTrueSExpr c = "true"
| True = "false"
as = unwords $ map shc args
cmd = "(get-value ((" ++ nm ++ " " ++ as ++ ")))"
bad = unexpected "get-value" cmd ("pointwise value of boolean function " ++ nm ++ " on " ++ show as) Nothing
r <- ask cmd
parse r bad $ \case EApp [EApp [_, e]] -> return (args, e)
_ -> bad r Nothing
getBVals :: m [([SExpr], SExpr)]
getBVals = mapM getBVal $ replicateM nArgs [falseSExpr, trueSExpr]
tryPointWise
| not isBoolFunc
= return Nothing
| nArgs < 1
= error $ "Data.SBV.pointWiseExtract: Impossible happened, nArgs < 1: " ++ show nArgs ++ " type: " ++ show typ
| True
= do vs <- getBVals
-- Pick the value that will give us the fewer entries
let (trues, falses) = partition (\(_, v) -> isTrueSExpr v) vs
return $ Just $ if length trues <= length falses
then (trues, falseSExpr)
else (falses, trueSExpr)
-- | For saturation purposes, get a proper argument. The forall quantification
-- is safe here since we only use in smtFunSaturate calls, which looks at the
-- kind stored inside only.
mkSaturatingArg :: forall a. Kind -> SBV a
mkSaturatingArg k = SBV $ SVal k (Left (defaultKindedValue k))
-- | Functions of arity 1
instance ( SymVal a, HasKind a
, SatModel r, HasKind r
) => SMTFunction (SBV a -> SBV r) a r
where
sexprToArg _ [a0] = contextState >>= getSInfo >>= \si -> pure $ sexprToVal si a0
sexprToArg _ _ = pure Nothing
smtFunType _ = SBVType [kindOf (Proxy @a), kindOf (Proxy @r)]
smtFunSaturate f = f $ mkSaturatingArg (kindOf (Proxy @a))
-- | Functions of arity 2
instance ( SymVal a, HasKind a
, SymVal b, HasKind b
, SatModel r, HasKind r
) => SMTFunction (SBV a -> SBV b -> SBV r) (a, b) r
where
sexprToArg _ [a0, a1] = contextState >>= getSInfo >>= \si -> pure $ (,) <$> sexprToVal si a0 <*> sexprToVal si a1
sexprToArg _ _ = pure Nothing
smtFunType _ = SBVType [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @r)]
smtFunSaturate f = f (mkSaturatingArg (kindOf (Proxy @a)))
(mkSaturatingArg (kindOf (Proxy @b)))
-- | Functions of arity 3
instance ( SymVal a, HasKind a
, SymVal b, HasKind b
, SymVal c, HasKind c
, SatModel r, HasKind r
) => SMTFunction (SBV a -> SBV b -> SBV c -> SBV r) (a, b, c) r
where
sexprToArg _ [a0, a1, a2] = contextState >>= getSInfo >>= \si -> pure $ (,,) <$> sexprToVal si a0 <*> sexprToVal si a1 <*> sexprToVal si a2
sexprToArg _ _ = pure Nothing
smtFunType _ = SBVType [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @c), kindOf (Proxy @r)]
smtFunSaturate f = f (mkSaturatingArg (kindOf (Proxy @a)))
(mkSaturatingArg (kindOf (Proxy @b)))
(mkSaturatingArg (kindOf (Proxy @c)))
-- | Functions of arity 4
instance ( SymVal a, HasKind a
, SymVal b, HasKind b
, SymVal c, HasKind c
, SymVal d, HasKind d
, SatModel r, HasKind r
) => SMTFunction (SBV a -> SBV b -> SBV c -> SBV d -> SBV r) (a, b, c, d) r
where
sexprToArg _ [a0, a1, a2, a3] = contextState >>= getSInfo >>= \si -> pure $ (,,,) <$> sexprToVal si a0 <*> sexprToVal si a1 <*> sexprToVal si a2 <*> sexprToVal si a3
sexprToArg _ _ = pure Nothing
smtFunType _ = SBVType [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @c), kindOf (Proxy @d), kindOf (Proxy @r)]
smtFunSaturate f = f (mkSaturatingArg (kindOf (Proxy @a)))
(mkSaturatingArg (kindOf (Proxy @b)))
(mkSaturatingArg (kindOf (Proxy @c)))
(mkSaturatingArg (kindOf (Proxy @d)))
-- | Functions of arity 5
instance ( SymVal a, HasKind a
, SymVal b, HasKind b
, SymVal c, HasKind c
, SymVal d, HasKind d
, SymVal e, HasKind e
, SatModel r, HasKind r
) => SMTFunction (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r) (a, b, c, d, e) r
where
sexprToArg _ [a0, a1, a2, a3, a4] = contextState >>= getSInfo >>= \si -> pure $ (,,,,) <$> sexprToVal si a0 <*> sexprToVal si a1 <*> sexprToVal si a2 <*> sexprToVal si a3 <*> sexprToVal si a4
sexprToArg _ _ = pure Nothing
smtFunType _ = SBVType [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @c), kindOf (Proxy @d), kindOf (Proxy @e), kindOf (Proxy @r)]
smtFunSaturate f = f (mkSaturatingArg (kindOf (Proxy @a)))
(mkSaturatingArg (kindOf (Proxy @b)))
(mkSaturatingArg (kindOf (Proxy @c)))
(mkSaturatingArg (kindOf (Proxy @d)))
(mkSaturatingArg (kindOf (Proxy @e)))
-- | Functions of arity 6
instance ( SymVal a, HasKind a
, SymVal b, HasKind b
, SymVal c, HasKind c
, SymVal d, HasKind d
, SymVal e, HasKind e
, SymVal f, HasKind f
, SatModel r, HasKind r
) => SMTFunction (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r) (a, b, c, d, e, f) r
where
sexprToArg _ [a0, a1, a2, a3, a4, a5] = contextState >>= getSInfo >>= \si -> pure $ (,,,,,) <$> sexprToVal si a0 <*> sexprToVal si a1 <*> sexprToVal si a2 <*> sexprToVal si a3 <*> sexprToVal si a4 <*> sexprToVal si a5
sexprToArg _ _ = pure Nothing
smtFunType _ = SBVType [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @c), kindOf (Proxy @d), kindOf (Proxy @e), kindOf (Proxy @f), kindOf (Proxy @r)]
smtFunSaturate f = f (mkSaturatingArg (kindOf (Proxy @a)))
(mkSaturatingArg (kindOf (Proxy @b)))
(mkSaturatingArg (kindOf (Proxy @c)))
(mkSaturatingArg (kindOf (Proxy @d)))
(mkSaturatingArg (kindOf (Proxy @e)))
(mkSaturatingArg (kindOf (Proxy @f)))
-- | Functions of arity 7
instance ( SymVal a, HasKind a
, SymVal b, HasKind b
, SymVal c, HasKind c
, SymVal d, HasKind d
, SymVal e, HasKind e
, SymVal f, HasKind f
, SymVal g, HasKind g
, SatModel r, HasKind r
) => SMTFunction (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r) (a, b, c, d, e, f, g) r
where
sexprToArg _ [a0, a1, a2, a3, a4, a5, a6] = contextState >>= getSInfo >>= \si -> pure $ (,,,,,,) <$> sexprToVal si a0 <*> sexprToVal si a1 <*> sexprToVal si a2 <*> sexprToVal si a3 <*> sexprToVal si a4 <*> sexprToVal si a5 <*> sexprToVal si a6
sexprToArg _ _ = pure Nothing
smtFunType _ = SBVType [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @c), kindOf (Proxy @d), kindOf (Proxy @e), kindOf (Proxy @f), kindOf (Proxy @g), kindOf (Proxy @r)]
smtFunSaturate f = f (mkSaturatingArg (kindOf (Proxy @a)))
(mkSaturatingArg (kindOf (Proxy @b)))
(mkSaturatingArg (kindOf (Proxy @c)))
(mkSaturatingArg (kindOf (Proxy @d)))
(mkSaturatingArg (kindOf (Proxy @e)))
(mkSaturatingArg (kindOf (Proxy @f)))
(mkSaturatingArg (kindOf (Proxy @g)))
-- | Functions of arity 8
instance ( SymVal a, HasKind a
, SymVal b, HasKind b
, SymVal c, HasKind c
, SymVal d, HasKind d
, SymVal e, HasKind e
, SymVal f, HasKind f
, SymVal g, HasKind g
, SymVal h, HasKind h
, SatModel r, HasKind r
) => SMTFunction (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV h -> SBV r) (a, b, c, d, e, f, g, h) r
where
sexprToArg _ [a0, a1, a2, a3, a4, a5, a6, a7] = contextState >>= getSInfo >>= \si -> pure $ (,,,,,,,) <$> sexprToVal si a0 <*> sexprToVal si a1 <*> sexprToVal si a2 <*> sexprToVal si a3 <*> sexprToVal si a4 <*> sexprToVal si a5 <*> sexprToVal si a6 <*> sexprToVal si a7
sexprToArg _ _ = pure Nothing
smtFunType _ = SBVType [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @c), kindOf (Proxy @d), kindOf (Proxy @e), kindOf (Proxy @f), kindOf (Proxy @g), kindOf (Proxy @h), kindOf (Proxy @r)]
smtFunSaturate f = f (mkSaturatingArg (kindOf (Proxy @a)))
(mkSaturatingArg (kindOf (Proxy @b)))
(mkSaturatingArg (kindOf (Proxy @c)))
(mkSaturatingArg (kindOf (Proxy @d)))
(mkSaturatingArg (kindOf (Proxy @e)))
(mkSaturatingArg (kindOf (Proxy @f)))
(mkSaturatingArg (kindOf (Proxy @g)))
(mkSaturatingArg (kindOf (Proxy @h)))
-- | Curried functions of arity 2
instance ( SymVal a, HasKind a
, SymVal b, HasKind b
, SatModel r, HasKind r
) => SMTFunction ((SBV a, SBV b) -> SBV r) (a, b) r
where
sexprToArg _ [a0, a1] = contextState >>= getSInfo >>= \si -> pure $ (,) <$> sexprToVal si a0 <*> sexprToVal si a1
sexprToArg _ _ = pure Nothing
smtFunType _ = SBVType [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @r)]
smtFunSaturate f = f ( mkSaturatingArg (kindOf (Proxy @a))
, mkSaturatingArg (kindOf (Proxy @b))
)
-- | Curried functions of arity 3
instance ( SymVal a, HasKind a
, SymVal b, HasKind b
, SymVal c, HasKind c
, SatModel r, HasKind r
) => SMTFunction ((SBV a, SBV b, SBV c) -> SBV r) (a, b, c) r
where
sexprToArg _ [a0, a1, a2] = contextState >>= getSInfo >>= \si -> pure $ (,,) <$> sexprToVal si a0 <*> sexprToVal si a1 <*> sexprToVal si a2
sexprToArg _ _ = pure Nothing
smtFunType _ = SBVType [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @c), kindOf (Proxy @r)]
smtFunSaturate f = f ( mkSaturatingArg (kindOf (Proxy @a))
, mkSaturatingArg (kindOf (Proxy @b))
, mkSaturatingArg (kindOf (Proxy @c))
)
-- | Curried functions of arity 4
instance ( SymVal a, HasKind a
, SymVal b, HasKind b
, SymVal c, HasKind c
, SymVal d, HasKind d
, SatModel r, HasKind r
) => SMTFunction ((SBV a, SBV b, SBV c, SBV d) -> SBV r) (a, b, c, d) r
where
sexprToArg _ [a0, a1, a2, a3] = contextState >>= getSInfo >>= \si -> pure $ (,,,) <$> sexprToVal si a0 <*> sexprToVal si a1 <*> sexprToVal si a2 <*> sexprToVal si a3
sexprToArg _ _ = pure Nothing
smtFunType _ = SBVType [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @c), kindOf (Proxy @d), kindOf (Proxy @r)]
smtFunSaturate f = f ( mkSaturatingArg (kindOf (Proxy @a))
, mkSaturatingArg (kindOf (Proxy @b))
, mkSaturatingArg (kindOf (Proxy @c))
, mkSaturatingArg (kindOf (Proxy @d))
)
-- | Curried functions of arity 5
instance ( SymVal a, HasKind a
, SymVal b, HasKind b
, SymVal c, HasKind c
, SymVal d, HasKind d
, SymVal e, HasKind e
, SatModel r, HasKind r
) => SMTFunction ((SBV a, SBV b, SBV c, SBV d, SBV e) -> SBV r) (a, b, c, d, e) r
where
sexprToArg _ [a0, a1, a2, a3, a4] = contextState >>= getSInfo >>= \si -> pure $ (,,,,) <$> sexprToVal si a0 <*> sexprToVal si a1 <*> sexprToVal si a2 <*> sexprToVal si a3 <*> sexprToVal si a4
sexprToArg _ _ = pure Nothing
smtFunType _ = SBVType [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @c), kindOf (Proxy @d), kindOf (Proxy @e), kindOf (Proxy @r)]
smtFunSaturate f = f ( mkSaturatingArg (kindOf (Proxy @a))
, mkSaturatingArg (kindOf (Proxy @b))
, mkSaturatingArg (kindOf (Proxy @c))
, mkSaturatingArg (kindOf (Proxy @d))
, mkSaturatingArg (kindOf (Proxy @e))
)
-- | Curried functions of arity 6
instance ( SymVal a, HasKind a
, SymVal b, HasKind b
, SymVal c, HasKind c
, SymVal d, HasKind d
, SymVal e, HasKind e
, SymVal f, HasKind f
, SatModel r, HasKind r
) => SMTFunction ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> SBV r) (a, b, c, d, e, f) r
where
sexprToArg _ [a0, a1, a2, a3, a4, a5] = contextState >>= getSInfo >>= \si -> pure $ (,,,,,) <$> sexprToVal si a0 <*> sexprToVal si a1 <*> sexprToVal si a2 <*> sexprToVal si a3 <*> sexprToVal si a4 <*> sexprToVal si a5
sexprToArg _ _ = pure Nothing
smtFunType _ = SBVType [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @c), kindOf (Proxy @d), kindOf (Proxy @e), kindOf (Proxy @f), kindOf (Proxy @r)]
smtFunSaturate f = f ( mkSaturatingArg (kindOf (Proxy @a))
, mkSaturatingArg (kindOf (Proxy @b))
, mkSaturatingArg (kindOf (Proxy @c))
, mkSaturatingArg (kindOf (Proxy @d))
, mkSaturatingArg (kindOf (Proxy @e))
, mkSaturatingArg (kindOf (Proxy @f))
)
-- | Curried functions of arity 7
instance ( SymVal a, HasKind a
, SymVal b, HasKind b
, SymVal c, HasKind c
, SymVal d, HasKind d
, SymVal e, HasKind e
, SymVal f, HasKind f
, SymVal g, HasKind g
, SatModel r, HasKind r
) => SMTFunction ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> SBV r) (a, b, c, d, e, f, g) r
where
sexprToArg _ [a0, a1, a2, a3, a4, a5, a6] = contextState >>= getSInfo >>= \si -> pure $ (,,,,,,) <$> sexprToVal si a0 <*> sexprToVal si a1 <*> sexprToVal si a2 <*> sexprToVal si a3 <*> sexprToVal si a4 <*> sexprToVal si a5 <*> sexprToVal si a6
sexprToArg _ _ = pure Nothing
smtFunType _ = SBVType [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @c), kindOf (Proxy @d), kindOf (Proxy @e), kindOf (Proxy @f), kindOf (Proxy @g), kindOf (Proxy @r)]
smtFunSaturate f = f ( mkSaturatingArg (kindOf (Proxy @a))
, mkSaturatingArg (kindOf (Proxy @b))
, mkSaturatingArg (kindOf (Proxy @c))
, mkSaturatingArg (kindOf (Proxy @d))
, mkSaturatingArg (kindOf (Proxy @e))
, mkSaturatingArg (kindOf (Proxy @f))
, mkSaturatingArg (kindOf (Proxy @g))
)
-- | Curried functions of arity 8
instance ( SymVal a, HasKind a
, SymVal b, HasKind b
, SymVal c, HasKind c
, SymVal d, HasKind d
, SymVal e, HasKind e
, SymVal f, HasKind f
, SymVal g, HasKind g
, SymVal h, HasKind h
, SatModel r, HasKind r
) => SMTFunction ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> SBV r) (a, b, c, d, e, f, g, h) r
where
sexprToArg _ [a0, a1, a2, a3, a4, a5, a6, a7] = contextState >>= getSInfo >>= \si -> pure $ (,,,,,,,) <$> sexprToVal si a0 <*> sexprToVal si a1 <*> sexprToVal si a2 <*> sexprToVal si a3 <*> sexprToVal si a4 <*> sexprToVal si a5 <*> sexprToVal si a6 <*> sexprToVal si a7
sexprToArg _ _ = pure Nothing
smtFunType _ = SBVType [kindOf (Proxy @a), kindOf (Proxy @b), kindOf (Proxy @c), kindOf (Proxy @d), kindOf (Proxy @e), kindOf (Proxy @f), kindOf (Proxy @g), kindOf (Proxy @h), kindOf (Proxy @r)]
smtFunSaturate f = f ( mkSaturatingArg (kindOf (Proxy @a))
, mkSaturatingArg (kindOf (Proxy @b))
, mkSaturatingArg (kindOf (Proxy @c))
, mkSaturatingArg (kindOf (Proxy @d))
, mkSaturatingArg (kindOf (Proxy @e))
, mkSaturatingArg (kindOf (Proxy @f))
, mkSaturatingArg (kindOf (Proxy @g))
, mkSaturatingArg (kindOf (Proxy @h))
)
-- Turn "((F (lambda ((x!1 Int)) (+ 3 (* 2 x!1)))))"
-- into something more palatable.
-- If we can't do that, we simply return the input unchanged
trimFunctionResponse :: String -> String -> Bool -> Maybe [String] -> String
trimFunctionResponse resp nm isCurried mbArgs
| Just parsed <- makeHaskellFunction resp nm isCurried mbArgs
= parsed
| True
= def $ case trim resp of
'(':'(':rest | nm `isPrefixOf` rest -> butLast2 $ trim (drop (length nm) rest)
_ -> resp
where trim = dropWhile isSpace
butLast2 = reverse . drop 2 . reverse
def x = nm ++ " = fromSMTLib " ++ x
-- | Generalization of 'Data.SBV.Control.getFunction'
getFunction :: (MonadIO m, MonadQuery m, SolverContext m, MonadSymbolic m, SymVal a, SymVal r, SMTFunction fun a r)
=> fun -> m (Either (String, (Bool, Maybe [String], SExpr)) ([(a, r)], r))
getFunction f = do ((nm, args), isCurried) <- smtFunName f
let cmd = "(get-value (" ++ nm ++ "))"
bad = unexpected "getFunction" cmd "a function value" Nothing
r <- ask cmd
si <- contextState >>= getSInfo
parse r bad $ \case EApp [EApp [ECon o, e]] | o == nm -> do
mbAssocs <- sexprToFun f (trimFunctionResponse r nm isCurried args, e)
case mbAssocs of
Right assocs -> return $ Right assocs
Left raw -> do
let rawRes = Left (raw, (isCurried, args, e))
mbPVS <- pointWiseExtract nm (smtFunType f)
case mbPVS of
Just ps -> do rs <- convert si ps
case rs of
Just x -> return $ Right x
Nothing -> return rawRes
Nothing -> return rawRes
_ -> bad r Nothing
where convert si (vs, d) = do ps <- mapM (sexprPoint si) vs
pure $ (,) <$> sequenceA ps <*> sexprToVal si d
sexprPoint si (as, v) = do mbA <- sexprToArg f as
pure $ (,) <$> mbA <*> sexprToVal si v
-- | Get the value of a term, but in CV form. Used internally. The model-index, in particular is extremely Z3 specific!
getValueCVHelper :: (MonadIO m, MonadQuery m) => Maybe Int -> SV -> m CV
getValueCVHelper mbi s
| s == trueSV
= return trueCV
| s == falseSV
= return falseCV
| True
= extractValue mbi (show s) (kindOf s)
-- | "Make up" a CV for this type. Like zero, but smarter.
defaultKindedValue :: Kind -> CV
defaultKindedValue k = CV k $ cvt k
where cvt :: Kind -> CVal
cvt (KVar s) = error ("defaultKindedValue: Unexpected kind: " ++ s)
cvt KBool = CInteger 0
cvt KBounded{} = CInteger 0
cvt KUnbounded = CInteger 0
cvt KReal = CAlgReal 0
cvt KFloat = CFloat 0
cvt KDouble = CDouble 0
cvt KRational = CRational 0
cvt (KFP eb sb) = CFP (fpZero False eb sb)
cvt KChar = CChar '\NUL' -- why not?
cvt KString = CString ""
cvt (KList _) = CList []
cvt (KSet _) = CSet $ RegularSet Set.empty -- why not? Arguably, could be the universal set
cvt (KTuple ks) = CTuple $ map cvt ks
cvt (KArray _ k2) = CArray $ ArrayModel [] (cvt k2)
cvt (KApp s _) = error ("defaultKindedValue not supported for ADT app: " ++ s) -- tough luck
-- For ADTs, just return the first element if there's any
cvt (KADT s _ cstrs) = case cstrs of
[] -> error ("defaultKindedValue not supported for ADT: " ++ s) -- tough luck
((c, ks) : _) -> CADT (c, [(k, cvt fk) | fk <- ks])
-- | Go from an SExpr directly to a value
sexprToVal :: forall a. SymVal a => SInfo -> SExpr -> Maybe a
sexprToVal si e = fromCV <$> recoverKindedValue si (kindOf (Proxy @a)) e
-- | Recover a given solver-printed value with a possible interpretation
recoverKindedValue :: SInfo -> Kind -> SExpr -> Maybe CV
recoverKindedValue si k e =
case k of
KVar{} -> error $ "Data.SBV.recoverKindedValue: Unexpected var kind: " ++ show k
KApp n ks -> case [(s, ps, cstrs) | KADT s ps cstrs <- sInfoKinds si, s == n] of
[(s, ps, cstr)]
| length ks == length ps -> recoverKindedValue si (KADT s (zip (map fst ps) ks) cstr) e
xs -> error $ unlines [ "Data.SBV.recoverKindedValue: Can't uniquely locate reference to ADT: "
, "***"
, "*** ADT : " ++ show n
, "*** Params : " ++ show ks
, "*** Matched: " ++ show xs
, "*** Expr : " ++ show e
, "***"
, "*** Please report this as a bug."
]
KBool | ENum (i, _, _) <- e -> Just $ mkConstCV k i
| True -> Nothing
KBounded{} | ENum (i, _, _) <- e -> Just $ mkConstCV k i
| True -> Nothing
KUnbounded | ENum (i, _, _) <- e -> Just $ mkConstCV k i
| True -> Nothing
KReal | ENum (i, _, _) <- e -> Just $ mkConstCV k i
| EReal i <- e -> Just $ CV KReal (CAlgReal i)
| True -> interpretInterval e
KADT nm dict def -> let k' = KADT nm dict [(c, map (substituteADTVars nm dict) ks) | (c, ks) <- def]
in Just $ CV k' $ CADT $ interpretADT k' e
KFloat | ENum (i, _, _) <- e -> Just $ mkConstCV k i
| EFloat i <- e -> Just $ CV KFloat (CFloat i)
| True -> Nothing
KDouble | ENum (i, _, _) <- e -> Just $ mkConstCV k i
| EDouble i <- e -> Just $ CV KDouble (CDouble i)
| True -> Nothing
KFP eb sb | ENum (i, _, _) <- e -> Just $ CV k $ CFP $ fpFromInteger eb sb i
| EFloat f <- e -> Just $ CV k $ CFP $ fpFromFloat eb sb f
| EDouble d <- e -> Just $ CV k $ CFP $ fpFromDouble eb sb d
| EFloatingPoint c <- e -> Just $ CV k $ CFP c
| True -> Nothing
KChar | ECon s <- e -> Just $ CV KChar $ CChar $ interpretChar s
| True -> Nothing
KString | ECon s <- e -> Just $ CV KString $ CString $ interpretString s
| True -> Nothing
KRational -> Just $ CV k $ CRational $ interpretRational e
KList ek -> Just $ CV k $ CList $ interpretList ek e
KSet ek -> Just $ CV k $ CSet $ interpretSet ek e
KTuple{} -> Just $ CV k $ CTuple $ interpretTuple e
KArray k1 k2 -> Just $ CV k $ CArray $ interpretArray k1 k2 e
where stringLike xs = length xs >= 2 && "\"" `isPrefixOf` xs && "\"" `isSuffixOf` xs
-- Make sure strings are really strings
interpretString xs
| not (stringLike xs)
= error $ "Expected a string constant with quotes, received: <" ++ xs ++ ">"
| True
= qfsToString $ drop 1 (init xs)
interpretChar xs = case interpretString xs of
[c] -> c
_ -> error $ "Expected a singleton char constant, received: <" ++ xs ++ ">"
interpretRational (EApp [ECon "SBV.Rational", v1, v2])
| Just (CV _ (CInteger n)) <- recoverKindedValue si KUnbounded v1
, Just (CV _ (CInteger d)) <- recoverKindedValue si KUnbounded v2
= n % d
interpretRational xs = error $ "Expected a rational constant, received: <" ++ show xs ++ ">"
interpretList ek topExpr = walk topExpr
where walk (EApp [ECon "as", v, _]) = walk v
walk (ECon "seq.empty") = []
walk (EApp [ECon "seq.unit", v]) = case recoverKindedValue si ek v of
Just w -> [cvVal w]
Nothing -> error $ "Cannot parse a sequence item of kind " ++ show ek ++ " from: " ++ show v ++ extra v
walk (EApp (ECon "seq.++" : rest)) = concatMap walk rest
walk cur = error $ "Expected a sequence constant, but received: " ++ show cur ++ extra cur
extra cur | show cur == t = ""
| True = "\nWhile parsing: " ++ t
where t = show topExpr
-- Essentially treat sets as functions, since we do allow for store associations
interpretSet ke setExpr
| isUniversal setExpr = ComplementSet Set.empty
| isEmpty setExpr = RegularSet Set.empty
| Just (Right assocs) <- mbAssocs = decode assocs
| True = tbd "Expected a set value, but couldn't decipher the solver output."
where tbd :: String -> a
tbd w = error $ unlines [ ""
, "*** Data.SBV.interpretSet: Unable to process solver output."
, "***"
, "*** Kind : " ++ show (KSet ke)
, "*** Received: " ++ show setExpr
, "*** Reason : " ++ w
, "***"
, "*** This is either a bug or something SBV currently does not support."
, "*** Please report this as a feature request!"
]
isTrue (ENum (1, Nothing, True)) = True
isTrue (ENum (0, Nothing, True)) = False
isTrue bad = tbd $ "Non-boolean membership value seen: " ++ show bad
isUniversal (EApp [EApp [ECon "as", ECon "const", EApp [ECon "Array", _, ECon "Bool"]], r]) = isTrue r
isUniversal _ = False
isEmpty (EApp [EApp [ECon "as", ECon "const", EApp [ECon "Array", _, ECon "Bool"]], r]) = not $ isTrue r
isEmpty _ = False
mbAssocs = parseSExprFunction setExpr
decode (args, r) | isTrue r = ComplementSet $ Set.fromList [x | (x, False) <- concatMap (contents True) args] -- deletions from universal
| True = RegularSet $ Set.fromList [x | (x, True) <- concatMap (contents False) args] -- additions to empty
contents cvt ([v], r) = let t = isTrue r in map (, t) (element cvt v)
contents _ bad = tbd $ "Multi-valued set member seen: " ++ show bad
element cvt x = case (cvt, ke) of
(True, KChar) -> case recoverKindedValue si KString x of
Just v -> case cvVal v of
CString [c] -> [CChar c]
CString _ -> []
_ -> tbd $ "Unexpected value for kind: " ++ show (x, ke)
Nothing -> tbd $ "Unexpected value for kind: " ++ show (x, ke)
_ -> case recoverKindedValue si ke x of
Just v -> [cvVal v]
Nothing -> tbd $ "Unexpected value for kind: " ++ show (x, ke)
interpretTuple te = walk (1 :: Int) (zipWith (recoverKindedValue si) ks args) []
where (ks, n) = case k of
KTuple eks -> (eks, length eks)
_ -> error $ unlines [ "Impossible: Expected a tuple kind, but got: " ++ show k
, "While trying to parse: " ++ show te
]
-- | Convert a sexpr of n-tuple to constituent sexprs. Z3 and CVC4 differ here on how they
-- present tuples, so we accommodate both:
args = try te
where -- Z3 way
try (EApp (ECon f : as)) = case splitAt (T.length "mkSBVTuple") f of
("mkSBVTuple", c) | all isDigit c && read c == n && length as == n -> as
_ -> bad
-- CVC4 way
try (EApp (EApp [ECon "as", ECon f, _] : as)) = try (EApp (ECon f : as))
try _ = bad
bad = error $ "Data.SBV.sexprToTuple: Impossible: Expected a constructor for " ++ show n ++ " tuple, but got: " ++ show te
walk _ [] sofar = reverse sofar
walk i (Just el:es) sofar = walk (i+1) es (cvVal el : sofar)
walk i (Nothing:_) _ = error $ unlines [ "Couldn't parse a tuple element at position " ++ show i
, "Kind: " ++ show k
, "Expr: " ++ show te
]
-- Intervals, for dReal
interpretInterval expr = case expr of
EApp [ECon "interval", lo, hi] -> do vlo <- getBorder lo
vhi <- getBorder hi
pure $ CV KReal (CAlgReal (AlgInterval vlo vhi))
_ -> Nothing
where getBorder (EApp [ECon "open", v]) = recoverKindedValue si KReal v >>= border OpenPoint
getBorder (EApp [ECon "closed", v]) = recoverKindedValue si KReal v >>= border ClosedPoint
getBorder _ = Nothing
border b (CV KReal (CAlgReal (AlgRational True v))) = pure $ b v
border _ other = error $ "Data.SBV.interpretInterval.border: Expected a real-valued sexp, but received: " ++ show other
-- Essentially treat sets as functions, since we do allow for store associations
interpretArray k1 k2 expr = case parseSExprFunction expr of
Just (Right ascs) -> decode ascs
_ -> tbd "Expected a set value, but couldn't decipher the solver output."
where tbd :: String -> a
tbd w = error $ unlines [ ""
, "*** Data.SBV.interpretArray: Unable to process solver output."
, "***"
, "*** Kind : " ++ show k
, "*** Received: " ++ show e
, "*** Reason : " ++ w
, "***"
, "*** This is either a bug or something SBV currently does not support."
, "*** Please report this as a feature request!"
]
decode (args, d) = ArrayModel [(cvt k1 l, cvt k2 [r]) | (l, r) <- args] (cvt k2 [d])
where cvt ek [v] = case recoverKindedValue si ek v of
Just (CV _ x) -> x
_ -> tbd $ "Cannot convert value: " ++ show v
cvt _ vs = tbd $ "Unexpected function-like-value as array index" ++ show vs
interpretADT :: Kind -> SExpr -> (String, [(Kind, CVal)])
interpretADT adtK@(KADT _ _ cks) expr
| isUninterpreted adtK
= case expr of
ECon s -> (simplifyECon s, [])
_ -> bad ["Unexpected expression value for uninterpreted kind."]
| Just ks <- cstr `lookup` cks
= if length fs == length ks
then (cstr, zipWith convert (zip [1..] ks) fs)
else bad ["Mismatching field count: " ++ show (fs, ks)]
| True
= bad ["Cannot find constructor in the kind: " ++ show (cstr, adtK)]
where (cstr, fs) = case removeAS expr of
ECon c -> (c, [])
EApp (ECon c : cs) -> (c, cs)
_ -> bad ["Unexpected expression value; does not start with a constructor."]
removeAS :: SExpr -> SExpr
removeAS (EApp [ECon "as", i, _]) = removeAS i
removeAS (EApp xs) = EApp $ map removeAS xs
removeAS ae = ae
bad :: [String] -> a
bad extras = error $ unlines $ [ "Data.SBV.interpretADT: Cannot recover ADT value from solver output."
, " Kind: " ++ show adtK
, " Expr: " ++ show expr
] ++ extras
convert :: (Int, Kind) -> SExpr -> (Kind, CVal)
convert (i, fk) f = case recoverKindedValue si fk f of
Just (CV kv v) -> (kv, v)
Nothing -> bad ["Couldn't convert field " ++ show i ++ ": " ++ show (fk, f)]
interpretADT someK expr = error $ unlines [ "Data.SBV.interpretADT: Expected an ADT kind, but got something else."
, " Expr: " ++ show expr
, " Kind: " ++ show someK
]
-- | Generalization of 'Data.SBV.Control.getValueCV'
getValueCV :: (MonadIO m, MonadQuery m) => Maybe Int -> SV -> m CV
getValueCV mbi s
| kindOf s /= KReal
= getValueCVHelper mbi s
| True
= do cfg <- getConfig
if not (supportsApproxReals (capabilities (solver cfg)))
then getValueCVHelper mbi s
else do send True "(set-option :pp.decimal false)"
rep1 <- getValueCVHelper mbi s
send True "(set-option :pp.decimal true)"
send True $ "(set-option :pp.decimal_precision " ++ show (printRealPrec cfg) ++ ")"
rep2 <- getValueCVHelper mbi s
let bad = unexpected "getValueCV" "get-value" ("a real-valued binding for " ++ show s) Nothing (show (rep1, rep2)) Nothing
case (rep1, rep2) of
(CV KReal (CAlgReal a), CV KReal (CAlgReal b)) -> return $ CV KReal (CAlgReal (mergeAlgReals ("Cannot merge real-values for " ++ show s) a b))
_ -> bad
-- | Retrieve value from the solver
extractValue :: forall m. (MonadIO m, MonadQuery m) => Maybe Int -> String -> Kind -> m CV
extractValue mbi nm k = do
let modelIndex = case mbi of
Nothing -> ""
Just i -> " :model_index " ++ show i
cmd = "(get-value (" ++ nm ++ ")" ++ modelIndex ++ ")"
bad = unexpected "get-value" cmd ("a value binding for kind: " ++ show k) Nothing
r <- ask cmd
si <- queryState >>= getSInfo
let recover val = case recoverKindedValue si k val of
Just cv -> return cv
Nothing -> bad r Nothing
parse r bad $ \case EApp [EApp [ECon v, val]] | v == nm -> recover val
_ -> bad r Nothing
-- | Generalization of 'Data.SBV.Control.getUICVal'
getUICVal :: forall m. (MonadIO m, MonadQuery m) => Maybe Int -> (String, (Bool, Maybe [String], SBVType)) -> m CV
getUICVal mbi (nm, (_, _, t)) = case t of
SBVType [k] -> extractValue mbi nm k
_ -> error $ "SBV.getUICVal: Expected to be called on an uninterpeted value of a base type, received something else: " ++ show (nm, t)
-- | Generalization of 'Data.SBV.Control.getUIFunCVAssoc'
getUIFunCVAssoc :: forall m. (MonadIO m, MonadQuery m) => Maybe Int -> (String, (Bool, Maybe [String], SBVType)) -> m (Either String ([([CV], CV)], CV))
getUIFunCVAssoc mbi (nm, (isCurried, mbArgs, typ)) = do
let modelIndex = case mbi of
Nothing -> ""
Just i -> " :model_index " ++ show i
cmd = "(get-value (" ++ nm ++ ")" ++ modelIndex ++ ")"
bad = unexpected "get-value" cmd "a function value" Nothing
r <- ask cmd
si <- queryState >>= getSInfo
let (ats, rt) = case typ of
SBVType as | length as > 1 -> (init as, last as)
_ -> error $ "Data.SBV.getUIFunCVAssoc: Expected a function type, got: " ++ show typ
let convert (vs, d) = (,) <$> mapM toPoint vs <*> toRes d
toPoint (as, v)
| length as == length ats = (,) <$> zipWithM (recoverKindedValue si) ats as <*> toRes v
| True = error $ "Data.SBV.getUIFunCVAssoc: Mismatching type/value arity, got: " ++ show (as, ats)
toRes :: SExpr -> Maybe CV
toRes = recoverKindedValue si rt
-- if we fail to parse, we'll return this answer as the string
fallBack = trimFunctionResponse r nm isCurried mbArgs
-- In case we end up in the pointwise scenario, boolify the result
-- as that's the only type we support here.
tryPointWise = do mbSExprs <- pointWiseExtract nm typ
case mbSExprs of
Nothing -> pure $ Left fallBack
Just sExprs -> pure $ maybe (Left fallBack) Right (convert sExprs)
parse r bad $ \case EApp [EApp [ECon o, e]] | o == nm -> case parseSExprFunction e of
Just (Right assocs) | Just res <- convert assocs -> return (Right res)
| True -> tryPointWise
Just (Left nm') | nm == nm', let res = defaultKindedValue rt -> return (Right ([], res))
| True -> bad r Nothing
Nothing -> tryPointWise
_ -> bad r Nothing
-- | Generalization of 'Data.SBV.Control.checkSat'
checkSat :: (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat = do cfg <- getConfig
checkSatUsing $ satCmd cfg
-- | Generalization of 'Data.SBV.Control.checkSatUsing'
checkSatUsing :: (MonadIO m, MonadQuery m) => String -> m CheckSatResult
checkSatUsing cmd = do let bad = unexpected "checkSat" cmd "one of sat/unsat/unknown" Nothing
-- Sigh.. Ignore some of the pesky warnings. We only do it as an exception here.
ignoreList = ["WARNING: optimization with quantified constraints is not supported"]
r <- askIgnoring cmd ignoreList
-- query for the precision if supported
let getPrecision = do cfg <- getConfig
case supportsDeltaSat (capabilities (solver cfg)) of
Nothing -> pure Nothing
Just o -> Just <$> ask o
parse r bad $ \case ECon "sat" -> return Sat
ECon "unsat" -> return Unsat
ECon "unknown" -> return Unk
ECon "delta-sat" -> DSat <$> getPrecision
_ -> bad r Nothing
-- | What are the top level inputs? Trackers are returned as top level existentials
getTopLevelInputs :: (MonadIO m, MonadQuery m) => m UserInputs
getTopLevelInputs = do State{rinps} <- queryState
Inputs{userInputs, internInputs} <- liftIO $ readIORef rinps
pure $ userInputs <> internInputs
-- | Get observables, i.e., those explicitly labeled by the user with a call to 'Data.SBV.observe'.
getObservables :: (MonadIO m, MonadQuery m) => m [(Name, CV)]
getObservables = do State{rObservables} <- queryState
rObs <- liftIO $ readIORef rObservables
-- This intentionally reverses the result; since 'rObs' stores in reversed order
let walk [] !sofar = return sofar
walk ((n, f, s):os) !sofar = do cv <- getValueCV Nothing s
if f cv
then walk os ((n, cv) : sofar)
else walk os sofar
walk (F.toList rObs) []
-- | Get UIs, both constants and functions. This call returns both the before and after query ones.
-- Generalization of 'Data.SBV.Control.getUIs'.
getUIs :: forall m. (MonadIO m, MonadQuery m) => m [(String, (Bool, Maybe [String], SBVType))]
getUIs = do State{rUIMap, rDefns, rIncState} <- queryState
-- NB. no need to worry about new-defines, because we don't allow definitions once query mode starts
defineSet <- Map.keysSet <$> io (readIORef rDefns)
prior <- io $ readIORef rUIMap
new <- io $ readIORef rIncState >>= readIORef . rNewUIs
return $ Map.toList $ Map.withoutKeys (Map.union prior new) defineSet
-- | Return all satisfying models.
getAllSatResult :: forall m. (MonadIO m, MonadQuery m, SolverContext m) => m AllSatResult
getAllSatResult = do queryDebug ["*** Checking Satisfiability, all solutions.."]
cfg <- getConfig
unless (supportsCustomQueries (capabilities (solver cfg))) $
error $ unlines [ ""
, "*** Data.SBV: Backend solver " ++ show (name (solver cfg)) ++ " does not support custom queries."
, "***"
, "*** Custom query support is needed for allSat functionality."
, "*** Please use a solver that supports this feature."
]
topState@State{rUsedKinds, rPartitionVars, rProgInfo} <- queryState
progInfo <- liftIO $ readIORef rProgInfo
ki <- liftIO $ readIORef rUsedKinds
allModelInputs <- getTopLevelInputs
allUninterpreteds <- getUIs
partitionVars <- liftIO $ readIORef rPartitionVars
-- Functions have at least two kinds in their type and all components must be "interpreted"
let allUiFuns = [u | allSatTrackUFs cfg -- config says consider UIFs
, u@(nm, (_, _, SBVType as)) <- allUninterpreteds, length as > 1 -- get the function ones
, not (mustIgnoreVar cfg nm) -- make sure they aren't explicitly ignored
]
allUiRegs = [u | u@(nm, (_, _, SBVType as)) <- allUninterpreteds, length as == 1 -- non-function ones
, not (mustIgnoreVar cfg nm) -- make sure they aren't explicitly ignored
]
-- We can only "allSat" if all component types themselves are interpreted. (Otherwise
-- there is no way to reflect back the values to the solver.)
collectAcceptable [] sofar = return sofar
collectAcceptable ((nm, (_, _, t@(SBVType ats))):rest) sofar
| not (any hasUninterpretedSorts ats)
= collectAcceptable rest (nm : sofar)
| True
= do queryDebug [ "*** SBV.allSat: Uninterpreted function: " ++ nm ++ " :: " ++ show t
, "*** Will *not* be used in allSat considerations since its type"
, "*** has uninterpreted sorts present."
]
collectAcceptable rest sofar
uiFuns <- reverse <$> collectAcceptable allUiFuns []
_ <- collectAcceptable allUiRegs [] -- only done to get the queryDebug output. Actual result not needed/used
-- If there are uninterpreted functions, arrange so that z3's pretty-printer flattens things out
-- as cex's tend to get larger
unless (null uiFuns) $
let solverCaps = capabilities (solver cfg)
in case supportsFlattenedModels solverCaps of
Nothing -> return ()
Just cmds -> mapM_ (send True) cmds
let usorts = [s | us@(KADT s _ _) <- Set.toAscList ki, isUninterpreted us]
unless (null usorts) $ queryDebug [ "*** SBV.allSat: Uninterpreted sorts present: " ++ unwords usorts
, "*** SBV will use equivalence classes to generate all-satisfying instances."
]
-- Drop the things that are not model vars or internal
let mkSVal nm@(getSV -> sv) = (SVal (kindOf sv) (Right (cache (const (return sv)))), nm)
let extractVars :: S.Seq (SVal, NamedSymVar)
extractVars = mkSVal <$> S.filter (not . mustIgnoreVar cfg . getUserName') allModelInputs
vars :: S.Seq (SVal, NamedSymVar)
vars = case partitionVars of
[] -> extractVars
pv -> mkSVal <$> S.filter (\k -> getUserName' k `elem` pv) allModelInputs
-- We can go fast using the disjoint model trick if things are simple enough:
-- - No uninterpreted functions (uninterpreted values are OK)
-- - No uninterpreted sorts
-- - No quantifiers
--
-- Why can't we support the above?
-- - Uninterpreted functions: There is no (standard) way to define a function as a literal in SMTLib.
-- Some solvers support lambda, but this isn't common/reliable yet.
-- - Uninterpreted sort: There's no way to access the value the solver assigns to an uninterpreted sort.
-- - Quantifiers: Too complicated!
--
-- So, if these two things are present, we go the "slow" route, by repeatedly rejecting the
-- previous model and asking for a new one. If they don't exist (which is the common case anyhow)
-- we use an idea due to z3 folks <http://theory.stanford.edu/%7Enikolaj/programmingz3.html#sec-blocking-evaluations>
-- which splits the search space into disjoint models and can produce results much more quickly.
let isSimple = null allUiFuns && null usorts && not (hasQuants progInfo)
start = AllSatResult { allSatMaxModelCountReached = False
, allSatSolverReturnedUnknown = False
, allSatSolverReturnedDSat = False
, allSatResults = []
}
-- partition-variables are only supported if simple
case partitionVars of
[] -> pure ()
xs -> unless isSimple $ error $ unlines [ ""
, "Data.SBV: Unsupported complex allSat call in the presence of partition-variables"
, ""
, "Partition variables are only supported when there are no uninterpreted"
, "functions or uninterpreted sorts."
, ""
, "Saw parition vars: " ++ unwords xs
]
if isSimple
then do let mkVar :: (String, (Bool, Maybe [String], SBVType)) -> IO (SVal, NamedSymVar)
mkVar (nm, (_, _, SBVType [k])) = do sv <- newExpr topState k (SBVApp (Uninterpreted nm) [])
let sval = SVal k $ Right $ cache $ \_ -> pure sv
nsv = NamedSymVar sv (T.pack nm)
pure (sval, nsv)
mkVar nmt = error $ "Data.SBV: Impossible happened; allSat.mkVar. Unexpected: " ++ show nmt
uiVars <- io $ S.fromList <$> mapM mkVar allUiRegs
fastAllSat allModelInputs (uiVars S.>< extractVars) (uiVars S.>< vars) cfg start
else loop topState (allUiFuns, uiFuns) allUiRegs allModelInputs vars cfg start
where finalize cnt cfg sofar extra
= when (allSatPrintAlong cfg && not (null (allSatResults sofar))) $ do
let msg 0 = "No solutions found."
msg 1 = "This is the only solution."
msg n = "Found " ++ show n ++ " different solutions."
io . putStrLn $ msg (cnt - 1)
case extra of
Nothing -> pure ()
Just m -> io $ putStrLn m
fastAllSat :: S.Seq NamedSymVar -> S.Seq (SVal, NamedSymVar) -> S.Seq (SVal, NamedSymVar) -> SMTConfig -> AllSatResult -> m AllSatResult
fastAllSat allInputs extractVars vars cfg start = do
result <- io $ newIORef (0, start, False, Nothing)
go result vars
(found, sofar, _, extra) <- io $ readIORef result
finalize (found+1) cfg sofar extra
pure sofar
where haveEnough have = case allSatMaxModelCount cfg of
Just maxModels -> have >= maxModels
_ -> False
go :: IORef (Int, AllSatResult, Bool, Maybe String) -> S.Seq (SVal, NamedSymVar) -> m ()
go finalResult = walk True
where shouldContinue = do (have, _, exitLoop, _) <- io $ readIORef finalResult
pure $ not (exitLoop || haveEnough have)
walk :: Bool -> S.Seq (SVal, NamedSymVar) -> m ()
walk firstRun terms
| not firstRun && S.null terms
= pure ()
| True
= do mbCont <- do (have, sofar, exitLoop, _) <- io $ readIORef finalResult
if exitLoop
then pure Nothing
else case allSatMaxModelCount cfg of
Just maxModels
| have >= maxModels -> do unless (allSatMaxModelCountReached sofar) $ do
queryDebug ["*** Maximum model count request of " ++ show maxModels ++ " reached, stopping the search."]
when (allSatPrintAlong cfg) $ io $ putStrLn "Search stopped since model count request was reached."
io $ modifyIORef' finalResult $ \(h, s, _, m) -> (h, s{ allSatMaxModelCountReached = True }, True, m)
pure Nothing
_ -> pure $ Just $ have+1
case mbCont of
Nothing -> pure ()
Just cnt -> do
queryDebug ["Fast allSat, Looking for solution " ++ show cnt]
cs <- checkSat
case cs of
Unsat -> pure ()
Unk -> do let m = "Solver returned unknown, terminating query."
queryDebug ["*** " ++ m]
io $ modifyIORef' finalResult $ \(h, s, _, _) -> (h, s{allSatSolverReturnedUnknown = True}, True, Just ("[" ++ m ++ "]"))
DSat _ -> do let m = "Solver returned delta-sat, terminating query."
queryDebug ["*** " ++ m]
io $ modifyIORef' finalResult $ \(h, s, _, _) -> (h, s{allSatSolverReturnedDSat = True}, True, Just ("[" ++ m ++ "]"))
Sat -> do assocs <- mapM (\(sval, NamedSymVar sv n) -> do !cv <- getValueCV Nothing sv
return (sv, (n, (sval, cv)))) extractVars
bindings <- let grab i@(getSV -> sv) = case lookupInput fst sv assocs of
Just (_, (_, (_, cv))) -> return (i, cv)
Nothing -> do !cv <- getValueCV Nothing sv
return (i, cv)
in if validationRequested cfg
then Just <$> mapM grab allInputs
else return Nothing
obsvs <- getObservables
let lassocs = F.toList assocs
model = SMTModel { modelObjectives = []
, modelBindings = F.toList <$> bindings
, modelAssocs = (first T.unpack <$> sortOn fst obsvs)
<> [(T.unpack n, cv) | (_, (n, (_, cv))) <- lassocs]
, modelUIFuns = []
}
currentResult = Satisfiable cfg model
io $ modifyIORef' finalResult $ \(h, s, e, m) -> let h' = h+1 in h' `seq` (h', s{allSatResults = currentResult : allSatResults s}, e, m)
when (allSatPrintAlong cfg) $ do
io $ putStrLn $ "Solution #" ++ show cnt ++ ":"
io $ putStrLn $ showModel cfg model
let findVal :: (SVal, NamedSymVar) -> (SVal, CV)
findVal (_, NamedSymVar sv nm) = case F.toList (S.filter (\(sv', _) -> sv == sv') assocs) of
[(_, (_, scv))] -> scv
_ -> error $ "Data.SBV: Cannot uniquely determine " ++ show nm ++ " in " ++ show assocs
cstr :: Bool -> (SVal, CV) -> m ()
cstr shouldReject (sv, cv) = constrain (SBV $ mkEq (kindOf sv) sv (SVal (kindOf sv) (Left cv)) :: SBool)
where mkEq :: Kind -> SVal -> SVal -> SVal
mkEq k a b
| any isSomeKindOfFloat (expandKinds k)
= if shouldReject
then svNot (a `fpEq` b)
else a `fpEq` b
| True
= if shouldReject
then a `svNotEqual` b
else a `svEqual` b
fpEq a b = SVal KBool $ Right $ cache r
where r st = do sva <- svToSV st a
svb <- svToSV st b
newExpr st KBool (SBVApp (IEEEFP FP_ObjEqual) [sva, svb])
reject, accept :: (SVal, NamedSymVar) -> m ()
reject = cstr True . findVal
accept = cstr False . findVal
scope :: (SVal, NamedSymVar) -> S.Seq (SVal, NamedSymVar) -> m () -> m ()
scope cur pres c = do
send True "(push 1)"
reject cur
mapM_ accept pres
r <- c
send True "(pop 1)"
pure r
forM_ [0 .. length terms - 1] $ \i -> do
sc <- shouldContinue
when sc $ do case S.splitAt i terms of
(pre, rest@(cur S.:<| _)) -> scope cur pre $ walk False rest
_ -> error "Data.SBV.allSat: Impossible happened, ran out of terms!"
-- All sat loop. This is slower, as it implements the reject-the-previous model and loop around logic. But
-- it can handle uninterpreted sorts; so we keep it here as a fall-back.
loop topState (allUiFuns, uiFunsToReject) allUiRegs allInputs vars cfg = go (1::Int)
where go :: Int -> AllSatResult -> m AllSatResult
go !cnt !sofar
| Just maxModels <- allSatMaxModelCount cfg, cnt > maxModels
= do queryDebug ["*** Maximum model count request of " ++ show maxModels ++ " reached, stopping the search."]
when (allSatPrintAlong cfg) $ io $ putStrLn "Search stopped since model count request was reached."
return $! sofar { allSatMaxModelCountReached = True }
| True
= do queryDebug ["Looking for solution " ++ show cnt]
cs <- checkSat
let endMsg = finalize cnt cfg sofar
case cs of
Unsat -> do endMsg Nothing
return sofar
Unk -> do let m = "Solver returned unknown, terminating query."
queryDebug ["*** " ++ m]
endMsg $ Just $ "[" ++ m ++ "]"
return sofar{ allSatSolverReturnedUnknown = True }
DSat _ -> do let m = "Solver returned delta-sat, terminating query."
queryDebug ["*** " ++ m]
endMsg $ Just $ "[" ++ m ++ "]"
return sofar{ allSatSolverReturnedDSat = True }
Sat -> do assocs <- mapM (\(sval, NamedSymVar sv n) -> do !cv <- getValueCV Nothing sv
return (sv, (n, (sval, cv)))) vars
let getUIFun ui@(nm, (isCurried, _, t)) = do cvs <- getUIFunCVAssoc Nothing ui
return (nm, (isCurried, t, cvs))
uiFunVals <- mapM getUIFun allUiFuns
uiRegVals <- mapM (\ui@(nm, _) -> (nm,) <$> getUICVal Nothing ui) allUiRegs
obsvs <- getObservables
bindings <- let grab i@(getSV -> sv) = case lookupInput fst sv assocs of
Just (_, (_, (_, cv))) -> return (i, cv)
Nothing -> do !cv <- getValueCV Nothing sv
return (i, cv)
in if validationRequested cfg
then Just <$> mapM grab allInputs
else return Nothing
let model = SMTModel { modelObjectives = []
, modelBindings = F.toList <$> bindings
, modelAssocs = uiRegVals
<> (first T.unpack <$> sortOn fst obsvs)
<> [(T.unpack n, cv) | (_, (n, (_, cv))) <- F.toList assocs]
, modelUIFuns = uiFunVals
}
m = Satisfiable cfg model
(interpreteds, uninterpreteds) = S.partition (not . isUninterpreted . kindOf . fst) (fmap (snd . snd) assocs)
interpretedRegUis = filter (not . isUninterpreted . kindOf . snd) uiRegVals
interpretedRegUiSVs = [(cvt n (kindOf cv), cv) | (n, cv) <- interpretedRegUis]
where cvt :: String -> Kind -> SVal
cvt nm k = SVal k $ Right $ cache r
where r st = newExpr st k (SBVApp (Uninterpreted nm) [])
-- For each interpreted variable, figure out the model equivalence
-- NB. When the kind is floating, we *have* to be careful, since +/- zero, and NaN's
-- and equality don't get along!
interpretedEqs :: [SVal]
interpretedEqs = [mkNotEq (kindOf sv) sv (SVal (kindOf sv) (Left cv)) | (sv, cv) <- interpretedRegUiSVs <> F.toList interpreteds]
where mkNotEq k a b
| isDouble k || isFloat k || isFP k
= svNot (a `fpEq` b)
| True
= a `svNotEqual` b
fpEq a b = SVal KBool $ Right $ cache r
where r st = do sva <- svToSV st a
svb <- svToSV st b
newExpr st KBool (SBVApp (IEEEFP FP_ObjEqual) [sva, svb])
-- For each uninterpreted constant, use equivalence class
uninterpretedEqs :: [SVal]
uninterpretedEqs = concatMap pwDistinct -- Assert that they are pairwise distinct
. filter (\l -> length l > 1) -- Only need this class if it has at least two members
. map (map fst) -- throw away values, we only need svals
. groupBy ((==) `on` snd) -- make sure they belong to the same sort and have the same value
. sortOn snd -- sort them according to their CV (i.e., sort/value)
$ F.toList uninterpreteds
where pwDistinct :: [SVal] -> [SVal]
pwDistinct ss = [x `svNotEqual` y | (x:ys) <- tails ss, y <- ys]
-- For each uninterpreted function, create a disqualifying equation
-- We do this rather brute-force, since we need to create a new function
-- and do an existential assertion.
uninterpretedReject :: Maybe [String]
uninterpretedFuns :: [String]
(uninterpretedReject, uninterpretedFuns) = (uiReject, concat defs)
where uiReject = case rejects of
[] -> Nothing
xs -> Just xs
(rejects, defs) = unzip [mkNotEq ui | ui@(nm, _) <- uiFunVals, nm `elem` uiFunsToReject]
-- Otherwise, we have things to refute, go for it if we have a good interpretation for it
mkNotEq (nm, (_, typ, Left def)) =
error $ unlines [
""
, "*** allSat: Unsupported: Building a rejecting instance for:"
, "***"
, "*** " ++ nm ++ " :: " ++ show typ
, "*** " ++ def
, "***"
, "*** At this time, SBV cannot compute allSat when the model has a non-table definition."
, "***"
, "*** You can ignore specific functions via the 'isNonModelVar' filter:"
, "***"
, "*** allSatWith z3{isNonModelVar = (`elem` [" ++ show nm ++ "])} ..."
, "***"
, "*** Or you can ignore all uninterpreted functions for all-sat purposes using the 'allSatTrackUFs' parameter:"
, "***"
, "*** allSatWith z3{allSatTrackUFs = False} ..."
, "***"
, "*** You can see the response from the solver by running with the '{verbose = True}' option."
, "***"
, "*** NB. If this is a use case you'd like SBV to support, please get in touch!"
]
mkNotEq (nm, (_, SBVType ts, Right vs)) = (reject, def ++ dif)
where nm' = nm ++ "_model" ++ show cnt
reject = nm' ++ "_reject"
-- rounding mode doesn't matter here, just pick one
scv = cvToSMTLib RoundNearestTiesToEven
(ats, rt) = (init ts, last ts)
args = unwords ["(x!" ++ show i ++ " " ++ smtType t ++ ")" | (t, i) <- zip ats [(0::Int)..]]
res = smtType rt
params = ["x!" ++ show i | (_, i) <- zip ats [(0::Int)..]]
uparams = unwords params
chain (vals, fallThru) = walk vals
where walk [] = [" " ++ scv fallThru ++ replicate (length vals) ')']
walk ((as, r) : rest) = (" (ite " ++ cond as ++ " " ++ scv r) : walk rest
cond as = "(and " ++ unwords (zipWith eq params as) ++ ")"
eq p a = "(= " ++ p ++ " " ++ scv a ++ ")"
def = ("(define-fun " ++ nm' ++ " (" ++ args ++ ") " ++ res)
: chain vs
++ [")"]
pad = replicate (1 + length nm' - length nm) ' '
dif = [ "(define-fun " ++ reject ++ " () Bool"
, " (exists (" ++ args ++ ")"
, " (distinct (" ++ nm ++ pad ++ uparams ++ ")"
, " (" ++ nm' ++ " " ++ uparams ++ "))))"
]
eqs = interpretedEqs ++ uninterpretedEqs
disallow = case eqs of
[] -> Nothing
_ -> Just $ SBV $ foldr1 svOr eqs
when (allSatPrintAlong cfg) $ do
io $ putStrLn $ "Solution #" ++ show cnt ++ ":"
io $ putStrLn $ showModel cfg model
let resultsSoFar = sofar { allSatResults = m : allSatResults sofar }
-- This is clunky, but let's not generate a rejector unless we really need it
needMoreIterations
| Just maxModels <- allSatMaxModelCount cfg, (cnt+1) > maxModels = False
| True = True
-- Send function disequalities, if any:
if not needMoreIterations
then go (cnt+1) resultsSoFar
else do let uiFunRejector = "uiFunRejector_model_" ++ show cnt
header = "define-fun " ++ uiFunRejector ++ " () Bool "
defineRejector [] = return ()
defineRejector [x] = send True $ "(" ++ header ++ x ++ ")"
defineRejector (x:xs) = mapM_ (send True) $ mergeSExpr $ ("(" ++ header)
: (" (or " ++ x)
: [" " ++ e | e <- xs]
++ [" ))"]
rejectFuncs <- case uninterpretedReject of
Nothing -> return Nothing
Just fs -> do mapM_ (send True) $ mergeSExpr uninterpretedFuns
defineRejector fs
return $ Just uiFunRejector
-- send the disallow clause and the uninterpreted rejector:
case (disallow, rejectFuncs) of
(Nothing, Nothing) -> pure resultsSoFar
(Just d, Nothing) -> do constrain d
go (cnt+1) resultsSoFar
(Nothing, Just f) -> do send True $ "(assert " ++ f ++ ")"
go (cnt+1) resultsSoFar
(Just d, Just f) -> -- This is where it gets ugly. We have an SBV and a string and we need to "or" them.
-- But we need a way to force 'd' to be produced. So, go ahead and force it:
do constrain $ d .=> d -- NB: Redundant, but it makes sure the corresponding constraint gets shown
svd <- io $ svToSV topState (unSBV d)
send True $ "(assert (or " ++ f ++ " " ++ show svd ++ "))"
go (cnt+1) resultsSoFar
-- | Generalization of 'Data.SBV.Control.getUnsatAssumptions'
getUnsatAssumptions :: (MonadIO m, MonadQuery m) => [String] -> [(String, a)] -> m [a]
getUnsatAssumptions originals proxyMap = do
let cmd = "(get-unsat-assumptions)"
bad = unexpected "getUnsatAssumptions" cmd "a list of unsatisfiable assumptions"
$ Just [ "Make sure you use:"
, ""
, " setOption $ ProduceUnsatAssumptions True"
, ""
, "to make sure the solver is ready for producing unsat assumptions,"
, "and that there is a model by first issuing a 'checkSat' call."
]
fromECon (ECon s) = Just s
fromECon _ = Nothing
r <- ask cmd
-- If unsat-cores are enabled, z3 might end-up printing an assumption that wasn't
-- in the original list of assumptions for `check-sat-assuming`. So, we walk over
-- and ignore those that weren't in the original list, and put a warning for those
-- we couldn't find.
let walk [] sofar = return $ reverse sofar
walk (a:as) sofar = case a `lookup` proxyMap of
Just v -> walk as (v:sofar)
Nothing -> do queryDebug [ "*** In call to 'getUnsatAssumptions'"
, "***"
, "*** Unexpected assumption named: " ++ show a
, "*** Was expecting one of : " ++ show originals
, "***"
, "*** This can happen if unsat-cores are also enabled. Ignoring."
]
walk as sofar
parse r bad $ \case
EApp es | Just xs <- mapM fromECon es -> walk xs []
_ -> bad r Nothing
-- | Timeout a query action, typically a command call to the underlying SMT solver.
-- The duration is in microseconds (@1\/10^6@ seconds). If the duration
-- is negative, then no timeout is imposed. When specifying long timeouts, be careful not to exceed
-- @maxBound :: Int@. (On a 64 bit machine, this bound is practically infinite. But on a 32 bit
-- machine, it corresponds to about 36 minutes!)
--
-- Semantics: The call @timeout n q@ causes the timeout value to be applied to all interactive calls that take place
-- as we execute the query @q@. That is, each call that happens during the execution of @q@ gets a separate
-- time-out value, as opposed to one timeout value that limits the whole query. This is typically the intended behavior.
-- It is advisable to apply this combinator to calls that involve a single call to the solver for
-- finer control, as opposed to an entire set of interactions. However, different use cases might call for different scenarios.
--
-- If the solver responds within the time-out specified, then we continue as usual. However, if the backend solver times-out
-- using this mechanism, there is no telling what the state of the solver will be. Thus, we raise an error in this case.
timeout :: (MonadIO m, MonadQuery m) => Int -> m a -> m a
timeout n q = do modifyQueryState (\qs -> qs {queryTimeOutValue = Just n})
r <- q
modifyQueryState (\qs -> qs {queryTimeOutValue = Nothing})
return r
-- | Bail out if a parse goes bad
parse :: String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse r fCont sCont = case parseSExpr r of
Left e -> fCont r (Just [e])
Right res -> sCont res
-- | Generalization of 'Data.SBV.Control.unexpected'
unexpected :: (MonadIO m, MonadQuery m) => String -> String -> String -> Maybe [String] -> String -> Maybe [String] -> m a
unexpected ctx sent expected mbHint received mbReason = do
-- empty the response channel first
extras <- retrieveResponse "terminating upon unexpected response" (Just 5000000)
cfg <- getConfig
let exc = SBVException { sbvExceptionDescription = "Unexpected response from the solver, context: " ++ ctx
, sbvExceptionSent = Just sent
, sbvExceptionExpected = Just expected
, sbvExceptionReceived = Just received
, sbvExceptionStdOut = Just $ unlines extras
, sbvExceptionStdErr = Nothing
, sbvExceptionExitCode = Nothing
, sbvExceptionConfig = cfg
, sbvExceptionReason = mbReason
, sbvExceptionHint = mbHint
}
io $ C.throwIO exc
-- | Convert a query result to an SMT Problem
runProofOn :: SBVRunMode -> QueryContext -> [String] -> Result -> SMTProblem
runProofOn rm context comments res@(Result progInfo ki _qcInfo _observables _codeSegs is consts tbls uis defns pgm cstrs _assertions outputs) =
let (config, isSat, isSafe, isSetup) = case rm of
SMTMode _ stage s c -> (c, s, isSafetyCheckingIStage stage, isSetupIStage stage)
_ -> error $ "runProofOn: Unexpected run mode: " ++ show rm
o | isSafe = trueSV
| True = case outputs of
[] | isSetup -> trueSV
[so] -> case so of
SV KBool _ -> so
_ -> error $ unlines [ "Impossible happened, non-boolean output: " ++ show so
, "Detected while generating the trace:\n" ++ show res
]
os -> error $ unlines [ "User error: Multiple output values detected: " ++ show os
, "Detected while generating the trace:\n" ++ show res
, "*** Check calls to \"output\", they are typically not needed!"
]
in SMTProblem { smtLibPgm = toSMTLib config context progInfo ki isSat comments is consts tbls uis defns pgm cstrs o }
-- | Generalization of 'Data.SBV.Control.executeQuery'
executeQuery :: forall m a. ExtractIO m => QueryContext -> QueryT m a -> SymbolicT m a
executeQuery queryContext originalQuery = do
st <- symbolicEnv
rm <- liftIO $ readIORef (runMode st)
-- Make sure the phases match:
() <- liftIO $ case (queryContext, rm) of
(QueryInternal, _) -> return () -- no worries, internal
(QueryExternal, SMTMode QueryExternal ISetup _ _) -> return () -- legitimate runSMT call
_ -> invalidQuery rm
case rm of
-- Transitioning from setup
SMTMode qc stage isSAT cfg | not (isRunIStage stage) -> do
let slvr = solver cfg
backend = engine slvr
-- make sure if we have dsat precision, then solver supports it
let dsatOK = isNothing (dsatPrecision cfg)
|| isJust (supportsDeltaSat (capabilities slvr))
unless dsatOK $ error $ unlines
[ ""
, "*** Data.SBV: Delta-sat precision is specified."
, "*** But the chosen solver (" ++ show (name slvr) ++ ") does not support"
, "*** delta-satisfiability."
]
res <- liftIO $ extractSymbolicSimulationState st
setOpts <- liftIO $ reverse <$> readIORef (rSMTOptions st)
-- Run any registered measure checks (termination/productivity verification)
liftIO $ do skip <- readIORef (rSkipMeasureChecks st)
unless skip $ do
checks <- readIORef (rMeasureChecks st)
unless (null checks) $ do
let nms = map (\(n, _, _) -> n) checks
debug cfg ["[MEASURE] Verifying termination measures for: " ++ intercalate ", " nms]
mapM_ (\(nm, isProductive, check) -> do
debug cfg ["[MEASURE] Checking: " ++ nm]
check cfg
let tag = if isProductive then "productive" else "terminating"
debug cfg ["[MEASURE] Passed (" ++ tag ++ "): " ++ nm]
) checks
let SMTProblem{smtLibPgm} = runProofOn rm queryContext [] res
cfg' = cfg { solverSetOptions = solverSetOptions cfg ++ setOpts }
pgm = smtLibPgm cfg'
liftIO $ writeIORef (runMode st) $ SMTMode qc IRun isSAT cfg
let terminateSolver maybeForwardedException = do
qs <- readIORef $ rQueryState st
case qs of
Nothing -> return ()
Just QueryState{queryTerminate} -> queryTerminate maybeForwardedException
-- If this is an extrnal query and there are objectives, let's add those to the list before we run
-- Here we only allow Lexicographic; we might want to make that configurable later.
let userQuery = case queryContext of
QueryInternal -> originalQuery
QueryExternal -> do mbDirs <- startOptimizer cfg Lexicographic
case mbDirs of
Nothing -> pure ()
Just (_, cmds) -> mapM_ (send True) cmds
originalQuery
lift $ join $ liftIO $ C.mask $ \restore -> do
r <- restore (extractIO $ join $ liftIO $ backend cfg' st (show pgm) $ extractIO . runReaderT (runQueryT userQuery))
`C.catch` \e -> terminateSolver (Just e) >> C.throwIO (e :: C.SomeException)
terminateSolver Nothing
return r
-- Already in a query, in theory we can just continue, but that causes use-case issues
-- so we reject it. TODO: Review if we should actually support this. The issue arises with
-- expressions like this:
--
-- In the following t0's output doesn't get recorded, as the output call is too late when we get
-- here. (The output field isn't "incremental.") So, t0/t1 behave differently!
--
-- t0 = satWith z3{verbose=True, transcript=Just "t.smt2"} $ query (return (false::SBool))
-- t1 = satWith z3{verbose=True, transcript=Just "t.smt2"} $ ((return (false::SBool)) :: Predicate)
--
-- Also, not at all clear what it means to go in an out of query mode:
--
-- r = runSMTWith z3{verbose=True} $ do
-- a' <- sInteger "a"
--
-- (a, av) <- query $ do _ <- checkSat
-- av <- getValue a'
-- return (a', av)
--
-- liftIO $ putStrLn $ "Got: " ++ show av
-- -- constrain $ a .> literal av + 1 -- Can't do this since we're "out" of query. Sigh.
--
-- bv <- query $ do constrain $ a .> literal av + 1
-- _ <- checkSat
-- getValue a
--
-- return $ a' .== a' + 1
--
-- This would be one possible implementation, alas it has the problems above:
--
-- SMTMode IRun _ _ -> liftIO $ evalStateT userQuery st
--
-- So, we just reject it.
SMTMode _ IRun _ _ -> error $ unlines [ ""
, "*** Data.SBV: Unsupported nested query is detected."
, "***"
, "*** Please group your queries into one block. Note that this"
, "*** can also arise if you have a call to 'query' not within 'runSMT'"
, "*** For instance, within 'sat'/'prove' calls with custom user queries."
, "*** The solution is to do the sat/prove part in the query directly."
, "***"
, "*** While multiple/nested queries should not be necessary in general,"
, "*** please do get in touch if your use case does require such a feature,"
, "*** to see how we can accommodate such scenarios."
]
-- Otherwise choke!
_ -> invalidQuery rm
where invalidQuery rm = error $ unlines [ ""
, "*** Data.SBV: Invalid query call."
, "***"
, "*** Current mode: " ++ show rm
, "***"
, "*** Query calls are only valid within runSMT/runSMTWith calls,"
, "*** and each call to runSMT should have only one query call inside."
]
-- | Preparing for optimization. If we have objectives, returns the directives for the solver. If not, it returns nothing.
startOptimizer :: (MonadIO m, MonadQuery m) => SMTConfig -> OptimizeStyle -> m (Maybe ([Objective (SV, SV)], [String]))
startOptimizer config style = do
objectives <- getObjectives
if null objectives
then return Nothing
else do unless (supportsOptimization (capabilities (solver config))) $
error $ unlines [ ""
, "*** Data.SBV: The backend solver " ++ show (name (solver config)) ++ "does not support optimization goals."
, "*** Please use a solver that has support, such as z3"
]
when (validateModel config && not (optimizeValidateConstraints config)) $
error $ unlines [ ""
, "*** Data.SBV: Model validation is not supported in optimization calls."
, "***"
, "*** Instead, use `cfg{optimizeValidateConstraints = True}`"
, "***"
, "*** which checks that the results satisfy the constraints but does"
, "*** NOT ensure that they are optimal."
]
let optimizerDirectives = concatMap minmax objectives ++ priority style
where mkEq (x, y) = "(assert (= " ++ show x ++ " " ++ show y ++ "))"
minmax (Minimize _ xy@(_, v)) = [mkEq xy, "(minimize " ++ show v ++ ")"]
minmax (Maximize _ xy@(_, v)) = [mkEq xy, "(maximize " ++ show v ++ ")"]
minmax (AssertWithPenalty nm xy@(_, v) mbp) = [mkEq xy, "(assert-soft " ++ show v ++ penalize mbp ++ ")"]
where penalize DefaultPenalty = ""
penalize (Penalty w mbGrp)
| w <= 0 = error $ unlines [ "SBV.AssertWithPenalty: Goal " ++ show nm ++ " is assigned a non-positive penalty: " ++ shw
, "All soft goals must have > 0 penalties associated."
]
| True = " :weight " ++ shw ++ maybe "" group mbGrp
where shw = show (fromRational w :: Double)
group g = " :id " ++ g
priority Lexicographic = [] -- default, no option needed
priority Independent = ["(set-option :opt.priority box)"]
priority (Pareto _) = ["(set-option :opt.priority pareto)"]
pure $ Just (objectives, optimizerDirectives)
-- | Just after a check-sat is issued, collect objective values. Used
-- internally only, not exposed to the user.
getObjectiveValues :: forall m. (MonadIO m, MonadQuery m) => m [(String, GeneralizedCV)]
getObjectiveValues = do let cmd = "(get-objectives)"
bad = unexpected "getObjectiveValues" cmd "a list of objective values" Nothing
r <- ask cmd
si <- queryState >>= getSInfo
inputs <- F.toList <$> getTopLevelInputs
parse r bad $ \case EApp (ECon "objectives" : es) -> catMaybes <$> mapM (getObjValue si (bad r) inputs) es
_ -> bad r Nothing
where -- | Parse an objective value out.
getObjValue :: SInfo -> (forall a. Maybe [String] -> m a) -> [NamedSymVar] -> SExpr -> m (Maybe (String, GeneralizedCV))
getObjValue si bailOut inputs expr =
case expr of
EApp [_] -> return Nothing -- Happens when a soft-assertion has no associated group.
EApp [ECon nm, v] -> locate nm v -- Regular case
_ -> dontUnderstand (show expr)
where locate nm v = case listToMaybe [p | p@(NamedSymVar sv _) <- inputs, show sv == nm] of
Nothing -> return Nothing -- Happens when the soft assertion has a group-id that's not one of the input names
Just (NamedSymVar sv actualName) -> grab sv v >>= \val -> return $ Just (T.unpack actualName, val)
dontUnderstand s = bailOut $ Just [ "Unable to understand solver output."
, "While trying to process: " ++ s
]
grab :: SV -> SExpr -> m GeneralizedCV
grab s topExpr
| Just v <- recoverKindedValue si k topExpr = return $ RegularCV v
| True = ExtendedCV <$> cvt (simplify topExpr)
where k = kindOf s
-- Convert to an extended expression. Hopefully complete!
cvt :: SExpr -> m ExtCV
cvt (ECon "oo") = return $ Infinite k
cvt (ECon "epsilon") = return $ Epsilon k
cvt (EApp [ECon "interval", x, y]) = Interval <$> cvt x <*> cvt y
cvt (ENum (i, _, _)) = return $ BoundedCV $ mkConstCV k i
cvt (EReal r) = return $ BoundedCV $ CV k $ CAlgReal r
cvt (EFloat f) = return $ BoundedCV $ CV k $ CFloat f
cvt (EDouble d) = return $ BoundedCV $ CV k $ CDouble d
cvt (EApp [ECon "+", x, y]) = AddExtCV <$> cvt x <*> cvt y
cvt (EApp [ECon "*", x, y]) = MulExtCV <$> cvt x <*> cvt y
-- Nothing else should show up, hopefully!
cvt e = dontUnderstand (show e)
-- drop the pesky to_real's that Z3 produces.. Cool but useless.
simplify :: SExpr -> SExpr
simplify (EApp [ECon "to_real", n]) = n
simplify (EApp xs) = EApp (map simplify xs)
simplify e = e
-- | Generalization of 'Data.SBV.Control.getModel'
getModel :: (MonadIO m, MonadQuery m) => m SMTModel
getModel = getModelAtIndex Nothing
-- | Get a model stored at an index. This is likely very Z3 specific!
getModelAtIndex :: (MonadIO m, MonadQuery m) => Maybe Int -> m SMTModel
getModelAtIndex mbi = do
State{runMode} <- queryState
rm <- io $ readIORef runMode
case rm of
m@CodeGen -> error $ "SBV.getModel: Model is not available in mode: " ++ show m
m@LambdaGen{} -> error $ "SBV.getModel: Model is not available in mode: " ++ show m
m@Concrete{} -> error $ "SBV.getModel: Model is not available in mode: " ++ show m
SMTMode{} -> do
cfg <- getConfig
uis <- getUIs
allModelInputs <- getTopLevelInputs
obsvs <- getObservables
inputAssocs <- let grab (NamedSymVar sv nm) = let wrap !c = (sv, (nm, c)) in wrap <$> getValueCV mbi sv
in mapM grab allModelInputs
let name = fst . snd
removeSV = snd
prepare = S.unstableSort . S.filter (not . mustIgnoreVar cfg . T.unpack . name)
assocs = fmap removeSV (prepare inputAssocs) <> S.fromList (sortOn fst obsvs)
-- collect UIs, and UI functions if requested
let uiFuns = [ui | ui@(nm, (_, _, SBVType as)) <- uis, length as > 1, allSatTrackUFs cfg, not (mustIgnoreVar cfg nm)] -- functions have at least two things in their type!
uiRegs = [ui | ui@(nm, (_, _, SBVType as)) <- uis, length as == 1, not (mustIgnoreVar cfg nm)]
-- If there are uninterpreted functions, arrange so that z3's pretty-printer flattens things out
-- as cex's tend to get larger
unless (null uiFuns) $
let solverCaps = capabilities (solver cfg)
in case supportsFlattenedModels solverCaps of
Nothing -> return ()
Just cmds -> mapM_ (send True) cmds
bindings <- let get i@(getSV -> sv) = case lookupInput fst sv inputAssocs of
Just (_, (_, cv)) -> return (i, cv)
Nothing -> do cv <- getValueCV mbi sv
return (i, cv)
in if validationRequested cfg
then Just <$> mapM get allModelInputs
else return Nothing
uiFunVals <- mapM (\ui@(nm, (c, _, t)) -> (\a -> (nm, (c, t, a))) <$> getUIFunCVAssoc mbi ui) uiFuns
uiVals <- mapM (\ui@(nm, (_, _, _)) -> (nm,) <$> getUICVal mbi ui) uiRegs
return $ unBarModel $ SMTModel { modelObjectives = []
, modelBindings = F.toList <$> bindings
, modelAssocs = uiVals ++ F.toList (first T.unpack <$> assocs)
, modelUIFuns = uiFunVals
}
-- | Remove the bars from model names; these are (mostly!) automatically inserted
unBarModel :: SMTModel -> SMTModel
unBarModel SMTModel {modelObjectives, modelBindings, modelAssocs, modelUIFuns}
= SMTModel { modelObjectives = ubf <$> modelObjectives
, modelBindings = (ubn <$>) <$> modelBindings
, modelAssocs = ubf <$> modelAssocs
, modelUIFuns = ubf <$> modelUIFuns
}
where ubf (n, a) = (unBar n, a)
ubn (NamedSymVar sv nm, a) = (NamedSymVar sv (T.pack (unBar (T.unpack nm))), a)
{- HLint ignore module "Reduce duplication" -}
{- HLint ignore getAllSatResult "Use forM_" -}
{- HLint ignore getModelAtIndex "Use forM_" -}