-----------------------------------------------------------------------------
-- |
-- 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         #-}
{-# LANGUAGE UndecidableInstances  #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.Provers.Prover (
         SMTSolver(..), SMTConfig(..), Predicate
       , ProvableM(..), Provable, SatisfiableM(..), Satisfiable
       , generateSMTBenchmarkSat, generateSMTBenchmarkProof, defs2smt, ConstraintSet
       , ThmResult(..), SatResult(..), AllSatResult(..), SafeResult(..), OptimizeResult(..), SMTResult(..)
       , SExecutable(..), isSafe
       , runSMT, runSMTWith
       , SatModel(..), Modelable(..), displayModels, extractModels
       , getModelDictionaries, getModelValues, getModelUninterpretedValues
       , abc, boolector, bitwuzla, cvc4, cvc5, dReal, mathSAT, yices, z3, openSMT, defaultSMTCfg, defaultDeltaSMTCfg
       , proveWithAny, proveWithAll, proveConcurrentWithAny, proveConcurrentWithAll
       , satWithAny,   satWithAll,   satConcurrentWithAny,   satConcurrentWithAll
       ) where


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

import Control.Concurrent.Async (async, waitAny, asyncThreadId, Async, mapConcurrently)
import Control.Exception (finally, throwTo)
import System.Exit (ExitCode(ExitSuccess))

import System.IO.Unsafe (unsafeInterleaveIO)             -- only used safely!

import System.Directory  (getCurrentDirectory)
import Data.Time (getZonedTime, NominalDiffTime, UTCTime, getCurrentTime, diffUTCTime)
import Data.List (intercalate, isPrefixOf)

import Data.Maybe (mapMaybe, listToMaybe)

import qualified Data.Foldable   as S (toList)
import qualified Data.Text       as T

import Data.SBV.Core.Data
import Data.SBV.Core.Symbolic
import Data.SBV.SMT.SMT
import Data.SBV.SMT.Utils (debug, alignPlain)
import Data.SBV.Utils.ExtractIO
import Data.SBV.Utils.TDiff

import Data.SBV.Lambda () -- instances only

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

import GHC.Stack

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

import GHC.TypeLits

mkConfig :: SMTSolver -> SMTLibVersion -> [Control.SMTOption] -> SMTConfig
mkConfig :: SMTSolver -> SMTLibVersion -> [SMTOption] -> SMTConfig
mkConfig SMTSolver
s SMTLibVersion
smtVersion [SMTOption]
startOpts = SMTConfig { verbose :: Bool
verbose                     = Bool
False
                                            , timing :: Timing
timing                      = Timing
NoTiming
                                            , printBase :: Int
printBase                   = Int
10
                                            , printRealPrec :: Int
printRealPrec               = Int
16
                                            , crackNum :: Bool
crackNum                    = Bool
False
                                            , crackNumSurfaceVals :: [(String, Integer)]
crackNumSurfaceVals         = []
                                            , transcript :: Maybe String
transcript                  = Maybe String
forall a. Maybe a
Nothing
                                            , solver :: SMTSolver
solver                      = SMTSolver
s
                                            , smtLibVersion :: SMTLibVersion
smtLibVersion               = SMTLibVersion
smtVersion
                                            , dsatPrecision :: Maybe Double
dsatPrecision               = Maybe Double
forall a. Maybe a
Nothing
                                            , extraArgs :: [String]
extraArgs                   = []
                                            , satCmd :: String
satCmd                      = String
"(check-sat)"
                                            , allSatTrackUFs :: Bool
allSatTrackUFs              = 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
                                            , 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
                                            , generateHOEquivs :: Bool
generateHOEquivs            = Bool
False
                                            , kdOptions :: KDOptions
kdOptions                   = KDOptions { ribbonLength :: Int
ribbonLength      = Int
40
                                                                                      , firstifyUniqueLen :: Int
firstifyUniqueLen = Int
6
                                                                                      , quiet :: Bool
quiet             = Bool
False
                                                                                      , measureTime :: Bool
measureTime       = Bool
False
                                                                                      }
                                            }

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

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

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

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

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

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

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

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

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

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

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

-- | The default solver used by SBV. This is currently set to z3.
defaultSMTCfg :: SMTConfig
defaultSMTCfg :: SMTConfig
defaultSMTCfg = SMTConfig
z3

-- | The default solver used by SBV for delta-satisfiability problems. This is currently set to dReal,
-- which is also the only solver that supports delta-satisfiability.
defaultDeltaSMTCfg :: SMTConfig
defaultDeltaSMTCfg :: SMTConfig
defaultDeltaSMTCfg = SMTConfig
dReal

-- | A predicate is a symbolic program that returns a (symbolic) boolean value. For all intents and
-- purposes, it can be treated as an n-ary function from symbolic-values to a boolean. The 'Symbolic'
-- monad captures the underlying representation, and can/should be ignored by the users of the library,
-- unless you are building further utilities on top of SBV itself. Instead, simply use the 'Predicate'
-- type when necessary.
type Predicate = Symbolic SBool

-- | A constraint set is a symbolic program that returns no values. The idea is that the constraints/min-max
-- goals will serve as the collection of constraints that will be used for sat/optimize calls.
type ConstraintSet = Symbolic ()

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

-- | `Data.SBV.Provers.Satisfiable` is specialization of `SatisfiableM` to the `IO` monad. Unless you are using
-- transformers explicitly, this is the type you should prefer.
type Satisfiable = SatisfiableM IO

-- | A type @a@ is satisfiable if it has constraints, potentially returning a boolean. This class
-- captures essentially sat and optimize calls.
class ExtractIO m => SatisfiableM m a where
  -- | Reduce an arg, for sat purposes.
  satArgReduce :: a -> SymbolicT m SBool

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

  -- | Generalization of 'Data.SBV.satWith'
  satWith :: SMTConfig -> a -> m SatResult
  satWith SMTConfig
