-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.SMT.SMT
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Abstraction of SMT solvers
-----------------------------------------------------------------------------

{-# LANGUAGE DefaultSignatures          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NamedFieldPuns             #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE Rank2Types                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE ViewPatterns               #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.SMT.SMT (
       -- * Model extraction
         Modelable(..)
       , SatModel(..), genParse
       , extractModels, getModelValues
       , getModelDictionaries, getModelUninterpretedValues
       , displayModels, showModel, shCV, showModelDictionary

       -- * Standard prover engine
       , standardEngine

       -- * Results of various tasks
       , ThmResult(..)
       , SatResult(..)
       , AllSatResult(..)
       , SafeResult(..)
       , OptimizeResult(..)
       )
       where

import qualified Control.Exception as C

import Control.Concurrent (newEmptyMVar, takeMVar, putMVar, forkIO)
import Control.DeepSeq    (NFData(..))
import Control.Monad      (zipWithM)
import Data.Char          (isSpace)
import Data.Maybe         (fromMaybe, isJust)
import Data.Int           (Int8, Int16, Int32, Int64)
import Data.List          (intercalate, isPrefixOf, transpose, isInfixOf)
import Data.Word          (Word8, Word16, Word32, Word64)

import Data.IORef (readIORef, writeIORef)

import Data.Time          (getZonedTime, defaultTimeLocale, formatTime, diffUTCTime, getCurrentTime)

import System.Directory   (findExecutable)
import System.Environment (getEnv)
import System.Exit        (ExitCode(..))
import System.IO          (hClose, hFlush, hPutStrLn, hGetContents, hGetLine)
import System.Process     (runInteractiveProcess, waitForProcess, terminateProcess)

import qualified Data.Map.Strict as M
import qualified Data.Text       as T

import Data.SBV.Core.AlgReals
import Data.SBV.Core.Data
import Data.SBV.Core.Symbolic (SMTEngine, State(..))
import Data.SBV.Core.Concrete (showCV)
import Data.SBV.Core.Kind     (showBaseKind)

import Data.SBV.SMT.Utils     (showTimeoutValue, alignPlain, debug, mergeSExpr, SBVException(..))

import Data.SBV.Utils.PrettyNum
import Data.SBV.Utils.Lib       (joinArgs, splitArgs)
import Data.SBV.Utils.SExpr     (parenDeficit)
import Data.SBV.Utils.TDiff     (Timing(..), showTDiff)

import qualified System.Timeout as Timeout (timeout)

import Numeric

-- | Extract the final configuration from a result
resultConfig :: SMTResult -> SMTConfig
resultConfig :: SMTResult -> SMTConfig
resultConfig (Unsatisfiable SMTConfig
c Maybe [String]
_  ) = SMTConfig
c
resultConfig (Satisfiable   SMTConfig
c SMTModel
_  ) = SMTConfig
c
resultConfig (DeltaSat      SMTConfig
c Maybe String
_ SMTModel
_) = SMTConfig
c
resultConfig (SatExtField   SMTConfig
c SMTModel
_  ) = SMTConfig
c
resultConfig (Unknown       SMTConfig
c SMTReasonUnknown
_  ) = SMTConfig
c
resultConfig (ProofError    SMTConfig
c [String]
_ Maybe SMTResult
_) = SMTConfig
c

-- | A 'Data.SBV.prove' call results in a 'ThmResult'
newtype ThmResult = ThmResult SMTResult
                  deriving ThmResult -> ()
(ThmResult -> ()) -> NFData ThmResult
forall a. (a -> ()) -> NFData a
rnf :: ThmResult -> ()
$crnf :: ThmResult -> ()
NFData

-- | A 'Data.SBV.sat' call results in a 'SatResult'
-- The reason for having a separate 'SatResult' is to have a more meaningful 'Show' instance.
newtype SatResult = SatResult SMTResult
                  deriving SatResult -> ()
(SatResult -> ()) -> NFData SatResult
forall a. (a -> ()) -> NFData a
rnf :: SatResult -> ()
$crnf :: SatResult -> ()
NFData

-- | An 'Data.SBV.allSat' call results in a 'AllSatResult'
data AllSatResult = AllSatResult { AllSatResult -> Bool
allSatMaxModelCountReached  :: Bool          -- ^ Did we reach the user given model count limit?
                                 , AllSatResult -> Bool
allSatHasPrefixExistentials :: Bool          -- ^ Were there quantifiers in the problem (unique upto prefix existentials)
                                 , AllSatResult -> Bool
allSatSolverReturnedUnknown :: Bool          -- ^ Did the solver report unknown at the end?
                                 , AllSatResult -> Bool
allSatSolverReturnedDSat    :: Bool          -- ^ Did the solver report delta-satisfiable at the end?
                                 , AllSatResult -> [SMTResult]
allSatResults               :: [SMTResult]   -- ^ All satisfying models
                                 }

-- | A 'Data.SBV.safe' call results in a 'SafeResult'
newtype SafeResult   = SafeResult   (Maybe String, String, SMTResult)

-- | An 'Data.SBV.optimize' call results in a 'OptimizeResult'. In the 'ParetoResult' case, the boolean is 'True'
-- if we reached pareto-query limit and so there might be more unqueried results remaining. If 'False',
-- it means that we have all the pareto fronts returned. See the 'Pareto' 'OptimizeStyle' for details.
data OptimizeResult = LexicographicResult SMTResult
                    | ParetoResult        (Bool, [SMTResult])
                    | IndependentResult   [(String, SMTResult)]

-- | What's the precision of a delta-sat query?
getPrecision :: SMTResult -> Maybe String -> String
getPrecision :: SMTResult -> Maybe String -> String
getPrecision SMTResult
r Maybe String
queriedPrecision = case (Maybe String
queriedPrecision, SMTConfig -> Maybe Double
dsatPrecision (SMTResult -> SMTConfig
resultConfig SMTResult
r)) of
                                   (Just String
s, Maybe Double
_     ) -> String
s
                                   (Maybe String
_,      Just Double
d) -> Maybe Int -> Double -> ShowS
forall a. RealFloat a => Maybe Int -> a -> ShowS
showFFloat Maybe Int
forall a. Maybe a
Nothing Double
d String
""
                                   (Maybe String, Maybe Double)
_                -> String
"tool default"

-- User friendly way of printing theorem results
instance Show ThmResult where
  show :: ThmResult -> String
show (ThmResult SMTResult
r) = String
-> String
-> String
-> String
-> (Maybe String -> String)
-> String
-> SMTResult
-> String
showSMTResult String
"Q.E.D."
                                     String
"Unknown"
                                     String
"Falsifiable"
                                     String
"Falsifiable. Counter-example:\n"
                                     (\Maybe String
mbP -> String
"Delta falsifiable, precision: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SMTResult -> Maybe String -> String
getPrecision SMTResult
r Maybe String
mbP String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
". Counter-example:\n")
                                     String
"Falsifiable in an extension field:\n"
                                     SMTResult
r

-- User friendly way of printing satisfiablity results
instance Show SatResult where
  show :: SatResult -> String
show (SatResult SMTResult
r) = String
-> String
-> String
-> String
-> (Maybe String -> String)
-> String
-> SMTResult
-> String
showSMTResult String
"Unsatisfiable"
                                     String
"Unknown"
                                     String
"Satisfiable"
                                     String
"Satisfiable. Model:\n"
                                     (\Maybe String
mbP -> String
"Delta satisfiable, precision: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SMTResult -> Maybe String -> String
getPrecision SMTResult
r Maybe String
mbP String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
". Model:\n")
                                     String
"Satisfiable in an extension field. Model:\n"
                                     SMTResult
r

-- User friendly way of printing safety results
instance Show SafeResult where
   show :: SafeResult -> String
show (SafeResult (Maybe String
mbLoc, String
msg, SMTResult
r)) = String
-> String
-> String
-> String
-> (Maybe String -> String)
-> String
-> SMTResult
-> String
showSMTResult (ShowS
tag String
"No violations detected")
                                                     (ShowS
tag String
"Unknown")
                                                     (ShowS
tag String
"Violated")
                                                     (ShowS
tag String
"Violated. Model:\n")
                                                     (\Maybe String
mbP -> ShowS
tag String
"Violated in a delta-satisfiable context, precision: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SMTResult -> Maybe String -> String
getPrecision SMTResult
r Maybe String
mbP String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
". Model:\n")
                                                     (ShowS
tag String
"Violated in an extension field:\n")
                                                     SMTResult
r
        where loc :: String
loc   = String -> ShowS -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": ") Maybe String
mbLoc
              tag :: ShowS
tag String
s = String
loc String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
msg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s

-- The Show instance of AllSatResults.
instance Show AllSatResult where
  show :: AllSatResult -> String
show AllSatResult { allSatMaxModelCountReached :: AllSatResult -> Bool
allSatMaxModelCountReached  = Bool
l
                    , allSatHasPrefixExistentials :: AllSatResult -> Bool
allSatHasPrefixExistentials = Bool
e
                    , allSatSolverReturnedUnknown :: AllSatResult -> Bool
allSatSolverReturnedUnknown = Bool
u
                    , allSatSolverReturnedDSat :: AllSatResult -> Bool
allSatSolverReturnedDSat    = Bool
d
                    , allSatResults :: AllSatResult -> [SMTResult]
allSatResults               = [SMTResult]
xs
                    } = Int -> [SMTResult] -> String
forall t. (Eq t, Num t, Show t) => t -> [SMTResult] -> String
go (Int
0::Int) [SMTResult]
xs
    where warnings :: String
warnings = case (Bool
e, Bool
u) of
                       (Bool
False, Bool
False) -> String
""
                       (Bool
False, Bool
True)  -> String
" (Search stopped since solver has returned unknown.)"
                       (Bool
True,  Bool
False) -> String
" (Unique up to prefix existentials.)"
                       (Bool
True,  Bool
True)  -> String
" (Search stopped becase solver has returned unknown, only prefix existentials were considered.)"

          go :: t -> [SMTResult] -> String
go t
c (SMTResult
s:[SMTResult]
ss) = let c' :: t
c'      = t
ct -> t -> t
forall a. Num a => a -> a -> a
+t
1
                            (Bool
ok, String
o) = t -> SMTResult -> (Bool, String)
forall a. Show a => a -> SMTResult -> (Bool, String)
sh t
c' SMTResult
s
                        in t
c' t -> ShowS
`seq` if Bool
ok then String
o String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> [SMTResult] -> String
go t
c' [SMTResult]
ss else String
o
          go t
c []     = case (Bool
l, Bool
d, t
c) of
                          (Bool
True,  Bool
_   , t
_) -> String
"Search stopped since model count request was reached."  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
warnings
                          (Bool
_   ,  Bool
True, t
_) -> String
"Search stopped since the result was delta-satisfiable." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
warnings
                          (Bool
False, Bool
_   , t
0) -> String
"No solutions found."
                          (Bool
False, Bool
_   , t
1) -> String
"This is the only solution." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
warnings
                          (Bool
False, Bool
_   , t
_) -> String
"Found " String -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
c String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" different solutions." String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
warnings

          sh :: a -> SMTResult -> (Bool, String)
sh a
i SMTResult
c = (Bool
ok, String
-> String
-> String
-> String
-> (Maybe String -> String)
-> String
-> SMTResult
-> String
showSMTResult String
"Unsatisfiable"
                                      String
"Unknown"
                                      (String
"Solution #" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":\nSatisfiable") (String
"Solution #" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":\n")
                                      (\Maybe String
mbP -> String
"Solution $" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" with delta-satisfiability, precision: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SMTResult -> Maybe String -> String
getPrecision SMTResult
c Maybe String
mbP String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":\n")
                                      (String
"Solution $" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" in an extension field:\n")
                                      SMTResult
c)
              where ok :: Bool
ok = case SMTResult
c of
                           Satisfiable{} -> Bool
True
                           SMTResult
_             -> Bool
False

-- Show instance for optimization results
instance Show OptimizeResult where
  show :: OptimizeResult -> String
show OptimizeResult
res = case OptimizeResult
res of
               LexicographicResult SMTResult
r   -> ShowS -> SMTResult -> String
forall t. IsString t => (t -> String) -> SMTResult -> String
sh ShowS
forall a. a -> a
id SMTResult
r

               IndependentResult   [(String, SMTResult)]
rs  -> String -> [String] -> String
multi String
"objectives" (((String, SMTResult) -> String)
-> [(String, SMTResult)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> SMTResult -> String) -> (String, SMTResult) -> String
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String -> SMTResult -> String
forall a. Show a => a -> SMTResult -> String
shI) [(String, SMTResult)]
rs)

               ParetoResult (Bool
False, [SMTResult
r]) -> ShowS -> SMTResult -> String
forall t. IsString t => (t -> String) -> SMTResult -> String
sh (String
"Unique pareto front: " String -> ShowS
forall a. [a] -> [a] -> [a]
++) SMTResult
r
               ParetoResult (Bool
False, [SMTResult]
rs)  -> String -> [String] -> String
multi String
"pareto optimal values" ((Int -> SMTResult -> String) -> [Int] -> [SMTResult] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> SMTResult -> String
forall a. Show a => a -> SMTResult -> String
shP [(Int
1::Int)..] [SMTResult]
rs)
               ParetoResult (Bool
True,  [SMTResult]
rs)  ->    String -> [String] -> String
multi String
"pareto optimal values" ((Int -> SMTResult -> String) -> [Int] -> [SMTResult] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> SMTResult -> String
forall a. Show a => a -> SMTResult -> String
shP [(Int
1::Int)..] [SMTResult]
rs)
                                           String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n*** Note: Pareto-front extraction was terminated as requested by the user."
                                           String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n***       There might be many other results!"

       where multi :: String -> [String] -> String
