-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Control.Query
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Querying a solver interactively.
-----------------------------------------------------------------------------

{-# LANGUAGE BangPatterns        #-}
{-# LANGUAGE LambdaCase          #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE Rank2Types          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections       #-}
{-# LANGUAGE ViewPatterns        #-}

{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}

module Data.SBV.Control.Query (
       send, ask, retrieveResponse
     , CheckSatResult(..), checkSat, checkSatUsing, checkSatAssuming, checkSatAssumingWithUnsatisfiableSet
     , getUnsatCore, getProof, getInterpolantMathSAT, getInterpolantZ3, getAbduct, getAbductNext, getAssignment, getOption
     , push, pop, getAssertionStackDepth
     , inNewAssertionStack, echo, caseSplit, resetAssertions, exit, getAssertions, getUninterpretedValue, getModel, getSMTResult
     , getLexicographicOptResults, getIndependentOptResults, getParetoOptResults, getAllSatResult, getUnknownReason, getObservables, ensureSat
     , SMTOption(..), SMTInfoFlag(..), SMTErrorBehavior(..), SMTReasonUnknown(..), SMTInfoResponse(..), getInfo
     , Logic(..), Assignment(..)
     , ignoreExitCode, timeout
     , (|->)
     , mkSMTResult
     , io
     ) where

import Control.Monad          (unless, when, zipWithM)
import Control.Monad.IO.Class (MonadIO)

import Data.IORef (readIORef)

import qualified Data.Map.Strict as M
import qualified Data.Sequence   as S
import qualified Data.Text       as T
import qualified Data.Foldable   as F


import Data.Char      (toLower)
import Data.List      (intercalate, nubBy, sortOn)
import Data.Maybe     (listToMaybe, catMaybes, fromMaybe)
import Data.Function  (on)
import Data.Bifunctor (first)
import Data.Foldable  (toList)

import Data.SBV.Core.Data

import Data.SBV.Core.Symbolic (MonadQuery(..), State(..), incrementInternalCounter, validationRequested, getSV, lookupInput, mustIgnoreVar)

import Data.SBV.Utils.SExpr

import Data.SBV.Control.Types
import Data.SBV.Control.Utils

import Data.SBV.Utils.Lib       (unBar)
import Data.SBV.Utils.PrettyNum (showNegativeNumber)

-- | An Assignment of a model binding
data Assignment = Assign SVal CV

-- | Remove the bars from model names; these are (mostly!) automatically inserted
unBarModel :: SMTModel -> SMTModel
unBarModel :: SMTModel -> SMTModel
unBarModel SMTModel {[(String, GeneralizedCV)]
modelObjectives :: [(String, GeneralizedCV)]
modelObjectives :: SMTModel -> [(String, GeneralizedCV)]
modelObjectives, Maybe [(NamedSymVar, CV)]
modelBindings :: Maybe [(NamedSymVar, CV)]
modelBindings :: SMTModel -> Maybe [(NamedSymVar, CV)]
modelBindings, [(String, CV)]
modelAssocs :: [(String, CV)]
modelAssocs :: SMTModel -> [(String, CV)]
modelAssocs, [(String, (Bool, SBVType, Either String ([([CV], CV)], CV)))]
modelUIFuns :: [(String, (Bool, SBVType, Either String ([([CV], CV)], CV)))]
modelUIFuns :: SMTModel
-> [(String, (Bool, SBVType, Either String ([([CV], CV)], CV)))]
modelUIFuns}
   = SMTModel { modelObjectives :: [(String, GeneralizedCV)]
modelObjectives = (String, GeneralizedCV) -> (String, GeneralizedCV)
forall {b}. (String, b) -> (String, b)
ubf       ((String, GeneralizedCV) -> (String, GeneralizedCV))
-> [(String, GeneralizedCV)] -> [(String, GeneralizedCV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(String, GeneralizedCV)]
modelObjectives
              , modelBindings :: Maybe [(NamedSymVar, CV)]
modelBindings   = ((NamedSymVar, CV) -> (NamedSymVar, CV)
forall {b}. (NamedSymVar, b) -> (NamedSymVar, b)
ubn ((NamedSymVar, CV) -> (NamedSymVar, CV))
-> [(NamedSymVar, CV)] -> [(NamedSymVar, CV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) ([(NamedSymVar, CV)] -> [(NamedSymVar, CV)])
-> Maybe [(NamedSymVar, CV)] -> Maybe [(NamedSymVar, CV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [(NamedSymVar, CV)]
modelBindings
              , modelAssocs :: [(String, CV)]
modelAssocs     = (String, CV) -> (String, CV)
forall {b}. (String, b) -> (String, b)
ubf       ((String, CV) -> (String, CV)) -> [(String, CV)] -> [(String, CV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(String, CV)]
modelAssocs
              , modelUIFuns :: [(String, (Bool, SBVType, Either String ([([CV], CV)], CV)))]
modelUIFuns     = (String, (Bool, SBVType, Either String ([([CV], CV)], CV)))
-> (String, (Bool, SBVType, Either String ([([CV], CV)], CV)))
forall {b}. (String, b) -> (String, b)
ubf       ((String, (Bool, SBVType, Either String ([([CV], CV)], CV)))
 -> (String, (Bool, SBVType, Either String ([([CV], CV)], CV))))
-> [(String, (Bool, SBVType, Either String ([([CV], CV)], CV)))]
-> [(String, (Bool, SBVType, Either String ([([CV], CV)], CV)))]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(String, (Bool, SBVType, Either String ([([CV], CV)], CV)))]
modelUIFuns
              }
   where ubf :: (String, b) -> (String, b)
ubf (String
n, b
a) = (String -> String
unBar String
n, b
a)
         ubn :: (NamedSymVar, b) -> (NamedSymVar, b)
ubn (NamedSymVar SV
sv Name
nm, b
a) = (SV -> Name -> NamedSymVar
NamedSymVar SV
sv (String -> Name
T.pack (String -> String
unBar (Name -> String
T.unpack Name
nm))), b
a)

-- Is this a string? If so, return it, otherwise fail in the Maybe monad.
fromECon :: SExpr -> Maybe String
fromECon :: SExpr -> Maybe String
fromECon (ECon String
s) = String -> Maybe String
forall a. a -> Maybe a
Just String
s
fromECon SExpr
_        = Maybe String
forall a. Maybe a
Nothing

-- Collect strings appearing, used in 'getOption' only
stringsOf :: SExpr -> [String]
stringsOf :: SExpr -> [String]
stringsOf (ECon String
s)           = [String
s]
stringsOf (ENum (Integer
i, Maybe Int
_))      = [Integer -> String
forall a. Show a => a -> String
show Integer
i]
stringsOf (EReal   AlgReal
r)        = [AlgReal -> String
forall a. Show a => a -> String
show AlgReal
r]
stringsOf (EFloat  Float
f)        = [Float -> String
forall a. Show a => a -> String
show Float
f]
stringsOf (EFloatingPoint FP
f) = [FP -> String
forall a. Show a => a -> String
show FP
f]
stringsOf (EDouble Double
d)        = [Double -> String
forall a. Show a => a -> String
show Double
d]
stringsOf (EApp [SExpr]
ss)          = (SExpr -> [String]) -> [SExpr] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SExpr -> [String]
stringsOf [SExpr]
ss

-- Sort of a light-hearted show for SExprs, for better consumption at the user level.
serialize :: Bool -> SExpr -> String
serialize :: Bool -> SExpr -> String
serialize Bool
removeQuotes = SExpr -> String
go
  where go :: SExpr -> String
go (ECon String
s)           = if Bool
removeQuotes then String -> String
unQuote String
s else String
s
        go (ENum (Integer
i, Maybe Int
_))      = Integer -> String
forall a. (Show a, Num a, Ord a) => a -> String
showNegativeNumber Integer
i
        go (EReal   AlgReal
r)        = AlgReal -> String
forall a. (Show a, Num a, Ord a) => a -> String
showNegativeNumber AlgReal
r
        go (EFloat  Float
f)        = Float -> String
forall a. (Show a, Num a, Ord a) => a -> String
showNegativeNumber Float
f
        go (EDouble Double
d)        = Double -> String
forall a. (Show a, Num a, Ord a) => a -> String
showNegativeNumber Double
d
        go (EFloatingPoint FP
f) = FP -> String
forall a. Show a => a -> String
show FP
f
        go (EApp [SExpr
x])         = SExpr -> String
go SExpr
x
        go (EApp [SExpr]
ss)          = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SExpr -> String) -> [SExpr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SExpr -> String
go [SExpr]
ss) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

-- | Generalization of 'Data.SBV.Control.getInfo'
getInfo :: (MonadIO m, MonadQuery m) => SMTInfoFlag -> m SMTInfoResponse
getInfo :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
SMTInfoFlag -> m SMTInfoResponse
getInfo SMTInfoFlag
flag = do
    let cmd :: String
cmd = String
"(get-info " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SMTInfoFlag -> String
forall a. Show a => a -> String
show SMTInfoFlag
flag String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getInfo" String
cmd String
"a valid get-info response" Maybe [String]
forall a. Maybe a
Nothing

        isAllStatistics :: SMTInfoFlag -> Bool
isAllStatistics SMTInfoFlag
AllStatistics = Bool
True
        isAllStatistics SMTInfoFlag
_             = Bool
False

        isAllStat :: Bool
isAllStat = SMTInfoFlag -> Bool
isAllStatistics SMTInfoFlag
flag

        grabAllStat :: SExpr -> SExpr -> (String, String)
grabAllStat SExpr
k SExpr
v = (SExpr -> String
render SExpr
k, SExpr -> String
render SExpr
v)

        -- we're trying to do our best to get key-value pairs here, but this
        -- is necessarily a half-hearted attempt.
        grabAllStats :: SExpr -> [(String, String)]
grabAllStats (EApp [SExpr]
xs) = [SExpr] -> [(String, String)]
walk [SExpr]
xs
           where walk :: [SExpr] -> [(String, String)]
walk []             = []
                 walk [SExpr
t]            = [SExpr -> SExpr -> (String, String)
grabAllStat SExpr
t (String -> SExpr
ECon String
"")]
                 walk (SExpr
t : SExpr
v : [SExpr]
rest) =  SExpr -> SExpr -> (String, String)
grabAllStat SExpr
t SExpr
v          (String, String) -> [(String, String)] -> [(String, String)]
forall a. a -> [a] -> [a]
: [SExpr] -> [(String, String)]
walk [SExpr]
rest
        grabAllStats SExpr
o = [SExpr -> SExpr -> (String, String)
grabAllStat SExpr
o (String -> SExpr
ECon String
"")]

    r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd

    parse r bad $ \SExpr
pe ->
       if Bool
isAllStat
          then SMTInfoResponse -> m SMTInfoResponse
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTInfoResponse -> m SMTInfoResponse)
-> SMTInfoResponse -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ [(String, String)] -> SMTInfoResponse
Resp_AllStatistics ([(String, String)] -> SMTInfoResponse)
-> [(String, String)] -> SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ SExpr -> [(String, String)]
grabAllStats SExpr
pe
          else case SExpr
pe of
                 ECon String
"unsupported"                                        -> SMTInfoResponse -> m SMTInfoResponse
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return SMTInfoResponse
Resp_Unsupported
                 EApp [ECon String
":assertion-stack-levels", ENum (Integer
i, Maybe Int
_)]        -> SMTInfoResponse -> m SMTInfoResponse
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTInfoResponse -> m SMTInfoResponse)
-> SMTInfoResponse -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ Integer -> SMTInfoResponse
Resp_AssertionStackLevels Integer
i
                 EApp (ECon String
":authors" : [SExpr]
ns)                               -> SMTInfoResponse -> m SMTInfoResponse
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTInfoResponse -> m SMTInfoResponse)
-> SMTInfoResponse -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ [String] -> SMTInfoResponse
Resp_Authors ((SExpr -> String) -> [SExpr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SExpr -> String
render [SExpr]
ns)
                 EApp [ECon String
":error-behavior", ECon String
"immediate-exit"]      -> SMTInfoResponse -> m SMTInfoResponse
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTInfoResponse -> m SMTInfoResponse)
-> SMTInfoResponse -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ SMTErrorBehavior -> SMTInfoResponse
Resp_Error SMTErrorBehavior
ErrorImmediateExit
                 EApp [ECon String
":error-behavior", ECon String
"continued-execution"] -> SMTInfoResponse -> m SMTInfoResponse
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTInfoResponse -> m SMTInfoResponse)
-> SMTInfoResponse -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ SMTErrorBehavior -> SMTInfoResponse
Resp_Error SMTErrorBehavior
ErrorContinuedExecution
                 EApp (ECon String
":name" : [SExpr]
o)                                   -> SMTInfoResponse -> m SMTInfoResponse
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTInfoResponse -> m SMTInfoResponse)
-> SMTInfoResponse -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ String -> SMTInfoResponse
Resp_Name (SExpr -> String
render ([SExpr] -> SExpr
EApp [SExpr]
o))
                 EApp (ECon String
":reason-unknown" : [SExpr]
o)                         -> SMTInfoResponse -> m SMTInfoResponse
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTInfoResponse -> m SMTInfoResponse)
-> SMTInfoResponse -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ SMTReasonUnknown -> SMTInfoResponse
Resp_ReasonUnknown ([SExpr] -> SMTReasonUnknown
unk [SExpr]
o)
                 EApp (ECon String
":version" : [SExpr]
o)                                -> SMTInfoResponse -> m SMTInfoResponse
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTInfoResponse -> m SMTInfoResponse)
-> SMTInfoResponse -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ String -> SMTInfoResponse
Resp_Version (SExpr -> String
render ([SExpr] -> SExpr
EApp [SExpr]
o))
                 EApp (ECon String
s : [SExpr]
o)                                         -> SMTInfoResponse -> m SMTInfoResponse
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTInfoResponse -> m SMTInfoResponse)
-> SMTInfoResponse -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ String -> [String] -> SMTInfoResponse
Resp_InfoKeyword String
s ((SExpr -> String) -> [SExpr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SExpr -> String
render [SExpr]
o)
                 SExpr
_                                                         -> String -> Maybe [String] -> m SMTInfoResponse
forall {a}. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing

  where render :: SExpr -> String
render = Bool -> SExpr -> String
serialize Bool
True

        unk :: [SExpr] -> SMTReasonUnknown
unk [ECon String
s] | Just SMTReasonUnknown
d <- String -> Maybe SMTReasonUnknown
getUR String
s = SMTReasonUnknown
d
        unk [SExpr]
o                            = String -> SMTReasonUnknown
UnknownOther (SExpr -> String
render ([SExpr] -> SExpr
EApp [SExpr]
o))

        getUR :: String -> Maybe SMTReasonUnknown
getUR String
s = (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (String -> String
unQuote String
s) String -> [(String, SMTReasonUnknown)] -> Maybe SMTReasonUnknown
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower String
k, SMTReasonUnknown
d) | (String
k, SMTReasonUnknown
d) <- [(String, SMTReasonUnknown)]
unknownReasons]

        -- As specified in Section 4.1 of the SMTLib document. Note that we're adding the
        -- extra timeout as it is useful in this context.
        unknownReasons :: [(String, SMTReasonUnknown)]
