-----------------------------------------------------------------------------
-- |
-- 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 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
       , satConcurrentWithAny, satConcurrentWithAll, proveConcurrentWithAny, proveConcurrentWithAll
       , generateSMTBenchmark
       , Goal
       , ThmResult(..), SatResult(..), AllSatResult(..), SafeResult(..), OptimizeResult(..), SMTResult(..)
       , SExecutable(..), isSafe
       , runSMT, runSMTWith
       , SatModel(..), Modelable(..), displayModels, extractModels
       , getModelDictionaries, getModelValues, getModelUninterpretedValues
       , abc, boolector, bitwuzla, cvc4, cvc5, dReal, mathSAT, yices, z3, defaultSMTCfg, defaultDeltaSMTCfg
       ) 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, 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, nub)

import Data.Maybe (mapMaybe, listToMaybe)

import qualified Data.Map.Strict as M
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.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.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

mkConfig :: SMTSolver -> SMTLibVersion -> [Control.SMTOption] -> SMTConfig
mkConfig :: SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
s SMTLibVersion
smtVersion [SMTOption]
startOpts = SMTConfig { verbose :: Bool
verbose                     = Bool
False
                                            , timing :: Timing
timing                      = Timing
NoTiming
                                            , printBase :: Int
printBase                   = Int
10
                                            , printRealPrec :: Int
printRealPrec               = Int
16
                                            , crackNum :: Bool
crackNum                    = Bool
False
                                            , transcript :: Maybe FilePath
transcript                  = forall a. Maybe a
Nothing
                                            , solver :: SMTSolver
solver                      = SMTSolver
s
                                            , smtLibVersion :: SMTLibVersion
smtLibVersion               = SMTLibVersion
smtVersion
                                            , dsatPrecision :: Maybe Double
dsatPrecision               = forall a. Maybe a
Nothing
                                            , extraArgs :: [FilePath]
extraArgs                   = []
                                            , satCmd :: FilePath
satCmd                      = FilePath
"(check-sat)"
                                            , satTrackUFs :: Bool
satTrackUFs                 = Bool
True                   -- i.e., yes, do extract UI function values
                                            , allSatMaxModelCount :: Maybe Int
allSatMaxModelCount         = forall a. Maybe a
Nothing                -- i.e., return all satisfying models
                                            , allSatPrintAlong :: Bool
allSatPrintAlong            = Bool
False                  -- i.e., do not print models as they are found
                                            , isNonModelVar :: FilePath -> Bool
isNonModelVar               = forall a b. a -> b -> a
const Bool
False            -- i.e., everything is a model-variable by default
                                            , 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 FilePath
redirectVerbose             = forall a. Maybe a
Nothing
                                            }

-- | If supported, this makes all output go to stdout, which works better with SBV
-- Alas, not all solvers support it..
allOnStdOut :: Control.SMTOption
allOnStdOut :: SMTOption
allOnStdOut = FilePath -> SMTOption
Control.DiagnosticOutputChannel FilePath
"stdout"

-- | Default configuration for the ABC synthesis and verification tool.
abc :: SMTConfig
abc :: SMTConfig
abc = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
ABC.abc SMTLibVersion
SMTLib2 [SMTOption
allOnStdOut]

-- | Default configuration for the Boolector SMT solver
boolector :: SMTConfig
boolector :: SMTConfig
boolector = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
Boolector.boolector SMTLibVersion
SMTLib2 []

-- | Default configuration for the Bitwuzla SMT solver
bitwuzla :: SMTConfig
bitwuzla :: SMTConfig
bitwuzla = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
Bitwuzla.bitwuzla SMTLibVersion
SMTLib2 []

-- | Default configuration for the CVC4 SMT Solver.
cvc4 :: SMTConfig
cvc4 :: SMTConfig
cvc4 = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
CVC4.cvc4 SMTLibVersion
SMTLib2 [SMTOption
allOnStdOut]

-- | Default configuration for the CVC5 SMT Solver.
cvc5 :: SMTConfig
cvc5 :: SMTConfig
cvc5 = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
CVC5.cvc5 SMTLibVersion
SMTLib2 [SMTOption
allOnStdOut]

-- | Default configuration for the Yices SMT Solver.
dReal :: SMTConfig
dReal :: SMTConfig
dReal = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
DReal.dReal SMTLibVersion
SMTLib2 [ FilePath -> [FilePath] -> SMTOption
Control.OptionKeyword FilePath
":smtlib2_compliant" [FilePath
"true"]
                                     ]

-- | Default configuration for the MathSAT SMT solver
mathSAT :: SMTConfig
mathSAT :: SMTConfig
mathSAT = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
MathSAT.mathSAT SMTLibVersion
SMTLib2 [SMTOption
allOnStdOut]

-- | Default configuration for the Yices SMT Solver.
yices :: SMTConfig
yices :: SMTConfig
yices = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
Yices.yices SMTLibVersion
SMTLib2 []

-- | Default configuration for the Z3 SMT solver
z3 :: SMTConfig
z3 :: SMTConfig
z3 = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
Z3.z3 SMTLibVersion
SMTLib2 [ FilePath -> [FilePath] -> SMTOption
Control.OptionKeyword FilePath
":smtlib2_compliant" [FilePath
"true"]
                            , SMTOption
allOnStdOut
                            ]

-- | The default solver used by SBV. This is currently set to z3.
defaultSMTCfg :: SMTConfig
defaultSMTCfg :: SMTConfig
defaultSMTCfg = SMTConfig
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 :: SMTConfig
defaultDeltaSMTCfg = SMTConfig
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 goal is a symbolic program that returns no values. The idea is that the constraints/min-max
-- goals will serve as appropriate directives for sat/prove calls.
type Goal = Symbolic ()

-- | A type @a@ is provable if we can turn it into a predicate.
-- Note that a predicate can be made from a curried function of arbitrary arity, where
-- each element is either a symbolic type or up-to a 7-tuple of symbolic-types. So
-- predicates can be constructed from almost arbitrary Haskell functions that have arbitrary
-- shapes. (See the instance declarations below.)
class ExtractIO m => MProvable m a where
  -- | Generalization of 'Data.SBV.universal_'
  universal_ :: a -> SymbolicT m SBool

  -- | Generalization of 'Data.SBV.universal'
  universal  :: [String] -> a -> SymbolicT m SBool

  -- | Generalization of 'Data.SBV.existential_'
  existential_ :: a -> SymbolicT m SBool

  -- | Generalization of 'Data.SBV.existential'
  existential :: [String] -> a -> SymbolicT m SBool

  -- | Generalization of 'Data.SBV.prove'
  prove :: a -> m ThmResult
  prove = forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m ThmResult
proveWith SMTConfig
defaultSMTCfg

  -- | Generalization of 'Data.SBV.proveWith'
  proveWith :: SMTConfig -> a -> m ThmResult
  proveWith SMTConfig
cfg a
a = do SMTResult
r <- forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
False (forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
Control.getSMTResult) SMTConfig
cfg a
a
                       SMTResult -> ThmResult
ThmResult forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> if SMTConfig -> Bool
validationRequested SMTConfig
cfg
                                     then forall (m :: * -> *) a.
MProvable m a =>
Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
validate Bool
False SMTConfig
cfg a
a SMTResult
r
                                     else forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
r

  -- | Generalization of 'Data.SBV.dprove'
  dprove :: a -> m ThmResult
  dprove = forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m ThmResult
dproveWith SMTConfig
defaultDeltaSMTCfg

  -- | Generalization of 'Data.SBV.dproveWith'
  dproveWith :: SMTConfig -> a -> m ThmResult
  dproveWith SMTConfig
cfg a
a = do SMTResult
r <- forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
False (forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
Control.getSMTResult) SMTConfig
cfg a
a
                        SMTResult -> ThmResult
ThmResult forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> if SMTConfig -> Bool
validationRequested SMTConfig
cfg
                                      then forall (m :: * -> *) a.
MProvable m a =>
Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
validate Bool
False SMTConfig
cfg a
a SMTResult
r
                                      else forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
r

  -- | Generalization of 'Data.SBV.sat'
  sat :: a -> m SatResult
  sat = forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m SatResult
satWith SMTConfig
defaultSMTCfg

  -- | Generalization of 'Data.SBV.satWith'
  satWith :: SMTConfig -> a -> m SatResult
  satWith SMTConfig
cfg a
a = do SMTResult
r <- forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
True (forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
Control.getSMTResult) SMTConfig
cfg a
a
                     SMTResult -> SatResult
SatResult forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> if SMTConfig -> Bool
validationRequested SMTConfig
cfg
                                   then forall (m :: * -> *) a.
MProvable m a =>
Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
validate Bool
True SMTConfig
cfg a
a SMTResult
r
                                   else forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
r

  -- | Generalization of 'Data.SBV.sat'
  dsat :: a -> m SatResult
  dsat = forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m SatResult
dsatWith SMTConfig
defaultDeltaSMTCfg

  -- | Generalization of 'Data.SBV.satWith'
  dsatWith :: SMTConfig -> a -> m SatResult
  dsatWith SMTConfig
cfg a
a = do SMTResult
r <- forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
True (forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
Control.getSMTResult) SMTConfig
cfg a
a
                      SMTResult -> SatResult
SatResult forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> if SMTConfig -> Bool
validationRequested SMTConfig
cfg
                                    then forall (m :: * -> *) a.
MProvable m a =>
Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
validate Bool
True SMTConfig
cfg a
a SMTResult
r
                                    else forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
r

  -- | Generalization of 'Data.SBV.allSat'
  allSat :: a -> m AllSatResult
  allSat = forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m AllSatResult
allSatWith SMTConfig
defaultSMTCfg

  -- | Generalization of 'Data.SBV.allSatWith'
  allSatWith :: SMTConfig -> a -> m AllSatResult
  allSatWith SMTConfig
cfg a
a = do AllSatResult
asr <- forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
True (forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *).
(MonadIO m, MonadQuery m, SolverContext m) =>
m AllSatResult
Control.getAllSatResult) SMTConfig
cfg a
a
                        if SMTConfig -> Bool
validationRequested SMTConfig
cfg
                           then do [SMTResult]
rs' <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (m :: * -> *) a.
MProvable m a =>
Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
validate Bool
True SMTConfig
cfg a
a) (AllSatResult -> [SMTResult]
allSatResults AllSatResult
asr)
                                   forall (m :: * -> *) a. Monad m => a -> m a
