-----------------------------------------------------------------------------
-- |
-- 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
       , boolector, cvc4, yices, dReal, z3, mathSAT, abc, 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 Data.SBV.Core.Data
import Data.SBV.Core.Symbolic
import Data.SBV.SMT.SMT
import Data.SBV.SMT.Utils (debug, alignPlain)
import Data.SBV.Utils.ExtractIO
import Data.SBV.Utils.TDiff

import qualified Data.SBV.Trans.Control as Control
import qualified Data.SBV.Control.Query as Control
import qualified Data.SBV.Control.Utils as Control

import GHC.Stack

import qualified Data.SBV.Provers.Boolector  as Boolector
import qualified Data.SBV.Provers.CVC4       as CVC4
import qualified Data.SBV.Provers.Yices      as Yices
import qualified Data.SBV.Provers.DReal      as DReal
import qualified Data.SBV.Provers.Z3         as Z3
import qualified Data.SBV.Provers.MathSAT    as MathSAT
import qualified Data.SBV.Provers.ABC        as ABC

mkConfig :: SMTSolver -> SMTLibVersion -> [Control.SMTOption] -> SMTConfig
mkConfig :: SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
s SMTLibVersion
smtVersion [SMTOption]
startOpts = SMTConfig :: Bool
-> Timing
-> Int
-> Int
-> String
-> Maybe Int
-> Bool
-> Bool
-> (String -> Bool)
-> Bool
-> Bool
-> Maybe String
-> SMTLibVersion
-> Maybe Double
-> SMTSolver
-> [String]
-> Bool
-> RoundingMode
-> [SMTOption]
-> Bool
-> Maybe String
-> SMTConfig
SMTConfig { verbose :: Bool
verbose                     = Bool
False
                                            , timing :: Timing
timing                      = Timing
NoTiming
                                            , printBase :: Int
printBase                   = Int
10
                                            , printRealPrec :: Int
printRealPrec               = Int
16
                                            , transcript :: Maybe String
transcript                  = Maybe String
forall a. Maybe a
Nothing
                                            , solver :: SMTSolver
solver                      = SMTSolver
s
                                            , smtLibVersion :: SMTLibVersion
smtLibVersion               = SMTLibVersion
smtVersion
                                            , dsatPrecision :: Maybe Double
dsatPrecision               = Maybe Double
forall a. Maybe a
Nothing
                                            , extraArgs :: [String]
extraArgs                   = []
                                            , satCmd :: String
satCmd                      = String
"(check-sat)"
                                            , satTrackUFs :: Bool
satTrackUFs                 = Bool
True                   -- i.e., yes, do extract UI function values
                                            , allSatMaxModelCount :: Maybe Int
allSatMaxModelCount         = Maybe Int
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 :: String -> Bool
isNonModelVar               = Bool -> String -> Bool
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 String
redirectVerbose             = Maybe String
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 = String -> SMTOption
Control.DiagnosticOutputChannel String
"stdout"

-- | 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 CVC4 SMT Solver.
cvc4 :: SMTConfig
cvc4 :: SMTConfig
cvc4 = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
CVC4.cvc4 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 Yices SMT Solver.
dReal :: SMTConfig
dReal :: SMTConfig
dReal = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
DReal.dReal SMTLibVersion
SMTLib2 [ String -> [String] -> SMTOption
Control.OptionKeyword String
":smtlib2_compliant" [String
"true"]
                                     ]

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

-- | 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 ABC synthesis and verification tool.
abc :: SMTConfig
abc :: SMTConfig
abc = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
ABC.abc SMTLibVersion
SMTLib2 [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.forAll_'
  forAll_ :: a -> SymbolicT m SBool

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

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

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

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

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

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

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

  -- | Generalization of 'Data.SBV.allSat'
  allSat :: a -> m AllSatResult
  allSat = SMTConfig -> a -> m AllSatResult
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 <- Bool -> QueryT m AllSatResult -> SMTConfig -> a -> m AllSatResult
forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
True (QueryT m ()
forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations QueryT m () -> QueryT m AllSatResult -> QueryT m AllSatResult
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QueryT m AllSatResult
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' <- (SMTResult -> m SMTResult) -> [SMTResult] -> m [SMTResult]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
forall (m :: * -> *) a.
MProvable m a =>
Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
validate Bool
True SMTConfig
cfg a
a) (AllSatResult -> [SMTResult]
allSatResults AllSatResult
asr)
                                   AllSatResult -> m AllSatResult
forall (m :: * -> *) a. Monad m => a -> m a
return AllSatResult
asr{allSatResults :: [SMTResult]
allSatResults = [SMTResult]
rs'}
                           else AllSatResult -> m AllSatResult
forall (m :: * -> *) a. Monad m => a -> m a
return AllSatResult
asr

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

  -- | Generalization of 'Data.SBV.optimizeWith'
  optimizeWith :: SMTConfig -> OptimizeStyle -> a -> m OptimizeResult
  optimizeWith SMTConfig
config OptimizeStyle
style a
optGoal = do
                   OptimizeResult
res <- Bool
-> QueryT m OptimizeResult -> SMTConfig -> a -> m OptimizeResult
forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
True QueryT m OptimizeResult
opt SMTConfig
config a
optGoal
                   if Bool -> Bool
not (SMTConfig -> Bool
optimizeValidateConstraints SMTConfig
config)
                      then OptimizeResult -> m OptimizeResult
forall (m :: * -> *) a. Monad m => a -> m a
return OptimizeResult
res
                      else let v :: SMTResult -> m SMTResult
                               v :: SMTResult -> m SMTResult
v = Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
forall (m :: * -> *) a.
MProvable m a =>
Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
validate Bool
True SMTConfig
config a
optGoal
                           in case OptimizeResult
res of
                                LexicographicResult SMTResult
m -> SMTResult -> OptimizeResult
LexicographicResult (SMTResult -> OptimizeResult) -> m SMTResult -> m OptimizeResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SMTResult -> m SMTResult
v SMTResult
m
                                IndependentResult [(String, SMTResult)]
xs  -> let w :: [(a, SMTResult)] -> [(a, SMTResult)] -> m [(a, SMTResult)]
w []            [(a, SMTResult)]
sofar = [(a, SMTResult)] -> m [(a, SMTResult)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(a, SMTResult)] -> [(a, SMTResult)]
forall a. [a] -> [a]
reverse [(a, SMTResult)]
sofar)
                                                             w ((a
n, SMTResult
m):[(a, SMTResult)]
rest) [(a, SMTResult)]
sofar = SMTResult -> m SMTResult
v SMTResult
m m SMTResult
-> (SMTResult -> m [(a, SMTResult)]) -> m [(a, SMTResult)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SMTResult
m' -> [(a, SMTResult)] -> [(a, SMTResult)] -> m [(a, SMTResult)]
w [(a, SMTResult)]
rest ((a
n, SMTResult
m') (a, SMTResult) -> [(a, SMTResult)] -> [(a, SMTResult)]
forall a. a -> [a] -> [a]
: [(a, SMTResult)]
sofar)
                                                         in [(String, SMTResult)] -> OptimizeResult
IndependentResult ([(String, SMTResult)] -> OptimizeResult)
-> m [(String, SMTResult)] -> m OptimizeResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(String, SMTResult)]
-> [(String, SMTResult)] -> m [(String, SMTResult)]
forall a.
[(a, SMTResult)] -> [(a, SMTResult)] -> m [(a, SMTResult)]
w [(String, SMTResult)]
xs []
                                ParetoResult (Bool
b, [SMTResult]
rs)  -> (Bool, [SMTResult]) -> OptimizeResult
ParetoResult ((Bool, [SMTResult]) -> OptimizeResult)
-> ([SMTResult] -> (Bool, [SMTResult]))
-> [SMTResult]
-> OptimizeResult
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool
b, ) ([SMTResult] -> OptimizeResult)
-> m [SMTResult] -> m OptimizeResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SMTResult -> m SMTResult) -> [SMTResult] -> m [SMTResult]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SMTResult -> m SMTResult
v [SMTResult]
rs

    where opt :: QueryT m OptimizeResult
opt = do [Objective (SV, SV)]
objectives <- QueryT m [Objective (SV, SV)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [Objective (SV, SV)]
Control.getObjectives
                   [(Quantifier, NamedSymVar)]
qinps      <- QueryT m [(Quantifier, NamedSymVar)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(Quantifier, NamedSymVar)]
Control.getQuantifiedInputs
                   SBVPgm
spgm       <- QueryT m SBVPgm
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SBVPgm
Control.getSBVPgm

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

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

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


                   let universals :: [NamedSymVar]
universals = [NamedSymVar
s | (Quantifier
ALL, NamedSymVar
s) <- [(Quantifier, NamedSymVar)]
qinps]

                       firstUniversal :: NodeId
firstUniversal
                         | [NamedSymVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedSymVar]
universals = String -> NodeId
forall a. HasCallStack => String -> a
error String
"Data.SBV: Impossible happened! Universal optimization with no universals!"
                         | Bool
True            = [NodeId] -> NodeId
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum ((NamedSymVar -> NodeId) -> [NamedSymVar] -> [NodeId]
forall a b. (a -> b) -> [a] -> [b]
map (SV -> NodeId
nodeId (SV -> NodeId) -> (NamedSymVar -> SV) -> NamedSymVar -> NodeId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedSymVar -> SV
forall a b. (a, b) -> a
fst) [NamedSymVar]
universals)

                       nodeId :: SV -> NodeId
nodeId (SV Kind
_ NodeId
n) = NodeId
n

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

                       chaseUniversal :: SV -> [String]
chaseUniversal SV
entry = (NamedSymVar -> String) -> [NamedSymVar] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map NamedSymVar -> String
forall a b. (a, b) -> b
snd ([NamedSymVar] -> [String]) -> [NamedSymVar] -> [String]
forall a b. (a -> b) -> a -> b
$ SV -> [NamedSymVar] -> [NamedSymVar]
go SV
entry []
                         where go :: SV -> [NamedSymVar] -> [NamedSymVar]
go SV
x [NamedSymVar]
sofar
                                | NodeId
nx NodeId -> NodeId -> Bool
forall a. Ord a => a -> a -> Bool
>= NodeId
firstUniversal
                                = [NamedSymVar] -> [NamedSymVar]
forall a. Eq a => [a] -> [a]
nub ([NamedSymVar] -> [NamedSymVar]) -> [NamedSymVar] -> [NamedSymVar]
forall a b. (a -> b) -> a -> b
$ [NamedSymVar
unm | unm :: NamedSymVar
unm@(SV
u, String
_) <- [NamedSymVar]
universals, NodeId
nx NodeId -> NodeId -> Bool
forall a. Ord a => a -> a -> Bool
>= SV -> NodeId
nodeId SV
u] [NamedSymVar] -> [NamedSymVar] -> [NamedSymVar]
forall a. [a] -> [a] -> [a]
++ [NamedSymVar]
sofar
                                | Bool
True
                                = let oVars :: Op -> [SV]
oVars (LkUp (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 SV -> Map SV SBVExpr -> Maybe SBVExpr
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) -> [SV] -> [SV]
forall a. Eq a => [a] -> [a]
nub (Op -> [SV]
oVars Op
o [SV] -> [SV] -> [SV]
forall a. [a] -> [a] -> [a]
++ [SV]
ss)
                                  in (SV -> [NamedSymVar] -> [NamedSymVar])
-> [NamedSymVar] -> [SV] -> [NamedSymVar]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SV -> [NamedSymVar] -> [NamedSymVar]
go [NamedSymVar]
sofar [SV]
vars
                                where nx :: NodeId
nx = SV -> NodeId
nodeId SV
x

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

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

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

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

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

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

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

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

  -- | Generalization of 'Data.SBV.isVacuous'
  isVacuous :: a -> m Bool
  isVacuous = SMTConfig -> a -> m Bool
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!
       (Bool, Result) -> Bool
forall a b. (a, b) -> a
fst ((Bool, Result) -> Bool) -> m (Bool, Result) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBVRunMode -> SymbolicT m Bool -> m (Bool, Result)
forall (m :: * -> *) a.
MonadIO m =>
SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
SMTMode QueryContext
QueryInternal IStage
ISetup Bool
True SMTConfig
cfg) (a -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ a
a SymbolicT m SBool -> SymbolicT m Bool -> SymbolicT m Bool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QueryContext -> QueryT m Bool -> SymbolicT m Bool
forall (m :: * -> *) a.
ExtractIO m =>
QueryContext -> QueryT m a -> SymbolicT m a
Control.executeQuery QueryContext
QueryInternal QueryT m Bool
check)
     where
       check :: QueryT m Bool
       check :: QueryT m Bool
check = do CheckSatResult
cs <- QueryT m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
Control.checkSat
                  case CheckSatResult
cs of
                    CheckSatResult
Control.Unsat  -> Bool -> QueryT m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                    CheckSatResult
Control.Sat    -> Bool -> QueryT m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                    Control.DSat{} -> Bool -> QueryT m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                    CheckSatResult
Control.Unk    -> String -> QueryT m Bool
forall a. HasCallStack => String -> a
error String
"SBV: isVacuous: Solver returned unknown!"

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

  -- | Generalization of 'Data.SBV.isSatisfiable'
  isSatisfiable :: a -> m Bool
  isSatisfiable = SMTConfig -> a -> m Bool
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 <- SMTConfig -> a -> m SatResult
forall (m :: * -> *) a.
MProvable m a =>
SMTConfig -> a -> m SatResult
satWith SMTConfig
cfg a
p
                               case SatResult
r of
                                 SatResult Satisfiable{}   -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                                 SatResult Unsatisfiable{} -> Bool -> m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                                 SatResult
_                         -> String -> m Bool
forall a. HasCallStack => String -> a
error (String -> m Bool) -> String -> m Bool
forall a b. (a -> b) -> a -> b
$ String
"SBV.isSatisfiable: Received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SatResult -> String
forall a. Show a => a -> String
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{} -> SMTResult -> m SMTResult
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  -> String -> m SMTResult
forall a. HasCallStack => String -> a
error String
"Data.SBV.validate: Impossible happened; no bindings generated during model validation."
                                                    Just [((Quantifier, NamedSymVar), Maybe CV)]
env -> [((Quantifier, NamedSymVar), Maybe CV)] -> m SMTResult
forall (m :: * -> *).
MProvable m a =>
[((Quantifier, NamedSymVar), Maybe CV)] -> m SMTResult
check [((Quantifier, NamedSymVar), Maybe CV)]
env

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                             -- SAT: All outputs must be true
                             satLoop :: [SV] -> m SMTResult
satLoop []
                               = do String -> m ()
forall (m :: * -> *). MonadIO m => String -> m ()
notify String
"All outputs are satisfied. Validation complete."
                                    SMTResult -> m SMTResult
forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
res
                             satLoop (SV
sv:[SV]
svs)
                               | SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
sv Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind
KBool
                               = String -> m SMTResult
forall (m :: * -> *). Monad m => String -> m SMTResult
giveUp (String -> m SMTResult) -> String -> m SMTResult
forall a b. (a -> b) -> a -> b
$ String
"Output tied to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
sv String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is non-boolean."
                               | SV
sv SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV
                               = [SV] -> m SMTResult
satLoop [SV]
svs
                               | SV
sv SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV
                               = String -> m SMTResult
forall (m :: * -> *). Monad m => String -> m SMTResult
badModel String
"Final output evaluated to False."
                               | Bool
True
                               = SV -> m SMTResult
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 String -> m ()
forall (m :: * -> *). MonadIO m => String -> m ()
notify String
"Counterexample is validated."
                                                      SMTResult -> m SMTResult
forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
res
                               | Bool
True            = do String -> m ()
forall (m :: * -> *). MonadIO m => String -> m ()
notify String
"Counterexample violates none of the outputs."
                                                      String -> m SMTResult
forall (m :: * -> *). Monad m => String -> m SMTResult
badModel String
"Counter-example violates no constraints."
                             proveLoop (SV
sv:[SV]
svs) Bool
somethingFailed
                               | SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
sv Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind
KBool
                               = String -> m SMTResult
forall (m :: * -> *). Monad m => String -> m SMTResult
giveUp (String -> m SMTResult) -> String -> m SMTResult
forall a b. (a -> b) -> a -> b
$ String
"Output tied to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
sv String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is non-boolean."
                               | SV
sv SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV
                               = [SV] -> Bool -> m SMTResult
proveLoop [SV]
svs Bool
somethingFailed
                               | SV
sv SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV
                               = [SV] -> Bool -> m SMTResult
proveLoop [SV]
svs Bool
True
                               | Bool
True
                               = SV -> m SMTResult
forall (m :: * -> *). Monad m => SV -> m SMTResult
notConcrete SV
sv

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

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

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

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

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

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

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

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

-- | 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 :: SMTConfig
-> [Query b] -> a -> IO (Solver, NominalDiffTime, ThmResult)
proveConcurrentWithAny SMTConfig
solver [Query b]
qs a
a = do (Solver
slvr,NominalDiffTime
time,SMTResult
result) <- SMTConfig
-> (SMTConfig -> a -> Query b -> IO SMTResult)
-> [Query b]
-> a
-> IO (Solver, NominalDiffTime, SMTResult)
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 -> Query b -> IO SMTResult
forall (m :: * -> *) a a.
MProvable m a =>
SMTConfig -> a -> QueryT m a -> m SMTResult
go [Query b]
qs a
a
                                        (Solver, NominalDiffTime, ThmResult)
-> IO (Solver, NominalDiffTime, ThmResult)
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 = Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
False (do a
_ <- QueryT m a
q;  QueryT m ()
forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QueryT m SMTResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
Control.getSMTResult) SMTConfig
cfg a
a'

-- | 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 :: SMTConfig
-> [Query b] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
satConcurrentWithAll SMTConfig
solver [Query b]
qs a
a = do [(Solver, NominalDiffTime, SMTResult)]
results <- SMTConfig
-> (SMTConfig -> a -> Query b -> IO SMTResult)
-> [Query b]
-> a
-> IO [(Solver, NominalDiffTime, SMTResult)]
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 -> Query b -> IO SMTResult
forall (m :: * -> *) a a.
MProvable m a =>
SMTConfig -> a -> QueryT m a -> m SMTResult
go [Query b]
qs a
a
                                      [(Solver, NominalDiffTime, SatResult)]
-> IO [(Solver, NominalDiffTime, SatResult)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Solver, NominalDiffTime, SatResult)]
 -> IO [(Solver, NominalDiffTime, SatResult)])