cfg a
a = do r <- (a -> SymbolicT m SBool)
-> Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
forall (m :: * -> *) a b.
ExtractIO m =>
(a -> SymbolicT m SBool)
-> Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery a -> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce Bool
True (QueryT m ()
forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
forall a b. QueryT m a -> QueryT m b -> QueryT m b
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
                     SatResult <$> if validationRequested cfg
                                   then validate satArgReduce True cfg a r
                                   else return r

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

  -- | Generalization of 'Data.SBV.satWith'
  dsatWith :: SMTConfig -> a -> m SatResult
  dsatWith SMTConfig
cfg a
a = do r <- (a -> SymbolicT m SBool)
-> Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
forall (m :: * -> *) a b.
ExtractIO m =>
(a -> SymbolicT m SBool)
-> Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery a -> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce Bool
True (QueryT m ()
forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
forall a b. QueryT m a -> QueryT m b -> QueryT m b
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
                      SatResult <$> if validationRequested cfg
                                    then validate satArgReduce True cfg a r
                                    else return r

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

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

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

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

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

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

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

                   when (null objectives) $
                          error $ unlines [ ""
                                          , "*** Data.SBV: Unsupported call to optimize when no objectives are present."
                                          , "*** Use \"sat\" for plain satisfaction"
                                          ]

                   unless (supportsOptimization (capabilities (solver config))) $
                          error $ unlines [ ""
                                          , "*** Data.SBV: The backend solver " ++ show (name (solver config)) ++ "does not support optimization goals."
                                          , "*** Please use a solver that has support, such as z3"
                                          ]

                   when (validateModel config && not (optimizeValidateConstraints config)) $
                          error $ 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 optimizerDirectives = (Objective (SV, SV) -> [String])
-> [Objective (SV, SV)] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Objective (SV, SV) -> [String]
forall {a} {a}. (Show a, Show a) => Objective (a, a) -> [String]
minmax [Objective (SV, SV)]
objectives [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ OptimizeStyle -> [String]
priority OptimizeStyle
style
                         where mkEq :: (a, a) -> String
mkEq (a
x, a
y) = String
"(assert (= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"

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

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

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

                   mapM_ (Control.send True) optimizerDirectives

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

-- | Find a satisfying assignment to a property with multiple solvers, running them in separate threads. The
-- results will be returned in the order produced.
satWithAll :: Satisfiable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
satWithAll :: forall a.
Satisfiable a =>
[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.
SatisfiableM m a =>
SMTConfig -> a -> m SatResult
satWith)

-- | Find a satisfying assignment to a property with multiple solvers, running them in separate threads. Only
-- the result of the first one to finish will be returned, remaining threads will be killed.
-- Note that we send an exception to the losing processes, but we do *not* actually wait for them
-- to finish. In rare cases this can lead to zombie processes. In previous experiments, we found
-- that some processes take their time to terminate. So, this solution favors quick turnaround.
satWithAny :: Satisfiable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, SatResult)
satWithAny :: forall a.
Satisfiable a =>
[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.
SatisfiableM m a =>
SMTConfig -> a -> m SatResult
satWith)

-- | Find a satisfying assignment to a property using a single solver, but
-- providing several query problems of interest, with each query running in a
-- separate thread and return the first one that returns. This can be useful to
-- use symbolic mode to drive to a location in the search space of the solver
-- and then refine the problem in query mode. If the computation is very hard to
-- solve for the solver than running in concurrent mode may provide a large
-- performance benefit.
satConcurrentWithAny :: Satisfiable a => SMTConfig -> [Query b] -> a -> IO (Solver, NominalDiffTime, SatResult)
satConcurrentWithAny :: forall a b.
Satisfiable a =>
SMTConfig
-> [Query b] -> a -> IO (Solver, NominalDiffTime, SatResult)
satConcurrentWithAny SMTConfig
solver [Query b]
qs a
a = do (slvr,time,result) <- SMTConfig
-> (SMTConfig -> a -> Query b -> IO SMTResult)
-> [Query b]
-> a
-> IO (Solver, NominalDiffTime, SMTResult)
forall c a (m :: * -> *) b.
NFData c =>
SMTConfig
-> (SMTConfig -> a -> QueryT m b -> IO c)
-> [QueryT m b]
-> a
-> IO (Solver, NominalDiffTime, c)
sbvConcurrentWithAny SMTConfig
solver SMTConfig -> a -> Query b -> IO SMTResult
forall {m :: * -> *} {a} {a}.
SatisfiableM m a =>
SMTConfig -> a -> QueryT m a -> m SMTResult
go [Query b]
qs a
a
                                      return (slvr, time, SatResult result)
  where go :: SMTConfig -> a -> QueryT m a -> m SMTResult
go SMTConfig
cfg a
a' QueryT m a
q = (a -> SymbolicT m SBool)
-> Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
forall (m :: * -> *) a b.
ExtractIO m =>
(a -> SymbolicT m SBool)
-> Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery a -> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce Bool
True (do _ <- QueryT m a
q; checkNoOptimizations >> Control.getSMTResult) SMTConfig
cfg a
a'

-- | Find a satisfying assignment to a property using a single solver, but run
-- each query problem in a separate isolated thread and wait for each thread to
-- finish. See 'satConcurrentWithAny' for more details.
satConcurrentWithAll :: Satisfiable a => SMTConfig -> [Query b] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
satConcurrentWithAll :: forall a b.
Satisfiable a =>
SMTConfig
-> [Query b] -> a -> IO [(Solver, NominalDiffTime, SatResult)]
satConcurrentWithAll SMTConfig
solver [Query b]
qs a
a = do results <- SMTConfig
-> (SMTConfig -> a -> Query b -> IO SMTResult)
-> [Query b]
-> a
-> IO [(Solver, NominalDiffTime, SMTResult)]
forall c a (m :: * -> *) b.
NFData c =>
SMTConfig
-> (SMTConfig -> a -> QueryT m b -> IO c)
-> [QueryT m b]
-> a
-> IO [(Solver, NominalDiffTime, c)]
sbvConcurrentWithAll SMTConfig
solver SMTConfig -> a -> Query b -> IO SMTResult
forall {m :: * -> *} {a} {a}.
SatisfiableM m a =>
SMTConfig -> a -> QueryT m a -> m SMTResult
go [Query b]
qs a
a
                                      return $ (\(Solver
a',NominalDiffTime
b,SMTResult
c) -> (Solver
a',NominalDiffTime
b,SMTResult -> SatResult
SatResult SMTResult
c)) <$> results
  where go :: SMTConfig -> a -> QueryT m a -> m SMTResult
go SMTConfig
cfg a
a' QueryT m a
q = (a -> SymbolicT m SBool)
-> Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
forall (m :: * -> *) a b.
ExtractIO m =>
(a -> SymbolicT m SBool)
-> Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery a -> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce Bool
True (do _ <- QueryT m a
q; checkNoOptimizations >> Control.getSMTResult) SMTConfig
cfg a
a'

-- | A type @a@ is provable if we can turn it into a predicate, i.e., it has to return a boolean.
-- This class captures essentially prove calls.
class ExtractIO m => ProvableM m a where
  -- | Reduce an arg, for proof purposes.
  proofArgReduce :: a -> SymbolicT m SBool

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

  -- | Generalization of 'Data.SBV.proveWith'
  proveWith :: SMTConfig -> a -> m ThmResult
  proveWith SMTConfig
cfg a
a = do r <- (a -> SymbolicT m SBool)
-> Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
forall (m :: * -> *) a b.
ExtractIO m =>
(a -> SymbolicT m SBool)
-> Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery a -> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce Bool
False (QueryT m ()
forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
forall a b. QueryT m a -> QueryT m b -> QueryT m b
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
                       ThmResult <$> if validationRequested cfg
                                     then validate proofArgReduce False cfg a r
                                     else return r

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

  -- | Generalization of 'Data.SBV.dproveWith'
  dproveWith :: SMTConfig -> a -> m ThmResult
  dproveWith SMTConfig
cfg a
a = do r <- (a -> SymbolicT m SBool)
-> Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
forall (m :: * -> *) a b.
ExtractIO m =>
(a -> SymbolicT m SBool)
-> Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery a -> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce Bool
False (QueryT m ()
forall (m :: * -> *). MonadIO m => QueryT m ()
checkNoOptimizations QueryT m () -> QueryT m SMTResult -> QueryT m SMTResult
forall a b. QueryT m a -> QueryT m b -> QueryT m b
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
                        ThmResult <$> if validationRequested cfg
                                      then validate proofArgReduce False cfg a r
                                      else return r

  -- | Generalization of 'Data.SBV.isVacuousProof'
  isVacuousProof :: a -> m Bool
  isVacuousProof = SMTConfig -> a -> m Bool
forall (m :: * -> *) a. ProvableM m a => SMTConfig -> a -> m Bool
isVacuousProofWith SMTConfig
defaultSMTCfg

  -- | Generalization of 'Data.SBV.isVacuousProofWith'
  isVacuousProofWith :: SMTConfig -> a -> m Bool
  isVacuousProofWith SMTConfig
cfg a
a = -- NB. Can't call runWithQuery since last constraint would become the implication!
       (Bool, Result) -> Bool
forall a b. (a, b) -> a
fst ((Bool, Result) -> Bool) -> m (Bool, Result) -> m Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SMTConfig -> SBVRunMode -> SymbolicT m Bool -> m (Bool, Result)
forall (m :: * -> *) a.
MonadIO m =>
SMTConfig -> SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic SMTConfig
cfg (QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
SMTMode QueryContext
QueryInternal IStage
ISetup Bool
True SMTConfig
cfg) (a -> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce a
a SymbolicT m SBool -> SymbolicT m Bool -> SymbolicT m Bool
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
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 = do cs <- QueryT m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
Control.checkSat
                  case cs of
                    CheckSatResult
Control.Unsat  -> Bool -> QueryT m Bool
forall a. a -> QueryT m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
                    CheckSatResult
Control.Sat    -> Bool -> QueryT m Bool
forall a. a -> QueryT m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                    Control.DSat{} -> Bool -> QueryT m Bool
forall a. a -> QueryT m a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
                    CheckSatResult
Control.Unk    -> String -> QueryT m Bool
forall a. HasCallStack => String -> a
error String
"SBV: isVacuous: Solver returned unknown!"

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

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

-- | Prove a property with multiple solvers, running them in separate threads. Only
-- the result of the first one to finish will be returned, remaining threads will be killed.
-- Note that we send an exception to the losing processes, but we do *not* actually wait for them
-- to finish. In rare cases this can lead to zombie processes. In previous experiments, we found
-- that some processes take their time to terminate. So, this solution favors quick turnaround.
proveWithAny :: Provable a => [SMTConfig] -> a -> IO (Solver, NominalDiffTime, ThmResult)
proveWithAny :: forall a.
Provable a =>
[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.
ProvableM m a =>
SMTConfig -> a -> m ThmResult
proveWith)

-- | Prove a property with multiple solvers, running them in separate threads. The
-- results will be returned in the order produced.
proveWithAll :: Provable a => [SMTConfig] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
proveWithAll :: forall a.
Provable a =>
[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.
ProvableM m a =>
SMTConfig -> a -> m ThmResult
proveWith)

-- | Prove a property by running many queries each isolated to their own thread
-- concurrently and return the first that finishes, killing the others
proveConcurrentWithAny :: Provable a => SMTConfig -> [Query b] -> a -> IO (Solver, NominalDiffTime, ThmResult)
proveConcurrentWithAny :: forall a b.
Provable a =>
SMTConfig
-> [Query b] -> a -> IO (Solver, NominalDiffTime, ThmResult)
proveConcurrentWithAny SMTConfig
solver [Query b]
qs a
a = do (slvr,time,result) <- SMTConfig
-> (SMTConfig -> a -> Query b -> IO SMTResult)
-> [Query b]
-> a
-> IO (Solver, NominalDiffTime, SMTResult)
forall c a (m :: * -> *) b.
NFData c =>
SMTConfig
-> (SMTConfig -> a -> QueryT m b -> IO c)
-> [QueryT m b]
-> a
-> IO (Solver, NominalDiffTime, c)
sbvConcurrentWithAny SMTConfig
solver SMTConfig -> a -> Query b -> IO SMTResult
forall {m :: * -> *} {a} {a}.
ProvableM m a =>
SMTConfig -> a -> QueryT m a -> m SMTResult
go [Query b]
qs a
a
                                        return (slvr, time, ThmResult result)
  where go :: SMTConfig -> a -> QueryT m a -> m SMTResult
go SMTConfig
cfg a
a' QueryT m a
q = (a -> SymbolicT m SBool)
-> Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
forall (m :: * -> *) a b.
ExtractIO m =>
(a -> SymbolicT m SBool)
-> Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery a -> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce Bool
False (do _ <- QueryT m a
q;  checkNoOptimizations >> Control.getSMTResult) SMTConfig
cfg a
a'

-- | Prove a property by running many queries each isolated to their own thread
-- concurrently and wait for each to finish returning all results
proveConcurrentWithAll :: Provable a => SMTConfig -> [Query b] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
proveConcurrentWithAll :: forall a b.
Provable a =>
SMTConfig
-> [Query b] -> a -> IO [(Solver, NominalDiffTime, ThmResult)]
proveConcurrentWithAll SMTConfig
solver [Query b]
qs a
a = do results <- SMTConfig
-> (SMTConfig -> a -> Query b -> IO SMTResult)
-> [Query b]
-> a
-> IO [(Solver, NominalDiffTime, SMTResult)]
forall c a (m :: * -> *) b.
NFData c =>
SMTConfig
-> (SMTConfig -> a -> QueryT m b -> IO c)
-> [QueryT m b]
-> a
-> IO [(Solver, NominalDiffTime, c)]
sbvConcurrentWithAll SMTConfig
solver SMTConfig -> a -> Query b -> IO SMTResult
forall {m :: * -> *} {a} {a}.
ProvableM m a =>
SMTConfig -> a -> QueryT m a -> m SMTResult
go [Query b]
qs a
a
                                        return $ (\(Solver
a',NominalDiffTime
b,SMTResult
c) -> (Solver
a',NominalDiffTime
b,SMTResult -> ThmResult
ThmResult SMTResult
c)) <$> results
  where go :: SMTConfig -> a -> QueryT m a -> m SMTResult
go SMTConfig
cfg a
a' QueryT m a
q = (a -> SymbolicT m SBool)
-> Bool -> QueryT m SMTResult -> SMTConfig -> a -> m SMTResult
forall (m :: * -> *) a b.
ExtractIO m =>
(a -> SymbolicT m SBool)
-> Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery a -> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce Bool
False (do _ <- QueryT m a
q; checkNoOptimizations >> Control.getSMTResult) SMTConfig
cfg a
a'

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

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

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

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

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

        check :: [(NamedSymVar, CV)] -> m SMTResult
check [(NamedSymVar, CV)]
env = do let envShown :: String
envShown = Bool -> Bool -> SMTConfig -> [(String, GeneralizedCV)] -> String
showModelDictionary Bool
True Bool
True SMTConfig
cfg [(String, GeneralizedCV)]
modelBinds
                              where modelBinds :: [(String, GeneralizedCV)]
modelBinds = [(Text -> String
T.unpack Text
n, CV -> GeneralizedCV
RegularCV CV
v) | (NamedSymVar SV
_ Text
n, CV
v) <- [(NamedSymVar, CV)]
env]

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

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

                       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
<$> SMTConfig -> SBVRunMode -> SymbolicT m SBool -> m (SBool, Result)
forall (m :: * -> *) a.
MonadIO m =>
SMTConfig -> SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic SMTConfig
cfg (Maybe (Bool, [(NamedSymVar, CV)]) -> SBVRunMode
Concrete ((Bool, [(NamedSymVar, CV)]) -> Maybe (Bool, [(NamedSymVar, CV)])
forall a. a -> Maybe a
Just (Bool
isSAT, [(NamedSymVar, CV)]
env))) (a -> SymbolicT m SBool
reducer a
p SymbolicT m SBool
-> (SBool -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
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
forall (m :: * -> *). MonadSymbolic m => SBool -> m SBool
output)

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

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

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

                           notConcrete SV
sv = String -> [String] -> m SMTResult
forall {m :: * -> *}. Monad m => String -> [String] -> m SMTResult
wrap (String
"Data.SBV: Cannot validate the model, since " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
sv String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is not concretely computable.")
                                                 (  Maybe String -> [String]
perhaps (SV -> Maybe String
why SV
sv)
                                                 )
                                where perhaps :: Maybe String -> [String]
perhaps Maybe String
Nothing  = case Result -> [(String, CV -> Bool, SV)]
resObservables Result
result of
                                                           [] -> []
                                                           [(String, CV -> Bool, SV)]
xs -> [ String
"There are observable values in the model: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String -> String
forall a. Show a => a -> String
show String
n | (String
n, CV -> Bool
_, SV
_) <- [(String, CV -> Bool, SV)]
xs]
                                                                 , String
"SBV cannot validate in the presence of observables, unfortunately."
                                                                 , String
"Try validation after removing calls to 'observe'."
                                                                 ]

                                      perhaps (Just String
x) = [ String
x
                                                         , String
""
                                                         , String
"SBV's model validator is incomplete, and cannot handle this particular case."
                                                         , String
"Please report this as a feature request or possibly a bug!"
                                                         ]

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

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

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

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

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

                       notify $ if null cstrs
                                then "There are no constraints to check."
                                else "Validating " ++ show (length cstrs) ++ " constraint(s)."

                       walkConstraints cstrs (checkOutputs (resOutputs result))

-- | Given a satisfiability problem, extract the function definitions in it
defs2smt :: SatisfiableM m a => a -> m String
defs2smt :: forall (m :: * -> *) a. SatisfiableM m a => a -> m String
defs2smt = Bool
-> (a -> SymbolicT m SBool)
-> (SMTLibPgm -> String)
-> a
-> m String
forall (m :: * -> *) a b.
MonadIO m =>
Bool -> (a -> SymbolicT m SBool) -> (SMTLibPgm -> b) -> a -> m b
generateSMTBenchMarkGen Bool
True a -> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce SMTLibPgm -> String
defs
  where defs :: SMTLibPgm -> String
defs (SMTLibPgm SMTLibVersion
_ [String]
_ [String]
ds) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String]
ds

-- | Create an SMT-Lib2 benchmark, for a SAT query.
generateSMTBenchmarkSat :: SatisfiableM m a => a -> m String
generateSMTBenchmarkSat :: forall (m :: * -> *) a. SatisfiableM m a => a -> m String
generateSMTBenchmarkSat = Bool
-> (a -> SymbolicT m SBool)
-> (SMTLibPgm -> String)
-> a
-> m String
forall (m :: * -> *) a b.
MonadIO m =>
Bool -> (a -> SymbolicT m SBool) -> (SMTLibPgm -> b) -> a -> m b
generateSMTBenchMarkGen Bool
True a -> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce (\SMTLibPgm
p -> SMTLibPgm -> String
forall a. Show a => a -> String
show SMTLibPgm
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n(check-sat)\n")

-- | Create an SMT-Lib2 benchmark, for a Proof query.
generateSMTBenchmarkProof :: ProvableM m a => a -> m String
generateSMTBenchmarkProof :: forall (m :: * -> *) a. ProvableM m a => a -> m String
generateSMTBenchmarkProof = Bool
-> (a -> SymbolicT m SBool)
-> (SMTLibPgm -> String)
-> a
-> m String
forall (m :: * -> *) a b.
MonadIO m =>
Bool -> (a -> SymbolicT m SBool) -> (SMTLibPgm -> b) -> a -> m b
generateSMTBenchMarkGen Bool
False a -> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce (\SMTLibPgm
p -> SMTLibPgm -> String
forall a. Show a => a -> String
show SMTLibPgm
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n(check-sat)\n")

-- | Generic benchmark creator
generateSMTBenchMarkGen :: MonadIO m => Bool -> (a -> SymbolicT m SBool) -> (SMTLibPgm -> b) -> a -> m b
generateSMTBenchMarkGen :: forall (m :: * -> *) a b.
MonadIO m =>
Bool -> (a -> SymbolicT m SBool) -> (SMTLibPgm -> b) -> a -> m b
generateSMTBenchMarkGen Bool
isSat a -> SymbolicT m SBool
reduce SMTLibPgm -> b
render a
a = do
      t <- IO ZonedTime -> m ZonedTime
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO IO ZonedTime
getZonedTime

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

      (_, res) <- runSymbolic cfg (SMTMode QueryInternal ISetup isSat cfg) $ reduce a >>= output

      let SMTProblem{smtLibPgm} = Control.runProofOn (SMTMode QueryInternal IRun isSat cfg) QueryInternal comments res

      return $ render (smtLibPgm cfg)

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

                          unless (null objectives) $
                                error $ unlines [ ""
                                                , "*** Data.SBV: Unsupported call sat/prove when optimization objectives are present."
                                                , "*** Use \"optimize\"/\"optimizeWith\" to calculate optimal satisfaction!"
                                                ]

instance ExtractIO m => SatisfiableM m (SymbolicT m ()) where satArgReduce :: SymbolicT m () -> SymbolicT m SBool
satArgReduce SymbolicT m ()
a = SymbolicT m SBool -> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce ((SymbolicT m ()
a SymbolicT m () -> SymbolicT m SBool -> SymbolicT m SBool
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SBool -> SymbolicT m SBool
forall a. a -> SymbolicT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SBool
sTrue) :: SymbolicT m SBool)
-- instance ExtractIO m => ProvableM m (SymbolicT m ())  -- NO INSTANCE ON PURPOSE; don't want to prove goals

instance ExtractIO m => SatisfiableM m (SymbolicT m SBool) where satArgReduce :: SymbolicT m SBool -> SymbolicT m SBool
satArgReduce   = SymbolicT m SBool -> SymbolicT m SBool
forall a. a -> a
id
instance ExtractIO m => ProvableM    m (SymbolicT m SBool) where proofArgReduce :: SymbolicT m SBool -> SymbolicT m SBool
proofArgReduce = SymbolicT m SBool -> SymbolicT m SBool
forall a. a -> a
id

instance ExtractIO m => SatisfiableM m SBool where satArgReduce :: SBool -> SymbolicT m SBool
satArgReduce   = SBool -> SymbolicT m SBool
forall a. a -> SymbolicT m a
forall (m :: * -> *) a. Monad m => a -> m a
return
instance ExtractIO m => ProvableM    m SBool where proofArgReduce :: SBool -> SymbolicT m SBool
proofArgReduce = SBool -> SymbolicT m SBool
forall a. a -> SymbolicT m a
forall (m :: * -> *) a. Monad m => a -> m a
return

instance {-# OVERLAPPABLE #-} (ExtractIO m, SatisfiableM m a) => SatisfiableM m (SymbolicT m a) where satArgReduce :: SymbolicT m a -> SymbolicT m SBool
satArgReduce   SymbolicT m a
a = SymbolicT m a
a SymbolicT m a -> (a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce
instance {-# OVERLAPPABLE #-} (ExtractIO m, ProvableM    m a) => ProvableM    m (SymbolicT m a) where proofArgReduce :: SymbolicT m a -> SymbolicT m SBool
proofArgReduce SymbolicT m a
a = SymbolicT m a
a SymbolicT m a -> (a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= a -> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce

instance (ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r) => SatisfiableM m (Forall nm a -> r) where
  satArgReduce :: (Forall nm a -> r) -> SymbolicT m SBool
satArgReduce = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce (SBool -> SymbolicT m SBool)
-> ((Forall nm a -> r) -> SBool)
-> (Forall nm a -> r)
-> SymbolicT m SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Forall nm a -> r) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

instance (ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r) => ProvableM m (Forall nm a -> r) where
  proofArgReduce :: (Forall nm a -> r) -> SymbolicT m SBool
proofArgReduce = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce (SBool -> SymbolicT m SBool)
-> ((Forall nm a -> r) -> SBool)
-> (Forall nm a -> r)
-> SymbolicT m SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Forall nm a -> r) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

instance (ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r) => SatisfiableM m (Exists nm a -> r) where
  satArgReduce :: (Exists nm a -> r) -> SymbolicT m SBool
satArgReduce = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce (SBool -> SymbolicT m SBool)
-> ((Exists nm a -> r) -> SBool)
-> (Exists nm a -> r)
-> SymbolicT m SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Exists nm a -> r) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

instance (ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r, EqSymbolic (SBV a)) => SatisfiableM m (ExistsUnique nm a -> r) where
  satArgReduce :: (ExistsUnique nm a -> r) -> SymbolicT m SBool
satArgReduce = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce (SBool -> SymbolicT m SBool)
-> ((ExistsUnique nm a -> r) -> SBool)
-> (ExistsUnique nm a -> r)
-> SymbolicT m SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ExistsUnique nm a -> r) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

instance (KnownNat n, ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r) => ProvableM m (ForallN n nm a -> r) where
  proofArgReduce :: (ForallN n nm a -> r) -> SymbolicT m SBool
proofArgReduce = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce (SBool -> SymbolicT m SBool)
-> ((ForallN n nm a -> r) -> SBool)
-> (ForallN n nm a -> r)
-> SymbolicT m SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ForallN n nm a -> r) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

instance (KnownNat n, ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r) => SatisfiableM m (ExistsN n nm a -> r) where
  satArgReduce :: (ExistsN n nm a -> r) -> SymbolicT m SBool
satArgReduce = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce (SBool -> SymbolicT m SBool)
-> ((ExistsN n nm a -> r) -> SBool)
-> (ExistsN n nm a -> r)
-> SymbolicT m SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ExistsN n nm a -> r) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

instance (ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r) => ProvableM m (Exists nm a -> r) where
  proofArgReduce :: (Exists nm a -> r) -> SymbolicT m SBool
proofArgReduce = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce (SBool -> SymbolicT m SBool)
-> ((Exists nm a -> r) -> SBool)
-> (Exists nm a -> r)
-> SymbolicT m SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Exists nm a -> r) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

instance (ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r, EqSymbolic (SBV a)) => ProvableM m (ExistsUnique nm a -> r) where
  proofArgReduce :: (ExistsUnique nm a -> r) -> SymbolicT m SBool
proofArgReduce = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce (SBool -> SymbolicT m SBool)
-> ((ExistsUnique nm a -> r) -> SBool)
-> (ExistsUnique nm a -> r)
-> SymbolicT m SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ExistsUnique nm a -> r) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

instance (KnownNat n, ExtractIO m, SymVal a, Constraint Symbolic r, SatisfiableM m r) => SatisfiableM m (ForallN n nm a -> r) where
  satArgReduce :: (ForallN n nm a -> r) -> SymbolicT m SBool
satArgReduce = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce (SBool -> SymbolicT m SBool)
-> ((ForallN n nm a -> r) -> SBool)
-> (ForallN n nm a -> r)
-> SymbolicT m SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ForallN n nm a -> r) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

instance (KnownNat n, ExtractIO m, SymVal a, Constraint Symbolic r, ProvableM m r) => ProvableM m (ExistsN n nm a -> r) where
  proofArgReduce :: (ExistsN n nm a -> r) -> SymbolicT m SBool
proofArgReduce = SBool -> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce (SBool -> SymbolicT m SBool)
-> ((ExistsN n nm a -> r) -> SBool)
-> (ExistsN n nm a -> r)
-> SymbolicT m SBool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ExistsN n nm a -> r) -> SBool
forall a. QuantifiedBool a => a -> SBool
quantifiedBool

{-
-- The following is a possible definition, but it lets us write properties that
-- are not useful.. Such as: prove $ \x y -> (x::SInt8) == y
-- Running that will throw an exception since Haskell's equality is not be supported by symbolic things. (Needs .==).
-- So, we avoid these insteances.
instance ExtractIO m => ProvableM m Bool where
  proofArgReduce x  = proofArgReduce (if x then sTrue else sFalse :: SBool)

instance ExtractIO m => SatisfiableM m Bool where
  satArgReduce x  = satArgReduce (if x then sTrue else sFalse :: SBool)
-}

-- | Create an argument
mkArg :: (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg :: forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg = VarContext -> Maybe String -> m (SBV a)
forall a (m :: * -> *).
(SymVal a, MonadSymbolic m) =>
VarContext -> Maybe String -> m (SBV a)
forall (m :: * -> *).
MonadSymbolic m =>
VarContext -> Maybe String -> m (SBV a)
mkSymVal (Maybe Quantifier -> VarContext
NonQueryVar Maybe Quantifier
forall a. Maybe a
Nothing) Maybe String
forall a. Maybe a
Nothing

-- Functions
instance (SymVal a, SatisfiableM m p) => SatisfiableM m (SBV a -> p) where
  satArgReduce :: (SBV a -> p) -> SymbolicT m SBool
satArgReduce SBV a -> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> p -> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SBV a -> p
fn SBV a
a

instance (SymVal a, ProvableM m p) => ProvableM m (SBV a -> p) where
  proofArgReduce :: (SBV a -> p) -> SymbolicT m SBool
proofArgReduce SBV a -> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> p -> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce (p -> SymbolicT m SBool) -> p -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ SBV a -> p
fn SBV a
a

-- 2 Tuple
instance (SymVal a, SymVal b, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b) -> p) where
  satArgReduce :: ((SBV a, SBV b) -> p) -> SymbolicT m SBool
satArgReduce (SBV a, SBV b) -> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce ((SBV b -> p) -> SymbolicT m SBool)
-> (SBV b -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b -> (SBV a, SBV b) -> p
fn (SBV a
a, SBV b
b)

instance (SymVal a, SymVal b, ProvableM m p) => ProvableM m ((SBV a, SBV b) -> p) where
  proofArgReduce :: ((SBV a, SBV b) -> p) -> SymbolicT m SBool
proofArgReduce (SBV a, SBV b) -> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce ((SBV b -> p) -> SymbolicT m SBool)
-> (SBV b -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b -> (SBV a, SBV b) -> p
fn (SBV a
a, SBV b
b)

-- 3 Tuple
instance (SymVal a, SymVal b, SymVal c, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c) -> p) where
  satArgReduce :: ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
satArgReduce (SBV a, SBV b, SBV c) -> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce ((SBV b -> SBV c -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c -> (SBV a, SBV b, SBV c) -> p
fn (SBV a
a, SBV b
b, SBV c
c)

instance (SymVal a, SymVal b, SymVal c, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c) -> p) where
  proofArgReduce :: ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m SBool
proofArgReduce (SBV a, SBV b, SBV c) -> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce ((SBV b -> SBV c -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c -> (SBV a, SBV b, SBV c) -> p
fn (SBV a
a, SBV b
b, SBV c
c)

-- 4 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d) -> p) where
  satArgReduce :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
satArgReduce (SBV a, SBV b, SBV c, SBV d) -> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg  SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce ((SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d -> (SBV a, SBV b, SBV c, SBV d) -> p
fn (SBV a
a, SBV b
b, SBV c
c, SBV d
d)

instance (SymVal a, SymVal b, SymVal c, SymVal d, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d) -> p) where
  proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m SBool
proofArgReduce (SBV a, SBV b, SBV c, SBV d) -> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg  SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce ((SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d -> (SBV a, SBV b, SBV c, SBV d) -> p
fn (SBV a
a, SBV b
b, SBV c
c, SBV d
d)

-- 5 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) where
  satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
satArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce ((SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
fn (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e)

instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) where
  proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m SBool
proofArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce ((SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
fn (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e)

-- 6 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) where
  satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m SBool
satArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
 -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
fn (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f)

instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) where
  proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p)
-> SymbolicT m SBool
proofArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
 -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
fn (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f)

-- 7 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) where
  satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m SBool
satArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
 -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f SBV g
g -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
fn (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g)

instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) where
  proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m SBool
proofArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
 -> SymbolicT m SBool)
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f SBV g
g -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
fn (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g)

-- 8 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) where
  satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p)