unknownReasons = [ (String
"memout",     SMTReasonUnknown
UnknownMemOut)
                         , (String
"incomplete", SMTReasonUnknown
UnknownIncomplete)
                         , (String
"timeout",    SMTReasonUnknown
UnknownTimeOut)
                         ]

-- | Generalization of 'Data.SBV.Control.getOption'
getOption :: (MonadIO m, MonadQuery m) => (a -> SMTOption) -> m (Maybe SMTOption)
getOption :: forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(a -> SMTOption) -> m (Maybe SMTOption)
getOption a -> SMTOption
f = case a -> SMTOption
f a
forall a. HasCallStack => a
undefined of
                 DiagnosticOutputChannel{}   -> String
-> String
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a} {a}.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor String
"DiagnosticOutputChannel"   String
":diagnostic-output-channel"   ((SExpr
  -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
 -> m (Maybe SMTOption))
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (String -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a}.
Monad m =>
(String -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
string     String -> SMTOption
DiagnosticOutputChannel
                 ProduceAssertions{}         -> String
-> String
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a} {a}.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor String
"ProduceAssertions"         String
":produce-assertions"          ((SExpr
  -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
 -> m (Maybe SMTOption))
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Bool -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a}.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool       Bool -> SMTOption
ProduceAssertions
                 ProduceAssignments{}        -> String
-> String
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a} {a}.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor String
"ProduceAssignments"        String
":produce-assignments"         ((SExpr
  -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
 -> m (Maybe SMTOption))
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Bool -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a}.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool       Bool -> SMTOption
ProduceAssignments
                 ProduceProofs{}             -> String
-> String
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a} {a}.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor String
"ProduceProofs"             String
":produce-proofs"              ((SExpr
  -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
 -> m (Maybe SMTOption))
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Bool -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a}.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool       Bool -> SMTOption
ProduceProofs
                 ProduceInterpolants{}       -> String
-> String
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a} {a}.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor String
"ProduceInterpolants"       String
":produce-interpolants"        ((SExpr
  -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
 -> m (Maybe SMTOption))
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Bool -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a}.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool       Bool -> SMTOption
ProduceInterpolants
                 ProduceUnsatAssumptions{}   -> String
-> String
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a} {a}.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor String
"ProduceUnsatAssumptions"   String
":produce-unsat-assumptions"   ((SExpr
  -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
 -> m (Maybe SMTOption))
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Bool -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a}.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool       Bool -> SMTOption
ProduceUnsatAssumptions
                 ProduceUnsatCores{}         -> String
-> String
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a} {a}.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor String
"ProduceUnsatCores"         String
":produce-unsat-cores"         ((SExpr
  -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
 -> m (Maybe SMTOption))
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Bool -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a}.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool       Bool -> SMTOption
ProduceUnsatCores
                 ProduceAbducts{}            -> String
-> String
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a} {a}.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor String
"ProduceAbducts"            String
":produce-abducts"             ((SExpr
  -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
 -> m (Maybe SMTOption))
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Bool -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a}.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool       Bool -> SMTOption
ProduceAbducts
                 RandomSeed{}                -> String
