-----------------------------------------------------------------------------
-- |
-- 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
       , generateSMTBenchmark
       , Goal
       , ThmResult(..), SatResult(..), AllSatResult(..), SafeResult(..), OptimizeResult(..), SMTResult(..)
       , SExecutable(..), isSafe
       , runSMT, runSMTWith
       , SatModel(..), Modelable(..), displayModels, extractModels
       , getModelDictionaries, getModelValues, getModelUninterpretedValues
       , boolector, cvc4, yices, z3, mathSAT, abc, defaultSMTCfg
       ) where


import Control.Monad          (when, unless)
import Control.Monad.IO.Class (MonadIO, liftIO)
import Control.DeepSeq        (rnf, NFData(..))

import Control.Concurrent.Async (async, waitAny, asyncThreadId, Async)
import Control.Exception (finally, throwTo, AsyncException(ThreadKilled))

import System.IO.Unsafe (unsafeInterleaveIO)             -- 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.Z3         as Z3
import qualified Data.SBV.Provers.MathSAT    as MathSAT
import qualified Data.SBV.Provers.ABC        as ABC

mkConfig :: SMTSolver -> SMTLibVersion -> [Control.SMTOption] -> SMTConfig
mkConfig :: SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig s :: SMTSolver
s smtVersion :: SMTLibVersion
smtVersion startOpts :: [SMTOption]
startOpts = SMTConfig :: Bool
-> Timing
-> Int
-> Int
-> String
-> Maybe Int
-> Bool
-> Bool
-> (String -> Bool)
-> Bool
-> Bool
-> Maybe String
-> SMTLibVersion
-> SMTSolver
-> Bool
-> RoundingMode
-> [SMTOption]
-> Bool
-> Maybe String
-> SMTConfig
SMTConfig { verbose :: Bool
verbose                     = Bool
False
                                            , timing :: Timing
timing                      = Timing
NoTiming
                                            , printBase :: Int
printBase                   = 10
                                            , printRealPrec :: Int
printRealPrec               = 16
                                            , transcript :: Maybe String
transcript                  = Maybe String
forall a. Maybe a
Nothing
                                            , solver :: SMTSolver
solver                      = SMTSolver
s
                                            , smtLibVersion :: SMTLibVersion
smtLibVersion               = SMTLibVersion
smtVersion
                                            , satCmd :: String
satCmd                      = "(check-sat)"
                                            , satTrackUFs :: Bool
satTrackUFs                 = Bool
True                   -- 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 -> [String] -> SMTOption
Control.OptionKeyword ":diagnostic-output-channel" [String -> String
forall a. Show a => a -> String
show "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 Z3 SMT solver
z3 :: SMTConfig
z3 :: SMTConfig
z3 = SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
Z3.z3 SMTLibVersion
SMTLib2 [ String -> [String] -> SMTOption
Control.OptionKeyword ":smtlib2_compliant" ["true"]
                            , SMTOption
allOnStdOut
                            ]

-- | 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

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

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

  -- | 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 cfg :: SMTConfig
cfg a :: a
a = do f :: (Bool, Bool, Bool, [SMTResult])
f@(mm :: Bool
mm, pe :: Bool
pe, un :: Bool
un, rs :: [SMTResult]
rs) <- Bool
-> QueryT m (Bool, Bool, Bool, [SMTResult])
-> SMTConfig
-> a
-> m (Bool, Bool, Bool, [SMTResult])
forall (m :: * -> *) a b.
MProvable m a =>
Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery Bool
True (QueryT m ()
forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations QueryT m ()
-> QueryT m (Bool, Bool, Bool, [SMTResult])
-> QueryT m (Bool, Bool, Bool, [SMTResult])
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QueryT m (Bool, Bool, Bool, [SMTResult])
forall (m :: * -> *).
(MonadIO m, MonadQuery m, SolverContext m) =>
m (Bool, Bool, Bool, [SMTResult])
Control.getAllSatResult) SMTConfig
cfg a
a
                        (Bool, Bool, Bool, [SMTResult]) -> AllSatResult
AllSatResult ((Bool, Bool, Bool, [SMTResult]) -> AllSatResult)
-> m (Bool, Bool, Bool, [SMTResult]) -> m AllSatResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> if SMTConfig -> Bool
validationRequested SMTConfig
cfg
                                         then do [SMTResult]
rs' <- (SMTResult -> m SMTResult) -> [SMTResult] -> m [SMTResult]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
forall (m :: * -> *) a.
MProvable m a =>
Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
validate Bool
True SMTConfig
cfg a
a) [SMTResult]
rs
                                                 (Bool, Bool, Bool, [SMTResult])
-> m (Bool, Bool, Bool, [SMTResult])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
mm, Bool
pe, Bool
un, [SMTResult]
rs')
                                         else (Bool, Bool, Bool, [SMTResult])
-> m (Bool, Bool, Bool, [SMTResult])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool, Bool, Bool, [SMTResult])
f

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

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

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

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

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


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

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

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

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

                       chaseUniversal :: SV -> [String]