return AllSatResult
asr{allSatResults :: [SMTResult]
allSatResults = [SMTResult]
rs'}
                           else forall (m :: * -> *) a. Monad m => a -> m a
return AllSatResult
asr

  -- | Generalization of 'Data.SBV.optimize'
  optimize :: OptimizeStyle -> a -> m OptimizeResult
  optimize = forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> OptimizeStyle -> a -> m OptimizeResult
optimizeWith SMTConfig
defaultSMTCfg

  -- | Generalization of 'Data.SBV.optimizeWith'
  optimizeWith :: SMTConfig -> OptimizeStyle -> a -> m OptimizeResult
  optimizeWith SMTConfig
config OptimizeStyle
style a
optGoal = do
                   OptimizeResult
res <- 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 forall (m :: * -> *) a. Monad m => a -> m a
return OptimizeResult
res
                      else let v :: SMTResult -> m SMTResult
                               v :: SMTResult -> m SMTResult
v = 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 SMTResult
m -> SMTResult -> OptimizeResult
LexicographicResult forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SMTResult -> m SMTResult
v SMTResult
m
                                IndependentResult [(FilePath, SMTResult)]
xs  -> let w :: [(a, SMTResult)] -> [(a, SMTResult)] -> m [(a, SMTResult)]
w []            [(a, SMTResult)]
sofar = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. [a] -> [a]
reverse [(a, SMTResult)]
sofar)
                                                             w ((a
n, SMTResult
m):[(a, SMTResult)]
rest) [(a, SMTResult)]
sofar = SMTResult -> m SMTResult
v SMTResult
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SMTResult
m' -> [(a, SMTResult)] -> [(a, SMTResult)] -> m [(a, SMTResult)]
w [(a, SMTResult)]
rest ((a
n, SMTResult
m') forall a. a -> [a] -> [a]
: [(a, SMTResult)]
sofar)
                                                         in [(FilePath, SMTResult)] -> OptimizeResult
IndependentResult forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {a}.
[(a, SMTResult)] -> [(a, SMTResult)] -> m [(a, SMTResult)]
w [(FilePath, SMTResult)]
xs []
                                ParetoResult (Bool
b, [SMTResult]
rs)  -> (Bool, [SMTResult]) -> OptimizeResult
ParetoResult forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool
b, ) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [Objective (SV, SV)]
Control.getObjectives
                   UserInputs
qinps      <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m UserInputs
Control.getQuantifiedInputs
                   SBVPgm
spgm       <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SBVPgm
Control.getSBVPgm

                   forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Objective (SV, SV)]
objectives) forall a b. (a -> b) -> a -> b
$
                          forall a. HasCallStack => FilePath -> a
error forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines [ FilePath
""
                                          , FilePath
"*** Data.SBV: Unsupported call to optimize when no objectives are present."
                                          , FilePath
"*** Use \"sat\" for plain satisfaction"
                                          ]

                   forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (SolverCapabilities -> Bool
supportsOptimization (SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
config))) forall a b. (a -> b) -> a -> b
$
                          forall a. HasCallStack => FilePath -> a
error forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines [ FilePath
""
                                          , FilePath
"*** Data.SBV: The backend solver " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show (SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
config)) forall a. [a] -> [a] -> [a]
++ FilePath
"does not support optimization goals."
                                          , FilePath
"*** Please use a solver that has support, such as z3"
                                          ]

                   forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SMTConfig -> Bool
validateModel SMTConfig
config Bool -> Bool -> Bool
&& Bool -> Bool
not (SMTConfig -> Bool
optimizeValidateConstraints SMTConfig
config)) forall a b. (a -> b) -> a -> b
$
                          forall a. HasCallStack => FilePath -> a
error forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines [ FilePath
""
                                          , FilePath
"*** Data.SBV: Model validation is not supported in optimization calls."
                                          , FilePath
"***"
                                          , FilePath
"*** Instead, use `cfg{optimizeValidateConstraints = True}`"
                                          , FilePath
"***"
                                          , FilePath
"*** which checks that the results satisfy the constraints but does"
                                          , FilePath
"*** NOT ensure that they are optimal."
                                          ]


                   let universals :: [NamedSymVar]
universals = forall (t :: * -> *) a. Foldable t => t a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ UserInputs -> Seq NamedSymVar
getUniversals UserInputs
qinps

                       firstUniversal :: NodeId
firstUniversal
                         | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedSymVar]
universals = forall a. HasCallStack => FilePath -> a
error FilePath
"Data.SBV: Impossible happened! Universal optimization with no universals!"
                         | Bool
True            = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SV -> NodeId
swNodeId forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedSymVar -> SV
getSV) [NamedSymVar]
universals

                       mappings :: M.Map SV SBVExpr
                       mappings :: Map SV SBVExpr
mappings = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (forall (t :: * -> *) a. Foldable t => t a -> [a]
S.toList (SBVPgm -> Seq (SV, SBVExpr)
pgmAssignments SBVPgm
spgm))

                       chaseUniversal :: SV -> [NamedSymVar]
chaseUniversal SV
entry = SV -> [NamedSymVar] -> [NamedSymVar]
go SV
entry []
                         where go :: SV -> [NamedSymVar] -> [NamedSymVar]
go SV
x [NamedSymVar]
sofar
                                | NodeId
nx forall a. Ord a => a -> a -> Bool
>= NodeId
firstUniversal
                                = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ [NamedSymVar
unm | NamedSymVar
unm <- [NamedSymVar]
universals, NodeId
nx forall a. Ord a => a -> a -> Bool
>= SV -> NodeId
swNodeId (NamedSymVar -> SV
getSV NamedSymVar
unm)] forall a. [a] -> [a] -> [a]
++ [NamedSymVar]
sofar
                                | Bool
True
                                = let oVars :: Op -> [SV]
oVars (LkUp (Int, Kind, Kind, Int)
_ SV
a SV
b)             = [SV
a, SV
b]
                                      oVars (IEEEFP (FP_Cast Kind
_ Kind
_ SV
o)) = [SV
o]
                                      oVars Op
_                        = []
                                      vars :: [SV]
vars = case SV
x forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map SV SBVExpr
mappings of
                                               Maybe SBVExpr
Nothing            -> []
                                               Just (SBVApp Op
o [SV]
ss) -> forall a. Eq a => [a] -> [a]
nub (Op -> [SV]
oVars Op
o forall a. [a] -> [a] -> [a]
++ [SV]
ss)
                                  in 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
swNodeId SV
x

                   let needsUniversalOpt :: [(FilePath, [NamedSymVar])]
needsUniversalOpt = let tag :: a -> [a] -> Maybe (a, [a])
tag a
_  [] = forall a. Maybe a
Nothing
                                               tag a
nm [a]
xs = forall a. a -> Maybe a
Just (a
nm, [a]
xs)
                                               needsUniversal :: Objective (SV, b) -> Maybe (FilePath, [NamedSymVar])
needsUniversal (Maximize          FilePath
nm (SV
x, b
_))   = forall {a} {a}. a -> [a] -> Maybe (a, [a])
tag FilePath
nm (SV -> [NamedSymVar]
chaseUniversal SV
x)
                                               needsUniversal (Minimize          FilePath
nm (SV
x, b
_))   = forall {a} {a}. a -> [a] -> Maybe (a, [a])
tag FilePath
nm (SV -> [NamedSymVar]
chaseUniversal SV
x)
                                               needsUniversal (AssertWithPenalty FilePath
nm (SV
x, b
_) Penalty
_) = forall {a} {a}. a -> [a] -> Maybe (a, [a])
tag FilePath
nm (SV -> [NamedSymVar]
chaseUniversal SV
x)
                                           in forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe forall {b}. Objective (SV, b) -> Maybe (FilePath, [NamedSymVar])
needsUniversal [Objective (SV, SV)]
objectives

                   forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedSymVar]
universals Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(FilePath, [NamedSymVar])]
needsUniversalOpt) forall a b. (a -> b) -> a -> b
$
                          let len :: Int
len = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum forall a b. (a -> b) -> a -> b
$ Int
0 forall a. a -> [a] -> [a]
: [forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
nm | (FilePath
nm, [NamedSymVar]
_) <- [(FilePath, [NamedSymVar])]
needsUniversalOpt]
                              pad :: FilePath -> FilePath
pad FilePath
n = FilePath
n forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate (Int
len forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
n) Char
' '
                          in forall a. HasCallStack => FilePath -> a
error forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines forall a b. (a -> b) -> a -> b
$ [ FilePath
""
                                               , FilePath
"*** Data.SBV: Problem needs optimization of metric in the scope of universally quantified variable(s):"
                                               , FilePath
"***"
                                               ]
                                           forall a. [a] -> [a] -> [a]
++  [ FilePath
"***          " forall a. [a] -> [a] -> [a]
++  FilePath -> FilePath
pad FilePath
s forall a. [a] -> [a] -> [a]
++ FilePath
" [Depends on: " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate FilePath
", " (NamedSymVar -> FilePath
getUserName' forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [NamedSymVar]
xs) forall a. [a] -> [a] -> [a]
++ FilePath
"]"  | (FilePath
s, [NamedSymVar]
xs) <- [(FilePath, [NamedSymVar])]
needsUniversalOpt ]
                                           forall a. [a] -> [a] -> [a]
++  [ FilePath
"***"
                                               , FilePath
"*** Optimization is only meaningful with existentially quantified metrics."
                                               ]

                   let optimizerDirectives :: [FilePath]
optimizerDirectives = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {a} {a}. (Show a, Show a) => Objective (a, a) -> [FilePath]
minmax [Objective (SV, SV)]
objectives forall a. [a] -> [a] -> [a]
++ OptimizeStyle -> [FilePath]
priority OptimizeStyle
style
                         where mkEq :: (a, a) -> FilePath
mkEq (a
x, a
y) = FilePath
"(assert (= " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show a
x forall a. [a] -> [a] -> [a]
++ FilePath
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show a
y forall a. [a] -> [a] -> [a]
++ FilePath
"))"

                               minmax :: Objective (a, a) -> [FilePath]
minmax (Minimize          FilePath
_  xy :: (a, a)
xy@(a
_, a
v))     = [forall {a} {a}. (Show a, Show a) => (a, a) -> FilePath
mkEq (a, a)
xy, FilePath
"(minimize "    forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show a
v                 forall a. [a] -> [a] -> [a]
++ FilePath
")"]
                               minmax (Maximize          FilePath
_  xy :: (a, a)
xy@(a
_, a
v))     = [forall {a} {a}. (Show a, Show a) => (a, a) -> FilePath
mkEq (a, a)
xy, FilePath
"(maximize "    forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show a
v                 forall a. [a] -> [a] -> [a]
++ FilePath
")"]
                               minmax (AssertWithPenalty FilePath
nm xy :: (a, a)
xy@(a
_, a
v) Penalty
mbp) = [forall {a} {a}. (Show a, Show a) => (a, a) -> FilePath
mkEq (a, a)
xy, FilePath
"(assert-soft " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show a
v forall a. [a] -> [a] -> [a]
++ Penalty -> FilePath
penalize Penalty
mbp forall a. [a] -> [a] -> [a]
++ FilePath
")"]
                                 where penalize :: Penalty -> FilePath
