sbv-14.1: Data/SBV/Provers/Prover.hs
-----------------------------------------------------------------------------
-- |
-- Module : Data.SBV.Provers.Prover
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Provable abstraction and the connection to SMT solvers
-----------------------------------------------------------------------------
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module Data.SBV.Provers.Prover (
SMTSolver(..), SMTConfig(..), Predicate
, ProvableM(..), Provable, SatisfiableM(..), Satisfiable
, generateSMTBenchmarkSat, generateSMTBenchmarkProof, defs2smt, ConstraintSet
, ThmResult(..), SatResult(..), AllSatResult(..), SafeResult(..), OptimizeResult(..), SMTResult(..)
, SExecutable(..), isSafe
, runSMT, runSMTWith
, SatModel(..), Modelable(..), displayModels, extractModels
, getModelDictionaries, getModelValues
, abc, boolector, bitwuzla, cvc4, cvc5, dReal, mathSAT, yices, z3, openSMT, defaultSMTCfg, defaultDeltaSMTCfg
, proveWithAny, proveWithAll, proveConcurrentWithAny, proveConcurrentWithAll
, satWithAny, satWithAll, satConcurrentWithAny, satConcurrentWithAll
) where
import Control.Monad (unless)
import Control.Monad.IO.Class (MonadIO, liftIO)
import Control.DeepSeq (rnf, NFData(..))
import Control.Concurrent.Async (async, waitAny, asyncThreadId, Async, mapConcurrently)
import Control.Exception (finally, throwTo)
import System.Exit (ExitCode(ExitSuccess))
import System.IO.Unsafe (unsafeInterleaveIO) -- only used safely!
import System.Directory (getCurrentDirectory)
import Data.Time (getZonedTime, NominalDiffTime, UTCTime, getCurrentTime, diffUTCTime)
import Data.List (intercalate, isPrefixOf)
import Data.Maybe (mapMaybe, listToMaybe)
import qualified Data.Set as Set (empty)
import qualified Data.Foldable as S (toList)
import qualified Data.Text as T
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.Lib (showText)
import Data.SBV.Utils.TDiff
import Data.SBV.Lambda () -- instances only
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.ABC as ABC
import qualified Data.SBV.Provers.Boolector as Boolector
import qualified Data.SBV.Provers.Bitwuzla as Bitwuzla
import qualified Data.SBV.Provers.CVC4 as CVC4
import qualified Data.SBV.Provers.CVC5 as CVC5
import qualified Data.SBV.Provers.DReal as DReal
import qualified Data.SBV.Provers.MathSAT as MathSAT
import qualified Data.SBV.Provers.Yices as Yices
import qualified Data.SBV.Provers.Z3 as Z3
import qualified Data.SBV.Provers.OpenSMT as OpenSMT
import GHC.TypeLits
mkConfig :: SMTSolver -> SMTLibVersion -> [Control.SMTOption] -> SMTConfig
mkConfig s smtVersion startOpts = SMTConfig { verbose = False
, timing = NoTiming
, printBase = 10
, printRealPrec = 16
, crackNum = False
, crackNumSurfaceVals = []
, transcript = Nothing
, solver = s
, smtLibVersion = smtVersion
, dsatPrecision = Nothing
, extraArgs = []
, satCmd = "(check-sat)"
, allSatTrackUFs = True -- i.e., yes, do extract UI function values
, allSatMaxModelCount = Nothing -- i.e., return all satisfying models
, allSatPrintAlong = False -- i.e., do not print models as they are found
, isNonModelVar = const False -- i.e., everything is a model-variable by default
, validateModel = False
, optimizeValidateConstraints = False
, roundingMode = RoundNearestTiesToEven
, solverSetOptions = startOpts
, ignoreExitCode = False
, redirectVerbose = Nothing
, firstifyUniqueLen = 10
, tpOptions = TPOptions { ribbonLength = 40
, quiet = False
, printAsms = False
, printStats = False
, measuresBeingVerified = Set.empty
}
}
-- | If supported, this makes all output go to stdout, which works better with SBV
-- Alas, not all solvers support it..
allOnStdOut :: Control.SMTOption
allOnStdOut = Control.DiagnosticOutputChannel "stdout"
-- | Default configuration for the ABC synthesis and verification tool.
abc :: SMTConfig
abc = mkConfig ABC.abc SMTLib2 [allOnStdOut]
-- | Default configuration for the Boolector SMT solver
boolector :: SMTConfig
boolector = mkConfig Boolector.boolector SMTLib2 []
-- | Default configuration for the Bitwuzla SMT solver
bitwuzla :: SMTConfig
bitwuzla = mkConfig Bitwuzla.bitwuzla SMTLib2 []
-- | Default configuration for the CVC4 SMT Solver.
cvc4 :: SMTConfig
cvc4 = mkConfig CVC4.cvc4 SMTLib2 [allOnStdOut]
-- | Default configuration for the CVC5 SMT Solver.
cvc5 :: SMTConfig
cvc5 = mkConfig CVC5.cvc5 SMTLib2 [allOnStdOut]
-- | Default configuration for the Yices SMT Solver.
dReal :: SMTConfig
dReal = mkConfig DReal.dReal SMTLib2 [ Control.OptionKeyword ":smtlib2_compliant" ["true"]
]
-- | Default configuration for the MathSAT SMT solver
mathSAT :: SMTConfig
mathSAT = mkConfig MathSAT.mathSAT SMTLib2 [allOnStdOut]
-- | Default configuration for the Yices SMT Solver.
yices :: SMTConfig
yices = mkConfig Yices.yices SMTLib2 []
-- | Default configuration for the Z3 SMT solver
z3 :: SMTConfig
z3 = mkConfig Z3.z3 SMTLib2 [ Control.OptionKeyword ":smtlib2_compliant" ["true"]
, allOnStdOut
]
-- | Default configuration for the OpenSMT SMT solver
openSMT :: SMTConfig
openSMT = mkConfig OpenSMT.openSMT SMTLib2 [ Control.OptionKeyword ":smtlib2_compliant" ["true"]
, allOnStdOut
]
-- | The default solver used by SBV. This is currently set to z3.
defaultSMTCfg :: SMTConfig
defaultSMTCfg = z3
-- | The default solver used by SBV for delta-satisfiability problems. This is currently set to dReal,
-- which is also the only solver that supports delta-satisfiability.
defaultDeltaSMTCfg :: SMTConfig
defaultDeltaSMTCfg = dReal
-- | A predicate is a symbolic program that returns a (symbolic) boolean value. For all intents and
-- purposes, it can be treated as an n-ary function from symbolic-values to a boolean. The 'Symbolic'
-- monad captures the underlying representation, and can/should be ignored by the users of the library,
-- unless you are building further utilities on top of SBV itself. Instead, simply use the 'Predicate'
-- type when necessary.
type Predicate = Symbolic SBool
-- | A constraint set is a symbolic program that returns no values. The idea is that the constraints/min-max
-- goals will serve as the collection of constraints that will be used for sat/optimize calls.
type ConstraintSet = Symbolic ()
-- | `Provable` is specialization of `ProvableM` to the `IO` monad. Unless you are using
-- transformers explicitly, this is the type you should prefer.
type Provable = ProvableM IO
-- | `Data.SBV.Provers.Satisfiable` is specialization of `SatisfiableM` to the `IO` monad. Unless you are using
-- transformers explicitly, this is the type you should prefer.
type Satisfiable = SatisfiableM IO
-- | A type @a@ is satisfiable if it has constraints, potentially returning a boolean. This class
-- captures essentially sat and optimize calls.
class ExtractIO m => SatisfiableM m a where
-- | Reduce an arg, for sat purposes.
satArgReduce :: a -> SymbolicT m SBool
-- | Generalization of 'Data.SBV.sat'
sat :: a -> m SatResult
sat = satWith defaultSMTCfg
-- | Generalization of 'Data.SBV.satWith'
satWith :: SMTConfig -> a -> m SatResult
satWith cfg a = do r <- runWithQuery satArgReduce True (checkNoOptimizations >> Control.getSMTResult) cfg a
SatResult <$> if validationRequested cfg
then validate satArgReduce True cfg a r
else pure r
-- | Generalization of 'Data.SBV.sat'
dsat :: a -> m SatResult
dsat = dsatWith defaultDeltaSMTCfg
-- | Generalization of 'Data.SBV.satWith'
dsatWith :: SMTConfig -> a -> m SatResult
dsatWith cfg a = do r <- runWithQuery satArgReduce True (checkNoOptimizations >> Control.getSMTResult) cfg a
SatResult <$> if validationRequested cfg
then validate satArgReduce True cfg a r
else pure r
-- | Generalization of 'Data.SBV.allSat'
allSat :: a -> m AllSatResult
allSat = allSatWith defaultSMTCfg
-- | Generalization of 'Data.SBV.allSatWith'
allSatWith :: SMTConfig -> a -> m AllSatResult
allSatWith cfg a = do asr <- runWithQuery satArgReduce True (checkNoOptimizations >> Control.getAllSatResult) cfg a
if validationRequested cfg
then do rs' <- mapM (validate satArgReduce True cfg a) (allSatResults asr)
pure asr{allSatResults = rs'}
else pure asr
-- | Generalization of 'Data.SBV.isSatisfiable'
isSatisfiable :: a -> m Bool
isSatisfiable = isSatisfiableWith defaultSMTCfg
-- | Generalization of 'Data.SBV.isSatisfiableWith'
isSatisfiableWith :: SMTConfig -> a -> m Bool
isSatisfiableWith cfg p = do r <- satWith cfg p
case r of
SatResult Satisfiable{} -> pure True
SatResult Unsatisfiable{} -> pure False
_ -> error $ "SBV.isSatisfiable: Received: " ++ show r
-- | Generalization of 'Data.SBV.optimize'
optimize :: OptimizeStyle -> a -> m OptimizeResult
optimize = optimizeWith defaultSMTCfg
-- | Generalization of 'Data.SBV.optimizeWith'
optimizeWith :: SMTConfig -> OptimizeStyle -> a -> m OptimizeResult
optimizeWith config style optGoal = do
res <- runWithQuery satArgReduce True opt config optGoal
if not (optimizeValidateConstraints config)
then pure res
else let v :: SMTResult -> m SMTResult
v = validate satArgReduce True config optGoal
in case res of
LexicographicResult m -> LexicographicResult <$> v m
IndependentResult xs -> let w [] sofar = pure (reverse sofar)
w ((n, m):rest) sofar = v m >>= \m' -> w rest ((n, m') : sofar)
in IndependentResult <$> w xs []
ParetoResult (b, rs) -> ParetoResult . (b, ) <$> mapM v rs
where opt = do mbDirs <- Control.startOptimizer config style
case mbDirs of
Nothing -> error $ unlines [ ""
, "*** Data.SBV: Unsupported call to optimize when no objectives are present."
, "*** Use \"sat\" for plain satisfaction"
]
Just (objectives, optimizerDirectives) -> do
mapM_ (Control.send True . T.pack) optimizerDirectives
case style of
Lexicographic -> LexicographicResult <$> Control.getLexicographicOptResults
Independent -> IndependentResult <$> Control.getIndependentOptResults (map objectiveName objectives)
Pareto mbN -> ParetoResult <$> Control.getParetoOptResults mbN
-- | Find a satisfying assignment to a property with multiple solvers, running them in separate threads. The
-- results will be returned in the order produced.
satWithAll :: Satisfiable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
satWithAll = (`sbvWithAll` satWith)
-- | Find a satisfying assignment to a property with multiple solvers, running them in separate threads. Only
-- the result of the first one to finish will be returned, remaining threads will be killed.
-- Note that we send an exception to the losing processes, but we do *not* actually wait for them
-- to finish. In rare cases this can lead to zombie processes. In previous experiments, we found
-- that some processes take their time to terminate. So, this solution favors quick turnaround.
satWithAny :: Satisfiable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult)
satWithAny = (`sbvWithAny` satWith)
-- | Find a satisfying assignment to a property using a single solver, but
-- providing several query problems of interest, with each query running in a
-- separate thread and return the first one that returns. This can be useful to
-- use symbolic mode to drive to a location in the search space of the solver
-- and then refine the problem in query mode. If the computation is very hard to
-- solve for the solver than running in concurrent mode may provide a large
-- performance benefit.
satConcurrentWithAny :: Satisfiable a => SMTConfig -> [Query b] -> a -> IO (Solver, NominalDiffTime, SatResult)
satConcurrentWithAny solver qs a = do (slvr,time,result) <- sbvConcurrentWithAny solver go qs a
pure (slvr, time, SatResult result)
where go cfg a' q = runWithQuery satArgReduce True (do _ <- q; checkNoOptimizations >> Control.getSMTResult) cfg a'
-- | Find a satisfying assignment to a property using a single solver, but run
-- each query problem in a separate isolated thread and wait for each thread to
-- finish. See 'satConcurrentWithAny' for more details.
satConcurrentWithAll :: Satisfiable a => SMTConfig -> [Query b] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
satConcurrentWithAll solver qs a = do results <- sbvConcurrentWithAll solver go qs a
pure $ (\(a',b,c) -> (a',b,SatResult c)) <$> results
where go cfg a' q = runWithQuery satArgReduce True (do _ <- q; checkNoOptimizations >> Control.getSMTResult) cfg a'
-- | A type @a@ is provable if we can turn it into a predicate, i.e., it has to return a boolean.
-- This class captures essentially prove calls.
class ExtractIO m => ProvableM m a where
-- | Reduce an arg, for proof purposes.
proofArgReduce :: a -> SymbolicT m SBool
-- | Generalization of 'Data.SBV.prove'
prove :: a -> m ThmResult
prove = proveWith defaultSMTCfg
-- | Generalization of 'Data.SBV.proveWith'
proveWith :: SMTConfig -> a -> m ThmResult
proveWith cfg a = do r <- runWithQuery proofArgReduce False (checkNoOptimizations >> Control.getSMTResult) cfg a
ThmResult <$> if validationRequested cfg
then validate proofArgReduce False cfg a r
else pure r
-- | Generalization of 'Data.SBV.dprove'
dprove :: a -> m ThmResult
dprove = dproveWith defaultDeltaSMTCfg
-- | Generalization of 'Data.SBV.dproveWith'
dproveWith :: SMTConfig -> a -> m ThmResult
dproveWith cfg a = do r <- runWithQuery proofArgReduce False (checkNoOptimizations >> Control.getSMTResult) cfg a
ThmResult <$> if validationRequested cfg
then validate proofArgReduce False cfg a r
else pure r
-- | Generalization of 'Data.SBV.isVacuousProof'
isVacuousProof :: a -> m Bool
isVacuousProof = isVacuousProofWith defaultSMTCfg
-- | Generalization of 'Data.SBV.isVacuousProofWith'
isVacuousProofWith :: SMTConfig -> a -> m Bool
isVacuousProofWith cfg a = -- NB. Can't call runWithQuery since last constraint would become the implication!
fst <$> runSymbolic cfg (SMTMode QueryInternal ISetup True cfg) (proofArgReduce a >> Control.executeQuery QueryInternal check)
where
check = do cs <- Control.checkSat
case cs of
Control.Unsat -> pure True
Control.Sat -> pure False
Control.DSat{} -> pure False
Control.Unk -> error "SBV: isVacuous: Solver returned unknown!"
-- | Generalization of 'Data.SBV.isTheorem'
isTheorem :: a -> m Bool
isTheorem = isTheoremWith defaultSMTCfg
-- | Generalization of 'Data.SBV.isTheoremWith'
isTheoremWith :: SMTConfig -> a -> m Bool
isTheoremWith cfg p = do r <- proveWith cfg p
let bad = error $ "SBV.isTheorem: Received:\n" ++ show r
case r of
ThmResult Unsatisfiable{} -> pure True
ThmResult Satisfiable{} -> pure False
ThmResult DeltaSat{} -> pure False
ThmResult SatExtField{} -> pure False
ThmResult Unknown{} -> bad
ThmResult ProofError{} -> bad
-- | Prove a property with multiple solvers, running them in separate threads. Only
-- the result of the first one to finish will be returned, remaining threads will be killed.
-- Note that we send an exception to the losing processes, but we do *not* actually wait for them
-- to finish. In rare cases this can lead to zombie processes. In previous experiments, we found
-- that some processes take their time to terminate. So, this solution favors quick turnaround.
proveWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, ThmResult)
proveWithAny = (`sbvWithAny` proveWith)
-- | Prove a property with multiple solvers, running them in separate threads. The
-- results will be returned in the order produced.
proveWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
proveWithAll = (`sbvWithAll` proveWith)
-- | Prove a property by running many queries each isolated to their own thread
-- concurrently and return the first that finishes, killing the others
proveConcurrentWithAny :: Provable a => SMTConfig -> [Query b] -> a -> IO (Solver, NominalDiffTime, ThmResult)
proveConcurrentWithAny solver qs a = do (slvr,time,result) <- sbvConcurrentWithAny solver go qs a
pure (slvr, time, ThmResult result)
where go cfg a' q = runWithQuery proofArgReduce False (do _ <- q; checkNoOptimizations >> Control.getSMTResult) cfg a'
-- | Prove a property by running many queries each isolated to their own thread
-- concurrently and wait for each to finish returning all results
proveConcurrentWithAll :: Provable a => SMTConfig -> [Query b] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
proveConcurrentWithAll solver qs a = do results <- sbvConcurrentWithAll solver go qs a
pure $ (\(a',b,c) -> (a',b,ThmResult c)) <$> results
where go cfg a' q = runWithQuery proofArgReduce False (do _ <- q; checkNoOptimizations >> Control.getSMTResult) cfg a'
-- | Validate a model obtained from the solver
validate :: MonadIO m => (a -> SymbolicT m SBool) -> Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
validate reducer isSAT cfg p res =
case res of
Unsatisfiable{} -> pure res
Satisfiable _ m -> case modelBindings m of
Nothing -> error "Data.SBV.validate: Impossible happened; no bindings generated during model validation."
Just env -> check env
DeltaSat {} -> cant [ "The model is delta-satisfiable."
, "Cannot validate delta-satisfiable models."
]
SatExtField{} -> cant [ "The model requires an extension field value."
, "Cannot validate models with infinities/epsilons produced during optimization."
, ""
, "To turn validation off, use `cfg{optimizeValidateConstraints = False}`"
]
Unknown{} -> pure res
ProofError{} -> pure res
where cant msg = pure $ ProofError cfg (msg ++ [ ""
, "Unable to validate the produced model."
]) (Just res)
check env = do let envShown = showModelDictionary True True cfg modelBinds
where modelBinds = [(T.unpack n, RegularCV v) | (NamedSymVar _ n, v) <- env]
notify s
| not (verbose cfg) = pure ()
| True = debug cfg ["[VALIDATE] " `alignPlain` T.pack s]
notify $ "Validating the model. " ++ if null env then "There are no assignments." else "Assignment:"
mapM_ notify [" " ++ l | l <- lines envShown]
result <- snd <$> runSymbolic cfg (Concrete (Just (isSAT, env))) (reducer p >>= output)
let explain = [ ""
, "Assignment:" ++ if null env then " <none>" else ""
]
++ [ "" | not (null env)]
++ [ " " ++ l | l <- lines envShown]
++ [ "" ]
wrap tag extras = pure $ ProofError cfg (tag : explain ++ extras) (Just res)
giveUp s = wrap ("Data.SBV: Cannot validate the model: " ++ 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 s = wrap ("Data.SBV: Model validation failure: " ++ 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 = wrap ("Data.SBV: Cannot validate the model, since " ++ show sv ++ " is not concretely computable.")
( perhaps (why sv)
)
where perhaps Nothing = case resObservables result of
[] -> []
xs -> [ "There are observable values in the model: " ++ unwords [show n | (n, _, _) <- xs]
, "SBV cannot validate in the presence of observables, unfortunately."
, "Try validation after removing calls to 'observe'."
]
perhaps (Just x) = [ x
, ""
, "SBV's model validator is incomplete, and cannot handle this particular case."
, "Please report this as a feature request or possibly a bug!"
]
-- This is incomplete, but should capture the most common cases
why s = case s `lookup` S.toList (pgmAssignments (resAsgns result)) of
Nothing -> Nothing
Just (SBVApp o as) -> case o of
QuantifiedBool{} -> Just "The value depends on a quantified variable."
IEEEFP FP_FMA -> Just "Floating point FMA operation is not supported concretely."
IEEEFP _ -> Just "Not all floating point operations are supported concretely."
OverflowOp _ -> Just "Overflow-checking is not done concretely."
Uninterpreted v
| any isADT as -> Just "Models containing ADTs are currently only partially supported."
| True -> Just $ "The value depends on the uninterpreted constant " ++ T.unpack v ++ "."
_ -> listToMaybe $ mapMaybe why as
cstrs = S.toList $ resConstraints result
walkConstraints [] cont = do
unless (null cstrs) $ notify "Validated all constraints."
cont
walkConstraints ((isSoft, attrs, sv) : rest) cont
| kindOf sv /= KBool
= giveUp $ "Constraint tied to " ++ show sv ++ " is non-boolean."
| isSoft || sv == trueSV
= walkConstraints rest cont
| sv == falseSV
= case mbName of
Just nm -> badModel $ "Named constraint " ++ show nm ++ " evaluated to False."
Nothing -> badModel "A constraint was violated."
| True
= notConcrete sv
where mbName = listToMaybe [n | (":named", n) <- attrs]
-- SAT: All outputs must be true
satLoop []
= do notify "All outputs are satisfied. Validation complete."
pure res
satLoop (sv:svs)
| kindOf sv /= KBool
= giveUp $ "Output tied to " ++ show sv ++ " is non-boolean."
| sv == trueSV
= satLoop svs
| sv == falseSV
= badModel "Final output evaluated to False."
| True
= notConcrete sv
-- Proof: At least one output must be false
proveLoop [] somethingFailed
| somethingFailed = do notify "Counterexample is validated."
pure res
| True = do notify "Counterexample violates none of the outputs."
badModel "Counter-example violates no constraints."
proveLoop (sv:svs) somethingFailed
| kindOf sv /= KBool
= giveUp $ "Output tied to " ++ show sv ++ " is non-boolean."
| sv == trueSV
= proveLoop svs somethingFailed
| sv == falseSV
= proveLoop svs True
| True
= notConcrete sv
-- Output checking is tricky, since we behave differently for different modes
checkOutputs []
| null cstrs
= giveUp "Impossible happened: There are no outputs nor any constraints to check."
checkOutputs os
= do notify "Validating outputs."
if isSAT then satLoop os
else proveLoop os False
notify $ if null cstrs
then "There are no constraints to check."
else "Validating " ++ show (length cstrs) ++ " constraint(s)."
walkConstraints cstrs (checkOutputs (resOutputs result))
-- | Given a satisfiability problem, extract the function definitions in it
defs2smt :: SatisfiableM m a => a -> m String
defs2smt = generateSMTBenchMarkGen True satArgReduce defs
where defs (SMTLibPgm _ _ ds) = T.unpack ds
-- | Create an SMT-Lib2 benchmark, for a SAT query.
generateSMTBenchmarkSat :: SatisfiableM m a => a -> m String
generateSMTBenchmarkSat = generateSMTBenchMarkGen True satArgReduce (\p -> show p ++ "\n(check-sat)\n")
-- | Create an SMT-Lib2 benchmark, for a Proof query.
generateSMTBenchmarkProof :: ProvableM m a => a -> m String
generateSMTBenchmarkProof = generateSMTBenchMarkGen False proofArgReduce (\p -> show p ++ "\n(check-sat)\n")
-- | Generic benchmark creator
generateSMTBenchMarkGen :: MonadIO m => Bool -> (a -> SymbolicT m SBool) -> (SMTLibPgm -> b) -> a -> m b
generateSMTBenchMarkGen isSat reduce render a = do
t <- liftIO getZonedTime
let comments = ["Automatically created by SBV on " ++ show t]
cfg = defaultSMTCfg { smtLibVersion = SMTLib2 }
(_, res) <- runSymbolic cfg (SMTMode QueryInternal ISetup isSat cfg) $ reduce a >>= output
let SMTProblem{smtLibPgm} = Control.runProofOn (SMTMode QueryInternal IRun isSat cfg) QueryInternal comments res
pure $ render (smtLibPgm cfg)
checkNoOptimizations :: MonadIO m => QueryT m ()
checkNoOptimizations = do objectives <- Control.getObjectives
unless (null objectives) $
error $ unlines [ ""
, "*** Data.SBV: Unsupported call sat/prove when optimization objectives are present."
, "*** Use \"optimize\"/\"optimizeWith\" to calculate optimal satisfaction!"
]
instance ExtractIO m => SatisfiableM m (SymbolicT m ()) where satArgReduce a = satArgReduce ((a >> pure sTrue) :: SymbolicT m SBool)
-- instance ExtractIO m => ProvableM m (SymbolicT m ()) -- NO INSTANCE ON PURPOSE; don't want to prove goals
instance ExtractIO m => SatisfiableM m (SymbolicT m SBool) where satArgReduce = id
instance ExtractIO m => ProvableM m (SymbolicT m SBool) where proofArgReduce = id
instance ExtractIO m => SatisfiableM m SBool where satArgReduce = pure
instance ExtractIO m => ProvableM m SBool where proofArgReduce = pure
instance {-# OVERLAPPABLE #-} (ExtractIO m, SatisfiableM m a) => SatisfiableM m (SymbolicT m a) where satArgReduce a = a >>= satArgReduce
instance {-# OVERLAPPABLE #-} (ExtractIO m, ProvableM m a) => ProvableM m (SymbolicT m a) where proofArgReduce a = a >>= proofArgReduce
instance (ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r) => SatisfiableM m (Forall nm a -> r) where
satArgReduce = satArgReduce . quantifiedBool
instance (ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r) => ProvableM m (Forall nm a -> r) where
proofArgReduce = proofArgReduce . quantifiedBool
instance (ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r) => SatisfiableM m (Exists nm a -> r) where
satArgReduce = satArgReduce . quantifiedBool
instance (ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r, EqSymbolic (SBV a)) => SatisfiableM m (ExistsUnique nm a -> r) where
satArgReduce = satArgReduce . quantifiedBool
instance (KnownNat n, ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r) => ProvableM m (ForallN n nm a -> r) where
proofArgReduce = proofArgReduce . quantifiedBool
instance (KnownNat n, ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r) => SatisfiableM m (ExistsN n nm a -> r) where
satArgReduce = satArgReduce . quantifiedBool
instance (ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r) => ProvableM m (Exists nm a -> r) where
proofArgReduce = proofArgReduce . quantifiedBool
instance (ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r, EqSymbolic (SBV a)) => ProvableM m (ExistsUnique nm a -> r) where
proofArgReduce = proofArgReduce . quantifiedBool
instance (KnownNat n, ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r) => SatisfiableM m (ForallN n nm a -> r) where
satArgReduce = satArgReduce . quantifiedBool
instance (KnownNat n, ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r) => ProvableM m (ExistsN n nm a -> r) where
proofArgReduce = proofArgReduce . quantifiedBool
{-
-- The following is a possible definition, but it lets us write properties that
-- are not useful.. Such as: prove $ \x y -> (x::SInt8) == y
-- Running that will throw an exception since Haskell's equality is not be supported by symbolic things. (Needs .==).
-- So, we avoid these insteances.
instance ExtractIO m => ProvableM m Bool where
proofArgReduce x = proofArgReduce (if x then sTrue else sFalse :: SBool)
instance ExtractIO m => SatisfiableM m Bool where
satArgReduce x = satArgReduce (if x then sTrue else sFalse :: SBool)
-}
-- | Create an argument
mkArg :: (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg = mkSymVal (NonQueryVar Nothing) Nothing
-- Functions
instance (SymVal a, SatisfiableM m p) => SatisfiableM m (SBV a -> p) where
satArgReduce fn = mkArg >>= \a -> satArgReduce $ fn a
instance (SymVal a, ProvableM m p) => ProvableM m (SBV a -> p) where
proofArgReduce fn = mkArg >>= \a -> proofArgReduce $ fn a
-- | Create an 'SBVs' sequence of arguments
mkArgs :: MonadSymbolic m => SymValInsts as -> m (SBVs as)
mkArgs SymValsNil = pure SBVsNil
mkArgs (SymValsCons insts) = SBVsCons <$> mkArgs insts <*> mkArg
-- Multi-arity Functions
instance (SymVals as, SatisfiableM m p) => SatisfiableM m (SBVs as -> p) where
satArgReduce fn = mkArgs symValInsts >>= \args -> satArgReduce $ fn args
instance (SymVals as, ProvableM m p) => ProvableM m (SBVs as -> p) where
proofArgReduce fn = mkArgs symValInsts >>= \args -> proofArgReduce $ fn args
-- 2 Tuple
instance (SymVal a, SymVal b, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b) -> p) where
satArgReduce fn = mkArg >>= \a -> satArgReduce $ \b -> fn (a, b)
instance (SymVal a, SymVal b, ProvableM m p) => ProvableM m ((SBV a, SBV b) -> p) where
proofArgReduce fn = mkArg >>= \a -> proofArgReduce $ \b -> fn (a, b)
-- 3 Tuple
instance (SymVal a, SymVal b, SymVal c, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c) -> p) where
satArgReduce fn = mkArg >>= \a -> satArgReduce $ \b c -> fn (a, b, c)
instance (SymVal a, SymVal b, SymVal c, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c) -> p) where
proofArgReduce fn = mkArg >>= \a -> proofArgReduce $ \b c -> fn (a, b, c)
-- 4 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d) -> p) where
satArgReduce fn = mkArg >>= \a -> satArgReduce $ \b c d -> fn (a, b, c, d)
instance (SymVal a, SymVal b, SymVal c, SymVal d, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d) -> p) where
proofArgReduce fn = mkArg >>= \a -> proofArgReduce $ \b c d -> fn (a, b, c, d)
-- 5 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) where
satArgReduce fn = mkArg >>= \a -> satArgReduce $ \b c d e -> fn (a, b, c, d, e)
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) where
proofArgReduce fn = mkArg >>= \a -> proofArgReduce $ \b c d e -> fn (a, b, c, d, e)
-- 6 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) where
satArgReduce fn = mkArg >>= \a -> satArgReduce $ \b c d e f -> fn (a, b, c, d, e, f)
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) where
proofArgReduce fn = mkArg >>= \a -> proofArgReduce $ \b c d e f -> fn (a, b, c, d, e, f)
-- 7 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) where
satArgReduce fn = mkArg >>= \a -> satArgReduce $ \b c d e f g -> fn (a, b, c, d, e, f, g)
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) where
proofArgReduce fn = mkArg >>= \a -> proofArgReduce $ \b c d e f g -> fn (a, b, c, d, e, f, g)
-- 8 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) where
satArgReduce fn = mkArg >>= \a -> satArgReduce $ \b c d e f g h -> fn (a, b, c, d, e, f, g, h)
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) where
proofArgReduce fn = mkArg >>= \a -> proofArgReduce $ \b c d e f g h -> fn (a, b, c, d, e, f, g, h)
-- 9 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) where
satArgReduce fn = mkArg >>= \a -> satArgReduce $ \b c d e f g h i -> fn (a, b, c, d, e, f, g, h, i)
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) where
proofArgReduce fn = mkArg >>= \a -> proofArgReduce $ \b c d e f g h i -> fn (a, b, c, d, e, f, g, h, i)
-- 10 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SymVal j, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) where
satArgReduce fn = mkArg >>= \a -> satArgReduce $ \b c d e f g h i j -> fn (a, b, c, d, e, f, g, h, i, j)
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SymVal j, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) where
proofArgReduce fn = mkArg >>= \a -> proofArgReduce $ \b c d e f g h i j -> fn (a, b, c, d, e, f, g, h, i, j)
-- 11 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SymVal j, SymVal k, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) where
satArgReduce fn = mkArg >>= \a -> satArgReduce $ \b c d e f g h i j k -> fn (a, b, c, d, e, f, g, h, i, j, k)
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SymVal j, SymVal k, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) where
proofArgReduce fn = mkArg >>= \a -> proofArgReduce $ \b c d e f g h i j k -> fn (a, b, c, d, e, f, g, h, i, j, k)
-- 12 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SymVal j, SymVal k, SymVal l, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) where
satArgReduce fn = mkArg >>= \a -> satArgReduce $ \b c d e f g h i j k l -> fn (a, b, c, d, e, f, g, h, i, j, k, l)
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SymVal j, SymVal k, SymVal l, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) where
proofArgReduce fn = mkArg >>= \a -> proofArgReduce $ \b c d e f g h i j k l -> fn (a, b, c, d, e, f, g, h, i, j, k, l)
-- | Generalization of 'Data.SBV.runSMT'
runSMT :: MonadIO m => SymbolicT m a -> m a
runSMT = runSMTWith defaultSMTCfg
-- | Generalization of 'Data.SBV.runSMTWith'
runSMTWith :: MonadIO m => SMTConfig -> SymbolicT m a -> m a
runSMTWith cfg a = fst <$> runSymbolic cfg (SMTMode QueryExternal ISetup True cfg) a
-- | Runs with a query.
runWithQuery :: ExtractIO m => (a -> SymbolicT m SBool) -> Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery reducer isSAT q cfg a = fst <$> runSymbolic cfg (SMTMode QueryInternal ISetup isSAT cfg) comp
where comp = do _ <- reducer a >>= output
Control.executeQuery QueryInternal q
-- | Check if a safe-call was safe or not, turning a t'SafeResult' to a Bool.
isSafe :: SafeResult -> Bool
isSafe (SafeResult (_, _, result)) = case result of
Unsatisfiable{} -> True
Satisfiable{} -> False
DeltaSat{} -> False -- conservative
SatExtField{} -> False -- conservative
Unknown{} -> False -- conservative
ProofError{} -> False -- conservative
-- | Perform an action asynchronously, returning results together with diff-time.
runInThread :: NFData b => UTCTime -> (SMTConfig -> IO b) -> SMTConfig -> IO (Async (Solver, NominalDiffTime, b))
runInThread beginTime action config = async $ do
result <- action config
endTime <- rnf result `seq` getCurrentTime
pure (name (solver config), endTime `diffUTCTime` beginTime, result)
-- | Perform action for all given configs, return the first one that wins. Note that we do
-- not wait for the other asyncs to terminate; hopefully they'll do so quickly.
sbvWithAny :: NFData b => [SMTConfig] -> (SMTConfig -> a -> IO b) -> a -> IO (Solver, NominalDiffTime, b)
sbvWithAny [] _ _ = error "SBV.withAny: No solvers given!"
sbvWithAny solvers what a = do beginTime <- getCurrentTime
snd <$> (mapM (runInThread beginTime (`what` a)) solvers >>= waitAnyFastCancel)
where -- Async's `waitAnyCancel` nicely blocks; so we use this variant to ignore the
-- wait part for killed threads.
waitAnyFastCancel asyncs = waitAny asyncs `finally` mapM_ cancelFast asyncs
cancelFast other = throwTo (asyncThreadId other) ExitSuccess
sbvConcurrentWithAny :: NFData c => SMTConfig -> (SMTConfig -> a -> QueryT m b -> IO c) -> [QueryT m b] -> a -> IO (Solver, NominalDiffTime, c)
sbvConcurrentWithAny solver what queries a = snd <$> (mapM runQueryInThread queries >>= waitAnyFastCancel)
where -- Async's `waitAnyCancel` nicely blocks; so we use this variant to ignore the
-- wait part for killed threads.
waitAnyFastCancel asyncs = waitAny asyncs `finally` mapM_ cancelFast asyncs
cancelFast other = throwTo (asyncThreadId other) ExitSuccess
runQueryInThread q = do beginTime <- getCurrentTime
runInThread beginTime (\cfg -> what cfg a q) solver
sbvConcurrentWithAll :: NFData c => SMTConfig -> (SMTConfig -> a -> QueryT m b -> IO c) -> [QueryT m b] -> a -> IO [(Solver, NominalDiffTime, c)]
sbvConcurrentWithAll solver what queries a = mapConcurrently runQueryInThread queries >>= unsafeInterleaveIO . go
where runQueryInThread q = do beginTime <- getCurrentTime
runInThread beginTime (\cfg -> what cfg a q) solver
go [] = pure []
go as = do (d, r) <- waitAny as
-- The following filter works because the Eq instance on Async
-- checks the thread-id; so we know that we're removing the
-- correct solver from the list. This also allows for
-- running the same-solver (with different options), since
-- they will get different thread-ids.
rs <- unsafeInterleaveIO $ go (filter (/= d) as)
pure (r : rs)
-- | Perform action for all given configs, return all the results.
sbvWithAll :: NFData b => [SMTConfig] -> (SMTConfig -> a -> IO b) -> a -> IO [(Solver, NominalDiffTime, b)]
sbvWithAll solvers what a = do beginTime <- getCurrentTime
mapM (runInThread beginTime (`what` a)) solvers >>= (unsafeInterleaveIO . go)
where go [] = pure []
go as = do (d, r) <- waitAny as
-- The following filter works because the Eq instance on Async
-- checks the thread-id; so we know that we're removing the
-- correct solver from the list. This also allows for
-- running the same-solver (with different options), since
-- they will get different thread-ids.
rs <- unsafeInterleaveIO $ go (filter (/= d) as)
pure (r : rs)
-- | Symbolically executable program fragments. This class is mainly used for 'safe' calls, and is sufficiently populated internally to cover most use
-- cases. Users can extend it as they wish to allow 'safe' checks for SBV programs that return/take types that are user-defined.
class ExtractIO m => SExecutable m a where
-- | Generalization of 'Data.SBV.sName'
sName :: a -> SymbolicT m ()
-- | Generalization of 'Data.SBV.safe'
safe :: a -> m [SafeResult]
safe = safeWith defaultSMTCfg
-- | Generalization of 'Data.SBV.safeWith'
safeWith :: SMTConfig -> a -> m [SafeResult]
safeWith cfg a = do cwd <- (++ "/") <$> liftIO getCurrentDirectory
let mkRelative path
| cwd `isPrefixOf` path = drop (length cwd) path
| True = path
fst <$> runSymbolic cfg (SMTMode QueryInternal ISafe True cfg) (sName a >> check mkRelative)
where check :: (FilePath -> FilePath) -> SymbolicT m [SafeResult]
check mkRelative = Control.executeQuery QueryInternal $ Control.getSBVAssertions >>= mapM (verify mkRelative)
-- check that the cond is unsatisfiable. If satisfiable, that would
-- indicate the assignment under which the 'Data.SBV.sAssert' would fail
verify :: (FilePath -> FilePath) -> (String, Maybe CallStack, SV) -> QueryT m SafeResult
verify mkRelative (msg, cs, cond) = do
let locInfo ps = let loc (f, sl) = concat [mkRelative (srcLocFile sl), ":", show (srcLocStartLine sl), ":", show (srcLocStartCol sl), ":", f]
in intercalate ",\n " (map loc ps)
location = locInfo . getCallStack <$> cs
result <- do Control.push 1
Control.send True $ "(assert " <> showText cond <> ")"
r <- Control.getSMTResult
Control.pop 1
pure r
pure $ SafeResult (location, msg, result)
instance (ExtractIO m, NFData a) => SExecutable m (SymbolicT m a) where
sName a = a >>= \r -> rnf r `seq` pure ()
instance ExtractIO m => SExecutable m (SBV a) where
sName v = sName (output v :: SymbolicT m (SBV a))
-- Unit output
instance ExtractIO m => SExecutable m () where
sName () = sName (output () :: SymbolicT m ())
-- List output
instance ExtractIO m => SExecutable m [SBV a] where
sName vs = sName (output vs :: SymbolicT m [SBV a])
-- 2 Tuple output
instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b) => SExecutable m (SBV a, SBV b) where
sName (a, b) = sName (output a >> output b :: SymbolicT m (SBV b))
-- 3 Tuple output
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 (a, b, c) = sName (output a >> output b >> output c :: SymbolicT m (SBV c))
-- 4 Tuple output
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 (a, b, c, d) = sName (output a >> output b >> output c >> output c >> output d :: SymbolicT m (SBV d))
-- 5 Tuple output
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 (a, b, c, d, e) = sName (output a >> output b >> output c >> output d >> output e :: SymbolicT m (SBV e))
-- 6 Tuple output
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 (a, b, c, d, e, f) = sName (output a >> output b >> output c >> output d >> output e >> output f :: SymbolicT m (SBV f))
-- 7 Tuple output
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 (a, b, c, d, e, f, g) = sName (output a >> output b >> output c >> output d >> output e >> output f >> output g :: SymbolicT m (SBV g))
-- Functions
instance (SymVal a, SExecutable m p) => SExecutable m (SBV a -> p) where
sName k = mkArg >>= \a -> sName $ k a
-- 2 Tuple input
instance (SymVal a, SymVal b, SExecutable m p) => SExecutable m ((SBV a, SBV b) -> p) where
sName k = mkArg >>= \a -> sName $ \b -> k (a, b)
-- 3 Tuple input
instance (SymVal a, SymVal b, SymVal c, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c) -> p) where
sName k = mkArg >>= \a -> sName $ \b c -> k (a, b, c)
-- 4 Tuple input
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 k = mkArg >>= \a -> sName $ \b c d -> k (a, b, c, d)
-- 5 Tuple input
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 k = mkArg >>= \a -> sName $ \b c d e -> k (a, b, c, d, e)
-- 6 Tuple input
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 k = mkArg >>= \a -> sName $ \b c d e f -> k (a, b, c, d, e, f)
-- 7 Tuple input
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 k = mkArg >>= \a -> sName $ \b c d e f g -> k (a, b, c, d, e, f, g)
{- HLint ignore module "Reduce duplication" -}