-----------------------------------------------------------------------------
-- |
-- 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
     , freshVar, freshVar_, freshArray, freshArray_, freshLambdaArray, freshLambdaArray_
     , push, pop, getAssertionStackDepth
     , inNewAssertionStack, echo, caseSplit, resetAssertions, exit, getAssertions, getValue, 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.IntMap.Strict as IM
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.PrettyNum (showNegativeNumber)

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

-- Remove one pair of surrounding 'c's, if present
noSurrounding :: Char -> String -> String
noSurrounding :: Char -> String -> String
noSurrounding Char
c (Char
c':cs :: String
cs@(Char
_:String
_)) | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
c' Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Char
forall a. HasCallStack => [a] -> a
last String
cs  = String -> String
forall a. HasCallStack => [a] -> [a]
init String
cs
noSurrounding Char
_ String
s                                        = String
s

-- Remove a pair of surrounding quotes
unQuote :: String -> String
unQuote :: String -> String
unQuote = Char -> String -> String
noSurrounding Char
'"'

-- Remove a pair of surrounding bars
unBar :: String -> String
unBar :: String -> String
unBar = Char -> String -> String
noSurrounding Char
'|'

-- 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
"")]

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

    String
-> (String -> Maybe [String] -> m SMTInfoResponse)
-> (SExpr -> m SMTInfoResponse)
-> m SMTInfoResponse
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m SMTInfoResponse
forall {a}. String -> Maybe [String] -> m a
bad ((SExpr -> m SMTInfoResponse) -> m SMTInfoResponse)
-> (SExpr -> m SMTInfoResponse) -> m SMTInfoResponse
forall a b. (a -> b) -> a -> b
$ \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.getInfo'
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 Any) -> 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 Any) -> m (Maybe SMTOption))
 -> m (Maybe SMTOption))
-> (SExpr -> (Maybe [String] -> m Any) -> m (Maybe SMTOption))
-> m (Maybe SMTOption)
forall a b. (a -> b) -> a -> b
$ ([String] -> SMTOption)
-> SExpr -> (Maybe [String] -> m Any) -> 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 value of the logic!"
                 -- 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

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

                String
-> (String -> Maybe [String] -> m (Maybe a))
-> (SExpr -> m (Maybe a))
-> m (Maybe a)
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m (Maybe a)
forall {a}. String -> Maybe [String] -> m a
bad ((SExpr -> m (Maybe a)) -> m (Maybe a))
-> (SExpr -> m (Maybe a)) -> m (Maybe a)
forall a b. (a -> b) -> a -> b
$ \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 SMTInfoResponse
ru <- SMTInfoFlag -> m SMTInfoResponse
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
SMTInfoFlag -> m SMTInfoResponse
getInfo SMTInfoFlag
ReasonUnknown
                      case SMTInfoResponse
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 SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
               CheckSatResult
cs <- String -> m CheckSatResult
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m CheckSatResult
checkSatUsing (String -> m CheckSatResult) -> String -> m CheckSatResult
forall a b. (a -> b) -> a -> b
$ SMTConfig -> String
satCmd SMTConfig
cfg
               case CheckSatResult
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 SMTReasonUnknown
s <- m SMTReasonUnknown
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
                              String -> m ()
forall a. HasCallStack => String -> a
error (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                              , String
"*** Data.SBV.ensureSat: Solver reported Unknown!"
                                              , String
"*** Reason: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SMTReasonUnknown -> String
forall a. Show a => a -> String
show SMTReasonUnknown
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 SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
                  CheckSatResult
cs  <- m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
                  case CheckSatResult
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 SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
                                CheckSatResult
cs  <- m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
                                case CheckSatResult
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 [(String, GeneralizedCV)]
objectiveValues <- m [(String, GeneralizedCV)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, GeneralizedCV)]
getObjectiveValues
                                     SMTModel
m               <- m SMTModel
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
                                     SMTModel -> m SMTModel
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return SMTModel
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 SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
                                       CheckSatResult
cs  <- m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat

                                       case CheckSatResult
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 SMTResult
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
                                                      [(String, SMTResult)] -> m [(String, SMTResult)]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [(String
nm, SMTResult
ur) | String
nm <- [String]
objNames]

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

        getIndependentResult :: Int -> String -> m (String, SMTModel)
        getIndependentResult :: Int -> String -> m (String, SMTModel)
