{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE Rank2Types #-}
{-# 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, getAssignment, getOption, freshVar, freshVar_, freshArray, freshArray_, push, pop, getAssertionStackDepth
, inNewAssertionStack, echo, caseSplit, resetAssertions, exit, getAssertions, getValue, getUninterpretedValue, 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.IntMap.Strict as IM
import Data.Char (toLower)
import Data.List (intercalate, nubBy, sortBy, sortOn)
import Data.Maybe (listToMaybe, catMaybes)
import Data.Function (on)
import Data.SBV.Core.Data
import Data.SBV.Core.Symbolic ( MonadQuery(..), State(..)
, incrementInternalCounter, validationRequested
)
import Data.SBV.Utils.SExpr
import Data.SBV.Control.Types
import Data.SBV.Control.Utils
data Assignment = Assign SVal CV
noSurrounding :: Char -> String -> String
noSurrounding :: Char -> String -> String
noSurrounding c :: Char
c (c' :: Char
c':cs :: String
cs@(_:_)) | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
c' Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Char
forall a. [a] -> a
last String
cs = String -> String
forall a. [a] -> [a]
init String
cs
noSurrounding _ s :: String
s = String
s
unQuote :: String -> String
unQuote :: String -> String
unQuote = Char -> String -> String
noSurrounding '"'
unBar :: String -> String
unBar :: String -> String
unBar = Char -> String -> String
noSurrounding '|'
fromECon :: SExpr -> Maybe String
fromECon :: SExpr -> Maybe String
fromECon (ECon s :: String
s) = String -> Maybe String
forall a. a -> Maybe a
Just String
s
fromECon _ = Maybe String
forall a. Maybe a
Nothing
stringsOf :: SExpr -> [String]
stringsOf :: SExpr -> [String]
stringsOf (ECon s :: String
s) = [String
s]
stringsOf (ENum (i :: Integer
i, _)) = [Integer -> String
forall a. Show a => a -> String
show Integer
i]
stringsOf (EReal r :: AlgReal
r) = [AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r]
stringsOf (EFloat f :: Float
f) = [Float -> String
forall a. Show a => a -> String
show Float
f]
stringsOf (EDouble d :: Double
d) = [Double -> String
forall a. Show a => a -> String
show Double
d]
stringsOf (EApp ss :: [SExpr]
ss) = (SExpr -> [String]) -> [SExpr] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SExpr -> [String]
stringsOf [SExpr]
ss
serialize :: Bool -> SExpr -> String
serialize :: Bool -> SExpr -> String
serialize removeQuotes :: Bool
removeQuotes = SExpr -> String
go
where go :: SExpr -> String
go (ECon s :: String
s) = if Bool
removeQuotes then String -> String
unQuote String
s else String
s
go (ENum (i :: Integer
i, _)) = Integer -> String
forall a. (Show a, Num a, Ord a) => a -> String
shNN Integer
i
go (EReal r :: AlgReal
r) = AlgReal -> String
forall a. (Show a, Num a, Ord a) => a -> String
shNN AlgReal
r
go (EFloat f :: Float
f) = Float -> String
forall a. (Show a, Num a, Ord a) => a -> String
shNN Float
f
go (EDouble d :: Double
d) = Double -> String
forall a. (Show a, Num a, Ord a) => a -> String
shNN Double
d
go (EApp [x :: SExpr
x]) = SExpr -> String
go SExpr
x
go (EApp ss :: [SExpr]
ss) = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SExpr -> String) -> [SExpr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SExpr -> String
go [SExpr]
ss) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
shNN :: (Show a, Num a, Ord a) => a -> String
shNN :: a -> String
shNN i :: a
i
| a
i a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< 0 = "(- " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show (-a
i) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
| Bool
True = a -> String
forall a. Show a => a -> String
show a
i
getInfo :: (MonadIO m, MonadQuery m) => SMTInfoFlag -> m SMTInfoResponse
getInfo :: SMTInfoFlag -> m SMTInfoResponse
getInfo flag :: SMTInfoFlag
flag = do
let cmd :: String
cmd = "(get-info " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SMTInfoFlag -> String
forall a. Show a => a -> String
show SMTInfoFlag
flag String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected "getInfo" String
cmd "a valid get-info response" Maybe [String]
forall a. Maybe a
Nothing
isAllStatistics :: SMTInfoFlag -> Bool
isAllStatistics AllStatistics = Bool
True
isAllStatistics _ = Bool
False
isAllStat :: Bool
isAllStat = SMTInfoFlag -> Bool
isAllStatistics SMTInfoFlag
flag
grabAllStat :: SExpr -> SExpr -> (String, String)
grabAllStat k :: SExpr
k v :: SExpr
v = (SExpr -> String
render SExpr
k, SExpr -> String
render SExpr
v)
grabAllStats :: SExpr -> [(String, String)]
grabAllStats (EApp xs :: [SExpr]
xs) = [SExpr] -> [(String, String)]
walk [SExpr]
xs
where walk :: [SExpr] -> [(String, String)]
walk [] = []
walk [t :: SExpr
t] = [SExpr -> SExpr -> (String, String)
grabAllStat SExpr
t (String -> SExpr
ECon "")]
walk (t :: SExpr
t : v :: SExpr
v : rest :: [SExpr]
rest) = SExpr -> SExpr -> (String, String)
grabAllStat SExpr
t SExpr
v (String, String) -> [(String, String)] -> [(String, String)]
forall a. a -> [a] -> [a]
: [SExpr] -> [(String, String)]
walk [SExpr]
rest
grabAllStats o :: SExpr
o = [SExpr -> SExpr -> (String, String)
grabAllStat SExpr
o (String -> SExpr
ECon "")]
String
r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd
String
-> (String -> Maybe [String] -> m SMTInfoResponse)
-> (SExpr -> m SMTInfoResponse)
-> m SMTInfoResponse
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m SMTInfoResponse
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m SMTInfoResponse) -> m SMTInfoResponse)
-> (SExpr -> m SMTInfoResponse) -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ \pe :: SExpr
pe ->
if Bool
isAllStat
then SMTInfoResponse -> m SMTInfoResponse
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTInfoResponse -> m SMTInfoResponse)
-> SMTInfoResponse -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ [(String, String)] -> SMTInfoResponse
Resp_AllStatistics ([(String, String)] -> SMTInfoResponse)
-> [(String, String)] -> SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ SExpr -> [(String, String)]
grabAllStats SExpr
pe
else case SExpr
pe of
ECon "unsupported" -> SMTInfoResponse -> m SMTInfoResponse
forall (m :: * -> *) a. Monad m => a -> m a
return SMTInfoResponse
Resp_Unsupported
EApp [ECon ":assertion-stack-levels", ENum (i :: Integer
i, _)] -> SMTInfoResponse -> m SMTInfoResponse
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTInfoResponse -> m SMTInfoResponse)
-> SMTInfoResponse -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ Integer -> SMTInfoResponse
Resp_AssertionStackLevels Integer
i
EApp (ECon ":authors" : ns :: [SExpr]
ns) -> SMTInfoResponse -> m SMTInfoResponse
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTInfoResponse -> m SMTInfoResponse)
-> SMTInfoResponse -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ [String] -> SMTInfoResponse
Resp_Authors ((SExpr -> String) -> [SExpr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SExpr -> String
render [SExpr]
ns)
EApp [ECon ":error-behavior", ECon "immediate-exit"] -> SMTInfoResponse -> m SMTInfoResponse
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTInfoResponse -> m SMTInfoResponse)
-> SMTInfoResponse -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ SMTErrorBehavior -> SMTInfoResponse
Resp_Error SMTErrorBehavior
ErrorImmediateExit
EApp [ECon ":error-behavior", ECon "continued-execution"] -> SMTInfoResponse -> m SMTInfoResponse
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTInfoResponse -> m SMTInfoResponse)
-> SMTInfoResponse -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ SMTErrorBehavior -> SMTInfoResponse
Resp_Error SMTErrorBehavior
ErrorContinuedExecution
EApp (ECon ":name" : o :: [SExpr]
o) -> SMTInfoResponse -> m SMTInfoResponse
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTInfoResponse -> m SMTInfoResponse)
-> SMTInfoResponse -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ String -> SMTInfoResponse
Resp_Name (SExpr -> String
render ([SExpr] -> SExpr
EApp [SExpr]
o))
EApp (ECon ":reason-unknown" : o :: [SExpr]
o) -> SMTInfoResponse -> m SMTInfoResponse
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTInfoResponse -> m SMTInfoResponse)
-> SMTInfoResponse -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ SMTReasonUnknown -> SMTInfoResponse
Resp_ReasonUnknown ([SExpr] -> SMTReasonUnknown
unk [SExpr]
o)
EApp (ECon ":version" : o :: [SExpr]
o) -> SMTInfoResponse -> m SMTInfoResponse
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTInfoResponse -> m SMTInfoResponse)
-> SMTInfoResponse -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ String -> SMTInfoResponse
Resp_Version (SExpr -> String
render ([SExpr] -> SExpr
EApp [SExpr]
o))
EApp (ECon s :: String
s : o :: [SExpr]
o) -> SMTInfoResponse -> m SMTInfoResponse
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTInfoResponse -> m SMTInfoResponse)
-> SMTInfoResponse -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ String -> [String] -> SMTInfoResponse
Resp_InfoKeyword String
s ((SExpr -> String) -> [SExpr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SExpr -> String
render [SExpr]
o)
_ -> String -> Maybe [String] -> m SMTInfoResponse
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
where render :: SExpr -> String
render = Bool -> SExpr -> String
serialize Bool
True
unk :: [SExpr] -> SMTReasonUnknown
unk [ECon s :: String
s] | Just d :: SMTReasonUnknown
d <- String -> Maybe SMTReasonUnknown
getUR String
s = SMTReasonUnknown
d
unk o :: [SExpr]
o = String -> SMTReasonUnknown
UnknownOther (SExpr -> String
render ([SExpr] -> SExpr
EApp [SExpr]
o))
getUR :: String -> Maybe SMTReasonUnknown
getUR s :: String
s = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (String -> String
unQuote String
s) String -> [(String, SMTReasonUnknown)] -> Maybe SMTReasonUnknown
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
k, SMTReasonUnknown
d) | (k :: String
k, d :: SMTReasonUnknown
d) <- [(String, SMTReasonUnknown)]
unknownReasons]
unknownReasons :: [(String, SMTReasonUnknown)]
unknownReasons = [ ("memout", SMTReasonUnknown
UnknownMemOut)
, ("incomplete", SMTReasonUnknown
UnknownIncomplete)
, ("timeout", SMTReasonUnknown
UnknownTimeOut)
]
getOption :: (MonadIO m, MonadQuery m) => (a -> SMTOption) -> m (Maybe SMTOption)
getOption :: (a -> SMTOption) -> m (Maybe SMTOption)
getOption f :: a -> SMTOption
f = case a -> SMTOption
f a
forall a. HasCallStack => a
undefined of
DiagnosticOutputChannel{} -> String
-> String
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor "DiagnosticOutputChannel" ":diagnostic-output-channel" ((SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption))
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (String -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a.
Monad m =>
(String -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
string String -> SMTOption
DiagnosticOutputChannel
ProduceAssertions{} -> String
-> String
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor "ProduceAssertions" ":produce-assertions" ((SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption))
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Bool -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool Bool -> SMTOption
ProduceAssertions
ProduceAssignments{} -> String
-> String
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor "ProduceAssignments" ":produce-assignments" ((SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption))
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Bool -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool Bool -> SMTOption
ProduceAssignments
ProduceProofs{} -> String
-> String
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor "ProduceProofs" ":produce-proofs" ((SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption))
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Bool -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool Bool -> SMTOption
ProduceProofs
ProduceInterpolants{} -> String
-> String
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor "ProduceInterpolants" ":produce-interpolants" ((SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption))
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Bool -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool Bool -> SMTOption
ProduceInterpolants
ProduceUnsatAssumptions{} -> String
-> String
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor "ProduceUnsatAssumptions" ":produce-unsat-assumptions" ((SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption))
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Bool -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool Bool -> SMTOption
ProduceUnsatAssumptions
ProduceUnsatCores{} -> String
-> String
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor "ProduceUnsatCores" ":produce-unsat-cores" ((SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption))
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Bool -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool Bool -> SMTOption
ProduceUnsatCores
RandomSeed{} -> String
-> String
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor "RandomSeed" ":random-seed" ((SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption))
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Integer -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a.
Monad m =>
(Integer -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
integer Integer -> SMTOption
RandomSeed
ReproducibleResourceLimit{} -> String
-> String
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor "ReproducibleResourceLimit" ":reproducible-resource-limit" ((SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption))
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Integer -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a.
Monad m =>
(Integer -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
integer Integer -> SMTOption
ReproducibleResourceLimit
SMTVerbosity{} -> String
-> String
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor "SMTVerbosity" ":verbosity" ((SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption))
-> (SExpr
-> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Integer -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a.
Monad m =>
(Integer -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
integer Integer -> SMTOption
SMTVerbosity
OptionKeyword nm :: String
nm _ -> String
-> String
-> (SExpr -> (Maybe [String] -> m Any) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall (m :: * -> *) a a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor ("OptionKeyword" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm) String
nm ((SExpr -> (Maybe [String] -> m Any) -> m (Maybe SMTOption))
-> m (Maybe SMTOption))
-> (SExpr -> (Maybe [String] -> m Any) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ ([String] -> SMTOption)
-> SExpr -> (Maybe [String] -> m Any) -> m (Maybe SMTOption)
forall (m :: * -> *) a p.
Monad m =>
([String] -> a) -> SExpr -> p -> m (Maybe a)
stringList (String -> [String] -> SMTOption
OptionKeyword String
nm)
SetLogic{} -> String -> m (Maybe SMTOption)
forall a. HasCallStack => String -> a
error "Data.SBV.Query: SMTLib does not allow querying value of the logic!"
SetInfo{} -> String -> m (Maybe SMTOption)
forall a. HasCallStack => String -> a
error "Data.SBV.Query: SMTLib does not allow querying value of meta-info!"
where askFor :: String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor sbvName :: String
sbvName smtLibName :: String
smtLibName continue :: SExpr -> (Maybe [String] -> m a) -> m (Maybe a)
continue = do
let cmd :: String
cmd = "(get-option " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
smtLibName String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected ("getOption " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sbvName) String
cmd "a valid option value" Maybe [String]
forall a. Maybe a
Nothing
String
r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd
String
-> (String -> Maybe [String] -> m (Maybe a))
-> (SExpr -> m (Maybe a))
-> m (Maybe a)
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m (Maybe a)
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m (Maybe a)) -> m (Maybe a))
-> (SExpr -> m (Maybe a)) -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ \case ECon "unsupported" -> Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
e :: SExpr
e -> SExpr -> (Maybe [String] -> m a) -> m (Maybe a)
continue SExpr
e (String -> Maybe [String] -> m a
forall a. String -> Maybe [String] -> m a
bad String
r)
string :: (String -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
string c :: String -> a
c (ECon s :: String
s) _ = Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ String -> a
c String
s
string _ e :: SExpr
e k :: Maybe [String] -> m (Maybe a)
k = Maybe [String] -> m (Maybe a)
k (Maybe [String] -> m (Maybe a)) -> Maybe [String] -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just ["Expected string, but got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show (Bool -> SExpr -> String
serialize Bool
False SExpr
e)]
bool :: (Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool c :: Bool -> a
c (ENum (0, _)) _ = Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ Bool -> a
c Bool
False
bool c :: Bool -> a
c (ENum (1, _)) _ = Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ Bool -> a
c Bool
True
bool _ e :: SExpr
e k :: Maybe [String] -> m (Maybe a)
k = Maybe [String] -> m (Maybe a)
k (Maybe [String] -> m (Maybe a)) -> Maybe [String] -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just ["Expected boolean, but got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show (Bool -> SExpr -> String
serialize Bool
False SExpr
e)]
integer :: (Integer -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
integer c :: Integer -> a
c (ENum (i :: Integer
i, _)) _ = Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ Integer -> a
c Integer
i
integer _ e :: SExpr
e k :: Maybe [String] -> m (Maybe a)
k = Maybe [String] -> m (Maybe a)
k (Maybe [String] -> m (Maybe a)) -> Maybe [String] -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just ["Expected integer, but got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show (Bool -> SExpr -> String
serialize Bool
False SExpr
e)]
stringList :: ([String] -> a) -> SExpr -> p -> m (Maybe a)
stringList c :: [String] -> a
c e :: SExpr
e _ = Maybe a -> m (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ [String] -> a
c ([String] -> a) -> [String] -> a
forall a b. (a -> b) -> a -> b
$ SExpr -> [String]
stringsOf SExpr
e
getUnknownReason :: (MonadIO m, MonadQuery m) => m SMTReasonUnknown
getUnknownReason :: m SMTReasonUnknown
getUnknownReason = do SMTInfoResponse
ru <- SMTInfoFlag -> m SMTInfoResponse
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
SMTInfoFlag -> m SMTInfoResponse
getInfo SMTInfoFlag
ReasonUnknown
case SMTInfoResponse
ru of
Resp_Unsupported -> SMTReasonUnknown -> m SMTReasonUnknown
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTReasonUnknown -> m SMTReasonUnknown)
-> SMTReasonUnknown -> m SMTReasonUnknown
forall a b. (a -> b) -> a -> b
$ String -> SMTReasonUnknown
UnknownOther "Solver responded: Unsupported."
Resp_ReasonUnknown r :: SMTReasonUnknown
r -> SMTReasonUnknown -> m SMTReasonUnknown
forall (m :: * -> *) a. Monad m => a -> m a
return SMTReasonUnknown
r
_ -> String -> m SMTReasonUnknown
forall a. HasCallStack => String -> a
error (String -> m SMTReasonUnknown) -> String -> m SMTReasonUnknown
forall a b. (a -> b) -> a -> b
$ "Unexpected reason value received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SMTInfoResponse -> String
forall a. Show a => a -> String
show SMTInfoResponse
ru
ensureSat :: (MonadIO m, MonadQuery m) => m ()
ensureSat :: m ()
ensureSat = do SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
CheckSatResult
cs <- String -> m CheckSatResult
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m CheckSatResult
checkSatUsing (String -> m CheckSatResult) -> String -> m CheckSatResult
forall a b. (a -> b) -> a -> b
$ SMTConfig -> String
satCmd SMTConfig
cfg
case CheckSatResult
cs of
Sat -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Unk -> do SMTReasonUnknown
s <- m SMTReasonUnknown
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
String -> m ()
forall a. HasCallStack => String -> a
error (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ ""
, "*** Data.SBV.ensureSat: Solver reported Unknown!"
, "*** Reason: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SMTReasonUnknown -> String
forall a. Show a => a -> String
show SMTReasonUnknown
s
]
Unsat -> String -> m ()
forall a. HasCallStack => String -> a
error "Data.SBV.ensureSat: Solver reported Unsat!"
getSMTResult :: (MonadIO m, MonadQuery m) => m SMTResult
getSMTResult :: m SMTResult
getSMTResult = do SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
CheckSatResult
cs <- m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
case CheckSatResult
cs of
Unsat -> SMTConfig -> Maybe [String] -> SMTResult
Unsatisfiable SMTConfig
cfg (Maybe [String] -> SMTResult) -> m (Maybe [String]) -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe [String])
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m (Maybe [String])
getUnsatCoreIfRequested
Sat -> SMTConfig -> SMTModel -> SMTResult
Satisfiable SMTConfig
cfg (SMTModel -> SMTResult) -> m SMTModel -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTModel
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
Unk -> SMTConfig -> SMTReasonUnknown -> SMTResult
Unknown SMTConfig
cfg (SMTReasonUnknown -> SMTResult)
-> m SMTReasonUnknown -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTReasonUnknown
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
classifyModel :: SMTConfig -> SMTModel -> SMTResult
classifyModel :: SMTConfig -> SMTModel -> SMTResult
classifyModel cfg :: SMTConfig
cfg m :: SMTModel
m
| ((String, GeneralizedCV) -> Bool)
-> [(String, GeneralizedCV)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String, GeneralizedCV) -> Bool
forall a. (a, GeneralizedCV) -> Bool
isExt (SMTModel -> [(String, GeneralizedCV)]
modelObjectives SMTModel
m) = SMTConfig -> SMTModel -> SMTResult
SatExtField SMTConfig
cfg SMTModel
m
| Bool
True = SMTConfig -> SMTModel -> SMTResult
Satisfiable SMTConfig
cfg SMTModel
m
where isExt :: (a, GeneralizedCV) -> Bool
isExt (_, v :: GeneralizedCV
v) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ GeneralizedCV -> Bool
isRegularCV GeneralizedCV
v
getLexicographicOptResults :: (MonadIO m, MonadQuery m) => m SMTResult
getLexicographicOptResults :: m SMTResult
getLexicographicOptResults = do SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
CheckSatResult
cs <- m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
case CheckSatResult
cs of
Unsat -> SMTConfig -> Maybe [String] -> SMTResult
Unsatisfiable SMTConfig
cfg (Maybe [String] -> SMTResult) -> m (Maybe [String]) -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe [String])
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m (Maybe [String])
getUnsatCoreIfRequested
Sat -> SMTConfig -> SMTModel -> SMTResult
classifyModel SMTConfig
cfg (SMTModel -> SMTResult) -> m SMTModel -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTModel
getModelWithObjectives
Unk -> SMTConfig -> SMTReasonUnknown -> SMTResult
Unknown SMTConfig
cfg (SMTReasonUnknown -> SMTResult)
-> m SMTReasonUnknown -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTReasonUnknown
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
where getModelWithObjectives :: m SMTModel
getModelWithObjectives = do [(String, GeneralizedCV)]
objectiveValues <- m [(String, GeneralizedCV)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, GeneralizedCV)]
getObjectiveValues
SMTModel
m <- m SMTModel
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
SMTModel -> m SMTModel
forall (m :: * -> *) a. Monad m => a -> m a
return SMTModel
m {modelObjectives :: [(String, GeneralizedCV)]
modelObjectives = [(String, GeneralizedCV)]
objectiveValues}
getIndependentOptResults :: forall m. (MonadIO m, MonadQuery m) => [String] -> m [(String, SMTResult)]
getIndependentOptResults :: [String] -> m [(String, SMTResult)]
getIndependentOptResults objNames :: [String]
objNames = do SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
CheckSatResult
cs <- m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
case CheckSatResult
cs of
Unsat -> m (Maybe [String])
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m (Maybe [String])
getUnsatCoreIfRequested m (Maybe [String])
-> (Maybe [String] -> m [(String, SMTResult)])
-> m [(String, SMTResult)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \mbUC :: Maybe [String]
mbUC -> [(String, SMTResult)] -> m [(String, SMTResult)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(String
nm, SMTConfig -> Maybe [String] -> SMTResult
Unsatisfiable SMTConfig
cfg Maybe [String]
mbUC) | String
nm <- [String]
objNames]
Sat -> (SMTModel -> SMTResult) -> m [(String, SMTResult)]
forall b. (SMTModel -> b) -> m [(String, b)]
continue (SMTConfig -> SMTModel -> SMTResult
classifyModel SMTConfig
cfg)
Unk -> do SMTResult
ur <- SMTConfig -> SMTReasonUnknown -> SMTResult
Unknown SMTConfig
cfg (SMTReasonUnknown -> SMTResult)
-> m SMTReasonUnknown -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTReasonUnknown
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
[(String, SMTResult)] -> m [(String, SMTResult)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(String
nm, SMTResult
ur) | String
nm <- [String]
objNames]
where continue :: (SMTModel -> b) -> m [(String, b)]
continue classify :: SMTModel -> b
classify = do [(String, GeneralizedCV)]
objectiveValues <- m [(String, GeneralizedCV)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, GeneralizedCV)]
getObjectiveValues
[(String, SMTModel)]
nms <- (Int -> String -> m (String, SMTModel))
-> [Int] -> [String] -> m [(String, SMTModel)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Int -> String -> m (String, SMTModel)
getIndependentResult [0..] [String]
objNames
[(String, b)] -> m [(String, b)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(String
n, SMTModel -> b
classify (SMTModel
m {modelObjectives :: [(String, GeneralizedCV)]
modelObjectives = [(String, GeneralizedCV)]
objectiveValues})) | (n :: String
n, m :: SMTModel
m) <- [(String, SMTModel)]
nms]
getIndependentResult :: Int -> String -> m (String, SMTModel)
getIndependentResult :: Int -> String -> m (String, SMTModel)
getIndependentResult i :: Int
i s :: String
s = do SMTModel
m <- Maybe Int -> m SMTModel
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> m SMTModel
getModelAtIndex (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i)
(String, SMTModel) -> m (String, SMTModel)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
s, SMTModel
m)
getParetoOptResults :: (MonadIO m, MonadQuery m) => Maybe Int -> m (Bool, [SMTResult])
getParetoOptResults :: Maybe Int -> m (Bool, [SMTResult])
getParetoOptResults (Just i :: Int
i)
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 = (Bool, [SMTResult]) -> m (Bool, [SMTResult])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [])
getParetoOptResults mbN :: Maybe Int
mbN = do SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
CheckSatResult
cs <- m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
case CheckSatResult
cs of
Unsat -> (Bool, [SMTResult]) -> m (Bool, [SMTResult])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [])
Sat -> (SMTModel -> SMTResult) -> m (Bool, [SMTResult])
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(SMTModel -> a) -> m (Bool, [a])
continue (SMTConfig -> SMTModel -> SMTResult
classifyModel SMTConfig
cfg)
Unk -> do SMTReasonUnknown
ur <- m SMTReasonUnknown
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
(Bool, [SMTResult]) -> m (Bool, [SMTResult])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [SMTConfig -> [String] -> Maybe SMTResult -> SMTResult
ProofError SMTConfig
cfg [SMTReasonUnknown -> String
forall a. Show a => a -> String
show SMTReasonUnknown
ur] Maybe SMTResult
forall a. Maybe a
Nothing])
where continue :: (SMTModel -> a) -> m (Bool, [a])
continue classify :: SMTModel -> a
classify = do SMTModel
m <- m SMTModel
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
(limReached :: Bool
limReached, fronts :: [SMTModel]
fronts) <- Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
getParetoFronts (Int -> Int -> Int
forall a. Num a => a -> a -> a
subtract 1 (Int -> Int) -> Maybe Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
mbN) [SMTModel
m]
(Bool, [a]) -> m (Bool, [a])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
limReached, [a] -> [a]
forall a. [a] -> [a]
reverse ((SMTModel -> a) -> [SMTModel] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map SMTModel -> a
classify [SMTModel]
fronts))
getParetoFronts :: (MonadIO m, MonadQuery m) => Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
getParetoFronts :: Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
getParetoFronts (Just i :: Int
i) sofar :: [SMTModel]
sofar | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 = (Bool, [SMTModel]) -> m (Bool, [SMTModel])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [SMTModel]
sofar)
getParetoFronts mbi :: Maybe Int
mbi sofar :: [SMTModel]
sofar = do CheckSatResult
cs <- m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
let more :: m (Bool, [SMTModel])
more = m SMTModel
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel m SMTModel
-> (SMTModel -> m (Bool, [SMTModel])) -> m (Bool, [SMTModel])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \m :: SMTModel
m -> Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
getParetoFronts (Int -> Int -> Int
forall a. Num a => a -> a -> a
subtract 1 (Int -> Int) -> Maybe Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
mbi) (SMTModel
m SMTModel -> [SMTModel] -> [SMTModel]
forall a. a -> [a] -> [a]
: [SMTModel]
sofar)
case CheckSatResult
cs of
Unsat -> (Bool, [SMTModel]) -> m (Bool, [SMTModel])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [SMTModel]
sofar)
Sat -> m (Bool, [SMTModel])
more
Unk -> m (Bool, [SMTModel])
more
getModel :: (MonadIO m, MonadQuery m) => m SMTModel
getModel :: m SMTModel
getModel = Maybe Int -> m SMTModel
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> m SMTModel
getModelAtIndex Maybe Int
forall a. Maybe a
Nothing
getModelAtIndex :: (MonadIO m, MonadQuery m) => Maybe Int -> m SMTModel
getModelAtIndex :: Maybe Int -> m SMTModel
getModelAtIndex mbi :: Maybe Int
mbi = do
State{IORef SBVRunMode
runMode :: State -> IORef SBVRunMode
runMode :: IORef SBVRunMode
runMode} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
SBVRunMode
rm <- IO SBVRunMode -> m SBVRunMode
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO SBVRunMode -> m SBVRunMode) -> IO SBVRunMode -> m SBVRunMode
forall a b. (a -> b) -> a -> b
$ IORef SBVRunMode -> IO SBVRunMode
forall a. IORef a -> IO a
readIORef IORef SBVRunMode
runMode
case SBVRunMode
rm of
m :: SBVRunMode
m@SBVRunMode
CodeGen -> String -> m SMTModel
forall a. HasCallStack => String -> a
error (String -> m SMTModel) -> String -> m SMTModel
forall a b. (a -> b) -> a -> b
$ "SBV.getModel: Model is not available in mode: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVRunMode -> String
forall a. Show a => a -> String
show SBVRunMode
m
m :: SBVRunMode
m@Concrete{} -> String -> m SMTModel
forall a. HasCallStack => String -> a
error (String -> m SMTModel) -> String -> m SMTModel
forall a b. (a -> b) -> a -> b
$ "SBV.getModel: Model is not available in mode: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVRunMode -> String
forall a. Show a => a -> String
show SBVRunMode
m
SMTMode _ _ isSAT :: Bool
isSAT _ -> do
SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
[(Quantifier, NamedSymVar)]
qinps <- m [(Quantifier, NamedSymVar)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(Quantifier, NamedSymVar)]
getQuantifiedInputs
[(String, SBVType)]
uis <- m [(String, SBVType)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, SBVType)]
getUIs
let allModelInputs :: [(Quantifier, NamedSymVar)]
allModelInputs = if Bool
isSAT then ((Quantifier, NamedSymVar) -> Bool)
-> [(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile ((Quantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
/= Quantifier
ALL) (Quantifier -> Bool)
-> ((Quantifier, NamedSymVar) -> Quantifier)
-> (Quantifier, NamedSymVar)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Quantifier, NamedSymVar) -> Quantifier
forall a b. (a, b) -> a
fst) [(Quantifier, NamedSymVar)]
qinps
else ((Quantifier, NamedSymVar) -> Bool)
-> [(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile ((Quantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
== Quantifier
ALL) (Quantifier -> Bool)
-> ((Quantifier, NamedSymVar) -> Quantifier)
-> (Quantifier, NamedSymVar)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Quantifier, NamedSymVar) -> Quantifier
forall a b. (a, b) -> a
fst) [(Quantifier, NamedSymVar)]
qinps
grabObservables :: Bool
grabObservables = [(Quantifier, NamedSymVar)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Quantifier, NamedSymVar)]
allModelInputs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [(Quantifier, NamedSymVar)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Quantifier, NamedSymVar)]
qinps
[(String, CV)]
obsvs <- if Bool
grabObservables
then m [(String, CV)]
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m [(String, CV)]
getObservables
else do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["*** In a quantified context, obvservables will not be printed."]
[(String, CV)] -> m [(String, CV)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
let sortByNodeId :: [(SV, (String, CV))] -> [(String, CV)]
sortByNodeId :: [(SV, (String, CV))] -> [(String, CV)]
sortByNodeId = ((SV, (String, CV)) -> (String, CV))
-> [(SV, (String, CV))] -> [(String, CV)]
forall a b. (a -> b) -> [a] -> [b]
map (SV, (String, CV)) -> (String, CV)
forall a b. (a, b) -> b
snd ([(SV, (String, CV))] -> [(String, CV)])
-> ([(SV, (String, CV))] -> [(SV, (String, CV))])
-> [(SV, (String, CV))]
-> [(String, CV)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SV, (String, CV)) -> (SV, (String, CV)) -> Ordering)
-> [(SV, (String, CV))] -> [(SV, (String, CV))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (NodeId -> NodeId -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (NodeId -> NodeId -> Ordering)
-> ((SV, (String, CV)) -> NodeId)
-> (SV, (String, CV))
-> (SV, (String, CV))
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (\(SV _ nid :: NodeId
nid, _) -> NodeId
nid))
grab :: (SV, b) -> f (SV, (b, CV))
grab (sv :: SV
sv, nm :: b
nm) = CV -> (SV, (b, CV))
forall b. b -> (SV, (b, b))
wrap (CV -> (SV, (b, CV))) -> f CV -> f (SV, (b, CV))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int -> SV -> f CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> SV -> m CV
getValueCV Maybe Int
mbi SV
sv
where wrap :: b -> (SV, (b, b))
wrap c :: b
c = (SV
sv, (b
nm, b
c))
[(SV, (String, CV))]
inputAssocs <- ((Quantifier, NamedSymVar) -> m (SV, (String, CV)))
-> [(Quantifier, NamedSymVar)] -> m [(SV, (String, CV))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (NamedSymVar -> m (SV, (String, CV))
forall (f :: * -> *) b.
(MonadIO f, MonadQuery f) =>
(SV, b) -> f (SV, (b, CV))
grab (NamedSymVar -> m (SV, (String, CV)))
-> ((Quantifier, NamedSymVar) -> NamedSymVar)
-> (Quantifier, NamedSymVar)
-> m (SV, (String, CV))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Quantifier, NamedSymVar) -> NamedSymVar
forall a b. (a, b) -> b
snd) [(Quantifier, NamedSymVar)]
allModelInputs
let assocs :: [(String, CV)]
assocs = ((String, CV) -> String) -> [(String, CV)] -> [(String, CV)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (String, CV) -> String
forall a b. (a, b) -> a
fst [(String, CV)]
obsvs
[(String, CV)] -> [(String, CV)] -> [(String, CV)]
forall a. [a] -> [a] -> [a]
++ [(SV, (String, CV))] -> [(String, CV)]
sortByNodeId [(SV, (String, CV))
p | p :: (SV, (String, CV))
p@(_, (nm :: String
nm, _)) <- [(SV, (String, CV))]
inputAssocs, Bool -> Bool
not (SMTConfig -> String -> Bool
isNonModelVar SMTConfig
cfg String
nm)]
let uiFuns :: [(String, SBVType)]
uiFuns = [(String, SBVType)
ui | ui :: (String, SBVType)
ui@(_, SBVType as :: [Kind]
as) <- [(String, SBVType)]
uis, [Kind] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
as Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1, SMTConfig -> Bool
satTrackUFs SMTConfig
cfg]
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(String, SBVType)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, SBVType)]
uiFuns) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
let solverCaps :: SolverCapabilities
solverCaps = SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)
in case SolverCapabilities -> Maybe [String]
supportsFlattenedModels SolverCapabilities
solverCaps of
Nothing -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just cmds :: [String]
cmds -> (String -> m ()) -> [String] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True) [String]
cmds
Maybe [((Quantifier, NamedSymVar), Maybe CV)]
bindings <- let get :: (Quantifier, (SV, b)) -> m ((Quantifier, (SV, b)), Maybe CV)
get i :: (Quantifier, (SV, b))
i@(ALL, _) = ((Quantifier, (SV, b)), Maybe CV)
-> m ((Quantifier, (SV, b)), Maybe CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, (SV, b))
i, Maybe CV
forall a. Maybe a
Nothing)
get i :: (Quantifier, (SV, b))
i@(EX, (sv :: SV
sv, _)) = case SV
sv SV -> [(SV, (String, CV))] -> Maybe (String, CV)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(SV, (String, CV))]
inputAssocs of
Just (_, cv :: CV
cv) -> ((Quantifier, (SV, b)), Maybe CV)
-> m ((Quantifier, (SV, b)), Maybe CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, (SV, b))
i, CV -> Maybe CV
forall a. a -> Maybe a
Just CV
cv)
Nothing -> do CV
cv <- Maybe Int -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> SV -> m CV
getValueCV Maybe Int
mbi SV
sv
((Quantifier, (SV, b)), Maybe CV)
-> m ((Quantifier, (SV, b)), Maybe CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, (SV, b))
i, CV -> Maybe CV
forall a. a -> Maybe a
Just CV
cv)
flipQ :: (Quantifier, b) -> (Quantifier, b)
flipQ i :: (Quantifier, b)
i@(q :: Quantifier
q, sv :: b
sv) = case (Bool
isSAT, Quantifier
q) of
(True, _ ) -> (Quantifier, b)
i
(False, EX) -> (Quantifier
ALL, b
sv)
(False, ALL) -> (Quantifier
EX, b
sv)
in if SMTConfig -> Bool
validationRequested SMTConfig
cfg
then [((Quantifier, NamedSymVar), Maybe CV)]
-> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
forall a. a -> Maybe a
Just ([((Quantifier, NamedSymVar), Maybe CV)]
-> Maybe [((Quantifier, NamedSymVar), Maybe CV)])
-> m [((Quantifier, NamedSymVar), Maybe CV)]
-> m (Maybe [((Quantifier, NamedSymVar), Maybe CV)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV))
-> [(Quantifier, NamedSymVar)]
-> m [((Quantifier, NamedSymVar), Maybe CV)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV)
forall (m :: * -> *) b.
(MonadIO m, MonadQuery m) =>
(Quantifier, (SV, b)) -> m ((Quantifier, (SV, b)), Maybe CV)
get ((Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV))
-> ((Quantifier, NamedSymVar) -> (Quantifier, NamedSymVar))
-> (Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Quantifier, NamedSymVar) -> (Quantifier, NamedSymVar)
forall b. (Quantifier, b) -> (Quantifier, b)
flipQ) [(Quantifier, NamedSymVar)]
qinps
else Maybe [((Quantifier, NamedSymVar), Maybe CV)]
-> m (Maybe [((Quantifier, NamedSymVar), Maybe CV)])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [((Quantifier, NamedSymVar), Maybe CV)]
forall a. Maybe a
Nothing
[(String, (SBVType, ([([CV], CV)], CV)))]
uivs <- ((String, SBVType) -> m (String, (SBVType, ([([CV], CV)], CV))))
-> [(String, SBVType)]
-> m [(String, (SBVType, ([([CV], CV)], CV)))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ui :: (String, SBVType)
ui@(nm :: String
nm, t :: SBVType
t) -> (\a :: ([([CV], CV)], CV)
a -> (String
nm, (SBVType
t, ([([CV], CV)], CV)
a))) (([([CV], CV)], CV) -> (String, (SBVType, ([([CV], CV)], CV))))
-> m ([([CV], CV)], CV)
-> m (String, (SBVType, ([([CV], CV)], CV)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int -> (String, SBVType) -> m ([([CV], CV)], CV)
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> (String, SBVType) -> m ([([CV], CV)], CV)
getUIFunCVAssoc Maybe Int
mbi (String, SBVType)
ui) [(String, SBVType)]
uiFuns
SMTModel -> m SMTModel
forall (m :: * -> *) a. Monad m => a -> m a
return SMTModel :: [(String, GeneralizedCV)]
-> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
-> [(String, CV)]
-> [(String, (SBVType, ([([CV], CV)], CV)))]
-> SMTModel
SMTModel { modelObjectives :: [(String, GeneralizedCV)]
modelObjectives = []
, modelBindings :: Maybe [((Quantifier, NamedSymVar), Maybe CV)]
modelBindings = Maybe [((Quantifier, NamedSymVar), Maybe CV)]
bindings
, modelAssocs :: [(String, CV)]
modelAssocs = [(String, CV)]
assocs
, modelUIFuns :: [(String, (SBVType, ([([CV], CV)], CV)))]
modelUIFuns = [(String, (SBVType, ([([CV], CV)], CV)))]
uivs
}
getObjectiveValues :: forall m. (MonadIO m, MonadQuery m) => m [(String, GeneralizedCV)]
getObjectiveValues :: m [(String, GeneralizedCV)]
getObjectiveValues = do let cmd :: String
cmd = "(get-objectives)"
bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected "getObjectiveValues" String
cmd "a list of objective values" Maybe [String]
forall a. Maybe a
Nothing
String
r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd
[NamedSymVar]
inputs <- ((Quantifier, NamedSymVar) -> NamedSymVar)
-> [(Quantifier, NamedSymVar)] -> [NamedSymVar]
forall a b. (a -> b) -> [a] -> [b]
map (Quantifier, NamedSymVar) -> NamedSymVar
forall a b. (a, b) -> b
snd ([(Quantifier, NamedSymVar)] -> [NamedSymVar])
-> m [(Quantifier, NamedSymVar)] -> m [NamedSymVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m [(Quantifier, NamedSymVar)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(Quantifier, NamedSymVar)]
getQuantifiedInputs
String
-> (String -> Maybe [String] -> m [(String, GeneralizedCV)])
-> (SExpr -> m [(String, GeneralizedCV)])
-> m [(String, GeneralizedCV)]
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m [(String, GeneralizedCV)]
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m [(String, GeneralizedCV)])
-> m [(String, GeneralizedCV)])
-> (SExpr -> m [(String, GeneralizedCV)])
-> m [(String, GeneralizedCV)]
forall a b. (a -> b) -> a -> b
$ \case EApp (ECon "objectives" : es :: [SExpr]
es) -> [Maybe (String, GeneralizedCV)] -> [(String, GeneralizedCV)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (String, GeneralizedCV)] -> [(String, GeneralizedCV)])
-> m [Maybe (String, GeneralizedCV)] -> m [(String, GeneralizedCV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SExpr -> m (Maybe (String, GeneralizedCV)))
-> [SExpr] -> m [Maybe (String, GeneralizedCV)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((forall a. Maybe [String] -> m a)
-> [NamedSymVar] -> SExpr -> m (Maybe (String, GeneralizedCV))
getObjValue (String -> Maybe [String] -> m a
forall a. String -> Maybe [String] -> m a
bad String
r) [NamedSymVar]
inputs) [SExpr]
es
_ -> String -> Maybe [String] -> m [(String, GeneralizedCV)]
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
where
getObjValue :: (forall a. Maybe [String] -> m a) -> [NamedSymVar] -> SExpr -> m (Maybe (String, GeneralizedCV))
getObjValue :: (forall a. Maybe [String] -> m a)
-> [NamedSymVar] -> SExpr -> m (Maybe (String, GeneralizedCV))
getObjValue bailOut :: forall a. Maybe [String] -> m a
bailOut inputs :: [NamedSymVar]
inputs expr :: SExpr
expr =
case SExpr
expr of
EApp [_] -> Maybe (String, GeneralizedCV) -> m (Maybe (String, GeneralizedCV))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (String, GeneralizedCV)
forall a. Maybe a
Nothing
EApp [ECon nm :: String
nm, v :: SExpr
v] -> String -> SExpr -> m (Maybe (String, GeneralizedCV))
locate String
nm SExpr
v
_ -> String -> m (Maybe (String, GeneralizedCV))
forall a. String -> m a
dontUnderstand (SExpr -> String
forall a. Show a => a -> String
show SExpr
expr)
where locate :: String -> SExpr -> m (Maybe (String, GeneralizedCV))
locate nm :: String
nm v :: SExpr
v = case [NamedSymVar] -> Maybe NamedSymVar
forall a. [a] -> Maybe a
listToMaybe [NamedSymVar
p | p :: NamedSymVar
p@(sv :: SV
sv, _) <- [NamedSymVar]
inputs, SV -> String
forall a. Show a => a -> String
show SV
sv String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
nm] of
Nothing -> Maybe (String, GeneralizedCV) -> m (Maybe (String, GeneralizedCV))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (String, GeneralizedCV)
forall a. Maybe a
Nothing
Just (sv :: SV
sv, actualName :: String
actualName) -> SV -> SExpr -> m GeneralizedCV
grab SV
sv SExpr
v m GeneralizedCV
-> (GeneralizedCV -> m (Maybe (String, GeneralizedCV)))
-> m (Maybe (String, GeneralizedCV))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \val :: GeneralizedCV
val -> Maybe (String, GeneralizedCV) -> m (Maybe (String, GeneralizedCV))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (String, GeneralizedCV)
-> m (Maybe (String, GeneralizedCV)))
-> Maybe (String, GeneralizedCV)
-> m (Maybe (String, GeneralizedCV))
forall a b. (a -> b) -> a -> b
$ (String, GeneralizedCV) -> Maybe (String, GeneralizedCV)
forall a. a -> Maybe a
Just (String
actualName, GeneralizedCV
val)
dontUnderstand :: String -> m a
dontUnderstand s :: String
s = Maybe [String] -> m a
forall a. Maybe [String] -> m a
bailOut (Maybe [String] -> m a) -> Maybe [String] -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just [ "Unable to understand solver output."
, "While trying to process: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
]
grab :: SV -> SExpr -> m GeneralizedCV
grab :: SV -> SExpr -> m GeneralizedCV
grab s :: SV
s topExpr :: SExpr
topExpr
| Just v :: CV
v <- Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
k SExpr
topExpr = GeneralizedCV -> m GeneralizedCV
forall (m :: * -> *) a. Monad m => a -> m a
return (GeneralizedCV -> m GeneralizedCV)
-> GeneralizedCV -> m GeneralizedCV
forall a b. (a -> b) -> a -> b
$ CV -> GeneralizedCV
RegularCV CV
v
| Bool
True = ExtCV -> GeneralizedCV
ExtendedCV (ExtCV -> GeneralizedCV) -> m ExtCV -> m GeneralizedCV
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> m ExtCV
cvt (SExpr -> SExpr
simplify SExpr
topExpr)
where k :: Kind
k = SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
s
cvt :: SExpr -> m ExtCV
cvt :: SExpr -> m ExtCV
cvt (ECon "oo") = ExtCV -> m ExtCV
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtCV -> m ExtCV) -> ExtCV -> m ExtCV
forall a b. (a -> b) -> a -> b
$ Kind -> ExtCV
Infinite Kind
k
cvt (ECon "epsilon") = ExtCV -> m ExtCV
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtCV -> m ExtCV) -> ExtCV -> m ExtCV
forall a b. (a -> b) -> a -> b
$ Kind -> ExtCV
Epsilon Kind
k
cvt (EApp [ECon "interval", x :: SExpr
x, y :: SExpr
y]) = ExtCV -> ExtCV -> ExtCV
Interval (ExtCV -> ExtCV -> ExtCV) -> m ExtCV -> m (ExtCV -> ExtCV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> m ExtCV
cvt SExpr
x m (ExtCV -> ExtCV) -> m ExtCV -> m ExtCV
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> m ExtCV
cvt SExpr
y
cvt (ENum (i :: Integer
i, _)) = ExtCV -> m ExtCV
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtCV -> m ExtCV) -> ExtCV -> m ExtCV
forall a b. (a -> b) -> a -> b
$ CV -> ExtCV
BoundedCV (CV -> ExtCV) -> CV -> ExtCV
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k Integer
i
cvt (EReal r :: AlgReal
r) = ExtCV -> m ExtCV
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtCV -> m ExtCV) -> ExtCV -> m ExtCV
forall a b. (a -> b) -> a -> b
$ CV -> ExtCV
BoundedCV (CV -> ExtCV) -> CV -> ExtCV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ AlgReal -> CVal
CAlgReal AlgReal
r
cvt (EFloat f :: Float
f) = ExtCV -> m ExtCV
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtCV -> m ExtCV) -> ExtCV -> m ExtCV
forall a b. (a -> b) -> a -> b
$ CV -> ExtCV
BoundedCV (CV -> ExtCV) -> CV -> ExtCV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ Float -> CVal
CFloat Float
f
cvt (EDouble d :: Double
d) = ExtCV -> m ExtCV
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtCV -> m ExtCV) -> ExtCV -> m ExtCV
forall a b. (a -> b) -> a -> b
$ CV -> ExtCV
BoundedCV (CV -> ExtCV) -> CV -> ExtCV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ Double -> CVal
CDouble Double
d
cvt (EApp [ECon "+", x :: SExpr
x, y :: SExpr
y]) = ExtCV -> ExtCV -> ExtCV
AddExtCV (ExtCV -> ExtCV -> ExtCV) -> m ExtCV -> m (ExtCV -> ExtCV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> m ExtCV
cvt SExpr
x m (ExtCV -> ExtCV) -> m ExtCV -> m ExtCV
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> m ExtCV
cvt SExpr
y
cvt (EApp [ECon "*", x :: SExpr
x, y :: SExpr
y]) = ExtCV -> ExtCV -> ExtCV
MulExtCV (ExtCV -> ExtCV -> ExtCV) -> m ExtCV -> m (ExtCV -> ExtCV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> m ExtCV
cvt SExpr
x m (ExtCV -> ExtCV) -> m ExtCV -> m ExtCV
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> m ExtCV
cvt SExpr
y
cvt e :: SExpr
e = String -> m ExtCV
forall a. String -> m a
dontUnderstand (SExpr -> String
forall a. Show a => a -> String
show SExpr
e)
simplify :: SExpr -> SExpr
simplify :: SExpr -> SExpr
simplify (EApp [ECon "to_real", n :: SExpr
n]) = SExpr
n
simplify (EApp xs :: [SExpr]
xs) = [SExpr] -> SExpr
EApp ((SExpr -> SExpr) -> [SExpr] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map SExpr -> SExpr
simplify [SExpr]
xs)
simplify e :: SExpr
e = SExpr
e
checkSatAssuming :: (MonadIO m, MonadQuery m) => [SBool] -> m CheckSatResult
checkSatAssuming :: [SBool] -> m CheckSatResult
checkSatAssuming sBools :: [SBool]
sBools = (CheckSatResult, Maybe [SBool]) -> CheckSatResult
forall a b. (a, b) -> a
fst ((CheckSatResult, Maybe [SBool]) -> CheckSatResult)
-> m (CheckSatResult, Maybe [SBool]) -> m CheckSatResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
checkSatAssumingHelper Bool
False [SBool]
sBools
checkSatAssumingWithUnsatisfiableSet :: (MonadIO m, MonadQuery m) => [SBool] -> m (CheckSatResult, Maybe [SBool])
checkSatAssumingWithUnsatisfiableSet :: [SBool] -> m (CheckSatResult, Maybe [SBool])
checkSatAssumingWithUnsatisfiableSet = Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
checkSatAssumingHelper Bool
True
checkSatAssumingHelper :: (MonadIO m, MonadQuery m) => Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
checkSatAssumingHelper :: Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
checkSatAssumingHelper getAssumptions :: Bool
getAssumptions sBools :: [SBool]
sBools = do
let mkAssumption :: State -> IO [(String, [String], (String, SBool))]
mkAssumption st :: State
st = do [(SV, SBool)]
swsOriginal <- (SBool -> IO (SV, SBool)) -> [SBool] -> IO [(SV, SBool)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\sb :: SBool
sb -> do SV
sv <- State -> SBool -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBool
sb
(SV, SBool) -> IO (SV, SBool)
forall (m :: * -> *) a. Monad m => a -> m a
return (SV
sv, SBool
sb)) [SBool]
sBools
let swbs :: [(SV, SBool)]
swbs = [(SV, SBool)
p | p :: (SV, SBool)
p@(sv :: SV
sv, _) <- ((SV, SBool) -> (SV, SBool) -> Bool)
-> [(SV, SBool)] -> [(SV, SBool)]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
(==) (SV -> SV -> Bool)
-> ((SV, SBool) -> SV) -> (SV, SBool) -> (SV, SBool) -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (SV, SBool) -> SV
forall a b. (a, b) -> a
fst) [(SV, SBool)]
swsOriginal, SV
sv SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
/= SV
trueSV]
[(SV, (Int, SBool))]
uniqueSWBs <- ((SV, SBool) -> IO (SV, (Int, SBool)))
-> [(SV, SBool)] -> IO [(SV, (Int, SBool))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(sv :: SV
sv, sb :: SBool
sb) -> do Int
unique <- State -> IO Int
incrementInternalCounter State
st
(SV, (Int, SBool)) -> IO (SV, (Int, SBool))
forall (m :: * -> *) a. Monad m => a -> m a
return (SV
sv, (Int
unique, SBool
sb))) [(SV, SBool)]
swbs
let translate :: (a, (a, b)) -> (String, [String], (String, b))
translate (sv :: a
sv, (unique :: a
unique, sb :: b
sb)) = (String
nm, [String]
decls, (String
proxy, b
sb))
where nm :: String
nm = a -> String
forall a. Show a => a -> String
show a
sv
proxy :: String
proxy = "__assumption_proxy_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
unique
decls :: [String]
decls = [ "(declare-const " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
proxy String -> String -> String
forall a. [a] -> [a] -> [a]
++ " Bool)"
, "(assert (= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
proxy String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))"
]
[(String, [String], (String, SBool))]
-> IO [(String, [String], (String, SBool))]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(String, [String], (String, SBool))]
-> IO [(String, [String], (String, SBool))])
-> [(String, [String], (String, SBool))]
-> IO [(String, [String], (String, SBool))]
forall a b. (a -> b) -> a -> b
$ ((SV, (Int, SBool)) -> (String, [String], (String, SBool)))
-> [(SV, (Int, SBool))] -> [(String, [String], (String, SBool))]
forall a b. (a -> b) -> [a] -> [b]
map (SV, (Int, SBool)) -> (String, [String], (String, SBool))
forall a a b.
(Show a, Show a) =>
(a, (a, b)) -> (String, [String], (String, b))
translate [(SV, (Int, SBool))]
uniqueSWBs
[(String, [String], (String, SBool))]
assumptions <- (State -> IO [(String, [String], (String, SBool))])
-> m [(String, [String], (String, SBool))]
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext State -> IO [(String, [String], (String, SBool))]
mkAssumption
let (origNames :: [String]
origNames, declss :: [[String]]
declss, proxyMap :: [(String, SBool)]
proxyMap) = [(String, [String], (String, SBool))]
-> ([String], [[String]], [(String, SBool)])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 [(String, [String], (String, SBool))]
assumptions
let cmd :: String
cmd = "(check-sat-assuming (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (((String, SBool) -> String) -> [(String, SBool)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, SBool) -> String
forall a b. (a, b) -> a
fst [(String, SBool)]
proxyMap) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))"
bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected "checkSatAssuming" String
cmd "one of sat/unsat/unknown"
(Maybe [String] -> String -> Maybe [String] -> m a)
-> Maybe [String] -> String -> Maybe [String] -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just [ "Make sure you use:"
, ""
, " setOption $ ProduceUnsatAssumptions True"
, ""
, "to tell the solver to produce unsat assumptions."
]
(String -> m ()) -> [String] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True) ([String] -> m ()) -> [String] -> m ()
forall a b. (a -> b) -> a -> b
$ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
declss
String
r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd
let grabUnsat :: m (CheckSatResult, Maybe [SBool])
grabUnsat
| Bool
getAssumptions = do [SBool]
as <- [String] -> [(String, SBool)] -> m [SBool]
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
[String] -> [(String, a)] -> m [a]
getUnsatAssumptions [String]
origNames [(String, SBool)]
proxyMap
(CheckSatResult, Maybe [SBool])
-> m (CheckSatResult, Maybe [SBool])
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckSatResult
Unsat, [SBool] -> Maybe [SBool]
forall a. a -> Maybe a
Just [SBool]
as)
| Bool
True = (CheckSatResult, Maybe [SBool])
-> m (CheckSatResult, Maybe [SBool])
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckSatResult
Unsat, Maybe [SBool]
forall a. Maybe a
Nothing)
String
-> (String -> Maybe [String] -> m (CheckSatResult, Maybe [SBool]))
-> (SExpr -> m (CheckSatResult, Maybe [SBool]))
-> m (CheckSatResult, Maybe [SBool])
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m (CheckSatResult, Maybe [SBool])
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m (CheckSatResult, Maybe [SBool]))
-> m (CheckSatResult, Maybe [SBool]))
-> (SExpr -> m (CheckSatResult, Maybe [SBool]))
-> m (CheckSatResult, Maybe [SBool])
forall a b. (a -> b) -> a -> b
$ \case ECon "sat" -> (CheckSatResult, Maybe [SBool])
-> m (CheckSatResult, Maybe [SBool])
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckSatResult
Sat, Maybe [SBool]
forall a. Maybe a
Nothing)
ECon "unsat" -> m (CheckSatResult, Maybe [SBool])
grabUnsat
ECon "unknown" -> (CheckSatResult, Maybe [SBool])
-> m (CheckSatResult, Maybe [SBool])
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckSatResult
Unk, Maybe [SBool]
forall a. Maybe a
Nothing)
_ -> String -> Maybe [String] -> m (CheckSatResult, Maybe [SBool])
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
getAssertionStackDepth :: (MonadIO m, MonadQuery m) => m Int
getAssertionStackDepth :: m Int
getAssertionStackDepth = QueryState -> Int
queryAssertionStackDepth (QueryState -> Int) -> m QueryState -> m Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState
restoreTablesAndArrays :: (MonadIO m, MonadQuery m) => m ()
restoreTablesAndArrays :: m ()
restoreTablesAndArrays = do State
st <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
Int
tCount <- Map (Kind, Kind, [SV]) Int -> Int
forall k a. Map k a -> Int
M.size (Map (Kind, Kind, [SV]) Int -> Int)
-> m (Map (Kind, Kind, [SV]) Int) -> m Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (IO (Map (Kind, Kind, [SV]) Int) -> m (Map (Kind, Kind, [SV]) Int)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (Map (Kind, Kind, [SV]) Int) -> m (Map (Kind, Kind, [SV]) Int))
-> (IORef (Map (Kind, Kind, [SV]) Int)
-> IO (Map (Kind, Kind, [SV]) Int))
-> IORef (Map (Kind, Kind, [SV]) Int)
-> m (Map (Kind, Kind, [SV]) Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IORef (Map (Kind, Kind, [SV]) Int)
-> IO (Map (Kind, Kind, [SV]) Int)
forall a. IORef a -> IO a
readIORef) (State -> IORef (Map (Kind, Kind, [SV]) Int)
rtblMap State
st)
Int
aCount <- IntMap ArrayInfo -> Int
forall a. IntMap a -> Int
IM.size (IntMap ArrayInfo -> Int) -> m (IntMap ArrayInfo) -> m Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (IO (IntMap ArrayInfo) -> m (IntMap ArrayInfo)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (IntMap ArrayInfo) -> m (IntMap ArrayInfo))
-> (IORef (IntMap ArrayInfo) -> IO (IntMap ArrayInfo))
-> IORef (IntMap ArrayInfo)
-> m (IntMap ArrayInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IORef (IntMap ArrayInfo) -> IO (IntMap ArrayInfo)
forall a. IORef a -> IO a
readIORef) (State -> IORef (IntMap ArrayInfo)
rArrayMap State
st)
let tInits :: [String]
tInits = [ "table" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_initializer" | Int
i <- [0 .. Int
tCount Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1]]
aInits :: [String]
aInits = [ "array_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_initializer" | Int
i <- [0 .. Int
aCount Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1]]
inits :: [String]
inits = [String]
tInits [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
aInits
case [String]
inits of
[] -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
[x :: String
x] -> Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
xs :: [String]
xs -> Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "(assert (and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))"
inNewAssertionStack :: (MonadIO m, MonadQuery m) => m a -> m a
inNewAssertionStack :: m a -> m a
inNewAssertionStack q :: m a
q = do Int -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
push 1
a
r <- m a
q
Int -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
pop 1
a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r
push :: (MonadIO m, MonadQuery m) => Int -> m ()
push :: Int -> m ()
push i :: Int
i
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 = String -> m ()
forall a. HasCallStack => String -> a
error (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "Data.SBV: push requires a strictly positive level argument, received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
| Bool
True = do Int
depth <- m Int
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m Int
getAssertionStackDepth
Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "(push " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
(QueryState -> QueryState) -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(QueryState -> QueryState) -> m ()
modifyQueryState ((QueryState -> QueryState) -> m ())
-> (QueryState -> QueryState) -> m ()
forall a b. (a -> b) -> a -> b
$ \s :: QueryState
s -> QueryState
s{queryAssertionStackDepth :: Int
queryAssertionStackDepth = Int
depth Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
i}
pop :: (MonadIO m, MonadQuery m) => Int -> m ()
pop :: Int -> m ()
pop i :: Int
i
| Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 = String -> m ()
forall a. HasCallStack => String -> a
error (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "Data.SBV: pop requires a strictly positive level argument, received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
| Bool
True = do Int
depth <- m Int
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m Int
getAssertionStackDepth
if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
depth
then String -> m ()
forall a. HasCallStack => String -> a
error (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "Data.SBV: Illegally trying to pop " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. (Eq a, Num a, Show a) => a -> String
shl Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ ", at current level: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
depth
else do QueryState{SMTConfig
queryConfig :: QueryState -> SMTConfig
queryConfig :: SMTConfig
queryConfig} <- m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState
if Bool -> Bool
not (SolverCapabilities -> Bool
supportsGlobalDecls (SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
queryConfig)))
then String -> m ()
forall a. HasCallStack => String -> a
error (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
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 Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "(pop " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m ()
restoreTablesAndArrays
(QueryState -> QueryState) -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(QueryState -> QueryState) -> m ()
modifyQueryState ((QueryState -> QueryState) -> m ())
-> (QueryState -> QueryState) -> m ()
forall a b. (a -> b) -> a -> b
$ \s :: QueryState
s -> QueryState
s{queryAssertionStackDepth :: Int
queryAssertionStackDepth = Int
depth Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i}
where shl :: a -> String
shl 1 = "one level"
shl n :: a
n = a -> String
forall a. Show a => a -> String
show a
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ " levels"
caseSplit :: (MonadIO m, MonadQuery m) => Bool -> [(String, SBool)] -> m (Maybe (String, SMTResult))
caseSplit :: Bool -> [(String, SBool)] -> m (Maybe (String, SMTResult))
caseSplit printCases :: Bool
printCases cases :: [(String, SBool)]
cases = do SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
SMTConfig -> [(String, SBool)] -> m (Maybe (String, SMTResult))
go SMTConfig
cfg ([(String, SBool)]
cases [(String, SBool)] -> [(String, SBool)] -> [(String, SBool)]
forall a. [a] -> [a] -> [a]
++ [("Coverage", SBool -> SBool
sNot ([SBool] -> SBool
sOr (((String, SBool) -> SBool) -> [(String, SBool)] -> [SBool]
forall a b. (a -> b) -> [a] -> [b]
map (String, SBool) -> SBool
forall a b. (a, b) -> b
snd [(String, SBool)]
cases)))])
where msg :: String -> m ()
msg = Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
printCases (m () -> m ()) -> (String -> m ()) -> String -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> (String -> IO ()) -> String -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn
go :: SMTConfig -> [(String, SBool)] -> m (Maybe (String, SMTResult))
go _ [] = Maybe (String, SMTResult) -> m (Maybe (String, SMTResult))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (String, SMTResult)
forall a. Maybe a
Nothing
go cfg :: SMTConfig
cfg ((n :: String
n,c :: SBool
c):ncs :: [(String, SBool)]
ncs) = do let notify :: String -> m ()
notify s :: String
s = String -> m ()
msg (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "Case " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
String -> m ()
notify "Starting"
CheckSatResult
r <- [SBool] -> m CheckSatResult
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
[SBool] -> m CheckSatResult
checkSatAssuming [SBool
c]
case CheckSatResult
r of
Unsat -> do String -> m ()
notify "Unsatisfiable"
SMTConfig -> [(String, SBool)] -> m (Maybe (String, SMTResult))
go SMTConfig
cfg [(String, SBool)]
ncs
Sat -> do String -> m ()
notify "Satisfiable"
SMTResult
res <- SMTConfig -> SMTModel -> SMTResult
Satisfiable SMTConfig
cfg (SMTModel -> SMTResult) -> m SMTModel -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTModel
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
Maybe (String, SMTResult) -> m (Maybe (String, SMTResult))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (String, SMTResult) -> m (Maybe (String, SMTResult)))
-> Maybe (String, SMTResult) -> m (Maybe (String, SMTResult))
forall a b. (a -> b) -> a -> b
$ (String, SMTResult) -> Maybe (String, SMTResult)
forall a. a -> Maybe a
Just (String
n, SMTResult
res)
Unk -> do String -> m ()
notify "Unknown"
SMTResult
res <- SMTConfig -> SMTReasonUnknown -> SMTResult
Unknown SMTConfig
cfg (SMTReasonUnknown -> SMTResult)
-> m SMTReasonUnknown -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTReasonUnknown
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
Maybe (String, SMTResult) -> m (Maybe (String, SMTResult))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (String, SMTResult) -> m (Maybe (String, SMTResult)))
-> Maybe (String, SMTResult) -> m (Maybe (String, SMTResult))
forall a b. (a -> b) -> a -> b
$ (String, SMTResult) -> Maybe (String, SMTResult)
forall a. a -> Maybe a
Just (String
n, SMTResult
res)
resetAssertions :: (MonadIO m, MonadQuery m) => m ()
resetAssertions :: m ()
resetAssertions = do Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True "(reset-assertions)"
(QueryState -> QueryState) -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(QueryState -> QueryState) -> m ()
modifyQueryState ((QueryState -> QueryState) -> m ())
-> (QueryState -> QueryState) -> m ()
forall a b. (a -> b) -> a -> b
$ \s :: QueryState
s -> QueryState
s{ queryAssertionStackDepth :: Int
queryAssertionStackDepth = 0 }
m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m ()
restoreTablesAndArrays
echo :: (MonadIO m, MonadQuery m) => String -> m ()
echo :: String -> m ()
echo s :: String
s = do let cmd :: String
cmd = "(echo \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
sanitize String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\")"
String
_ <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd
() -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where sanitize :: Char -> String
sanitize '"' = "\"\""
sanitize c :: Char
c = [Char
c]
exit :: (MonadIO m, MonadQuery m) => m ()
exit :: m ()
exit = do Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True "(exit)"
(QueryState -> QueryState) -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(QueryState -> QueryState) -> m ()
modifyQueryState ((QueryState -> QueryState) -> m ())
-> (QueryState -> QueryState) -> m ()
forall a b. (a -> b) -> a -> b
$ \s :: QueryState
s -> QueryState
s{queryAssertionStackDepth :: Int
queryAssertionStackDepth = 0}
getUnsatCore :: (MonadIO m, MonadQuery m) => m [String]
getUnsatCore :: m [String]
getUnsatCore = do
let cmd :: String
cmd = "(get-unsat-core)"
bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected "getUnsatCore" String
cmd "an unsat-core response"
(Maybe [String] -> String -> Maybe [String] -> m a)
-> Maybe [String] -> String -> Maybe [String] -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
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."
]
String
r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd
String
-> (String -> Maybe [String] -> m [String])
-> (SExpr -> m [String])
-> m [String]
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m [String]
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m [String]) -> m [String])
-> (SExpr -> m [String]) -> m [String]
forall a b. (a -> b) -> a -> b
$ \case
EApp es :: [SExpr]
es | Just xs :: [String]
xs <- (SExpr -> Maybe String) -> [SExpr] -> Maybe [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SExpr -> Maybe String
fromECon [SExpr]
es -> [String] -> m [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> m [String]) -> [String] -> m [String]
forall a b. (a -> b) -> a -> b
$ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
unBar [String]
xs
_ -> String -> Maybe [String] -> m [String]
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
getUnsatCoreIfRequested :: (MonadIO m, MonadQuery m) => m (Maybe [String])
getUnsatCoreIfRequested :: m (Maybe [String])
getUnsatCoreIfRequested = do
SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
if [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool
b | ProduceUnsatCores b :: Bool
b <- SMTConfig -> [SMTOption]
solverSetOptions SMTConfig
cfg]
then [String] -> Maybe [String]
forall a. a -> Maybe a
Just ([String] -> Maybe [String]) -> m [String] -> m (Maybe [String])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m [String]
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m [String]
getUnsatCore
else Maybe [String] -> m (Maybe [String])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [String]
forall a. Maybe a
Nothing
getProof :: (MonadIO m, MonadQuery m) => m String
getProof :: m String
getProof = do
let cmd :: String
cmd = "(get-proof)"
bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected "getProof" String
cmd "a get-proof response"
(Maybe [String] -> String -> Maybe [String] -> m a)
-> Maybe [String] -> String -> Maybe [String] -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
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."
]
String
r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd
String
-> (String -> Maybe [String] -> m String)
-> (SExpr -> m String)
-> m String
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m String
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m String) -> m String)
-> (SExpr -> m String) -> m String
forall a b. (a -> b) -> a -> b
$ \_ -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return String
r
getInterpolantMathSAT :: (MonadIO m, MonadQuery m) => [String] -> m String
getInterpolantMathSAT :: [String] -> m String
getInterpolantMathSAT fs :: [String]
fs
| [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
fs
= String -> m String
forall a. HasCallStack => String -> a
error "SBV.getInterpolantMathSAT requires at least one marked constraint, received none!"
| Bool
True
= do let bar :: String -> String
bar s :: String
s = '|' Char -> String -> String
forall a. a -> [a] -> [a]
: String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "|"
cmd :: String
cmd = "(get-interpolant (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
bar [String]
fs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))"
bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected "getInterpolant" String
cmd "a get-interpolant response"
(Maybe [String] -> String -> Maybe [String] -> m a)
-> Maybe [String] -> String -> Maybe [String] -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
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."
]
String
r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd
String
-> (String -> Maybe [String] -> m String)
-> (SExpr -> m String)
-> m String
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m String
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m String) -> m String)
-> (SExpr -> m String) -> m String
forall a b. (a -> b) -> a -> b
$ \e :: SExpr
e -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ Bool -> SExpr -> String
serialize Bool
False SExpr
e
getInterpolantZ3 :: (MonadIO m, MonadQuery m) => [SBool] -> m String
getInterpolantZ3 :: [SBool] -> m String
getInterpolantZ3 fs :: [SBool]
fs
| [SBool] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBool]
fs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< 2
= String -> m String
forall a. HasCallStack => String -> a
error (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ "SBV.getInterpolantZ3 requires at least two booleans, received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SBool] -> String
forall a. Show a => a -> String
show [SBool]
fs
| Bool
True
= do [SV]
ss <- let fAll :: [SBV a] -> [SV] -> m [SV]
fAll [] sofar :: [SV]
sofar = [SV] -> m [SV]
forall (m :: * -> *) a. Monad m => a -> m a
return ([SV] -> m [SV]) -> [SV] -> m [SV]
forall a b. (a -> b) -> a -> b
$ [SV] -> [SV]
forall a. [a] -> [a]
reverse [SV]
sofar
fAll (b :: SBV a
b:bs :: [SBV a]
bs) sofar :: [SV]
sofar = do SV
sv <- (State -> IO SV) -> m SV
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext (State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
`sbvToSV` SBV a
b)
[SBV a] -> [SV] -> m [SV]
fAll [SBV a]
bs (SV
sv SV -> [SV] -> [SV]
forall a. a -> [a] -> [a]
: [SV]
sofar)
in [SBool] -> [SV] -> m [SV]
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
[SBV a] -> [SV] -> m [SV]
fAll [SBool]
fs []
let cmd :: String
cmd = "(get-interpolant " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
forall a. Show a => a -> String
show [SV]
ss) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected "getInterpolant" String
cmd "a get-interpolant response" Maybe [String]
forall a. Maybe a
Nothing
String
r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd
String
-> (String -> Maybe [String] -> m String)
-> (SExpr -> m String)
-> m String
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m String
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m String) -> m String)
-> (SExpr -> m String) -> m String
forall a b. (a -> b) -> a -> b
$ \e :: SExpr
e -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ Bool -> SExpr -> String
serialize Bool
False SExpr
e
getAssertions :: (MonadIO m, MonadQuery m) => m [String]
getAssertions :: m [String]
getAssertions = do
let cmd :: String
cmd = "(get-assertions)"
bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected "getAssertions" String
cmd "a get-assertions response"
(Maybe [String] -> String -> Maybe [String] -> m a)
-> Maybe [String] -> String -> Maybe [String] -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just [ "Make sure you use:"
, ""
, " setOption $ ProduceAssertions True"
, ""
, "to make sure the solver is ready for producing assertions."
]
render :: SExpr -> String
render = Bool -> SExpr -> String
serialize Bool
False
String
r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd
String
-> (String -> Maybe [String] -> m [String])
-> (SExpr -> m [String])
-> m [String]
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m [String]
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m [String]) -> m [String])
-> (SExpr -> m [String]) -> m [String]
forall a b. (a -> b) -> a -> b
$ \pe :: SExpr
pe -> case SExpr
pe of
EApp xs :: [SExpr]
xs -> [String] -> m [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> m [String]) -> [String] -> m [String]
forall a b. (a -> b) -> a -> b
$ (SExpr -> String) -> [SExpr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SExpr -> String
render [SExpr]
xs
_ -> [String] -> m [String]
forall (m :: * -> *) a. Monad m => a -> m a
return [SExpr -> String
render SExpr
pe]
getAssignment :: (MonadIO m, MonadQuery m) => m [(String, Bool)]
getAssignment :: m [(String, Bool)]
getAssignment = do
let cmd :: String
cmd = "(get-assignment)"
bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected "getAssignment" String
cmd "a get-assignment response"
(Maybe [String] -> String -> Maybe [String] -> m a)
-> Maybe [String] -> String -> Maybe [String] -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
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."
]
grab :: SExpr -> Maybe (String, Bool)
grab (EApp [ECon s :: String
s, ENum (0, _)]) = (String, Bool) -> Maybe (String, Bool)
forall a. a -> Maybe a
Just (String -> String
unQuote String
s, Bool
False)
grab (EApp [ECon s :: String
s, ENum (1, _)]) = (String, Bool) -> Maybe (String, Bool)
forall a. a -> Maybe a
Just (String -> String
unQuote String
s, Bool
True)
grab _ = Maybe (String, Bool)
forall a. Maybe a
Nothing
String
r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd
String
-> (String -> Maybe [String] -> m [(String, Bool)])
-> (SExpr -> m [(String, Bool)])
-> m [(String, Bool)]
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m [(String, Bool)]
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m [(String, Bool)]) -> m [(String, Bool)])
-> (SExpr -> m [(String, Bool)]) -> m [(String, Bool)]
forall a b. (a -> b) -> a -> b
$ \case EApp ps :: [SExpr]
ps | Just vs :: [(String, Bool)]
vs <- (SExpr -> Maybe (String, Bool))
-> [SExpr] -> Maybe [(String, Bool)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SExpr -> Maybe (String, Bool)
grab [SExpr]
ps -> [(String, Bool)] -> m [(String, Bool)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(String, Bool)]
vs
_ -> String -> Maybe [String] -> m [(String, Bool)]
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
infix 1 |->
(|->) :: SymVal a => SBV a -> a -> Assignment
SBV a :: SVal
a |-> :: SBV a -> a -> Assignment
|-> v :: a
v = case a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
v of
SBV (SVal _ (Left cv :: CV
cv)) -> SVal -> CV -> Assignment
Assign SVal
a CV
cv
r :: SBV a
r -> String -> Assignment
forall a. HasCallStack => String -> a
error (String -> Assignment) -> String -> Assignment
forall a b. (a -> b) -> a -> b
$ "Data.SBV: Impossible happened in |->: Cannot construct a CV with literal: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBV a -> String
forall a. Show a => a -> String
show SBV a
r
mkSMTResult :: (MonadIO m, MonadQuery m) => [Assignment] -> m SMTResult
mkSMTResult :: [Assignment] -> m SMTResult
mkSMTResult asgns :: [Assignment]
asgns = do
QueryState{SMTConfig
queryConfig :: SMTConfig
queryConfig :: QueryState -> SMTConfig
queryConfig} <- m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState
[(Quantifier, NamedSymVar)]
inps <- m [(Quantifier, NamedSymVar)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(Quantifier, NamedSymVar)]
getQuantifiedInputs
let grabValues :: State -> IO [(String, CV)]
grabValues st :: State
st = do let extract :: Assignment -> IO (SV, CV)
extract (Assign s :: SVal
s n :: CV
n) = State -> SBV Any -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st (SVal -> SBV Any
forall a. SVal -> SBV a
SBV SVal
s) IO SV -> (SV -> IO (SV, CV)) -> IO (SV, CV)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \sv :: SV
sv -> (SV, CV) -> IO (SV, CV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SV
sv, CV
n)
[(SV, CV)]
modelAssignment <- (Assignment -> IO (SV, CV)) -> [Assignment] -> IO [(SV, CV)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Assignment -> IO (SV, CV)
extract [Assignment]
asgns
let userSS :: [SV]
userSS = ((SV, CV) -> SV) -> [(SV, CV)] -> [SV]
forall a b. (a -> b) -> [a] -> [b]
map (SV, CV) -> SV
forall a b. (a, b) -> a
fst [(SV, CV)]
modelAssignment
missing, extra, dup :: [String]
missing :: [String]
missing = [String
n | (EX, (s :: SV
s, n :: String
n)) <- [(Quantifier, NamedSymVar)]
inps, SV
s SV -> [SV] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [SV]
userSS]
extra :: [String]
extra = [SV -> String
forall a. Show a => a -> String
show SV
s | SV
s <- [SV]
userSS, SV
s SV -> [SV] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` ((Quantifier, NamedSymVar) -> SV)
-> [(Quantifier, NamedSymVar)] -> [SV]
forall a b. (a -> b) -> [a] -> [b]
map (NamedSymVar -> SV
forall a b. (a, b) -> a
fst (NamedSymVar -> SV)
-> ((Quantifier, NamedSymVar) -> NamedSymVar)
-> (Quantifier, NamedSymVar)
-> SV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Quantifier, NamedSymVar) -> NamedSymVar
forall a b. (a, b) -> b
snd) [(Quantifier, NamedSymVar)]
inps]
dup :: [String]
dup = let walk :: [a] -> [String]
walk [] = []
walk (n :: a
n:ns :: [a]
ns)
| a
n a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
ns = a -> String
forall a. Show a => a -> String
show a
n String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [a] -> [String]
walk ((a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
n) [a]
ns)
| Bool
True = [a] -> [String]
walk [a]
ns
in [SV] -> [String]
forall a. (Eq a, Show a) => [a] -> [String]
walk [SV]
userSS
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String]
missing [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
extra [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
dup)) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
let misTag :: String
misTag = "*** Missing inputs"
dupTag :: String
dupTag = "*** Duplicate bindings"
extTag :: String
extTag = "*** Extra bindings"
maxLen :: Int
maxLen = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ 0
Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
misTag | Bool -> Bool
not ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
missing)]
[Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
extTag | Bool -> Bool
not ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
extra)]
[Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
dupTag | Bool -> Bool
not ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
dup)]
align :: String -> String
align s :: String
s = String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
maxLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s) ' ' String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": "
String -> IO ()
forall a. HasCallStack => String -> a
error (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [""
, "*** Data.SBV: Query model construction has a faulty assignment."
, "***"
]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String -> String
align String
misTag String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " [String]
missing | Bool -> Bool
not ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
missing)]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String -> String
align String
extTag String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " [String]
extra | Bool -> Bool
not ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
extra) ]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String -> String
align String
dupTag String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " [String]
dup | Bool -> Bool
not ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
dup) ]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ "***"
, "*** Data.SBV: Check your query result construction!"
]
let findName :: SV -> String
findName s :: SV
s = case [String
nm | (_, (i :: SV
i, nm :: String
nm)) <- [(Quantifier, NamedSymVar)]
inps, SV
s SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
i] of
[nm :: String
nm] -> String
nm
[] -> String -> String
forall a. HasCallStack => String -> a
error "*** Data.SBV: Impossible happened: Cannot find " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " in the input list"
nms :: [String]
nms -> String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ ""
, "*** Data.SBV: Impossible happened: Multiple matches for: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
s
, "*** Candidates: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
nms
]
[(String, CV)] -> IO [(String, CV)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(SV -> String
findName SV
s, CV
n) | (s :: SV
s, n :: CV
n) <- [(SV, CV)]
modelAssignment]
[(String, CV)]
assocs <- (State -> IO [(String, CV)]) -> m [(String, CV)]
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext State -> IO [(String, CV)]
grabValues
let m :: SMTModel
m = SMTModel :: [(String, GeneralizedCV)]
-> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
-> [(String, CV)]
-> [(String, (SBVType, ([([CV], CV)], CV)))]
-> SMTModel
SMTModel { modelObjectives :: [(String, GeneralizedCV)]
modelObjectives = []
, modelBindings :: Maybe [((Quantifier, NamedSymVar), Maybe CV)]
modelBindings = Maybe [((Quantifier, NamedSymVar), Maybe CV)]
forall a. Maybe a
Nothing
, modelAssocs :: [(String, CV)]
modelAssocs = [(String, CV)]
assocs
, modelUIFuns :: [(String, (SBVType, ([([CV], CV)], CV)))]
modelUIFuns = []
}
SMTResult -> m SMTResult
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTResult -> m SMTResult) -> SMTResult -> m SMTResult
forall a b. (a -> b) -> a -> b
$ SMTConfig -> SMTModel -> SMTResult
Satisfiable SMTConfig
queryConfig SMTModel
m
{-# ANN getModelAtIndex ("HLint: ignore Use forM_" :: String) #-}