multi String
w [] = String
"There are no " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
w String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" to display models for."
             multi String
_ [String]
xs = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String]
xs

             shI :: a -> SMTResult -> String
shI a
n = ShowS -> SMTResult -> String
forall t. IsString t => (t -> String) -> SMTResult -> String
sh (\String
s -> String
"Objective "     String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s)
             shP :: a -> SMTResult -> String
shP a
i = ShowS -> SMTResult -> String
forall t. IsString t => (t -> String) -> SMTResult -> String
sh (\String
s -> String
"Pareto front #" String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
": " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s)

             sh :: (t -> String) -> SMTResult -> String
sh t -> String
tag SMTResult
r = String
-> String
-> String
-> String
-> (Maybe String -> String)
-> String
-> SMTResult
-> String
showSMTResult (t -> String
tag t
"Unsatisfiable.")
                                      (t -> String
tag t
"Unknown.")
                                      (t -> String
tag t
"Optimal with no assignments.")
                                      (t -> String
tag t
"Optimal model:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n")
                                      (\Maybe String
mbP -> t -> String
tag t
"Optimal model with delta-satisfiability, precision: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SMTResult -> Maybe String -> String
getPrecision SMTResult
r Maybe String
mbP String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
":" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n")
                                      (t -> String
tag t
"Optimal in an extension field:" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n")
                                      SMTResult
r

-- | Instances of 'SatModel' can be automatically extracted from models returned by the
-- solvers. The idea is that the sbv infrastructure provides a stream of CV's (constant values)
-- coming from the solver, and the type @a@ is interpreted based on these constants. Many typical
-- instances are already provided, so new instances can be declared with relative ease.
--
-- Minimum complete definition: 'parseCVs'
class SatModel a where
  -- | Given a sequence of constant-words, extract one instance of the type @a@, returning
  -- the remaining elements untouched. If the next element is not what's expected for this
  -- type you should return 'Nothing'
  parseCVs  :: [CV] -> Maybe (a, [CV])
  -- | Given a parsed model instance, transform it using @f@, and return the result.
  -- The default definition for this method should be sufficient in most use cases.
  cvtModel  :: (a -> Maybe b) -> Maybe (a, [CV]) -> Maybe (b, [CV])
  cvtModel a -> Maybe b
f Maybe (a, [CV])
x = Maybe (a, [CV])
x Maybe (a, [CV])
-> ((a, [CV]) -> Maybe (b, [CV])) -> Maybe (b, [CV])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(a
a, [CV]
r) -> a -> Maybe b
f a
a Maybe b -> (b -> Maybe (b, [CV])) -> Maybe (b, [CV])
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b
b -> (b, [CV]) -> Maybe (b, [CV])
forall (m :: * -> *) a. Monad m => a -> m a
return (b
b, [CV]
r)

  default parseCVs :: Read a => [CV] -> Maybe (a, [CV])
  parseCVs (CV Kind
_ (CUserSort (Maybe Int
_, String
s)) : [CV]
r) = (a, [CV]) -> Maybe (a, [CV])
forall a. a -> Maybe a
Just (String -> a
forall a. Read a => String -> a
read String
s, [CV]
r)
  parseCVs [CV]
_                             = Maybe (a, [CV])
forall a. Maybe a
Nothing

-- | Parse a signed/sized value from a sequence of CVs
genParse :: Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse :: Kind -> [CV] -> Maybe (a, [CV])
genParse Kind
k (x :: CV
x@(CV Kind
_ (CInteger Integer
i)):[CV]
r) | CV -> Kind
forall a. HasKind a => a -> Kind
kindOf CV
x Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
k = (a, [CV]) -> Maybe (a, [CV])
forall a. a -> Maybe a
Just (Integer -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i, [CV]
r)
genParse Kind
_ [CV]
_                                         = Maybe (a, [CV])
forall a. Maybe a
Nothing

-- | Base case for 'SatModel' at unit type. Comes in handy if there are no real variables.
instance SatModel () where
  parseCVs :: [CV] -> Maybe ((), [CV])
parseCVs [CV]
xs = ((), [CV]) -> Maybe ((), [CV])
forall (m :: * -> *) a. Monad m => a -> m a
return ((), [CV]
xs)

-- | 'Bool' as extracted from a model
instance SatModel Bool where
  parseCVs :: [CV] -> Maybe (Bool, [CV])
parseCVs [CV]
xs = do (Integer
x, [CV]
r) <- Kind -> [CV] -> Maybe (Integer, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse Kind
KBool [CV]
xs
                   (Bool, [CV]) -> Maybe (Bool, [CV])
forall (m :: * -> *) a. Monad m => a -> m a
return ((Integer
x :: Integer) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0, [CV]
r)

-- | 'Word8' as extracted from a model
instance SatModel Word8 where
  parseCVs :: [CV] -> Maybe (Word8, [CV])
parseCVs = Kind -> [CV] -> Maybe (Word8, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (Bool -> Int -> Kind
KBounded Bool
False Int
8)

-- | 'Int8' as extracted from a model
instance SatModel Int8 where
  parseCVs :: [CV] -> Maybe (Int8, [CV])
parseCVs = Kind -> [CV] -> Maybe (Int8, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (Bool -> Int -> Kind
KBounded Bool
True Int
8)

-- | 'Word16' as extracted from a model
instance SatModel Word16 where
  parseCVs :: [CV] -> Maybe (Word16, [CV])
parseCVs = Kind -> [CV] -> Maybe (Word16, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (Bool -> Int -> Kind
KBounded Bool
False Int
16)

-- | 'Int16' as extracted from a model
instance SatModel Int16 where
  parseCVs :: [CV] -> Maybe (Int16, [CV])
parseCVs = Kind -> [CV] -> Maybe (Int16, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (Bool -> Int -> Kind
KBounded Bool
True Int
16)

-- | 'Word32' as extracted from a model
instance SatModel Word32 where
  parseCVs :: [CV] -> Maybe (Word32, [CV])
parseCVs = Kind -> [CV] -> Maybe (Word32, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (Bool -> Int -> Kind
KBounded Bool
False Int
32)

-- | 'Int32' as extracted from a model
instance SatModel Int32 where
  parseCVs :: [CV] -> Maybe (Int32, [CV])
parseCVs = Kind -> [CV] -> Maybe (Int32, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (Bool -> Int -> Kind
KBounded Bool
True Int
32)

-- | 'Word64' as extracted from a model
instance SatModel Word64 where
  parseCVs :: [CV] -> Maybe (Word64, [CV])
parseCVs = Kind -> [CV] -> Maybe (Word64, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (Bool -> Int -> Kind
KBounded Bool
False Int
64)

-- | 'Int64' as extracted from a model
instance SatModel Int64 where
  parseCVs :: [CV] -> Maybe (Int64, [CV])
parseCVs = Kind -> [CV] -> Maybe (Int64, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (Bool -> Int -> Kind
KBounded Bool
True Int
64)

-- | 'Integer' as extracted from a model
instance SatModel Integer where
  parseCVs :: [CV] -> Maybe (Integer, [CV])
parseCVs = Kind -> [CV] -> Maybe (Integer, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse Kind
KUnbounded

-- | 'AlgReal' as extracted from a model
instance SatModel AlgReal where
  parseCVs :: [CV] -> Maybe (AlgReal, [CV])
parseCVs (CV Kind
KReal (CAlgReal AlgReal
i) : [CV]
r) = (AlgReal, [CV]) -> Maybe (AlgReal, [CV])
forall a. a -> Maybe a
Just (AlgReal
i, [CV]
r)
  parseCVs [CV]
_                           = Maybe (AlgReal, [CV])
forall a. Maybe a
Nothing

-- | 'Float' as extracted from a model
instance SatModel Float where
  parseCVs :: [CV] -> Maybe (Float, [CV])
parseCVs (CV Kind
KFloat (CFloat Float
i) : [CV]
r) = (Float, [CV]) -> Maybe (Float, [CV])
forall a. a -> Maybe a
Just (Float
i, [CV]
r)
  parseCVs [CV]
_                          = Maybe (Float, [CV])
forall a. Maybe a
Nothing

-- | 'Double' as extracted from a model
instance SatModel Double where
  parseCVs :: [CV] -> Maybe (Double, [CV])
parseCVs (CV Kind
KDouble (CDouble Double
i) : [CV]
r) = (Double, [CV]) -> Maybe (Double, [CV])
forall a. a -> Maybe a
Just (Double
i, [CV]
r)
  parseCVs [CV]
_                            = Maybe (Double, [CV])
forall a. Maybe a
Nothing

-- | @CV@ as extracted from a model; trivial definition
instance SatModel CV where
  parseCVs :: [CV] -> Maybe (CV, [CV])
parseCVs (CV
cv : [CV]
r) = (CV, [CV]) -> Maybe (CV, [CV])
forall a. a -> Maybe a
Just (CV
cv, [CV]
r)
  parseCVs []       = Maybe (CV, [CV])
forall a. Maybe a
Nothing

-- | A rounding mode, extracted from a model. (Default definition suffices)
instance SatModel RoundingMode

-- | A list of values as extracted from a model. When reading a list, we
-- go as long as we can (maximal-munch). Note that this never fails, as
-- we can always return the empty list!
instance SatModel a => SatModel [a] where
  parseCVs :: [CV] -> Maybe ([a], [CV])
parseCVs [] = ([a], [CV]) -> Maybe ([a], [CV])
forall a. a -> Maybe a
Just ([], [])
  parseCVs [CV]
xs = case [CV] -> Maybe (a, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
xs of
                  Just (a
a, [CV]
ys) -> case [CV] -> Maybe ([a], [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
ys of
                                    Just ([a]
as, [CV]
zs) -> ([a], [CV]) -> Maybe ([a], [CV])
forall a. a -> Maybe a
Just (a
aa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
as, [CV]
zs)
                                    Maybe ([a], [CV])
Nothing       -> ([a], [CV]) -> Maybe ([a], [CV])
forall a. a -> Maybe a
Just ([], [CV]
ys)
                  Maybe (a, [CV])
Nothing     -> ([a], [CV]) -> Maybe ([a], [CV])
forall a. a -> Maybe a
Just ([], [CV]
xs)

-- | Tuples extracted from a model
instance (SatModel a, SatModel b) => SatModel (a, b) where
  parseCVs :: [CV] -> Maybe ((a, b), [CV])
parseCVs [CV]
as = do (a
a, [CV]
bs) <- [CV] -> Maybe (a, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
as
                   (b
b, [CV]
cs) <- [CV] -> Maybe (b, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
bs
                   ((a, b), [CV]) -> Maybe ((a, b), [CV])
forall (m :: * -> *) a. Monad m => a -> m a
return ((a
a, b
b), [CV]
cs)

-- | 3-Tuples extracted from a model
instance (SatModel a, SatModel b, SatModel c) => SatModel (a, b, c) where
  parseCVs :: [CV] -> Maybe ((a, b, c), [CV])
parseCVs [CV]
as = do (a
a,      [CV]
bs) <- [CV] -> Maybe (a, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
as
                   ((b
b, c
c), [CV]
ds) <- [CV] -> Maybe ((b, c), [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
bs
                   ((a, b, c), [CV]) -> Maybe ((a, b, c), [CV])
forall (m :: * -> *) a. Monad m => a -> m a
return ((a
a, b
b, c
c), [CV]
ds)

-- | 4-Tuples extracted from a model
instance (SatModel a, SatModel b, SatModel c, SatModel d) => SatModel (a, b, c, d) where
  parseCVs :: [CV] -> Maybe ((a, b, c, d), [CV])
parseCVs [CV]
as = do (a
a,         [CV]
bs) <- [CV] -> Maybe (a, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
as
                   ((b
b, c
c, d
d), [CV]
es) <- [CV] -> Maybe ((b, c, d), [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
bs
                   ((a, b, c, d), [CV]) -> Maybe ((a, b, c, d), [CV])
forall (m :: * -> *) a. Monad m => a -> m a
return ((a
a, b
b, c
c, d
d), [CV]
es)

-- | 5-Tuples extracted from a model
instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e) => SatModel (a, b, c, d, e) where
  parseCVs :: [CV] -> Maybe ((a, b, c, d, e), [CV])
parseCVs [CV]
as = do (a
a, [CV]
bs)            <- [CV] -> Maybe (a, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
as
                   ((b
b, c
c, d
d, e
e), [CV]
fs) <- [CV] -> Maybe ((b, c, d, e), [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
bs
                   ((a, b, c, d, e), [CV]) -> Maybe ((a, b, c, d, e), [CV])
forall (m :: * -> *) a. Monad m => a -> m a
return ((a
a, b
b, c
c, d
d, e
e), [CV]
fs)

-- | 6-Tuples extracted from a model
instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f) => SatModel (a, b, c, d, e, f) where
  parseCVs :: [CV] -> Maybe ((a, b, c, d, e, f), [CV])
parseCVs [CV]
as = do (a
a, [CV]
bs)               <- [CV] -> Maybe (a, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
as
                   ((b
b, c
c, d
d, e
e, f
f), [CV]
gs) <- [CV] -> Maybe ((b, c, d, e, f), [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
bs
                   ((a, b, c, d, e, f), [CV]) -> Maybe ((a, b, c, d, e, f), [CV])
forall (m :: * -> *) a. Monad m => a -> m a
return ((a
a, b
b, c
c, d
d, e
e, f
f), [CV]
gs)

-- | 7-Tuples extracted from a model
instance (SatModel a, SatModel b, SatModel c, SatModel d, SatModel e, SatModel f, SatModel g) => SatModel (a, b, c, d, e, f, g) where
  parseCVs :: [CV] -> Maybe ((a, b, c, d, e, f, g), [CV])
parseCVs [CV]
as = do (a
a, [CV]
bs)                  <- [CV] -> Maybe (a, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
as
                   ((b
b, c
c, d
d, e
e, f
f, g
g), [CV]
hs) <- [CV] -> Maybe ((b, c, d, e, f, g), [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
bs
                   ((a, b, c, d, e, f, g), [CV])
-> Maybe ((a, b, c, d, e, f, g), [CV])
forall (m :: * -> *) a. Monad m => a -> m a
return ((a
a, b
b, c
c, d
d, e
e, f
f, g
g), [CV]
hs)

-- | Various SMT results that we can extract models out of.
class Modelable a where
  -- | Is there a model?
  modelExists :: a -> Bool

  -- | Extract assignments of a model, the result is a tuple where the first argument (if True)
  -- indicates whether the model was "probable". (i.e., if the solver returned unknown.)
  getModelAssignment :: SatModel b => a -> Either String (Bool, b)

  -- | Extract a model dictionary. Extract a dictionary mapping the variables to
  -- their respective values as returned by the SMT solver. Also see `getModelDictionaries`.
  getModelDictionary :: a -> M.Map String CV

  -- | Extract a model value for a given element. Also see `getModelValues`.
  getModelValue :: SymVal b => String -> a -> Maybe b
  getModelValue String
v a
r = CV -> b
forall a. SymVal a => CV -> a
fromCV (CV -> b) -> Maybe CV -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` (String
v String -> Map String CV -> Maybe CV
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` a -> Map String CV
forall a. Modelable a => a -> Map String CV
getModelDictionary a
r)

  -- | Extract a representative name for the model value of an uninterpreted kind.
  -- This is supposed to correspond to the value as computed internally by the
  -- SMT solver; and is unportable from solver to solver. Also see `getModelUninterpretedValues`.
  getModelUninterpretedValue :: String -> a -> Maybe String
  getModelUninterpretedValue String
v a
r = case String
v String -> Map String CV -> Maybe CV
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` a -> Map String CV
forall a. Modelable a => a -> Map String CV
getModelDictionary a
r of
                                     Just (CV Kind
_ (CUserSort (Maybe Int
_, String
s))) -> String -> Maybe String
forall a. a -> Maybe a
Just String
s
                                     Maybe CV
_                              -> Maybe String
forall a. Maybe a
Nothing

  -- | A simpler variant of 'getModelAssignment' to get a model out without the fuss.
  extractModel :: SatModel b => a -> Maybe b
  extractModel a
a = case a -> Either String (Bool, b)
forall a b.
(Modelable a, SatModel b) =>
a -> Either String (Bool, b)
getModelAssignment a
a of
                     Right (Bool
_, b
b) -> b -> Maybe b
forall a. a -> Maybe a
Just b
b
                     Either String (Bool, b)
_            -> Maybe b
forall a. Maybe a
Nothing

  -- | Extract model objective values, for all optimization goals.
  getModelObjectives :: a -> M.Map String GeneralizedCV

  -- | Extract the value of an objective
  getModelObjectiveValue :: String -> a -> Maybe GeneralizedCV
  getModelObjectiveValue String
v a
r = String
v String -> Map String GeneralizedCV -> Maybe GeneralizedCV
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` a -> Map String GeneralizedCV
forall a. Modelable a => a -> Map String GeneralizedCV
getModelObjectives a
r

  -- | Extract model uninterpreted-functions
  getModelUIFuns :: a -> M.Map String (SBVType, ([([CV], CV)], CV))

  -- | Extract the value of an uninterpreted-function as an association list
  getModelUIFunValue :: String -> a -> Maybe (SBVType, ([([CV], CV)], CV))
  getModelUIFunValue String
v a
r = String
v String
-> Map String (SBVType, ([([CV], CV)], CV))
-> Maybe (SBVType, ([([CV], CV)], CV))
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` a -> Map String (SBVType, ([([CV], CV)], CV))
forall a.
Modelable a =>
a -> Map String (SBVType, ([([CV], CV)], CV))
getModelUIFuns a
r

-- | Return all the models from an 'Data.SBV.allSat' call, similar to 'extractModel' but
-- is suitable for the case of multiple results.
extractModels :: SatModel a => AllSatResult -> [a]
extractModels :: AllSatResult -> [a]
extractModels AllSatResult{allSatResults :: AllSatResult -> [SMTResult]
allSatResults = [SMTResult]
xs} = [a
ms | Right (Bool
_, a
ms) <- (SMTResult -> Either String (Bool, a))
-> [SMTResult] -> [Either String (Bool, a)]
forall a b. (a -> b) -> [a] -> [b]
map SMTResult -> Either String (Bool, a)
forall a b.
(Modelable a, SatModel b) =>
a -> Either String (Bool, b)
getModelAssignment [SMTResult]
xs]

-- | Get dictionaries from an all-sat call. Similar to `getModelDictionary`.
getModelDictionaries :: AllSatResult -> [M.Map String CV]
getModelDictionaries :: AllSatResult -> [Map String CV]
getModelDictionaries AllSatResult{allSatResults :: AllSatResult -> [SMTResult]
allSatResults = [SMTResult]
xs} = (SMTResult -> Map String CV) -> [SMTResult] -> [Map String CV]
forall a b. (a -> b) -> [a] -> [b]
map SMTResult -> Map String CV
forall a. Modelable a => a -> Map String CV
getModelDictionary [SMTResult]
xs

-- | Extract value of a variable from an all-sat call. Similar to `getModelValue`.
getModelValues :: SymVal b => String -> AllSatResult -> [Maybe b]
getModelValues :: String -> AllSatResult -> [Maybe b]
getModelValues String
s AllSatResult{allSatResults :: AllSatResult -> [SMTResult]
allSatResults = [SMTResult]
xs} =  (SMTResult -> Maybe b) -> [SMTResult] -> [Maybe b]
forall a b. (a -> b) -> [a] -> [b]
map (String
s String -> SMTResult -> Maybe b
forall a b. (Modelable a, SymVal b) => String -> a -> Maybe b
`getModelValue`) [SMTResult]
xs

-- | Extract value of an uninterpreted variable from an all-sat call. Similar to `getModelUninterpretedValue`.
getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String]
getModelUninterpretedValues :: String -> AllSatResult -> [Maybe String]
getModelUninterpretedValues String
s AllSatResult{allSatResults :: AllSatResult -> [SMTResult]
allSatResults = [SMTResult]
xs} =  (SMTResult -> Maybe String) -> [SMTResult] -> [Maybe String]
forall a b. (a -> b) -> [a] -> [b]
map (String
s String -> SMTResult -> Maybe String
forall a. Modelable a => String -> a -> Maybe String
`getModelUninterpretedValue`) [SMTResult]
xs

-- | 'ThmResult' as a generic model provider
instance Modelable ThmResult where
  getModelAssignment :: ThmResult -> Either String (Bool, b)
getModelAssignment (ThmResult SMTResult
r) = SMTResult -> Either String (Bool, b)
forall a b.
(Modelable a, SatModel b) =>
a -> Either String (Bool, b)
getModelAssignment SMTResult
r
  modelExists :: ThmResult -> Bool
modelExists        (ThmResult SMTResult
r) = SMTResult -> Bool
forall a. Modelable a => a -> Bool
modelExists        SMTResult
r
  getModelDictionary :: ThmResult -> Map String CV
getModelDictionary (ThmResult SMTResult
r) = SMTResult -> Map String CV
forall a. Modelable a => a -> Map String CV
getModelDictionary SMTResult
r
  getModelObjectives :: ThmResult -> Map String GeneralizedCV
getModelObjectives (ThmResult SMTResult
r) = SMTResult -> Map String GeneralizedCV
forall a. Modelable a => a -> Map String GeneralizedCV
getModelObjectives SMTResult
r
  getModelUIFuns :: ThmResult -> Map String (SBVType, ([([CV], CV)], CV))
getModelUIFuns     (ThmResult SMTResult
r) = SMTResult -> Map String (SBVType, ([([CV], CV)], CV))
forall a.
Modelable a =>
a -> Map String (SBVType, ([([CV], CV)], CV))
getModelUIFuns     SMTResult
r

-- | 'SatResult' as a generic model provider
instance Modelable SatResult where
  getModelAssignment :: SatResult -> Either String (Bool, b)
getModelAssignment (SatResult SMTResult
r) = SMTResult -> Either String (Bool, b)
forall a b.
(Modelable a, SatModel b) =>
a -> Either String (Bool, b)
getModelAssignment SMTResult
r
  modelExists :: SatResult -> Bool
modelExists        (SatResult SMTResult
r) = SMTResult -> Bool
forall a. Modelable a => a -> Bool
modelExists        SMTResult
r
  getModelDictionary :: SatResult -> Map String CV
getModelDictionary (SatResult SMTResult
r) = SMTResult -> Map String CV
forall a. Modelable a => a -> Map String CV
getModelDictionary SMTResult
r
  getModelObjectives :: SatResult -> Map String GeneralizedCV
getModelObjectives (SatResult SMTResult
r) = SMTResult -> Map String GeneralizedCV
forall a. Modelable a => a -> Map String GeneralizedCV
getModelObjectives SMTResult
r
  getModelUIFuns :: SatResult -> Map String (SBVType, ([([CV], CV)], CV))
getModelUIFuns     (SatResult SMTResult
r) = SMTResult -> Map String (SBVType, ([([CV], CV)], CV))
forall a.
Modelable a =>
a -> Map String (SBVType, ([([CV], CV)], CV))
getModelUIFuns     SMTResult
r

-- | 'SMTResult' as a generic model provider
instance Modelable SMTResult where
  getModelAssignment :: SMTResult -> Either String (Bool, b)
getModelAssignment (Unsatisfiable SMTConfig
_ Maybe [String]
_  ) = String -> Either String (Bool, b)
forall a b. a -> Either a b
Left String
"SBV.getModelAssignment: Unsatisfiable result"
  getModelAssignment (Satisfiable   SMTConfig
_   SMTModel
m) = (Bool, b) -> Either String (Bool, b)
forall a b. b -> Either a b
Right (Bool
False, SMTModel -> b
forall a. SatModel a => SMTModel -> a
parseModelOut SMTModel
m)
  getModelAssignment (DeltaSat      SMTConfig
_ Maybe String
_ SMTModel
m) = (Bool, b) -> Either String (Bool, b)
forall a b. b -> Either a b
Right (Bool
False, SMTModel -> b
forall a. SatModel a => SMTModel -> a
parseModelOut SMTModel
m)
  getModelAssignment (SatExtField   SMTConfig
_ SMTModel
_  ) = String -> Either String (Bool, b)
forall a b. a -> Either a b
Left String
"SBV.getModelAssignment: The model is in an extension field"
  getModelAssignment (Unknown       SMTConfig
_ SMTReasonUnknown
m  ) = String -> Either String (Bool, b)
forall a b. a -> Either a b
Left (String -> Either String (Bool, b))
-> String -> Either String (Bool, b)
forall a b. (a -> b) -> a -> b
$ String
"SBV.getModelAssignment: Solver state is unknown: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SMTReasonUnknown -> String
forall a. Show a => a -> String
show SMTReasonUnknown
m
  getModelAssignment (ProofError    SMTConfig
_ [String]
s Maybe SMTResult
_) = String -> Either String (Bool, b)
forall a. HasCallStack => String -> a
error (String -> Either String (Bool, b))
-> String -> Either String (Bool, b)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.getModelAssignment: Failed to produce a model: " String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
s

  modelExists :: SMTResult -> Bool
modelExists Satisfiable{}   = Bool
True
  modelExists Unknown{}       = Bool
False -- don't risk it
  modelExists SMTResult
_               = Bool
False

  getModelDictionary :: SMTResult -> Map String CV
getModelDictionary Unsatisfiable{}     = Map String CV
forall k a. Map k a
M.empty
  getModelDictionary (Satisfiable SMTConfig
_   SMTModel
m) = [(String, CV)] -> Map String CV
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel -> [(String, CV)]
modelAssocs SMTModel
m)
  getModelDictionary (DeltaSat    SMTConfig
_ Maybe String
_ SMTModel
m) = [(String, CV)] -> Map String CV
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel -> [(String, CV)]
modelAssocs SMTModel
m)
  getModelDictionary SatExtField{}       = Map String CV
forall k a. Map k a
M.empty
  getModelDictionary Unknown{}           = Map String CV
forall k a. Map k a
M.empty
  getModelDictionary ProofError{}        = Map String CV
forall k a. Map k a
M.empty

  getModelObjectives :: SMTResult -> Map String GeneralizedCV
getModelObjectives Unsatisfiable{}     = Map String GeneralizedCV
forall k a. Map k a
M.empty
  getModelObjectives (Satisfiable SMTConfig
_ SMTModel
m  ) = [(String, GeneralizedCV)] -> Map String GeneralizedCV
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel -> [(String, GeneralizedCV)]
modelObjectives SMTModel
m)
  getModelObjectives (DeltaSat    SMTConfig
_ Maybe String
_ SMTModel
m) = [(String, GeneralizedCV)] -> Map String GeneralizedCV
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel -> [(String, GeneralizedCV)]
modelObjectives SMTModel
m)
  getModelObjectives (SatExtField SMTConfig
_ SMTModel
m  ) = [(String, GeneralizedCV)] -> Map String GeneralizedCV
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel -> [(String, GeneralizedCV)]
modelObjectives SMTModel
m)
  getModelObjectives Unknown{}           = Map String GeneralizedCV
forall k a. Map k a
M.empty
  getModelObjectives ProofError{}        = Map String GeneralizedCV
forall k a. Map k a
M.empty

  getModelUIFuns :: SMTResult -> Map String (SBVType, ([([CV], CV)], CV))
getModelUIFuns Unsatisfiable{}     = Map String (SBVType, ([([CV], CV)], CV))
forall k a. Map k a
M.empty
  getModelUIFuns (Satisfiable SMTConfig
_ SMTModel
m  ) = [(String, (SBVType, ([([CV], CV)], CV)))]
-> Map String (SBVType, ([([CV], CV)], CV))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel -> [(String, (SBVType, ([([CV], CV)], CV)))]
modelUIFuns SMTModel
m)
  getModelUIFuns (DeltaSat    SMTConfig
_ Maybe String
_ SMTModel
m) = [(String, (SBVType, ([([CV], CV)], CV)))]
-> Map String (SBVType, ([([CV], CV)], CV))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel -> [(String, (SBVType, ([([CV], CV)], CV)))]
modelUIFuns SMTModel
m)
  getModelUIFuns (SatExtField SMTConfig
_ SMTModel
m  ) = [(String, (SBVType, ([([CV], CV)], CV)))]
-> Map String (SBVType, ([([CV], CV)], CV))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel -> [(String, (SBVType, ([([CV], CV)], CV)))]
modelUIFuns SMTModel
m)
  getModelUIFuns Unknown{}           = Map String (SBVType, ([([CV], CV)], CV))
forall k a. Map k a
M.empty
  getModelUIFuns ProofError{}        = Map String (SBVType, ([([CV], CV)], CV))
forall k a. Map k a
M.empty

-- | Extract a model out, will throw error if parsing is unsuccessful
parseModelOut :: SatModel a => SMTModel -> a
parseModelOut :: SMTModel -> a
parseModelOut SMTModel
m = case [CV] -> Maybe (a, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV
c | (String
_, CV
c) <- SMTModel -> [(String, CV)]
modelAssocs SMTModel
m] of
                   Just (a
x, []) -> a
x
                   Just (a
_, [CV]
ys) -> String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"SBV.parseModelOut: Partially constructed model; remaining elements: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [CV] -> String
forall a. Show a => a -> String
show [CV]
ys
                   Maybe (a, [CV])
Nothing      -> String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"SBV.parseModelOut: Cannot construct a model from: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ SMTModel -> String
forall a. Show a => a -> String
show SMTModel
m

-- | Given an 'Data.SBV.allSat' call, we typically want to iterate over it and print the results in sequence. The
-- 'displayModels' function automates this task by calling @disp@ on each result, consecutively. The first
-- 'Int' argument to @disp@ 'is the current model number. The second argument is a tuple, where the first
-- element indicates whether the model is alleged (i.e., if the solver is not sure, returning Unknown).
-- The arrange argument can sort the results in any way you like, if necessary.
displayModels :: SatModel a => ([(Bool, a)] -> [(Bool, a)]) -> (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
displayModels :: ([(Bool, a)] -> [(Bool, a)])
-> (Int -> (Bool, a) -> IO ()) -> AllSatResult -> IO Int
displayModels [(Bool, a)] -> [(Bool, a)]
arrange Int -> (Bool, a) -> IO ()
disp AllSatResult{allSatResults :: AllSatResult -> [SMTResult]
allSatResults = [SMTResult]
ms} = do
    let models :: [(Bool, a)]
models = [(Bool, a)
a | Right (Bool, a)
a <- (SMTResult -> Either String (Bool, a))
-> [SMTResult] -> [Either String (Bool, a)]
forall a b. (a -> b) -> [a] -> [b]
map (SatResult -> Either String (Bool, a)
forall a b.
(Modelable a, SatModel b) =>
a -> Either String (Bool, b)
getModelAssignment (SatResult -> Either String (Bool, a))
-> (SMTResult -> SatResult) -> SMTResult -> Either String (Bool, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTResult -> SatResult
SatResult) [SMTResult]
ms]
    [Int]
inds <- ((Bool, a) -> Int -> IO Int) -> [(Bool, a)] -> [Int] -> IO [Int]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM (Bool, a) -> Int -> IO Int
display ([(Bool, a)] -> [(Bool, a)]
arrange [(Bool, a)]
models) [(Int
1::Int)..]
    Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> IO Int) -> Int -> IO Int
forall a b. (a -> b) -> a -> b
$ [Int] -> Int
forall a. [a] -> a
last (Int
0Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
:[Int]
inds)
  where display :: (Bool, a) -> Int -> IO Int
display (Bool, a)
r Int
i = Int -> (Bool, a) -> IO ()
disp Int
i (Bool, a)
r IO () -> IO Int -> IO Int
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> IO Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
i

-- | Show an SMTResult; generic version
showSMTResult :: String -> String -> String -> String -> (Maybe String -> String) -> String -> SMTResult -> String
showSMTResult :: String
-> String
-> String
-> String
-> (Maybe String -> String)
-> String
-> SMTResult
-> String
showSMTResult String
unsatMsg String
unkMsg String
satMsg String
satMsgModel Maybe String -> String
dSatMsgModel String
satExtMsg SMTResult
result = case SMTResult
result of
  Unsatisfiable SMTConfig
_ Maybe [String]
uc                 -> String
unsatMsg String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe [String] -> String
showUnsatCore Maybe [String]
uc
  Satisfiable SMTConfig
_ (SMTModel [(String, GeneralizedCV)]
_ Maybe [((Quantifier, NamedSymVar), Maybe CV)]
_ [] []) -> String
satMsg
  Satisfiable SMTConfig
_   SMTModel
m                  -> String
satMsgModel    String -> ShowS
forall a. [a] -> [a] -> [a]
++ SMTConfig -> SMTModel -> String
showModel SMTConfig
cfg SMTModel
m
  DeltaSat    SMTConfig
_ Maybe String
p SMTModel
m                  -> Maybe String -> String
dSatMsgModel Maybe String
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ SMTConfig -> SMTModel -> String
showModel SMTConfig
cfg SMTModel
m
  SatExtField SMTConfig
_ (SMTModel [(String, GeneralizedCV)]
b Maybe [((Quantifier, NamedSymVar), Maybe CV)]
_ [(String, CV)]
_ [(String, (SBVType, ([([CV], CV)], CV)))]
_)   -> String
satExtMsg   String -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> Bool -> SMTConfig -> [(String, GeneralizedCV)] -> String
showModelDictionary Bool
True Bool
False SMTConfig
cfg [(String, GeneralizedCV)]
b
  Unknown     SMTConfig
_ SMTReasonUnknown
r                    -> String
unkMsg String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
".\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"  Reason: " String -> ShowS
`alignPlain` SMTReasonUnknown -> String
forall a. Show a => a -> String
show SMTReasonUnknown
r
  ProofError  SMTConfig
_ [] Maybe SMTResult
Nothing           -> String
"*** An error occurred. No additional information available. Try running in verbose mode."
  ProofError  SMTConfig
_ [String]
ls Maybe SMTResult
Nothing           -> String
"*** An error occurred.\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" (ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"***  " String -> ShowS
forall a. [a] -> [a] -> [a]
++) [String]
ls)
  ProofError  SMTConfig
_ [String]
ls (Just SMTResult
r)          -> String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$  [ String
"*** " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
l | String
l <- [String]
ls]
                                                         [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"***"
                                                            , String
"*** Alleged model:"
                                                            , String
"***"
                                                            ]
                                                         [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"*** "  String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
l | String
l <- String -> [String]
lines (String
-> String
-> String
-> String
-> (Maybe String -> String)
-> String
-> SMTResult
-> String
showSMTResult String
unsatMsg String
unkMsg String
satMsg String
satMsgModel Maybe String -> String
dSatMsgModel String
satExtMsg SMTResult
r)]

 where cfg :: SMTConfig
cfg = SMTResult -> SMTConfig
resultConfig SMTResult
result
       showUnsatCore :: Maybe [String] -> String
showUnsatCore Maybe [String]
Nothing   = String
""
       showUnsatCore (Just [String]
xs) = String
". Unsat core:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String
"    " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x | String
x <- [String]
xs]

-- | Show a model in human readable form. Ignore bindings to those variables that start
-- with "__internal_sbv_" and also those marked as "nonModelVar" in the config; as these are only for internal purposes
showModel :: SMTConfig -> SMTModel -> String
showModel :: SMTConfig -> SMTModel -> String
showModel SMTConfig
cfg SMTModel
model
   | [(String, (SBVType, ([([CV], CV)], CV)))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, (SBVType, ([([CV], CV)], CV)))]
uiFuncs
   = String
nonUIFuncs
   | Bool
True
   = ShowS
sep String
nonUIFuncs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n\n" (((String, (SBVType, ([([CV], CV)], CV))) -> String)
-> [(String, (SBVType, ([([CV], CV)], CV)))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (SMTConfig -> (String, (SBVType, ([([CV], CV)], CV))) -> String
showModelUI SMTConfig
cfg) [(String, (SBVType, ([([CV], CV)], CV)))]
uiFuncs)
   where nonUIFuncs :: String
nonUIFuncs = Bool -> Bool -> SMTConfig -> [(String, GeneralizedCV)] -> String
showModelDictionary ([(String, (SBVType, ([([CV], CV)], CV)))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, (SBVType, ([([CV], CV)], CV)))]
uiFuncs) Bool
False SMTConfig
cfg [(String
n, CV -> GeneralizedCV
RegularCV CV
c) | (String
n, CV
c) <- SMTModel -> [(String, CV)]
modelAssocs SMTModel
model]
         uiFuncs :: [(String, (SBVType, ([([CV], CV)], CV)))]
uiFuncs    = SMTModel -> [(String, (SBVType, ([([CV], CV)], CV)))]
modelUIFuns SMTModel
model
         sep :: ShowS
sep String
""     = String
""
         sep String
x      = String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n\n"

-- | Show bindings in a generalized model dictionary, tabulated
showModelDictionary :: Bool -> Bool -> SMTConfig -> [(String, GeneralizedCV)] -> String
showModelDictionary :: Bool -> Bool -> SMTConfig -> [(String, GeneralizedCV)] -> String
showModelDictionary Bool
warnEmpty Bool
includeEverything SMTConfig
cfg [(String, GeneralizedCV)]
allVars
   | [(String, GeneralizedCV)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, GeneralizedCV)]
allVars
   = ShowS
forall p. IsString p => p -> p
warn String
"[There are no variables bound by the model.]"
   | [(String, GeneralizedCV)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, GeneralizedCV)]
relevantVars
   = ShowS
forall p. IsString p => p -> p
warn String
"[There are no model-variables bound by the model.]"
   | Bool
True
   = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String)
-> ([(String, GeneralizedCV)] -> [String])
-> [(String, GeneralizedCV)]
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [((Int, String), (Int, String))] -> [String]
display ([((Int, String), (Int, String))] -> [String])
-> ([(String, GeneralizedCV)] -> [((Int, String), (Int, String))])
-> [(String, GeneralizedCV)]
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, GeneralizedCV) -> ((Int, String), (Int, String)))
-> [(String, GeneralizedCV)] -> [((Int, String), (Int, String))]
forall a b. (a -> b) -> [a] -> [b]
map (String, GeneralizedCV) -> ((Int, String), (Int, String))
forall (t :: * -> *) a.
Foldable t =>
(t a, GeneralizedCV) -> ((Int, t a), (Int, String))
shM ([(String, GeneralizedCV)] -> String)
-> [(String, GeneralizedCV)] -> String
forall a b. (a -> b) -> a -> b
$ [(String, GeneralizedCV)]
relevantVars
  where warn :: p -> p
warn p
s = if Bool
warnEmpty then p
s else p
""

        relevantVars :: [(String, GeneralizedCV)]
relevantVars  = ((String, GeneralizedCV) -> Bool)
-> [(String, GeneralizedCV)] -> [(String, GeneralizedCV)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> ((String, GeneralizedCV) -> Bool)
-> (String, GeneralizedCV)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, GeneralizedCV) -> Bool
forall b. (String, b) -> Bool
ignore) [(String, GeneralizedCV)]
allVars
        ignore :: (String, b) -> Bool
ignore (String -> Text
T.pack -> Text
s, b
_)
          | Bool
includeEverything = Bool
False
          | Bool
True              = Text
"__internal_sbv_" Text -> Text -> Bool
`T.isPrefixOf` Text
s Bool -> Bool -> Bool
|| SMTConfig -> Text -> Bool
isNonModelVar SMTConfig
cfg Text
s

        shM :: (t a, GeneralizedCV) -> ((Int, t a), (Int, String))
shM (t a
s, RegularCV CV
v) = let vs :: String
vs = SMTConfig -> CV -> String
shCV SMTConfig
cfg CV
v in ((t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
s, t a
s), (String -> Int
vlength String
vs, String
vs))
        shM (t a
s, GeneralizedCV
other)       = let vs :: String
vs = GeneralizedCV -> String
forall a. Show a => a -> String
show GeneralizedCV
other in ((t a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length t a
s, t a
s), (String -> Int
vlength String
vs, String
vs))

        display :: [((Int, String), (Int, String))] -> [String]
display [((Int, String), (Int, String))]
svs   = (((Int, String), (Int, String)) -> String)
-> [((Int, String), (Int, String))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((Int, String), (Int, String)) -> String
forall a a. ((a, String), (a, String)) -> String
line [((Int, String), (Int, String))]
svs
           where line :: ((a, String), (a, String)) -> String
line ((a
_, String
s), (a
_, String
v)) = String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> ShowS
right (Int
nameWidth Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s) String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> ShowS
left (Int
valWidth Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
lTrimRight (ShowS
valPart String
v)) String
v
                 nameWidth :: Int
nameWidth             = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int
l | ((Int
l, String
_), (Int, String)
_) <- [((Int, String), (Int, String))]
svs]
                 valWidth :: Int
valWidth              = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int
l | ((Int, String)
_, (Int
l, String
_)) <- [((Int, String), (Int, String))]
svs]

        right :: Int -> ShowS
right Int
p String
s = String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
p Char
' '
        left :: Int -> ShowS
left  Int
p String
s = Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
p Char
' ' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
        vlength :: String -> Int
vlength String
s = case (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
':') (ShowS
forall a. [a] -> [a]
reverse ((Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'\n') String
s)) of
                      (Char
':':Char
':':String
r) -> String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace String
r)
                      String
_           -> String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s -- conservative

        valPart :: ShowS
valPart String
""          = String
""
        valPart (Char
':':Char
':':String
_) = String
""
        valPart (Char
x:String
xs)      = Char
x Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
valPart String
xs

        lTrimRight :: String -> Int
lTrimRight = String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int) -> ShowS -> String -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
forall a. [a] -> [a]
reverse

-- | Show an uninterpreted function
showModelUI :: SMTConfig -> (String, (SBVType, ([([CV], CV)], CV))) -> String
showModelUI :: SMTConfig -> (String, (SBVType, ([([CV], CV)], CV))) -> String
showModelUI SMTConfig
cfg (String
nm, (SBVType [Kind]
ts, ([([CV], CV)]
defs, CV
dflt))) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String
"  " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
l | String
l <- String
sig String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (([String], String) -> String) -> [([String], String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ([String], String) -> String
align [([String], String)]
body]
  where noOfArgs :: Int
noOfArgs = [Kind] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
ts Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1

        sig :: String
sig      = String
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" -> " ((Kind -> String) -> [Kind] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Kind -> String
showBaseKind [Kind]
ts)

        ls :: [([String], String)]
ls       = (([CV], CV) -> ([String], String))
-> [([CV], CV)] -> [([String], String)]
forall a b. (a -> b) -> [a] -> [b]
map ([CV], CV) -> ([String], String)
line [([CV], CV)]
defs
        defLine :: ([String], String)
defLine  = (String
nm String -> [String] -> [String]
forall a. a -> [a] -> [a]
: Int -> String -> [String]
forall a. Int -> a -> [a]
replicate Int
noOfArgs String
"_", CV -> String
scv CV
dflt)

        body :: [([String], String)]
body     = [([String], String)]
ls [([String], String)]
-> [([String], String)] -> [([String], String)]
forall a. [a] -> [a] -> [a]
++ [([String], String)
defLine]

        colWidths :: [Int]
colWidths = [[Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: (String -> Int) -> [String] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
col) | [String]
col <- [[String]] -> [[String]]
forall a. [[a]] -> [[a]]
transpose ((([String], String) -> [String])
-> [([String], String)] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map ([String], String) -> [String]
forall a b. (a, b) -> a
fst [([String], String)]
body)]

        resWidth :: Int
resWidth  = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum  (Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: (([String], String) -> Int) -> [([String], String)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (String -> Int)
-> (([String], String) -> String) -> ([String], String) -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([String], String) -> String
forall a b. (a, b) -> b
snd) [([String], String)]
body)

        align :: ([String], String) -> String
align ([String]
xs, String
r) = [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (Int -> ShowS) -> [Int] -> [String] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> ShowS
left [Int]
colWidths [String]
xs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"=", Int -> ShowS
left Int
resWidth String
r]
           where left :: Int -> ShowS
left Int
i String
x = Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
i (String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. a -> [a]
repeat Char
' ')

        scv :: CV -> String
scv = Int -> CV -> String
forall a. (Eq a, Num a) => a -> CV -> String
sh (SMTConfig -> Int
printBase SMTConfig
cfg)
          where sh :: a -> CV -> String
sh a
2  = CV -> String
forall a. PrettyNum a => a -> String
binP
                sh a
10 = Bool -> CV -> String
showCV Bool
False
                sh a
16 = CV -> String
forall a. PrettyNum a => a -> String
hexP
                sh a
_  = CV -> String
forall a. Show a => a -> String
show

        -- NB. If we have a float NaN/Infinity/+0/-0 etc. these will
        -- simply print as is, but will not be valid patterns. (We
        -- have the semi-goal of being able to paste these definitions
        -- in a Haskell file.) For the time being, punt on this, but
        -- we might want to do this properly later somehow. (Perhaps
        -- using some sort of a view pattern.)
        line :: ([CV], CV) -> ([String], String)
        line :: ([CV], CV) -> ([String], String)
line ([CV]
args, CV
r) = (String
nm String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (CV -> String) -> [CV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (ShowS
paren ShowS -> (CV -> String) -> CV -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> String
scv) [CV]
args, CV -> String
scv CV
r)
          where -- If negative, parenthesize. I think this is the only case
                -- we need to worry about. Hopefully!
                paren :: String -> String
                paren :: ShowS
paren x :: String
x@(Char
'-':String
_) = Char
'(' Char -> ShowS
forall a. a -> [a] -> [a]
: String
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
                paren String
x         = String
x

-- | Show a constant value, in the user-specified base
shCV :: SMTConfig -> CV -> String
shCV :: SMTConfig -> CV -> String
shCV = Int -> CV -> String
forall a a.
(Eq a, Num a, PrettyNum a, Show a, Show a) =>
a -> a -> String
sh (Int -> CV -> String)
-> (SMTConfig -> Int) -> SMTConfig -> CV -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTConfig -> Int
printBase
  where sh :: a -> a -> String
sh a
2  = a -> String
forall a. PrettyNum a => a -> String
binS
        sh a
10 = a -> String
forall a. Show a => a -> String
show
        sh a
16 = a -> String
forall a. PrettyNum a => a -> String
hexS
        sh a
n  = \a
w -> a -> String
forall a. Show a => a -> String
show a
w String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -- Ignoring unsupported printBase " String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", use 2, 10, or 16."

-- | Helper function to spin off to an SMT solver.
pipeProcess :: SMTConfig -> State -> String -> [String] -> String -> (State -> IO a) -> IO a
pipeProcess :: SMTConfig
-> State -> String -> [String] -> String -> (State -> IO a) -> IO a
pipeProcess SMTConfig
cfg State
ctx String
execName [String]
opts String
pgm State -> IO a
continuation = do
    Maybe String
mbExecPath <- String -> IO (Maybe String)
findExecutable String
execName
    case Maybe String
mbExecPath of
      Maybe String
Nothing      -> String -> IO a
forall a. HasCallStack => String -> a
error (String -> IO a) -> String -> IO a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Unable to locate executable for " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Solver -> String
forall a. Show a => a -> String
show (SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
cfg))
                                      , String
"Executable specified: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
execName
                                      ]

      Just String
execPath -> SMTConfig
-> State -> String -> [String] -> String -> (State -> IO a) -> IO a
forall a.
SMTConfig
-> State -> String -> [String] -> String -> (State -> IO a) -> IO a
runSolver SMTConfig
cfg State
ctx String
execPath [String]
opts String
pgm State -> IO a
continuation
                       IO a -> [Handler a] -> IO a
forall a. IO a -> [Handler a] -> IO a
`C.catches`
                        [ (SBVException -> IO a) -> Handler a
forall a e. Exception e => (e -> IO a) -> Handler a
C.Handler (\(SBVException
e :: SBVException)    -> SBVException -> IO a
forall e a. Exception e => e -> IO a
C.throwIO SBVException
e)
                        , (ErrorCall -> IO a) -> Handler a
forall a e. Exception e => (e -> IO a) -> Handler a
C.Handler (\(ErrorCall
e :: C.ErrorCall)     -> ErrorCall -> IO a
forall e a. Exception e => e -> IO a
C.throwIO ErrorCall
e)
                        , (SomeException -> IO a) -> Handler a
forall a e. Exception e => (e -> IO a) -> Handler a
C.Handler (\(SomeException
e :: C.SomeException) -> SomeException -> IO a -> IO a
forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (IO a -> IO a) -> IO a -> IO a
forall a b. (a -> b) -> a -> b
$ String -> IO a
forall a. HasCallStack => String -> a
error (String -> IO a) -> String -> IO a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Failed to start the external solver:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ SomeException -> String
forall a. Show a => a -> String
show SomeException
e
                                                                                                , String
"Make sure you can start " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> String
show String
execPath
                                                                                                , String
"from the command line without issues."
                                                                                                ])
                        ]

-- | A standard engine interface. Most solvers follow-suit here in how we "chat" to them..
standardEngine :: String
               -> String
               -> SMTEngine
standardEngine :: String -> String -> SMTEngine
standardEngine String
envName String
envOptName SMTConfig
cfg State
ctx String
pgm State -> IO res
continuation = do

    String
execName <-                    String -> IO String
getEnv String
envName     IO String -> (SomeException -> IO String) -> IO String
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch` (\(SomeException
e :: C.SomeException) -> SomeException -> IO String -> IO String
forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTSolver -> String
executable (SMTConfig -> SMTSolver
solver SMTConfig
cfg))))
    [String]
execOpts <- (String -> [String]
splitArgs (String -> [String]) -> IO String -> IO [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap`  String -> IO String
getEnv String
envOptName) IO [String] -> (SomeException -> IO [String]) -> IO [String]
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch` (\(SomeException
e :: C.SomeException) -> SomeException -> IO [String] -> IO [String]
forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e ([String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTSolver -> SMTConfig -> [String]
options (SMTConfig -> SMTSolver
solver SMTConfig
cfg) SMTConfig
cfg)))

    let cfg' :: SMTConfig
cfg' = SMTConfig
cfg {solver :: SMTSolver
solver = (SMTConfig -> SMTSolver
solver SMTConfig
cfg) {executable :: String
executable = String
execName, options :: SMTConfig -> [String]
options = [String] -> SMTConfig -> [String]
forall a b. a -> b -> a
const [String]
execOpts}}

    SMTConfig -> State -> String -> (State -> IO res) -> IO res
SMTEngine
standardSolver SMTConfig
cfg' State
ctx String
pgm State -> IO res
continuation

-- | A standard solver interface. If the solver is SMT-Lib compliant, then this function should suffice in
-- communicating with it.
standardSolver :: SMTConfig       -- ^ The currrent configuration
               -> State           -- ^ Context in which we are running
               -> String          -- ^ The program
               -> (State -> IO a) -- ^ The continuation
               -> IO a
standardSolver :: SMTConfig -> State -> String -> (State -> IO a) -> IO a
standardSolver SMTConfig
config State
ctx String
pgm State -> IO a
continuation = do
    let msg :: String -> m ()
msg String
s    = SMTConfig -> [String] -> m ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
debug SMTConfig
config [String
"** " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s]
        smtSolver :: SMTSolver
smtSolver= SMTConfig -> SMTSolver
solver SMTConfig
config
        exec :: String
exec     = SMTSolver -> String
executable SMTSolver
smtSolver
        opts :: [String]
opts     = SMTSolver -> SMTConfig -> [String]
options SMTSolver
smtSolver SMTConfig
config [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ SMTConfig -> [String]
extraArgs SMTConfig
config
    String -> IO ()
forall (m :: * -> *). MonadIO m => String -> m ()
msg (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Calling: "  String -> ShowS
forall a. [a] -> [a] -> [a]
++ (String
exec String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
opts then String
"" else String
" ") String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
joinArgs [String]
opts)
    String -> ()
forall a. NFData a => a -> ()
rnf String
pgm () -> IO a -> IO a
`seq` SMTConfig
-> State -> String -> [String] -> String -> (State -> IO a) -> IO a
forall a.
SMTConfig
-> State -> String -> [String] -> String -> (State -> IO a) -> IO a
pipeProcess SMTConfig
config State
ctx String
exec [String]
opts String
pgm State -> IO a
continuation

-- | An internal type to track of solver interactions
data SolverLine = SolverRegular   String  -- ^ All is well
                | SolverTimeout   String  -- ^ Timeout expired
                | SolverException String  -- ^ Something else went wrong

-- | A variant of @readProcessWithExitCode@; except it deals with SBV continuations
runSolver :: SMTConfig -> State -> FilePath -> [String] -> String -> (State -> IO a) -> IO a
runSolver :: SMTConfig
-> State -> String -> [String] -> String -> (State -> IO a) -> IO a
runSolver SMTConfig
cfg State
ctx String
execPath [String]
opts String
pgm State -> IO a
continuation
 = do let nm :: String
nm  = Solver -> String
forall a. Show a => a -> String
show (SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
cfg))
          msg :: [String] -> IO ()
msg = SMTConfig -> [String] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
debug SMTConfig
cfg ([String] -> IO ()) -> ([String] -> [String]) -> [String] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"*** " String -> ShowS
forall a. [a] -> [a] -> [a]
++)

          clean :: ShowS
clean = SMTSolver -> ShowS
preprocess (SMTConfig -> SMTSolver
solver SMTConfig
cfg)

      (Maybe Int -> String -> IO ()
send, Maybe Int -> String -> IO String
ask, Maybe String -> Maybe Int -> IO String
getResponseFromSolver, IO (String, String, ExitCode)
terminateSolver, IO ()
cleanUp, ProcessHandle
pid) <- do
                (Handle
inh, Handle
outh, Handle
errh, ProcessHandle
pid) <- String
-> [String]
-> Maybe String
-> Maybe [(String, String)]
-> IO (Handle, Handle, Handle, ProcessHandle)
runInteractiveProcess String
execPath [String]
opts Maybe String
forall a. Maybe a
Nothing Maybe [(String, String)]
forall a. Maybe a
Nothing

                let send :: Maybe Int -> String -> IO ()
                    send :: Maybe Int -> String -> IO ()
send Maybe Int
mbTimeOut String
command = do Handle -> String -> IO ()
hPutStrLn Handle
inh (ShowS
clean String
command)
                                                Handle -> IO ()
hFlush Handle
inh
                                                Maybe String -> Either (String, Maybe Int) String -> IO ()
recordTranscript (SMTConfig -> Maybe String
transcript SMTConfig
cfg) (Either (String, Maybe Int) String -> IO ())
-> Either (String, Maybe Int) String -> IO ()
forall a b. (a -> b) -> a -> b
$ (String, Maybe Int) -> Either (String, Maybe Int) String
forall a b. a -> Either a b
Left (String
command, Maybe Int
mbTimeOut)

                    -- Send a line, get a whole s-expr. We ignore the pathetic case that there might be a string with an unbalanced parentheses in it in a response.
                    ask :: Maybe Int -> String -> IO String
                    ask :: Maybe Int -> String -> IO String
ask Maybe Int
mbTimeOut String
command =
                                  -- solvers don't respond to empty lines or comments; we just pass back
                                  -- success in these cases to keep the illusion of everything has a response
                                  let cmd :: String
cmd = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace String
command
                                  in if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
cmd Bool -> Bool -> Bool
|| String
";" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
cmd
                                     then String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
"success"
                                     else do Maybe Int -> String -> IO ()
send Maybe Int
mbTimeOut String
command
                                             Maybe String -> Maybe Int -> IO String
getResponseFromSolver (String -> Maybe String
forall a. a -> Maybe a
Just String
command) Maybe Int
mbTimeOut

                    -- Get a response from the solver, with an optional time-out on how long
                    -- to wait. Note that there's *always* a time-out of 5 seconds once we get the
                    -- first line of response, as while the solver might take it's time to respond,
                    -- once it starts responding successive lines should come quickly.
                    getResponseFromSolver :: Maybe String -> Maybe Int -> IO String
                    getResponseFromSolver :: Maybe String -> Maybe Int -> IO String
getResponseFromSolver Maybe String
mbCommand Maybe Int
mbTimeOut = do
                                [String]
response <- Bool -> Int -> [String] -> IO [String]
go Bool
True Int
0 []
                                let collated :: String
collated = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. [a] -> [a]
reverse [String]
response
                                Maybe String -> Either (String, Maybe Int) String -> IO ()
recordTranscript (SMTConfig -> Maybe String
transcript SMTConfig
cfg) (Either (String, Maybe Int) String -> IO ())
-> Either (String, Maybe Int) String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Either (String, Maybe Int) String
forall a b. b -> Either a b
Right String
collated
                                String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
collated

                      where safeGetLine :: Bool -> Handle -> IO SolverLine
safeGetLine Bool
isFirst Handle
h =
                                         let timeOutToUse :: Maybe Int
timeOutToUse | Bool
isFirst = Maybe Int
mbTimeOut
                                                          | Bool
True    = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
5000000
                                             timeOutMsg :: Int -> String
timeOutMsg Int
t | Bool
isFirst = String
"User specified timeout of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
showTimeoutValue Int
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" exceeded"
                                                          | Bool
True    = String
"A multiline complete response wasn't received before " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
showTimeoutValue Int
t String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" exceeded"

                                             -- Like hGetLine, except it keeps getting lines if inside a string.
                                             getFullLine :: IO String
                                             getFullLine :: IO String
getFullLine = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String)
-> ([String] -> [String]) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [String]
forall a. [a] -> [a]
reverse ([String] -> String) -> IO [String] -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> [String] -> IO [String]
collect Bool
False []
                                                where collect :: Bool -> [String] -> IO [String]
collect Bool
inString [String]
sofar = do String
ln <- Handle -> IO String
hGetLine Handle
h

                                                                                  let walk :: Bool -> String -> Bool
walk Bool
inside []           = Bool
inside
                                                                                      walk Bool
inside (Char
'"':String
cs)     = Bool -> String -> Bool
walk (Bool -> Bool
not Bool
inside) String
cs
                                                                                      walk Bool
inside (Char
_:String
cs)       = Bool -> String -> Bool
walk Bool
inside       String
cs

                                                                                      stillInside :: Bool
stillInside = Bool -> String -> Bool
walk Bool
inString String
ln

                                                                                      sofar' :: [String]
sofar' = String
ln String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar

                                                                                  if Bool
stillInside
                                                                                     then Bool -> [String] -> IO [String]
collect Bool
True [String]
sofar'
                                                                                     else [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return [String]
sofar'

                                         in case Maybe Int
timeOutToUse of
                                              Maybe Int
Nothing -> String -> SolverLine
SolverRegular (String -> SolverLine) -> IO String -> IO SolverLine
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO String
getFullLine
                                              Just Int
t  -> do Maybe String
r <- Int -> IO String -> IO (Maybe String)
forall a. Int -> IO a -> IO (Maybe a)
Timeout.timeout Int
t IO String
getFullLine
                                                            case Maybe String
r of
                                                              Just String
l  -> SolverLine -> IO SolverLine
forall (m :: * -> *) a. Monad m => a -> m a
return (SolverLine -> IO SolverLine) -> SolverLine -> IO SolverLine
forall a b. (a -> b) -> a -> b
$ String -> SolverLine
SolverRegular String
l
                                                              Maybe String
Nothing -> SolverLine -> IO SolverLine
forall (m :: * -> *) a. Monad m => a -> m a
return (SolverLine -> IO SolverLine) -> SolverLine -> IO SolverLine
forall a b. (a -> b) -> a -> b
$ String -> SolverLine
SolverTimeout (String -> SolverLine) -> String -> SolverLine
forall a b. (a -> b) -> a -> b
$ Int -> String
timeOutMsg Int
t


                            go :: Bool -> Int -> [String] -> IO [String]
go Bool
isFirst Int
i [String]
sofar = do
                                            SolverLine
errln <- Bool -> Handle -> IO SolverLine
safeGetLine Bool
isFirst Handle
outh IO SolverLine -> (SomeException -> IO SolverLine) -> IO SolverLine
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch` (\(SomeException
e :: C.SomeException) -> SomeException -> IO SolverLine -> IO SolverLine
forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (SolverLine -> IO SolverLine
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> SolverLine
SolverException (SomeException -> String
forall a. Show a => a -> String
show SomeException
e))))
                                            case SolverLine
errln of
                                              SolverRegular String
ln -> let need :: Int
need  = Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ String -> Int
parenDeficit String
ln
                                                                      -- make sure we get *something*
                                                                      empty :: Bool
empty = case (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace String
ln of
                                                                                []      -> Bool
True
                                                                                (Char
';':String
_) -> Bool
True   -- yes this does happen! I've seen z3 print out comments on stderr.
                                                                                String
_       -> Bool
False
                                                                  in case (Bool
empty, Int
need Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0) of
                                                                        (Bool
True, Bool
_)      -> do SMTConfig -> [String] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
debug SMTConfig
cfg [String
"[SKIP] " String -> ShowS
`alignPlain` String
ln]
                                                                                             Bool -> Int -> [String] -> IO [String]
go Bool
isFirst Int
need [String]
sofar
                                                                        (Bool
False, Bool
False) -> Bool -> Int -> [String] -> IO [String]
go Bool
False   Int
need (String
lnString -> [String] -> [String]
forall a. a -> [a] -> [a]
:[String]
sofar)
                                                                        (Bool
False, Bool
True)  -> [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return (String
lnString -> [String] -> [String]
forall a. a -> [a] -> [a]
:[String]
sofar)

                                              SolverException String
e -> do ProcessHandle -> IO ()
terminateProcess ProcessHandle
pid
                                                                      SBVException -> IO [String]
forall e a. Exception e => e -> IO a
C.throwIO SBVException :: String
-> Maybe String
-> Maybe String
-> Maybe String
-> Maybe String
-> Maybe String
-> Maybe ExitCode
-> SMTConfig
-> Maybe [String]
-> Maybe [String]
-> SBVException
SBVException { sbvExceptionDescription :: String
sbvExceptionDescription = String
e
                                                                                             , sbvExceptionSent :: Maybe String
sbvExceptionSent        = Maybe String
mbCommand
                                                                                             , sbvExceptionExpected :: Maybe String
sbvExceptionExpected    = Maybe String
forall a. Maybe a
Nothing
                                                                                             , sbvExceptionReceived :: Maybe String
sbvExceptionReceived    = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> [String]
forall a. [a] -> [a]
reverse [String]
sofar)
                                                                                             , sbvExceptionStdOut :: Maybe String
sbvExceptionStdOut      = Maybe String
forall a. Maybe a
Nothing
                                                                                             , sbvExceptionStdErr :: Maybe String
sbvExceptionStdErr      = Maybe String
forall a. Maybe a
Nothing
                                                                                             , sbvExceptionExitCode :: Maybe ExitCode
sbvExceptionExitCode    = Maybe ExitCode
forall a. Maybe a
Nothing
                                                                                             , sbvExceptionConfig :: SMTConfig
sbvExceptionConfig      = SMTConfig
cfg { solver :: SMTSolver
solver = (SMTConfig -> SMTSolver
solver SMTConfig
cfg) { executable :: String
executable = String
execPath } }
                                                                                             , sbvExceptionReason :: Maybe [String]
sbvExceptionReason      = Maybe [String]
forall a. Maybe a
Nothing
                                                                                             , sbvExceptionHint :: Maybe [String]
sbvExceptionHint        = if String
"hGetLine: end of file" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isInfixOf` String
e
                                                                                                                         then [String] -> Maybe [String]
forall a. a -> Maybe a
Just [ String
"Solver process prematurely ended communication."
                                                                                                                                   , String
""
                                                                                                                                   , String
"It is likely it was terminated because of a seg-fault."
                                                                                                                                   , String
"Run with 'transcript=Just \"bad.smt2\"' option, and feed"
                                                                                                                                   , String
"the generated \"bad.smt2\" file directly to the solver"
                                                                                                                                   , String
"outside of SBV for further information."
                                                                                                                                   ]
                                                                                                                         else Maybe [String]
forall a. Maybe a
Nothing
                                                                                             }

                                              SolverTimeout String
e -> do ProcessHandle -> IO ()
terminateProcess ProcessHandle
pid -- NB. Do not *wait* for the process, just quit.
                                                                    SBVException -> IO [String]
forall e a. Exception e => e -> IO a
C.throwIO SBVException :: String
-> Maybe String
-> Maybe String
-> Maybe String
-> Maybe String
-> Maybe String
-> Maybe ExitCode
-> SMTConfig
-> Maybe [String]
-> Maybe [String]
-> SBVException
SBVException { sbvExceptionDescription :: String
sbvExceptionDescription = String
"Timeout! " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
e
                                                                                           , sbvExceptionSent :: Maybe String
sbvExceptionSent        = Maybe String
mbCommand
                                                                                           , sbvExceptionExpected :: Maybe String
sbvExceptionExpected    = Maybe String
forall a. Maybe a
Nothing
                                                                                           , sbvExceptionReceived :: Maybe String
sbvExceptionReceived    = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> [String]
forall a. [a] -> [a]
reverse [String]
sofar)
                                                                                           , sbvExceptionStdOut :: Maybe String
sbvExceptionStdOut      = Maybe String
forall a. Maybe a
Nothing
                                                                                           , sbvExceptionStdErr :: Maybe String
sbvExceptionStdErr      = Maybe String
forall a. Maybe a
Nothing
                                                                                           , sbvExceptionExitCode :: Maybe ExitCode
sbvExceptionExitCode    = Maybe ExitCode
forall a. Maybe a
Nothing
                                                                                           , sbvExceptionConfig :: SMTConfig
sbvExceptionConfig      = SMTConfig
cfg { solver :: SMTSolver
solver = (SMTConfig -> SMTSolver
solver SMTConfig
cfg) { executable :: String
executable = String
execPath } }
                                                                                           , sbvExceptionReason :: Maybe [String]
sbvExceptionReason      = Maybe [String]
forall a. Maybe a
Nothing
                                                                                           , sbvExceptionHint :: Maybe [String]
sbvExceptionHint        = if Bool -> Bool
not (SMTConfig -> Bool
verbose SMTConfig
cfg)
                                                                                                                       then [String] -> Maybe [String]
forall a. a -> Maybe a
Just [String
"Run with 'verbose=True' for further information"]
                                                                                                                       else Maybe [String]
forall a. Maybe a
Nothing
                                                                                           }

                    terminateSolver :: IO (String, String, ExitCode)
terminateSolver = do Handle -> IO ()
hClose Handle
inh
                                         MVar ()
outMVar <- IO (MVar ())
forall a. IO (MVar a)
newEmptyMVar
                                         String
out <- Handle -> IO String
hGetContents Handle
outh IO String -> (SomeException -> IO String) -> IO String
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch`  (\(SomeException
e :: C.SomeException) -> SomeException -> IO String -> IO String
forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeException -> String
forall a. Show a => a -> String
show SomeException
e)))
                                         ThreadId
_ <- IO () -> IO ThreadId
forkIO (IO () -> IO ThreadId) -> IO () -> IO ThreadId
forall a b. (a -> b) -> a -> b
$ Int -> IO Int
forall a. a -> IO a
C.evaluate (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
out) IO Int -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MVar () -> () -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ()
outMVar ()
                                         String
err <- Handle -> IO String
hGetContents Handle
errh IO String -> (SomeException -> IO String) -> IO String
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch`  (\(SomeException
e :: C.SomeException) -> SomeException -> IO String -> IO String
forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeException -> String
forall a. Show a => a -> String
show SomeException
e)))
                                         ThreadId
_ <- IO () -> IO ThreadId
forkIO (IO () -> IO ThreadId) -> IO () -> IO ThreadId
forall a b. (a -> b) -> a -> b
$ Int -> IO Int
forall a. a -> IO a
C.evaluate (String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
err) IO Int -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MVar () -> () -> IO ()
forall a. MVar a -> a -> IO ()
putMVar MVar ()
outMVar ()
                                         MVar () -> IO ()
forall a. MVar a -> IO a
takeMVar MVar ()
outMVar
                                         MVar () -> IO ()
forall a. MVar a -> IO a
takeMVar MVar ()
outMVar
                                         Handle -> IO ()
hClose Handle
outh IO () -> (SomeException -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch`  (\(SomeException
e :: C.SomeException) -> SomeException -> IO () -> IO ()
forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()))
                                         Handle -> IO ()
hClose Handle
errh IO () -> (SomeException -> IO ()) -> IO ()
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch`  (\(SomeException
e :: C.SomeException) -> SomeException -> IO () -> IO ()
forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()))
                                         ExitCode
ex <- ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
pid IO ExitCode -> (SomeException -> IO ExitCode) -> IO ExitCode
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch` (\(SomeException
e :: C.SomeException) -> SomeException -> IO ExitCode -> IO ExitCode
forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (ExitCode -> IO ExitCode
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> ExitCode
ExitFailure (-Int
999))))
                                         (String, String, ExitCode) -> IO (String, String, ExitCode)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
out, String
err, ExitCode
ex)

                    cleanUp :: IO ()
cleanUp
                      = do (String
out, String
err, ExitCode
ex) <- IO (String, String, ExitCode)
terminateSolver

                           [String] -> IO ()
msg ([String] -> IO ()) -> [String] -> IO ()
forall a b. (a -> b) -> a -> b
$   [ String
"Solver   : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm
                                   , String
"Exit code: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ExitCode -> String
forall a. Show a => a -> String
show ExitCode
ex
                                   ]
                                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"Std-out  : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n           " (String -> [String]
lines String
out) | Bool -> Bool
not (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
out)]
                                [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"Std-err  : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n           " (String -> [String]
lines String
err) | Bool -> Bool
not (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
err)]

                           Maybe String -> ExitCode -> IO ()
finalizeTranscript (SMTConfig -> Maybe String
transcript SMTConfig
cfg) ExitCode
ex
                           SMTConfig -> State -> IO ()
recordEndTime SMTConfig
cfg State
ctx

                           case ExitCode
ex of
                             ExitCode
ExitSuccess -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                             ExitCode
_           -> if SMTConfig -> Bool
ignoreExitCode SMTConfig
cfg
                                               then [String] -> IO ()
msg [String
"Ignoring non-zero exit code of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ExitCode -> String
forall a. Show a => a -> String
show ExitCode
ex String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" per user request!"]
                                               else SBVException -> IO ()
forall e a. Exception e => e -> IO a
C.throwIO SBVException :: String
-> Maybe String
-> Maybe String
-> Maybe String
-> Maybe String
-> Maybe String
-> Maybe ExitCode
-> SMTConfig
-> Maybe [String]
-> Maybe [String]
-> SBVException
SBVException { sbvExceptionDescription :: String
sbvExceptionDescription = String
"Failed to complete the call to " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm
                                                                           , sbvExceptionSent :: Maybe String
sbvExceptionSent        = Maybe String
forall a. Maybe a
Nothing
                                                                           , sbvExceptionExpected :: Maybe String
sbvExceptionExpected    = Maybe String
forall a. Maybe a
Nothing
                                                                           , sbvExceptionReceived :: Maybe String
sbvExceptionReceived    = Maybe String
forall a. Maybe a
Nothing
                                                                           , sbvExceptionStdOut :: Maybe String
sbvExceptionStdOut      = String -> Maybe String
forall a. a -> Maybe a
Just String
out
                                                                           , sbvExceptionStdErr :: Maybe String
sbvExceptionStdErr      = String -> Maybe String
forall a. a -> Maybe a
Just String
err
                                                                           , sbvExceptionExitCode :: Maybe ExitCode
sbvExceptionExitCode    = ExitCode -> Maybe ExitCode
forall a. a -> Maybe a
Just ExitCode
ex
                                                                           , sbvExceptionConfig :: SMTConfig
sbvExceptionConfig      = SMTConfig
cfg { solver :: SMTSolver
solver = (SMTConfig -> SMTSolver
solver SMTConfig
cfg) { executable :: String
executable = String
execPath } }
                                                                           , sbvExceptionReason :: Maybe [String]
sbvExceptionReason      = Maybe [String]
forall a. Maybe a
Nothing
                                                                           , sbvExceptionHint :: Maybe [String]
sbvExceptionHint        = if Bool -> Bool
not (SMTConfig -> Bool
verbose SMTConfig
cfg)
                                                                                                       then [String] -> Maybe [String]
forall a. a -> Maybe a
Just [String
"Run with 'verbose=True' for further information"]
                                                                                                       else Maybe [String]
forall a. Maybe a
Nothing
                                                                           }

                (Maybe Int -> String -> IO (), Maybe Int -> String -> IO String,
 Maybe String -> Maybe Int -> IO String,
 IO (String, String, ExitCode), IO (), ProcessHandle)
-> IO
     (Maybe Int -> String -> IO (), Maybe Int -> String -> IO String,
      Maybe String -> Maybe Int -> IO String,
      IO (String, String, ExitCode), IO (), ProcessHandle)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Int -> String -> IO ()
send, Maybe Int -> String -> IO String
ask, Maybe String -> Maybe Int -> IO String
getResponseFromSolver, IO (String, String, ExitCode)
terminateSolver, IO ()
cleanUp, ProcessHandle
pid)

      let executeSolver :: IO a
executeSolver = do let sendAndGetSuccess :: Maybe Int -> String -> IO ()
                                 sendAndGetSuccess :: Maybe Int -> String -> IO ()
sendAndGetSuccess Maybe Int
mbTimeOut String
l
                                   -- The pathetic case when the solver doesn't support queries, so we pretend it responded "success"
                                   -- Currently ABC is the only such solver.
                                   | Bool -> Bool
not (SolverCapabilities -> Bool
supportsCustomQueries (SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)))
                                   = do Maybe Int -> String -> IO ()
send Maybe Int
mbTimeOut String
l
                                        SMTConfig -> [String] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
debug SMTConfig
cfg [String
"[ISSUE] " String -> ShowS
`alignPlain` String
l]
                                   | Bool
True
                                   = do String
r <- Maybe Int -> String -> IO String
ask Maybe Int
mbTimeOut String
l
                                        case String -> [String]
words String
r of
                                          [String
"success"] -> SMTConfig -> [String] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
debug SMTConfig
cfg [String
"[GOOD] " String -> ShowS
`alignPlain` String
l]
                                          [String]
_           -> do SMTConfig -> [String] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
debug SMTConfig
cfg [String
"[FAIL] " String -> ShowS
`alignPlain` String
l]

                                                            let isOption :: Bool
isOption = String
"(set-option" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace String
l

                                                                reason :: [String]
reason | Bool
isOption = [ String
"Backend solver reports it does not support this option."
                                                                                    , String
"Check the spelling, and if correct please report this as a"
                                                                                    , String
"bug/feature request with the solver!"
                                                                                    ]
                                                                       | Bool
True     = [ String
"Check solver response for further information. If your code is correct,"
                                                                                    , String
"please report this as an issue either with SBV or the solver itself!"
                                                                                    ]

                                                            -- put a sync point here before we die so we consume everything
                                                            Either String String
mbExtras <- (String -> Either String String
forall a b. b -> Either a b
Right (String -> Either String String)
-> IO String -> IO (Either String String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe String -> Maybe Int -> IO String
getResponseFromSolver Maybe String
forall a. Maybe a
Nothing (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
5000000))
                                                                        IO (Either String String)
-> (SomeException -> IO (Either String String))
-> IO (Either String String)
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch` (\(SomeException
e :: C.SomeException) -> SomeException
-> IO (Either String String) -> IO (Either String String)
forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (Either String String -> IO (Either String String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Either String String
forall a b. a -> Either a b
Left (SomeException -> String
forall a. Show a => a -> String
show SomeException
e))))

                                                            -- Ignore any exceptions from last sync, pointless.
                                                            let extras :: String
extras = case Either String String
mbExtras of
                                                                           Left String
_   -> []
                                                                           Right String
xs -> String
xs

                                                            (String
outOrig, String
errOrig, ExitCode
ex) <- IO (String, String, ExitCode)
terminateSolver
                                                            let out :: String
out = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> (String -> [String]) -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
outOrig
                                                                err :: String
err = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> (String -> [String]) -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
lines ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
errOrig

                                                                exc :: SBVException
exc = SBVException :: String
-> Maybe String
-> Maybe String
-> Maybe String
-> Maybe String
-> Maybe String
-> Maybe ExitCode
-> SMTConfig
-> Maybe [String]
-> Maybe [String]
-> SBVException
SBVException { sbvExceptionDescription :: String
sbvExceptionDescription = String
"Unexpected non-success response from " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
nm
                                                                                   , sbvExceptionSent :: Maybe String
sbvExceptionSent        = String -> Maybe String
forall a. a -> Maybe a
Just String
l
                                                                                   , sbvExceptionExpected :: Maybe String
sbvExceptionExpected    = String -> Maybe String
forall a. a -> Maybe a
Just String
"success"
                                                                                   , sbvExceptionReceived :: Maybe String
sbvExceptionReceived    = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
r String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
extras
                                                                                   , sbvExceptionStdOut :: Maybe String
sbvExceptionStdOut      = String -> Maybe String
forall a. a -> Maybe a
Just String
out
                                                                                   , sbvExceptionStdErr :: Maybe String
sbvExceptionStdErr      = String -> Maybe String
forall a. a -> Maybe a
Just String
err
                                                                                   , sbvExceptionExitCode :: Maybe ExitCode
sbvExceptionExitCode    = ExitCode -> Maybe ExitCode
forall a. a -> Maybe a
Just ExitCode
ex
                                                                                   , sbvExceptionConfig :: SMTConfig
sbvExceptionConfig      = SMTConfig
cfg { solver :: SMTSolver
solver = (SMTConfig -> SMTSolver
solver SMTConfig
cfg) {executable :: String
executable = String
execPath } }
                                                                                   , sbvExceptionReason :: Maybe [String]
sbvExceptionReason      = [String] -> Maybe [String]
forall a. a -> Maybe a
Just [String]
reason
                                                                                   , sbvExceptionHint :: Maybe [String]
sbvExceptionHint        = Maybe [String]
forall a. Maybe a
Nothing
                                                                                   }

                                                            SBVException -> IO ()
forall e a. Exception e => e -> IO a
C.throwIO SBVException
exc

                             -- Mark in the log, mostly.
                             Maybe Int -> String -> IO ()
sendAndGetSuccess Maybe Int
forall a. Maybe a
Nothing String
"; Automatically generated by SBV. Do not edit."

                             -- First check that the solver supports :print-success
                             let backend :: Solver
backend = SMTSolver -> Solver
name (SMTSolver -> Solver) -> SMTSolver -> Solver
forall a b. (a -> b) -> a -> b
$ SMTConfig -> SMTSolver
solver SMTConfig
cfg
                             if Bool -> Bool
not (SolverCapabilities -> Bool
supportsCustomQueries (SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)))
                                then SMTConfig -> [String] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
debug SMTConfig
cfg [String
"** Skipping heart-beat for the solver " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Solver -> String
forall a. Show a => a -> String
show Solver
backend]
                                else do let heartbeat :: String
heartbeat = String
"(set-option :print-success true)"
                                        String
r <- Maybe Int -> String -> IO String
ask (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
5000000) String
heartbeat  -- Give the solver 5s to respond, this should be plenty enough!
                                        case String -> [String]
words String
r of
                                          [String
"success"]     -> SMTConfig -> [String] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
debug SMTConfig
cfg [String
"[GOOD] " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
heartbeat]
                                          [String
"unsupported"] -> String -> IO ()
forall a. HasCallStack => String -> a
error (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                                             , String
"*** Backend solver (" String -> ShowS
forall a. [a] -> [a] -> [a]
++  Solver -> String
forall a. Show a => a -> String
show Solver
backend String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
") does not support the command:"
                                                                             , String
"***"
                                                                             , String
"***     (set-option :print-success true)"
                                                                             , String
"***"
                                                                             , String
"*** SBV relies on this feature to coordinate communication!"
                                                                             , String
"*** Please request this as a feature!"
                                                                             ]
                                          [String]
_               -> String -> IO ()
forall a. HasCallStack => String -> a
error (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                                             , String
"*** Data.SBV: Failed to initiate contact with the solver!"
                                                                             , String
"***"
                                                                             , String
"***   Sent    : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
heartbeat
                                                                             , String
"***   Expected: success"
                                                                             , String
"***   Received: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
r
                                                                             , String
"***"
                                                                             , String
"*** Try running in debug mode for further information."
                                                                             ]

                             -- For push/pop support, we require :global-declarations to be true. But not all solvers
                             -- support this. Issue it if supported. (If not, we'll reject pop calls.)
                             if Bool -> Bool
not (SolverCapabilities -> Bool
supportsGlobalDecls (SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)))
                                then SMTConfig -> [String] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
debug SMTConfig
cfg [ String
"** Backend solver " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Solver -> String
forall a. Show a => a -> String
show Solver
backend String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" does not support global decls."
                                               , String
"** Some incremental calls, such as pop, will be limited."
                                               ]
                                else Maybe Int -> String -> IO ()
sendAndGetSuccess Maybe Int
forall a. Maybe a
Nothing String
"(set-option :global-declarations true)"

                             -- Now dump the program!
                             (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Maybe Int -> String -> IO ()
sendAndGetSuccess Maybe Int
forall a. Maybe a
Nothing) ([String] -> [String]
mergeSExpr (String -> [String]
lines String
pgm))

                             -- Prepare the query context and ship it off
                             let qs :: QueryState
qs = QueryState :: (Maybe Int -> String -> IO String)
-> (Maybe Int -> String -> IO ())
-> (Maybe Int -> IO String)
-> SMTConfig
-> IO ()
-> Maybe Int
-> Int
-> QueryState
QueryState { queryAsk :: Maybe Int -> String -> IO String
queryAsk                 = Maybe Int -> String -> IO String
ask
                                                 , querySend :: Maybe Int -> String -> IO ()
querySend                = Maybe Int -> String -> IO ()
send
                                                 , queryRetrieveResponse :: Maybe Int -> IO String
queryRetrieveResponse    = Maybe String -> Maybe Int -> IO String
getResponseFromSolver Maybe String
forall a. Maybe a
Nothing
                                                 , queryConfig :: SMTConfig
queryConfig              = SMTConfig
cfg
                                                 , queryTerminate :: IO ()
queryTerminate           = IO ()
cleanUp
                                                 , queryTimeOutValue :: Maybe Int
queryTimeOutValue        = Maybe Int
forall a. Maybe a
Nothing
                                                 , queryAssertionStackDepth :: Int
queryAssertionStackDepth = Int
0
                                                 }
                                 qsp :: IORef (Maybe QueryState)
qsp = State -> IORef (Maybe QueryState)
rQueryState State
ctx

                             Maybe QueryState
mbQS <- IORef (Maybe QueryState) -> IO (Maybe QueryState)
forall a. IORef a -> IO a
readIORef IORef (Maybe QueryState)
qsp

                             case Maybe QueryState
mbQS of
                               Maybe QueryState
Nothing -> IORef (Maybe QueryState) -> Maybe QueryState -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (Maybe QueryState)
qsp (QueryState -> Maybe QueryState
forall a. a -> Maybe a
Just QueryState
qs)
                               Just QueryState
_  -> String -> IO ()
forall a. HasCallStack => String -> a
error (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                          , String
"Data.SBV: Impossible happened, query-state was already set."
                                                          , String
"Please report this as a bug!"
                                                          ]

                             -- off we go!
                             State -> IO a
continuation State
ctx

      -- NB. Don't use 'bracket' here, as it wouldn't have access to the exception.
      let launchSolver :: IO a
launchSolver = do Maybe String -> SMTConfig -> IO ()
startTranscript (SMTConfig -> Maybe String
transcript SMTConfig
cfg) SMTConfig
cfg
                            IO a
executeSolver

      IO a
launchSolver IO a -> (SomeException -> IO a) -> IO a
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch` (\(SomeException
e :: C.SomeException) -> SomeException -> IO a -> IO a
forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (IO a -> IO a) -> IO a -> IO a
forall a b. (a -> b) -> a -> b
$ do ProcessHandle -> IO ()
terminateProcess ProcessHandle
pid
                                                                            ExitCode
ec <- ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
pid
                                                                            Maybe String -> String -> IO ()
recordException    (SMTConfig -> Maybe String
transcript SMTConfig
cfg) (SomeException -> String
forall a. Show a => a -> String
show SomeException
e)
                                                                            Maybe String -> ExitCode -> IO ()
finalizeTranscript (SMTConfig -> Maybe String
transcript SMTConfig
cfg) ExitCode
ec
                                                                            SMTConfig -> State -> IO ()
recordEndTime SMTConfig
cfg State
ctx
                                                                            SomeException -> IO a
forall e a. Exception e => e -> IO a
C.throwIO SomeException
e)

-- | Compute and report the end time
recordEndTime :: SMTConfig -> State -> IO ()
recordEndTime :: SMTConfig -> State -> IO ()
recordEndTime SMTConfig{Timing
timing :: SMTConfig -> Timing
timing :: Timing
timing} State
state = case Timing
timing of
                                           Timing
NoTiming        -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                           Timing
PrintTiming     -> do NominalDiffTime
e <- IO NominalDiffTime
elapsed
                                                                 String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"*** SBV: Elapsed time: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NominalDiffTime -> String
showTDiff NominalDiffTime
e
                                           SaveTiming IORef NominalDiffTime
here -> IORef NominalDiffTime -> NominalDiffTime -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef NominalDiffTime
here (NominalDiffTime -> IO ()) -> IO NominalDiffTime -> IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< IO NominalDiffTime
elapsed
  where elapsed :: IO NominalDiffTime
elapsed = IO UTCTime
getCurrentTime IO UTCTime -> (UTCTime -> IO NominalDiffTime) -> IO NominalDiffTime
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \UTCTime
end -> NominalDiffTime -> IO NominalDiffTime
forall (m :: * -> *) a. Monad m => a -> m a
return (NominalDiffTime -> IO NominalDiffTime)
-> NominalDiffTime -> IO NominalDiffTime
forall a b. (a -> b) -> a -> b
$ UTCTime -> UTCTime -> NominalDiffTime
diffUTCTime UTCTime
end (State -> UTCTime
startTime State
state)

-- | Start a transcript file, if requested.
startTranscript :: Maybe FilePath -> SMTConfig -> IO ()
startTranscript :: Maybe String -> SMTConfig -> IO ()
startTranscript Maybe String
Nothing  SMTConfig
_   = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
startTranscript (Just String
f) SMTConfig
cfg = do String
ts <- ZonedTime -> String
forall a. Show a => a -> String
show (ZonedTime -> String) -> IO ZonedTime -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO ZonedTime
getZonedTime
                                  Maybe String
mbExecPath <- String -> IO (Maybe String)
findExecutable (SMTSolver -> String
executable (SMTConfig -> SMTSolver
solver SMTConfig
cfg))
                                  String -> String -> IO ()
writeFile String
f (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> Maybe String -> String
start String
ts Maybe String
mbExecPath
  where SMTSolver{Solver
name :: Solver
name :: SMTSolver -> Solver
name, SMTConfig -> [String]
options :: SMTConfig -> [String]
options :: SMTSolver -> SMTConfig -> [String]
options} = SMTConfig -> SMTSolver
solver SMTConfig
cfg
        start :: String -> Maybe String -> String
start String
ts Maybe String
mbPath = [String] -> String
unlines [ String
";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                                  , String
";;; SBV: Starting at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ts
                                  , String
";;;"
                                  , String
";;;           Solver    : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Solver -> String
forall a. Show a => a -> String
show Solver
name
                                  , String
";;;           Executable: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
"Unable to locate the executable" Maybe String
mbPath
                                  , String
";;;           Options   : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (SMTConfig -> [String]
options SMTConfig
cfg [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ SMTConfig -> [String]
extraArgs SMTConfig
cfg)
                                  , String
";;;"
                                  , String
";;; This file is an auto-generated loadable SMT-Lib file."
                                  , String
";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                                  , String
""
                                  ]

-- | Finish up the transcript file.
finalizeTranscript :: Maybe FilePath -> ExitCode -> IO ()
finalizeTranscript :: Maybe String -> ExitCode -> IO ()
finalizeTranscript Maybe String
Nothing  ExitCode
_  = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
finalizeTranscript (Just String
f) ExitCode
ec = do String
ts <- ZonedTime -> String
forall a. Show a => a -> String
show (ZonedTime -> String) -> IO ZonedTime -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO ZonedTime
getZonedTime
                                    String -> String -> IO ()
appendFile String
f (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ ShowS
end String
ts
  where end :: ShowS
end String
ts = [String] -> String
unlines [ String
""
                         , String
";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                         , String
";;;"
                         , String
";;; SBV: Finished at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ts
                         , String
";;;"
                         , String
";;; Exit code: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ExitCode -> String
forall a. Show a => a -> String
show ExitCode
ec
                         , String
";;;"
                         , String
";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                         ]

-- If requested, record in the transcript file
recordTranscript :: Maybe FilePath -> Either (String, Maybe Int) String -> IO ()
recordTranscript :: Maybe String -> Either (String, Maybe Int) String -> IO ()
recordTranscript Maybe String
Nothing  Either (String, Maybe Int) String
_ = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
recordTranscript (Just String
f) Either (String, Maybe Int) String
m = do String
tsPre <- TimeLocale -> String -> ZonedTime -> String
forall t. FormatTime t => TimeLocale -> String -> t -> String
formatTime TimeLocale
defaultTimeLocale String
"; [%T%Q" (ZonedTime -> String) -> IO ZonedTime -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO ZonedTime
getZonedTime
                                 let ts :: String
ts = Int -> ShowS
forall a. Int -> [a] -> [a]
take Int
15 ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
tsPre String -> ShowS
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. a -> [a]
repeat Char
'0'
                                 case Either (String, Maybe Int) String
m of
                                   Left  (String
sent, Maybe Int
mbTimeOut) -> String -> String -> IO ()
appendFile String
f (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (String
ts String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"] " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe Int -> String
to Maybe Int
mbTimeOut String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"Sending:") String -> [String] -> [String]
forall a. a -> [a] -> [a]
: String -> [String]
lines String
sent
                                   Right String
recv              -> String -> String -> IO ()
appendFile String
f (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ case String -> [String]
lines ((Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace String
recv) of
                                                                                        []  -> [String
ts String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"] Received: <NO RESPONSE>"]  -- can't really happen.
                                                                                        [String
x] -> [String
ts String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"] Received: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x]
                                                                                        [String]
xs  -> (String
ts String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"] Received: ") String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
";   " String -> ShowS
forall a. [a] -> [a] -> [a]
++) [String]
xs
        where to :: Maybe Int -> String
to Maybe Int
Nothing  = String
""
              to (Just Int
i) = String
"[Timeout: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
showTimeoutValue Int
i String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"] "
{-# INLINE recordTranscript #-}

-- Record the exception
recordException :: Maybe FilePath -> String -> IO ()
recordException :: Maybe String -> String -> IO ()
recordException Maybe String
Nothing  String
_ = () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
recordException (Just String
f) String
m = do String
ts <- ZonedTime -> String
forall a. Show a => a -> String
show (ZonedTime -> String) -> IO ZonedTime -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO ZonedTime
getZonedTime
                                String -> String -> IO ()
appendFile String
f (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ ShowS
exc String
ts
  where exc :: ShowS
exc String
ts = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [ String
""
                           , String
";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                           , String
";;;"
                           , String
";;; SBV: Caught an exception at " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ts
                           , String
";;;"
                           ]
                        [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
";;;   " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
l | String
l <- (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
dropWhile String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (String -> [String]
lines String
m) ]
                        [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
";;;"
                           , String
";;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;"
                           ]

-- We should not be catching/processing asynchronous exceptions.
-- See http://github.com/LeventErkok/sbv/issues/410
handleAsync :: C.SomeException -> IO a -> IO a
handleAsync :: SomeException -> IO a -> IO a
handleAsync SomeException
e IO a
cont
  | Bool
isAsynchronous = SomeException -> IO a
forall e a. Exception e => e -> IO a
C.throwIO SomeException
e
  | Bool
True           = IO a
cont
  where -- Stealing this definition from the asynchronous exceptions package to reduce dependencies
        isAsynchronous :: Bool
        isAsynchronous :: Bool
isAsynchronous = Maybe AsyncException -> Bool
forall a. Maybe a -> Bool
isJust (SomeException -> Maybe AsyncException
forall e. Exception e => SomeException -> Maybe e
C.fromException SomeException
e :: Maybe C.AsyncException) Bool -> Bool -> Bool
|| Maybe SomeAsyncException -> Bool
forall a. Maybe a -> Bool
isJust (SomeException -> Maybe SomeAsyncException
forall e. Exception e => SomeException -> Maybe e
C.fromException SomeException
e :: Maybe C.SomeAsyncException)