-> SymbolicT m SBool
satArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV h -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV h -> p)
 -> SymbolicT m SBool)
-> (SBV b
    -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV h -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f SBV g
g SBV h
h -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p
fn (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g, SBV h
h)

instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p) where
  proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p)
-> SymbolicT m SBool
proofArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV h -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV h -> p)
 -> SymbolicT m SBool)
-> (SBV b
    -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV h -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f SBV g
g SBV h
h -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h) -> p
fn (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g, SBV h
h)

-- 9 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) where
  satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i)
 -> p)
-> SymbolicT m SBool
satArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i)
-> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b
 -> SBV c
 -> SBV d
 -> SBV e
 -> SBV f
 -> SBV g
 -> SBV h
 -> SBV i
 -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce ((SBV b
  -> SBV c
  -> SBV d
  -> SBV e
  -> SBV f
  -> SBV g
  -> SBV h
  -> SBV i
  -> p)
 -> SymbolicT m SBool)
-> (SBV b
    -> SBV c
    -> SBV d
    -> SBV e
    -> SBV f
    -> SBV g
    -> SBV h
    -> SBV i
    -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f SBV g
g SBV h
h SBV i
i -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i)
-> p
fn (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g, SBV h
h, SBV i
i)

instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i) -> p) where
  proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i)
 -> p)