penalize Penalty
DefaultPenalty    = FilePath
""
                                       penalize (Penalty Rational
w Maybe FilePath
mbGrp)
                                          | Rational
w forall a. Ord a => a -> a -> Bool
<= Rational
0         = forall a. HasCallStack => FilePath -> a
error forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines [ FilePath
"SBV.AssertWithPenalty: Goal " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show FilePath
nm forall a. [a] -> [a] -> [a]
++ FilePath
" is assigned a non-positive penalty: " forall a. [a] -> [a] -> [a]
++ FilePath
shw
                                                                             , FilePath
"All soft goals must have > 0 penalties associated."
                                                                             ]
                                          | Bool
True           = FilePath
" :weight " forall a. [a] -> [a] -> [a]
++ FilePath
shw forall a. [a] -> [a] -> [a]
++ forall b a. b -> (a -> b) -> Maybe a -> b
maybe FilePath
"" FilePath -> FilePath
group Maybe FilePath
mbGrp
                                          where shw :: FilePath
shw = forall a. Show a => a -> FilePath
show (forall a. Fractional a => Rational -> a
fromRational Rational
w :: Double)

                                       group :: FilePath -> FilePath
group FilePath
g = FilePath
" :id " forall a. [a] -> [a] -> [a]
++ FilePath
g

                               priority :: OptimizeStyle -> [FilePath]
priority OptimizeStyle
Lexicographic = [] -- default, no option needed
                               priority OptimizeStyle
Independent   = [FilePath
"(set-option :opt.priority box)"]
                               priority (Pareto Maybe Int
_)    = [FilePath
"(set-option :opt.priority pareto)"]

                   forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> FilePath -> m ()
Control.send Bool
True) [FilePath]
optimizerDirectives

                   case OptimizeStyle
style of
                     OptimizeStyle
Lexicographic -> SMTResult -> OptimizeResult
LexicographicResult forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
Control.getLexicographicOptResults
                     OptimizeStyle
Independent   -> [(FilePath, SMTResult)] -> OptimizeResult
IndependentResult   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
[FilePath] -> m [(FilePath, SMTResult)]
Control.getIndependentOptResults (forall a b. (a -> b) -> [a] -> [b]
map forall a. Objective a -> FilePath
objectiveName [Objective (SV, SV)]
objectives)
                     Pareto Maybe Int
mbN    -> (Bool, [SMTResult]) -> OptimizeResult
ParetoResult        forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> m (Bool, [SMTResult])
Control.getParetoOptResults Maybe Int
mbN

  -- | Generalization of 'Data.SBV.isVacuous'
  isVacuous :: a -> m Bool
  isVacuous = forall (m :: * -> *) a. MProvable m a => SMTConfig -> a -> m Bool
isVacuousWith SMTConfig
defaultSMTCfg

  -- | Generalization of 'Data.SBV.isVacuousWith'
  isVacuousWith :: SMTConfig -> a -> m Bool
  isVacuousWith SMTConfig
cfg a
a = -- NB. Can't call runWithQuery since last constraint would become the implication!
       forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) (forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_ a
a forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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 <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
Control.checkSat
                  case CheckSatResult
cs of
                    CheckSatResult
Control.Unsat  -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                    CheckSatResult
Control.Sat    -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                    Control.DSat{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                    CheckSatResult
Control.Unk    -> forall a. HasCallStack => FilePath -> a
error FilePath
"SBV: isVacuous: Solver returned unknown!"

  -- | Generalization of 'Data.SBV.isTheorem'
  isTheorem :: a -> m Bool
  isTheorem = forall (m :: * -> *) a. MProvable m a => SMTConfig -> a -> m Bool
isTheoremWith SMTConfig
defaultSMTCfg

  -- | Generalization of 'Data.SBV.isTheoremWith'
  isTheoremWith :: SMTConfig -> a -> m Bool
  isTheoremWith SMTConfig
cfg a
p = do ThmResult
r <- forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m ThmResult
proveWith SMTConfig
cfg a
p
                           let bad :: a
bad = forall a. HasCallStack => FilePath -> a
error forall a b. (a -> b) -> a -> b
$ FilePath
"SBV.isTheorem: Received:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show ThmResult
r
                           case ThmResult
r of
                             ThmResult Unsatisfiable{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                             ThmResult Satisfiable{}   -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                             ThmResult DeltaSat{}      -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                             ThmResult SatExtField{}   -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                             ThmResult Unknown{}       -> forall {a}. a
bad
                             ThmResult ProofError{}    -> forall {a}. a
bad

  -- | Generalization of 'Data.SBV.isSatisfiable'
  isSatisfiable :: a -> m Bool
  isSatisfiable = forall (m :: * -> *) a. MProvable m a => SMTConfig -> a -> m Bool
isSatisfiableWith SMTConfig
defaultSMTCfg

  -- | Generalization of 'Data.SBV.isSatisfiableWith'
  isSatisfiableWith :: SMTConfig -> a -> m Bool
  isSatisfiableWith SMTConfig
cfg a
p = do SatResult
r <- forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m SatResult
satWith SMTConfig
cfg a
p
                               case SatResult
r of
                                 SatResult Satisfiable{}   -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                                 SatResult Unsatisfiable{} -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                                 SatResult
_                         -> forall a. HasCallStack => FilePath -> a
error forall a b. (a -> b) -> a -> b
$ FilePath
"SBV.isSatisfiable: Received: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show SatResult
r

  -- | Validate a model obtained from the solver
  validate :: Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
  validate Bool
isSAT SMTConfig
cfg a
p SMTResult
res = case SMTResult
res of
                               Unsatisfiable{} -> forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
res
                               Satisfiable SMTConfig
_ SMTModel
m -> case SMTModel -> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
modelBindings SMTModel
m of
                                                    Maybe [((Quantifier, NamedSymVar), Maybe CV)]
Nothing  -> forall a. HasCallStack => FilePath -> a
error FilePath
"Data.SBV.validate: Impossible happened; no bindings generated during model validation."
                                                    Just [((Quantifier, NamedSymVar), Maybe CV)]
env -> forall {m :: * -> *}.
MProvable m a =>
[((Quantifier, NamedSymVar), Maybe CV)] -> m SMTResult
check [((Quantifier, NamedSymVar), Maybe CV)]
env

                               DeltaSat {}     -> forall {m :: * -> *}. Monad m => [FilePath] -> m SMTResult
cant [ FilePath
"The model is delta-satisfiable."
                                                       , FilePath
"Cannot validate delta-satisfiable models."
                                                       ]

                               SatExtField{}   -> forall {m :: * -> *}. Monad m => [FilePath] -> m SMTResult
cant [ FilePath
"The model requires an extension field value."
                                                       , FilePath
"Cannot validate models with infinities/epsilons produced during optimization."
                                                       , FilePath
""
                                                       , FilePath
"To turn validation off, use `cfg{optimizeValidateConstraints = False}`"
                                                       ]

                               Unknown{}       -> forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
res
                               ProofError{}    -> forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
res

    where cant :: [FilePath] -> m SMTResult
cant [FilePath]
msg = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SMTConfig -> [FilePath] -> Maybe SMTResult -> SMTResult
ProofError SMTConfig
cfg ([FilePath]
msg forall a. [a] -> [a] -> [a]
++ [ FilePath
""
                                                     , FilePath
"Unable to validate the produced model."
                                                     ]) (forall a. a -> Maybe a
Just SMTResult
res)

          check :: [((Quantifier, NamedSymVar), Maybe CV)] -> m SMTResult
check [((Quantifier, NamedSymVar), Maybe CV)]
env = do let univs :: [FilePath]
univs    = [Text -> FilePath
T.unpack Text
n | ((Quantifier
ALL, NamedSymVar SV
_ Text
n), Maybe CV
_) <- [((Quantifier, NamedSymVar), Maybe CV)]
env]
                             envShown :: FilePath
envShown = Bool
-> Bool -> SMTConfig -> [(FilePath, GeneralizedCV)] -> FilePath
showModelDictionary Bool
True Bool
True SMTConfig
cfg [(FilePath, GeneralizedCV)]
modelBinds
                                where modelBinds :: [(FilePath, GeneralizedCV)]
modelBinds = [(Text -> FilePath
T.unpack Text
n, forall {a}.
HasKind a =>
Quantifier -> a -> Maybe CV -> GeneralizedCV
fake Quantifier
q SV
s Maybe CV
v) | ((Quantifier
q, NamedSymVar SV
s Text
n), Maybe CV
v) <- [((Quantifier, NamedSymVar), Maybe CV)]
env]
                                      fake :: Quantifier -> a -> Maybe CV -> GeneralizedCV
fake Quantifier
q a
s Maybe CV
Nothing
                                        | Quantifier
q forall a. Eq a => a -> a -> Bool
== Quantifier
ALL
                                        = CV -> GeneralizedCV
RegularCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (forall a. HasKind a => a -> Kind
kindOf a
s) forall a b. (a -> b) -> a -> b
$ (Maybe Int, FilePath) -> CVal
CUserSort (forall a. Maybe a
Nothing, FilePath
"<universally quantified>")
                                        | Bool
True
                                        = CV -> GeneralizedCV
RegularCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV (forall a. HasKind a => a -> Kind
kindOf a
s) forall a b. (a -> b) -> a -> b
$ (Maybe Int, FilePath) -> CVal
CUserSort (forall a. Maybe a
Nothing, FilePath
"<no binding found>")
                                      fake Quantifier
_ a
_ (Just CV
v) = CV -> GeneralizedCV
RegularCV CV
v

                             notify :: FilePath -> m ()
notify FilePath
s
                               | Bool -> Bool
not (SMTConfig -> Bool
verbose SMTConfig
cfg) = forall (m :: * -> *) a. Monad m => a -> m a
return ()
                               | Bool
True              = forall (m :: * -> *). MonadIO m => SMTConfig -> [FilePath] -> m ()
debug SMTConfig
cfg [FilePath
"[VALIDATE] " FilePath -> FilePath -> FilePath
`alignPlain` FilePath
s]

                         forall {m :: * -> *}. MonadIO m => FilePath -> m ()
notify forall a b. (a -> b) -> a -> b
$ FilePath
"Validating the model. " forall a. [a] -> [a] -> [a]
++ if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((Quantifier, NamedSymVar), Maybe CV)]
env then FilePath
"There are no assignments." else FilePath
"Assignment:"
                         forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {m :: * -> *}. MonadIO m => FilePath -> m ()
notify [FilePath
"    " forall a. [a] -> [a] -> [a]
++ FilePath
l | FilePath
l <- FilePath -> [FilePath]
lines FilePath
envShown]

                         forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FilePath]
univs) forall a b. (a -> b) -> a -> b
$ do
                                forall {m :: * -> *}. MonadIO m => FilePath -> m ()
notify forall a b. (a -> b) -> a -> b
$ FilePath
"NB. The following variable(s) are universally quantified: " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate FilePath
", " [FilePath]
univs
                                forall {m :: * -> *}. MonadIO m => FilePath -> m ()