-> [(Solver, NominalDiffTime, SatResult)]
-> IO [(Solver, NominalDiffTime, SatResult)]
forall a b. (a -> b) -> a -> b
$ (\(Solver
a',NominalDiffTime
b,SMTResult
c) -> (Solver
a',NominalDiffTime
b,SMTResult -> SatResult
SatResult SMTResult
c)) ((Solver, NominalDiffTime, SMTResult)
 -> (Solver, NominalDiffTime, SatResult))
-> [(Solver, NominalDiffTime, SMTResult)]
-> [(Solver, NominalDiffTime, SatResult)]
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 = Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
True (do a
_ <- QueryT m a
q; QueryT m ()
forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QueryT m SMTResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
Control.getSMTResult) SMTConfig
cfg a
a'

-- | 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 :: SMTConfig
-> [Query b] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
proveConcurrentWithAll SMTConfig
solver [Query b]
qs a
a = do [(Solver, NominalDiffTime, SMTResult)]
results <- SMTConfig
-> (SMTConfig -> a -> Query b -> IO SMTResult)
-> [Query b]
-> a
-> IO [(Solver, NominalDiffTime, SMTResult)]
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 -> Query b -> IO SMTResult
forall (m :: * -> *) a a.
MProvable m a =>
SMTConfig -> a -> QueryT m a -> m SMTResult
go [Query b]
qs a
a
                                        [(Solver, NominalDiffTime, ThmResult)]