-> SymbolicT m SBool
proofArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i)
-> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b
 -> SBV c
 -> SBV d
 -> SBV e
 -> SBV f
 -> SBV g
 -> SBV h
 -> SBV i
 -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce ((SBV b
  -> SBV c
  -> SBV d
  -> SBV e
  -> SBV f
  -> SBV g
  -> SBV h
  -> SBV i
  -> p)
 -> SymbolicT m SBool)
-> (SBV b
    -> SBV c
    -> SBV d
    -> SBV e
    -> SBV f
    -> SBV g
    -> SBV h
    -> SBV i
    -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f SBV g
g SBV h
h SBV i
i -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i)
-> p
fn (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g, SBV h
h, SBV i
i)

-- 10 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SymVal j, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) where
  satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i,
  SBV j)
 -> p)
-> SymbolicT m SBool
satArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i,
 SBV j)
-> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b
 -> SBV c
 -> SBV d
 -> SBV e
 -> SBV f
 -> SBV g
 -> SBV h
 -> SBV i
 -> SBV j
 -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce ((SBV b
  -> SBV c
  -> SBV d
  -> SBV e
  -> SBV f
  -> SBV g
  -> SBV h
  -> SBV i
  -> SBV j
  -> p)
 -> SymbolicT m SBool)