notify   FilePath
"    We will assume that they are essentially zero for the purposes of validation."
                                forall {m :: * -> *}. MonadIO m => FilePath -> m ()
notify   FilePath
"    Note that this is a gross simplification of the model validation with universals!"

                         Result
result <- forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a.
MonadIO m =>
SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic (Maybe (Bool, [((Quantifier, NamedSymVar), Maybe CV)]) -> SBVRunMode
Concrete (forall a. a -> Maybe a
Just (Bool
isSAT, [((Quantifier, NamedSymVar), Maybe CV)]
env))) ((if Bool
isSAT then forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_ a
p else forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_ a
p) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output)

                         let explain :: [FilePath]
explain  = [ FilePath
""
                                        , FilePath
"Assignment:"  forall a. [a] -> [a] -> [a]
++ if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((Quantifier, NamedSymVar), Maybe CV)]
env then FilePath
" <none>" else FilePath
""
                                        ]
                                     forall a. [a] -> [a] -> [a]
++ [ FilePath
""          | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((Quantifier, NamedSymVar), Maybe CV)]
env)]
                                     forall a. [a] -> [a] -> [a]
++ [ FilePath
"    " forall a. [a] -> [a] -> [a]
++ FilePath
l | FilePath
l <- FilePath -> [FilePath]
lines FilePath
envShown]
                                     forall a. [a] -> [a] -> [a]
++ [ FilePath
"" ]

                             wrap :: FilePath -> [FilePath] -> m SMTResult
wrap FilePath
tag [FilePath]
extras = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SMTConfig -> [FilePath] -> Maybe SMTResult -> SMTResult
ProofError SMTConfig
cfg (FilePath
tag forall a. a -> [a] -> [a]
: [FilePath]
explain forall a. [a] -> [a] -> [a]
++ [FilePath]
extras) (forall a. a -> Maybe a
Just SMTResult
res)

                             giveUp :: FilePath -> m SMTResult
giveUp   FilePath
s     = forall {m :: * -> *}.
Monad m =>
FilePath -> [FilePath] -> m SMTResult
wrap (FilePath
"Data.SBV: Cannot validate the model: " forall a. [a] -> [a] -> [a]
++ FilePath
s)
                                                   [ FilePath
"SBV's model validator is incomplete, and cannot handle this particular case."
                                                   , FilePath
"Please report this as a feature request or possibly a bug!"
                                                   ]

                             badModel :: FilePath -> m SMTResult
badModel FilePath
s     = forall {m :: * -> *}.
Monad m =>
FilePath -> [FilePath] -> m SMTResult
wrap (FilePath
"Data.SBV: Model validation failure: " forall a. [a] -> [a] -> [a]
++ FilePath
s)
                                                   [ FilePath
"Backend solver returned a model that does not satisfy the constraints."
                                                   , FilePath
"This could indicate a bug in the backend solver, or SBV itself. Please report."
                                                   ]

                             notConcrete :: SV -> m SMTResult
notConcrete SV
sv = forall {m :: * -> *}.
Monad m =>
FilePath -> [FilePath] -> m SMTResult
wrap (FilePath
"Data.SBV: Cannot validate the model, since " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show SV
sv forall a. [a] -> [a] -> [a]
++ FilePath
" is not concretely computable.")
                                                   (  Maybe FilePath -> [FilePath]
perhaps (SV -> Maybe FilePath
why SV
sv)
                                                   forall a. [a] -> [a] -> [a]
++ [ FilePath
"SBV's model validator is incomplete, and cannot handle this particular case."
                                                      , FilePath
"Please report this as a feature request or possibly a bug!"
                                                      ]
                                                   )
                                  where perhaps :: Maybe FilePath -> [FilePath]
perhaps Maybe FilePath
Nothing  = []
                                        perhaps (Just FilePath
x) = [FilePath
x, FilePath
""]

                                        -- This is incomplete, but should capture the most common cases
                                        why :: SV -> Maybe FilePath