-> IO [(Solver, NominalDiffTime, ThmResult)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Solver, NominalDiffTime, ThmResult)]
 -> IO [(Solver, NominalDiffTime, ThmResult)])
-> [(Solver, NominalDiffTime, ThmResult)]
-> IO [(Solver, NominalDiffTime, ThmResult)]
forall a b. (a -> b) -> a -> b
$ (\(Solver
a',NominalDiffTime
b,SMTResult
c) -> (Solver
a',NominalDiffTime
b,SMTResult -> ThmResult
ThmResult SMTResult
c)) ((Solver, NominalDiffTime, SMTResult)
 -> (Solver, NominalDiffTime, ThmResult))
-> [(Solver, NominalDiffTime, SMTResult)]
-> [(Solver, NominalDiffTime, ThmResult)]
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 = Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
False (do a
_ <- QueryT m a
q; QueryT m ()
forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QueryT m SMTResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
Control.getSMTResult) SMTConfig
cfg a
a'

-- | 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 :: Bool -> a -> m String
generateSMTBenchmark Bool
isSat a
a = do
      ZonedTime
t <- IO ZonedTime -> m ZonedTime
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ZonedTime
getZonedTime

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

      (SBool
_, Result
res) <- SBVRunMode -> SymbolicT m SBool -> m (SBool, Result)
forall (m :: * -> *) a.
MonadIO m =>
SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
SMTMode QueryContext
QueryInternal IStage
ISetup Bool
isSat SMTConfig
cfg) (SymbolicT m SBool -> m (SBool, Result))
-> SymbolicT m SBool -> m (SBool, Result)
forall a b. (a -> b) -> a -> b
$ (if Bool
isSat then a -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ else a -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_) a
a SymbolicT m SBool
-> (SBool -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SBool -> SymbolicT m SBool
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output

      let SMTProblem{SMTConfig -> SMTLibPgm
smtLibPgm :: SMTProblem -> SMTConfig -> SMTLibPgm
smtLibPgm :: SMTConfig -> SMTLibPgm
smtLibPgm} = SBVRunMode -> QueryContext -> [String] -> Result -> SMTProblem
Control.runProofOn (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
SMTMode QueryContext
QueryInternal IStage
IRun Bool
isSat SMTConfig
cfg) QueryContext
QueryInternal [String]
comments Result
res
          out :: String
out                   = SMTLibPgm -> String
forall a. Show a => a -> String
show (SMTConfig -> SMTLibPgm
smtLibPgm SMTConfig
cfg)

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

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

                          Bool -> QueryT m () -> QueryT m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Objective (SV, SV)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Objective (SV, SV)]