chaseUniversal entry :: SV
entry = (NamedSymVar -> String) -> [NamedSymVar] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map NamedSymVar -> String
forall a b. (a, b) -> b
snd ([NamedSymVar] -> [String]) -> [NamedSymVar] -> [String]
forall a b. (a -> b) -> a -> b
$ SV -> [NamedSymVar] -> [NamedSymVar]
go SV
entry []
                         where go :: SV -> [NamedSymVar] -> [NamedSymVar]
go x :: SV
x sofar :: [NamedSymVar]
sofar
                                | NodeId
nx NodeId -> NodeId -> Bool
forall a. Ord a => a -> a -> Bool
>= NodeId
firstUniversal
                                = [NamedSymVar] -> [NamedSymVar]
forall a. Eq a => [a] -> [a]
nub ([NamedSymVar] -> [NamedSymVar]) -> [NamedSymVar] -> [NamedSymVar]
forall a b. (a -> b) -> a -> b
$ [NamedSymVar
unm | unm :: NamedSymVar
unm@(u :: SV
u, _) <- [NamedSymVar]
universals, NodeId
nx NodeId -> NodeId -> Bool
forall a. Ord a => a -> a -> Bool
>= SV -> NodeId
nodeId SV
u] [NamedSymVar] -> [NamedSymVar] -> [NamedSymVar]
forall a. [a] -> [a] -> [a]
++ [NamedSymVar]
sofar
                                | Bool
True
                                = let oVars :: Op -> [SV]
oVars (LkUp _ a :: SV
a b :: SV
b)             = [SV
a, SV
b]
                                      oVars (IEEEFP (FP_Cast _ _ o :: SV
o)) = [SV
o]
                                      oVars _                        = []
                                      vars :: [SV]
vars = case SV
x SV -> Map SV SBVExpr -> Maybe SBVExpr
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map SV SBVExpr
mappings of
                                               Nothing            -> []
                                               Just (SBVApp o :: Op
o ss :: [SV]
ss) -> [SV] -> [SV]
forall a. Eq a => [a] -> [a]
nub (Op -> [SV]
oVars Op
o [SV] -> [SV] -> [SV]
forall a. [a] -> [a] -> [a]
++ [SV]
ss)
                                  in (SV -> [NamedSymVar] -> [NamedSymVar])
-> [NamedSymVar] -> [SV] -> [NamedSymVar]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SV -> [NamedSymVar] -> [NamedSymVar]
go [NamedSymVar]
sofar [SV]
vars
                                where nx :: NodeId
nx = SV -> NodeId
nodeId SV
x

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

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

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

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

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

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

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

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

  -- | 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 cfg :: SMTConfig