why SV
s = case SV
s forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` forall (t :: * -> *) a. Foldable t => t a -> [a]
S.toList (SBVPgm -> Seq (SV, SBVExpr)
pgmAssignments (Result -> SBVPgm
resAsgns Result
result)) of
                                                  Maybe SBVExpr
Nothing            -> forall a. Maybe a
Nothing
                                                  Just (SBVApp Op
o [SV]
as) -> case Op
o of
                                                                          Uninterpreted FilePath
v   -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ FilePath
"The value depends on the uninterpreted constant " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show FilePath
v forall a. [a] -> [a] -> [a]
++ FilePath
"."
                                                                          IEEEFP FPOp
FP_FMA     -> forall a. a -> Maybe a
Just FilePath
"Floating point FMA operation is not supported concretely."
                                                                          IEEEFP FPOp
_          -> forall a. a -> Maybe a
Just FilePath
"Not all floating point operations are supported concretely."
                                                                          OverflowOp OvOp
_      -> forall a. a -> Maybe a
Just FilePath
"Overflow-checking is not done concretely."
                                                                          Op
_                 -> forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe SV -> Maybe FilePath
why [SV]
as

                             cstrs :: [(Bool, [(FilePath, FilePath)], SV)]
cstrs = forall (t :: * -> *) a. Foldable t => t a -> [a]
S.toList forall a b. (a -> b) -> a -> b
$ Result -> Seq (Bool, [(FilePath, FilePath)], SV)
resConstraints Result
result

                             walkConstraints :: [(Bool, [(FilePath, a)], SV)] -> m SMTResult -> m SMTResult
walkConstraints [] m SMTResult
cont = do
                                forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Bool, [(FilePath, FilePath)], SV)]
cstrs) forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *}. MonadIO m => FilePath -> m ()
notify FilePath
"Validated all constraints."
                                m SMTResult
cont
                             walkConstraints ((Bool
isSoft, [(FilePath, a)]
attrs, SV
sv) : [(Bool, [(FilePath, a)], SV)]
rest) m SMTResult
cont
                                | forall a. HasKind a => a -> Kind
kindOf SV
sv forall a. Eq a => a -> a -> Bool
/= Kind
KBool
                                = forall {m :: * -> *}. Monad m => FilePath -> m SMTResult
giveUp forall a b. (a -> b) -> a -> b
$ FilePath
"Constraint tied to " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show SV
sv forall a. [a] -> [a] -> [a]
++ FilePath
" is non-boolean."
                                | Bool
isSoft Bool -> Bool -> Bool
|| SV
sv forall a. Eq a => a -> a -> Bool
== SV
trueSV
                                = [(Bool, [(FilePath, a)], SV)] -> m SMTResult -> m SMTResult
walkConstraints [(Bool, [(FilePath, a)], SV)]
rest m SMTResult
cont
                                | SV
sv forall a. Eq a => a -> a -> Bool
== SV
falseSV
                                = case Maybe a
mbName of
                                    Just a
nm -> forall {m :: * -> *}. Monad m => FilePath -> m SMTResult
badModel forall a b. (a -> b) -> a -> b
$ FilePath
"Named constraint " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show a
nm forall a. [a] -> [a] -> [a]
++ FilePath
" evaluated to False."
                                    Maybe a
Nothing -> forall {m :: * -> *}. Monad m => FilePath -> m SMTResult
badModel FilePath
"A constraint was violated."
                                | Bool
True
                                = forall {m :: * -> *}. Monad m => SV -> m SMTResult
notConcrete SV
sv
                                where mbName :: Maybe a
mbName = forall a. [a] -> Maybe a
listToMaybe [a
n | (FilePath
":named", a
n) <- [(FilePath, a)]
attrs]

                             -- SAT: All outputs must be true
                             satLoop :: [SV] -> m SMTResult
satLoop []
                               = do forall {m :: * -> *}. MonadIO m => FilePath -> m ()
notify FilePath
"All outputs are satisfied. Validation complete."
                                    forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
res
                             satLoop (SV
sv:[SV]
svs)
                               | forall a. HasKind a => a -> Kind
kindOf SV
sv forall a. Eq a => a -> a -> Bool
/= Kind
KBool
                               = forall {m :: * -> *}. Monad m => FilePath -> m SMTResult
giveUp forall a b. (a -> b) -> a -> b
$ FilePath
"Output tied to " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show SV
sv forall a. [a] -> [a] -> [a]
++ FilePath
" is non-boolean."
                               | SV
sv forall a. Eq a => a -> a -> Bool
== SV
trueSV
                               = [SV] -> m SMTResult
satLoop [SV]
svs
                               | SV
sv forall a. Eq a => a -> a -> Bool
== SV
falseSV
                               = forall {m :: * -> *}. Monad m => FilePath -> m SMTResult
badModel FilePath
"Final output evaluated to False."
                               | Bool
True
                               = forall {m :: * -> *}. Monad m => SV -> m SMTResult
notConcrete SV
sv

                             -- Proof: At least one output must be false
                             proveLoop :: [SV] -> Bool -> m SMTResult
proveLoop [] Bool
somethingFailed
                               | Bool
somethingFailed = do forall {m :: * -> *}. MonadIO m => FilePath -> m ()
notify FilePath
"Counterexample is validated."
                                                      forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
res
                               | Bool
True            = do forall {m :: * -> *}. MonadIO m => FilePath -> m ()
notify FilePath
"Counterexample violates none of the outputs."
                                                      forall {m :: * -> *}. Monad m => FilePath -> m SMTResult
badModel FilePath
"Counter-example violates no constraints."
                             proveLoop (SV
sv:[SV]
svs) Bool
somethingFailed
                               | forall a. HasKind a => a -> Kind
kindOf SV
sv forall a. Eq a => a -> a -> Bool
/= Kind
KBool
                               = forall {m :: * -> *}. Monad m => FilePath -> m SMTResult
giveUp forall a b. (a -> b) -> a -> b
$ FilePath
"Output tied to " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show SV
sv forall a. [a] -> [a] -> [a]
++ FilePath
" is non-boolean."
                               | SV
sv forall a. Eq a => a -> a -> Bool
== SV
trueSV
                               = [SV] -> Bool -> m SMTResult
proveLoop [SV]
svs Bool
somethingFailed
                               | SV
sv forall a. Eq a => a -> a -> Bool
== SV
falseSV
                               = [SV] -> Bool -> m SMTResult
proveLoop [SV]
svs Bool
True
                               | Bool
True
                               = forall {m :: * -> *}. Monad m => SV -> m SMTResult
notConcrete SV
sv

                             -- Output checking is tricky, since we behave differently for different modes
                             checkOutputs :: [SV] -> m SMTResult
checkOutputs []
                               | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Bool, [(FilePath, FilePath)], SV)]
cstrs
                               = forall {m :: * -> *}. Monad m => FilePath -> m SMTResult
giveUp FilePath
"Impossible happened: There are no outputs nor any constraints to check."
                             checkOutputs [SV]
os
                               = do forall {m :: * -> *}. MonadIO m => FilePath -> m ()
notify FilePath
"Validating outputs."
                                    if Bool
isSAT then forall {m :: * -> *}. MonadIO m => [SV] -> m SMTResult
satLoop   [SV]
os
                                             else forall {m :: * -> *}. MonadIO m => [SV] -> Bool -> m SMTResult
proveLoop [SV]
os Bool
False

                         forall {m :: * -> *}. MonadIO m => FilePath -> m ()
notify forall a b. (a -> b) -> a -> b
$ if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Bool, [(FilePath, FilePath)], SV)]
cstrs
                                  then FilePath
"There are no constraints to check."
                                  else FilePath
"Validating " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Bool, [(FilePath, FilePath)], SV)]
cstrs) forall a. [a] -> [a] -> [a]
++ FilePath
" constraint(s)."

                         forall {m :: * -> *} {a}.
(MonadIO m, Show a) =>
[(Bool, [(FilePath, a)], SV)] -> m SMTResult -> m SMTResult
walkConstraints [(Bool, [(FilePath, FilePath)], SV)]
cstrs (forall {m :: * -> *}. MonadIO m => [SV] -> m SMTResult
checkOutputs (Result -> [SV]
resOutputs Result
result))

-- | `Provable` is specialization of `MProvable` to the `IO` monad. Unless you are using
-- transformers explicitly, this is the type you should prefer.
type Provable = MProvable IO

-- | 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 :: forall a.
Provable a =>
[SMTConfig] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
proveWithAll  = (forall b a.
NFData b =>
[SMTConfig]
-> (SMTConfig -> a -> IO b)
-> a
-> IO [(Solver, NominalDiffTime, b)]
`sbvWithAll` forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m ThmResult
proveWith)

-- | 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 :: forall a.
Provable a =>
[SMTConfig] -> a -> IO (Solver, NominalDiffTime, ThmResult)
proveWithAny  = (forall b a.
NFData b =>
[SMTConfig]
-> (SMTConfig -> a -> IO b) -> a -> IO (Solver, NominalDiffTime, b)
`sbvWithAny` forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m ThmResult
proveWith)

-- | 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 :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
satWithAll :: forall a.
Provable a =>
[SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
satWithAll = (forall b a.
NFData b =>
[SMTConfig]
-> (SMTConfig -> a -> IO b)
-> a
-> IO [(Solver, NominalDiffTime, b)]
`sbvWithAll` forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m SatResult
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 :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult)
satWithAny :: forall a.
Provable a =>
[SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult)
satWithAny = (forall b a.
NFData b =>
[SMTConfig]
-> (SMTConfig -> a -> IO b) -> a -> IO (Solver, NominalDiffTime, b)
`sbvWithAny` forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m SatResult
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 :: Provable a => SMTConfig -> [Query b] -> a -> IO (Solver, NominalDiffTime, SatResult)
satConcurrentWithAny :: forall a b.
Provable a =>
SMTConfig
-> [Query b] -> a -> IO (Solver, NominalDiffTime, SatResult)
satConcurrentWithAny SMTConfig
solver [Query b]
qs a
a = do (Solver
slvr,NominalDiffTime
time,SMTResult
result) <- forall c a (m :: * -> *) b.
NFData c =>
SMTConfig
-> (SMTConfig -> a -> QueryT m b -> IO c)
-> [QueryT m b]
-> a
-> IO (Solver, NominalDiffTime, c)
sbvConcurrentWithAny SMTConfig
solver forall {m :: * -> *} {a} {a}.
MProvable m a =>
SMTConfig -> a -> QueryT m a -> m SMTResult
go [Query b]
qs a
a
                                      forall (m :: * -> *) a. Monad m => a -> m a
return (Solver
slvr, NominalDiffTime
time, SMTResult -> SatResult
SatResult SMTResult
result)
  where go :: SMTConfig -> a -> QueryT m a -> m SMTResult
go SMTConfig
cfg a
a' QueryT m a
q = forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
True (do a
_ <- QueryT m a
q; forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
Control.getSMTResult) SMTConfig
cfg a
a'

-- | 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 :: forall a b.
Provable a =>
SMTConfig
-> [Query b] -> a -> IO (Solver, NominalDiffTime, ThmResult)
proveConcurrentWithAny SMTConfig
solver [Query b]
qs a
a = do (Solver
slvr,NominalDiffTime
time,SMTResult
result) <- forall c a (m :: * -> *) b.
NFData c =>
SMTConfig
-> (SMTConfig -> a -> QueryT m b -> IO c)
-> [QueryT m b]
-> a
-> IO (Solver, NominalDiffTime, c)
sbvConcurrentWithAny SMTConfig
solver forall {m :: * -> *} {a} {a}.
MProvable m a =>
SMTConfig -> a -> QueryT m a -> m SMTResult
go [Query b]
qs a
a
                                        forall (m :: * -> *) a. Monad m => a -> m a
return (Solver
slvr, NominalDiffTime
time, SMTResult -> ThmResult
ThmResult SMTResult
result)
  where go :: SMTConfig -> a -> QueryT m a -> m SMTResult
go SMTConfig
cfg a
a' QueryT m a
q = forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
False (do a
_ <- QueryT m a
q;  forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
Control.getSMTResult) SMTConfig
cfg a
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 :: Provable a => SMTConfig -> [Query b] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
satConcurrentWithAll :: forall a b.
Provable a =>
SMTConfig
-> [Query b] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
satConcurrentWithAll SMTConfig
solver [Query b]
qs a
a = do [(Solver, NominalDiffTime, SMTResult)]
results <- forall c a (m :: * -> *) b.
NFData c =>
SMTConfig
-> (SMTConfig -> a -> QueryT m b -> IO c)
-> [QueryT m b]
-> a
-> IO [(Solver, NominalDiffTime, c)]
sbvConcurrentWithAll SMTConfig
solver forall {m :: * -> *} {a} {a}.
MProvable m a =>
SMTConfig -> a -> QueryT m a -> m SMTResult
go [Query b]
qs a
a
                                      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (\(Solver
a',NominalDiffTime
b,SMTResult
c) -> (Solver
a',NominalDiffTime
b,SMTResult -> SatResult
SatResult SMTResult
c)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Solver, NominalDiffTime, SMTResult)]
results
  where go :: SMTConfig -> a -> QueryT m a -> m SMTResult
go SMTConfig
cfg a
a' QueryT m a
q = forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
True (do a
_ <- QueryT m a
q; forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
Control.getSMTResult) SMTConfig
cfg a
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 :: forall a b.
Provable a =>
SMTConfig
-> [Query b] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
proveConcurrentWithAll SMTConfig
solver [Query b]
qs a
a = do [(Solver, NominalDiffTime, SMTResult)]
results <- forall c a (m :: * -> *) b.
NFData c =>
SMTConfig
-> (SMTConfig -> a -> QueryT m b -> IO c)
-> [QueryT m b]
-> a
-> IO [(Solver, NominalDiffTime, c)]
sbvConcurrentWithAll SMTConfig
solver forall {m :: * -> *} {a} {a}.
MProvable m a =>
SMTConfig -> a -> QueryT m a -> m SMTResult
go [Query b]
qs a
a
                                        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (\(Solver
a',NominalDiffTime
b,SMTResult
c) -> (Solver
a',NominalDiffTime
b,SMTResult -> ThmResult
ThmResult SMTResult
c)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Solver, NominalDiffTime, SMTResult)]
results
  where go :: SMTConfig -> a -> QueryT m a -> m SMTResult
go SMTConfig
cfg a
a' QueryT m a
q = forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
False (do a
_ <- QueryT m a
q; forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
Control.getSMTResult) SMTConfig
cfg a
a'

-- | Create an SMT-Lib2 benchmark. The 'Bool' argument controls whether this is a SAT instance, i.e.,
-- translate the query directly, or a PROVE instance, i.e., translate the negated query.
generateSMTBenchmark :: (MonadIO m, MProvable m a) => Bool -> a -> m String
generateSMTBenchmark :: forall (m :: * -> *) a.
(MonadIO m, MProvable m a) =>
Bool -> a -> m FilePath
generateSMTBenchmark Bool
isSat a
a = do
      ZonedTime
t <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ZonedTime
getZonedTime

      let comments :: [FilePath]
comments = [FilePath
"Automatically created by SBV on " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show ZonedTime
t]
          cfg :: SMTConfig
cfg      = SMTConfig
defaultSMTCfg { smtLibVersion :: SMTLibVersion
smtLibVersion = SMTLibVersion
SMTLib2 }

      (SBool
_, Result
res) <- 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) forall a b. (a -> b) -> a -> b
$ (if Bool
isSat then forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_ else forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_) a
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 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 -> [FilePath] -> Result -> SMTProblem
Control.runProofOn (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
SMTMode QueryContext
QueryInternal IStage
IRun Bool
isSat SMTConfig
cfg) QueryContext
QueryInternal [FilePath]
comments Result
res
          out :: FilePath
out                   = forall a. Show a => a -> FilePath
show (SMTConfig -> SMTLibPgm
smtLibPgm SMTConfig
cfg)

      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FilePath
out forall a. [a] -> [a] -> [a]
++ FilePath
"\n(check-sat)\n"

checkNoOptimizations :: MonadIO m => QueryT m ()
checkNoOptimizations :: forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations = do [Objective (SV, SV)]
objectives <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [Objective (SV, SV)]
Control.getObjectives

                          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Objective (SV, SV)]
objectives) forall a b. (a -> b) -> a -> b
$
                                forall a. HasCallStack => FilePath -> a
error forall a b. (a -> b) -> a -> b
$ [FilePath] -> FilePath
unlines [ FilePath
""
                                                , FilePath
"*** Data.SBV: Unsupported call sat/prove when optimization objectives are present."
                                                , FilePath
"*** Use \"optimize\"/\"optimizeWith\" to calculate optimal satisfaction!"
                                                ]

-- If we get a program producing nothing (i.e., Symbolic ()), pretend it simply returns True.
-- This is useful since min/max calls and constraints will provide the context
instance ExtractIO m => MProvable m (SymbolicT m ()) where
  universal_ :: SymbolicT m () -> SymbolicT m SBool
universal_     SymbolicT m ()
a = forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_     ((SymbolicT m ()
a forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return SBool
sTrue) :: SymbolicT m SBool)
  universal :: [FilePath] -> SymbolicT m () -> SymbolicT m SBool
universal [FilePath]
ns   SymbolicT m ()
a = forall (m :: * -> *) a.
MProvable m a =>
[FilePath] -> a -> SymbolicT m SBool
universal [FilePath]
ns   ((SymbolicT m ()
a forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return SBool
sTrue) :: SymbolicT m SBool)
  existential_ :: SymbolicT m () -> SymbolicT m SBool
existential_   SymbolicT m ()
a = forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_   ((SymbolicT m ()
a forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return SBool
sTrue) :: SymbolicT m SBool)
  existential :: [FilePath] -> SymbolicT m () -> SymbolicT m SBool
existential [FilePath]
ns SymbolicT m ()
a = forall (m :: * -> *) a.
MProvable m a =>
[FilePath] -> a -> SymbolicT m SBool
existential [FilePath]
ns ((SymbolicT m ()
a forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return SBool
sTrue) :: SymbolicT m SBool)

instance ExtractIO m => MProvable m (SymbolicT m SBool) where
  universal_ :: SymbolicT m SBool -> SymbolicT m SBool
universal_     = forall a. a -> a
id
  universal :: [FilePath] -> SymbolicT m SBool -> SymbolicT m SBool
universal []   = forall a. a -> a
id
  universal [FilePath]
xs   = forall a. HasCallStack => FilePath -> a
error forall a b. (a -> b) -> a -> b
$ FilePath
"SBV.universal: Extra unmapped name(s) in predicate construction: " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate FilePath
", " [FilePath]
xs
  existential_ :: SymbolicT m SBool -> SymbolicT m SBool
existential_   = forall a. a -> a
id
  existential :: [FilePath] -> SymbolicT m SBool -> SymbolicT m SBool
existential [] = forall a. a -> a
id
  existential [FilePath]
xs = forall a. HasCallStack => FilePath -> a
error forall a b. (a -> b) -> a -> b
$ FilePath
"SBV.existential: Extra unmapped name(s) in predicate construction: " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate FilePath
", " [FilePath]
xs

instance ExtractIO m => MProvable m SBool where
  universal_ :: SBool -> SymbolicT m SBool
universal_    = forall (m :: * -> *) a. Monad m => a -> m a
return
  universal :: [FilePath] -> SBool -> SymbolicT m SBool
universal [FilePath]
_   = forall (m :: * -> *) a. Monad m => a -> m a
return
  existential_ :: SBool -> SymbolicT m SBool
existential_  = forall (m :: * -> *) a. Monad m => a -> m a
return
  existential :: [FilePath] -> SBool -> SymbolicT m SBool
existential [FilePath]
_ = forall (m :: * -> *) a. Monad m => a -> m a
return

{-
-- The following works, 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 .==).
instance Provable Bool where
  universal_  x  = universal_     (if x then true else false :: SBool)
  universal s x  = universal s    (if x then true else false :: SBool)
  existential_  x = existential_  (if x then true else false :: SBool)
  existential s x = existential s (if x then true else false :: SBool)
-}

-- Functions
instance (SymVal a, MProvable m p) => MProvable m (SBV a -> p) where
  universal_ :: (SBV a -> p) -> SymbolicT m SBool
universal_         SBV a -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvForall_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_   forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a
  universal :: [FilePath] -> (SBV a -> p) -> SymbolicT m SBool
universal (FilePath
s:[FilePath]
ss)   SBV a -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvForall FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
MProvable m a =>
[FilePath] -> a -> SymbolicT m SBool
universal [FilePath]
ss forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a
  universal []       SBV a -> p
k = forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_ SBV a -> p
k
  existential_ :: (SBV a -> p) -> SymbolicT m SBool
existential_       SBV a -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvExists_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_   forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a
  existential :: [FilePath] -> (SBV a -> p) -> SymbolicT m SBool
existential (FilePath
s:[FilePath]
ss) SBV a -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvExists FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
MProvable m a =>
[FilePath] -> a -> SymbolicT m SBool
existential [FilePath]
ss forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a
  existential []     SBV a -> p
k = forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_ SBV a -> p
k

-- Arrays
instance (HasKind a, HasKind b, MProvable m p) => MProvable m (SArray a b -> p) where
  universal_ :: (SArray a b -> p) -> SymbolicT m SBool
universal_         SArray a b -> p
k = forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
Maybe (SBV b) -> m (array a b)
newArray_  forall a. Maybe a
Nothing forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SArray a b
a -> forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_   forall a b. (a -> b) -> a -> b
$ SArray a b -> p
k SArray a b
a
  universal :: [FilePath] -> (SArray a b -> p) -> SymbolicT m SBool
universal  (FilePath
s:[FilePath]
ss)  SArray a b -> p
k = forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
FilePath -> Maybe (SBV b) -> m (array a b)
newArray FilePath
s forall a. Maybe a
Nothing forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SArray a b
a -> forall (m :: * -> *) a.
MProvable m a =>
[FilePath] -> a -> SymbolicT m SBool
universal [FilePath]
ss forall a b. (a -> b) -> a -> b
$ SArray a b -> p
k SArray a b
a
  universal  []      SArray a b -> p
k = forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_ SArray a b -> p
k
  existential_ :: (SArray a b -> p) -> SymbolicT m SBool
existential_       SArray a b -> p
k = forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
Maybe (SBV b) -> m (array a b)
newArray_  forall a. Maybe a
Nothing forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SArray a b
a -> forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_   forall a b. (a -> b) -> a -> b
$ SArray a b -> p
k SArray a b
a
  existential :: [FilePath] -> (SArray a b -> p) -> SymbolicT m SBool
existential (FilePath
s:[FilePath]
ss) SArray a b -> p
k = forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
FilePath -> Maybe (SBV b) -> m (array a b)
newArray FilePath
s forall a. Maybe a
Nothing forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SArray a b
a -> forall (m :: * -> *) a.
MProvable m a =>
[FilePath] -> a -> SymbolicT m SBool
existential [FilePath]
ss forall a b. (a -> b) -> a -> b
$ SArray a b -> p
k SArray a b
a
  existential []     SArray a b -> p
k = forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_ SArray a b -> p
k

-- 2 Tuple
instance (SymVal a, SymVal b, MProvable m p) => MProvable m ((SBV a, SBV b) -> p) where
  universal_ :: ((SBV a, SBV b) -> p) -> SymbolicT m SBool
universal_         (SBV a, SBV b) -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvForall_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_   forall a b. (a -> b) -> a -> b
$ \SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)
  universal :: [FilePath] -> ((SBV a, SBV b) -> p) -> SymbolicT m SBool
universal (FilePath
s:[FilePath]
ss)   (SBV a, SBV b) -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvForall FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
MProvable m a =>
[FilePath] -> a -> SymbolicT m SBool
universal [FilePath]
ss forall a b. (a -> b) -> a -> b
$ \SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)
  universal []       (SBV a, SBV b) -> p
k = forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_ (SBV a, SBV b) -> p
k
  existential_ :: ((SBV a, SBV b) -> p) -> SymbolicT m SBool
existential_       (SBV a, SBV b) -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvExists_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_   forall a b. (a -> b) -> a -> b
$ \SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)
  existential :: [FilePath] -> ((SBV a, SBV b) -> p) -> SymbolicT m SBool
existential (FilePath
s:[FilePath]
ss) (SBV a, SBV b) -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvExists FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
MProvable m a =>
[FilePath] -> a -> SymbolicT m SBool
existential [FilePath]
ss forall a b. (a -> b) -> a -> b
$ \SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)
  existential []     (SBV a, SBV b) -> p
k = forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_ (SBV a, SBV b) -> p
k

-- 3 Tuple
instance (SymVal a, SymVal b, SymVal c, MProvable m p) => MProvable m ((SBV a, SBV b, SBV c) -> p) where
  universal_ :: ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
universal_         (SBV a, SBV b, SBV c) -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvForall_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_   forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c -> (SBV a, SBV b, SBV c) -> p
k (SBV a
a, SBV b
b, SBV c
c)
  universal :: [FilePath] -> ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
universal (FilePath
s:[FilePath]
ss)   (SBV a, SBV b, SBV c) -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvForall FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
MProvable m a =>
[FilePath] -> a -> SymbolicT m SBool
universal [FilePath]
ss forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c -> (SBV a, SBV b, SBV c) -> p
k (SBV a
a, SBV b
b, SBV c
c)
  universal []       (SBV a, SBV b, SBV c) -> p
k = forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_ (SBV a, SBV b, SBV c) -> p
k
  existential_ :: ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
existential_       (SBV a, SBV b, SBV c) -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvExists_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_   forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c -> (SBV a, SBV b, SBV c) -> p
k (SBV a
a, SBV b
b, SBV c
c)
  existential :: [FilePath] -> ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
existential (FilePath
s:[FilePath]
ss) (SBV a, SBV b, SBV c) -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvExists FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
MProvable m a =>
[FilePath] -> a -> SymbolicT m SBool
existential [FilePath]
ss forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c -> (SBV a, SBV b, SBV c) -> p
k (SBV a
a, SBV b
b, SBV c
c)
  existential []     (SBV a, SBV b, SBV c) -> p
k = forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_ (SBV a, SBV b, SBV c) -> p
k

-- 4 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, MProvable m p) => MProvable m ((SBV a, SBV b, SBV c, SBV d) -> p) where
  universal_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
universal_         (SBV a, SBV b, SBV c, SBV d) -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvForall_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_   forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c 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)
  universal :: [FilePath]
-> ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
universal (FilePath
s:[FilePath]
ss)   (SBV a, SBV b, SBV c, SBV d) -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvForall FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
MProvable m a =>
[FilePath] -> a -> SymbolicT m SBool
universal [FilePath]
ss forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c 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)
  universal []       (SBV a, SBV b, SBV c, SBV d) -> p
k = forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_ (SBV a, SBV b, SBV c, SBV d) -> p
k
  existential_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
existential_       (SBV a, SBV b, SBV c, SBV d) -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvExists_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_   forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c 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)
  existential :: [FilePath]
-> ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
existential (FilePath
s:[FilePath]
ss) (SBV a, SBV b, SBV c, SBV d) -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvExists FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
MProvable m a =>
[FilePath] -> a -> SymbolicT m SBool
existential [FilePath]
ss forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c 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)
  existential []     (SBV a, SBV b, SBV c, SBV d) -> p
k = forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_ (SBV a, SBV b, SBV c, SBV d) -> p
k

-- 5 Tuple
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
  universal_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
universal_         (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvForall_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_   forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d 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)
  universal :: [FilePath]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
universal (FilePath
s:[FilePath]
ss)   (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvForall FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
MProvable m a =>
[FilePath] -> a -> SymbolicT m SBool
universal [FilePath]
ss forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d 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)
  universal []       (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_ (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k
  existential_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
existential_       (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvExists_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_   forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d 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)
  existential :: [FilePath]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
existential (FilePath
s:[FilePath]
ss) (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvExists FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
MProvable m a =>
[FilePath] -> a -> SymbolicT m SBool
existential [FilePath]
ss forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d 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)
  existential []     (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_ (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k

-- 6 Tuple
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
  universal_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m SBool
universal_         (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvForall_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_   forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e 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)
  universal :: [FilePath]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m SBool
universal (FilePath
s:[FilePath]
ss)   (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvForall FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
MProvable m a =>
[FilePath] -> a -> SymbolicT m SBool
universal [FilePath]
ss forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e 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)
  universal []       (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k
  existential_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m SBool
existential_       (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvExists_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_   forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e 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)
  existential :: [FilePath]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m SBool
existential (FilePath
s:[FilePath]
ss) (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvExists FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
MProvable m a =>
[FilePath] -> a -> SymbolicT m SBool
existential [FilePath]
ss forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e 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)
  existential []     (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k

-- 7 Tuple
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
  universal_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m SBool
universal_         (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvForall_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_   forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f 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)
  universal :: [FilePath]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m SBool
universal (FilePath
s:[FilePath]
ss)   (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvForall FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
MProvable m a =>
[FilePath] -> a -> SymbolicT m SBool
universal [FilePath]
ss forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f 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)
  universal []       (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k
  existential_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m SBool
existential_       (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvExists_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_   forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f 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)
  existential :: [FilePath]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m SBool
existential (FilePath
s:[FilePath]
ss) (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvExists FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
MProvable m a =>
[FilePath] -> a -> SymbolicT m SBool
existential [FilePath]
ss forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f 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)
  existential []     (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k

-- | Generalization of 'Data.SBV.runSMT'
runSMT :: MonadIO m => SymbolicT m a -> m a
runSMT :: forall (m :: * -> *) a. MonadIO m => SymbolicT m a -> m a
runSMT = forall (m :: * -> *) a.
MonadIO m =>
SMTConfig -> SymbolicT m a -> m a
runSMTWith SMTConfig
defaultSMTCfg

-- | Generalization of 'Data.SBV.runSMTWith'
runSMTWith :: MonadIO m => SMTConfig -> SymbolicT m a -> m a
runSMTWith :: forall (m :: * -> *) a.
MonadIO m =>
SMTConfig -> SymbolicT m a -> m a
runSMTWith SMTConfig
cfg SymbolicT m a
a = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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

-- | Runs with a query.
runWithQuery :: MProvable m a => Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery :: forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
isSAT QueryT m b
q SMTConfig
cfg a
a = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
existential_ else forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
universal_) a
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output
                   forall (m :: * -> *) a.
ExtractIO m =>
QueryContext -> QueryT m a -> SymbolicT m a
Control.executeQuery QueryContext
QueryInternal QueryT m b
q

-- | Check if a safe-call was safe or not, turning a 'SafeResult' to a Bool.
isSafe :: SafeResult -> Bool
isSafe :: SafeResult -> Bool
isSafe (SafeResult (Maybe FilePath
_, FilePath
_, SMTResult
result)) = case SMTResult
result of
                                       Unsatisfiable{} -> Bool
True
                                       Satisfiable{}   -> Bool
False
                                       DeltaSat{}      -> Bool
False   -- conservative
                                       SatExtField{}   -> Bool
False   -- conservative
                                       Unknown{}       -> Bool
False   -- conservative
                                       ProofError{}    -> Bool
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 :: forall b.
NFData b =>
UTCTime
-> (SMTConfig -> IO b)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, b))
runInThread UTCTime
beginTime SMTConfig -> IO b
action SMTConfig
config = forall a. IO a -> IO (Async a)
async forall a b. (a -> b) -> a -> b
$ do
                b
result  <- SMTConfig -> IO b
action SMTConfig
config
                UTCTime
endTime <- forall a. NFData a => a -> ()
rnf b
result seq :: forall a b. a -> b -> b
`seq` IO UTCTime
getCurrentTime
                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)

-- | 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 :: forall b a.
NFData b =>
[SMTConfig]
-> (SMTConfig -> a -> IO b) -> a -> IO (Solver, NominalDiffTime, b)
sbvWithAny []      SMTConfig -> a -> IO b
_    a
_ = forall a. HasCallStack => FilePath -> a
error FilePath
"SBV.withAny: No solvers given!"
sbvWithAny [SMTConfig]
solvers SMTConfig -> a -> IO b
what a
a = do UTCTime
beginTime <- IO UTCTime
getCurrentTime
                               forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {a}. [Async a] -> IO (Async a, a)
waitAnyFastCancel)
   where -- Async's `waitAnyCancel` nicely blocks; so we use this variant to ignore the
         -- wait part for killed threads.
         waitAnyFastCancel :: [Async a] -> IO (Async a, a)
waitAnyFastCancel [Async a]
asyncs = forall {a}. [Async a] -> IO (Async a, a)
waitAny [Async a]
asyncs forall a b. IO a -> IO b -> IO a
`finally` forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {a}. Async a -> IO ()
cancelFast [Async a]
asyncs
         cancelFast :: Async a -> IO ()
cancelFast Async a
other = forall e. Exception e => ThreadId -> e -> IO ()
throwTo (forall a. Async a -> ThreadId
asyncThreadId Async a
other) ExitCode
ExitSuccess


sbvConcurrentWithAny :: NFData c => SMTConfig -> (SMTConfig -> a -> QueryT m b -> IO c) -> [QueryT m b] -> a -> IO (Solver, NominalDiffTime, c)
sbvConcurrentWithAny :: forall c a (m :: * -> *) b.
NFData c =>
SMTConfig
-> (SMTConfig -> a -> QueryT m b -> IO c)
-> [QueryT m b]
-> a
-> IO (Solver, NominalDiffTime, c)
sbvConcurrentWithAny SMTConfig
solver SMTConfig -> a -> QueryT m b -> IO c
what [QueryT m b]
queries a
a = forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM QueryT m b -> IO (Async (Solver, NominalDiffTime, c))
runQueryInThread [QueryT m b]
queries forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {a}. [Async a] -> IO (Async a, a)
waitAnyFastCancel)
  where  -- Async's `waitAnyCancel` nicely blocks; so we use this variant to ignore the
         -- wait part for killed threads.
         waitAnyFastCancel :: [Async a] -> IO (Async a, a)
waitAnyFastCancel [Async a]
asyncs = forall {a}. [Async a] -> IO (Async a, a)
waitAny [Async a]
asyncs forall a b. IO a -> IO b -> IO a
`finally` forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ forall {a}. Async a -> IO ()
cancelFast [Async a]
asyncs
         cancelFast :: Async a -> IO ()
cancelFast Async a
other = forall e. Exception e => ThreadId -> e -> IO ()
throwTo (forall a. Async a -> ThreadId
asyncThreadId Async a
other) ExitCode
ExitSuccess
         runQueryInThread :: QueryT m b -> IO (Async (Solver, NominalDiffTime, c))
runQueryInThread QueryT m b
q = do UTCTime
beginTime <- IO UTCTime
getCurrentTime
                                 forall b.
NFData b =>
UTCTime
-> (SMTConfig -> IO b)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, b))
runInThread UTCTime
beginTime (\SMTConfig
cfg -> SMTConfig -> a -> QueryT m b -> IO c
what SMTConfig
cfg a
a QueryT m b
q) SMTConfig
solver


sbvConcurrentWithAll :: NFData c => SMTConfig -> (SMTConfig -> a -> QueryT m b -> IO c) -> [QueryT m b] -> a -> IO [(Solver, NominalDiffTime, c)]
sbvConcurrentWithAll :: forall c a (m :: * -> *) b.
NFData c =>
SMTConfig
-> (SMTConfig -> a -> QueryT m b -> IO c)
-> [QueryT m b]
-> a
-> IO [(Solver, NominalDiffTime, c)]
sbvConcurrentWithAll SMTConfig
solver SMTConfig -> a -> QueryT m b -> IO c
what [QueryT m b]
queries a
a = forall (t :: * -> *) a b.
Traversable t =>
(a -> IO b) -> t a -> IO (t b)
mapConcurrently QueryT m b -> IO (Async (Solver, NominalDiffTime, c))
runQueryInThread [QueryT m b]
queries  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. IO a -> IO a
unsafeInterleaveIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. [Async a] -> IO [a]
go
  where  runQueryInThread :: QueryT m b -> IO (Async (Solver, NominalDiffTime, c))
runQueryInThread QueryT m b
q = do UTCTime
beginTime <- IO UTCTime
getCurrentTime
                                 forall b.
NFData b =>
UTCTime
-> (SMTConfig -> IO b)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, b))
runInThread UTCTime
beginTime (\SMTConfig
cfg -> SMTConfig -> a -> QueryT m b -> IO c
what SMTConfig
cfg a
a QueryT m b
q) SMTConfig
solver

         go :: [Async a] -> IO [a]
go []  = forall (m :: * -> *) a. Monad m => a -> m a
return []
         go [Async a]
as  = do (Async a
d, a
r) <- forall {a}. [Async a] -> IO (Async a, a)
waitAny [Async a]
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.
                     [a]
rs <- forall a. IO a -> IO a
unsafeInterleaveIO forall a b. (a -> b) -> a -> b
$ [Async a] -> IO [a]
go (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= Async a
d) [Async a]
as)
                     forall (m :: * -> *) a. Monad m => a -> m a
return (a
r forall a. a -> [a] -> [a]
: [a]
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 :: forall b a.
NFData b =>
[SMTConfig]
-> (SMTConfig -> a -> IO b)
-> a
-> IO [(Solver, NominalDiffTime, b)]
sbvWithAll [SMTConfig]
solvers SMTConfig -> a -> IO b
what a
a = do UTCTime
beginTime <- IO UTCTime
getCurrentTime
                               forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (forall a. IO a -> IO a
unsafeInterleaveIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. [Async a] -> IO [a]
go)
   where go :: [Async a] -> IO [a]
go []  = forall (m :: * -> *) a. Monad m => a -> m a
return []
         go [Async a]
as  = do (Async a
d, a
r) <- forall {a}. [Async a] -> IO (Async a, a)
waitAny [Async a]
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.
                     [a]
rs <- forall a. IO a -> IO a
unsafeInterleaveIO forall a b. (a -> b) -> a -> b
$ [Async a] -> IO [a]
go (forall a. (a -> Bool) -> [a] -> [a]
filter (forall a. Eq a => a -> a -> Bool
/= Async a
d) [Async a]
as)
                     forall (m :: * -> *) a. Monad m => a -> m a
return (a
r forall a. a -> [a] -> [a]
: [a]
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.sName'
   sName  :: [String] -> a -> SymbolicT m ()

   -- | Generalization of 'Data.SBV.safe'
   safe :: a -> m [SafeResult]
   safe = forall (m :: * -> *) a.
SExecutable m a =>
SMTConfig -> a -> m [SafeResult]
safeWith SMTConfig
defaultSMTCfg

   -- | Generalization of 'Data.SBV.safeWith'
   safeWith :: SMTConfig -> a -> m [SafeResult]
   safeWith SMTConfig
cfg a
a = do FilePath
cwd <- (forall a. [a] -> [a] -> [a]
++ FilePath
"/") forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO FilePath
getCurrentDirectory
                       let mkRelative :: FilePath -> FilePath
mkRelative FilePath
path
                              | FilePath
cwd forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` FilePath
path = forall a. Int -> [a] -> [a]
drop (forall (t :: * -> *) a. Foldable t => t a -> Int
length FilePath
cwd) FilePath
path
                              | Bool