objectives) (QueryT m () -> QueryT m ()) -> QueryT m () -> QueryT m ()
forall a b. (a -> b) -> a -> b
$
                                String -> QueryT m ()
forall a. HasCallStack => String -> a
error (String -> QueryT m ()) -> String -> QueryT m ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                , String
"*** Data.SBV: Unsupported call sat/prove when optimization objectives are present."
                                                , String
"*** 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
  forAll_ :: SymbolicT m () -> SymbolicT m SBool
forAll_    SymbolicT m ()
a = SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_    ((SymbolicT m ()
a SymbolicT m () -> SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return SBool
sTrue) :: SymbolicT m SBool)
  forAll :: [String] -> SymbolicT m () -> SymbolicT m SBool
forAll [String]
ns  SymbolicT m ()
a = [String] -> SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ns  ((SymbolicT m ()
a SymbolicT m () -> SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return SBool
sTrue) :: SymbolicT m SBool)
  forSome_ :: SymbolicT m () -> SymbolicT m SBool
forSome_   SymbolicT m ()
a = SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_   ((SymbolicT m ()
a SymbolicT m () -> SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return SBool
sTrue) :: SymbolicT m SBool)
  forSome :: [String] -> SymbolicT m () -> SymbolicT m SBool
forSome [String]
ns SymbolicT m ()
a = [String] -> SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ns ((SymbolicT m ()
a SymbolicT m () -> SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return SBool
sTrue) :: SymbolicT m SBool)

instance ExtractIO m => MProvable m (SymbolicT m SBool) where
  forAll_ :: SymbolicT m SBool -> SymbolicT m SBool
forAll_    = SymbolicT m SBool -> SymbolicT m SBool
forall a. a -> a
id
  forAll :: [String] -> SymbolicT m SBool -> SymbolicT m SBool
forAll []  = SymbolicT m SBool -> SymbolicT m SBool
forall a. a -> a
id
  forAll [String]
xs  = String -> SymbolicT m SBool -> SymbolicT m SBool
forall a. HasCallStack => String -> a
error (String -> SymbolicT m SBool -> SymbolicT m SBool)
-> String -> SymbolicT m SBool -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ String
"SBV.forAll: Extra unmapped name(s) in predicate construction: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
xs
  forSome_ :: SymbolicT m SBool -> SymbolicT m SBool
forSome_   = SymbolicT m SBool -> SymbolicT m SBool
forall a. a -> a
id
  forSome :: [String] -> SymbolicT m SBool -> SymbolicT m SBool
forSome [] = SymbolicT m SBool -> SymbolicT m SBool
forall a. a -> a
id
  forSome [String]
xs = String -> SymbolicT m SBool -> SymbolicT m SBool
forall a. HasCallStack => String -> a
error (String -> SymbolicT m SBool -> SymbolicT m SBool)
-> String -> SymbolicT m SBool -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ String
"SBV.forSome: Extra unmapped name(s) in predicate construction: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
xs

instance ExtractIO m => MProvable m SBool where
  forAll_ :: SBool -> SymbolicT m SBool
forAll_   = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return
  forAll :: [String] -> SBool -> SymbolicT m SBool
forAll [String]
_  = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return
  forSome_ :: SBool -> SymbolicT m SBool
forSome_  = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return
  forSome :: [String] -> SBool -> SymbolicT m SBool
forSome [String]
_ = SBool -> SymbolicT m SBool
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
  forAll_  x  = forAll_   (if x then true else false :: SBool)
  forAll s x  = forAll s  (if x then true else false :: SBool)
  forSome_  x = forSome_  (if x then true else false :: SBool)
  forSome s x = forSome s (if x then true else false :: SBool)
-}

-- Functions
instance (SymVal a, MProvable m p) => MProvable m (SBV a -> p) where
  forAll_ :: (SBV a -> p) -> SymbolicT m SBool