cfg a :: 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
                    Control.Unsat -> Bool -> QueryT m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                    Control.Sat   -> Bool -> QueryT m Bool
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                    Control.Unk   -> String -> QueryT m Bool
forall a. HasCallStack => String -> a
error "SBV: isVacuous: Solver returned unknown!"

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


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

  -- | Validate a model obtained from the solver
  validate :: Bool -> SMTConfig -> a -> SMTResult -> m SMTResult
  validate isSAT :: Bool
isSAT cfg :: SMTConfig
cfg p :: a
p res :: SMTResult
res = case SMTResult
res of
                               Unsatisfiable{} -> SMTResult -> m SMTResult
forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
res
                               Satisfiable _ m :: SMTModel
m -> case SMTModel -> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
modelBindings SMTModel
m of
                                                    Nothing  -> String -> m SMTResult
forall a. HasCallStack => String -> a
error "Data.SBV.validate: Impossible happaned; no bindings generated during model validation."
                                                    Just env :: [((Quantifier, NamedSymVar), Maybe CV)]
env -> [((Quantifier, NamedSymVar), Maybe CV)] -> m SMTResult
forall (m :: * -> *).
MProvable m a =>
[((Quantifier, NamedSymVar), Maybe CV)] -> m SMTResult
check [((Quantifier, NamedSymVar), Maybe CV)]
env
                               SatExtField{}   -> SMTResult -> m SMTResult
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTResult -> m SMTResult) -> SMTResult -> m SMTResult
forall a b. (a -> b) -> a -> b
$ SMTConfig -> [String] -> Maybe SMTResult -> SMTResult
ProofError SMTConfig
cfg [ "The model requires an extension field value."
                                                                          , "Cannot validate models with infinities/epsilons produced during optimization."
                                                                          , ""
                                                                          , "To turn validation off, use `cfg{optimizeValidateConstraints = False}`"
                                                                          , ""
                                                                          , "Unable to validate the produced model."
                                                                          ]
                                                                          (SMTResult -> Maybe SMTResult
forall a. a -> Maybe a
Just SMTResult
res)
                               Unknown{}       -> SMTResult -> m SMTResult
forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
res
                               ProofError{}    -> SMTResult -> m SMTResult
forall (m :: * -> *) a. Monad m => a -> m a
return SMTResult
res

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                             -- 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 "Impossible happened: There are no outputs nor any constraints to check."
                             checkOutputs os :: [SV]
os
                               = do String -> m ()
forall (m :: * -> *). MonadIO m => String -> m ()
notify "Validating outputs."
                                    if Bool
isSAT then [SV] -> m SMTResult
forall (m :: * -> *). MonadIO m => [SV] -> m SMTResult
satLoop   [SV]
os
                                             else [SV] -> Bool -> m SMTResult
forall (m :: * -> *). MonadIO m => [SV] -> Bool -> m SMTResult
proveLoop [SV]
os Bool
False

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

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