-> String
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a} {a}.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor String
"RandomSeed"                String
":random-seed"                 ((SExpr
  -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
 -> m (Maybe SMTOption))
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Integer -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a}.
Monad m =>
(Integer -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
integer    Integer -> SMTOption
RandomSeed
                 ReproducibleResourceLimit{} -> String
-> String
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a} {a}.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor String
"ReproducibleResourceLimit" String
":reproducible-resource-limit" ((SExpr
  -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
 -> m (Maybe SMTOption))
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Integer -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a}.
Monad m =>
(Integer -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
integer    Integer -> SMTOption
ReproducibleResourceLimit
                 SMTVerbosity{}              -> String
-> String
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a} {a}.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor String
"SMTVerbosity"              String
":verbosity"                   ((SExpr
  -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
 -> m (Maybe SMTOption))
-> (SExpr
    -> (Maybe [String] -> m (Maybe SMTOption)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ (Integer -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a}.
Monad m =>
(Integer -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
integer    Integer -> SMTOption
SMTVerbosity
                 OptionKeyword String
nm [String]
_          -> String
-> String
-> (SExpr
    -> (Maybe [String] -> m (ZonkAny 1)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a} {a}.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor (String
"OptionKeyword" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm)     String
nm                             ((SExpr
  -> (Maybe [String] -> m (ZonkAny 1)) -> m (Maybe SMTOption))
 -> m (Maybe SMTOption))
-> (SExpr
    -> (Maybe [String] -> m (ZonkAny 1)) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ ([String] -> SMTOption)
-> SExpr
-> (Maybe [String] -> m (ZonkAny 1))
-> m (Maybe SMTOption)
forall {m :: * -> *} {a} {p}.
Monad m =>
([String] -> a) -> SExpr -> p -> m (Maybe a)
stringList (String -> [String] -> SMTOption
OptionKeyword String
nm)
                 SetLogic{}                  -> String -> m (Maybe SMTOption)
forall a. HasCallStack => String -> a
error String
"Data.SBV.Query: SMTLib does not allow querying the value of logic!"
                 SetTimeOut{}                -> String -> m (Maybe SMTOption)
forall a. HasCallStack => String -> a
error String
"Data.SBV.Query: SMTLib does not allow querying the timeout value!"
                 -- Not to be confused by getInfo, which is totally irrelevant!
                 SetInfo{}                   -> String -> m (Maybe SMTOption)
forall a. HasCallStack => String -> a
error String
"Data.SBV.Query: SMTLib does not allow querying value of meta-info!"

  where askFor :: String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor String
sbvName String
smtLibName SExpr -> (Maybe [String] -> m a) -> m (Maybe a)
continue = do
                let cmd :: String
cmd = String
"(get-option " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
smtLibName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                    bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected (String
"getOption " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sbvName) String
cmd String
"a valid option value" Maybe [String]
forall a. Maybe a
Nothing

                r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd

                parse r bad $ \case ECon String
"unsupported" -> Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
                                    SExpr
e                  -> SExpr -> (Maybe [String] -> m a) -> m (Maybe a)
continue SExpr
e (String -> Maybe [String] -> m a
forall {a}. String -> Maybe [String] -> m a
bad String
r)

        string :: (String -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
string String -> a
c (ECon String
s) Maybe [String] -> m (Maybe a)
_ = Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ String -> a
c String
s
        string String -> a
_ SExpr
e        Maybe [String] -> m (Maybe a)
k = Maybe [String] -> m (Maybe a)
k (Maybe [String] -> m (Maybe a)) -> Maybe [String] -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just [String
"Expected string, but got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show (Bool -> SExpr -> String
serialize Bool
False SExpr
e)]

        bool :: (Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool Bool -> a
c (ENum (Integer
0, Maybe Int
_)) Maybe [String] -> m (Maybe a)
_ = Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ Bool -> a
c Bool
False
        bool Bool -> a
c (ENum (Integer
1, Maybe Int
_)) Maybe [String] -> m (Maybe a)
_ = Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ Bool -> a
c Bool
True
        bool Bool -> a
_ SExpr
e             Maybe [String] -> m (Maybe a)
k = Maybe [String] -> m (Maybe a)
k (Maybe [String] -> m (Maybe a)) -> Maybe [String] -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just [String
"Expected boolean, but got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show (Bool -> SExpr -> String
serialize Bool
False SExpr
e)]

        integer :: (Integer -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
integer Integer -> a
c (ENum (Integer
i, Maybe Int
_)) Maybe [String] -> m (Maybe a)
_ = Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ Integer -> a
c Integer
i
        integer Integer -> a
_ SExpr
e             Maybe [String] -> m (Maybe a)
k = Maybe [String] -> m (Maybe a)
k (Maybe [String] -> m (Maybe a)) -> Maybe [String] -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just [String
"Expected integer, but got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show (Bool -> SExpr -> String
serialize Bool
False SExpr
e)]

        -- free format, really
        stringList :: ([String] -> a) -> SExpr -> p -> m (Maybe a)
stringList [String] -> a
c SExpr
e p
_ = Maybe a -> m (Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe a -> m (Maybe a)) -> Maybe a -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ [String] -> a
c ([String] -> a) -> [String] -> a
forall a b. (a -> b) -> a -> b
$ SExpr -> [String]
stringsOf SExpr
e

-- | Generalization of 'Data.SBV.Control.getUnknownReason'
getUnknownReason :: (MonadIO m, MonadQuery m) => m SMTReasonUnknown
getUnknownReason :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason = do ru <- SMTInfoFlag -> m SMTInfoResponse
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
SMTInfoFlag -> m SMTInfoResponse
getInfo SMTInfoFlag
ReasonUnknown
                      case ru of
                        SMTInfoResponse
Resp_Unsupported     -> SMTReasonUnknown -> m SMTReasonUnknown
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTReasonUnknown -> m SMTReasonUnknown)
-> SMTReasonUnknown -> m SMTReasonUnknown
forall a b. (a -> b) -> a -> b
$ String -> SMTReasonUnknown
UnknownOther String
"Solver responded: Unsupported."
                        Resp_ReasonUnknown SMTReasonUnknown
r -> SMTReasonUnknown -> m SMTReasonUnknown
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return SMTReasonUnknown
r
                        -- Shouldn't happen, but just in case:
                        SMTInfoResponse
_                    -> String -> m SMTReasonUnknown
forall a. HasCallStack => String -> a
error (String -> m SMTReasonUnknown) -> String -> m SMTReasonUnknown
forall a b. (a -> b) -> a -> b
$ String
"Unexpected reason value received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SMTInfoResponse -> String
forall a. Show a => a -> String
show SMTInfoResponse
ru

-- | Generalization of 'Data.SBV.Control.ensureSat'
ensureSat :: (MonadIO m, MonadQuery m) => m ()
ensureSat :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m ()
ensureSat = do cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
               cs <- checkSatUsing $ satCmd cfg
               case cs of
                 CheckSatResult
Sat    -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                 DSat{} -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                 CheckSatResult
Unk    -> do s <- m SMTReasonUnknown
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
                              error $ unlines [ ""
                                              , "*** Data.SBV.ensureSat: Solver reported Unknown!"
                                              , "*** Reason: " ++ show s
                                              ]
                 CheckSatResult
Unsat  -> String -> m ()
forall a. HasCallStack => String -> a
error String
"Data.SBV.ensureSat: Solver reported Unsat!"

-- | Generalization of 'Data.SBV.Control.getSMTResult'
getSMTResult :: (MonadIO m, MonadQuery m) => m SMTResult
getSMTResult :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
getSMTResult = do cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
                  cs  <- checkSat
                  case cs of
                    CheckSatResult
Unsat  -> SMTConfig -> Maybe [String] -> SMTResult
Unsatisfiable SMTConfig
cfg   (Maybe [String] -> SMTResult) -> m (Maybe [String]) -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe [String])
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m (Maybe [String])
getUnsatCoreIfRequested
                    CheckSatResult
Sat    -> SMTConfig -> SMTModel -> SMTResult
Satisfiable   SMTConfig
cfg   (SMTModel -> SMTResult) -> m SMTModel -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTModel
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
                    DSat Maybe String
p -> SMTConfig -> Maybe String -> SMTModel -> SMTResult
DeltaSat      SMTConfig
cfg Maybe String
p (SMTModel -> SMTResult) -> m SMTModel -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTModel
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
                    CheckSatResult
Unk    -> SMTConfig -> SMTReasonUnknown -> SMTResult
Unknown       SMTConfig
cfg   (SMTReasonUnknown -> SMTResult)
-> m SMTReasonUnknown -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTReasonUnknown
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason

-- | Classify a model based on whether it has unbound objectives or not.
classifyModel :: SMTConfig -> SMTModel -> SMTResult
classifyModel :: SMTConfig -> SMTModel -> SMTResult
classifyModel SMTConfig
cfg SMTModel
m
  | ((String, GeneralizedCV) -> Bool)
-> [(String, GeneralizedCV)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String, GeneralizedCV) -> Bool
forall {a}. (a, GeneralizedCV) -> Bool
isExt (SMTModel -> [(String, GeneralizedCV)]
modelObjectives SMTModel
m) = SMTConfig -> SMTModel -> SMTResult
SatExtField SMTConfig
cfg SMTModel
m
  | Bool
True                          = SMTConfig -> SMTModel -> SMTResult
Satisfiable SMTConfig
cfg SMTModel
m
  where isExt :: (a, GeneralizedCV) -> Bool
isExt (a
_, GeneralizedCV
v) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ GeneralizedCV -> Bool
isRegularCV GeneralizedCV
v

-- | Generalization of 'Data.SBV.Control.getLexicographicOptResults'
getLexicographicOptResults :: (MonadIO m, MonadQuery m) => m SMTResult
getLexicographicOptResults :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTResult
getLexicographicOptResults = do cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
                                cs  <- checkSat
                                case cs of
                                  CheckSatResult
Unsat  -> SMTConfig -> Maybe [String] -> SMTResult
Unsatisfiable SMTConfig
cfg (Maybe [String] -> SMTResult) -> m (Maybe [String]) -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe [String])
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m (Maybe [String])
getUnsatCoreIfRequested
                                  CheckSatResult
Sat    -> SMTConfig -> SMTModel -> SMTResult
classifyModel SMTConfig
cfg (SMTModel -> SMTResult) -> m SMTModel -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTModel
getModelWithObjectives
                                  DSat{} -> SMTConfig -> SMTModel -> SMTResult
classifyModel SMTConfig
cfg (SMTModel -> SMTResult) -> m SMTModel -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTModel
getModelWithObjectives
                                  CheckSatResult
Unk    -> SMTConfig -> SMTReasonUnknown -> SMTResult
Unknown       SMTConfig
cfg (SMTReasonUnknown -> SMTResult)
-> m SMTReasonUnknown -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTReasonUnknown
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
   where getModelWithObjectives :: m SMTModel
getModelWithObjectives = do objectiveValues <- m [(String, GeneralizedCV)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, GeneralizedCV)]
getObjectiveValues
                                     m               <- getModel
                                     return m {modelObjectives = objectiveValues}

-- | Generalization of 'Data.SBV.Control.getIndependentOptResults'
getIndependentOptResults :: forall m. (MonadIO m, MonadQuery m) => [String] -> m [(String, SMTResult)]
getIndependentOptResults :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
[String] -> m [(String, SMTResult)]
getIndependentOptResults [String]
objNames = do cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
                                       cs  <- checkSat

                                       case cs of
                                         CheckSatResult
Unsat  -> m (Maybe [String])
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m (Maybe [String])
getUnsatCoreIfRequested m (Maybe [String])
-> (Maybe [String] -> m [(String, SMTResult)])
-> m [(String, SMTResult)]
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Maybe [String]
mbUC -> [(String, SMTResult)] -> m [(String, SMTResult)]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [(String
nm, SMTConfig -> Maybe [String] -> SMTResult
Unsatisfiable SMTConfig
cfg Maybe [String]
mbUC) | String
nm <- [String]
objNames]
                                         CheckSatResult
Sat    -> (SMTModel -> SMTResult) -> m [(String, SMTResult)]
forall {b}. (SMTModel -> b) -> m [(String, b)]
continue (SMTConfig -> SMTModel -> SMTResult
classifyModel SMTConfig
cfg)
                                         DSat{} -> (SMTModel -> SMTResult) -> m [(String, SMTResult)]
forall {b}. (SMTModel -> b) -> m [(String, b)]
continue (SMTConfig -> SMTModel -> SMTResult
classifyModel SMTConfig
cfg)
                                         CheckSatResult
Unk    -> do ur <- SMTConfig -> SMTReasonUnknown -> SMTResult
Unknown SMTConfig
cfg (SMTReasonUnknown -> SMTResult)
-> m SMTReasonUnknown -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTReasonUnknown
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
                                                      return [(nm, ur) | nm <- objNames]

  where continue :: (SMTModel -> b) -> m [(String, b)]
continue SMTModel -> b
classify = do objectiveValues <- m [(String, GeneralizedCV)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, GeneralizedCV)]
getObjectiveValues
                               nms <- zipWithM getIndependentResult [0..] objNames
                               return [(n, classify (m {modelObjectives = objectiveValues})) | (n, m) <- nms]

        getIndependentResult :: Int -> String -> m (String, SMTModel)
        getIndependentResult :: Int -> String -> m (String, SMTModel)
getIndependentResult Int
i String
s = do m <- Maybe Int -> m SMTModel
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> m SMTModel
getModelAtIndex (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i)
                                      return (s, m)

-- | Generalization of 'Data.SBV.Control.getParetoOptResults'
getParetoOptResults :: (MonadIO m, MonadQuery m) => Maybe Int -> m (Bool, [SMTResult])
getParetoOptResults :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> m (Bool, [SMTResult])
getParetoOptResults (Just Int
i)
        | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0             = (Bool, [SMTResult]) -> m (Bool, [SMTResult])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [])