forAll_        SBV a -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_   SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> p -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_   (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a
  forAll :: [String] -> (SBV a -> p) -> SymbolicT m SBool
forAll (String
s:[String]
ss)  SBV a -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
forall String
s  SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> [String] -> p -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a
  forAll []      SBV a -> p
k = (SBV a -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ SBV a -> p
k
  forSome_ :: (SBV a -> p) -> SymbolicT m SBool
forSome_       SBV a -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_  SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> p -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_   (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a
  forSome :: [String] -> (SBV a -> p) -> SymbolicT m SBool
forSome (String
s:[String]
ss) SBV a -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> [String] -> p -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ss (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a
  forSome []     SBV a -> p
k = (SBV a -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ SBV a -> p
k

-- SFunArrays (memory, functional representation), only supported universally for the time being
instance (HasKind a, HasKind b, MProvable m p) => MProvable m (SArray a b -> p) where
  forAll_ :: (SArray a b -> p) -> SymbolicT m SBool
forAll_        SArray a b -> p
k = Maybe (SBV b) -> SymbolicT m (SArray a b)
forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
Maybe (SBV b) -> m (array a b)
newArray_  Maybe (SBV b)
forall a. Maybe a
Nothing SymbolicT m (SArray a b)
-> (SArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SArray a b
a -> p -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_   (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SArray a b -> p
k SArray a b
a
  forAll :: [String] -> (SArray a b -> p) -> SymbolicT m SBool
forAll  (String
s:[String]
ss) SArray a b -> p
k = String -> Maybe (SBV b) -> SymbolicT m (SArray a b)
forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
String -> Maybe (SBV b) -> m (array a b)
newArray String
s Maybe (SBV b)
forall a. Maybe a
Nothing SymbolicT m (SArray a b)
-> (SArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SArray a b
a -> [String] -> p -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SArray a b -> p
k SArray a b
a
  forAll  []     SArray a b -> p
k = (SArray a b -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ SArray a b -> p
k
  forSome_ :: (SArray a b -> p) -> SymbolicT m SBool
forSome_       SArray a b -> p
k = Maybe (SBV b) -> SymbolicT m (SArray a b)
forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
Maybe (SBV b) -> m (array a b)
newArray_  Maybe (SBV b)
forall a. Maybe a
Nothing SymbolicT m (SArray a b)
-> (SArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SArray a b
a -> p -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_   (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SArray a b -> p
k SArray a b
a
  forSome :: [String] -> (SArray a b -> p) -> SymbolicT m SBool
forSome (String
s:[String]
ss) SArray a b -> p
k = String -> Maybe (SBV b) -> SymbolicT m (SArray a b)
forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
String -> Maybe (SBV b) -> m (array a b)
newArray String
s Maybe (SBV b)
forall a. Maybe a
Nothing SymbolicT m (SArray a b)
-> (SArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SArray a b
a -> [String] -> p -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ss (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SArray a b -> p
k SArray a b
a
  forSome []     SArray a b -> p
k = (SArray a b -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ SArray a b -> p
k

-- SArrays (memory, SMT-Lib notion of arrays), only supported universally for the time being
instance (HasKind a, HasKind b, MProvable m p) => MProvable m (SFunArray a b -> p) where
  forAll_ :: (SFunArray a b -> p) -> SymbolicT m SBool
forAll_        SFunArray a b -> p
k = Maybe (SBV b) -> SymbolicT m (SFunArray a b)
forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
Maybe (SBV b) -> m (array a b)
newArray_  Maybe (SBV b)
forall a. Maybe a
Nothing SymbolicT m (SFunArray a b)
-> (SFunArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SFunArray a b
a -> p -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_   (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SFunArray a b -> p
k SFunArray a b
a
  forAll :: [String] -> (SFunArray a b -> p) -> SymbolicT m SBool
forAll (String
s:[String]
ss)  SFunArray a b -> p
k = String -> Maybe (SBV b) -> SymbolicT m (SFunArray a b)
forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
String -> Maybe (SBV b) -> m (array a b)
newArray String
s Maybe (SBV b)
forall a. Maybe a
Nothing SymbolicT m (SFunArray a b)
-> (SFunArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SFunArray a b
a -> [String] -> p -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SFunArray a b -> p
k SFunArray a b
a
  forAll []      SFunArray a b -> p
k = (SFunArray a b -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ SFunArray a b -> p
k
  forSome_ :: (SFunArray a b -> p) -> SymbolicT m SBool
forSome_       SFunArray a b -> p
k = Maybe (SBV b) -> SymbolicT m (SFunArray a b)
forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
Maybe (SBV b) -> m (array a b)
newArray_  Maybe (SBV b)
forall a. Maybe a
Nothing SymbolicT m (SFunArray a b)
-> (SFunArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SFunArray a b
a -> p -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_   (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SFunArray a b -> p
k SFunArray a b
a
  forSome :: [String] -> (SFunArray a b -> p) -> SymbolicT m SBool
forSome (String
s:[String]
ss) SFunArray a b -> p
k = String -> Maybe (SBV b) -> SymbolicT m (SFunArray a b)
forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
String -> Maybe (SBV b) -> m (array a b)
newArray String
s Maybe (SBV b)
forall a. Maybe a
Nothing SymbolicT m (SFunArray a b)
-> (SFunArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SFunArray a b
a -> [String] -> p -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ss (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SFunArray a b -> p
k SFunArray a b
a
  forSome []     SFunArray a b -> p
k = (SFunArray a b -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ SFunArray a b -> p
k

-- 2 Tuple
instance (SymVal a, SymVal b, MProvable m p) => MProvable m ((SBV a, SBV b) -> p) where
  forAll_ :: ((SBV a, SBV b) -> p) -> SymbolicT m SBool
forAll_        (SBV a, SBV b) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_  SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_   ((SBV b -> p) -> SymbolicT m SBool)
-> (SBV b -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)
  forAll :: [String] -> ((SBV a, SBV b) -> p) -> SymbolicT m SBool
forAll (String
s:[String]
ss)  (SBV a, SBV b) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
forall String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> [String] -> (SBV b -> p) -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss ((SBV b -> p) -> SymbolicT m SBool)
-> (SBV b -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)
  forAll []      (SBV a, SBV b) -> p
k = ((SBV a, SBV b) -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ (SBV a, SBV b) -> p
k
  forSome_ :: ((SBV a, SBV b) -> p) -> SymbolicT m SBool
forSome_       (SBV a, SBV b) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_  SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_   ((SBV b -> p) -> SymbolicT m SBool)
-> (SBV b -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)
  forSome :: [String] -> ((SBV a, SBV b) -> p) -> SymbolicT m SBool
forSome (String
s:[String]
ss) (SBV a, SBV b) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> [String] -> (SBV b -> p) -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ss ((SBV b -> p) -> SymbolicT m SBool)
-> (SBV b -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)
  forSome []     (SBV a, SBV b) -> p
k = ((SBV a, SBV b) -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ (SBV a, SBV b) -> p
k

-- 3 Tuple
instance (SymVal a, SymVal b, SymVal c, MProvable m p) => MProvable m ((SBV a, SBV b, SBV c) -> p) where
  forAll_ :: ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
forAll_       (SBV a, SBV b, SBV c) -> p
k  = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_  SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_   ((SBV b -> SBV c -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c -> (SBV a, SBV b, SBV c) -> p
k (SBV a
a, SBV b
b, SBV c
c)
  forAll :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
forAll (String
s:[String]
ss) (SBV a, SBV b, SBV c) -> p
k  = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
forall String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> [String] -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss ((SBV b -> SBV c -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c -> (SBV a, SBV b, SBV c) -> p
k (SBV a
a, SBV b
b, SBV c
c)
  forAll []     (SBV a, SBV b, SBV c) -> p
k  = ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ (SBV a, SBV b, SBV c) -> p
k
  forSome_ :: ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
forSome_       (SBV a, SBV b, SBV c) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_  SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_   ((SBV b -> SBV c -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c -> (SBV a, SBV b, SBV c) -> p
k (SBV a
a, SBV b
b, SBV c
c)
  forSome :: [String] -> ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
forSome (String
s:[String]
ss) (SBV a, SBV b, SBV c) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> [String] -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ss ((SBV b -> SBV c -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c -> (SBV a, SBV b, SBV c) -> p
k (SBV a
a, SBV b
b, SBV c
c)
  forSome []     (SBV a, SBV b, SBV c) -> p
k = ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ (SBV a, SBV b, SBV c) -> p
k

-- 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
  forAll_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
forAll_        (SBV a, SBV b, SBV c, SBV d) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_  SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_   ((SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \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)
  forAll :: [String]
-> ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
forAll (String
s:[String]
ss)  (SBV a, SBV b, SBV c, SBV d) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
forall String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> [String] -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss ((SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \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)
  forAll []      (SBV a, SBV b, SBV c, SBV d) -> p
k = ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ (SBV a, SBV b, SBV c, SBV d) -> p
k
  forSome_ :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
forSome_       (SBV a, SBV b, SBV c, SBV d) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_  SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_   ((SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \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)
  forSome :: [String]
-> ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
forSome (String
s:[String]
ss) (SBV a, SBV b, SBV c, SBV d) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> [String] -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ss ((SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \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)
  forSome []     (SBV a, SBV b, SBV c, SBV d) -> p
k = ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ (SBV a, SBV b, SBV c, SBV d) -> p
k

-- 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
  forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
forAll_        (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_  SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_   ((SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \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)
  forAll :: [String]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
forAll (String
s:[String]
ss)  (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
forall String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> [String]
-> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss ((SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \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)
  forAll []      (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k
  forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
forSome_       (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_  SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_   ((SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \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)
  forSome :: [String]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
forSome (String
s:[String]
ss) (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> [String]
-> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ss ((SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \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)
  forSome []     (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k

-- 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
  forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m SBool
forAll_        (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_  SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_   ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
 -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \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)
  forAll :: [String]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m SBool
forAll (String
s:[String]
ss)  (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
forall String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> [String]
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
 -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \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)
  forAll []      (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k
  forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m SBool
forSome_       (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_  SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_   ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
 -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \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)
  forSome :: [String]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m SBool
forSome (String
s:[String]
ss) (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> [String]
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ss ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
 -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \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)
  forSome []     (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k

-- 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
  forAll_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m SBool
forAll_        (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
forall_  SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_   ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
 -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \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)
  forAll :: [String]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m SBool
forAll (String
s:[String]
ss)  (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
forall String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> [String]
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
 -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \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)
  forAll []      (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k
  forSome_ :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m SBool
forSome_       (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_  SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_   ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
 -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \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)
  forSome :: [String]
-> ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m SBool
forSome (String
s:[String]
ss) (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> [String]
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ss ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
 -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \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)
  forSome []     (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k

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

-- | Generalization of 'Data.SBV.runSMTWith'
runSMTWith :: MonadIO m => SMTConfig -> SymbolicT m a -> m a
runSMTWith :: SMTConfig -> SymbolicT m a -> m a
runSMTWith SMTConfig
cfg SymbolicT m a
a = (a, Result) -> a
forall a b. (a, b) -> a
fst ((a, Result) -> a) -> m (a, Result) -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBVRunMode -> SymbolicT m a -> m (a, Result)
forall (m :: * -> *) a.
MonadIO m =>
SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
SMTMode QueryContext
QueryExternal IStage
ISetup Bool
True SMTConfig
cfg) SymbolicT m a
a

-- | Runs with a query.
runWithQuery :: MProvable m a => Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery :: Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
isSAT QueryT m b
q SMTConfig
cfg a
a = (b, Result) -> b
forall a b. (a, b) -> a
fst ((b, Result) -> b) -> m (b, Result) -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBVRunMode -> SymbolicT m b -> m (b, Result)
forall (m :: * -> *) a.
MonadIO m =>
SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
SMTMode QueryContext
QueryInternal IStage
ISetup Bool
isSAT SMTConfig
cfg) SymbolicT m b
comp
  where comp :: SymbolicT m b
comp =  do SBool
_ <- (if Bool
isSAT then a -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_ else a -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_) a
a SymbolicT m SBool
-> (SBool -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= SBool -> SymbolicT m SBool
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output
                   QueryContext -> QueryT m b -> SymbolicT m b
forall (m :: * -> *) a.
ExtractIO m =>
QueryContext -> QueryT m a -> SymbolicT m a
Control.executeQuery QueryContext
QueryInternal QueryT m b
q

-- | Check if a safe-call was safe or not, turning a 'SafeResult' to a Bool.
isSafe :: SafeResult -> Bool
isSafe :: SafeResult -> Bool
isSafe (SafeResult (Maybe String
_, String
_, 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 :: UTCTime
-> (SMTConfig -> IO b)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, b))
runInThread UTCTime
beginTime SMTConfig -> IO b
action SMTConfig
config = IO (Solver, NominalDiffTime, b)
-> IO (Async (Solver, NominalDiffTime, b))
forall a. IO a -> IO (Async a)
async (IO (Solver, NominalDiffTime, b)
 -> IO (Async (Solver, NominalDiffTime, b)))
-> IO (Solver, NominalDiffTime, b)
-> IO (Async (Solver, NominalDiffTime, b))
forall a b. (a -> b) -> a -> b
$ do
                b
result  <- SMTConfig -> IO b
action SMTConfig
config
                UTCTime
endTime <- b -> ()
forall a. NFData a => a -> ()
rnf b
result () -> IO UTCTime -> IO UTCTime
`seq` IO UTCTime
getCurrentTime
                (Solver, NominalDiffTime, b) -> IO (Solver, NominalDiffTime, b)
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
config), UTCTime
endTime UTCTime -> UTCTime -> NominalDiffTime
`diffUTCTime` UTCTime
beginTime, b
result)

-- | 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 :: [SMTConfig]
-> (SMTConfig -> a -> IO b) -> a -> IO (Solver, NominalDiffTime, b)
sbvWithAny []      SMTConfig -> a -> IO b
_    a
_ = String -> IO (Solver, NominalDiffTime, b)
forall a. HasCallStack => String -> a
error String
"SBV.withAny: No solvers given!"
sbvWithAny [SMTConfig]
solvers SMTConfig -> a -> IO b
what a
a = do UTCTime
beginTime <- IO UTCTime
getCurrentTime
                               (Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
-> (Solver, NominalDiffTime, b)
forall a b. (a, b) -> b
snd ((Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
 -> (Solver, NominalDiffTime, b))
-> IO
     (Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
-> IO (Solver, NominalDiffTime, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ((SMTConfig -> IO (Async (Solver, NominalDiffTime, b)))
-> [SMTConfig] -> IO [Async (Solver, NominalDiffTime, b)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (UTCTime
-> (SMTConfig -> IO b)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, b))
forall b.
NFData b =>
UTCTime
-> (SMTConfig -> IO b)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, b))
runInThread UTCTime
beginTime (SMTConfig -> a -> IO b
`what` a
a)) [SMTConfig]
solvers IO [Async (Solver, NominalDiffTime, b)]
-> ([Async (Solver, NominalDiffTime, b)]
    -> IO
         (Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b)))
-> IO
     (Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Async (Solver, NominalDiffTime, b)]
-> IO
     (Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
forall a. [Async a] -> IO (Async a, a)
waitAnyFastCancel)
   where -- 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 = [Async a] -> IO (Async a, a)
forall a. [Async a] -> IO (Async a, a)
waitAny [Async a]
asyncs IO (Async a, a) -> IO () -> IO (Async a, a)
forall a b. IO a -> IO b -> IO a
`finally` (Async a -> IO ()) -> [Async a] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Async a -> IO ()
forall a. Async a -> IO ()
cancelFast [Async a]
asyncs
         cancelFast :: Async a -> IO ()
cancelFast Async a
other = ThreadId -> ExitCode -> IO ()
forall e. Exception e => ThreadId -> e -> IO ()
throwTo (Async a -> ThreadId
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 :: 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 = (Async (Solver, NominalDiffTime, c), (Solver, NominalDiffTime, c))
-> (Solver, NominalDiffTime, c)
forall a b. (a, b) -> b
snd ((Async (Solver, NominalDiffTime, c), (Solver, NominalDiffTime, c))
 -> (Solver, NominalDiffTime, c))
-> IO
     (Async (Solver, NominalDiffTime, c), (Solver, NominalDiffTime, c))
-> IO (Solver, NominalDiffTime, c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ((QueryT m b -> IO (Async (Solver, NominalDiffTime, c)))
-> [QueryT m b] -> IO [Async (Solver, NominalDiffTime, c)]
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 IO [Async (Solver, NominalDiffTime, c)]
-> ([Async (Solver, NominalDiffTime, c)]
    -> IO
         (Async (Solver, NominalDiffTime, c), (Solver, NominalDiffTime, c)))
-> IO
     (Async (Solver, NominalDiffTime, c), (Solver, NominalDiffTime, c))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Async (Solver, NominalDiffTime, c)]
-> IO
     (Async (Solver, NominalDiffTime, c), (Solver, NominalDiffTime, c))
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 = [Async a] -> IO (Async a, a)
forall a. [Async a] -> IO (Async a, a)
waitAny [Async a]
asyncs IO (Async a, a) -> IO () -> IO (Async a, a)
forall a b. IO a -> IO b -> IO a
`finally` (Async a -> IO ()) -> [Async a] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Async a -> IO ()
forall a. Async a -> IO ()
cancelFast [Async a]
asyncs
         cancelFast :: Async a -> IO ()
cancelFast Async a
other = ThreadId -> ExitCode -> IO ()
forall e. Exception e => ThreadId -> e -> IO ()
throwTo (Async a -> ThreadId
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
                                 UTCTime
-> (SMTConfig -> IO c)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, c))
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 :: 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 = (QueryT m b -> IO (Async (Solver, NominalDiffTime, c)))
-> [QueryT m b] -> IO [Async (Solver, NominalDiffTime, c)]
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  IO [Async (Solver, NominalDiffTime, c)]
-> ([Async (Solver, NominalDiffTime, c)]
    -> IO [(Solver, NominalDiffTime, c)])
-> IO [(Solver, NominalDiffTime, c)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IO [(Solver, NominalDiffTime, c)]
-> IO [(Solver, NominalDiffTime, c)]
forall a. IO a -> IO a
unsafeInterleaveIO (IO [(Solver, NominalDiffTime, c)]
 -> IO [(Solver, NominalDiffTime, c)])
-> ([Async (Solver, NominalDiffTime, c)]
    -> IO [(Solver, NominalDiffTime, c)])
-> [Async (Solver, NominalDiffTime, c)]
-> IO [(Solver, NominalDiffTime, c)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Async (Solver, NominalDiffTime, c)]
-> IO [(Solver, NominalDiffTime, 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
                                 UTCTime
-> (SMTConfig -> IO c)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, c))
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 []  = [a] -> IO [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
         go [Async a]
as  = do (Async a
d, a
r) <- [Async a] -> IO (Async a, a)
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 <- IO [a] -> IO [a]
forall a. IO a -> IO a
unsafeInterleaveIO (IO [a] -> IO [a]) -> IO [a] -> IO [a]
forall a b. (a -> b) -> a -> b
$ [Async a] -> IO [a]
go ((Async a -> Bool) -> [Async a] -> [Async a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Async a -> Async a -> Bool
forall a. Eq a => a -> a -> Bool
/= Async a
d) [Async a]
as)
                     [a] -> IO [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (a
r a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
rs)

-- | Perform action for all given configs, return all the results.
sbvWithAll :: NFData b => [SMTConfig] -> (SMTConfig -> a -> IO b) -> a -> IO [(Solver, NominalDiffTime, b)]
sbvWithAll :: [SMTConfig]
-> (SMTConfig -> a -> IO b)
-> a
-> IO [(Solver, NominalDiffTime, b)]
sbvWithAll [SMTConfig]
solvers SMTConfig -> a -> IO b
what a
a = do UTCTime
beginTime <- IO UTCTime
getCurrentTime
                               (SMTConfig -> IO (Async (Solver, NominalDiffTime, b)))
-> [SMTConfig] -> IO [Async (Solver, NominalDiffTime, b)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (UTCTime
-> (SMTConfig -> IO b)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, b))
forall b.
NFData b =>
UTCTime
-> (SMTConfig -> IO b)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, b))
runInThread UTCTime
beginTime (SMTConfig -> a -> IO b
`what` a
a)) [SMTConfig]
solvers IO [Async (Solver, NominalDiffTime, b)]
-> ([Async (Solver, NominalDiffTime, b)]
    -> IO [(Solver, NominalDiffTime, b)])
-> IO [(Solver, NominalDiffTime, b)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (IO [(Solver, NominalDiffTime, b)]
-> IO [(Solver, NominalDiffTime, b)]
forall a. IO a -> IO a
unsafeInterleaveIO (IO [(Solver, NominalDiffTime, b)]
 -> IO [(Solver, NominalDiffTime, b)])
-> ([Async (Solver, NominalDiffTime, b)]
    -> IO [(Solver, NominalDiffTime, b)])
-> [Async (Solver, NominalDiffTime, b)]
-> IO [(Solver, NominalDiffTime, b)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Async (Solver, NominalDiffTime, b)]
-> IO [(Solver, NominalDiffTime, b)]
forall a. [Async a] -> IO [a]
go)
   where go :: [Async a] -> IO [a]
go []  = [a] -> IO [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
         go [Async a]
as  = do (Async a
d, a
r) <- [Async a] -> IO (Async a, a)
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 <- IO [a] -> IO [a]
forall a. IO a -> IO a
unsafeInterleaveIO (IO [a] -> IO [a]) -> IO [a] -> IO [a]
forall a b. (a -> b) -> a -> b
$ [Async a] -> IO [a]
go ((Async a -> Bool) -> [Async a] -> [Async a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Async a -> Async a -> Bool
forall a. Eq a => a -> a -> Bool
/= Async a
d) [Async a]
as)
                     [a] -> IO [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (a
r a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
rs)

-- | 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 = SMTConfig -> a -> m [SafeResult]
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 String
cwd <- (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"/") (String -> String) -> m String -> m String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO String -> m String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO String
getCurrentDirectory
                       let mkRelative :: String -> String
mkRelative String
path
                              | String
cwd String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
path = Int -> String -> String
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
cwd) String
path
                              | Bool
True                  = String
path
                       ([SafeResult], Result) -> [SafeResult]
forall a b. (a, b) -> a
fst (([SafeResult], Result) -> [SafeResult])
-> m ([SafeResult], Result) -> m [SafeResult]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBVRunMode -> SymbolicT m [SafeResult] -> m ([SafeResult], Result)
forall (m :: * -> *) a.
MonadIO m =>
SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
SMTMode QueryContext
QueryInternal IStage
ISafe Bool
True SMTConfig
cfg) (a -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ a
a SymbolicT m ()
-> SymbolicT m [SafeResult] -> SymbolicT m [SafeResult]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (String -> String) -> SymbolicT m [SafeResult]
check String -> String
mkRelative)
     where check :: (FilePath -> FilePath) -> SymbolicT m [SafeResult]
           check :: (String -> String) -> SymbolicT m [SafeResult]
check String -> String
mkRelative = QueryContext -> QueryT m [SafeResult] -> SymbolicT m [SafeResult]
forall (m :: * -> *) a.
ExtractIO m =>
QueryContext -> QueryT m a -> SymbolicT m a
Control.executeQuery QueryContext
QueryInternal (QueryT m [SafeResult] -> SymbolicT m [SafeResult])
-> QueryT m [SafeResult] -> SymbolicT m [SafeResult]
forall a b. (a -> b) -> a -> b
$ QueryT m [(String, Maybe CallStack, SV)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, Maybe CallStack, SV)]
Control.getSBVAssertions QueryT m [(String, Maybe CallStack, SV)]
-> ([(String, Maybe CallStack, SV)] -> QueryT m [SafeResult])
-> QueryT m [SafeResult]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ((String, Maybe CallStack, SV) -> QueryT m SafeResult)
-> [(String, Maybe CallStack, SV)] -> QueryT m [SafeResult]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((String -> String)
-> (String, Maybe CallStack, SV) -> QueryT m SafeResult
verify String -> String
mkRelative)

           -- 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 :: (String -> String)
-> (String, Maybe CallStack, SV) -> QueryT m SafeResult
verify String -> String
mkRelative (String
msg, Maybe CallStack
cs, SV
cond) = do
                   let locInfo :: [(String, SrcLoc)] -> String
locInfo [(String, SrcLoc)]
ps = let loc :: (String, SrcLoc) -> String
loc (String
f, SrcLoc
sl) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String -> String
mkRelative (SrcLoc -> String
srcLocFile SrcLoc
sl), String
":", Int -> String
forall a. Show a => a -> String
show (SrcLoc -> Int
srcLocStartLine SrcLoc
sl), String
":", Int -> String
forall a. Show a => a -> String
show (SrcLoc -> Int
srcLocStartCol SrcLoc
sl), String
":", String
f]
                                    in String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
",\n " (((String, SrcLoc) -> String) -> [(String, SrcLoc)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, SrcLoc) -> String
loc [(String, SrcLoc)]
ps)
                       location :: Maybe String
location   = ([(String, SrcLoc)] -> String
locInfo ([(String, SrcLoc)] -> String)
-> (CallStack -> [(String, SrcLoc)]) -> CallStack -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> [(String, SrcLoc)]
getCallStack) (CallStack -> String) -> Maybe CallStack -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Maybe CallStack
cs

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

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

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

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

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

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

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

-- Functions
instance (SymVal a, SExecutable m p) => SExecutable m (SBV a -> p) where
   sName_ :: (SBV a -> p) -> SymbolicT m ()
sName_        SBV a -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_   SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> p -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_   (p -> SymbolicT m ()) -> p -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a
   sName :: [String] -> (SBV a -> p) -> SymbolicT m ()
sName (String
s:[String]
ss)  SBV a -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s  SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> [String] -> p -> SymbolicT m ()
forall (m :: * -> *) a.
SExecutable m a =>
[String] -> a -> SymbolicT m ()
sName [String]
ss (p -> SymbolicT m ()) -> p -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a
   sName []      SBV a -> p
k = (SBV a -> p) -> SymbolicT m ()
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 = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
exists_  SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> p) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_   ((SBV b -> p) -> SymbolicT m ()) -> (SBV b -> p) -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)
  sName :: [String] -> ((SBV a, SBV b) -> p) -> SymbolicT m ()
sName (String
s:[String]
ss)  (SBV a, SBV b) -> p
k = String -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
String -> m (SBV a)
exists String
s SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> [String] -> (SBV b -> p) -> SymbolicT m ()
forall (m :: * -> *) a.
SExecutable m a =>
[String] -> a -> SymbolicT m ()
sName [String]
ss ((SBV b -> p) -> SymbolicT m ()) -> (SBV b -> p) -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)
  sName []      (SBV a, SBV b) -> p
k = ((SBV a, SBV b) -> p) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ (SBV a, SBV b) -> p
k

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

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

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

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

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

{-# ANN module ("HLint: ignore Reduce duplication" :: String) #-}