getIndependentResult Int
i String
s = do SMTModel
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)
                                      (String, SMTModel) -> m (String, SMTModel)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (String
s, SMTModel
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 SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
                                  CheckSatResult
cs  <- m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat

                                  case CheckSatResult
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 SMTReasonUnknown
ur <- m SMTReasonUnknown
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
                                                 (Bool, [SMTResult]) -> m (Bool, [SMTResult])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, [SMTConfig -> [String] -> Maybe SMTResult -> SMTResult
ProofError SMTConfig
cfg [SMTReasonUnknown -> String
forall a. Show a => a -> String
show SMTReasonUnknown
ur] Maybe SMTResult
forall a. Maybe a
Nothing])

  where continue :: (SMTModel -> a) -> m (Bool, [a])
continue SMTModel -> a
classify = do SMTModel
m <- m SMTModel
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
                               (Bool
limReached, [SMTModel]
fronts) <- 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
mbN) [SMTModel
m]
                               (Bool, [a]) -> m (Bool, [a])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
limReached, [a] -> [a]
forall a. [a] -> [a]
reverse ((SMTModel -> a) -> [SMTModel] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map SMTModel -> a
classify [SMTModel]
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 CheckSatResult
cs <- m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
                                                     let more :: m (Bool, [SMTModel])
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 CheckSatResult
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{IORef SBVRunMode
runMode :: IORef SBVRunMode
runMode :: State -> IORef SBVRunMode
runMode} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
    SBVRunMode
rm <- IO SBVRunMode -> m SBVRunMode
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO SBVRunMode -> m SBVRunMode) -> IO SBVRunMode -> m SBVRunMode
forall a b. (a -> b) -> a -> b
$ IORef SBVRunMode -> IO SBVRunMode
forall a. IORef a -> IO a
readIORef IORef SBVRunMode
runMode
    case SBVRunMode
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
          SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
          [(String, (Bool, Maybe [String], SBVType))]
uis <- m [(String, (Bool, Maybe [String], SBVType))]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, (Bool, Maybe [String], SBVType))]
getUIs

          UserInputs
allModelInputs <- m UserInputs
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m UserInputs
getTopLevelInputs
          [(Name, CV)]
obsvs          <- m [(Name, CV)]
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m [(Name, CV)]
getObservables


          Seq (SV, (Name, CV))
inputAssocs <- let grab :: NamedSymVar -> f (SV, (Name, CV))
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 (NamedSymVar -> m (SV, (Name, CV)))
-> UserInputs -> m (Seq (SV, (Name, 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) -> Seq a -> m (Seq b)
mapM NamedSymVar -> m (SV, (Name, CV))
forall {f :: * -> *}.
(MonadIO f, MonadQuery f) =>
NamedSymVar -> f (SV, (Name, CV))
grab UserInputs
allModelInputs

          let name :: (a, (c, b)) -> c
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
removeSV = (a, b) -> b
forall a b. (a, b) -> b
snd
              prepare :: Seq (SV, (Name, CV)) -> Seq (SV, (Name, CV))
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 :: Seq (Name, CV)
assocs   = [(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) Seq (Name, CV) -> Seq (Name, CV) -> Seq (Name, CV)
forall a. Semigroup a => a -> a -> a
<> ((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)

          -- collect UIs, and UI functions if requested
          let uiFuns :: [(String, (Bool, Maybe [String], SBVType))]
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))]
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
          Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(String, (Bool, Maybe [String], SBVType))] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, (Bool, Maybe [String], SBVType))]
uiFuns) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
             let solverCaps :: SolverCapabilities
solverCaps = SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)
             in case SolverCapabilities -> Maybe [String]
supportsFlattenedModels SolverCapabilities
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

          Maybe (Seq (NamedSymVar, CV))
bindings <- let get :: NamedSymVar -> m (NamedSymVar, CV)
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
cv <- Maybe Int -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> SV -> m CV
getValueCV Maybe Int
mbi SV
sv
                                                                          (NamedSymVar, CV) -> m (NamedSymVar, CV)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (NamedSymVar
i, CV
cv)

                      in if SMTConfig -> Bool
validationRequested SMTConfig
cfg
                         then Seq (NamedSymVar, CV) -> Maybe (Seq (NamedSymVar, CV))