getParetoOptResults Maybe Int
mbN      = do cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
                                  cs  <- checkSat

                                  case cs of
                                    CheckSatResult
Unsat  -> (Bool, [SMTResult]) -> m (Bool, [SMTResult])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [])
                                    CheckSatResult
Sat    -> (SMTModel -> SMTResult) -> m (Bool, [SMTResult])
forall {m :: * -> *} {a}.
(MonadIO m, MonadQuery m) =>
(SMTModel -> a) -> m (Bool, [a])
continue (SMTConfig -> SMTModel -> SMTResult
classifyModel SMTConfig
cfg)
                                    DSat{} -> (SMTModel -> SMTResult) -> m (Bool, [SMTResult])
forall {m :: * -> *} {a}.
(MonadIO m, MonadQuery m) =>
(SMTModel -> a) -> m (Bool, [a])
continue (SMTConfig -> SMTModel -> SMTResult
classifyModel SMTConfig
cfg)
                                    CheckSatResult
Unk    -> do ur <- m SMTReasonUnknown
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
                                                 return (False, [ProofError cfg [show ur] Nothing])

  where continue :: (SMTModel -> a) -> m (Bool, [a])
continue SMTModel -> a
classify = do m <- m SMTModel
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
                               (limReached, fronts) <- getParetoFronts (subtract 1 <$> mbN) [m]
                               return (limReached, reverse (map classify fronts))

        getParetoFronts :: (MonadIO m, MonadQuery m) => Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
        getParetoFronts :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
getParetoFronts (Just Int
i) [SMTModel]
sofar | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = (Bool, [SMTModel]) -> m (Bool, [SMTModel])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [SMTModel]
sofar)
        getParetoFronts Maybe Int
mbi      [SMTModel]
sofar          = do cs <- m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
                                                     let more = m SMTModel
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel m SMTModel
-> (SMTModel -> m (Bool, [SMTModel])) -> m (Bool, [SMTModel])
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SMTModel
m -> Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
getParetoFronts (Int -> Int -> Int
forall a. Num a => a -> a -> a
subtract Int
1 (Int -> Int) -> Maybe Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
mbi) (SMTModel
m SMTModel -> [SMTModel] -> [SMTModel]
forall a. a -> [a] -> [a]
: [SMTModel]
sofar)
                                                     case cs of
                                                       CheckSatResult
Unsat  -> (Bool, [SMTModel]) -> m (Bool, [SMTModel])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [SMTModel]
sofar)
                                                       CheckSatResult
Sat    -> m (Bool, [SMTModel])
more
                                                       DSat{} -> m (Bool, [SMTModel])
more
                                                       CheckSatResult
Unk    -> m (Bool, [SMTModel])
more

-- | Generalization of 'Data.SBV.Control.getModel'
getModel :: (MonadIO m, MonadQuery m) => m SMTModel
getModel :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel = Maybe Int -> m SMTModel
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> m SMTModel
getModelAtIndex Maybe Int
forall a. Maybe a
Nothing

-- | Get a model stored at an index. This is likely very Z3 specific!
getModelAtIndex :: (MonadIO m, MonadQuery m) => Maybe Int -> m SMTModel
getModelAtIndex :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> m SMTModel
getModelAtIndex Maybe Int
mbi = do
    State{runMode} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
    rm <- io $ readIORef runMode
    case rm of
      m :: SBVRunMode
m@SBVRunMode
CodeGen     -> String -> m SMTModel
forall a. HasCallStack => String -> a
error (String -> m SMTModel) -> String -> m SMTModel
forall a b. (a -> b) -> a -> b
$ String
"SBV.getModel: Model is not available in mode: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVRunMode -> String
forall a. Show a => a -> String
show SBVRunMode
m
      m :: SBVRunMode
m@LambdaGen{} -> String -> m SMTModel
forall a. HasCallStack => String -> a
error (String -> m SMTModel) -> String -> m SMTModel
forall a b. (a -> b) -> a -> b
$ String
"SBV.getModel: Model is not available in mode: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVRunMode -> String
forall a. Show a => a -> String
show SBVRunMode
m
      m :: SBVRunMode
m@Concrete{}  -> String -> m SMTModel
forall a. HasCallStack => String -> a
error (String -> m SMTModel) -> String -> m SMTModel
forall a b. (a -> b) -> a -> b
$ String
"SBV.getModel: Model is not available in mode: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVRunMode -> String
forall a. Show a => a -> String
show SBVRunMode
m
      SMTMode{}     -> do
          cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
          uis <- getUIs

          allModelInputs <- getTopLevelInputs
          obsvs          <- getObservables

          inputAssocs <- let grab (NamedSymVar SV
sv Name
nm) = let wrap :: b -> (SV, (Name, b))
wrap !b
c = (SV
sv, (Name
nm, b
c)) in CV -> (SV, (Name, CV))
forall {b}. b -> (SV, (Name, b))
wrap (CV -> (SV, (Name, CV))) -> f CV -> f (SV, (Name, CV))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int -> SV -> f CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> SV -> m CV
getValueCV Maybe Int
mbi SV
sv
                         in mapM grab allModelInputs

          let name     = (c, b) -> c
forall a b. (a, b) -> a
fst ((c, b) -> c) -> ((a, (c, b)) -> (c, b)) -> (a, (c, b)) -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, (c, b)) -> (c, b)
forall a b. (a, b) -> b
snd
              removeSV = (a, b) -> b
forall a b. (a, b) -> b
snd
              prepare  = Seq (SV, (Name, CV)) -> Seq (SV, (Name, CV))
forall a. Ord a => Seq a -> Seq a
S.unstableSort (Seq (SV, (Name, CV)) -> Seq (SV, (Name, CV)))
-> (Seq (SV, (Name, CV)) -> Seq (SV, (Name, CV)))
-> Seq (SV, (Name, CV))
-> Seq (SV, (Name, CV))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SV, (Name, CV)) -> Bool)
-> Seq (SV, (Name, CV)) -> Seq (SV, (Name, CV))
forall a. (a -> Bool) -> Seq a -> Seq a
S.filter (Bool -> Bool
not (Bool -> Bool)
-> ((SV, (Name, CV)) -> Bool) -> (SV, (Name, CV)) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTConfig -> String -> Bool
mustIgnoreVar SMTConfig
cfg (String -> Bool)
-> ((SV, (Name, CV)) -> String) -> (SV, (Name, CV)) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
T.unpack (Name -> String)
-> ((SV, (Name, CV)) -> Name) -> (SV, (Name, CV)) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SV, (Name, CV)) -> Name
forall {a} {c} {b}. (a, (c, b)) -> c
name)
              assocs   = ((SV, (Name, CV)) -> (Name, CV))
-> Seq (SV, (Name, CV)) -> Seq (Name, CV)
forall a b. (a -> b) -> Seq a -> Seq b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (SV, (Name, CV)) -> (Name, CV)
forall a b. (a, b) -> b
removeSV (Seq (SV, (Name, CV)) -> Seq (SV, (Name, CV))
prepare Seq (SV, (Name, CV))
inputAssocs) Seq (Name, CV) -> Seq (Name, CV) -> Seq (Name, CV)
forall a. Semigroup a => a -> a -> a
<> [(Name, CV)] -> Seq (Name, CV)
forall a. [a] -> Seq a
S.fromList (((Name, CV) -> Name) -> [(Name, CV)] -> [(Name, CV)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (Name, CV) -> Name
forall a b. (a, b) -> a
fst [(Name, CV)]
obsvs)

          -- collect UIs, and UI functions if requested
          let uiFuns = [(String, (Bool, Maybe [String], SBVType))
ui | ui :: (String, (Bool, Maybe [String], SBVType))
ui@(String
nm, (Bool
_, Maybe [String]
_, SBVType [Kind]
as)) <- [(String, (Bool, Maybe [String], SBVType))]
uis, [Kind] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
as Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>  Int
1, SMTConfig -> Bool
allSatTrackUFs SMTConfig
cfg, Bool -> Bool
not (SMTConfig -> String -> Bool
mustIgnoreVar SMTConfig
cfg String
nm)] -- functions have at least two things in their type!
              uiRegs = [(String, (Bool, Maybe [String], SBVType))
ui | ui :: (String, (Bool, Maybe [String], SBVType))
ui@(String
nm, (Bool
_, Maybe [String]
_, SBVType [Kind]
as)) <- [(String, (Bool, Maybe [String], SBVType))]
uis, [Kind] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1,                     Bool -> Bool
not (SMTConfig -> String -> Bool
mustIgnoreVar SMTConfig
cfg String
nm)]

          -- If there are uninterpreted functions, arrange so that z3's pretty-printer flattens things out
          -- as cex's tend to get larger
          unless (null uiFuns) $
             let solverCaps = SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)
             in case supportsFlattenedModels solverCaps of
                  Maybe [String]
Nothing   -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                  Just [String]
cmds -> (String -> m ()) -> [String] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True) [String]
cmds

          bindings <- let get i :: NamedSymVar
i@(NamedSymVar -> SV
getSV -> SV
sv) = case ((SV, (Name, CV)) -> SV)
-> SV -> Seq (SV, (Name, CV)) -> Maybe (SV, (Name, CV))
forall a. Eq a => (a -> SV) -> SV -> Seq a -> Maybe a
lookupInput (SV, (Name, CV)) -> SV
forall a b. (a, b) -> a
fst SV
sv Seq (SV, (Name, CV))
inputAssocs of
                                                  Just (SV
_, (Name
_, CV
cv)) -> (NamedSymVar, CV) -> m (NamedSymVar, CV)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (NamedSymVar
i, CV
cv)
                                                  Maybe (SV, (Name, CV))