-- | `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 a @ThreadKilled@ 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 a @ThreadKilled@ 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)

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

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

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

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

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

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

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

-- 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_    a :: SymbolicT m ()
a = SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_    ((SymbolicT m ()
a SymbolicT m () -> SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return SBool
sTrue) :: SymbolicT m SBool)
  forAll :: [String] -> SymbolicT m () -> SymbolicT m SBool
forAll ns :: [String]
ns  a :: SymbolicT m ()
a = [String] -> SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ns  ((SymbolicT m ()
a SymbolicT m () -> SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return SBool
sTrue) :: SymbolicT m SBool)
  forSome_ :: SymbolicT m () -> SymbolicT m SBool
forSome_   a :: SymbolicT m ()
a = SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forSome_   ((SymbolicT m ()
a SymbolicT m () -> SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return SBool
sTrue) :: SymbolicT m SBool)
  forSome :: [String] -> SymbolicT m () -> SymbolicT m SBool
forSome ns :: [String]
ns a :: SymbolicT m ()
a = [String] -> SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forSome [String]
ns ((SymbolicT m ()
a SymbolicT m () -> SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return SBool
sTrue) :: SymbolicT m SBool)

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

instance ExtractIO m => MProvable m SBool where
  forAll_ :: SBool -> SymbolicT m SBool
forAll_   = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return
  forAll :: [String] -> SBool -> SymbolicT m SBool
forAll _  = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return
  forSome_ :: SBool -> SymbolicT m SBool
forSome_  = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return
  forSome :: [String] -> SBool -> SymbolicT m SBool
forSome _ = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. Monad m => a -> m a
return

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

-- 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_       k :: SArray a b -> p
k = Maybe (SBV b) -> SymbolicT m (SArray a b)
forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
Maybe (SBV b) -> m (array a b)
newArray_  Maybe (SBV b)
forall a. Maybe a
Nothing SymbolicT m (SArray a b)
-> (SArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SArray a b
a -> p -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_   (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SArray a b -> p
k SArray a b
a
  forAll :: [String] -> (SArray a b -> p) -> SymbolicT m SBool
forAll (s :: String
s:ss :: [String]
ss) k :: SArray a b -> p
k = String -> Maybe (SBV b) -> SymbolicT m (SArray a b)
forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
String -> Maybe (SBV b) -> m (array a b)
newArray String
s Maybe (SBV b)
forall a. Maybe a
Nothing SymbolicT m (SArray a b)
-> (SArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SArray a b
a -> [String] -> p -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SArray a b -> p
k SArray a b
a
  forAll []     k :: SArray a b -> p
k = (SArray a b -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ SArray a b -> p
k
  forSome_ :: (SArray a b -> p) -> SymbolicT m SBool
forSome_      _ = String -> SymbolicT m SBool
forall a. HasCallStack => String -> a
error "SBV.forSome.SFunArray: Existential arrays are not currently supported."
  forSome :: [String] -> (SArray a b -> p) -> SymbolicT m SBool
forSome _     _ = String -> SymbolicT m SBool
forall a. HasCallStack => String -> a
error "SBV.forSome.SFunArray: Existential arrays are not currently supported."

-- 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_       k :: SFunArray a b -> p
k = Maybe (SBV b) -> SymbolicT m (SFunArray a b)
forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
Maybe (SBV b) -> m (array a b)
newArray_  Maybe (SBV b)
forall a. Maybe a
Nothing SymbolicT m (SFunArray a b)
-> (SFunArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SFunArray a b
a -> p -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_   (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SFunArray a b -> p
k SFunArray a b
a
  forAll :: [String] -> (SFunArray a b -> p) -> SymbolicT m SBool
forAll (s :: String
s:ss :: [String]
ss) k :: SFunArray a b -> p
k = String -> Maybe (SBV b) -> SymbolicT m (SFunArray a b)
forall (array :: * -> * -> *) (m :: * -> *) a b.
(SymArray array, MonadSymbolic m, HasKind a, HasKind b) =>
String -> Maybe (SBV b) -> m (array a b)
newArray String
s Maybe (SBV b)
forall a. Maybe a
Nothing SymbolicT m (SFunArray a b)
-> (SFunArray a b -> SymbolicT m SBool) -> SymbolicT m SBool
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a :: SFunArray a b
a -> [String] -> p -> SymbolicT m SBool
forall (m :: * -> *) a.
MProvable m a =>
[String] -> a -> SymbolicT m SBool
forAll [String]
ss (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SFunArray a b -> p
k SFunArray a b
a
  forAll []     k :: SFunArray a b -> p
k = (SFunArray a b -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. MProvable m a => a -> SymbolicT m SBool
forAll_ SFunArray a b -> p
k
  forSome_ :: (SFunArray a b -> p) -> SymbolicT m SBool
forSome_      _ = String -> SymbolicT m SBool
forall a. HasCallStack => String -> a
error "SBV.forSome.SArray: Existential arrays are not currently supported."
  forSome :: [String] -> (SFunArray a b -> p) -> SymbolicT m SBool
forSome _     _ = String -> SymbolicT m SBool
forall a. HasCallStack => String -> a
error "SBV.forSome.SArray: Existential arrays are not currently supported."

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

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

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

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

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

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

-- | 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 cfg :: SMTConfig
cfg a :: SymbolicT m a
a = (a, Result) -> a
forall a b. (a, b) -> a
fst ((a, Result) -> a) -> m (a, Result) -> m a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBVRunMode -> SymbolicT m a -> m (a, Result)
forall (m :: * -> *) a.
MonadIO m =>
SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
SMTMode QueryContext
QueryExternal IStage
ISetup Bool
True SMTConfig
cfg) SymbolicT m a
a

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

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

-- | 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 []      _    _ = String -> IO (Solver, NominalDiffTime, b)
forall a. HasCallStack => String -> a
error "SBV.withAny: No solvers given!"
sbvWithAny solvers :: [SMTConfig]
solvers what :: SMTConfig -> a -> IO b
what a :: a
a = do UTCTime
beginTime <- IO UTCTime
getCurrentTime
                               (Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
-> (Solver, NominalDiffTime, b)
forall a b. (a, b) -> b
snd ((Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
 -> (Solver, NominalDiffTime, b))
-> IO
     (Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
-> IO (Solver, NominalDiffTime, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ((SMTConfig -> IO (Async (Solver, NominalDiffTime, b)))
-> [SMTConfig] -> IO [Async (Solver, NominalDiffTime, b)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (UTCTime
-> (SMTConfig -> IO b)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, b))
forall b.
NFData b =>
UTCTime
-> (SMTConfig -> IO b)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, b))
runInThread UTCTime
beginTime (SMTConfig -> a -> IO b
`what` a
a)) [SMTConfig]
solvers IO [Async (Solver, NominalDiffTime, b)]
-> ([Async (Solver, NominalDiffTime, b)]
    -> IO
         (Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b)))
-> IO
     (Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Async (Solver, NominalDiffTime, b)]
-> IO
     (Async (Solver, NominalDiffTime, b), (Solver, NominalDiffTime, b))
forall a. [Async a] -> IO (Async a, a)
waitAnyFastCancel)
   where -- 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 asyncs :: [Async a]
asyncs = [Async a] -> IO (Async a, a)
forall a. [Async a] -> IO (Async a, a)
waitAny [Async a]
asyncs IO (Async a, a) -> IO () -> IO (Async a, a)
forall a b. IO a -> IO b -> IO a
`finally` (Async a -> IO ()) -> [Async a] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Async a -> IO ()
forall a. Async a -> IO ()
cancelFast [Async a]
asyncs
         cancelFast :: Async a -> IO ()
cancelFast other :: Async a
other = ThreadId -> AsyncException -> IO ()
forall e. Exception e => ThreadId -> e -> IO ()
throwTo (Async a -> ThreadId
forall a. Async a -> ThreadId
asyncThreadId Async a
other) AsyncException
ThreadKilled

-- | 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 solvers :: [SMTConfig]
solvers what :: SMTConfig -> a -> IO b
what a :: a
a = do UTCTime
beginTime <- IO UTCTime
getCurrentTime
                               (SMTConfig -> IO (Async (Solver, NominalDiffTime, b)))
-> [SMTConfig] -> IO [Async (Solver, NominalDiffTime, b)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (UTCTime
-> (SMTConfig -> IO b)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, b))
forall b.
NFData b =>
UTCTime
-> (SMTConfig -> IO b)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, b))
runInThread UTCTime
beginTime (SMTConfig -> a -> IO b
`what` a
a)) [SMTConfig]
solvers IO [Async (Solver, NominalDiffTime, b)]
-> ([Async (Solver, NominalDiffTime, b)]
    -> IO [(Solver, NominalDiffTime, b)])
-> IO [(Solver, NominalDiffTime, b)]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (IO [(Solver, NominalDiffTime, b)]
-> IO [(Solver, NominalDiffTime, b)]
forall a. IO a -> IO a
unsafeInterleaveIO (IO [(Solver, NominalDiffTime, b)]
 -> IO [(Solver, NominalDiffTime, b)])
-> ([Async (Solver, NominalDiffTime, b)]
    -> IO [(Solver, NominalDiffTime, b)])
-> [Async (Solver, NominalDiffTime, b)]
-> IO [(Solver, NominalDiffTime, b)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Async (Solver, NominalDiffTime, b)]
-> IO [(Solver, NominalDiffTime, b)]
forall a. [Async a] -> IO [a]
go)
   where go :: [Async a] -> IO [a]
go []  = [a] -> IO [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []
         go as :: [Async a]
as  = do (d :: Async a
d, r :: a
r) <- [Async a] -> IO (Async a, a)
forall a. [Async a] -> IO (Async a, a)
waitAny [Async a]
as
                     -- 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 sufficently 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 cfg :: SMTConfig
cfg a :: a
a = do String
cwd <- (String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/") (String -> String) -> m String -> m String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO String -> m String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO String
getCurrentDirectory
                       let mkRelative :: String -> String
mkRelative path :: String
path
                              | String
cwd String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
path = Int -> String -> String
forall a. Int -> [a] -> [a]
drop (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
cwd) String
path
                              | Bool
True                  = String
path
                       ([SafeResult], Result) -> [SafeResult]
forall a b. (a, b) -> a
fst (([SafeResult], Result) -> [SafeResult])
-> m ([SafeResult], Result) -> m [SafeResult]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SBVRunMode -> SymbolicT m [SafeResult] -> m ([SafeResult], Result)
forall (m :: * -> *) a.
MonadIO m =>
SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
SMTMode QueryContext
QueryInternal IStage
ISafe Bool
True SMTConfig
cfg) (a -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName_ a
a SymbolicT m ()
-> SymbolicT m [SafeResult] -> SymbolicT m [SafeResult]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (String -> String) -> SymbolicT m [SafeResult]
check String -> String
mkRelative)
     where check :: (FilePath -> FilePath) -> SymbolicT m [SafeResult]
           check :: (String -> String) -> SymbolicT m [SafeResult]
check mkRelative :: String -> String
mkRelative = QueryContext -> QueryT m [SafeResult] -> SymbolicT m [SafeResult]
forall (m :: * -> *) a.
ExtractIO m =>
QueryContext -> QueryT m a -> SymbolicT m a
Control.executeQuery QueryContext
QueryInternal (QueryT m [SafeResult] -> SymbolicT m [SafeResult])
-> QueryT m [SafeResult] -> SymbolicT m [SafeResult]
forall a b. (a -> b) -> a -> b
$ QueryT m [(String, Maybe CallStack, SV)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, Maybe CallStack, SV)]
Control.getSBVAssertions QueryT m [(String, Maybe CallStack, SV)]
-> ([(String, Maybe CallStack, SV)] -> QueryT m [SafeResult])
-> QueryT m [SafeResult]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ((String, Maybe CallStack, SV) -> QueryT m SafeResult)
-> [(String, Maybe CallStack, SV)] -> QueryT m [SafeResult]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((String -> String)
-> (String, Maybe CallStack, SV) -> QueryT m SafeResult
verify String -> String
mkRelative)

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

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

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

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

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

-- 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 xs :: [String]
xs () = [String] -> SymbolicT m () -> SymbolicT m ()
forall (m :: * -> *) a.
SExecutable m a =>
[String] -> a -> SymbolicT m ()
sName [String]
xs (() -> SymbolicT m ()
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
output () :: SymbolicT m ())

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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