True                  = FilePath
path
                       forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) (forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ a
a forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (FilePath -> FilePath) -> SymbolicT m [SafeResult]
check FilePath -> FilePath
mkRelative)
     where check :: (FilePath -> FilePath) -> SymbolicT m [SafeResult]
           check :: (FilePath -> FilePath) -> SymbolicT m [SafeResult]
check FilePath -> FilePath
mkRelative = forall (m :: * -> *) a.
ExtractIO m =>
QueryContext -> QueryT m a -> SymbolicT m a
Control.executeQuery QueryContext
QueryInternal forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(FilePath, Maybe CallStack, SV)]
Control.getSBVAssertions forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((FilePath -> FilePath)
-> (FilePath, Maybe CallStack, SV) -> QueryT m SafeResult
verify FilePath -> FilePath
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 :: (FilePath -> FilePath)
-> (FilePath, Maybe CallStack, SV) -> QueryT m SafeResult
verify FilePath -> FilePath
mkRelative (FilePath
msg, Maybe CallStack
cs, SV
cond) = do
                   let locInfo :: [(FilePath, SrcLoc)] -> FilePath
locInfo [(FilePath, SrcLoc)]
ps = let loc :: (FilePath, SrcLoc) -> FilePath
loc (FilePath
f, SrcLoc
sl) = forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [FilePath -> FilePath
mkRelative (SrcLoc -> FilePath
srcLocFile SrcLoc
sl), FilePath
":", forall a. Show a => a -> FilePath
show (SrcLoc -> Int
srcLocStartLine SrcLoc
sl), FilePath
":", forall a. Show a => a -> FilePath
show (SrcLoc -> Int
srcLocStartCol SrcLoc
sl), FilePath
":", FilePath
f]
                                    in forall a. [a] -> [[a]] -> [a]
intercalate FilePath
",\n " (forall a b. (a -> b) -> [a] -> [b]
map (FilePath, SrcLoc) -> FilePath
loc [(FilePath, SrcLoc)]
ps)
                       location :: Maybe FilePath
location   = ([(FilePath, SrcLoc)] -> FilePath
locInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> [(FilePath, SrcLoc)]
getCallStack) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Maybe CallStack
cs

                   SMTResult
result <- do forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
Control.push Int
1
                                forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> FilePath -> m ()
Control.send Bool
True forall a b. (a -> b) -> a -> b
$ FilePath
"(assert " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> FilePath
show SV
cond forall a. [a] -> [a] -> [a]
++ FilePath
")"
                                SMTResult
r <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
Control.getSMTResult
                                forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
Control.pop Int
1
                                forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
r

                   forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Maybe FilePath, FilePath, SMTResult) -> SafeResult