-> (SBV b
    -> SBV c
    -> SBV d
    -> SBV e
    -> SBV f
    -> SBV g
    -> SBV h
    -> SBV i
    -> SBV j
    -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f SBV g
g SBV h
h SBV i
i SBV j
j -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i,
 SBV j)
-> p
fn (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g, SBV h
h, SBV i
i, SBV j
j)

instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SymVal j, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j) -> p) where
  proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i,
  SBV j)
 -> p)
-> SymbolicT m SBool
proofArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i,
 SBV j)
-> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b
 -> SBV c
 -> SBV d
 -> SBV e
 -> SBV f
 -> SBV g
 -> SBV h
 -> SBV i
 -> SBV j
 -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce ((SBV b
  -> SBV c
  -> SBV d
  -> SBV e
  -> SBV f
  -> SBV g
  -> SBV h
  -> SBV i
  -> SBV j
  -> p)
 -> SymbolicT m SBool)
-> (SBV b
    -> SBV c
    -> SBV d
    -> SBV e
    -> SBV f
    -> SBV g
    -> SBV h
    -> SBV i
    -> SBV j
    -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f SBV g
g SBV h
h SBV i
i SBV j
j -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i,
 SBV j)
-> p
fn (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g, SBV h
h, SBV i
i, SBV j
j)