Nothing           -> do cv <- Maybe Int -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> SV -> m CV
getValueCV Maybe Int
mbi SV
sv
                                                                          return (i, cv)

                      in if validationRequested cfg
                         then Just <$> mapM get allModelInputs
                         else return Nothing

          uiFunVals <- mapM (\ui :: (String, (Bool, Maybe [String], SBVType))
ui@(String
nm, (Bool
c, Maybe [String]
_, SBVType
t)) -> (\Either String ([([CV], CV)], CV)
a -> (String
nm, (Bool
c, SBVType
t, Either String ([([CV], CV)], CV)
a))) (Either String ([([CV], CV)], CV)
 -> (String, (Bool, SBVType, Either String ([([CV], CV)], CV))))
-> m (Either String ([([CV], CV)], CV))
-> m (String, (Bool, SBVType, Either String ([([CV], CV)], CV)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
-> (String, (Bool, Maybe [String], SBVType))
-> m (Either String ([([CV], CV)], CV))
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int
-> (String, (Bool, Maybe [String], SBVType))
-> m (Either String ([([CV], CV)], CV))
getUIFunCVAssoc Maybe Int
mbi (String, (Bool, Maybe [String], SBVType))
ui) uiFuns

          uiVals    <- mapM (\ui :: (String, (Bool, Maybe [String], SBVType))
ui@(String
nm, (Bool
_, Maybe [String]
_, SBVType
_)) -> (String
nm,) (CV -> (String, CV)) -> m CV -> m (String, CV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int -> (String, (Bool, Maybe [String], SBVType)) -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> (String, (Bool, Maybe [String], SBVType)) -> m CV
getUICVal Maybe Int
mbi (String, (Bool, Maybe [String], SBVType))
ui) uiRegs

          return $ unBarModel $ SMTModel { modelObjectives = []
                                         , modelBindings   = toList <$> bindings
                                         , modelAssocs     = uiVals ++ toList (first T.unpack <$> assocs)
                                         , modelUIFuns     = uiFunVals
                                         }

-- | Just after a check-sat is issued, collect objective values. Used
-- internally only, not exposed to the user.
getObjectiveValues :: forall m. (MonadIO m, MonadQuery m) => m [(String, GeneralizedCV)]
getObjectiveValues :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, GeneralizedCV)]
getObjectiveValues = do let cmd :: String
cmd = String
"(get-objectives)"

                            bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getObjectiveValues" String
cmd String
"a list of objective values" Maybe [String]
forall a. Maybe a
Nothing

                        r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd

                        inputs <- F.toList <$> getTopLevelInputs

                        parse r bad $ \case EApp (ECon String
"objectives" : [SExpr]
es) -> [Maybe (String, GeneralizedCV)] -> [(String, GeneralizedCV)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (String, GeneralizedCV)] -> [(String, GeneralizedCV)])
-> m [Maybe (String, GeneralizedCV)] -> m [(String, GeneralizedCV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (SExpr -> m (Maybe (String, GeneralizedCV)))
-> [SExpr] -> m [Maybe (String, GeneralizedCV)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((forall a. Maybe [String] -> m a)
-> [NamedSymVar] -> SExpr -> m (Maybe (String, GeneralizedCV))
getObjValue (String -> Maybe [String] -> m a
forall {a}. String -> Maybe [String] -> m a
bad String
r) [NamedSymVar]
inputs) [SExpr]
es
                                            SExpr
_                             -> String -> Maybe [String] -> m [(String, GeneralizedCV)]
forall {a}. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing

  where -- | Parse an objective value out.
        getObjValue :: (forall a. Maybe [String] -> m a) -> [NamedSymVar] -> SExpr -> m (Maybe (String, GeneralizedCV))
        getObjValue :: (forall a. Maybe [String] -> m a)
-> [NamedSymVar] -> SExpr -> m (Maybe (String, GeneralizedCV))
getObjValue forall a. Maybe [String] -> m a
bailOut [NamedSymVar]
inputs SExpr
expr =
                case SExpr
expr of
                  EApp [SExpr
_]          -> Maybe (String, GeneralizedCV) -> m (Maybe (String, GeneralizedCV))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (String, GeneralizedCV)
forall a. Maybe a
Nothing            -- Happens when a soft-assertion has no associated group.
                  EApp [ECon String
nm, SExpr
v] -> String -> SExpr -> m (Maybe (String, GeneralizedCV))
locate String
nm SExpr
v               -- Regular case
                  SExpr
_                 -> String -> m (Maybe (String, GeneralizedCV))
forall {a}. String -> m a
dontUnderstand (SExpr -> String
forall a. Show a => a -> String
show SExpr
expr)

          where locate :: String -> SExpr -> m (Maybe (String, GeneralizedCV))
locate String
nm SExpr
v = case [NamedSymVar] -> Maybe NamedSymVar
forall a. [a] -> Maybe a
listToMaybe [NamedSymVar
p | p :: NamedSymVar
p@(NamedSymVar SV
sv Name
_) <- [NamedSymVar]
inputs, SV -> String
forall a. Show a => a -> String
show SV
sv String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
nm] of
                                Maybe NamedSymVar
Nothing                          -> Maybe (String, GeneralizedCV) -> m (Maybe (String, GeneralizedCV))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (String, GeneralizedCV)
forall a. Maybe a
Nothing -- Happens when the soft assertion has a group-id that's not one of the input names
                                Just (NamedSymVar SV
sv Name
actualName) -> SV -> SExpr -> m GeneralizedCV
grab SV
sv SExpr
v m GeneralizedCV
-> (GeneralizedCV -> m (Maybe (String, GeneralizedCV)))
-> m (Maybe (String, GeneralizedCV))
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \GeneralizedCV
val -> Maybe (String, GeneralizedCV) -> m (Maybe (String, GeneralizedCV))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (String, GeneralizedCV)
 -> m (Maybe (String, GeneralizedCV)))
-> Maybe (String, GeneralizedCV)
-> m (Maybe (String, GeneralizedCV))
forall a b. (a -> b) -> a -> b
$ (String, GeneralizedCV) -> Maybe (String, GeneralizedCV)
forall a. a -> Maybe a
Just (Name -> String
T.unpack Name
actualName, GeneralizedCV
val)

                dontUnderstand :: String -> m a
dontUnderstand String
s = Maybe [String] -> m a
forall a. Maybe [String] -> m a
bailOut (Maybe [String] -> m a) -> Maybe [String] -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just [ String
"Unable to understand solver output."
                                                  , String
"While trying to process: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
                                                  ]

                grab :: SV -> SExpr -> m GeneralizedCV
                grab :: SV -> SExpr -> m GeneralizedCV
grab SV
s SExpr
topExpr
                  | Just CV
v <- Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
k SExpr
topExpr = GeneralizedCV -> m GeneralizedCV
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (GeneralizedCV -> m GeneralizedCV)
-> GeneralizedCV -> m GeneralizedCV
forall a b. (a -> b) -> a -> b
$ CV -> GeneralizedCV
RegularCV CV
v
                  | Bool
True                                   = ExtCV -> GeneralizedCV
ExtendedCV (ExtCV -> GeneralizedCV) -> m ExtCV -> m GeneralizedCV
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> m ExtCV
cvt (SExpr -> SExpr
simplify SExpr
topExpr)
                  where k :: Kind
k = SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
s

                        -- Convert to an extended expression. Hopefully complete!
                        cvt :: SExpr -> m ExtCV
                        cvt :: SExpr -> m ExtCV
cvt (ECon String
"oo")                    = ExtCV -> m ExtCV
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtCV -> m ExtCV) -> ExtCV -> m ExtCV
forall a b. (a -> b) -> a -> b
$ Kind -> ExtCV
Infinite  Kind
k
                        cvt (ECon String
"epsilon")               = ExtCV -> m ExtCV
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtCV -> m ExtCV) -> ExtCV -> m ExtCV
forall a b. (a -> b) -> a -> b
$ Kind -> ExtCV
Epsilon   Kind
k
                        cvt (EApp [ECon String
"interval", SExpr
x, SExpr
y]) =          ExtCV -> ExtCV -> ExtCV
Interval  (ExtCV -> ExtCV -> ExtCV) -> m ExtCV -> m (ExtCV -> ExtCV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> m ExtCV
cvt SExpr
x m (ExtCV -> ExtCV) -> m ExtCV -> m ExtCV
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> m ExtCV
cvt SExpr
y
                        cvt (ENum    (Integer
i, Maybe Int
_))               = ExtCV -> m ExtCV
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtCV -> m ExtCV) -> ExtCV -> m ExtCV
forall a b. (a -> b) -> a -> b
$ CV -> ExtCV
BoundedCV (CV -> ExtCV) -> CV -> ExtCV
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k Integer
i
                        cvt (EReal   AlgReal
r)                    = ExtCV -> m ExtCV
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtCV -> m ExtCV) -> ExtCV -> m ExtCV
forall a b. (a -> b) -> a -> b
$ CV -> ExtCV
BoundedCV (CV -> ExtCV) -> CV -> ExtCV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ AlgReal -> CVal
CAlgReal AlgReal
r
                        cvt (EFloat  Float
f)                    = ExtCV -> m ExtCV
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtCV -> m ExtCV) -> ExtCV -> m ExtCV
forall a b. (a -> b) -> a -> b
$ CV -> ExtCV
BoundedCV (CV -> ExtCV) -> CV -> ExtCV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ Float -> CVal
CFloat   Float
f
                        cvt (EDouble Double
d)                    = ExtCV -> m ExtCV
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtCV -> m ExtCV) -> ExtCV -> m ExtCV
forall a b. (a -> b) -> a -> b
$ CV -> ExtCV
BoundedCV (CV -> ExtCV) -> CV -> ExtCV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ Double -> CVal
CDouble  Double
d
                        cvt (EApp [ECon String
"+", SExpr
x, SExpr
y])        =          ExtCV -> ExtCV -> ExtCV
AddExtCV (ExtCV -> ExtCV -> ExtCV) -> m ExtCV -> m (ExtCV -> ExtCV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> m ExtCV
cvt SExpr
x m (ExtCV -> ExtCV) -> m ExtCV -> m ExtCV
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> m ExtCV
cvt SExpr
y
                        cvt (EApp [ECon String
"*", SExpr
x, SExpr
y])        =          ExtCV -> ExtCV -> ExtCV
MulExtCV (ExtCV -> ExtCV -> ExtCV) -> m ExtCV -> m (ExtCV -> ExtCV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> m ExtCV
cvt SExpr
x m (ExtCV -> ExtCV) -> m ExtCV -> m ExtCV
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> m ExtCV
cvt SExpr
y
                        -- Nothing else should show up, hopefully!
                        cvt SExpr
e = String -> m ExtCV
forall {a}. String -> m a
dontUnderstand (SExpr -> String
forall a. Show a => a -> String
show SExpr
e)

                        -- drop the pesky to_real's that Z3 produces.. Cool but useless.
                        simplify :: SExpr -> SExpr
                        simplify :: SExpr -> SExpr
simplify (EApp [ECon String
"to_real", SExpr
n]) = SExpr
n
                        simplify (EApp [SExpr]
xs)                  = [SExpr] -> SExpr
EApp ((SExpr -> SExpr) -> [SExpr] -> [SExpr]
forall a b. (a -> b) -> [a] -> [b]
map SExpr -> SExpr
simplify [SExpr]
xs)
                        simplify SExpr
e                          = SExpr
e

-- | Generalization of 'Data.SBV.Control.checkSatAssuming'
checkSatAssuming :: (MonadIO m, MonadQuery m) => [SBool] -> m CheckSatResult
checkSatAssuming :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
[SBool] -> m CheckSatResult
checkSatAssuming [SBool]
sBools = (CheckSatResult, Maybe [SBool]) -> CheckSatResult
forall a b. (a, b) -> a
fst ((CheckSatResult, Maybe [SBool]) -> CheckSatResult)
-> m (CheckSatResult, Maybe [SBool]) -> m CheckSatResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
checkSatAssumingHelper Bool
False [SBool]
sBools

-- | Generalization of 'Data.SBV.Control.checkSatAssumingWithUnsatisfiableSet'
checkSatAssumingWithUnsatisfiableSet :: (MonadIO m, MonadQuery m) => [SBool] -> m (CheckSatResult, Maybe [SBool])
checkSatAssumingWithUnsatisfiableSet :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
[SBool] -> m (CheckSatResult, Maybe [SBool])
checkSatAssumingWithUnsatisfiableSet = Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
checkSatAssumingHelper Bool
True

-- | Helper for the two variants of checkSatAssuming we have. Internal only.
checkSatAssumingHelper :: (MonadIO m, MonadQuery m) => Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
checkSatAssumingHelper :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> [SBool] -> m (CheckSatResult, Maybe [SBool])
checkSatAssumingHelper Bool
getAssumptions [SBool]
sBools = do
        -- sigh.. SMT-Lib requires the values to be literals only. So, create proxies.
        let mkAssumption :: State -> IO [(String, [String], (String, SBool))]
mkAssumption State
st = do swsOriginal <- (SBool -> IO (SV, SBool)) -> [SBool] -> IO [(SV, SBool)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\SBool
sb -> do sv <- State -> SBool -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBool
sb
                                                                return (sv, sb)) [SBool]
sBools

                                 -- drop duplicates and trues
                                 let swbs = [(SV, SBool)
p | p :: (SV, SBool)
p@(SV
sv, SBool
_) <- ((SV, SBool) -> (SV, SBool) -> Bool)
-> [(SV, SBool)] -> [(SV, SBool)]
forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
(==) (SV -> SV -> Bool)
-> ((SV, SBool) -> SV) -> (SV, SBool) -> (SV, SBool) -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (SV, SBool) -> SV
forall a b. (a, b) -> a
fst) [(SV, SBool)]
swsOriginal, SV
sv SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
/= SV
trueSV]

                                 -- get a unique proxy name for each
                                 uniqueSWBs <- mapM (\(SV
sv, SBool
sb) -> do unique <- State -> IO Int
incrementInternalCounter State
st
                                                                     return (sv, (unique, sb))) swbs

                                 let translate (a
sv, (a
unique, b
sb)) = (String
nm, [String]
decls, (String
proxy, b
sb))
                                        where nm :: String
nm    = a -> String
forall a. Show a => a -> String
show a
sv
                                              proxy :: String
proxy = String
"__assumption_proxy_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
unique
                                              decls :: [String]
decls = [ String
"(declare-const " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
proxy String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" Bool)"
                                                      , String
"(assert (= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
proxy String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
                                                      ]

                                 return $ map translate uniqueSWBs

        assumptions <- (State -> IO [(String, [String], (String, SBool))])
-> m [(String, [String], (String, SBool))]
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext State -> IO [(String, [String], (String, SBool))]
mkAssumption

        let (origNames, declss, proxyMap) = unzip3 assumptions

        let cmd = String
"(check-sat-assuming (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (((String, SBool) -> String) -> [(String, SBool)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, SBool) -> String
forall a b. (a, b) -> a
fst [(String, SBool)]
proxyMap) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
            bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"checkSatAssuming" String