SafeResult (Maybe FilePath
location, FilePath
msg, SMTResult
result)

instance (ExtractIO m, NFData a) => SExecutable m (SymbolicT m a) where
   sName_ :: SymbolicT m a -> SymbolicT m ()
sName_   SymbolicT m a
a = SymbolicT m a
a forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
r -> forall a. NFData a => a -> ()
rnf a
r seq :: forall a b. a -> b -> b
`seq` forall (m :: * -> *) a. Monad m => a -> m a
return ()
   sName :: [FilePath] -> SymbolicT m a -> SymbolicT m ()
sName []   = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_
   sName [FilePath]
xs   = forall a. HasCallStack => FilePath -> a
error forall a b. (a -> b) -> a -> b
$ FilePath
"SBV.SExecutable.sName: Extra unmapped name(s): " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate FilePath
", " [FilePath]
xs

instance ExtractIO m => SExecutable m (SBV a) where
   sName_ :: SBV a -> SymbolicT m ()
sName_   SBV a
v = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_   (forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
v :: SymbolicT m (SBV a))
   sName :: [FilePath] -> SBV a -> SymbolicT m ()
sName [FilePath]
xs SBV a
v = forall (m :: * -> *) a.
SExecutable m a =>
[FilePath] -> a -> SymbolicT m ()
sName [FilePath]
xs (forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
v :: SymbolicT m (SBV a))