forall a. a -> Maybe a
Just (Seq (NamedSymVar, CV) -> Maybe (Seq (NamedSymVar, CV)))
-> m (Seq (NamedSymVar, CV)) -> m (Maybe (Seq (NamedSymVar, CV)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (NamedSymVar -> m (NamedSymVar, CV))
-> UserInputs -> m (Seq (NamedSymVar, 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) -> Seq a -> m (Seq b)
mapM NamedSymVar -> m (NamedSymVar, CV)
forall {m :: * -> *}.
(MonadIO m, MonadQuery m) =>
NamedSymVar -> m (NamedSymVar, CV)
get UserInputs
allModelInputs
                         else Maybe (Seq (NamedSymVar, CV)) -> m (Maybe (Seq (NamedSymVar, CV)))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Seq (NamedSymVar, CV))
forall a. Maybe a
Nothing

          [(String, (Bool, SBVType, Either String ([([CV], CV)], CV)))]
uiFunVals <- ((String, (Bool, Maybe [String], SBVType))
 -> m (String, (Bool, SBVType, Either String ([([CV], CV)], CV))))
-> [(String, (Bool, Maybe [String], SBVType))]
-> m [(String, (Bool, SBVType, Either String ([([CV], CV)], 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 (\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) [(String, (Bool, Maybe [String], SBVType))]
uiFuns

          [(String, CV)]
uiVals    <- ((String, (Bool, Maybe [String], SBVType)) -> m (String, CV))
-> [(String, (Bool, Maybe [String], SBVType))] -> m [(String, 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 (\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) [(String, (Bool, Maybe [String], SBVType))]
uiRegs

          SMTModel -> m SMTModel
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return SMTModel { modelObjectives :: [(String, GeneralizedCV)]
modelObjectives = []
                          , modelBindings :: Maybe [(NamedSymVar, CV)]
modelBindings   = Seq (NamedSymVar, CV) -> [(NamedSymVar, CV)]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Seq (NamedSymVar, CV) -> [(NamedSymVar, CV)])
-> Maybe (Seq (NamedSymVar, CV)) -> Maybe [(NamedSymVar, CV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Seq (NamedSymVar, CV))
bindings
                          , modelAssocs :: [(String, CV)]
modelAssocs     = [(String, CV)]
uiVals [(String, CV)] -> [(String, CV)] -> [(String, CV)]
forall a. [a] -> [a] -> [a]
++ Seq (String, CV) -> [(String, CV)]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList ((Name -> String) -> (Name, CV) -> (String, CV)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Name -> String
T.unpack ((Name, CV) -> (String, CV)) -> Seq (Name, CV) -> Seq (String, CV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Seq (Name, CV)
assocs)
                          , modelUIFuns :: [(String, (Bool, SBVType, Either String ([([CV], CV)], CV)))]
modelUIFuns     = [(String, (Bool, SBVType, Either String ([([CV], CV)], CV)))]
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

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

                        [NamedSymVar]
inputs <- UserInputs -> [NamedSymVar]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList (UserInputs -> [NamedSymVar]) -> m UserInputs -> m [NamedSymVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m UserInputs
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m UserInputs
getTopLevelInputs

                        String
-> (String -> Maybe [String] -> m [(String, GeneralizedCV)])
-> (SExpr -> m [(String, GeneralizedCV)])
-> m [(String, GeneralizedCV)]
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m [(String, GeneralizedCV)]
forall {a}. String -> Maybe [String] -> m a
bad ((SExpr -> m [(String, GeneralizedCV)])
 -> m [(String, GeneralizedCV)])
-> (SExpr -> m [(String, GeneralizedCV)])
-> m [(String, GeneralizedCV)]
forall a b. (a -> b) -> a -> b
$ \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 [(SV, SBool)]
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
sv <- State -> SBool -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBool
sb
                                                                (SV, SBool) -> IO (SV, SBool)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SV
sv, SBool
sb)) [SBool]
sBools

                                 -- drop duplicates and trues
                                 let swbs :: [(SV, SBool)]
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
                                 [(SV, (Int, SBool))]
uniqueSWBs <- ((SV, SBool) -> IO (SV, (Int, SBool)))
-> [(SV, SBool)] -> IO [(SV, (Int, 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 (\(SV
sv, SBool
sb) -> do Int
unique <- State -> IO Int
incrementInternalCounter State
st
                                                                     (SV, (Int, SBool)) -> IO (SV, (Int, SBool))
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SV
sv, (Int
unique, SBool
sb))) [(SV, SBool)]
swbs

                                 let translate :: (a, (a, b)) -> (String, [String], (String, b))
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
"))"
                                                      ]

                                 [(String, [String], (String, SBool))]
-> IO [(String, [String], (String, SBool))]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(String, [String], (String, SBool))]
 -> IO [(String, [String], (String, SBool))])
-> [(String, [String], (String, SBool))]
-> IO [(String, [String], (String, SBool))]
forall a b. (a -> b) -> a -> b
$ ((SV, (Int, SBool)) -> (String, [String], (String, SBool)))
-> [(SV, (Int, SBool))] -> [(String, [String], (String, SBool))]
forall a b. (a -> b) -> [a] -> [b]
map (SV, (Int, SBool)) -> (String, [String], (String, SBool))
forall {a} {a} {b}.
(Show a, Show a) =>
(a, (a, b)) -> (String, [String], (String, b))
translate [(SV, (Int, SBool))]
uniqueSWBs

        [(String, [String], (String, SBool))]
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 ([String]
origNames, [[String]]
declss, [(String, SBool)]
proxyMap) = [(String, [String], (String, SBool))]
-> ([String], [[String]], [(String, SBool)])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 [(String, [String], (String, SBool))]
assumptions

        let cmd :: String
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 -> 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
"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."
                                  ]

        (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] -> m ()) -> [String] -> m ()
forall a b. (a -> b) -> a -> b
$ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
declss
        String
r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd

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

        String
-> (String -> Maybe [String] -> m (CheckSatResult, Maybe [SBool]))
-> (SExpr -> m (CheckSatResult, Maybe [SBool]))
-> m (CheckSatResult, Maybe [SBool])
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m (CheckSatResult, Maybe [SBool])
forall {a}. String -> Maybe [String] -> m a
bad ((SExpr -> m (CheckSatResult, Maybe [SBool]))
 -> m (CheckSatResult, Maybe [SBool]))
-> (SExpr -> m (CheckSatResult, Maybe [SBool]))
-> m (CheckSatResult, Maybe [SBool])
forall a b. (a -> b) -> a -> b
$ \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 State
st <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState

                            Int
tCount <- Map (Kind, Kind, [SV]) Int -> Int
forall k a. Map k a -> Int
M.size  (Map (Kind, Kind, [SV]) Int -> Int)
-> m (Map (Kind, Kind, [SV]) Int) -> m Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (IO (Map (Kind, Kind, [SV]) Int) -> m (Map (Kind, Kind, [SV]) Int)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (Map (Kind, Kind, [SV]) Int) -> m (Map (Kind, Kind, [SV]) Int))
-> (IORef (Map (Kind, Kind, [SV]) Int)
    -> IO (Map (Kind, Kind, [SV]) Int))
-> IORef (Map (Kind, Kind, [SV]) Int)
-> m (Map (Kind, Kind, [SV]) Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IORef (Map (Kind, Kind, [SV]) Int)
-> IO (Map (Kind, Kind, [SV]) Int)
forall a. IORef a -> IO a
readIORef) (State -> IORef (Map (Kind, Kind, [SV]) Int)
rtblMap   State
st)
                            Int
aCount <- IntMap ArrayInfo -> Int
forall a. IntMap a -> Int
IM.size (IntMap ArrayInfo -> Int) -> m (IntMap ArrayInfo) -> m Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (IO (IntMap ArrayInfo) -> m (IntMap ArrayInfo)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (IntMap ArrayInfo) -> m (IntMap ArrayInfo))
-> (IORef (IntMap ArrayInfo) -> IO (IntMap ArrayInfo))
-> IORef (IntMap ArrayInfo)
-> m (IntMap ArrayInfo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IORef (IntMap ArrayInfo) -> IO (IntMap ArrayInfo)
forall a. IORef a -> IO a
readIORef) (State -> IORef (IntMap ArrayInfo)
rArrayMap State
st)

                            let tInits :: [String]
tInits = [ 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]]
                                aInits :: [String]
aInits = [ String
"array_" 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
aCount Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]]
                                inits :: [String]
inits  = [String]
tInits [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
aInits

                            case [String]
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
                           a
r <- m a
q
                           Int -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
pop Int
1
                           a -> m a
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
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 Int
depth <- m Int
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m Int
getAssertionStackDepth
               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
"(push " 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
")"
               (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 = 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 Int
depth <- m Int
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m Int
getAssertionStackDepth
               if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
depth
                  then String -> m ()
forall a. HasCallStack => String -> a
error (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: Illegally trying to pop " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall {a}. (Eq a, Num a, Show a) => a -> String
shl Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", at current level: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
depth
                  else do QueryState{SMTConfig
queryConfig :: SMTConfig
queryConfig :: QueryState -> SMTConfig
queryConfig} <- m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState
                          if Bool -> Bool
not (SolverCapabilities -> Bool
supportsGlobalDecls (SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
queryConfig)))
                             then String -> m ()
forall a. HasCallStack => String -> a
error (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                  , String
"*** Data.SBV: Backend solver does not support global-declarations."
                                                  , String
"***           Hence, calls to 'pop' are not supported."
                                                  , String
"***"
                                                  , String
"*** Request this as a feature for the underlying solver!"
                                                  ]
                             else do 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
"(pop " 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
")"
                                     m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m ()
restoreTablesAndArrays
                                     (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 = 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 SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
                                SMTConfig -> [(String, SBool)] -> m (Maybe (String, SMTResult))
go SMTConfig
cfg ([(String, SBool)]
cases [(String, SBool)] -> [(String, SBool)] -> [(String, SBool)]
forall a. [a] -> [a] -> [a]
++ [(String
"Coverage", SBool -> SBool
sNot ([SBool] -> SBool
sOr (((String, SBool) -> SBool) -> [(String, SBool)] -> [SBool]
forall a b. (a -> b) -> [a] -> [b]
map (String, SBool) -> SBool
forall a b. (a, b) -> b
snd [(String, SBool)]
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"
                                CheckSatResult
r <- [SBool] -> m CheckSatResult
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
[SBool] -> m CheckSatResult
checkSatAssuming [SBool
c]

                                case CheckSatResult
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"
                                                 SMTResult
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
                                                 Maybe (String, SMTResult) -> m (Maybe (String, SMTResult))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (String, SMTResult) -> m (Maybe (String, SMTResult)))
-> Maybe (String, SMTResult) -> m (Maybe (String, SMTResult))
forall a b. (a -> b) -> a -> b
$ (String, SMTResult) -> Maybe (String, SMTResult)
forall a. a -> Maybe a
Just (String
n, SMTResult
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
                                                 SMTResult
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
                                                 Maybe (String, SMTResult) -> m (Maybe (String, SMTResult))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (String, SMTResult) -> m (Maybe (String, SMTResult)))
-> Maybe (String, SMTResult) -> m (Maybe (String, SMTResult))
forall a b. (a -> b) -> a -> b
$ (String, SMTResult) -> Maybe (String, SMTResult)
forall a. a -> Maybe a
Just (String
n, SMTResult
res)

                                  CheckSatResult
Unk      -> do String -> m ()
notify String
"Unknown"
                                                 SMTResult
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
                                                 Maybe (String, SMTResult) -> m (Maybe (String, SMTResult))
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (String, SMTResult) -> m (Maybe (String, SMTResult)))
-> Maybe (String, SMTResult) -> m (Maybe (String, SMTResult))
forall a b. (a -> b) -> a -> b
$ (String, SMTResult) -> Maybe (String, SMTResult)
forall a. a -> Maybe a
Just (String
n, SMTResult
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
_ <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd

            () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
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."


                                  ]

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

        String
-> (String -> Maybe [String] -> m [String])
-> (SExpr -> m [String])
-> m [String]
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m [String]
forall {a}. String -> Maybe [String] -> m a
bad ((SExpr -> m [String]) -> m [String])
-> (SExpr -> m [String]) -> m [String]
forall a b. (a -> b) -> a -> b
$ \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
        SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
        if [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool
b | ProduceUnsatCores Bool
b <- SMTConfig -> [SMTOption]
solverSetOptions SMTConfig
cfg]
           then [String] -> Maybe [String]
forall a. a -> Maybe a
Just ([String] -> Maybe [String]) -> m [String] -> m (Maybe [String])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m [String]
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m [String]
getUnsatCore
           else Maybe [String] -> m (Maybe [String])
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [String]
forall a. Maybe a
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."
                                  ]


        String
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.
        String
-> (String -> Maybe [String] -> m String)
-> (SExpr -> m String)
-> m String
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m String
forall {a}. String -> Maybe [String] -> m a
bad ((SExpr -> m String) -> m String)
-> (SExpr -> m String) -> m String
forall a b. (a -> b) -> a -> b
$ \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."
                                 ]

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

       String
-> (String -> Maybe [String] -> m String)
-> (SExpr -> m String)
-> m String
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m String
forall {a}. String -> Maybe [String] -> m a
bad ((SExpr -> m String) -> m String)
-> (SExpr -> m String) -> m String
forall a b. (a -> b) -> a -> b
$ \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
   SV
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
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 -> 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
"getAbduct" String
cmd String
"a get-abduct response" Maybe [String]
forall a. Maybe a
Nothing

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

   String
-> (String -> Maybe [String] -> m String)
-> (SExpr -> m String)
-> m String
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m String
forall {a}. String -> Maybe [String] -> m a
bad ((SExpr -> m String) -> m String)
-> (SExpr -> m String) -> m String
forall a b. (a -> b) -> a -> b
$ \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

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

   String
-> (String -> Maybe [String] -> m String)
-> (SExpr -> m String)
-> m String
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m String
forall {a}. String -> Maybe [String] -> m a
bad ((SExpr -> m String) -> m String)
-> (SExpr -> m String) -> m String
forall a b. (a -> b) -> a -> b
$ \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 [SV]
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
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)
                                        [SBV a] -> [SV] -> m [SV]
fAll [SBV a]
bs (SV
sv SV -> [SV] -> [SV]
forall a. a -> [a] -> [a]
: [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
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 -> 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]
forall a. Maybe a
Nothing

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

       String
-> (String -> Maybe [String] -> m String)
-> (SExpr -> m String)
-> m String
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m String
forall {a}. String -> Maybe [String] -> m a
bad ((SExpr -> m String) -> m String)
-> (SExpr -> m String) -> m String
forall a b. (a -> b) -> a -> b
$ \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

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

        String
-> (String -> Maybe [String] -> m [String])
-> (SExpr -> m [String])
-> m [String]
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m [String]
forall {a}. String -> Maybe [String] -> m a
bad ((SExpr -> m [String]) -> m [String])
-> (SExpr -> m [String]) -> m [String]
forall a b. (a -> b) -> a -> b
$ \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

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

        String
-> (String -> Maybe [String] -> m [(String, Bool)])
-> (SExpr -> m [(String, Bool)])
-> m [(String, Bool)]
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m [(String, Bool)]
forall {a}. String -> Maybe [String] -> m a
bad ((SExpr -> m [(String, Bool)]) -> m [(String, Bool)])
-> (SExpr -> m [(String, Bool)]) -> m [(String, Bool)]
forall a b. (a -> b) -> a -> b
$ \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{SMTConfig
queryConfig :: QueryState -> SMTConfig
queryConfig :: SMTConfig
queryConfig} <- m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState
             [NamedSymVar]
inps <- UserInputs -> [NamedSymVar]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList (UserInputs -> [NamedSymVar]) -> m UserInputs -> m [NamedSymVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m UserInputs
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m UserInputs
getTopLevelInputs

             let grabValues :: State -> IO [(String, CV)]
grabValues State
st = do let extract :: Assignment -> IO (SV, CV)
extract (Assign SVal
s CV
n) = State -> SBV Any -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st (SVal -> SBV Any
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)

                                    [(SV, CV)]
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]
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 :: [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 :: [String]
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 :: [String]
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

                                    Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String]
missing [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
extra [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
dup)) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do

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

                                              maxLen :: Int
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 -> String
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
": "

                                          String -> IO ()
forall a. HasCallStack => String -> a
error (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [String
""
                                                            , String
"*** Data.SBV: Query model construction has a faulty assignment."
                                                            , String
"***"
                                                            ]
                                                         [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String -> String
align String
misTag String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", "  [String]
missing | Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
missing)]
                                                         [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String -> String
align String
extTag String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", "  [String]
extra   | Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
extra)  ]
                                                         [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String -> String
align String
dupTag String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", "  [String]
dup     | Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
dup)    ]
                                                         [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"***"
                                                            , String
"*** Data.SBV: Check your query result construction!"
                                                            ]

                                    let findName :: SV -> String
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
                                                                                ]

                                    [(String, CV)] -> IO [(String, CV)]
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return [(SV -> String
findName SV
s, CV
n) | (SV
s, CV
n) <- [(SV, CV)]
modelAssignment]

             [(String, CV)]
assocs <- (State -> IO [(String, CV)]) -> m [(String, CV)]
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext State -> IO [(String, CV)]
grabValues

             let m :: SMTModel
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     = []
                              }

             SMTResult -> m SMTResult
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTResult -> m SMTResult) -> SMTResult -> m SMTResult
forall a b. (a -> b) -> a -> b
$ SMTConfig -> SMTModel -> SMTResult
Satisfiable SMTConfig
queryConfig SMTModel
m

{- HLint ignore getModelAtIndex "Use forM_" -}