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

{-# LANGUAGE DefaultSignatures          #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NamedFieldPuns             #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE Rank2Types                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# 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, mplus)
import Data.Char          (isSpace)
import Data.Maybe         (isJust)
import Data.Int           (Int8, Int16, Int32, Int64)
import Data.List          (intercalate, isPrefixOf, transpose, isInfixOf)
import Data.Word          (Word8, Word16, Word32, Word64)

import GHC.TypeLits
import Data.Proxy

import Data.IORef (readIORef, writeIORef)

import Data.Either (rights)

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

import qualified Data.Map.Strict as M
import qualified Data.Text       as T
import Text.Read (readMaybe)

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

import Data.SBV.Core.SizedFloats(FloatingPoint(..))

import Data.SBV.SMT.Utils     ( showTimeoutValue, alignPlain, debug, mergeSExpr, SBVException(..)
                              , startTranscript, recordTranscript, finalizeTranscript, recordEndTime, recordException, TranscriptMsg(..)
                              )

import Data.SBV.Utils.PrettyNum
import Data.SBV.Utils.Lib       (joinArgs, splitArgs, needsBars)
import Data.SBV.Utils.SExpr     (parenDeficit, nameSupply)

import qualified System.Timeout as Timeout (timeout)

import Numeric

import qualified Data.SBV.Utils.CrackNum as CN

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

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

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

-- | An 'Data.SBV.allSat' call results in a t'AllSatResult'
data AllSatResult = AllSatResult { AllSatResult -> Bool
allSatMaxModelCountReached  :: Bool          -- ^ Did we reach the user given model count limit?
                                 , 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 t'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 [Char] -> [Char]
getPrecision SMTResult
r Maybe [Char]
queriedPrecision = case (Maybe [Char]
queriedPrecision, SMTConfig -> Maybe Double
dsatPrecision (SMTResult -> SMTConfig
resultConfig SMTResult
r)) of
                                   (Just [Char]
s, Maybe Double
_     ) -> [Char]
s
                                   (Maybe [Char]
_,      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 [Char]
""
                                   (Maybe [Char], Maybe Double)
_                -> [Char]
"tool default"

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

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

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

-- The Show instance of AllSatResults.
instance Show AllSatResult where
  show :: AllSatResult -> [Char]
show AllSatResult { allSatMaxModelCountReached :: AllSatResult -> Bool
allSatMaxModelCountReached  = Bool
l
                    , allSatSolverReturnedUnknown :: AllSatResult -> Bool
allSatSolverReturnedUnknown = Bool
u
                    , allSatSolverReturnedDSat :: AllSatResult -> Bool
allSatSolverReturnedDSat    = Bool
d
                    , allSatResults :: AllSatResult -> [SMTResult]
allSatResults               = [SMTResult]
xs
                    } = Int -> [SMTResult] -> [Char]
forall {a}. (Eq a, Num a, Show a) => a -> [SMTResult] -> [Char]
go (Int
0::Int) [SMTResult]
xs
    where warnings :: [Char]
warnings | Bool
u    = [Char]
" (Search stopped since solver has returned unknown.)"
                   | Bool
True = [Char]
""

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

          sh :: a -> SMTResult -> (Bool, [Char])
sh a
i SMTResult
c = (Bool
ok, [Char]
-> [Char]
-> [Char]
-> [Char]
-> (Maybe [Char] -> [Char])
-> [Char]
-> SMTResult
-> [Char]
showSMTResult [Char]
"Unsatisfiable"
                                      [Char]
"Unknown"
                                      ([Char]
"Solution #" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
i [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
":\nSatisfiable") ([Char]
"Solution #" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
i [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
":\n")
                                      (\Maybe [Char]
mbP -> [Char]
"Solution $" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
i [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" with delta-satisfiability, precision: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SMTResult -> Maybe [Char] -> [Char]
getPrecision SMTResult
c Maybe [Char]
mbP [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
":\n")
                                      ([Char]
"Solution $" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
i [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" 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 -> [Char]
show OptimizeResult
res = case OptimizeResult
res of
               LexicographicResult SMTResult
r   -> ShowS -> SMTResult -> [Char]
forall {t}. IsString t => (t -> [Char]) -> SMTResult -> [Char]
sh ShowS
forall a. a -> a
id SMTResult
r

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

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

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

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

             sh :: (t -> [Char]) -> SMTResult -> [Char]
sh t -> [Char]
tag SMTResult
r = [Char]
-> [Char]
-> [Char]
-> [Char]
-> (Maybe [Char] -> [Char])
-> [Char]
-> SMTResult
-> [Char]
showSMTResult (t -> [Char]
tag t
"Unsatisfiable.")
                                      (t -> [Char]
tag t
"Unknown.")
                                      (t -> [Char]
tag t
"Optimal with no assignments.")
                                      (t -> [Char]
tag t
"Optimal model:" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n")
                                      (\Maybe [Char]
mbP -> t -> [Char]
tag t
"Optimal model with delta-satisfiability, precision: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SMTResult -> Maybe [Char] -> [Char]
getPrecision SMTResult
r Maybe [Char]
mbP [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
":" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n")
                                      (t -> [Char]
tag t
"Optimal in an extension field:" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\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 a b. Maybe a -> (a -> Maybe b) -> Maybe b
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 a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \b
b -> (b, [CV]) -> Maybe (b, [CV])
forall a. a -> Maybe a
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
_, [Char]
s)) : [CV]
r) = (a, [CV]) -> Maybe (a, [CV])
forall a. a -> Maybe a
Just ([Char] -> a
forall a. Read a => [Char] -> a
read [Char]
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 :: forall a. Integral a => 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 a. a -> Maybe a
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 (x, r) <- Kind -> [CV] -> Maybe (Integer, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse Kind
KBool [CV]
xs
                   return ((x :: Integer) /= 0, 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

-- | A general floating-point extracted from a model
instance (KnownNat eb, KnownNat sb) => SatModel (FloatingPoint eb sb) where
  parseCVs :: [CV] -> Maybe (FloatingPoint eb sb, [CV])
parseCVs (CV (KFP Int
ei Int
si) (CFP FP
fp) : [CV]
r)
    | Proxy eb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @eb) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ei , Proxy sb -> Int
forall (n :: Nat). KnownNat n => Proxy n -> Int
intOfProxy (forall (t :: Nat). Proxy t
forall {k} (t :: k). Proxy t
Proxy @sb) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
si = (FloatingPoint eb sb, [CV]) -> Maybe (FloatingPoint eb sb, [CV])
forall a. a -> Maybe a
Just (FP -> FloatingPoint eb sb
forall (eb :: Nat) (sb :: Nat). FP -> FloatingPoint eb sb
FloatingPoint FP
fp, [CV]
r)
  parseCVs [CV]
_                                                      = Maybe (FloatingPoint eb sb, [CV])
forall a. Maybe a
Nothing

-- | Constructing models for 'WordN'
instance (KnownNat n, BVIsNonZero n) => SatModel (WordN n) where
  parseCVs :: [CV] -> Maybe (WordN n, [CV])
parseCVs = Kind -> [CV] -> Maybe (WordN n, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (WordN n -> Kind
forall a. HasKind a => a -> Kind
kindOf (WordN n
forall a. HasCallStack => a
undefined :: WordN n))

-- | Constructing models for 'IntN'
instance (KnownNat n, BVIsNonZero n) => SatModel (IntN n) where
  parseCVs :: [CV] -> Maybe (IntN n, [CV])
parseCVs = Kind -> [CV] -> Maybe (IntN n, [CV])
forall a. Integral a => Kind -> [CV] -> Maybe (a, [CV])
genParse (IntN n -> Kind
forall a. HasKind a => a -> Kind
kindOf (IntN n
forall a. HasCallStack => a
undefined :: IntN n))

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

-- | 'String' as extracted from a model
instance {-# OVERLAPS #-} SatModel [Char] where
  parseCVs :: [CV] -> Maybe ([Char], [CV])
parseCVs (CV Kind
_ (CString [Char]
c):[CV]
r) = ([Char], [CV]) -> Maybe ([Char], [CV])
forall a. a -> Maybe a
Just ([Char]
c, [CV]
r)
  parseCVs [CV]
_                    = Maybe ([Char], [CV])
forall a. Maybe a
Nothing

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

-- | 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 {-# OVERLAPPABLE #-} 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, bs) <- [CV] -> Maybe (a, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
as
                   (b, cs) <- parseCVs bs
                   return ((a, b), 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,      bs) <- [CV] -> Maybe (a, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
as
                   ((b, c), ds) <- parseCVs bs
                   return ((a, b, c), 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,         bs) <- [CV] -> Maybe (a, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
as
                   ((b, c, d), es) <- parseCVs bs
                   return ((a, b, c, d), 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, bs)            <- [CV] -> Maybe (a, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
as
                   ((b, c, d, e), fs) <- parseCVs bs
                   return ((a, b, c, d, e), 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, bs)               <- [CV] -> Maybe (a, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
as
                   ((b, c, d, e, f), gs) <- parseCVs bs
                   return ((a, b, c, d, e, f), 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, bs)                  <- [CV] -> Maybe (a, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV]
as
                   ((b, c, d, e, f, g), hs) <- parseCVs bs
                   return ((a, b, c, d, e, f, g), 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 [Char]
v a
r = CV -> b
forall a. SymVal a => CV -> a
fromCV (CV -> b) -> Maybe CV -> Maybe b
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
`fmap` ([Char]
v [Char] -> Map [Char] CV -> Maybe CV
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` a -> Map [Char] CV
forall a. Modelable a => a -> Map [Char] 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 [Char]
v a
r = case [Char]
v [Char] -> Map [Char] CV -> Maybe CV
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` a -> Map [Char] CV
forall a. Modelable a => a -> Map [Char] CV
getModelDictionary a
r of
                                     Just (CV Kind
_ (CUserSort (Maybe Int
_, [Char]
s))) -> [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
s
                                     Maybe CV
_                              -> Maybe [Char]
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 [Char] (Bool, b)
forall a b.
(Modelable a, SatModel b) =>
a -> Either [Char] (Bool, b)
forall b. SatModel b => a -> Either [Char] (Bool, b)
getModelAssignment a
a of
                     Right (Bool
_, b
b) -> b -> Maybe b
forall a. a -> Maybe a
Just b
b
                     Either [Char] (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 [Char]
v a
r = [Char]
v [Char] -> Map [Char] GeneralizedCV -> Maybe GeneralizedCV
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` a -> Map [Char] GeneralizedCV
forall a. Modelable a => a -> Map [Char] GeneralizedCV
getModelObjectives a
r

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

  -- | Extract the value of an uninterpreted-function as an association list
  getModelUIFunValue :: String -> a -> Maybe (Bool, SBVType, Either String ([([CV], CV)], CV))
  getModelUIFunValue [Char]
v a
r = [Char]
v [Char]
-> Map [Char] (Bool, SBVType, Either [Char] ([([CV], CV)], CV))
-> Maybe (Bool, SBVType, Either [Char] ([([CV], CV)], CV))
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` a -> Map [Char] (Bool, SBVType, Either [Char] ([([CV], CV)], CV))
forall a.
Modelable a =>
a -> Map [Char] (Bool, SBVType, Either [Char] ([([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 :: forall a. SatModel a => AllSatResult -> [a]
extractModels AllSatResult{allSatResults :: AllSatResult -> [SMTResult]
allSatResults = [SMTResult]
xs} = [a
ms | Right (Bool
_, a
ms) <- (SMTResult -> Either [Char] (Bool, a))
-> [SMTResult] -> [Either [Char] (Bool, a)]
forall a b. (a -> b) -> [a] -> [b]
map SMTResult -> Either [Char] (Bool, a)
forall a b.
(Modelable a, SatModel b) =>
a -> Either [Char] (Bool, b)
forall b. SatModel b => SMTResult -> Either [Char] (Bool, b)
getModelAssignment [SMTResult]
xs]

-- | Get dictionaries from an all-sat call. Similar to `getModelDictionary`.
getModelDictionaries :: AllSatResult -> [M.Map String CV]
getModelDictionaries :: AllSatResult -> [Map [Char] CV]
getModelDictionaries AllSatResult{allSatResults :: AllSatResult -> [SMTResult]
allSatResults = [SMTResult]
xs} = (SMTResult -> Map [Char] CV) -> [SMTResult] -> [Map [Char] CV]
forall a b. (a -> b) -> [a] -> [b]
map SMTResult -> Map [Char] CV
forall a. Modelable a => a -> Map [Char] 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 :: forall b. SymVal b => [Char] -> AllSatResult -> [Maybe b]
getModelValues [Char]
s AllSatResult{allSatResults :: AllSatResult -> [SMTResult]
allSatResults = [SMTResult]
xs} =  (SMTResult -> Maybe b) -> [SMTResult] -> [Maybe b]
forall a b. (a -> b) -> [a] -> [b]
map ([Char]
s [Char] -> SMTResult -> Maybe b
forall b. SymVal b => [Char] -> SMTResult -> Maybe b
forall a b. (Modelable a, SymVal b) => [Char] -> 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 :: [Char] -> AllSatResult -> [Maybe [Char]]
getModelUninterpretedValues [Char]
s AllSatResult{allSatResults :: AllSatResult -> [SMTResult]
allSatResults = [SMTResult]
xs} =  (SMTResult -> Maybe [Char]) -> [SMTResult] -> [Maybe [Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char]
s [Char] -> SMTResult -> Maybe [Char]
forall a. Modelable a => [Char] -> a -> Maybe [Char]
`getModelUninterpretedValue`) [SMTResult]
xs

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

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

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

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

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

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

  getModelUIFuns :: SMTResult
-> Map [Char] (Bool, SBVType, Either [Char] ([([CV], CV)], CV))
getModelUIFuns Unsatisfiable{}     = Map [Char] (Bool, SBVType, Either [Char] ([([CV], CV)], CV))
forall k a. Map k a
M.empty
  getModelUIFuns (Satisfiable SMTConfig
_ SMTModel
m  ) = [([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))]
-> Map [Char] (Bool, SBVType, Either [Char] ([([CV], CV)], CV))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel
-> [([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))]
modelUIFuns SMTModel
m)
  getModelUIFuns (DeltaSat    SMTConfig
_ Maybe [Char]
_ SMTModel
m) = [([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))]
-> Map [Char] (Bool, SBVType, Either [Char] ([([CV], CV)], CV))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel
-> [([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))]
modelUIFuns SMTModel
m)
  getModelUIFuns (SatExtField SMTConfig
_ SMTModel
m  ) = [([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))]
-> Map [Char] (Bool, SBVType, Either [Char] ([([CV], CV)], CV))
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList (SMTModel
-> [([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))]
modelUIFuns SMTModel
m)
  getModelUIFuns Unknown{}           = Map [Char] (Bool, SBVType, Either [Char] ([([CV], CV)], CV))
forall k a. Map k a
M.empty
  getModelUIFuns ProofError{}        = Map [Char] (Bool, SBVType, Either [Char] ([([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 :: forall a. SatModel a => SMTModel -> a
parseModelOut SMTModel
m = case [CV] -> Maybe (a, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV
c | ([Char]
_, CV
c) <- SMTModel -> [([Char], CV)]
modelAssocs SMTModel
m] of
                   Just (a
x, []) -> a
x
                   Just (a
_, [CV]
ys) -> [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ [Char]
"SBV.parseModelOut: Partially constructed model; remaining elements: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [CV] -> [Char]
forall a. Show a => a -> [Char]
show [CV]
ys
                   Maybe (a, [CV])
Nothing      -> [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char] -> a) -> [Char] -> a
forall a b. (a -> b) -> a -> b
$ [Char]
"SBV.parseModelOut: Cannot construct a model from: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SMTModel -> [Char]
forall a. Show a => a -> [Char]
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 :: forall a.
SatModel a =>
([(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 = [Either [Char] (Bool, a)] -> [(Bool, a)]
forall a b. [Either a b] -> [b]
rights ((SMTResult -> Either [Char] (Bool, a))
-> [SMTResult] -> [Either [Char] (Bool, a)]
forall a b. (a -> b) -> [a] -> [b]
map (SatResult -> Either [Char] (Bool, a)
forall a b.
(Modelable a, SatModel b) =>
a -> Either [Char] (Bool, b)
forall b. SatModel b => SatResult -> Either [Char] (Bool, b)
getModelAssignment (SatResult -> Either [Char] (Bool, a))
-> (SMTResult -> SatResult) -> SMTResult -> Either [Char] (Bool, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTResult -> SatResult
SatResult) [SMTResult]
ms)
    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)..]
    return $ last (0: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 a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Int -> IO Int
forall a. a -> IO a
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 :: [Char]
-> [Char]
-> [Char]
-> [Char]
-> (Maybe [Char] -> [Char])
-> [Char]
-> SMTResult
-> [Char]
showSMTResult [Char]
unsatMsg [Char]
unkMsg [Char]
satMsg [Char]
satMsgModel Maybe [Char] -> [Char]
dSatMsgModel [Char]
satExtMsg SMTResult
result = case SMTResult
result of
  Unsatisfiable SMTConfig
_ Maybe [[Char]]
uc                 -> [Char]
unsatMsg [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Maybe [[Char]] -> [Char]
showUnsatCore Maybe [[Char]]
uc
  Satisfiable SMTConfig
_ (SMTModel [([Char], GeneralizedCV)]
_ Maybe [(NamedSymVar, CV)]
_ [] []) -> [Char]
satMsg
  Satisfiable SMTConfig
_   SMTModel
m                  -> [Char]
satMsgModel    [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SMTConfig -> SMTModel -> [Char]
showModel SMTConfig
cfg SMTModel
m
  DeltaSat    SMTConfig
_ Maybe [Char]
p SMTModel
m                  -> Maybe [Char] -> [Char]
dSatMsgModel Maybe [Char]
p [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SMTConfig -> SMTModel -> [Char]
showModel SMTConfig
cfg SMTModel
m
  SatExtField SMTConfig
_ (SMTModel [([Char], GeneralizedCV)]
b Maybe [(NamedSymVar, CV)]
_ [([Char], CV)]
_ [([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))]
_)   -> [Char]
satExtMsg   [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Bool -> Bool -> SMTConfig -> [([Char], GeneralizedCV)] -> [Char]
showModelDictionary Bool
True Bool
False SMTConfig
cfg [([Char], GeneralizedCV)]
b
  Unknown     SMTConfig
_ SMTReasonUnknown
r                    -> [Char]
unkMsg [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
".\n" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"  Reason: " [Char] -> ShowS
`alignPlain` SMTReasonUnknown -> [Char]
forall a. Show a => a -> [Char]
show SMTReasonUnknown
r
  ProofError  SMTConfig
_ [] Maybe SMTResult
Nothing           -> [Char]
"*** An error occurred. No additional information available. Try running in verbose mode."
  ProofError  SMTConfig
_ [[Char]]
ls Maybe SMTResult
Nothing           -> [Char]
"*** An error occurred.\n" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" (ShowS -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char]
"***  " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++) [[Char]]
ls)
  ProofError  SMTConfig
_ [[Char]]
ls (Just SMTResult
r)          -> [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$  [ [Char]
"*** " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
l | [Char]
l <- [[Char]]
ls]
                                                         [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [ [Char]
"***"
                                                            , [Char]
"*** Alleged model:"
                                                            , [Char]
"***"
                                                            ]
                                                         [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [[Char]
"*** "  [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
l | [Char]
l <- [Char] -> [[Char]]
lines ([Char]
-> [Char]
-> [Char]
-> [Char]
-> (Maybe [Char] -> [Char])
-> [Char]
-> SMTResult
-> [Char]
showSMTResult [Char]
unsatMsg [Char]
unkMsg [Char]
satMsg [Char]
satMsgModel Maybe [Char] -> [Char]
dSatMsgModel [Char]
satExtMsg SMTResult
r)]

 where cfg :: SMTConfig
cfg = SMTResult -> SMTConfig
resultConfig SMTResult
result
       showUnsatCore :: Maybe [[Char]] -> [Char]
showUnsatCore Maybe [[Char]]
Nothing   = [Char]
""
       showUnsatCore (Just [[Char]]
xs) = [Char]
". Unsat core:\n" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" [[Char]
"    " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
x | [Char]
x <- [[Char]]
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 -> [Char]
showModel SMTConfig
cfg SMTModel
model
   | [([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))]
-> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))]
uiFuncs
   = [Char]
nonUIFuncs
   | Bool
True
   = ShowS
sep [Char]
nonUIFuncs [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n\n" ((([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))
 -> [Char])
-> [([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))]
-> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (SMTConfig
-> ([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))
-> [Char]
showModelUI SMTConfig
cfg) [([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))]
uiFuncs)
   where nonUIFuncs :: [Char]
nonUIFuncs = Bool -> Bool -> SMTConfig -> [([Char], GeneralizedCV)] -> [Char]
showModelDictionary ([([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))]
-> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))]
uiFuncs) Bool
False SMTConfig
cfg [([Char]
n, CV -> GeneralizedCV
RegularCV CV
c) | ([Char]
n, CV
c) <- SMTModel -> [([Char], CV)]
modelAssocs SMTModel
model]
         uiFuncs :: [([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))]
uiFuncs    = SMTModel
-> [([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))]
modelUIFuns SMTModel
model
         sep :: ShowS
sep [Char]
""     = [Char]
""
         sep [Char]
x      = [Char]
x [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n\n"

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

        relevantVars :: [([Char], GeneralizedCV)]
relevantVars  = (([Char], GeneralizedCV) -> Bool)
-> [([Char], GeneralizedCV)] -> [([Char], GeneralizedCV)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (([Char], GeneralizedCV) -> Bool)
-> ([Char], GeneralizedCV)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Char], GeneralizedCV) -> Bool
forall {b}. ([Char], b) -> Bool
ignore) [([Char], GeneralizedCV)]
allVars
        ignore :: ([Char], b) -> Bool
ignore ([Char] -> Text
T.pack -> Text
s, b
_)
          | Bool
includeEverything = Bool
False
          | Bool
True              = SMTConfig -> [Char] -> Bool
mustIgnoreVar SMTConfig
cfg (Text -> [Char]
T.unpack Text
s)

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

        display :: [((Int, [Char]), (Int, [Char]))] -> [[Char]]
display [((Int, [Char]), (Int, [Char]))]
svs   = (((Int, [Char]), (Int, [Char])) -> [Char])
-> [((Int, [Char]), (Int, [Char]))] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ((Int, [Char]), (Int, [Char])) -> [Char]
forall {a} {a}. ((a, [Char]), (a, [Char])) -> [Char]
line [((Int, [Char]), (Int, [Char]))]
svs
           where line :: ((a, [Char]), (a, [Char])) -> [Char]
line ((a
_, [Char]
s), (a
_, [Char]
v)) = [Char]
"  " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> ShowS
right (Int
nameWidth Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
s) [Char]
s [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" = " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> ShowS
left (Int
valWidth Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Char] -> Int
lTrimRight (ShowS
valPart [Char]
v)) [Char]
v
                 nameWidth :: Int
nameWidth             = [Int] -> Int
forall a. Ord a => [a] -> a
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, [Char]
_), (Int, [Char])
_) <- [((Int, [Char]), (Int, [Char]))]
svs]
                 valWidth :: Int
valWidth              = [Int] -> Int
forall a. Ord a => [a] -> a
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, [Char])
_, (Int
l, [Char]
_)) <- [((Int, [Char]), (Int, [Char]))]
svs]

        right :: Int -> ShowS
right Int
p [Char]
s = [Char]
s [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> Char -> [Char]
forall a. Int -> a -> [a]
replicate Int
p Char
' '
        left :: Int -> ShowS
left  Int
p [Char]
s = Int -> Char -> [Char]
forall a. Int -> a -> [a]
replicate Int
p Char
' ' [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
s
        vlength :: [Char] -> Int
vlength [Char]
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') [Char]
s)) of
                      (Char
':':Char
':':[Char]
r) -> [Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ((Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace [Char]
r)
                      [Char]
_           -> [Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Char]
s -- conservative

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

        lTrimRight :: [Char] -> Int
lTrimRight = [Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Char] -> Int) -> ShowS -> [Char] -> 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, (Bool, SBVType, Either String ([([CV], CV)], CV))) -> String
showModelUI :: SMTConfig
-> ([Char], (Bool, SBVType, Either [Char] ([([CV], CV)], CV)))
-> [Char]
showModelUI SMTConfig
cfg ([Char]
nm, (Bool
isCurried, SBVType [Kind]
ts, Either [Char] ([([CV], CV)], CV)
interp))
  = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ case Either [Char] ([([CV], CV)], CV)
interp of
                         Left  [Char]
e  -> [[Char]
"  " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
trim [Char]
l | [Char]
l <- [[Char]
sig, [Char]
e]]
                         Right ([([CV], CV)], CV)
ds -> [[Char]
"  " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
trim [Char]
l | [Char]
l <- [Char]
sig [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: ([([CV], CV)], CV) -> [[Char]]
mkBody ([([CV], CV)], CV)
ds]
  where noOfArgs :: Int
noOfArgs = [Kind] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
ts Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1

        trim :: ShowS
trim = ShowS
forall a. [a] -> [a]
reverse ShowS -> ShowS -> ShowS
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

        ([[Char]]
ats, [Char]
rt) = case (Kind -> [Char]) -> [Kind] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Kind -> [Char]
showBaseKind [Kind]
ts of
                     []  -> [Char] -> ([[Char]], [Char])
forall a. HasCallStack => [Char] -> a
error ([Char] -> ([[Char]], [Char])) -> [Char] -> ([[Char]], [Char])
forall a b. (a -> b) -> a -> b
$ [Char]
"showModelUI: Unexpected type: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SBVType -> [Char]
forall a. Show a => a -> [Char]
show ([Kind] -> SBVType
SBVType [Kind]
ts)
                     [[Char]]
tss -> ([[Char]] -> [[Char]]
forall a. HasCallStack => [a] -> [a]
init [[Char]]
tss, [[Char]] -> [Char]
forall a. HasCallStack => [a] -> a
last [[Char]]
tss)

        -- signatures require parens if this is a non-ascii name, i.e., needs bars
        sigName :: [Char]
sigName | [Char] -> Bool
needsBars [Char]
nm = Char
'(' Char -> ShowS
forall a. a -> [a] -> [a]
: [Char]
nm [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")"
                | Bool
True         = [Char]
nm

        sig :: [Char]
sig | Bool
isCurried = [Char]
sigName [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" :: "  [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
" -> " [[Char]]
ats [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++  [Char]
" -> " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
rt
            | Bool
True      = [Char]
sigName [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" :: (" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", "   [[Char]]
ats [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
") -> " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
rt

        mkBody :: ([([CV], CV)], CV) -> [[Char]]
mkBody ([([CV], CV)]
defs, CV
dflt) = (([[Char]], [Char]) -> [Char]) -> [([[Char]], [Char])] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([[Char]], [Char]) -> [Char]
align [([[Char]], [Char])]
body
          where ls :: [([[Char]], [Char])]
ls       = (([CV], CV) -> ([[Char]], [Char]))
-> [([CV], CV)] -> [([[Char]], [Char])]
forall a b. (a -> b) -> [a] -> [b]
map ([CV], CV) -> ([[Char]], [Char])
line [([CV], CV)]
defs
                body :: [([[Char]], [Char])]
body     = [([[Char]], [Char])]
ls [([[Char]], [Char])]
-> [([[Char]], [Char])] -> [([[Char]], [Char])]
forall a. [a] -> [a] -> [a]
++ [([[Char]], [Char])
defLine]

                -- is the default an argument? This is likely to be z3 specific
                defVal :: [Char]
defVal = CV -> [Char]
scv CV
dflt
                defPos :: Maybe (Int, [Char])
defPos = case (Char -> Bool) -> [Char] -> ([Char], [Char])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'!') [Char]
defVal of
                           ([Char]
_, Char
'!':[Char]
n) | Just (Int
i :: Int) <- [Char] -> Maybe Int
forall a. Read a => [Char] -> Maybe a
readMaybe [Char]
n, Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 -> (Int, [Char]) -> Maybe (Int, [Char])
forall a. a -> Maybe a
Just (Int
i, [[Char]] -> [[Char]]
nameSupply [] [[Char]] -> Int -> [Char]
forall a. HasCallStack => [a] -> Int -> a
!! (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) -- default is the ith argument
                           ([Char], [Char])
_                                                  -> Maybe (Int, [Char])
forall a. Maybe a
Nothing                          -- default is a constant (or something else?)
                defLine :: ([[Char]], [Char])
defLine = case Maybe (Int, [Char])
defPos of
                            Just (Int
i, [Char]
a) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 -> (Int -> [Char] -> [[Char]]
forall a. Int -> a -> [a]
replicate (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [Char]
"_" [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [Char]
a [Char] -> [[Char]] -> [[Char]]
forall a. a -> [a] -> [a]
: Int -> [Char] -> [[Char]]
forall a. Int -> a -> [a]
replicate (Int
noOfArgs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i) [Char]
"_", [Char]
a)
                            Maybe (Int, [Char])
_                   -> (Int -> [Char] -> [[Char]]
forall a. Int -> a -> [a]
replicate Int
noOfArgs [Char]
"_",                                    [Char]
defVal)

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

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

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

                         merge :: [[Char]] -> [Char]
merge [[Char]]
as | Bool
isCurried = [[Char]] -> [Char]
unwords [[Char]]
as
                                  | Bool
True      = Char
'(' Char -> ShowS
forall a. a -> [a] -> [a]
: [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " [[Char]]
as [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")"

        -- NB. We'll ignore crackNum here. Seems to be overkill while displaying an
        -- uninterpreted function.
        scv :: CV -> [Char]
scv = Int -> CV -> [Char]
forall {a}. (Eq a, Num a) => a -> CV -> [Char]
sh (SMTConfig -> Int
printBase SMTConfig
cfg)
          where sh :: a -> CV -> [Char]
sh a
2  = CV -> [Char]
forall a. PrettyNum a => a -> [Char]
binP
                sh a
10 = Bool -> CV -> [Char]
showCV Bool
False
                sh a
16 = CV -> [Char]
forall a. PrettyNum a => a -> [Char]
hexP
                sh a
_  = CV -> [Char]
forall a. Show a => a -> [Char]
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) -> ([[Char]], [Char])
line ([CV]
args, CV
r) = ((CV -> [Char]) -> [CV] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> ShowS
paren Bool
isCurried ShowS -> (CV -> [Char]) -> CV -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> [Char]
scv) [CV]
args, CV -> [Char]
scv CV
r)
          where -- If negative and if we're curried, parenthesize. I think this is the only case
                -- we need to worry about. Hopefully!
                paren :: Bool -> String -> String
                paren :: Bool -> ShowS
paren Bool
True x :: [Char]
x@(Char
'-':[Char]
_) = Char
'(' Char -> ShowS
forall a. a -> [a] -> [a]
: [Char]
x [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")"
                paren Bool
_    [Char]
x         = [Char]
x

-- | Show a constant value, in the user-specified base
shCV :: SMTConfig -> String -> CV -> String
shCV :: SMTConfig -> [Char] -> CV -> [Char]
shCV SMTConfig{Int
printBase :: SMTConfig -> Int
printBase :: Int
printBase, Bool
crackNum :: Bool
crackNum :: SMTConfig -> Bool
crackNum, Bool
verbose :: Bool
verbose :: SMTConfig -> Bool
verbose, [([Char], Integer)]
crackNumSurfaceVals :: [([Char], Integer)]
crackNumSurfaceVals :: SMTConfig -> [([Char], Integer)]
crackNumSurfaceVals} [Char]
nm CV
cv = ShowS
cracked (Int -> CV -> [Char]
forall {a} {a}.
(Eq a, Num a, PrettyNum a, Show a, Show a) =>
a -> a -> [Char]
sh Int
printBase CV
cv)
  where sh :: a -> a -> [Char]
sh a
2  = a -> [Char]
forall a. PrettyNum a => a -> [Char]
binS
        sh a
10 = a -> [Char]
forall a. Show a => a -> [Char]
show
        sh a
16 = a -> [Char]
forall a. PrettyNum a => a -> [Char]
hexS
        sh a
n  = \a
w -> a -> [Char]
forall a. Show a => a -> [Char]
show a
w [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" -- Ignoring unsupported printBase " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> [Char]
forall a. Show a => a -> [Char]
show a
n [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
", use 2, 10, or 16."

        cracked :: ShowS
cracked [Char]
def
          | Bool -> Bool
not Bool
crackNum = [Char]
def
          | Bool
True         = case CV -> Bool -> Maybe Integer -> Maybe [Char]
forall a. CrackNum a => a -> Bool -> Maybe Integer -> Maybe [Char]
CN.crackNum CV
cv Bool
verbose ([Char]
nm [Char] -> [([Char], Integer)] -> Maybe Integer
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [([Char], Integer)]
crackNumSurfaceVals) of
                             Maybe [Char]
Nothing -> [Char]
def
                             Just [Char]
cs -> [Char]
def [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"\n" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
cs

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

      Just [Char]
execPath -> SMTConfig
-> State -> [Char] -> [[Char]] -> [Char] -> (State -> IO a) -> IO a
forall a.
SMTConfig
-> State -> [Char] -> [[Char]] -> [Char] -> (State -> IO a) -> IO a
runSolver SMTConfig
cfg State
ctx [Char]
execPath [[Char]]
opts [Char]
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. (HasCallStack, 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. (HasCallStack, 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
$ [Char] -> IO a
forall a. HasCallStack => [Char] -> a
error ([Char] -> IO a) -> [Char] -> IO a
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [ [Char]
"Failed to start the external solver:\n" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ SomeException -> [Char]
forall a. Show a => a -> [Char]
show SomeException
e
                                                                                                , [Char]
"Make sure you can start " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ShowS
forall a. Show a => a -> [Char]
show [Char]
execPath
                                                                                                , [Char]
"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 :: [Char] -> [Char] -> SMTEngine
standardEngine [Char]
envName [Char]
envOptName SMTConfig
cfg State
ctx [Char]
pgm State -> IO res
continuation = do

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

    let cfg' = SMTConfig
cfg {solver = (solver cfg) {executable = execName, options = const execOpts}}

    standardSolver cfg' ctx pgm continuation

-- | A standard solver interface. If the solver is SMT-Lib compliant, then this function should suffice in
-- communicating with it.
standardSolver :: SMTConfig       -- ^ The current configuration
               -> State           -- ^ Context in which we are running
               -> String          -- ^ The program
               -> (State -> IO a) -- ^ The continuation
               -> IO a
standardSolver :: SMTEngine
standardSolver SMTConfig
config State
ctx [Char]
pgm State -> IO a
continuation = do
    let msg :: [Char] -> m ()
msg [Char]
s    = SMTConfig -> [[Char]] -> m ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
debug SMTConfig
config [[Char]
"** " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
s]
        smtSolver :: SMTSolver
smtSolver= SMTConfig -> SMTSolver
solver SMTConfig
config
        exec :: [Char]
exec     = SMTSolver -> [Char]
executable SMTSolver
smtSolver
        opts :: [[Char]]
opts     = SMTSolver -> SMTConfig -> [[Char]]
options SMTSolver
smtSolver SMTConfig
config [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ SMTConfig -> [[Char]]
extraArgs SMTConfig
config
    [Char] -> IO ()
forall {m :: * -> *}. MonadIO m => [Char] -> m ()
msg ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char]
"Calling: "  [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ([Char]
exec [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (if [[Char]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[Char]]
opts then [Char]
"" else [Char]
" ") [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [[Char]] -> [Char]
joinArgs [[Char]]
opts)
    [Char] -> ()
forall a. NFData a => a -> ()
rnf [Char]
pgm () -> IO a -> IO a
forall a b. a -> b -> b
`seq` SMTConfig
-> State -> [Char] -> [[Char]] -> [Char] -> (State -> IO a) -> IO a
forall a.
SMTConfig
-> State -> [Char] -> [[Char]] -> [Char] -> (State -> IO a) -> IO a
pipeProcess SMTConfig
config State
ctx [Char]
exec [[Char]]
opts [Char]
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 :: forall a.
SMTConfig
-> State -> [Char] -> [[Char]] -> [Char] -> (State -> IO a) -> IO a
runSolver SMTConfig
cfg State
ctx [Char]
execPath [[Char]]
opts [Char]
pgm State -> IO a
continuation
 = do let nm :: [Char]
nm  = Solver -> [Char]
forall a. Show a => a -> [Char]
show (SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
cfg))
          msg :: [[Char]] -> IO ()
msg = SMTConfig -> [[Char]] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
debug SMTConfig
cfg ([[Char]] -> IO ()) -> ([[Char]] -> [[Char]]) -> [[Char]] -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS -> [[Char]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map ([Char]
"*** " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++)

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

          -- the very first command we send
          heartbeat :: [Char]
heartbeat = [Char]
"(set-option :print-success true)"

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

                let send :: Maybe Int -> String -> IO ()
                    send Maybe Int
mbTimeOut [Char]
command = do Handle -> [Char] -> IO ()
hPutStrLn Handle
inh (ShowS
clean [Char]
command)
                                                Handle -> IO ()
hFlush Handle
inh
                                                Maybe [Char] -> TranscriptMsg -> IO ()
recordTranscript (SMTConfig -> Maybe [Char]
transcript SMTConfig
cfg) (TranscriptMsg -> IO ()) -> TranscriptMsg -> IO ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Maybe Int -> TranscriptMsg
SentMsg [Char]
command Maybe Int
mbTimeOut

                    -- is this a set-command? Then we expect faster response; except for the heartbeat
                    isSetCommand = Bool -> ([Char] -> Bool) -> Maybe [Char] -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False [Char] -> Bool
chk
                      where chk :: [Char] -> Bool
chk [Char]
cmd = [Char]
cmd [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
heartbeat Bool -> Bool -> Bool
&& [Char]
"(set-option :" [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Char]
cmd

                    -- 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
mbTimeOutGiven [Char]
command =
                                  let -- If the command is a set-option call, make sure there's a timeout on it
                                      -- This ensures that if we try to set an option before diagnostic-output
                                      -- is redirected to stdout and the solver chokes, then we can catch it
                                      mbTimeOut :: Maybe Int
mbTimeOut | Maybe [Char] -> Bool
isSetCommand ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
command) = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1000000
                                                | Bool
True                        = Maybe Int
mbTimeOutGiven

                                      -- 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
                                      cmd :: [Char]
cmd = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
dropWhile Char -> Bool
isSpace [Char]
command

                                  in if [Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
cmd Bool -> Bool -> Bool
|| [Char]
";" [Char] -> [Char] -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` [Char]
cmd
                                     then [Char] -> IO [Char]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [Char]
"success"
                                     else do Maybe Int -> [Char] -> IO ()
send Maybe Int
mbTimeOut [Char]
command
                                             Maybe [Char] -> Maybe Int -> IO [Char]
getResponseFromSolver ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
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 [Char]
mbCommand Maybe Int
mbTimeOut = do
                                response <- Bool -> Int -> [[Char]] -> IO [[Char]]
go Bool
True Int
0 []
                                let collated = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n" ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [[Char]]
forall a. [a] -> [a]
reverse [[Char]]
response
                                recordTranscript (transcript cfg) $ RecvMsg collated
                                return collated

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

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

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

                                                                                      stillInside = Bool -> [Char] -> Bool
walk Bool
inString [Char]
ln

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

                                                                                  if stillInside
                                                                                     then collect True sofar'
                                                                                     else return sofar'

                                             -- Carefully grab things as they are ready. But don't block!
                                             collectH :: Handle -> IO [Char]
collectH Handle
handle = ShowS
forall a. [a] -> [a]
reverse ShowS -> IO [Char] -> IO [Char]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> IO [Char]
coll [Char]
""
                                               where coll :: [Char] -> IO [Char]
coll [Char]
sofar = do b <- Handle -> IO Bool
hReady Handle
handle
                                                                     if b
                                                                        then hGetChar handle >>= \Char
c -> [Char] -> IO [Char]
coll (Char
cChar -> ShowS
forall a. a -> [a] -> [a]
:[Char]
sofar)
                                                                        else pure sofar

                                             -- grab the contents of a handle, and return it trimmed if any
                                             grab :: Handle -> IO (Maybe [Char])
grab Handle
handle = do mbCts <- ([Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char]) -> IO [Char] -> IO (Maybe [Char])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Handle -> IO [Char]
collectH Handle
handle) IO (Maybe [Char])
-> (SomeException -> IO (Maybe [Char])) -> IO (Maybe [Char])
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch` (\(SomeException
_ :: C.SomeException) -> Maybe [Char] -> IO (Maybe [Char])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe [Char]
forall a. Maybe a
Nothing)
                                                              pure $ dropWhile isSpace <$> mbCts

                                         in case Maybe Int
timeOutToUse of
                                              Maybe Int
Nothing -> [Char] -> SolverLine
SolverRegular ([Char] -> SolverLine) -> IO [Char] -> IO SolverLine
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO [Char]
getFullLine
                                              Just Int
t  -> do r <- Int -> IO [Char] -> IO (Maybe [Char])
forall a. Int -> IO a -> IO (Maybe a)
Timeout.timeout Int
t IO [Char]
getFullLine
                                                            case r of
                                                              Just [Char]
l  -> SolverLine -> IO SolverLine
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SolverLine -> IO SolverLine) -> SolverLine -> IO SolverLine
forall a b. (a -> b) -> a -> b
$ [Char] -> SolverLine
SolverRegular [Char]
l
                                                              Maybe [Char]
Nothing -> do out <- Handle -> IO (Maybe [Char])
grab Handle
outh
                                                                            err <- grab errh
                                                                            -- in this case, if we have something on out/err pass that back as regular
                                                                            case err `mplus` out of
                                                                              Just [Char]
x | Bool -> Bool
not ([Char] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
x) -> SolverLine -> IO SolverLine
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SolverLine -> IO SolverLine) -> SolverLine -> IO SolverLine
forall a b. (a -> b) -> a -> b
$ [Char] -> SolverLine
SolverRegular [Char]
x
                                                                              Maybe [Char]
_                     -> SolverLine -> IO SolverLine
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SolverLine -> IO SolverLine) -> SolverLine -> IO SolverLine
forall a b. (a -> b) -> a -> b
$ [Char] -> SolverLine
SolverTimeout (Int -> [Char]
timeOutMsg Int
t)

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

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

                                              SolverTimeout [Char]
e -> do ProcessHandle -> IO ()
terminateProcess ProcessHandle
pid -- NB. Do not *wait* for the process, just quit.

                                                                    SBVException -> IO [[Char]]
forall e a. (HasCallStack, Exception e) => e -> IO a
C.throwIO SBVException { sbvExceptionDescription :: [Char]
sbvExceptionDescription = [Char]
"Timeout! " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
e
                                                                                           , sbvExceptionSent :: Maybe [Char]
sbvExceptionSent        = Maybe [Char]
mbCommand
                                                                                           , sbvExceptionExpected :: Maybe [Char]
sbvExceptionExpected    = Maybe [Char]
forall a. Maybe a
Nothing
                                                                                           , sbvExceptionReceived :: Maybe [Char]
sbvExceptionReceived    = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just ([Char] -> Maybe [Char]) -> [Char] -> Maybe [Char]
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines ([[Char]] -> [[Char]]
forall a. [a] -> [a]
reverse [[Char]]
sofar)
                                                                                           , sbvExceptionStdOut :: Maybe [Char]
sbvExceptionStdOut      = Maybe [Char]
forall a. Maybe a
Nothing
                                                                                           , sbvExceptionStdErr :: Maybe [Char]
sbvExceptionStdErr      = Maybe [Char]
forall a. Maybe a
Nothing
                                                                                           , sbvExceptionExitCode :: Maybe ExitCode
sbvExceptionExitCode    = Maybe ExitCode
forall a. Maybe a
Nothing
                                                                                           , sbvExceptionConfig :: SMTConfig
sbvExceptionConfig      = SMTConfig
cfg { solver = (solver cfg) { executable = execPath } }
                                                                                           , sbvExceptionReason :: Maybe [[Char]]
sbvExceptionReason      = Maybe [[Char]]
forall a. Maybe a
Nothing
                                                                                           , sbvExceptionHint :: Maybe [[Char]]
sbvExceptionHint        = if Bool -> Bool
not (SMTConfig -> Bool
verbose SMTConfig
cfg)
                                                                                                                       then [[Char]] -> Maybe [[Char]]
forall a. a -> Maybe a
Just [[Char]
"Run with 'verbose=True' for further information"]
                                                                                                                       else Maybe [[Char]]
forall a. Maybe a
Nothing
                                                                                           }

                    terminateSolver = do Handle -> IO ()
hClose Handle
inh
                                         outMVar <- IO (MVar ())
forall a. IO (MVar a)
newEmptyMVar
                                         out <- hGetContents outh `C.catch`  (\(SomeException
e :: C.SomeException) -> SomeException -> IO [Char] -> IO [Char]
forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e ([Char] -> IO [Char]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeException -> [Char]
forall a. Show a => a -> [Char]
show SomeException
e)))
                                         _ <- forkIO $ C.evaluate (length out) >> putMVar outMVar ()
                                         err <- hGetContents errh `C.catch`  (\(SomeException
e :: C.SomeException) -> SomeException -> IO [Char] -> IO [Char]
forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e ([Char] -> IO [Char]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeException -> [Char]
forall a. Show a => a -> [Char]
show SomeException
e)))
                                         _ <- forkIO $ C.evaluate (length err) >> putMVar outMVar ()
                                         takeMVar outMVar
                                         takeMVar outMVar
                                         hClose outh `C.catch`  (\(SomeException
e :: C.SomeException) -> SomeException -> IO () -> IO ()
forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()))
                                         hClose errh `C.catch`  (\(SomeException
e :: C.SomeException) -> SomeException -> IO () -> IO ()
forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()))
                                         ex <- waitForProcess pid `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 a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> ExitCode
ExitFailure (-Int
999))))
                                         return (out, err, ex)

                    cleanUp Maybe e
maybeForwardedException
                      = do (out, err, ex) <- IO ([Char], [Char], ExitCode)
terminateSolver

                           msg $   [ "Solver   : " ++ nm
                                   , "Exit code: " ++ show ex
                                   ]
                                ++ [ "Std-out  : " ++ intercalate "\n           " (lines out) | not (null out)]
                                ++ [ "Std-err  : " ++ intercalate "\n           " (lines err) | not (null err)]

                           finalizeTranscript (transcript cfg) ex
                           recordEndTime cfg ctx

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

                return (send, ask, getResponseFromSolver, terminateSolver, cleanUp, pid)

      let executeSolver = do let sendAndGetSuccess :: Maybe Int -> String -> IO ()
                                 sendAndGetSuccess :: Maybe Int -> [Char] -> IO ()
sendAndGetSuccess Maybe Int
mbTimeOut [Char]
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 -> [Char] -> IO ()
send Maybe Int
mbTimeOut [Char]
l
                                        SMTConfig -> [[Char]] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
debug SMTConfig
cfg [[Char]
"[ISSUE] " [Char] -> ShowS
`alignPlain` [Char]
l]
                                   | Bool
True
                                   = do r <- Maybe Int -> [Char] -> IO [Char]
ask Maybe Int
mbTimeOut [Char]
l
                                        case words r of
                                          [[Char]
"success"] -> SMTConfig -> [[Char]] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
debug SMTConfig
cfg [[Char]
"[GOOD] " [Char] -> ShowS
`alignPlain` [Char]
l]
                                          [[Char]]
_           -> do SMTConfig -> [[Char]] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
debug SMTConfig
cfg [[Char]
"[FAIL] " [Char] -> ShowS
`alignPlain` [Char]
l]

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

                                                                reason :: [[Char]]
reason | Bool
isOption = [ [Char]
"Backend solver reports it does not support this option."
                                                                                    , [Char]
"Check the spelling, and if correct please report this as a"
                                                                                    , [Char]
"bug/feature request with the solver!"
                                                                                    ]
                                                                       | Bool
True     = [ [Char]
"Check solver response for further information. If your code is correct,"
                                                                                    , [Char]
"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
                                                            mbExtras <- ([Char] -> Either [Char] [Char]
forall a b. b -> Either a b
Right ([Char] -> Either [Char] [Char])
-> IO [Char] -> IO (Either [Char] [Char])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Char] -> Maybe Int -> IO [Char]
getResponseFromSolver Maybe [Char]
forall a. Maybe a
Nothing (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
5000000))
                                                                        IO (Either [Char] [Char])
-> (SomeException -> IO (Either [Char] [Char]))
-> IO (Either [Char] [Char])
forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`C.catch` (\(SomeException
e :: C.SomeException) -> SomeException
-> IO (Either [Char] [Char]) -> IO (Either [Char] [Char])
forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e (Either [Char] [Char] -> IO (Either [Char] [Char])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Char] -> Either [Char] [Char]
forall a b. a -> Either a b
Left (SomeException -> [Char]
forall a. Show a => a -> [Char]
show SomeException
e))))

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

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

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

                                                            C.throwIO exc

                             -- Mark in the log, mostly.
                             Maybe Int -> [Char] -> IO ()
sendAndGetSuccess Maybe Int
forall a. Maybe a
Nothing [Char]
"; 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 -> [[Char]] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
debug SMTConfig
cfg [[Char]
"** Skipping heart-beat for the solver " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Solver -> [Char]
forall a. Show a => a -> [Char]
show Solver
backend]
                                else do r <- Maybe Int -> [Char] -> IO [Char]
ask (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
5000000) [Char]
heartbeat  -- Give the solver 5s to respond, this should be plenty enough!
                                        case words r of
                                          [[Char]
"success"]     -> SMTConfig -> [[Char]] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
debug SMTConfig
cfg [[Char]
"[GOOD] " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
heartbeat]
                                          [[Char]
"unsupported"] -> [Char] -> IO ()
forall a. HasCallStack => [Char] -> a
error ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [ [Char]
""
                                                                             , [Char]
"*** Backend solver (" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++  Solver -> [Char]
forall a. Show a => a -> [Char]
show Solver
backend [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
") does not support the command:"
                                                                             , [Char]
"***"
                                                                             , [Char]
"***     (set-option :print-success true)"
                                                                             , [Char]
"***"
                                                                             , [Char]
"*** SBV relies on this feature to coordinate communication!"
                                                                             , [Char]
"*** Please request this as a feature!"
                                                                             ]
                                          [[Char]]
_               -> [Char] -> IO ()
forall a. HasCallStack => [Char] -> a
error ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [ [Char]
""
                                                                             , [Char]
"*** Data.SBV: Failed to initiate contact with the solver!"
                                                                             , [Char]
"***"
                                                                             , [Char]
"***   Sent    : " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
heartbeat
                                                                             , [Char]
"***   Expected: success"
                                                                             , [Char]
"***   Received: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
r
                                                                             , [Char]
"***"
                                                                             , [Char]
"*** 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 -> [[Char]] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [[Char]] -> m ()
debug SMTConfig
cfg [ [Char]
"** Backend solver " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Solver -> [Char]
forall a. Show a => a -> [Char]
show Solver
backend [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" does not support global decls."
                                               , [Char]
"** Some incremental calls, such as pop, will be limited."
                                               ]
                                else Maybe Int -> [Char] -> IO ()
sendAndGetSuccess Maybe Int
forall a. Maybe a
Nothing [Char]
"(set-option :global-declarations true)"

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

                             -- Prepare the query context and ship it off
                             let qs :: QueryState
qs = QueryState { queryAsk :: Maybe Int -> [Char] -> IO [Char]
queryAsk                 = Maybe Int -> [Char] -> IO [Char]
ask
                                                 , querySend :: Maybe Int -> [Char] -> IO ()
querySend                = Maybe Int -> [Char] -> IO ()
send
                                                 , queryRetrieveResponse :: Maybe Int -> IO [Char]
queryRetrieveResponse    = Maybe [Char] -> Maybe Int -> IO [Char]
getResponseFromSolver Maybe [Char]
forall a. Maybe a
Nothing
                                                 , queryConfig :: SMTConfig
queryConfig              = SMTConfig
cfg
                                                 , queryTerminate :: Maybe SomeException -> IO ()
queryTerminate           = Maybe SomeException -> 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

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

                             case 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
_  -> [Char] -> IO ()
forall a. HasCallStack => [Char] -> a
error ([Char] -> IO ()) -> [Char] -> IO ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
unlines [ [Char]
""
                                                          , [Char]
"Data.SBV: Impossible happened, query-state was already set."
                                                          , [Char]
"Please report this as a bug!"
                                                          ]

                             -- off we go!
                             continuation ctx

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

      launchSolver `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
                                                                            ec <- ProcessHandle -> IO ExitCode
waitForProcess ProcessHandle
pid
                                                                            recordException    (transcript cfg) (show e)
                                                                            finalizeTranscript (transcript cfg) ec
                                                                            recordEndTime cfg ctx
                                                                            C.throwIO e)

-- We should not be catching/processing asynchronous exceptions.
-- See http://github.com/LeventErkok/sbv/issues/410
handleAsync :: C.SomeException -> IO a -> IO a
handleAsync :: forall a. SomeException -> IO a -> IO a
handleAsync SomeException
e IO a
cont
  | Bool
isAsynchronous = SomeException -> IO a
forall e a. (HasCallStack, 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)