-- Unit output
instance ExtractIO m => SExecutable m () where
   sName_ :: () -> SymbolicT m ()
sName_   () = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_   (forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output () :: SymbolicT m ())
   sName :: [FilePath] -> () -> SymbolicT m ()
sName [FilePath]
xs () = forall (m :: * -> *) a.
SExecutable m a =>
[FilePath] -> a -> SymbolicT m ()
sName [FilePath]
xs (forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output () :: SymbolicT m ())

-- List output
instance ExtractIO m => SExecutable m [SBV a] where
   sName_ :: [SBV a] -> SymbolicT m ()
sName_   [SBV a]
vs = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_   (forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output [SBV a]
vs :: SymbolicT m [SBV a])
   sName :: [FilePath] -> [SBV a] -> SymbolicT m ()
sName [FilePath]
xs [SBV a]
vs = forall (m :: * -> *) a.
SExecutable m a =>
[FilePath] -> a -> SymbolicT m ()
sName [FilePath]
xs (forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output [SBV a]
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_ :: (SBV a, SBV b) -> SymbolicT m ()
sName_ (SBV a
a, SBV b
b) = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
a forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV b
b :: SymbolicT m (SBV b))
  sName :: [FilePath] -> (SBV a, SBV b) -> SymbolicT m ()
sName [FilePath]
_       = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_

-- 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_ :: (SBV a, SBV b, SBV c) -> SymbolicT m ()
sName_ (SBV a
a, SBV b
b, SBV c
c) = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
a forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV b
b forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV c
c :: SymbolicT m (SBV c))
  sName :: [FilePath] -> (SBV a, SBV b, SBV c) -> SymbolicT m ()
sName [FilePath]
_          = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_

-- 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_ :: (SBV a, SBV b, SBV c, SBV d) -> SymbolicT m ()
sName_ (SBV a
a, SBV b
b, SBV c
c, SBV d
d) = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
a forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV b
b forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV c
c forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV c
c forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV d
d :: SymbolicT m (SBV d))
  sName :: [FilePath] -> (SBV a, SBV b, SBV c, SBV d) -> SymbolicT m ()
sName [FilePath]
_             = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_

-- 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_ :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> SymbolicT m ()
sName_ (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e) = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
a forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV b
b forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV c
c forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV d
d forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV e
e :: SymbolicT m (SBV e))
  sName :: [FilePath] -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> SymbolicT m ()
sName [FilePath]
_                = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_

-- 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_ :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> SymbolicT m ()
sName_ (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f) = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
a forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV b
b forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV c
c forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV d
d forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV e
e forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV f
f :: SymbolicT m (SBV f))
  sName :: [FilePath]
-> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> SymbolicT m ()
sName [FilePath]
_                   = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_

-- 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_ :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> SymbolicT m ()
sName_ (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g) = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV a
a forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV b
b forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV c
c forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV d
d forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV e
e forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV f
f forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output SBV g
g :: SymbolicT m (SBV g))
  sName :: [FilePath]
-> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g)
-> SymbolicT m ()
sName [FilePath]
_                      = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_

-- Functions
instance (SymVal a, SExecutable m p) => SExecutable m (SBV a -> p) where
   sName_ :: (SBV a -> p) -> SymbolicT m ()
sName_        SBV a -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvExists_   forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_   forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a
   sName :: [FilePath] -> (SBV a -> p) -> SymbolicT m ()
sName (FilePath
s:[FilePath]
ss)  SBV a -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvExists FilePath
s  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
SExecutable m a =>
[FilePath] -> a -> SymbolicT m ()
sName [FilePath]
ss forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a
   sName []      SBV a -> p
k = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ SBV a -> p
k

-- 2 Tuple input
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_        (SBV a, SBV b) -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvExists_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_   forall a b. (a -> b) -> a -> b
$ \SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)
  sName :: [FilePath] -> ((SBV a, SBV b) -> p) -> SymbolicT m ()
sName (FilePath
s:[FilePath]
ss)  (SBV a, SBV b) -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvExists FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
SExecutable m a =>
[FilePath] -> a -> SymbolicT m ()
sName [FilePath]
ss forall a b. (a -> b) -> a -> b
$ \SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)
  sName []      (SBV a, SBV b) -> p
k = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a, SBV b) -> p
k

-- 3 Tuple input
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_       (SBV a, SBV b, SBV c) -> p
k  = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvExists_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_   forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c -> (SBV a, SBV b, SBV c) -> p
k (SBV a
a, SBV b
b, SBV c
c)
  sName :: [FilePath] -> ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m ()
sName (FilePath
s:[FilePath]
ss) (SBV a, SBV b, SBV c) -> p
k  = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvExists FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
SExecutable m a =>
[FilePath] -> a -> SymbolicT m ()
sName [FilePath]
ss forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c -> (SBV a, SBV b, SBV c) -> p
k (SBV a
a, SBV b
b, SBV c
c)
  sName []     (SBV a, SBV b, SBV c) -> p
k  = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a, SBV b, SBV c) -> p
k

-- 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_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m ()
sName_        (SBV a, SBV b, SBV c, SBV d) -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvExists_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_   forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c 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 :: [FilePath] -> ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m ()
sName (FilePath
s:[FilePath]
ss)  (SBV a, SBV b, SBV c, SBV d) -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvExists FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
SExecutable m a =>
[FilePath] -> a -> SymbolicT m ()
sName [FilePath]
ss forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c 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 []      (SBV a, SBV b, SBV c, SBV d) -> p
k = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a, SBV b, SBV c, SBV d) -> p
k

-- 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_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m ()
sName_        (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvExists_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_   forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d 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 :: [FilePath]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m ()
sName (FilePath
s:[FilePath]
ss)  (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvExists FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
SExecutable m a =>
[FilePath] -> a -> SymbolicT m ()
sName [FilePath]
ss forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d 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 []      (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k

-- 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_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> SymbolicT m ()
sName_        (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvExists_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_   forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e 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 :: [FilePath]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m ()
sName (FilePath
s:[FilePath]
ss)  (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvExists FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
SExecutable m a =>
[FilePath] -> a -> SymbolicT m ()
sName [FilePath]
ss forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e 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 []      (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k

-- 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_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m ()
sName_        (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
sbvExists_  forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_   forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f 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 :: [FilePath]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m ()
sName (FilePath
s:[FilePath]
ss)  (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
FilePath -> m (SBV a)
sbvExists FilePath
s forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> forall (m :: * -> *) a.
SExecutable m a =>
[FilePath] -> a -> SymbolicT m ()
sName [FilePath]
ss forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f 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 []      (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = 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) #-}