-- 11 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SymVal j, SymVal k, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) where
  satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i,
  SBV j, SBV k)
 -> p)
-> SymbolicT m SBool
satArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i,
 SBV j, SBV k)
-> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b
 -> SBV c
 -> SBV d
 -> SBV e
 -> SBV f
 -> SBV g
 -> SBV h
 -> SBV i
 -> SBV j
 -> SBV k
 -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce ((SBV b
  -> SBV c
  -> SBV d
  -> SBV e
  -> SBV f
  -> SBV g
  -> SBV h
  -> SBV i
  -> SBV j
  -> SBV k
  -> p)
 -> SymbolicT m SBool)
-> (SBV b
    -> SBV c
    -> SBV d
    -> SBV e
    -> SBV f
    -> SBV g
    -> SBV h
    -> SBV i
    -> SBV j
    -> SBV k
    -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f SBV g
g SBV h
h SBV i
i SBV j
j SBV k
k -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i,
 SBV j, SBV k)
-> p
fn (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g, SBV h
h, SBV i
i, SBV j
j, SBV k
k)

instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SymVal j, SymVal k, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k) -> p) where
  proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i,
  SBV j, SBV k)
 -> p)
-> SymbolicT m SBool
proofArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i,
 SBV j, SBV k)
-> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b
 -> SBV c
 -> SBV d
 -> SBV e
 -> SBV f
 -> SBV g
 -> SBV h
 -> SBV i
 -> SBV j
 -> SBV k
 -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce ((SBV b
  -> SBV c
  -> SBV d
  -> SBV e
  -> SBV f
  -> SBV g
  -> SBV h
  -> SBV i
  -> SBV j
  -> SBV k
  -> p)
 -> SymbolicT m SBool)
-> (SBV b
    -> SBV c
    -> SBV d
    -> SBV e
    -> SBV f
    -> SBV g
    -> SBV h
    -> SBV i
    -> SBV j
    -> SBV k
    -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f SBV g
g SBV h
h SBV i
i SBV j
j SBV k
k -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i,
 SBV j, SBV k)
-> p
fn (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g, SBV h
h, SBV i
i, SBV j
j, SBV k
k)

-- 12 Tuple
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SymVal j, SymVal k, SymVal l, SatisfiableM m p) => SatisfiableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) where
  satArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i,
  SBV j, SBV k, SBV l)
 -> p)
-> SymbolicT m SBool
satArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i,
 SBV j, SBV k, SBV l)
-> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b
 -> SBV c
 -> SBV d
 -> SBV e
 -> SBV f
 -> SBV g
 -> SBV h
 -> SBV i
 -> SBV j
 -> SBV k
 -> SBV l
 -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. SatisfiableM m a => a -> SymbolicT m SBool
satArgReduce ((SBV b
  -> SBV c
  -> SBV d
  -> SBV e
  -> SBV f
  -> SBV g
  -> SBV h
  -> SBV i
  -> SBV j
  -> SBV k
  -> SBV l
  -> p)
 -> SymbolicT m SBool)
-> (SBV b
    -> SBV c
    -> SBV d
    -> SBV e
    -> SBV f
    -> SBV g
    -> SBV h
    -> SBV i
    -> SBV j
    -> SBV k
    -> SBV l
    -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f SBV g
g SBV h
h SBV i
i SBV j
j SBV k
k SBV l
l -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i,
 SBV j, SBV k, SBV l)
-> p
fn (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g, SBV h
h, SBV i
i, SBV j
j, SBV k
k, SBV l
l)

instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SymVal h, SymVal i, SymVal j, SymVal k, SymVal l, ProvableM m p) => ProvableM m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i, SBV j, SBV k, SBV l) -> p) where
  proofArgReduce :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i,
  SBV j, SBV k, SBV l)
 -> p)
-> SymbolicT m SBool
proofArgReduce (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i,
 SBV j, SBV k, SBV l)
-> p
fn = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a)
-> (SBV a -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b
 -> SBV c
 -> SBV d
 -> SBV e
 -> SBV f
 -> SBV g
 -> SBV h
 -> SBV i
 -> SBV j
 -> SBV k
 -> SBV l
 -> p)
-> SymbolicT m SBool
forall (m :: * -> *) a. ProvableM m a => a -> SymbolicT m SBool
proofArgReduce ((SBV b
  -> SBV c
  -> SBV d
  -> SBV e
  -> SBV f
  -> SBV g
  -> SBV h
  -> SBV i
  -> SBV j
  -> SBV k
  -> SBV l
  -> p)
 -> SymbolicT m SBool)
-> (SBV b
    -> SBV c
    -> SBV d
    -> SBV e
    -> SBV f
    -> SBV g
    -> SBV h
    -> SBV i
    -> SBV j
    -> SBV k
    -> SBV l
    -> p)
-> SymbolicT m SBool
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f SBV g
g SBV h
h SBV i
i SBV j
j SBV k
k SBV l
l -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g, SBV h, SBV i,
 SBV j, SBV k, SBV l)
-> p
fn (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g, SBV h
h, SBV i
i, SBV j
j, SBV k
k, SBV l
l)

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