cmd String
"one of sat/unsat/unknown"
                           (Maybe [String] -> String -> Maybe [String] -> m a)
-> Maybe [String] -> String -> Maybe [String] -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just [ String
"Make sure you use:"
                                  , String
""
                                  , String
"       setOption $ ProduceUnsatAssumptions True"
                                  , String
""
                                  , String
"to tell the solver to produce unsat assumptions."
                                  ]

        mapM_ (send True) $ concat declss
        r <- ask cmd

        let grabUnsat
             | Bool
getAssumptions = do as <- [String] -> [(String, SBool)] -> m [SBool]
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
[String] -> [(String, a)] -> m [a]
getUnsatAssumptions [String]
origNames [(String, SBool)]
proxyMap
                                   return (Unsat, Just as)
             | Bool
True           = (CheckSatResult, Maybe [SBool])
-> m (CheckSatResult, Maybe [SBool])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckSatResult
Unsat, Maybe [SBool]
forall a. Maybe a
Nothing)

        parse r bad $ \case ECon String
"sat"     -> (CheckSatResult, Maybe [SBool])
-> m (CheckSatResult, Maybe [SBool])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckSatResult
Sat, Maybe [SBool]
forall a. Maybe a
Nothing)
                            ECon String
"unsat"   -> m (CheckSatResult, Maybe [SBool])
grabUnsat
                            ECon String
"unknown" -> (CheckSatResult, Maybe [SBool])
-> m (CheckSatResult, Maybe [SBool])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (CheckSatResult
Unk, Maybe [SBool]
forall a. Maybe a
Nothing)
                            SExpr
_              -> String -> Maybe [String] -> m (CheckSatResult, Maybe [SBool])
forall {a}. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing

-- | Generalization of 'Data.SBV.Control.getAssertionStackDepth'
getAssertionStackDepth :: (MonadIO m, MonadQuery m) => m Int
getAssertionStackDepth :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m Int
getAssertionStackDepth = QueryState -> Int
queryAssertionStackDepth (QueryState -> Int) -> m QueryState -> m Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState

-- | Upon a pop, we need to restore all arrays and tables. See: http://github.com/LeventErkok/sbv/issues/374
restoreTablesAndArrays :: (MonadIO m, MonadQuery m) => m ()
restoreTablesAndArrays :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m ()
restoreTablesAndArrays = do st <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState

                            tCount <- M.size  <$> (io . readIORef) (rtblMap   st)

                            let inits = [ String
"table"  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_initializer" | Int
i <- [Int
0 .. Int
tCount Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]

                            case inits of
                              []  -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()   -- Nothing to do
                              [String
x] -> Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                              [String]
xs  -> Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"(assert (and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"

-- | Generalization of 'Data.SBV.Control.inNewAssertionStack'
inNewAssertionStack :: (MonadIO m, MonadQuery m) => m a -> m a
inNewAssertionStack :: forall (m :: * -> *) a. (MonadIO m, MonadQuery m) => m a -> m a
inNewAssertionStack m a
q = do Int -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
push Int
1
                           r <- m a
q
                           pop 1
                           return r

-- | Generalization of 'Data.SBV.Control.push'
push :: (MonadIO m, MonadQuery m) => Int -> m ()
push :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
push Int
i
 | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = String -> m ()
forall a. HasCallStack => String -> a
error (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: push requires a strictly positive level argument, received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
 | Bool
True   = do depth <- m Int
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m Int
getAssertionStackDepth
               send True $ "(push " ++ show i ++ ")"
               modifyQueryState $ \QueryState
s -> QueryState
s{queryAssertionStackDepth = depth + i}

-- | Generalization of 'Data.SBV.Control.pop'
pop :: (MonadIO m, MonadQuery m) => Int -> m ()
pop :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
pop Int
i
 | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = String -> m ()
forall a. HasCallStack => String -> a
error (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: pop requires a strictly positive level argument, received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
 | Bool
True   = do depth <- m Int
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m Int
getAssertionStackDepth
               if i > depth
                  then error $ "Data.SBV: Illegally trying to pop " ++ shl i ++ ", at current level: " ++ show depth
                  else do QueryState{queryConfig} <- getQueryState
                          if not (supportsGlobalDecls (capabilities (solver queryConfig)))
                             then error $ unlines [ ""
                                                  , "*** Data.SBV: Backend solver does not support global-declarations."
                                                  , "***           Hence, calls to 'pop' are not supported."
                                                  , "***"
                                                  , "*** Request this as a feature for the underlying solver!"
                                                  ]
                             else do send True $ "(pop " ++ show i ++ ")"
                                     restoreTablesAndArrays
                                     modifyQueryState $ \QueryState
s -> QueryState
s{queryAssertionStackDepth = depth - i}
   where shl :: a -> String
shl a
1 = String
"one level"
         shl a
n = a -> String
forall a. Show a => a -> String
show a
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" levels"

-- | Generalization of 'Data.SBV.Control.caseSplit'
caseSplit :: (MonadIO m, MonadQuery m) => Bool -> [(String, SBool)] -> m (Maybe (String, SMTResult))
caseSplit :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> [(String, SBool)] -> m (Maybe (String, SMTResult))
caseSplit Bool
printCases [(String, SBool)]
cases = do cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
                                go cfg (cases ++ [("Coverage", sNot (sOr (map snd cases)))])
  where msg :: String -> m ()
msg = Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
printCases (m () -> m ()) -> (String -> m ()) -> String -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> (String -> IO ()) -> String -> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn

        go :: SMTConfig -> [(String, SBool)] -> m (Maybe (String, SMTResult))
go SMTConfig
_ []            = Maybe (String, SMTResult) -> m (Maybe (String, SMTResult))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (String, SMTResult)
forall a. Maybe a
Nothing
        go SMTConfig
cfg ((String
n,SBool
c):[(String, SBool)]
ncs) = do let notify :: String -> m ()
notify String
s = String -> m ()
msg (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Case " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s

                                String -> m ()
notify String
"Starting"
                                r <- [SBool] -> m CheckSatResult
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
[SBool] -> m CheckSatResult
checkSatAssuming [SBool
c]

                                case r of
                                  CheckSatResult
Unsat    -> do String -> m ()
notify String
"Unsatisfiable"
                                                 SMTConfig -> [(String, SBool)] -> m (Maybe (String, SMTResult))
go SMTConfig
cfg [(String, SBool)]
ncs

                                  CheckSatResult
Sat      -> do String -> m ()
notify String
"Satisfiable"
                                                 res <- SMTConfig -> SMTModel -> SMTResult
Satisfiable SMTConfig
cfg (SMTModel -> SMTResult) -> m SMTModel -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTModel
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
                                                 return $ Just (n, res)

                                  DSat Maybe String
mbP -> do String -> m ()
notify (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Delta satisfiable" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (String
" (precision: " String -> String -> String
forall a. [a] -> [a] -> [a]
++) Maybe String
mbP
                                                 res <- SMTConfig -> Maybe String -> SMTModel -> SMTResult
DeltaSat SMTConfig
cfg Maybe String
mbP (SMTModel -> SMTResult) -> m SMTModel -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTModel
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
                                                 return $ Just (n, res)

                                  CheckSatResult
Unk      -> do String -> m ()
notify String
"Unknown"
                                                 res <- SMTConfig -> SMTReasonUnknown -> SMTResult
Unknown SMTConfig
cfg (SMTReasonUnknown -> SMTResult)
-> m SMTReasonUnknown -> m SMTResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTReasonUnknown
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
                                                 return $ Just (n, res)

-- | Generalization of 'Data.SBV.Control.resetAssertions'
resetAssertions :: (MonadIO m, MonadQuery m) => m ()
resetAssertions :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m ()
resetAssertions = do Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True String
"(reset-assertions)"
                     (QueryState -> QueryState) -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(QueryState -> QueryState) -> m ()
modifyQueryState ((QueryState -> QueryState) -> m ())
-> (QueryState -> QueryState) -> m ()
forall a b. (a -> b) -> a -> b
$ \QueryState
s -> QueryState
s{ queryAssertionStackDepth = 0 }

                     -- Make sure we restore tables and arrays after resetAssertions: See: https://github.com/LeventErkok/sbv/issues/535
                     m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m ()
restoreTablesAndArrays

-- | Generalization of 'Data.SBV.Control.echo'
echo :: (MonadIO m, MonadQuery m) => String -> m ()
echo :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => String -> m ()
echo String
s = do let cmd :: String
cmd = String
"(echo \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
sanitize String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\")"

            -- we send the command, but otherwise ignore the response
            -- note that 'send True/False' would be incorrect here. 'send True' would
            -- require a success response. 'send False' would fail to consume the
            -- output. But 'ask' does the right thing! It gets "some" response,
            -- and forgets about it immediately.
            _ <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd

            return ()
  where sanitize :: Char -> String
sanitize Char
'"'  = String
"\"\""  -- quotes need to be duplicated
        sanitize Char
c    = [Char
c]

-- | Generalization of 'Data.SBV.Control.exit'
exit :: (MonadIO m, MonadQuery m) => m ()
exit :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m ()
exit = do Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True String
"(exit)"
          (QueryState -> QueryState) -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(QueryState -> QueryState) -> m ()
modifyQueryState ((QueryState -> QueryState) -> m ())
-> (QueryState -> QueryState) -> m ()
forall a b. (a -> b) -> a -> b
$ \QueryState
s -> QueryState
s{queryAssertionStackDepth = 0}

-- | Generalization of 'Data.SBV.Control.getUnsatCore'
getUnsatCore :: (MonadIO m, MonadQuery m) => m [String]
getUnsatCore :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m [String]
getUnsatCore = do
        let cmd :: String
cmd = String
"(get-unsat-core)"
            bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getUnsatCore" String
cmd String
"an unsat-core response"
                           (Maybe [String] -> String -> Maybe [String] -> m a)
-> Maybe [String] -> String -> Maybe [String] -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just [ String
"Make sure you use:"
                                  , String
""
                                  , String
"       setOption $ ProduceUnsatCores True"
                                  , String
""
                                  , String
"so the solver will be ready to compute unsat cores,"
                                  , String
"and that there is a model by first issuing a 'checkSat' call."
                                  , String
""
                                  , String
"If using z3, you might also optionally want to set:"
                                  , String
""
                                  , String
"       setOption $ OptionKeyword \":smt.core.minimize\" [\"true\"]"
                                  , String
""
                                  , String
"to make sure the unsat core doesn't have irrelevant entries,"
                                  , String
"though this might incur a performance penalty."


                                  ]

        r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd

        parse r bad $ \case
           EApp [SExpr]
es | Just [String]
xs <- (SExpr -> Maybe String) -> [SExpr] -> Maybe [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SExpr -> Maybe String
fromECon [SExpr]
es -> [String] -> m [String]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> m [String]) -> [String] -> m [String]
forall a b. (a -> b) -> a -> b
$ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
unBar [String]
xs
           SExpr
_                                     -> String -> Maybe [String] -> m [String]
forall {a}. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing

-- | Retrieve the unsat core if it was asked for in the configuration
getUnsatCoreIfRequested :: (MonadIO m, MonadQuery m) => m (Maybe [String])
getUnsatCoreIfRequested :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m (Maybe [String])
getUnsatCoreIfRequested = do
        cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
        if or [b | ProduceUnsatCores b <- solverSetOptions cfg]
           then Just <$> getUnsatCore
           else return Nothing

-- | Generalization of 'Data.SBV.Control.getProof'
getProof :: (MonadIO m, MonadQuery m) => m String
getProof :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m String
getProof = do
        let cmd :: String
cmd = String
"(get-proof)"
            bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getProof" String
cmd String
"a get-proof response"
                           (Maybe [String] -> String -> Maybe [String] -> m a)
-> Maybe [String] -> String -> Maybe [String] -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just [ String
"Make sure you use:"
                                  , String
""
                                  , String
"       setOption $ ProduceProofs True"
                                  , String
""
                                  , String
"to make sure the solver is ready for producing proofs,"
                                  , String
"and that there is a proof by first issuing a 'checkSat' call."
                                  ]


        r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd

        -- we only care about the fact that we can parse the output, so the
        -- result of parsing is ignored.
        parse r bad $ \SExpr
_ -> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return String
r

-- | Generalization of 'Data.SBV.Control.getInterpolantMathSAT'. Use this version with MathSAT.
getInterpolantMathSAT :: (MonadIO m, MonadQuery m) => [String] -> m String
getInterpolantMathSAT :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
[String] -> m String
getInterpolantMathSAT [String]
fs
  | [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
fs
  = String -> m String
forall a. HasCallStack => String -> a
error String
"SBV.getInterpolantMathSAT requires at least one marked constraint, received none!"
  | Bool
True
  = do let bar :: String -> String
bar String
s = Char
'|' Char -> String -> String
forall a. a -> [a] -> [a]
: String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"|"
           cmd :: String
cmd = String
"(get-interpolant (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
bar [String]
fs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
           bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getInterpolant" String
cmd String
"a get-interpolant response"
                          (Maybe [String] -> String -> Maybe [String] -> m a)
-> Maybe [String] -> String -> Maybe [String] -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just [ String
"Make sure you use:"
                                 , String
""
                                 , String
"       setOption $ ProduceInterpolants True"
                                 , String
""
                                 , String
"to make sure the solver is ready for producing interpolants,"
                                 , String
"and that you have used the proper attributes using the"
                                 , String
"constrainWithAttribute function."
                                 ]

       r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd

       parse r bad $ \SExpr
e -> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ Bool -> SExpr -> String
serialize Bool
False SExpr
e


-- | Generalization of 'Data.SBV.Control.getAbduct'.
getAbduct :: (SolverContext m, MonadIO m, MonadQuery m) => Maybe String -> String -> SBool -> m String
getAbduct :: forall (m :: * -> *).
(SolverContext m, MonadIO m, MonadQuery m) =>
Maybe String -> String -> SBool -> m String
getAbduct Maybe String
mbGrammar String
defName SBool
b = do
   s <- (State -> IO SV) -> m SV
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext (State -> SBool -> IO SV
forall a. State -> SBV a -> IO SV
`sbvToSV` SBool
b)
   let cmd = String
"(get-abduct " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
defName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
"" Maybe String
mbGrammar String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
       bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getAbduct" String
cmd String
"a get-abduct response" Maybe [String]
forall a. Maybe a
Nothing

   r <- ask cmd

   parse r bad $ \SExpr
e -> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ Bool -> SExpr -> String
serialize Bool
False SExpr
e

-- | Generalization of 'Data.SBV.Control.getAbductNext'.
getAbductNext :: (MonadIO m, MonadQuery m) => m String
getAbductNext :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m String
getAbductNext = do
   let cmd :: String
cmd = String
"(get-abduct-next)"
       bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getAbductNext" String
cmd String
"a get-abduct-next response" Maybe [String]
forall a. Maybe a
Nothing

   r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd

   parse r bad $ \SExpr
e -> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ Bool -> SExpr -> String
serialize Bool
False SExpr
e

-- | Generalization of 'Data.SBV.Control.getInterpolantZ3'. Use this version with Z3.
getInterpolantZ3 :: (MonadIO m, MonadQuery m) => [SBool] -> m String
getInterpolantZ3 :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
[SBool] -> m String
getInterpolantZ3 [SBool]
fs
  | [SBool] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBool]
fs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2
  = String -> m String
forall a. HasCallStack => String -> a
error (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ String
"SBV.getInterpolantZ3 requires at least two booleans, received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SBool] -> String
forall a. Show a => a -> String
show [SBool]
fs
  | Bool
True
  = do ss <- let fAll :: [SBV a] -> [SV] -> m [SV]
fAll []     [SV]
sofar = [SV] -> m [SV]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([SV] -> m [SV]) -> [SV] -> m [SV]
forall a b. (a -> b) -> a -> b
$ [SV] -> [SV]
forall a. [a] -> [a]
reverse [SV]
sofar
                 fAll (SBV a
b:[SBV a]
bs) [SV]
sofar = do sv <- (State -> IO SV) -> m SV
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext (State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
`sbvToSV` SBV a
b)
                                        fAll bs (sv : sofar)
             in [SBool] -> [SV] -> m [SV]
forall {m :: * -> *} {a}.
(MonadIO m, MonadQuery m) =>
[SBV a] -> [SV] -> m [SV]
fAll [SBool]
fs []

       let cmd = String
"(get-interpolant " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
forall a. Show a => a -> String
show [SV]
ss) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
           bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getInterpolant" String
cmd String
"a get-interpolant response" Maybe [String]
forall a. Maybe a
Nothing

       r <- ask cmd

       parse r bad $ \SExpr
e -> String -> m String
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ Bool -> SExpr -> String
serialize Bool
False SExpr
e

-- | Generalization of 'Data.SBV.Control.getAssertions'
getAssertions :: (MonadIO m, MonadQuery m) => m [String]
getAssertions :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m [String]
getAssertions = do
        let cmd :: String
cmd = String
"(get-assertions)"
            bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getAssertions" String
cmd String
"a get-assertions response"
                           (Maybe [String] -> String -> Maybe [String] -> m a)
-> Maybe [String] -> String -> Maybe [String] -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just [ String
"Make sure you use:"
                                  , String
""
                                  , String
"       setOption $ ProduceAssertions True"
                                  , String
""
                                  , String
"to make sure the solver is ready for producing assertions."
                                  ]

            render :: SExpr -> String
render = Bool -> SExpr -> String
serialize Bool
False

        r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd

        parse r bad $ \SExpr
pe -> case SExpr
pe of
                                EApp [SExpr]
xs -> [String] -> m [String]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> m [String]) -> [String] -> m [String]
forall a b. (a -> b) -> a -> b
$ (SExpr -> String) -> [SExpr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SExpr -> String
render [SExpr]
xs
                                SExpr
_       -> [String] -> m [String]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [SExpr -> String
render SExpr
pe]

-- | Generalization of 'Data.SBV.Control.getAssignment'
getAssignment :: (MonadIO m, MonadQuery m) => m [(String, Bool)]
getAssignment :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, Bool)]
getAssignment = do
        let cmd :: String
cmd = String
"(get-assignment)"
            bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getAssignment" String
cmd String
"a get-assignment response"
                           (Maybe [String] -> String -> Maybe [String] -> m a)
-> Maybe [String] -> String -> Maybe [String] -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just [ String
"Make sure you use:"
                                  , String
""
                                  , String
"       setOption $ ProduceAssignments True"
                                  , String
""
                                  , String
"to make sure the solver is ready for producing assignments,"
                                  , String
"and that there is a model by first issuing a 'checkSat' call."
                                  ]

            -- we're expecting boolean assignment to labels, essentially
            grab :: SExpr -> Maybe (String, Bool)
grab (EApp [ECon String
s, ENum (Integer
0, Maybe Int
_)]) = (String, Bool) -> Maybe (String, Bool)
forall a. a -> Maybe a
Just (String -> String
unQuote String
s, Bool
False)
            grab (EApp [ECon String
s, ENum (Integer
1, Maybe Int
_)]) = (String, Bool) -> Maybe (String, Bool)
forall a. a -> Maybe a
Just (String -> String
unQuote String
s, Bool
True)
            grab SExpr
_                            = Maybe (String, Bool)
forall a. Maybe a
Nothing

        r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd

        parse r bad $ \case EApp [SExpr]
ps | Just [(String, Bool)]
vs <- (SExpr -> Maybe (String, Bool))
-> [SExpr] -> Maybe [(String, Bool)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM SExpr -> Maybe (String, Bool)
grab [SExpr]
ps -> [(String, Bool)] -> m [(String, Bool)]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [(String, Bool)]
vs
                            SExpr
_                                 -> String -> Maybe [String] -> m [(String, Bool)]
forall {a}. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing

-- | Make an assignment. The type 'Assignment' is abstract, the result is typically passed
-- to 'mkSMTResult':
--
-- @ mkSMTResult [ a |-> 332
--             , b |-> 2.3
--             , c |-> True
--             ]
-- @
--
-- End users should use 'getModel' for automatically constructing models from the current solver state.
-- However, an explicit 'Assignment' might be handy in complex scenarios where a model needs to be
-- created manually.
infix 1 |->
(|->) :: SymVal a => SBV a -> a -> Assignment
SBV SVal
a |-> :: forall a. SymVal a => SBV a -> a -> Assignment
|-> a
v = case a -> SBV a
forall a. SymVal a => a -> SBV a
literal a
v of
                SBV (SVal Kind
_ (Left CV
cv)) -> SVal -> CV -> Assignment
Assign SVal
a CV
cv
                SBV a
r                      -> String -> Assignment
forall a. HasCallStack => String -> a
error (String -> Assignment) -> String -> Assignment
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: Impossible happened in |->: Cannot construct a CV with literal: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBV a -> String
forall a. Show a => a -> String
show SBV a
r

-- | Generalization of 'Data.SBV.Control.mkSMTResult'
-- NB. This function does not allow users to create interpretations for UI-Funs. But that's
-- probably not a good idea anyhow. Also, if you use the 'validateModel' or 'optimizeValidateConstraints' features, SBV will
-- fail on models returned via this function.
mkSMTResult :: (MonadIO m, MonadQuery m) => [Assignment] -> m SMTResult
mkSMTResult :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
[Assignment] -> m SMTResult
mkSMTResult [Assignment]
asgns = do
             QueryState{queryConfig} <- m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState
             inps <- F.toList <$> getTopLevelInputs

             let grabValues State
st = do let extract :: Assignment -> IO (SV, CV)
extract (Assign SVal
s CV
n) = State -> SBV (ZonkAny 0) -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st (SVal -> SBV (ZonkAny 0)
forall a. SVal -> SBV a
SBV SVal
s) IO SV -> (SV -> IO (SV, CV)) -> IO (SV, CV)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SV
sv -> (SV, CV) -> IO (SV, CV)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SV
sv, CV
n)

                                    modelAssignment <- (Assignment -> IO (SV, CV)) -> [Assignment] -> IO [(SV, CV)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Assignment -> IO (SV, CV)
extract [Assignment]
asgns

                                    -- sanity checks
                                    --     - All existentials should be given a value
                                    --     - No duplicates
                                    --     - No bindings to vars that are not inputs
                                    let userSS = ((SV, CV) -> SV) -> [(SV, CV)] -> [SV]
forall a b. (a -> b) -> [a] -> [b]
map (SV, CV) -> SV
forall a b. (a, b) -> a
fst [(SV, CV)]
modelAssignment

                                        missing, extra, dup :: [String]
                                        missing = [Name -> String
T.unpack Name
n | NamedSymVar SV
s Name
n <- [NamedSymVar]
inps, SV
s SV -> [SV] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [SV]
userSS]
                                        extra   = [SV -> String
forall a. Show a => a -> String
show SV
s | SV
s <- [SV]
userSS, SV
s SV -> [SV] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` (NamedSymVar -> SV) -> [NamedSymVar] -> [SV]
forall a b. (a -> b) -> [a] -> [b]
map NamedSymVar -> SV
getSV [NamedSymVar]
inps]
                                        dup     = let walk :: [a] -> [String]
walk []     = []
                                                      walk (a
n:[a]
ns)
                                                        | a
n a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [a]
ns = a -> String
forall a. Show a => a -> String
show a
n String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [a] -> [String]
walk ((a -> Bool) -> [a] -> [a]
forall a. (a -> Bool) -> [a] -> [a]
filter (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
/= a
n) [a]
ns)
                                                        | Bool
True        = [a] -> [String]
walk [a]
ns
                                                  in [SV] -> [String]
forall {a}. (Eq a, Show a) => [a] -> [String]
walk [SV]
userSS

                                    unless (null (missing ++ extra ++ dup)) $ do

                                          let misTag = String
"***   Missing inputs"
                                              dupTag = String
"***   Duplicate bindings"
                                              extTag = String
"***   Extra bindings"

                                              maxLen = [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]
: [String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
misTag | Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
missing)]
                                                               [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
extTag | Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
extra)]
                                                               [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
dupTag | Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
dup)]

                                              align String
s = String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
maxLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s) Char
' ' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": "

                                          error $ unlines $ [""
                                                            , "*** Data.SBV: Query model construction has a faulty assignment."
                                                            , "***"
                                                            ]
                                                         ++ [ align misTag ++ intercalate ", "  missing | not (null missing)]
                                                         ++ [ align extTag ++ intercalate ", "  extra   | not (null extra)  ]
                                                         ++ [ align dupTag ++ intercalate ", "  dup     | not (null dup)    ]
                                                         ++ [ "***"
                                                            , "*** Data.SBV: Check your query result construction!"
                                                            ]

                                    let findName SV
s = case [Name -> String
T.unpack Name
nm | NamedSymVar SV
i Name
nm <- [NamedSymVar]
inps, SV
s SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
i] of
                                                        [String
nm] -> String
nm
                                                        []   -> String -> String
forall a. HasCallStack => String -> a
error String
"*** Data.SBV: Impossible happened: Cannot find " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in the input list"
                                                        [String]
nms  -> String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                                                , String
"*** Data.SBV: Impossible happened: Multiple matches for: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
s
                                                                                , String
"***   Candidates: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
nms
                                                                                ]

                                    return [(findName s, n) | (s, n) <- modelAssignment]

             assocs <- inNewContext grabValues

             let m = SMTModel { modelObjectives :: [(String, GeneralizedCV)]
modelObjectives = []
                              , modelBindings :: Maybe [(NamedSymVar, CV)]
modelBindings   = Maybe [(NamedSymVar, CV)]
forall a. Maybe a
Nothing
                              , modelAssocs :: [(String, CV)]
modelAssocs     = [(String, CV)]
assocs
                              , modelUIFuns :: [(String, (Bool, SBVType, Either String ([([CV], CV)], CV)))]
modelUIFuns     = []
                              }

             return $ Satisfiable queryConfig m

{- HLint ignore getModelAtIndex "Use forM_" -}