{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Provers.Prover (
SMTSolver(..), SMTConfig(..), Predicate
, MProvable(..), Provable, proveWithAll, proveWithAny , satWithAll, satWithAny
, generateSMTBenchmark
, Goal
, ThmResult(..), SatResult(..), AllSatResult(..), SafeResult(..), OptimizeResult(..), SMTResult(..)
, SExecutable(..), isSafe
, runSMT, runSMTWith
, SatModel(..), Modelable(..), displayModels, extractModels
, getModelDictionaries, getModelValues, getModelUninterpretedValues
, boolector, cvc4, yices, z3, mathSAT, abc, defaultSMTCfg
) where
import Control.Monad (when, unless)
import Control.Monad.IO.Class (MonadIO, liftIO)
import Control.DeepSeq (rnf, NFData(..))
import Control.Concurrent.Async (async, waitAny, asyncThreadId, Async)
import Control.Exception (finally, throwTo, AsyncException(ThreadKilled))
import System.IO.Unsafe (unsafeInterleaveIO)
import System.Directory (getCurrentDirectory)
import Data.Time (getZonedTime, NominalDiffTime, UTCTime, getCurrentTime, diffUTCTime)
import Data.List (intercalate, isPrefixOf, nub)
import Data.Maybe (mapMaybe, listToMaybe)
import qualified Data.Map.Strict as M
import qualified Data.Foldable as S (toList)
import Data.SBV.Core.Data
import Data.SBV.Core.Symbolic
import Data.SBV.SMT.SMT
import Data.SBV.SMT.Utils (debug, alignPlain)
import Data.SBV.Utils.ExtractIO
import Data.SBV.Utils.TDiff
import qualified Data.SBV.Trans.Control as Control
import qualified Data.SBV.Control.Query as Control
import qualified Data.SBV.Control.Utils as Control
import GHC.Stack
import qualified Data.SBV.Provers.Boolector as Boolector
import qualified Data.SBV.Provers.CVC4 as CVC4
import qualified Data.SBV.Provers.Yices as Yices
import qualified Data.SBV.Provers.Z3 as Z3
import qualified Data.SBV.Provers.MathSAT as MathSAT
import qualified Data.SBV.Provers.ABC as ABC
mkConfig :: SMTSolver -> SMTLibVersion -> [Control.SMTOption] -> SMTConfig
mkConfig :: SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig s :: SMTSolver
s smtVersion :: SMTLibVersion
smtVersion startOpts :: [SMTOption]
startOpts = SMTConfig :: Bool
-> Timing
-> Int
-> Int
-> String
-> Maybe Int
-> Bool
-> Bool
-> (String -> Bool)
-> Bool
-> Bool
-> Maybe String
-> SMTLibVersion
-> SMTSolver
-> Bool
-> RoundingMode
-> [SMTOption]
-> Bool
-> Maybe String
-> SMTConfig
SMTConfig { verbose :: Bool
verbose = Bool
False
, timing :: Timing
timing = Timing
NoTiming
, printBase :: Int
printBase = 10
, printRealPrec :: Int
printRealPrec = 16
, transcript :: Maybe String
transcript = Maybe String
forall a. Maybe a
Nothing
, solver :: SMTSolver
solver = SMTSolver
s
, smtLibVersion :: SMTLibVersion
smtLibVersion = SMTLibVersion
smtVersion
, satCmd :: String
satCmd = "(check-sat)"
, satTrackUFs :: Bool
satTrackUFs = Bool
True
, allSatMaxModelCount :: Maybe Int
allSatMaxModelCount = Maybe Int
forall a. Maybe a
Nothing
, allSatPrintAlong :: Bool
allSatPrintAlong = Bool
False
, isNonModelVar :: String -> Bool
isNonModelVar = Bool -> String -> Bool
forall a b. a -> b -> a
const Bool
False
, validateModel :: Bool
validateModel = Bool
False
, optimizeValidateConstraints :: Bool
optimizeValidateConstraints = Bool
False
, allowQuantifiedQueries :: Bool
allowQuantifiedQueries = Bool
False
, roundingMode :: RoundingMode
roundingMode = RoundingMode
RoundNearestTiesToEven
, solverSetOptions :: [SMTOption]
solverSetOptions = [SMTOption]
startOpts
, ignoreExitCode :: Bool
ignoreExitCode = Bool
False
, redirectVerbose :: Maybe String
redirectVerbose = Maybe String
forall a. Maybe a
Nothing
}
allOnStdOut :: Control.SMTOption
allOnStdOut :: SMTOption
allOnStdOut = String -> [String] -> SMTOption
Control.OptionKeyword ":diagnostic-output-channel" [String -> String
forall a. Show a => a -> String
show "stdout"]
boolector :: SMTConfig
boolector :: SMTConfig
boolector = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
Boolector.boolector SMTLibVersion
SMTLib2 []
cvc4 :: SMTConfig
cvc4 :: SMTConfig
cvc4 = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
CVC4.cvc4 SMTLibVersion
SMTLib2 [SMTOption
allOnStdOut]
yices :: SMTConfig
yices :: SMTConfig
yices = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
Yices.yices SMTLibVersion
SMTLib2 []
z3 :: SMTConfig
z3 :: SMTConfig
z3 = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
Z3.z3 SMTLibVersion
SMTLib2 [ String -> [String] -> SMTOption
Control.OptionKeyword ":smtlib2_compliant" ["true"]
, SMTOption
allOnStdOut
]
mathSAT :: SMTConfig
mathSAT :: SMTConfig
mathSAT = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
MathSAT.mathSAT SMTLibVersion
SMTLib2 [SMTOption
allOnStdOut]
abc :: SMTConfig
abc :: SMTConfig
abc = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
ABC.abc SMTLibVersion
SMTLib2 [SMTOption
allOnStdOut]
defaultSMTCfg :: SMTConfig
defaultSMTCfg :: SMTConfig
defaultSMTCfg = SMTConfig
z3
type Predicate = Symbolic SBool
type Goal = Symbolic ()
class ExtractIO m => MProvable m a where
forAll_ :: a -> SymbolicT m SBool
forAll :: [String] -> a -> SymbolicT m SBool
forSome_ :: a -> SymbolicT m SBool
forSome :: [String] -> a -> SymbolicT m SBool
prove :: a -> m ThmResult
prove = SMTConfig -> a -> m ThmResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m ThmResult
proveWith SMTConfig
defaultSMTCfg
proveWith :: SMTConfig -> a -> m ThmResult
proveWith cfg :: SMTConfig
cfg a :: a
a = do SMTResult
r <- Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
False (QueryT m ()
forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QueryT m SMTResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
Control.getSMTResult) SMTConfig
cfg a
a
SMTResult -> ThmResult
ThmResult (SMTResult -> ThmResult) -> m SMTResult -> m ThmResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> if SMTConfig -> Bool
validationRequested SMTConfig
cfg
then Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
forall (m :: * -> *) a.
MProvable m a =>
Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
validate Bool
False SMTConfig
cfg a
a SMTResult
r
else SMTResult -> m SMTResult
forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
r
sat :: a -> m SatResult
sat = SMTConfig -> a -> m SatResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m SatResult
satWith SMTConfig
defaultSMTCfg
satWith :: SMTConfig -> a -> m SatResult
satWith cfg :: SMTConfig
cfg a :: a
a = do SMTResult
r <- Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
True (QueryT m ()
forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QueryT m SMTResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
Control.getSMTResult) SMTConfig
cfg a
a
SMTResult -> SatResult
SatResult (SMTResult -> SatResult) -> m SMTResult -> m SatResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> if SMTConfig -> Bool
validationRequested SMTConfig
cfg
then Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
forall (m :: * -> *) a.
MProvable m a =>
Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
validate Bool
True SMTConfig
cfg a
a SMTResult
r
else SMTResult -> m SMTResult
forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
r
allSat :: a -> m AllSatResult
allSat = SMTConfig -> a -> m AllSatResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m AllSatResult
allSatWith SMTConfig
defaultSMTCfg
allSatWith :: SMTConfig -> a -> m AllSatResult
allSatWith cfg :: SMTConfig
cfg a :: a
a = do f :: (Bool, Bool, Bool, [SMTResult])
f@(mm :: Bool
mm, pe :: Bool
pe, un :: Bool
un, rs :: [SMTResult]
rs) <- Bool
-> QueryT m (Bool, Bool, Bool, [SMTResult])
-> SMTConfig
-> a
-> m (Bool, Bool, Bool, [SMTResult])
forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
True (QueryT m ()
forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations QueryT m ()
-> QueryT m (Bool, Bool, Bool, [SMTResult])
-> QueryT m (Bool, Bool, Bool, [SMTResult])
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QueryT m (Bool, Bool, Bool, [SMTResult])
forall (m :: * -> *).
(MonadIO m, MonadQuery m, SolverContext m) =>
m (Bool, Bool, Bool, [SMTResult])
Control.getAllSatResult) SMTConfig
cfg a
a
(Bool, Bool, Bool, [SMTResult]) -> AllSatResult
AllSatResult ((Bool, Bool, Bool, [SMTResult]) -> AllSatResult)
-> m (Bool, Bool, Bool, [SMTResult]) -> m AllSatResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> if SMTConfig -> Bool
validationRequested SMTConfig
cfg
then do [SMTResult]
rs' <- (SMTResult -> m SMTResult) -> [SMTResult] -> m [SMTResult]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
forall (m :: * -> *) a.
MProvable m a =>
Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
validate Bool
True SMTConfig
cfg a
a) [SMTResult]
rs
(Bool, Bool, Bool, [SMTResult])
-> m (Bool, Bool, Bool, [SMTResult])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
mm, Bool
pe, Bool
un, [SMTResult]
rs')
else (Bool, Bool, Bool, [SMTResult])
-> m (Bool, Bool, Bool, [SMTResult])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool, Bool, Bool, [SMTResult])
f
optimize :: OptimizeStyle -> a -> m OptimizeResult
optimize = SMTConfig -> OptimizeStyle -> a -> m OptimizeResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> OptimizeStyle -> a -> m OptimizeResult
optimizeWith SMTConfig
defaultSMTCfg
optimizeWith :: SMTConfig -> OptimizeStyle -> a -> m OptimizeResult
optimizeWith config :: SMTConfig
config style :: OptimizeStyle
style optGoal :: a
optGoal = do
OptimizeResult
res <- Bool
-> QueryT m OptimizeResult -> SMTConfig -> a -> m OptimizeResult
forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
True QueryT m OptimizeResult
opt SMTConfig
config a
optGoal
if Bool -> Bool
not (SMTConfig -> Bool
optimizeValidateConstraints SMTConfig
config)
then OptimizeResult -> m OptimizeResult
forall (m :: * -> *) a. Monad m => a -> m a
return OptimizeResult
res
else let v :: SMTResult -> m SMTResult
v :: SMTResult -> m SMTResult
v = Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
forall (m :: * -> *) a.
MProvable m a =>
Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
validate Bool
True SMTConfig
config a
optGoal
in case OptimizeResult
res of
LexicographicResult m :: SMTResult
m -> SMTResult -> OptimizeResult
LexicographicResult (SMTResult -> OptimizeResult) -> m SMTResult -> m OptimizeResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SMTResult -> m SMTResult
v SMTResult
m
IndependentResult xs :: [(String, SMTResult)]
xs -> let w :: [(a, SMTResult)] -> [(a, SMTResult)] -> m [(a, SMTResult)]
w [] sofar :: [(a, SMTResult)]
sofar = [(a, SMTResult)] -> m [(a, SMTResult)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(a, SMTResult)] -> [(a, SMTResult)]
forall a. [a] -> [a]
reverse [(a, SMTResult)]
sofar)
w ((n :: a
n, m :: SMTResult
m):rest :: [(a, SMTResult)]
rest) sofar :: [(a, SMTResult)]
sofar = SMTResult -> m SMTResult
v SMTResult
m m SMTResult
-> (SMTResult -> m [(a, SMTResult)]) -> m [(a, SMTResult)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \m' :: SMTResult
m' -> [(a, SMTResult)] -> [(a, SMTResult)] -> m [(a, SMTResult)]
w [(a, SMTResult)]
rest ((a
n, SMTResult
m') (a, SMTResult) -> [(a, SMTResult)] -> [(a, SMTResult)]
forall a. a -> [a] -> [a]
: [(a, SMTResult)]
sofar)
in [(String, SMTResult)] -> OptimizeResult
IndependentResult ([(String, SMTResult)] -> OptimizeResult)
-> m [(String, SMTResult)] -> m OptimizeResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(String, SMTResult)]
-> [(String, SMTResult)] -> m [(String, SMTResult)]
forall a.
[(a, SMTResult)] -> [(a, SMTResult)] -> m [(a, SMTResult)]
w [(String, SMTResult)]
xs []
ParetoResult (b :: Bool
b, rs :: [SMTResult]
rs) -> (Bool, [SMTResult]) -> OptimizeResult
ParetoResult ((Bool, [SMTResult]) -> OptimizeResult)
-> ([SMTResult] -> (Bool, [SMTResult]))
-> [SMTResult]
-> OptimizeResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool
b, ) ([SMTResult] -> OptimizeResult)
-> m [SMTResult] -> m OptimizeResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SMTResult -> m SMTResult) -> [SMTResult] -> m [SMTResult]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SMTResult -> m SMTResult
v [SMTResult]
rs
where opt :: QueryT m OptimizeResult
opt = do [Objective (SV, SV)]
objectives <- QueryT m [Objective (SV, SV)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [Objective (SV, SV)]
Control.getObjectives
[(Quantifier, NamedSymVar)]
qinps <- QueryT m [(Quantifier, NamedSymVar)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(Quantifier, NamedSymVar)]
Control.getQuantifiedInputs
SBVPgm
spgm <- QueryT m SBVPgm
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SBVPgm
Control.getSBVPgm
Bool -> QueryT m () -> QueryT m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Objective (SV, SV)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Objective (SV, SV)]
objectives) (QueryT m () -> QueryT m ()) -> QueryT m () -> QueryT m ()
forall a b. (a -> b) -> a -> b
$
String -> QueryT m ()
forall a. HasCallStack => String -> a
error (String -> QueryT m ()) -> String -> QueryT m ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ ""
, "*** Data.SBV: Unsupported call to optimize when no objectives are present."
, "*** Use \"sat\" for plain satisfaction"
]
Bool -> QueryT m () -> QueryT m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (SolverCapabilities -> Bool
supportsOptimization (SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
config))) (QueryT m () -> QueryT m ()) -> QueryT m () -> QueryT m ()
forall a b. (a -> b) -> a -> b
$
String -> QueryT m ()
forall a. HasCallStack => String -> a
error (String -> QueryT m ()) -> String -> QueryT m ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ ""
, "*** Data.SBV: The backend solver " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Solver -> String
forall a. Show a => a -> String
show (SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
config)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "does not support optimization goals."
, "*** Please use a solver that has support, such as z3"
]
Bool -> QueryT m () -> QueryT m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SMTConfig -> Bool
validateModel SMTConfig
config Bool -> Bool -> Bool
&& Bool -> Bool
not (SMTConfig -> Bool
optimizeValidateConstraints SMTConfig
config)) (QueryT m () -> QueryT m ()) -> QueryT m () -> QueryT m ()
forall a b. (a -> b) -> a -> b
$
String -> QueryT m ()
forall a. HasCallStack => String -> a
error (String -> QueryT m ()) -> String -> QueryT m ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ ""
, "*** Data.SBV: Model validation is not supported in optimization calls."
, "***"
, "*** Instead, use `cfg{optimizeValidateConstraints = True}`"
, "***"
, "*** which checks that the results satisfy the constraints but does"
, "*** NOT ensure that they are optimal."
]
let universals :: [NamedSymVar]
universals = [NamedSymVar
s | (ALL, s :: NamedSymVar
s) <- [(Quantifier, NamedSymVar)]
qinps]
firstUniversal :: NodeId
firstUniversal
| [NamedSymVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedSymVar]
universals = String -> NodeId
forall a. HasCallStack => String -> a
error "Data.SBV: Impossible happened! Universal optimization with no universals!"
| Bool
True = [NodeId] -> NodeId
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ((NamedSymVar -> NodeId) -> [NamedSymVar] -> [NodeId]
forall a b. (a -> b) -> [a] -> [b]
map (SV -> NodeId
nodeId (SV -> NodeId) -> (NamedSymVar -> SV) -> NamedSymVar -> NodeId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedSymVar -> SV
forall a b. (a, b) -> a
fst) [NamedSymVar]
universals)
nodeId :: SV -> NodeId
nodeId (SV _ n :: NodeId
n) = NodeId
n
mappings :: M.Map SV SBVExpr
mappings :: Map SV SBVExpr
mappings = [(SV, SBVExpr)] -> Map SV SBVExpr
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (Seq (SV, SBVExpr) -> [(SV, SBVExpr)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
S.toList (SBVPgm -> Seq (SV, SBVExpr)
pgmAssignments SBVPgm
spgm))
chaseUniversal :: SV -> [String]
chaseUniversal entry :: SV
entry = (NamedSymVar -> String) -> [NamedSymVar] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map NamedSymVar -> String
forall a b. (a, b) -> b
snd ([NamedSymVar] -> [String]) -> [NamedSymVar] -> [String]
forall a b. (a -> b) -> a -> b
$ SV -> [NamedSymVar] -> [NamedSymVar]
go SV
entry []
where go :: SV -> [NamedSymVar] -> [NamedSymVar]
go x :: SV
x sofar :: [NamedSymVar]
sofar
| NodeId
nx NodeId -> NodeId -> Bool
forall a. Ord a => a -> a -> Bool
>= NodeId
firstUniversal
= [NamedSymVar] -> [NamedSymVar]
forall a. Eq a => [a] -> [a]
nub ([NamedSymVar] -> [NamedSymVar]) -> [NamedSymVar] -> [NamedSymVar]
forall a b. (a -> b) -> a -> b
$ [NamedSymVar
unm | unm :: NamedSymVar
unm@(u :: SV
u, _) <- [NamedSymVar]
universals, NodeId
nx NodeId -> NodeId -> Bool
forall a. Ord a => a -> a -> Bool
>= SV -> NodeId
nodeId SV
u] [NamedSymVar] -> [NamedSymVar] -> [NamedSymVar]
forall a. [a] -> [a] -> [a]
++ [NamedSymVar]
sofar
| Bool
True
= let oVars :: Op -> [SV]
oVars (LkUp _ a :: SV
a b :: SV
b) = [SV
a, SV
b]
oVars (IEEEFP (FP_Cast _ _ o :: SV
o)) = [SV
o]
oVars _ = []
vars :: [SV]
vars = case SV
x SV -> Map SV SBVExpr -> Maybe SBVExpr
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map SV SBVExpr
mappings of
Nothing -> []
Just (SBVApp o :: Op
o ss :: [SV]
ss) -> [SV] -> [SV]
forall a. Eq a => [a] -> [a]
nub (Op -> [SV]
oVars Op
o [SV] -> [SV] -> [SV]
forall a. [a] -> [a] -> [a]
++ [SV]
ss)
in (SV -> [NamedSymVar] -> [NamedSymVar])
-> [NamedSymVar] -> [SV] -> [NamedSymVar]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SV -> [NamedSymVar] -> [NamedSymVar]
go [NamedSymVar]
sofar [SV]
vars
where nx :: NodeId
nx = SV -> NodeId
nodeId SV
x
let needsUniversalOpt :: [(String, [String])]
needsUniversalOpt = let tag :: a -> [a] -> Maybe (a, [a])
tag _ [] = Maybe (a, [a])
forall a. Maybe a
Nothing
tag nm :: a
nm xs :: [a]
xs = (a, [a]) -> Maybe (a, [a])
forall a. a -> Maybe a
Just (a
nm, [a]
xs)
needsUniversal :: Objective (SV, b) -> Maybe (String, [String])
needsUniversal (Maximize nm :: String
nm (x :: SV
x, _)) = String -> [String] -> Maybe (String, [String])
forall a a. a -> [a] -> Maybe (a, [a])
tag String
nm (SV -> [String]
chaseUniversal SV
x)
needsUniversal (Minimize nm :: String
nm (x :: SV
x, _)) = String -> [String] -> Maybe (String, [String])
forall a a. a -> [a] -> Maybe (a, [a])
tag String
nm (SV -> [String]
chaseUniversal SV
x)
needsUniversal (AssertWithPenalty nm :: String
nm (x :: SV
x, _) _) = String -> [String] -> Maybe (String, [String])
forall a a. a -> [a] -> Maybe (a, [a])
tag String
nm (SV -> [String]
chaseUniversal SV
x)
in (Objective (SV, SV) -> Maybe (String, [String]))
-> [Objective (SV, SV)] -> [(String, [String])]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Objective (SV, SV) -> Maybe (String, [String])
forall b. Objective (SV, b) -> Maybe (String, [String])
needsUniversal [Objective (SV, SV)]
objectives
Bool -> QueryT m () -> QueryT m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([NamedSymVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedSymVar]
universals Bool -> Bool -> Bool
|| [(String, [String])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, [String])]
needsUniversalOpt) (QueryT m () -> QueryT m ()) -> QueryT m () -> QueryT m ()
forall a b. (a -> b) -> a -> b
$
let len :: Int
len = [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
nm | (nm :: String
nm, _) <- [(String, [String])]
needsUniversalOpt]
pad :: String -> String
pad n :: String
n = String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
n) ' '
in String -> QueryT m ()
forall a. HasCallStack => String -> a
error (String -> QueryT m ()) -> String -> QueryT m ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [ ""
, "*** Data.SBV: Problem needs optimization of metric in the scope of universally quantified variable(s):"
, "***"
]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ "*** " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
pad String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " [Depends on: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " [String]
xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ "]" | (s :: String
s, xs :: [String]
xs) <- [(String, [String])]
needsUniversalOpt ]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ "***"
, "*** Optimization is only meaningful with existentially quantified metrics."
]
let optimizerDirectives :: [String]
optimizerDirectives = (Objective (SV, SV) -> [String])
-> [Objective (SV, SV)] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Objective (SV, SV) -> [String]
forall a a. (Show a, Show a) => Objective (a, a) -> [String]
minmax [Objective (SV, SV)]
objectives [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ OptimizeStyle -> [String]
priority OptimizeStyle
style
where mkEq :: (a, a) -> String
mkEq (x :: a
x, y :: a
y) = "(assert (= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
x 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
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))"
minmax :: Objective (a, a) -> [String]
minmax (Minimize _ xy :: (a, a)
xy@(_, v :: a
v)) = [(a, a) -> String
forall a a. (Show a, Show a) => (a, a) -> String
mkEq (a, a)
xy, "(minimize " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"]
minmax (Maximize _ xy :: (a, a)
xy@(_, v :: a
v)) = [(a, a) -> String
forall a a. (Show a, Show a) => (a, a) -> String
mkEq (a, a)
xy, "(maximize " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"]
minmax (AssertWithPenalty nm :: String
nm xy :: (a, a)
xy@(_, v :: a
v) mbp :: Penalty
mbp) = [(a, a) -> String
forall a a. (Show a, Show a) => (a, a) -> String
mkEq (a, a)
xy, "(assert-soft " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ Penalty -> String
penalize Penalty
mbp String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"]
where penalize :: Penalty -> String
penalize DefaultPenalty = ""
penalize (Penalty w :: Rational
w mbGrp :: Maybe String
mbGrp)
| Rational
w Rational -> Rational -> Bool
forall a. Ord a => a -> a -> Bool
<= 0 = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ "SBV.AssertWithPenalty: Goal " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is assigned a non-positive penalty: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
shw
, "All soft goals must have > 0 penalties associated."
]
| Bool
True = " :weight " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
shw String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe "" String -> String
group Maybe String
mbGrp
where shw :: String
shw = Double -> String
forall a. Show a => a -> String
show (Rational -> Double
forall a. Fractional a => Rational -> a
fromRational Rational
w :: Double)
group :: String -> String
group g :: String
g = " :id " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
g
priority :: OptimizeStyle -> [String]
priority Lexicographic = []
priority Independent = ["(set-option :opt.priority box)"]
priority (Pareto _) = ["(set-option :opt.priority pareto)"]
(String -> QueryT m ()) -> [String] -> QueryT m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> String -> QueryT m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
Control.send Bool
True) [String]
optimizerDirectives
case OptimizeStyle
style of
Lexicographic -> SMTResult -> OptimizeResult
LexicographicResult (SMTResult -> OptimizeResult)
-> QueryT m SMTResult -> QueryT m OptimizeResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QueryT m SMTResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
Control.getLexicographicOptResults
Independent -> [(String, SMTResult)] -> OptimizeResult
IndependentResult ([(String, SMTResult)] -> OptimizeResult)
-> QueryT m [(String, SMTResult)] -> QueryT m OptimizeResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [String] -> QueryT m [(String, SMTResult)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
[String] -> m [(String, SMTResult)]
Control.getIndependentOptResults ((Objective (SV, SV) -> String) -> [Objective (SV, SV)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Objective (SV, SV) -> String
forall a. Objective a -> String
objectiveName [Objective (SV, SV)]
objectives)
Pareto mbN :: Maybe Int
mbN -> (Bool, [SMTResult]) -> OptimizeResult
ParetoResult ((Bool, [SMTResult]) -> OptimizeResult)
-> QueryT m (Bool, [SMTResult]) -> QueryT m OptimizeResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int -> QueryT m (Bool, [SMTResult])
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> m (Bool, [SMTResult])
Control.getParetoOptResults Maybe Int
mbN
isVacuous :: a -> m Bool
isVacuous = SMTConfig -> a -> m Bool
forall (m :: * -> *) a. MProvable m a => SMTConfig -> a -> m Bool
isVacuousWith SMTConfig
defaultSMTCfg
isVacuousWith :: SMTConfig -> a -> m Bool
isVacuousWith cfg :: SMTConfig
cfg a :: a
a =
(Bool, Result) -> Bool
forall a b. (a, b) -> a
fst ((Bool, Result) -> Bool) -> m (Bool, Result) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBVRunMode -> SymbolicT m Bool -> m (Bool, Result)
forall (m :: * -> *) a.
MonadIO m =>
SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
SMTMode QueryContext
QueryInternal IStage
ISetup Bool
True SMTConfig
cfg) (a -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ a
a SymbolicT m SBool -> SymbolicT m Bool -> SymbolicT m Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QueryContext -> QueryT m Bool -> SymbolicT m Bool
forall (m :: * -> *) a.
ExtractIO m =>
QueryContext -> QueryT m a -> SymbolicT m a
Control.executeQuery QueryContext
QueryInternal QueryT m Bool
check)
where
check :: QueryT m Bool
check :: QueryT m Bool
check = do CheckSatResult
cs <- QueryT m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
Control.checkSat
case CheckSatResult
cs of
Control.Unsat -> Bool -> QueryT m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
Control.Sat -> Bool -> QueryT m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
Control.Unk -> String -> QueryT m Bool
forall a. HasCallStack => String -> a
error "SBV: isVacuous: Solver returned unknown!"
isTheorem :: a -> m Bool
isTheorem = SMTConfig -> a -> m Bool
forall (m :: * -> *) a. MProvable m a => SMTConfig -> a -> m Bool
isTheoremWith SMTConfig
defaultSMTCfg
isTheoremWith :: SMTConfig -> a -> m Bool
isTheoremWith cfg :: SMTConfig
cfg p :: a
p = do ThmResult
r <- SMTConfig -> a -> m ThmResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m ThmResult
proveWith SMTConfig
cfg a
p
case ThmResult
r of
ThmResult Unsatisfiable{} -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
ThmResult Satisfiable{} -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
_ -> String -> m Bool
forall a. HasCallStack => String -> a
error (String -> m Bool) -> String -> m Bool
forall a b. (a -> b) -> a -> b
$ "SBV.isTheorem: Received:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ ThmResult -> String
forall a. Show a => a -> String
show ThmResult
r
isSatisfiable :: a -> m Bool
isSatisfiable = SMTConfig -> a -> m Bool
forall (m :: * -> *) a. MProvable m a => SMTConfig -> a -> m Bool
isSatisfiableWith SMTConfig
defaultSMTCfg
isSatisfiableWith :: SMTConfig -> a -> m Bool
isSatisfiableWith cfg :: SMTConfig
cfg p :: a
p = do SatResult
r <- SMTConfig -> a -> m SatResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m SatResult
satWith SMTConfig
cfg a
p
case SatResult
r of
SatResult Satisfiable{} -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
SatResult Unsatisfiable{} -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
_ -> String -> m Bool
forall a. HasCallStack => String -> a
error (String -> m Bool) -> String -> m Bool
forall a b. (a -> b) -> a -> b
$ "SBV.isSatisfiable: Received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SatResult -> String
forall a. Show a => a -> String
show SatResult
r
validate :: Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
validate isSAT :: Bool
isSAT cfg :: SMTConfig
cfg p :: a
p res :: SMTResult
res = case SMTResult
res of
Unsatisfiable{} -> SMTResult -> m SMTResult
forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
res
Satisfiable _ m :: SMTModel
m -> case SMTModel -> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
modelBindings SMTModel
m of
Nothing -> String -> m SMTResult
forall a. HasCallStack => String -> a
error "Data.SBV.validate: Impossible happaned; no bindings generated during model validation."
Just env :: [((Quantifier, NamedSymVar), Maybe CV)]
env -> [((Quantifier, NamedSymVar), Maybe CV)] -> m SMTResult
forall (m :: * -> *).
MProvable m a =>
[((Quantifier, NamedSymVar), Maybe CV)] -> m SMTResult
check [((Quantifier, NamedSymVar), Maybe CV)]
env
SatExtField{} -> 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 -> [String] -> Maybe SMTResult -> SMTResult
ProofError SMTConfig
cfg [ "The model requires an extension field value."
, "Cannot validate models with infinities/epsilons produced during optimization."
, ""
, "To turn validation off, use `cfg{optimizeValidateConstraints = False}`"
, ""
, "Unable to validate the produced model."
]
(SMTResult -> Maybe SMTResult
forall a. a -> Maybe a
Just SMTResult
res)
Unknown{} -> SMTResult -> m SMTResult
forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
res
ProofError{} -> SMTResult -> m SMTResult
forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
res
where check :: [((Quantifier, NamedSymVar), Maybe CV)] -> m SMTResult
check env :: [((Quantifier, NamedSymVar), Maybe CV)]
env = do let univs :: [String]
univs = [String
n | ((ALL, (_, n :: String
n)), _) <- [((Quantifier, NamedSymVar), Maybe CV)]
env]
envShown :: String
envShown = Bool -> Bool -> SMTConfig -> [(String, GeneralizedCV)] -> String
showModelDictionary Bool
True Bool
True SMTConfig
cfg [(String, GeneralizedCV)]
modelBinds
where modelBinds :: [(String, GeneralizedCV)]
modelBinds = [(String
n, Quantifier -> SV -> Maybe CV -> GeneralizedCV
forall a. HasKind a => Quantifier -> a -> Maybe CV -> GeneralizedCV
fake Quantifier
q SV
s Maybe CV
v) | ((q :: Quantifier
q, (s :: SV
s, n :: String
n)), v :: Maybe CV
v) <- [((Quantifier, NamedSymVar), Maybe CV)]
env]
fake :: Quantifier -> a -> Maybe CV -> GeneralizedCV
fake q :: Quantifier
q s :: a
s Nothing
| Quantifier
q Quantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
== Quantifier
ALL
= CV -> GeneralizedCV
RegularCV (CV -> GeneralizedCV) -> CV -> GeneralizedCV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (a -> Kind
forall a. HasKind a => a -> Kind
kindOf a
s) (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ (Maybe Int, String) -> CVal
CUserSort (Maybe Int
forall a. Maybe a
Nothing, "<universally quantified>")
| Bool
True
= CV -> GeneralizedCV
RegularCV (CV -> GeneralizedCV) -> CV -> GeneralizedCV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (a -> Kind
forall a. HasKind a => a -> Kind
kindOf a
s) (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ (Maybe Int, String) -> CVal
CUserSort (Maybe Int
forall a. Maybe a
Nothing, "<no binding found>")
fake _ _ (Just v :: CV
v) = CV -> GeneralizedCV
RegularCV CV
v
notify :: String -> m ()
notify s :: String
s
| Bool -> Bool
not (SMTConfig -> Bool
verbose SMTConfig
cfg) = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
| Bool
True = SMTConfig -> [String] -> m ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
debug SMTConfig
cfg ["[VALIDATE] " String -> String -> String
`alignPlain` String
s]
String -> m ()
forall (m :: * -> *). MonadIO m => String -> m ()
notify (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "Validating the model. " String -> String -> String
forall a. [a] -> [a] -> [a]
++ if [((Quantifier, NamedSymVar), Maybe CV)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((Quantifier, NamedSymVar), Maybe CV)]
env then "There are no assignments." else "Assignment:"
(String -> m ()) -> [String] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ String -> m ()
forall (m :: * -> *). MonadIO m => String -> m ()
notify [" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
l | String
l <- String -> [String]
lines String
envShown]
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
univs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
String -> m ()
forall (m :: * -> *). MonadIO m => String -> m ()
notify (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ "NB. The following variable(s) are universally quantified: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " [String]
univs
String -> m ()
forall (m :: * -> *). MonadIO m => String -> m ()
notify " We will assume that they are essentially zero for the purposes of validation."
String -> m ()
forall (m :: * -> *). MonadIO m => String -> m ()
notify " Note that this is a gross simplification of the model validation with universals!"
Result
result <- (SBool, Result) -> Result
forall a b. (a, b) -> b
snd ((SBool, Result) -> Result) -> m (SBool, Result) -> m Result
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBVRunMode -> SymbolicT m SBool -> m (SBool, Result)
forall (m :: * -> *) a.
MonadIO m =>
SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic (Maybe (Bool, [((Quantifier, NamedSymVar), Maybe CV)]) -> SBVRunMode
Concrete ((Bool, [((Quantifier, NamedSymVar), Maybe CV)])
-> Maybe (Bool, [((Quantifier, NamedSymVar), Maybe CV)])
forall a. a -> Maybe a
Just (Bool
isSAT, [((Quantifier, NamedSymVar), Maybe CV)]
env))) ((if Bool
isSAT then a -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ a
p else a -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ a
p) SymbolicT m SBool
-> (SBool -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SBool -> SymbolicT m SBool
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output)
let explain :: [String]
explain = [ ""
, "Assignment:" String -> String -> String
forall a. [a] -> [a] -> [a]
++ if [((Quantifier, NamedSymVar), Maybe CV)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((Quantifier, NamedSymVar), Maybe CV)]
env then " <none>" else ""
]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ "" | Bool -> Bool
not ([((Quantifier, NamedSymVar), Maybe CV)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((Quantifier, NamedSymVar), Maybe CV)]
env)]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
l | String
l <- String -> [String]
lines String
envShown]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ "" ]
wrap :: String -> [String] -> m SMTResult
wrap tag :: String
tag extras :: [String]
extras = 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 -> [String] -> Maybe SMTResult -> SMTResult
ProofError SMTConfig
cfg (String
tag String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
explain [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
extras) (SMTResult -> Maybe SMTResult
forall a. a -> Maybe a
Just SMTResult
res)
giveUp :: String -> m SMTResult
giveUp s :: String
s = String -> [String] -> m SMTResult
forall (m :: * -> *). Monad m => String -> [String] -> m SMTResult
wrap ("Data.SBV: Cannot validate the model: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s)
[ "SBV's model validator is incomplete, and cannot handle this particular case."
, "Please report this as a feature request or possibly a bug!"
]
badModel :: String -> m SMTResult
badModel s :: String
s = String -> [String] -> m SMTResult
forall (m :: * -> *). Monad m => String -> [String] -> m SMTResult
wrap ("Data.SBV: Model validation failure: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s)
[ "Backend solver returned a model that does not satisfy the constraints."
, "This could indicate a bug in the backend solver, or SBV itself. Please report."
]
notConcrete :: SV -> m SMTResult
notConcrete sv :: SV
sv = String -> [String] -> m SMTResult
forall (m :: * -> *). Monad m => String -> [String] -> m SMTResult
wrap ("Data.SBV: Cannot validate the model, since " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
sv String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is not concretely computable.")
( Maybe String -> [String]
perhaps (SV -> Maybe String
why SV
sv)
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ "SBV's model validator is incomplete, and cannot handle this particular case."
, "Please report this as a feature request or possibly a bug!"
]
)
where perhaps :: Maybe String -> [String]
perhaps Nothing = []
perhaps (Just x :: String
x) = [String
x, ""]
why :: SV -> Maybe String
why s :: SV
s = case SV
s SV -> [(SV, SBVExpr)] -> Maybe SBVExpr
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` Seq (SV, SBVExpr) -> [(SV, SBVExpr)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
S.toList (SBVPgm -> Seq (SV, SBVExpr)
pgmAssignments (Result -> SBVPgm
resAsgns Result
result)) of
Nothing -> Maybe String
forall a. Maybe a
Nothing
Just (SBVApp o :: Op
o as :: [SV]
as) -> case Op
o of
Uninterpreted v :: String
v -> String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ "The value depends on the uninterpreted constant " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "."
IEEEFP FP_FMA -> String -> Maybe String
forall a. a -> Maybe a
Just "Floating point FMA operation is not supported concretely."
IEEEFP _ -> String -> Maybe String
forall a. a -> Maybe a
Just "Not all floating point operations are supported concretely."
OverflowOp _ -> String -> Maybe String
forall a. a -> Maybe a
Just "Overflow-checking is not done concretely."
_ -> [String] -> Maybe String
forall a. [a] -> Maybe a
listToMaybe ([String] -> Maybe String) -> [String] -> Maybe String
forall a b. (a -> b) -> a -> b
$ (SV -> Maybe String) -> [SV] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe SV -> Maybe String
why [SV]
as
cstrs :: [(Bool, [(String, String)], SV)]
cstrs = Seq (Bool, [(String, String)], SV)
-> [(Bool, [(String, String)], SV)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
S.toList (Seq (Bool, [(String, String)], SV)
-> [(Bool, [(String, String)], SV)])
-> Seq (Bool, [(String, String)], SV)
-> [(Bool, [(String, String)], SV)]
forall a b. (a -> b) -> a -> b
$ Result -> Seq (Bool, [(String, String)], SV)
resConstraints Result
result
walkConstraints :: [(Bool, [(String, a)], SV)] -> m SMTResult -> m SMTResult
walkConstraints [] cont :: m SMTResult
cont = do
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(Bool, [(String, String)], SV)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Bool, [(String, String)], SV)]
cstrs) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> m ()
forall (m :: * -> *). MonadIO m => String -> m ()
notify "Validated all constraints."
m SMTResult
cont
walkConstraints ((isSoft :: Bool
isSoft, attrs :: [(String, a)]
attrs, sv :: SV
sv) : rest :: [(Bool, [(String, a)], SV)]
rest) cont :: m SMTResult
cont
| SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
sv Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind
KBool
= String -> m SMTResult
forall (m :: * -> *). Monad m => String -> m SMTResult
giveUp (String -> m SMTResult) -> String -> m SMTResult
forall a b. (a -> b) -> a -> b
$ "Constraint tied to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
sv String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is non-boolean."
| Bool
isSoft Bool -> Bool -> Bool
|| SV
sv SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV
= [(Bool, [(String, a)], SV)] -> m SMTResult -> m SMTResult
walkConstraints [(Bool, [(String, a)], SV)]
rest m SMTResult
cont
| SV
sv SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV
= case Maybe a
mbName of
Just nm :: a
nm -> String -> m SMTResult
forall (m :: * -> *). Monad m => String -> m SMTResult
badModel (String -> m SMTResult) -> String -> m SMTResult
forall a b. (a -> b) -> a -> b
$ "Named constraint " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " evaluated to False."
Nothing -> String -> m SMTResult
forall (m :: * -> *). Monad m => String -> m SMTResult
badModel "A constraint was violated."
| Bool
True
= SV -> m SMTResult
forall (m :: * -> *). Monad m => SV -> m SMTResult
notConcrete SV
sv
where mbName :: Maybe a
mbName = [a] -> Maybe a
forall a. [a] -> Maybe a
listToMaybe [a
n | (":named", n :: a
n) <- [(String, a)]
attrs]
satLoop :: [SV] -> m SMTResult
satLoop []
= do String -> m ()
forall (m :: * -> *). MonadIO m => String -> m ()
notify "All outputs are satisfied. Validation complete."
SMTResult -> m SMTResult
forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
res
satLoop (sv :: SV
sv:svs :: [SV]
svs)
| SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
sv Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind
KBool
= String -> m SMTResult
forall (m :: * -> *). Monad m => String -> m SMTResult
giveUp (String -> m SMTResult) -> String -> m SMTResult
forall a b. (a -> b) -> a -> b
$ "Output tied to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
sv String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is non-boolean."
| SV
sv SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV
= [SV] -> m SMTResult
satLoop [SV]
svs
| SV
sv SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV
= String -> m SMTResult
forall (m :: * -> *). Monad m => String -> m SMTResult
badModel "Final output evaluated to False."
| Bool
True
= SV -> m SMTResult
forall (m :: * -> *). Monad m => SV -> m SMTResult
notConcrete SV
sv
proveLoop :: [SV] -> Bool -> m SMTResult
proveLoop [] somethingFailed :: Bool
somethingFailed
| Bool
somethingFailed = do String -> m ()
forall (m :: * -> *). MonadIO m => String -> m ()
notify "Counterexample is validated."
SMTResult -> m SMTResult
forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
res
| Bool
True = do String -> m ()
forall (m :: * -> *). MonadIO m => String -> m ()
notify "Counterexample violates none of the outputs."
String -> m SMTResult
forall (m :: * -> *). Monad m => String -> m SMTResult
badModel "Counter-example violates no constraints."
proveLoop (sv :: SV
sv:svs :: [SV]
svs) somethingFailed :: Bool
somethingFailed
| SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
sv Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind
KBool
= String -> m SMTResult
forall (m :: * -> *). Monad m => String -> m SMTResult
giveUp (String -> m SMTResult) -> String -> m SMTResult
forall a b. (a -> b) -> a -> b
$ "Output tied to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
sv String -> String -> String
forall a. [a] -> [a] -> [a]
++ " is non-boolean."
| SV
sv SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV
= [SV] -> Bool -> m SMTResult
proveLoop [SV]
svs Bool
somethingFailed
| SV
sv SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV
= [SV] -> Bool -> m SMTResult
proveLoop [SV]
svs Bool
True
| Bool
True
= SV -> m SMTResult
forall (m :: * -> *). Monad m => SV -> m SMTResult
notConcrete SV
sv
checkOutputs :: [SV] -> m SMTResult
checkOutputs []
| [(Bool, [(String, String)], SV)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Bool, [(String, String)], SV)]
cstrs
= String -> m SMTResult
forall (m :: * -> *). Monad m => String -> m SMTResult
giveUp "Impossible happened: There are no outputs nor any constraints to check."
checkOutputs os :: [SV]
os
= do String -> m ()
forall (m :: * -> *). MonadIO m => String -> m ()
notify "Validating outputs."
if Bool
isSAT then [SV] -> m SMTResult
forall (m :: * -> *). MonadIO m => [SV] -> m SMTResult
satLoop [SV]
os
else [SV] -> Bool -> m SMTResult
forall (m :: * -> *). MonadIO m => [SV] -> Bool -> m SMTResult
proveLoop [SV]
os Bool
False
String -> m ()
forall (m :: * -> *). MonadIO m => String -> m ()
notify (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ if [(Bool, [(String, String)], SV)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Bool, [(String, String)], SV)]
cstrs
then "There are no constraints to check."
else "Validating " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([(Bool, [(String, String)], SV)] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Bool, [(String, String)], SV)]
cstrs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " constraint(s)."
[(Bool, [(String, String)], SV)] -> m SMTResult -> m SMTResult
forall (m :: * -> *) a.
(MonadIO m, Show a) =>
[(Bool, [(String, a)], SV)] -> m SMTResult -> m SMTResult
walkConstraints [(Bool, [(String, String)], SV)]
cstrs ([SV] -> m SMTResult
forall (m :: * -> *). MonadIO m => [SV] -> m SMTResult
checkOutputs (Result -> [SV]
resOutputs Result
result))
type Provable = MProvable IO
proveWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
proveWithAll :: [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
proveWithAll = ([SMTConfig]
-> (SMTConfig -> a -> IO ThmResult)
-> a
-> IO [(Solver, NominalDiffTime, ThmResult)]
forall b a.
NFData b =>
[SMTConfig]
-> (SMTConfig -> a -> IO b)
-> a
-> IO [(Solver, NominalDiffTime, b)]
`sbvWithAll` SMTConfig -> a -> IO ThmResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m ThmResult
proveWith)
proveWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, ThmResult)
proveWithAny :: [SMTConfig] -> a -> IO (Solver, NominalDiffTime, ThmResult)
proveWithAny = ([SMTConfig]
-> (SMTConfig -> a -> IO ThmResult)
-> a
-> IO (Solver, NominalDiffTime, ThmResult)
forall b a.
NFData b =>
[SMTConfig]
-> (SMTConfig -> a -> IO b) -> a -> IO (Solver, NominalDiffTime, b)
`sbvWithAny` SMTConfig -> a -> IO ThmResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m ThmResult
proveWith)
satWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
satWithAll :: [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
satWithAll = ([SMTConfig]
-> (SMTConfig -> a -> IO SatResult)
-> a
-> IO [(Solver, NominalDiffTime, SatResult)]
forall b a.
NFData b =>
[SMTConfig]
-> (SMTConfig -> a -> IO b)
-> a
-> IO [(Solver, NominalDiffTime, b)]
`sbvWithAll` SMTConfig -> a -> IO SatResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m SatResult
satWith)
satWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult)
satWithAny :: [SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult)
satWithAny = ([SMTConfig]
-> (SMTConfig -> a -> IO SatResult)
-> a
-> IO (Solver, NominalDiffTime, SatResult)
forall b a.
NFData b =>
[SMTConfig]
-> (SMTConfig -> a -> IO b) -> a -> IO (Solver, NominalDiffTime, b)
`sbvWithAny` SMTConfig -> a -> IO SatResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m SatResult
satWith)
generateSMTBenchmark :: (MonadIO m, MProvable m a) => Bool -> a -> m String
generateSMTBenchmark :: Bool -> a -> m String
generateSMTBenchmark isSat :: Bool
isSat a :: a
a = do
ZonedTime
t <- IO ZonedTime -> m ZonedTime
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ZonedTime
getZonedTime
let comments :: [String]
comments = ["Automatically created by SBV on " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ZonedTime -> String
forall a. Show a => a -> String
show ZonedTime
t]
cfg :: SMTConfig
cfg = SMTConfig
defaultSMTCfg { smtLibVersion :: SMTLibVersion
smtLibVersion = SMTLibVersion
SMTLib2 }
(_, res :: Result
res) <- SBVRunMode -> SymbolicT m SBool -> m (SBool, Result)
forall (m :: * -> *) a.
MonadIO m =>
SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
SMTMode QueryContext
QueryInternal IStage
ISetup Bool
isSat SMTConfig
cfg) (SymbolicT m SBool -> m (SBool, Result))
-> SymbolicT m SBool -> m (SBool, Result)
forall a b. (a -> b) -> a -> b
$ (if Bool
isSat then a -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ else a -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_) a
a SymbolicT m SBool
-> (SBool -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SBool -> SymbolicT m SBool
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output
let SMTProblem{SMTConfig -> SMTLibPgm
smtLibPgm :: SMTProblem -> SMTConfig -> SMTLibPgm
smtLibPgm :: SMTConfig -> SMTLibPgm
smtLibPgm} = SBVRunMode -> QueryContext -> [String] -> Result -> SMTProblem
Control.runProofOn (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
SMTMode QueryContext
QueryInternal IStage
IRun Bool
isSat SMTConfig
cfg) QueryContext
QueryInternal [String]
comments Result
res
out :: String
out = SMTLibPgm -> String
forall a. Show a => a -> String
show (SMTConfig -> SMTLibPgm
smtLibPgm SMTConfig
cfg)
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
out String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n(check-sat)\n"
checkNoOptimizations :: MonadIO m => QueryT m ()
checkNoOptimizations :: QueryT m ()
checkNoOptimizations = do [Objective (SV, SV)]
objectives <- QueryT m [Objective (SV, SV)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [Objective (SV, SV)]
Control.getObjectives
Bool -> QueryT m () -> QueryT m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Objective (SV, SV)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Objective (SV, SV)]
objectives) (QueryT m () -> QueryT m ()) -> QueryT m () -> QueryT m ()
forall a b. (a -> b) -> a -> b
$
String -> QueryT m ()
forall a. HasCallStack => String -> a
error (String -> QueryT m ()) -> String -> QueryT m ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ ""
, "*** Data.SBV: Unsupported call sat/prove when optimization objectives are present."
, "*** Use \"optimize\"/\"optimizeWith\" to calculate optimal satisfaction!"
]
instance ExtractIO m => MProvable m (SymbolicT m ()) where
forAll_ :: SymbolicT m () -> SymbolicT m SBool
forAll_ a :: SymbolicT m ()
a = SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ ((SymbolicT m ()
a SymbolicT m () -> SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return SBool
sTrue) :: SymbolicT m SBool)
forAll :: [String] -> SymbolicT m () -> SymbolicT m SBool
forAll ns :: [String]
ns a :: SymbolicT m ()
a = [String] -> SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ns ((SymbolicT m ()
a SymbolicT m () -> SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return SBool
sTrue) :: SymbolicT m SBool)
forSome_ :: SymbolicT m () -> SymbolicT m SBool
forSome_ a :: SymbolicT m ()
a = SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ ((SymbolicT m ()
a SymbolicT m () -> SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return SBool
sTrue) :: SymbolicT m SBool)
forSome :: [String] -> SymbolicT m () -> SymbolicT m SBool
forSome ns :: [String]
ns a :: SymbolicT m ()
a = [String] -> SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ns ((SymbolicT m ()
a SymbolicT m () -> SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return SBool
sTrue) :: SymbolicT m SBool)
instance ExtractIO m => MProvable m (SymbolicT m SBool) where
forAll_ :: SymbolicT m SBool -> SymbolicT m SBool
forAll_ = SymbolicT m SBool -> SymbolicT m SBool
forall a. a -> a
id
forAll :: [String] -> SymbolicT m SBool -> SymbolicT m SBool
forAll [] = SymbolicT m SBool -> SymbolicT m SBool
forall a. a -> a
id
forAll xs :: [String]
xs = String -> SymbolicT m SBool -> SymbolicT m SBool
forall a. HasCallStack => String -> a
error (String -> SymbolicT m SBool -> SymbolicT m SBool)
-> String -> SymbolicT m SBool -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ "SBV.forAll: Extra unmapped name(s) in predicate construction: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " [String]
xs
forSome_ :: SymbolicT m SBool -> SymbolicT m SBool
forSome_ = SymbolicT m SBool -> SymbolicT m SBool
forall a. a -> a
id
forSome :: [String] -> SymbolicT m SBool -> SymbolicT m SBool
forSome [] = SymbolicT m SBool -> SymbolicT m SBool
forall a. a -> a
id
forSome xs :: [String]
xs = String -> SymbolicT m SBool -> SymbolicT m SBool
forall a. HasCallStack => String -> a
error (String -> SymbolicT m SBool -> SymbolicT m SBool)
-> String -> SymbolicT m SBool -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ "SBV.forSome: Extra unmapped name(s) in predicate construction: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " [String]
xs
instance ExtractIO m => MProvable m SBool where
forAll_ :: SBool -> SymbolicT m SBool
forAll_ = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return
forAll :: [String] -> SBool -> SymbolicT m SBool
forAll _ = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return
forSome_ :: SBool -> SymbolicT m SBool
forSome_ = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return
forSome :: [String] -> SBool -> SymbolicT m SBool
forSome _ = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return
instance (SymVal a, MProvable m p) => MProvable m (SBV a -> p) where
forAll_ :: (SBV a -> p) -> SymbolicT m SBool
forAll_ k :: SBV a -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_ SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> p -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a
forAll :: [String] -> (SBV a -> p) -> SymbolicT m SBool
forAll (s :: String
s:ss :: [String]
ss) k :: SBV a -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
forall String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String] -> p -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a
forAll [] k :: SBV a -> p
k = (SBV a -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ SBV a -> p
k
forSome_ :: (SBV a -> p) -> SymbolicT m SBool
forSome_ k :: SBV a -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_ SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> p -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a
forSome :: [String] -> (SBV a -> p) -> SymbolicT m SBool
forSome (s :: String
s:ss :: [String]
ss) k :: SBV a -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String] -> p -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ss (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a
forSome [] k :: SBV a -> p
k = (SBV a -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ SBV a -> p
k
instance (HasKind a, HasKind b, MProvable m p) => MProvable m (SArray a b -> p) where
forAll_ :: (SArray a b -> p) -> SymbolicT m SBool
forAll_ k :: SArray a b -> p
k = Maybe (SBV b) -> SymbolicT m (SArray a b)
forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
Maybe (SBV b) -> m (array a b)
newArray_ Maybe (SBV b)
forall a. Maybe a
Nothing SymbolicT m (SArray a b)
-> (SArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SArray a b
a -> p -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SArray a b -> p
k SArray a b
a
forAll :: [String] -> (SArray a b -> p) -> SymbolicT m SBool
forAll (s :: String
s:ss :: [String]
ss) k :: SArray a b -> p
k = String -> Maybe (SBV b) -> SymbolicT m (SArray a b)
forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
String -> Maybe (SBV b) -> m (array a b)
newArray String
s Maybe (SBV b)
forall a. Maybe a
Nothing SymbolicT m (SArray a b)
-> (SArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SArray a b
a -> [String] -> p -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SArray a b -> p
k SArray a b
a
forAll [] k :: SArray a b -> p
k = (SArray a b -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ SArray a b -> p
k
forSome_ :: (SArray a b -> p) -> SymbolicT m SBool
forSome_ _ = String -> SymbolicT m SBool
forall a. HasCallStack => String -> a
error "SBV.forSome.SFunArray: Existential arrays are not currently supported."
forSome :: [String] -> (SArray a b -> p) -> SymbolicT m SBool
forSome _ _ = String -> SymbolicT m SBool
forall a. HasCallStack => String -> a
error "SBV.forSome.SFunArray: Existential arrays are not currently supported."
instance (HasKind a, HasKind b, MProvable m p) => MProvable m (SFunArray a b -> p) where
forAll_ :: (SFunArray a b -> p) -> SymbolicT m SBool
forAll_ k :: SFunArray a b -> p
k = Maybe (SBV b) -> SymbolicT m (SFunArray a b)
forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
Maybe (SBV b) -> m (array a b)
newArray_ Maybe (SBV b)
forall a. Maybe a
Nothing SymbolicT m (SFunArray a b)
-> (SFunArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SFunArray a b
a -> p -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SFunArray a b -> p
k SFunArray a b
a
forAll :: [String] -> (SFunArray a b -> p) -> SymbolicT m SBool
forAll (s :: String
s:ss :: [String]
ss) k :: SFunArray a b -> p
k = String -> Maybe (SBV b) -> SymbolicT m (SFunArray a b)
forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
String -> Maybe (SBV b) -> m (array a b)
newArray String
s Maybe (SBV b)
forall a. Maybe a
Nothing SymbolicT m (SFunArray a b)
-> (SFunArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SFunArray a b
a -> [String] -> p -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SFunArray a b -> p
k SFunArray a b
a
forAll [] k :: SFunArray a b -> p
k = (SFunArray a b -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ SFunArray a b -> p
k
forSome_ :: (SFunArray a b -> p) -> SymbolicT m SBool
forSome_ _ = String -> SymbolicT m SBool
forall a. HasCallStack => String -> a
error "SBV.forSome.SArray: Existential arrays are not currently supported."
forSome :: [String] -> (SFunArray a b -> p) -> SymbolicT m SBool
forSome _ _ = String -> SymbolicT m SBool
forall a. HasCallStack => String -> a
error "SBV.forSome.SArray: Existential arrays are not currently supported."
instance (SymVal a, SymVal b, MProvable m p) => MProvable m ((SBV a, SBV b) -> p) where
forAll_ :: ((SBV a, SBV b) -> p) -> SymbolicT m SBool
forAll_ k :: (SBV a, SBV b) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_ SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> (SBV b -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ ((SBV b -> p) -> SymbolicT m SBool)
-> (SBV b -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)
forAll :: [String] -> ((SBV a, SBV b) -> p) -> SymbolicT m SBool
forAll (s :: String
s:ss :: [String]
ss) k :: (SBV a, SBV b) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
forall String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String] -> (SBV b -> p) -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss ((SBV b -> p) -> SymbolicT m SBool)
-> (SBV b -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)
forAll [] k :: (SBV a, SBV b) -> p
k = ((SBV a, SBV b) -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ (SBV a, SBV b) -> p
k
forSome_ :: ((SBV a, SBV b) -> p) -> SymbolicT m SBool
forSome_ k :: (SBV a, SBV b) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_ SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> (SBV b -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ ((SBV b -> p) -> SymbolicT m SBool)
-> (SBV b -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)
forSome :: [String] -> ((SBV a, SBV b) -> p) -> SymbolicT m SBool
forSome (s :: String
s:ss :: [String]
ss) k :: (SBV a, SBV b) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String] -> (SBV b -> p) -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ss ((SBV b -> p) -> SymbolicT m SBool)
-> (SBV b -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)
forSome [] k :: (SBV a, SBV b) -> p
k = ((SBV a, SBV b) -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ (SBV a, SBV b) -> p
k
instance (SymVal a, SymVal b, SymVal c, MProvable m p) => MProvable m ((SBV a, SBV b, SBV c) -> p) where
forAll_ :: ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
forAll_ k :: (SBV a, SBV b, SBV c) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_ SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ ((SBV b -> SBV c -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c -> (SBV a, SBV b, SBV c) -> p
k (SBV a
a, SBV b
b, SBV c
c)
forAll :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
forAll (s :: String
s:ss :: [String]
ss) k :: (SBV a, SBV b, SBV c) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
forall String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String] -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss ((SBV b -> SBV c -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c -> (SBV a, SBV b, SBV c) -> p
k (SBV a
a, SBV b
b, SBV c
c)
forAll [] k :: (SBV a, SBV b, SBV c) -> p
k = ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ (SBV a, SBV b, SBV c) -> p
k
forSome_ :: ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
forSome_ k :: (SBV a, SBV b, SBV c) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_ SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ ((SBV b -> SBV c -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c -> (SBV a, SBV b, SBV c) -> p
k (SBV a
a, SBV b
b, SBV c
c)
forSome :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
forSome (s :: String
s:ss :: [String]
ss) k :: (SBV a, SBV b, SBV c) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String] -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ss ((SBV b -> SBV c -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c -> (SBV a, SBV b, SBV c) -> p
k (SBV a
a, SBV b
b, SBV c
c)
forSome [] k :: (SBV a, SBV b, SBV c) -> p
k = ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ (SBV a, SBV b, SBV c) -> p
k
instance (SymVal a, SymVal b, SymVal c, SymVal d, MProvable m p) => MProvable m ((SBV a, SBV b, SBV c, SBV d) -> p) where
forAll_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
forAll_ k :: (SBV a, SBV b, SBV c, SBV d) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_ SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ ((SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d -> (SBV a, SBV b, SBV c, SBV d) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d)
forAll :: [String]
-> ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
forAll (s :: String
s:ss :: [String]
ss) k :: (SBV a, SBV b, SBV c, SBV d) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
forall String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String] -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss ((SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d -> (SBV a, SBV b, SBV c, SBV d) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d)
forAll [] k :: (SBV a, SBV b, SBV c, SBV d) -> p
k = ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ (SBV a, SBV b, SBV c, SBV d) -> p
k
forSome_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
forSome_ k :: (SBV a, SBV b, SBV c, SBV d) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_ SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ ((SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d -> (SBV a, SBV b, SBV c, SBV d) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d)
forSome :: [String]
-> ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
forSome (s :: String
s:ss :: [String]
ss) k :: (SBV a, SBV b, SBV c, SBV d) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String] -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ss ((SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d -> (SBV a, SBV b, SBV c, SBV d) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d)
forSome [] k :: (SBV a, SBV b, SBV c, SBV d) -> p
k = ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ (SBV a, SBV b, SBV c, SBV d) -> p
k
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, MProvable m p) => MProvable m ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) where
forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
forAll_ k :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_ SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ ((SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d e :: SBV e
e -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e)
forAll :: [String]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
forAll (s :: String
s:ss :: [String]
ss) k :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
forall String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String]
-> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss ((SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d e :: SBV e
e -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e)
forAll [] k :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k
forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
forSome_ k :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_ SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ ((SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d e :: SBV e
e -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e)
forSome :: [String]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
forSome (s :: String
s:ss :: [String]
ss) k :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String]
-> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ss ((SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d e :: SBV e
e -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e)
forSome [] k :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, MProvable m p) => MProvable m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) where
forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m SBool
forAll_ k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_ SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d e :: SBV e
e f :: SBV f
f -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f)
forAll :: [String]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m SBool
forAll (s :: String
s:ss :: [String]
ss) k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
forall String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String]
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d e :: SBV e
e f :: SBV f
f -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f)
forAll [] k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k
forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m SBool
forSome_ k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_ SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d e :: SBV e
e f :: SBV f
f -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f)
forSome :: [String]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m SBool
forSome (s :: String
s:ss :: [String]
ss) k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String]
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ss ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d e :: SBV e
e f :: SBV f
f -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f)
forSome [] k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, MProvable m p) => MProvable m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) where
forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m SBool
forAll_ k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_ SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d e :: SBV e
e f :: SBV f
f g :: SBV g
g -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g)
forAll :: [String]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m SBool
forAll (s :: String
s:ss :: [String]
ss) k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
forall String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String]
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d e :: SBV e
e f :: SBV f
f g :: SBV g
g -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g)
forAll [] k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k
forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m SBool
forSome_ k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_ SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d e :: SBV e
e f :: SBV f
f g :: SBV g
g -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g)
forSome :: [String]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m SBool
forSome (s :: String
s:ss :: [String]
ss) k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String]
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ss ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d e :: SBV e
e f :: SBV f
f g :: SBV g
g -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g)
forSome [] k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k
runSMT :: MonadIO m => SymbolicT m a -> m a
runSMT :: SymbolicT m a -> m a
runSMT = SMTConfig -> SymbolicT m a -> m a
forall (m :: * -> *) a.
MonadIO m =>
SMTConfig -> SymbolicT m a -> m a
runSMTWith SMTConfig
defaultSMTCfg
runSMTWith :: MonadIO m => SMTConfig -> SymbolicT m a -> m a
runSMTWith :: SMTConfig -> SymbolicT m a -> m a
runSMTWith cfg :: SMTConfig
cfg a :: SymbolicT m a
a = (a, Result) -> a
forall a b. (a, b) -> a
fst ((a, Result) -> a) -> m (a, Result) -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBVRunMode -> SymbolicT m a -> m (a, Result)
forall (m :: * -> *) a.
MonadIO m =>
SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
SMTMode QueryContext
QueryExternal IStage
ISetup Bool
True SMTConfig
cfg) SymbolicT m a
a
runWithQuery :: MProvable m a => Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery :: Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery isSAT :: Bool
isSAT q :: QueryT m b
q cfg :: SMTConfig
cfg a :: a
a = (b, Result) -> b
forall a b. (a, b) -> a
fst ((b, Result) -> b) -> m (b, Result) -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBVRunMode -> SymbolicT m b -> m (b, Result)
forall (m :: * -> *) a.
MonadIO m =>
SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
SMTMode QueryContext
QueryInternal IStage
ISetup Bool
isSAT SMTConfig
cfg) SymbolicT m b
comp
where comp :: SymbolicT m b
comp = do SBool
_ <- (if Bool
isSAT then a -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ else a -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_) a
a SymbolicT m SBool
-> (SBool -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SBool -> SymbolicT m SBool
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output
QueryContext -> QueryT m b -> SymbolicT m b
forall (m :: * -> *) a.
ExtractIO m =>
QueryContext -> QueryT m a -> SymbolicT m a
Control.executeQuery QueryContext
QueryInternal QueryT m b
q
isSafe :: SafeResult -> Bool
isSafe :: SafeResult -> Bool
isSafe (SafeResult (_, _, result :: SMTResult
result)) = case SMTResult
result of
Unsatisfiable{} -> Bool
True
Satisfiable{} -> Bool
False
SatExtField{} -> Bool
False
Unknown{} -> Bool
False
ProofError{} -> Bool
False
runInThread :: NFData b => UTCTime -> (SMTConfig -> IO b) -> SMTConfig -> IO (Async (Solver, NominalDiffTime, b))
runInThread :: UTCTime
-> (SMTConfig -> IO b)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, b))
runInThread beginTime :: UTCTime
beginTime action :: SMTConfig -> IO b
action config :: SMTConfig
config = IO (Solver, NominalDiffTime, b)
-> IO (Async (Solver, NominalDiffTime, b))
forall a. IO a -> IO (Async a)
async (IO (Solver, NominalDiffTime, b)
-> IO (Async (Solver, NominalDiffTime, b)))
-> IO (Solver, NominalDiffTime, b)
-> IO (Async (Solver, NominalDiffTime, b))
forall a b. (a -> b) -> a -> b
$ do
b
result <- SMTConfig -> IO b
action SMTConfig
config
UTCTime
endTime <- b -> ()
forall a. NFData a => a -> ()
rnf b
result () -> IO UTCTime -> IO UTCTime
forall a b. a -> b -> b
`seq` IO UTCTime
getCurrentTime
(Solver, NominalDiffTime, b) -> IO (Solver, NominalDiffTime, b)
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
config), UTCTime
endTime UTCTime -> UTCTime -> NominalDiffTime
`diffUTCTime` UTCTime
beginTime, b
result)
sbvWithAny :: NFData b => [SMTConfig] -> (SMTConfig -> a -> IO b) -> a -> IO (Solver, NominalDiffTime, b)
sbvWithAny :: [SMTConfig]
-> (SMTConfig -> a -> IO b) -> a -> IO (Solver, NominalDiffTime, b)
sbvWithAny [] _ _ = String -> IO (Solver, NominalDiffTime, b)
forall a. HasCallStack => String -> a
error "SBV.withAny: No solvers given!"
sbvWithAny solvers :: [SMTConfig]
solvers what :: SMTConfig -> a -> IO b
what a :: a
a = do UTCTime
beginTime <- IO UTCTime
getCurrentTime
(Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
-> (Solver, NominalDiffTime, b)
forall a b. (a, b) -> b
snd ((Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
-> (Solver, NominalDiffTime, b))
-> IO
(Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
-> IO (Solver, NominalDiffTime, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ((SMTConfig -> IO (Async (Solver, NominalDiffTime, b)))
-> [SMTConfig] -> IO [Async (Solver, NominalDiffTime, b)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (UTCTime
-> (SMTConfig -> IO b)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, b))
forall b.
NFData b =>
UTCTime
-> (SMTConfig -> IO b)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, b))
runInThread UTCTime
beginTime (SMTConfig -> a -> IO b
`what` a
a)) [SMTConfig]
solvers IO [Async (Solver, NominalDiffTime, b)]
-> ([Async (Solver, NominalDiffTime, b)]
-> IO
(Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b)))
-> IO
(Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Async (Solver, NominalDiffTime, b)]
-> IO
(Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
forall a. [Async a] -> IO (Async a, a)
waitAnyFastCancel)
where
waitAnyFastCancel :: [Async a] -> IO (Async a, a)
waitAnyFastCancel asyncs :: [Async a]
asyncs = [Async a] -> IO (Async a, a)
forall a. [Async a] -> IO (Async a, a)
waitAny [Async a]
asyncs IO (Async a, a) -> IO () -> IO (Async a, a)
forall a b. IO a -> IO b -> IO a
`finally` (Async a -> IO ()) -> [Async a] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Async a -> IO ()
forall a. Async a -> IO ()
cancelFast [Async a]
asyncs
cancelFast :: Async a -> IO ()
cancelFast other :: Async a
other = ThreadId -> AsyncException -> IO ()
forall e. Exception e => ThreadId -> e -> IO ()
throwTo (Async a -> ThreadId
forall a. Async a -> ThreadId
asyncThreadId Async a
other) AsyncException
ThreadKilled
sbvWithAll :: NFData b => [SMTConfig] -> (SMTConfig -> a -> IO b) -> a -> IO [(Solver, NominalDiffTime, b)]
sbvWithAll :: [SMTConfig]
-> (SMTConfig -> a -> IO b)
-> a
-> IO [(Solver, NominalDiffTime, b)]
sbvWithAll solvers :: [SMTConfig]
solvers what :: SMTConfig -> a -> IO b
what a :: a
a = do UTCTime
beginTime <- IO UTCTime
getCurrentTime
(SMTConfig -> IO (Async (Solver, NominalDiffTime, b)))
-> [SMTConfig] -> IO [Async (Solver, NominalDiffTime, b)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (UTCTime
-> (SMTConfig -> IO b)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, b))
forall b.
NFData b =>
UTCTime
-> (SMTConfig -> IO b)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, b))
runInThread UTCTime
beginTime (SMTConfig -> a -> IO b
`what` a
a)) [SMTConfig]
solvers IO [Async (Solver, NominalDiffTime, b)]
-> ([Async (Solver, NominalDiffTime, b)]
-> IO [(Solver, NominalDiffTime, b)])
-> IO [(Solver, NominalDiffTime, b)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (IO [(Solver, NominalDiffTime, b)]
-> IO [(Solver, NominalDiffTime, b)]
forall a. IO a -> IO a
unsafeInterleaveIO (IO [(Solver, NominalDiffTime, b)]
-> IO [(Solver, NominalDiffTime, b)])
-> ([Async (Solver, NominalDiffTime, b)]
-> IO [(Solver, NominalDiffTime, b)])
-> [Async (Solver, NominalDiffTime, b)]
-> IO [(Solver, NominalDiffTime, b)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Async (Solver, NominalDiffTime, b)]
-> IO [(Solver, NominalDiffTime, b)]
forall a. [Async a] -> IO [a]
go)
where go :: [Async a] -> IO [a]
go [] = [a] -> IO [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
go as :: [Async a]
as = do (d :: Async a
d, r :: a
r) <- [Async a] -> IO (Async a, a)
forall a. [Async a] -> IO (Async a, a)
waitAny [Async a]
as
[a]
rs <- IO [a] -> IO [a]
forall a. IO a -> IO a
unsafeInterleaveIO (IO [a] -> IO [a]) -> IO [a] -> IO [a]
forall a b. (a -> b) -> a -> b
$ [Async a] -> IO [a]
go ((Async a -> Bool) -> [Async a] -> [Async a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Async a -> Async a -> Bool
forall a. Eq a => a -> a -> Bool
/= Async a
d) [Async a]
as)
[a] -> IO [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (a
r a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
rs)
class ExtractIO m => SExecutable m a where
sName_ :: a -> SymbolicT m ()
sName :: [String] -> a -> SymbolicT m ()
safe :: a -> m [SafeResult]
safe = SMTConfig -> a -> m [SafeResult]
forall (m :: * -> *) a.
SExecutable m a =>
SMTConfig -> a -> m [SafeResult]
safeWith SMTConfig
defaultSMTCfg
safeWith :: SMTConfig -> a -> m [SafeResult]
safeWith cfg :: SMTConfig
cfg a :: a
a = do String
cwd <- (String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/") (String -> String) -> m String -> m String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO String -> m String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO String
getCurrentDirectory
let mkRelative :: String -> String
mkRelative path :: String
path
| String
cwd String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
path = Int -> String -> String
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
cwd) String
path
| Bool
True = String
path
([SafeResult], Result) -> [SafeResult]
forall a b. (a, b) -> a
fst (([SafeResult], Result) -> [SafeResult])
-> m ([SafeResult], Result) -> m [SafeResult]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBVRunMode -> SymbolicT m [SafeResult] -> m ([SafeResult], Result)
forall (m :: * -> *) a.
MonadIO m =>
SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
SMTMode QueryContext
QueryInternal IStage
ISafe Bool
True SMTConfig
cfg) (a -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ a
a SymbolicT m ()
-> SymbolicT m [SafeResult] -> SymbolicT m [SafeResult]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (String -> String) -> SymbolicT m [SafeResult]
check String -> String
mkRelative)
where check :: (FilePath -> FilePath) -> SymbolicT m [SafeResult]
check :: (String -> String) -> SymbolicT m [SafeResult]
check mkRelative :: String -> String
mkRelative = QueryContext -> QueryT m [SafeResult] -> SymbolicT m [SafeResult]
forall (m :: * -> *) a.
ExtractIO m =>
QueryContext -> QueryT m a -> SymbolicT m a
Control.executeQuery QueryContext
QueryInternal (QueryT m [SafeResult] -> SymbolicT m [SafeResult])
-> QueryT m [SafeResult] -> SymbolicT m [SafeResult]
forall a b. (a -> b) -> a -> b
$ QueryT m [(String, Maybe CallStack, SV)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, Maybe CallStack, SV)]
Control.getSBVAssertions QueryT m [(String, Maybe CallStack, SV)]
-> ([(String, Maybe CallStack, SV)] -> QueryT m [SafeResult])
-> QueryT m [SafeResult]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ((String, Maybe CallStack, SV) -> QueryT m SafeResult)
-> [(String, Maybe CallStack, SV)] -> QueryT m [SafeResult]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((String -> String)
-> (String, Maybe CallStack, SV) -> QueryT m SafeResult
verify String -> String
mkRelative)
verify :: (FilePath -> FilePath) -> (String, Maybe CallStack, SV) -> QueryT m SafeResult
verify :: (String -> String)
-> (String, Maybe CallStack, SV) -> QueryT m SafeResult
verify mkRelative :: String -> String
mkRelative (msg :: String
msg, cs :: Maybe CallStack
cs, cond :: SV
cond) = do
let locInfo :: [(String, SrcLoc)] -> String
locInfo ps :: [(String, SrcLoc)]
ps = let loc :: (String, SrcLoc) -> String
loc (f :: String
f, sl :: SrcLoc
sl) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String -> String
mkRelative (SrcLoc -> String
srcLocFile SrcLoc
sl), ":", Int -> String
forall a. Show a => a -> String
show (SrcLoc -> Int
srcLocStartLine SrcLoc
sl), ":", Int -> String
forall a. Show a => a -> String
show (SrcLoc -> Int
srcLocStartCol SrcLoc
sl), ":", String
f]
in String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ",\n " (((String, SrcLoc) -> String) -> [(String, SrcLoc)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, SrcLoc) -> String
loc [(String, SrcLoc)]
ps)
location :: Maybe String
location = ([(String, SrcLoc)] -> String
locInfo ([(String, SrcLoc)] -> String)
-> (CallStack -> [(String, SrcLoc)]) -> CallStack -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> [(String, SrcLoc)]
getCallStack) (CallStack -> String) -> Maybe CallStack -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Maybe CallStack
cs
SMTResult
result <- do Int -> QueryT m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
Control.push 1
Bool -> String -> QueryT m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
Control.send Bool
True (String -> QueryT m ()) -> String -> QueryT m ()
forall a b. (a -> b) -> a -> b
$ "(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
cond String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
SMTResult
r <- QueryT m SMTResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
Control.getSMTResult
Int -> QueryT m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
Control.pop 1
SMTResult -> QueryT m SMTResult
forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
r
SafeResult -> QueryT m SafeResult
forall (m :: * -> *) a. Monad m => a -> m a
return (SafeResult -> QueryT m SafeResult)
-> SafeResult -> QueryT m SafeResult
forall a b. (a -> b) -> a -> b
$ (Maybe String, String, SMTResult) -> SafeResult
SafeResult (Maybe String
location, String
msg, SMTResult
result)
instance (ExtractIO m, NFData a) => SExecutable m (SymbolicT m a) where
sName_ :: SymbolicT m a -> SymbolicT m ()
sName_ a :: SymbolicT m a
a = SymbolicT m a
a SymbolicT m a -> (a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \r :: a
r -> a -> ()
forall a. NFData a => a -> ()
rnf a
r () -> SymbolicT m () -> SymbolicT m ()
forall a b. a -> b -> b
`seq` () -> SymbolicT m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
sName :: [String] -> SymbolicT m a -> SymbolicT m ()
sName [] = SymbolicT m a -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_
sName xs :: [String]
xs = String -> SymbolicT m a -> SymbolicT m ()
forall a. HasCallStack => String -> a
error (String -> SymbolicT m a -> SymbolicT m ())
-> String -> SymbolicT m a -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ "SBV.SExecutable.sName: Extra unmapped name(s): " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " [String]
xs
instance ExtractIO m => SExecutable m (SBV a) where
sName_ :: SBV a -> SymbolicT m ()
sName_ v :: SBV a
v = SymbolicT m (SBV a) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
v :: SymbolicT m (SBV a))
sName :: [String] -> SBV a -> SymbolicT m ()
sName xs :: [String]
xs v :: SBV a
v = [String] -> SymbolicT m (SBV a) -> SymbolicT m ()
forall (m :: * -> *) a.
SExecutable m a =>
[String] -> a -> SymbolicT m ()
sName [String]
xs (SBV a -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
v :: SymbolicT m (SBV a))
instance ExtractIO m => SExecutable m () where
sName_ :: () -> SymbolicT m ()
sName_ () = SymbolicT m () -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (() -> SymbolicT m ()
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output () :: SymbolicT m ())
sName :: [String] -> () -> SymbolicT m ()
sName xs :: [String]
xs () = [String] -> SymbolicT m () -> SymbolicT m ()
forall (m :: * -> *) a.
SExecutable m a =>
[String] -> a -> SymbolicT m ()
sName [String]
xs (() -> SymbolicT m ()
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output () :: SymbolicT m ())
instance ExtractIO m => SExecutable m [SBV a] where
sName_ :: [SBV a] -> SymbolicT m ()
sName_ vs :: [SBV a]
vs = SymbolicT m [SBV a] -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ ([SBV a] -> SymbolicT m [SBV a]
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output [SBV a]
vs :: SymbolicT m [SBV a])
sName :: [String] -> [SBV a] -> SymbolicT m ()
sName xs :: [String]
xs vs :: [SBV a]
vs = [String] -> SymbolicT m [SBV a] -> SymbolicT m ()
forall (m :: * -> *) a.
SExecutable m a =>
[String] -> a -> SymbolicT m ()
sName [String]
xs ([SBV a] -> SymbolicT m [SBV a]
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output [SBV a]
vs :: SymbolicT m [SBV a])
instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b) => SExecutable m (SBV a, SBV b) where
sName_ :: (SBV a, SBV b) -> SymbolicT m ()
sName_ (a :: SBV a
a, b :: SBV b
b) = SymbolicT m (SBV b) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV b)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV b -> SymbolicT m (SBV b)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV b
b :: SymbolicT m (SBV b))
sName :: [String] -> (SBV a, SBV b) -> SymbolicT m ()
sName _ = (SBV a, SBV b) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_
instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c) => SExecutable m (SBV a, SBV b, SBV c) where
sName_ :: (SBV a, SBV b, SBV c) -> SymbolicT m ()
sName_ (a :: SBV a
a, b :: SBV b
b, c :: SBV c
c) = SymbolicT m (SBV c) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV b)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV b -> SymbolicT m (SBV b)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV b
b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV c -> SymbolicT m (SBV c)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV c
c :: SymbolicT m (SBV c))
sName :: [String] -> (SBV a, SBV b, SBV c) -> SymbolicT m ()
sName _ = (SBV a, SBV b, SBV c) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_
instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c, NFData d, SymVal d) => SExecutable m (SBV a, SBV b, SBV c, SBV d) where
sName_ :: (SBV a, SBV b, SBV c, SBV d) -> SymbolicT m ()
sName_ (a :: SBV a
a, b :: SBV b
b, c :: SBV c
c, d :: SBV d
d) = SymbolicT m (SBV d) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV b)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV b -> SymbolicT m (SBV b)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV b
b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV c -> SymbolicT m (SBV c)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV c
c SymbolicT m (SBV c) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV c -> SymbolicT m (SBV c)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV c
c SymbolicT m (SBV c) -> SymbolicT m (SBV d) -> SymbolicT m (SBV d)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV d -> SymbolicT m (SBV d)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV d
d :: SymbolicT m (SBV d))
sName :: [String] -> (SBV a, SBV b, SBV c, SBV d) -> SymbolicT m ()
sName _ = (SBV a, SBV b, SBV c, SBV d) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_
instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c, NFData d, SymVal d, NFData e, SymVal e) => SExecutable m (SBV a, SBV b, SBV c, SBV d, SBV e) where
sName_ :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> SymbolicT m ()
sName_ (a :: SBV a
a, b :: SBV b
b, c :: SBV c
c, d :: SBV d
d, e :: SBV e
e) = SymbolicT m (SBV e) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV b)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV b -> SymbolicT m (SBV b)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV b
b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV c -> SymbolicT m (SBV c)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV c
c SymbolicT m (SBV c) -> SymbolicT m (SBV d) -> SymbolicT m (SBV d)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV d -> SymbolicT m (SBV d)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV d
d SymbolicT m (SBV d) -> SymbolicT m (SBV e) -> SymbolicT m (SBV e)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV e -> SymbolicT m (SBV e)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV e
e :: SymbolicT m (SBV e))
sName :: [String] -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> SymbolicT m ()
sName _ = (SBV a, SBV b, SBV c, SBV d, SBV e) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_
instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c, NFData d, SymVal d, NFData e, SymVal e, NFData f, SymVal f) => SExecutable m (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) where
sName_ :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> SymbolicT m ()
sName_ (a :: SBV a
a, b :: SBV b
b, c :: SBV c
c, d :: SBV d
d, e :: SBV e
e, f :: SBV f
f) = SymbolicT m (SBV f) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV b)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV b -> SymbolicT m (SBV b)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV b
b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV c -> SymbolicT m (SBV c)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV c
c SymbolicT m (SBV c) -> SymbolicT m (SBV d) -> SymbolicT m (SBV d)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV d -> SymbolicT m (SBV d)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV d
d SymbolicT m (SBV d) -> SymbolicT m (SBV e) -> SymbolicT m (SBV e)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV e -> SymbolicT m (SBV e)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV e
e SymbolicT m (SBV e) -> SymbolicT m (SBV f) -> SymbolicT m (SBV f)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV f -> SymbolicT m (SBV f)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV f
f :: SymbolicT m (SBV f))
sName :: [String]
-> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> SymbolicT m ()
sName _ = (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_
instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c, NFData d, SymVal d, NFData e, SymVal e, NFData f, SymVal f, NFData g, SymVal g) => SExecutable m (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) where
sName_ :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> SymbolicT m ()
sName_ (a :: SBV a
a, b :: SBV b
b, c :: SBV c
c, d :: SBV d
d, e :: SBV e
e, f :: SBV f
f, g :: SBV g
g) = SymbolicT m (SBV g) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV b)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV b -> SymbolicT m (SBV b)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV b
b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV c -> SymbolicT m (SBV c)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV c
c SymbolicT m (SBV c) -> SymbolicT m (SBV d) -> SymbolicT m (SBV d)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV d -> SymbolicT m (SBV d)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV d
d SymbolicT m (SBV d) -> SymbolicT m (SBV e) -> SymbolicT m (SBV e)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV e -> SymbolicT m (SBV e)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV e
e SymbolicT m (SBV e) -> SymbolicT m (SBV f) -> SymbolicT m (SBV f)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV f -> SymbolicT m (SBV f)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV f
f SymbolicT m (SBV f) -> SymbolicT m (SBV g) -> SymbolicT m (SBV g)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBV g -> SymbolicT m (SBV g)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV g
g :: SymbolicT m (SBV g))
sName :: [String]
-> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g)
-> SymbolicT m ()
sName _ = (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_
instance (SymVal a, SExecutable m p) => SExecutable m (SBV a -> p) where
sName_ :: (SBV a -> p) -> SymbolicT m ()
sName_ k :: SBV a -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_ SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> p -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (p -> SymbolicT m ()) -> p -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a
sName :: [String] -> (SBV a -> p) -> SymbolicT m ()
sName (s :: String
s:ss :: [String]
ss) k :: SBV a -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String] -> p -> SymbolicT m ()
forall (m :: * -> *) a.
SExecutable m a =>
[String] -> a -> SymbolicT m ()
sName [String]
ss (p -> SymbolicT m ()) -> p -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a
sName [] k :: SBV a -> p
k = (SBV a -> p) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ SBV a -> p
k
instance (SymVal a, SymVal b, SExecutable m p) => SExecutable m ((SBV a, SBV b) -> p) where
sName_ :: ((SBV a, SBV b) -> p) -> SymbolicT m ()
sName_ k :: (SBV a, SBV b) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_ SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> (SBV b -> p) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ ((SBV b -> p) -> SymbolicT m ()) -> (SBV b -> p) -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)
sName :: [String] -> ((SBV a, SBV b) -> p) -> SymbolicT m ()
sName (s :: String
s:ss :: [String]
ss) k :: (SBV a, SBV b) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String] -> (SBV b -> p) -> SymbolicT m ()
forall (m :: * -> *) a.
SExecutable m a =>
[String] -> a -> SymbolicT m ()
sName [String]
ss ((SBV b -> p) -> SymbolicT m ()) -> (SBV b -> p) -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)
sName [] k :: (SBV a, SBV b) -> p
k = ((SBV a, SBV b) -> p) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a, SBV b) -> p
k
instance (SymVal a, SymVal b, SymVal c, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c) -> p) where
sName_ :: ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m ()
sName_ k :: (SBV a, SBV b, SBV c) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_ SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> (SBV b -> SBV c -> p) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ ((SBV b -> SBV c -> p) -> SymbolicT m ())
-> (SBV b -> SBV c -> p) -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c -> (SBV a, SBV b, SBV c) -> p
k (SBV a
a, SBV b
b, SBV c
c)
sName :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m ()
sName (s :: String
s:ss :: [String]
ss) k :: (SBV a, SBV b, SBV c) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String] -> (SBV b -> SBV c -> p) -> SymbolicT m ()
forall (m :: * -> *) a.
SExecutable m a =>
[String] -> a -> SymbolicT m ()
sName [String]
ss ((SBV b -> SBV c -> p) -> SymbolicT m ())
-> (SBV b -> SBV c -> p) -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c -> (SBV a, SBV b, SBV c) -> p
k (SBV a
a, SBV b
b, SBV c
c)
sName [] k :: (SBV a, SBV b, SBV c) -> p
k = ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a, SBV b, SBV c) -> p
k
instance (SymVal a, SymVal b, SymVal c, SymVal d, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d) -> p) where
sName_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m ()
sName_ k :: (SBV a, SBV b, SBV c, SBV d) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_ SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ ((SBV b -> SBV c -> SBV d -> p) -> SymbolicT m ())
-> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d -> (SBV a, SBV b, SBV c, SBV d) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d)
sName :: [String] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m ()
sName (s :: String
s:ss :: [String]
ss) k :: (SBV a, SBV b, SBV c, SBV d) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String] -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m ()
forall (m :: * -> *) a.
SExecutable m a =>
[String] -> a -> SymbolicT m ()
sName [String]
ss ((SBV b -> SBV c -> SBV d -> p) -> SymbolicT m ())
-> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d -> (SBV a, SBV b, SBV c, SBV d) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d)
sName [] k :: (SBV a, SBV b, SBV c, SBV d) -> p
k = ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a, SBV b, SBV c, SBV d) -> p
k
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) where
sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m ()
sName_ k :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_ SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ ((SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m ())
-> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d e :: SBV e
e -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e)
sName :: [String]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m ()
sName (s :: String
s:ss :: [String]
ss) k :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String]
-> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m ()
forall (m :: * -> *) a.
SExecutable m a =>
[String] -> a -> SymbolicT m ()
sName [String]
ss ((SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m ())
-> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d e :: SBV e
e -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e)
sName [] k :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) where
sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> SymbolicT m ()
sName_ k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_ SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m ())
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d e :: SBV e
e f :: SBV f
f -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f)
sName :: [String]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m ()
sName (s :: String
s:ss :: [String]
ss) k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String]
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m ()
forall (m :: * -> *) a.
SExecutable m a =>
[String] -> a -> SymbolicT m ()
sName [String]
ss ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m ())
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d e :: SBV e
e f :: SBV f
f -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f)
sName [] k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) where
sName_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m ()
sName_ k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_ SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m ())
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d e :: SBV e
e f :: SBV f
f g :: SBV g
g -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g)
sName :: [String]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m ()
sName (s :: String
s:ss :: [String]
ss) k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SBV a
a -> [String]
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m ()
forall (m :: * -> *) a.
SExecutable m a =>
[String] -> a -> SymbolicT m ()
sName [String]
ss ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m ())
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \b :: SBV b
b c :: SBV c
c d :: SBV d
d e :: SBV e
e f :: SBV f
f g :: SBV g
g -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g)
sName [] k :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k
{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}