-- | Runs with a query.
runWithQuery :: ExtractIO m => (a -> SymbolicT m SBool) -> Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery :: forall (m :: * -> *) a b.
ExtractIO m =>
(a -> SymbolicT m SBool)
-> Bool -> QueryT m b -> SMTConfig -> a -> m b
runWithQuery a -> SymbolicT m SBool
reducer Bool
isSAT QueryT m b
q SMTConfig
cfg a
a = (b, Result) -> b
forall a b. (a, b) -> a
fst ((b, Result) -> b) -> m (b, Result) -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SMTConfig -> SBVRunMode -> SymbolicT m b -> m (b, Result)
forall (m :: * -> *) a.
MonadIO m =>
SMTConfig -> SBVRunMode -> SymbolicT m a -> m (a, Result)
runSymbolic SMTConfig
cfg (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 _ <- a -> SymbolicT m SBool
reducer a
a SymbolicT m SBool
-> (SBool -> SymbolicT m SBool) -> SymbolicT m SBool
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
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
forall (m :: * -> *). MonadSymbolic m => SBool -> m SBool
output
                   Control.executeQuery QueryInternal q

-- | Check if a safe-call was safe or not, turning a t'SafeResult' to a Bool.
isSafe :: SafeResult -> Bool
isSafe :: SafeResult -> Bool
isSafe (SafeResult (Maybe String
_, String
_, SMTResult
result)) = case SMTResult
result of
                                       Unsatisfiable{} -> Bool
True
                                       Satisfiable{}   -> Bool
False
                                       DeltaSat{}      -> Bool
False   -- conservative
                                       SatExtField{}   -> Bool
False   -- conservative
                                       Unknown{}       -> Bool
False   -- conservative
                                       ProofError{}    -> Bool
False   -- conservative

-- | Perform an action asynchronously, returning results together with diff-time.
runInThread :: NFData b => UTCTime -> (SMTConfig -> IO b) -> SMTConfig -> IO (Async (Solver, NominalDiffTime, b))
runInThread :: forall b.
NFData b =>
UTCTime
-> (SMTConfig -> IO b)
-> SMTConfig
-> IO (Async (Solver, NominalDiffTime, b))
runInThread UTCTime
beginTime SMTConfig -> IO b
action SMTConfig
config = IO (Solver, NominalDiffTime, b)
-> IO (Async (Solver, NominalDiffTime, b))
forall a. IO a -> IO (Async a)
async (IO (Solver, NominalDiffTime, b)
 -> IO (Async (Solver, NominalDiffTime, b)))
-> IO (Solver, NominalDiffTime, b)
-> IO (Async (Solver, NominalDiffTime, b))
forall a b. (a -> b) -> a -> b
$ do
                result  <- SMTConfig -> IO b
action SMTConfig
config
                endTime <- rnf result `seq` getCurrentTime
                return (name (solver config), endTime `diffUTCTime` beginTime, result)

-- | Perform action for all given configs, return the first one that wins. Note that we do
-- not wait for the other asyncs to terminate; hopefully they'll do so quickly.
sbvWithAny :: NFData b => [SMTConfig] -> (SMTConfig -> a -> IO b) -> a -> IO (Solver, NominalDiffTime, b)
sbvWithAny :: forall b a.
NFData b =>
[SMTConfig]
-> (SMTConfig -> a -> IO b) -> a -> IO (Solver, NominalDiffTime, b)
sbvWithAny []      SMTConfig -> a -> IO b
_    a
_ = String -> IO (Solver, NominalDiffTime, b)
forall a. HasCallStack => String -> a
error String
"SBV.withAny: No solvers given!"
sbvWithAny [SMTConfig]
solvers SMTConfig -> a -> IO b
what a
a = do beginTime <- IO UTCTime
getCurrentTime
                               snd `fmap` (mapM (runInThread beginTime (`what` a)) solvers >>= waitAnyFastCancel)
   where -- Async's `waitAnyCancel` nicely blocks; so we use this variant to ignore the
         -- wait part for killed threads.
         waitAnyFastCancel :: [Async a] -> IO (Async a, a)
waitAnyFastCancel [Async a]
asyncs = [Async a] -> IO (Async a, a)
forall {a}. [Async a] -> IO (Async a, a)
waitAny [Async a]
asyncs IO (Async a, a) -> IO () -> IO (Async a, a)
forall a b. IO a -> IO b -> IO a
`finally` (Async a -> IO ()) -> [Async a] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Async a -> IO ()
forall {a}. Async a -> IO ()
cancelFast [Async a]
asyncs
         cancelFast :: Async a -> IO ()
cancelFast Async a
other = ThreadId -> ExitCode -> IO ()
forall e. Exception e => ThreadId -> e -> IO ()
throwTo (Async a -> ThreadId
forall a. Async a -> ThreadId
asyncThreadId Async a
other) ExitCode
ExitSuccess


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


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

         go :: [Async a] -> IO [a]
go []  = [a] -> IO [a]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return []
         go [Async a]
as  = do (d, 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.
                     rs <- unsafeInterleaveIO $ go (filter (/= d) as)
                     return (r : rs)

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

-- | Symbolically executable program fragments. This class is mainly used for 'safe' calls, and is sufficiently populated internally to cover most use
-- cases. Users can extend it as they wish to allow 'safe' checks for SBV programs that return/take types that are user-defined.
class ExtractIO m => SExecutable m a where
   -- | Generalization of 'Data.SBV.sName'
   sName :: a -> SymbolicT m ()

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

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

           -- check that the cond is unsatisfiable. If satisfiable, that would
           -- indicate the assignment under which the 'Data.SBV.sAssert' would fail
           verify :: (FilePath -> FilePath) -> (String, Maybe CallStack, SV) -> QueryT m SafeResult
           verify :: (String -> String)
-> (String, Maybe CallStack, SV) -> QueryT m SafeResult
verify String -> String
mkRelative (String
msg, Maybe CallStack
cs, SV
cond) = do
                   let locInfo :: [(String, SrcLoc)] -> String
locInfo [(String, SrcLoc)]
ps = let loc :: (String, SrcLoc) -> String
loc (String
f, SrcLoc
sl) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String -> String
mkRelative (SrcLoc -> String
srcLocFile SrcLoc
sl), String
":", Int -> String
forall a. Show a => a -> String
show (SrcLoc -> Int
srcLocStartLine SrcLoc
sl), String
":", Int -> String
forall a. Show a => a -> String
show (SrcLoc -> Int
srcLocStartCol SrcLoc
sl), String
":", String
f]
                                    in String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
",\n " (((String, SrcLoc) -> String) -> [(String, SrcLoc)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, SrcLoc) -> String
loc [(String, SrcLoc)]
ps)
                       location :: Maybe String
location   = ([(String, SrcLoc)] -> String
locInfo ([(String, SrcLoc)] -> String)
-> (CallStack -> [(String, SrcLoc)]) -> CallStack -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CallStack -> [(String, SrcLoc)]
getCallStack) (CallStack -> String) -> Maybe CallStack -> Maybe String
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` Maybe CallStack
cs

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

                   return $ SafeResult (location, msg, result)

instance (ExtractIO m, NFData a) => SExecutable m (SymbolicT m a) where
   sName :: SymbolicT m a -> SymbolicT m ()
sName SymbolicT m a
a = SymbolicT m a
a SymbolicT m a -> (a -> SymbolicT m ()) -> SymbolicT m ()
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
r -> a -> ()
forall a. NFData a => a -> ()
rnf a
r () -> SymbolicT m () -> SymbolicT m ()
forall a b. a -> b -> b
`seq` () -> SymbolicT m ()
forall a. a -> SymbolicT m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

instance ExtractIO m => SExecutable m (SBV a) where
   sName :: SBV a -> SymbolicT m ()
sName SBV a
v = SymbolicT m (SBV a) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName (SBV a -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV 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
forall (m :: * -> *). MonadSymbolic m => () -> m ()
output () :: SymbolicT m ())

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

-- 2 Tuple output
instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b) => SExecutable m (SBV a, SBV b) where
  sName :: (SBV a, SBV b) -> SymbolicT m ()
sName (SBV a
a, SBV b
b) = SymbolicT m (SBV b) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName (SBV a -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV a)
output SBV a
a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV b)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m 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
forall (m :: * -> *). MonadSymbolic m => SBV b -> m (SBV b)
output SBV b
b :: SymbolicT m (SBV b))

-- 3 Tuple output
instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c) => SExecutable m (SBV a, SBV b, SBV c) where
  sName :: (SBV a, SBV b, SBV c) -> SymbolicT m ()
sName (SBV a
a, SBV b
b, SBV c
c) = SymbolicT m (SBV c) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName (SBV a -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV a)
output SBV a
a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV b)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m 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
forall (m :: * -> *). MonadSymbolic m => SBV b -> m (SBV b)
output SBV b
b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
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
forall (m :: * -> *). MonadSymbolic m => SBV c -> m (SBV c)
output SBV c
c :: SymbolicT m (SBV c))

-- 4 Tuple output
instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c, NFData d, SymVal d) => SExecutable m (SBV a, SBV b, SBV c, SBV d) where
  sName :: (SBV a, SBV b, SBV c, SBV d) -> SymbolicT m ()
sName (SBV a
a, SBV b
b, SBV c
c, SBV d
d) = SymbolicT m (SBV d) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName (SBV a -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV a)
output SBV a
a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV b)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m 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
forall (m :: * -> *). MonadSymbolic m => SBV b -> m (SBV b)
output SBV b
b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
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
forall (m :: * -> *). MonadSymbolic m => SBV c -> m (SBV c)
output SBV c
c SymbolicT m (SBV c) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
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
forall (m :: * -> *). MonadSymbolic m => SBV c -> m (SBV c)
output SBV c
c SymbolicT m (SBV c) -> SymbolicT m (SBV d) -> SymbolicT m (SBV d)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
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
forall (m :: * -> *). MonadSymbolic m => SBV d -> m (SBV d)
output SBV d
d :: SymbolicT m (SBV d))

-- 5 Tuple output
instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c, NFData d, SymVal d, NFData e, SymVal e) => SExecutable m (SBV a, SBV b, SBV c, SBV d, SBV e) where
  sName :: (SBV a, SBV b, SBV c, SBV d, SBV e) -> SymbolicT m ()
sName (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e) = SymbolicT m (SBV e) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName (SBV a -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV a)
output SBV a
a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV b)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m 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
forall (m :: * -> *). MonadSymbolic m => SBV b -> m (SBV b)
output SBV b
b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
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
forall (m :: * -> *). MonadSymbolic m => SBV c -> m (SBV c)
output SBV c
c SymbolicT m (SBV c) -> SymbolicT m (SBV d) -> SymbolicT m (SBV d)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
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
forall (m :: * -> *). MonadSymbolic m => SBV d -> m (SBV d)
output SBV d
d SymbolicT m (SBV d) -> SymbolicT m (SBV e) -> SymbolicT m (SBV e)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
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
forall (m :: * -> *). MonadSymbolic m => SBV e -> m (SBV e)
output SBV e
e :: SymbolicT m (SBV e))

-- 6 Tuple output
instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c, NFData d, SymVal d, NFData e, SymVal e, NFData f, SymVal f) => SExecutable m (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) where
  sName :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> SymbolicT m ()
sName (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f) = SymbolicT m (SBV f) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName (SBV a -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV a)
output SBV a
a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV b)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m 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
forall (m :: * -> *). MonadSymbolic m => SBV b -> m (SBV b)
output SBV b
b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
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
forall (m :: * -> *). MonadSymbolic m => SBV c -> m (SBV c)
output SBV c
c SymbolicT m (SBV c) -> SymbolicT m (SBV d) -> SymbolicT m (SBV d)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
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
forall (m :: * -> *). MonadSymbolic m => SBV d -> m (SBV d)
output SBV d
d SymbolicT m (SBV d) -> SymbolicT m (SBV e) -> SymbolicT m (SBV e)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
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
forall (m :: * -> *). MonadSymbolic m => SBV e -> m (SBV e)
output SBV e
e SymbolicT m (SBV e) -> SymbolicT m (SBV f) -> SymbolicT m (SBV f)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
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
forall (m :: * -> *). MonadSymbolic m => SBV f -> m (SBV f)
output SBV f
f :: SymbolicT m (SBV f))

-- 7 Tuple output
instance (ExtractIO m, NFData a, SymVal a, NFData b, SymVal b, NFData c, SymVal c, NFData d, SymVal d, NFData e, SymVal e, NFData f, SymVal f, NFData g, SymVal g) => SExecutable m (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) where
  sName :: (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> SymbolicT m ()
sName (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g) = SymbolicT m (SBV g) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName (SBV a -> SymbolicT m (SBV a)
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
forall (m :: * -> *). MonadSymbolic m => SBV a -> m (SBV a)
output SBV a
a SymbolicT m (SBV a) -> SymbolicT m (SBV b) -> SymbolicT m (SBV b)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m 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
forall (m :: * -> *). MonadSymbolic m => SBV b -> m (SBV b)
output SBV b
b SymbolicT m (SBV b) -> SymbolicT m (SBV c) -> SymbolicT m (SBV c)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
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
forall (m :: * -> *). MonadSymbolic m => SBV c -> m (SBV c)
output SBV c
c SymbolicT m (SBV c) -> SymbolicT m (SBV d) -> SymbolicT m (SBV d)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
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
forall (m :: * -> *). MonadSymbolic m => SBV d -> m (SBV d)
output SBV d
d SymbolicT m (SBV d) -> SymbolicT m (SBV e) -> SymbolicT m (SBV e)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
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
forall (m :: * -> *). MonadSymbolic m => SBV e -> m (SBV e)
output SBV e
e SymbolicT m (SBV e) -> SymbolicT m (SBV f) -> SymbolicT m (SBV f)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
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
forall (m :: * -> *). MonadSymbolic m => SBV f -> m (SBV f)
output SBV f
f SymbolicT m (SBV f) -> SymbolicT m (SBV g) -> SymbolicT m (SBV g)
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
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
forall (m :: * -> *). MonadSymbolic m => SBV g -> m (SBV g)
output SBV g
g :: SymbolicT m (SBV g))

-- Functions
instance (SymVal a, SExecutable m p) => SExecutable m (SBV a -> p) where
   sName :: (SBV a -> p) -> SymbolicT m ()
sName SBV a -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> p -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName (p -> SymbolicT m ()) -> p -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ SBV a -> p
k SBV a
a

-- 2 Tuple input
instance (SymVal a, SymVal b, SExecutable m p) => SExecutable m ((SBV a, SBV b) -> p) where
  sName :: ((SBV a, SBV b) -> p) -> SymbolicT m ()
sName (SBV a, SBV b) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> p) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName ((SBV b -> p) -> SymbolicT m ()) -> (SBV b -> p) -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \SBV b
b -> (SBV a, SBV b) -> p
k (SBV a
a, SBV b
b)

-- 3 Tuple input
instance (SymVal a, SymVal b, SymVal c, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c) -> p) where
  sName :: ((SBV a, SBV b, SBV c) -> p) -> SymbolicT m ()
sName (SBV a, SBV b, SBV c) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> p) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName ((SBV b -> SBV c -> p) -> SymbolicT m ())
-> (SBV b -> SBV c -> p) -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c -> (SBV a, SBV b, SBV c) -> p
k (SBV a
a, SBV b
b, SBV c
c)

-- 4 Tuple input
instance (SymVal a, SymVal b, SymVal c, SymVal d, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d) -> p) where
  sName :: ((SBV a, SBV b, SBV c, SBV d) -> p) -> SymbolicT m ()
sName (SBV a, SBV b, SBV c, SBV d) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName ((SBV b -> SBV c -> SBV d -> p) -> SymbolicT m ())
-> (SBV b -> SBV c -> SBV d -> p) -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d -> (SBV a, SBV b, SBV c, SBV d) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d)

-- 5 Tuple input
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) where
  sName :: ((SBV a, SBV b, SBV c, SBV d, SBV e) -> p) -> SymbolicT m ()
sName (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName ((SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m ())
-> (SBV b -> SBV c -> SBV d -> SBV e -> p) -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e -> (SBV a, SBV b, SBV c, SBV d, SBV e) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e)

-- 6 Tuple input
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) where
  sName :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p) -> SymbolicT m ()
sName (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p) -> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
 -> SymbolicT m ())
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> p)
-> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f)

-- 7 Tuple input
instance (SymVal a, SymVal b, SymVal c, SymVal d, SymVal e, SymVal f, SymVal g, SExecutable m p) => SExecutable m ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p) where
  sName :: ((SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p)
-> SymbolicT m ()
sName (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k = SymbolicT m (SBV a)
forall a (m :: * -> *). (SymVal a, MonadSymbolic m) => m (SBV a)
mkArg SymbolicT m (SBV a) -> (SBV a -> SymbolicT m ()) -> SymbolicT m ()
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SBV a
a -> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m ()
forall (m :: * -> *) a. SExecutable m a => a -> SymbolicT m ()
sName ((SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
 -> SymbolicT m ())
-> (SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> p)
-> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ \SBV b
b SBV c
c SBV d
d SBV e
e SBV f
f SBV g
g -> (SBV a, SBV b, SBV c, SBV d, SBV e, SBV f, SBV g) -> p
k (SBV a
a, SBV b
b, SBV c
c, SBV d
d, SBV e
e, SBV f
f, SBV g
g)

{- HLint ignore module "Reduce duplication" -}