-----------------------------------------------------------------------------
-- |
-- 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, getAssignment, getOption, freshVar, freshVar_, freshArray, freshArray_, 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 Data.Char      (toLower)
import Data.List      (intercalate, nubBy, sortOn)
import Data.Maybe     (listToMaybe, catMaybes)
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
                                , prefixExistentials, prefixUniversals
                                , namedSymVar, getSV, lookupInput, userInputsToList
                                )

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 forall a. Eq a => a -> a -> Bool
== Char
c' Bool -> Bool -> Bool
&& Char
c forall a. Eq a => a -> a -> Bool
== forall a. [a] -> a
last String
cs  = forall a. [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) = forall a. a -> Maybe a
Just String
s
fromECon SExpr
_        = 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
_))      = [forall a. Show a => a -> String
show Integer
i]
stringsOf (EReal   AlgReal
r)        = [forall a. Show a => a -> String
show AlgReal
r]
stringsOf (EFloat  Float
f)        = [forall a. Show a => a -> String
show Float
f]
stringsOf (EFloatingPoint FP
f) = [forall a. Show a => a -> String
show FP
f]
stringsOf (EDouble Double
d)        = [forall a. Show a => a -> String
show Double
d]
stringsOf (EApp [SExpr]
ss)          = 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
_))      = forall a. (Show a, Num a, Ord a) => a -> String
showNegativeNumber Integer
i
        go (EReal   AlgReal
r)        = forall a. (Show a, Num a, Ord a) => a -> String
showNegativeNumber AlgReal
r
        go (EFloat  Float
f)        = forall a. (Show a, Num a, Ord a) => a -> String
showNegativeNumber Float
f
        go (EDouble Double
d)        = forall a. (Show a, Num a, Ord a) => a -> String
showNegativeNumber Double
d
        go (EFloatingPoint FP
f) = forall a. Show a => a -> String
show FP
f
        go (EApp [SExpr
x])         = SExpr -> String
go SExpr
x
        go (EApp [SExpr]
ss)          = String
"(" forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (forall a b. (a -> b) -> [a] -> [b]
map SExpr -> String
go [SExpr]
ss) 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 " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SMTInfoFlag
flag forall a. [a] -> [a] -> [a]
++ String
")"
        bad :: String -> Maybe [String] -> m a
bad = 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" 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          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 <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd

    forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r forall {a}. String -> Maybe [String] -> m a
bad forall a b. (a -> b) -> a -> b
$ \SExpr
pe ->
       if Bool
isAllStat
          then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [(String, String)] -> SMTInfoResponse
Resp_AllStatistics forall a b. (a -> b) -> a -> b
$ SExpr -> [(String, String)]
grabAllStats SExpr
pe
          else case SExpr
pe of
                 ECon String
"unsupported"                                        -> forall (m :: * -> *) a. Monad m => a -> m a
return SMTInfoResponse
Resp_Unsupported
                 EApp [ECon String
":assertion-stack-levels", ENum (Integer
i, Maybe Int
_)]        -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Integer -> SMTInfoResponse
Resp_AssertionStackLevels Integer
i
                 EApp (ECon String
":authors" : [SExpr]
ns)                               -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [String] -> SMTInfoResponse
Resp_Authors (forall a b. (a -> b) -> [a] -> [b]
map SExpr -> String
render [SExpr]
ns)
                 EApp [ECon String
":error-behavior", ECon String
"immediate-exit"]      -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SMTErrorBehavior -> SMTInfoResponse
Resp_Error SMTErrorBehavior
ErrorImmediateExit
                 EApp [ECon String
":error-behavior", ECon String
"continued-execution"] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SMTErrorBehavior -> SMTInfoResponse
Resp_Error SMTErrorBehavior
ErrorContinuedExecution
                 EApp (ECon String
":name" : [SExpr]
o)                                   -> forall (m :: * -> *) a. Monad m => a -> m a
return 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)                         -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SMTReasonUnknown -> SMTInfoResponse
Resp_ReasonUnknown ([SExpr] -> SMTReasonUnknown
unk [SExpr]
o)
                 EApp (ECon String
":version" : [SExpr]
o)                                -> forall (m :: * -> *) a. Monad m => a -> m a
return 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)                                         -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ String -> [String] -> SMTInfoResponse
Resp_InfoKeyword String
s (forall a b. (a -> b) -> [a] -> [b]
map SExpr -> String
render [SExpr]
o)
                 SExpr
_                                                         -> forall {a}. String -> Maybe [String] -> m a
bad String
r 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 = forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower (String -> String
unQuote String
s) forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(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 forall a. HasCallStack => a
undefined of
                 DiagnosticOutputChannel{}   -> 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"   forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *} {a}.
Monad m =>
(String -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
string     String -> SMTOption
DiagnosticOutputChannel
                 ProduceAssertions{}         -> 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"          forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *} {a}.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool       Bool -> SMTOption
ProduceAssertions
                 ProduceAssignments{}        -> 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"         forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *} {a}.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool       Bool -> SMTOption
ProduceAssignments
                 ProduceProofs{}             -> 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"              forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *} {a}.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool       Bool -> SMTOption
ProduceProofs
                 ProduceInterpolants{}       -> 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"        forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *} {a}.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool       Bool -> SMTOption
ProduceInterpolants
                 ProduceUnsatAssumptions{}   -> 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"   forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *} {a}.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool       Bool -> SMTOption
ProduceUnsatAssumptions
                 ProduceUnsatCores{}         -> 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"         forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *} {a}.
Monad m =>
(Bool -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
bool       Bool -> SMTOption
ProduceUnsatCores
                 RandomSeed{}                -> 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"                 forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *} {a}.
Monad m =>
(Integer -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
integer    Integer -> SMTOption
RandomSeed
                 ReproducibleResourceLimit{} -> 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" forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *} {a}.
Monad m =>
(Integer -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
integer    Integer -> SMTOption
ReproducibleResourceLimit
                 SMTVerbosity{}              -> 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"                   forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *} {a}.
Monad m =>
(Integer -> a)
-> SExpr -> (Maybe [String] -> m (Maybe a)) -> m (Maybe a)
integer    Integer -> SMTOption
SMTVerbosity
                 OptionKeyword String
nm [String]
_          -> forall {m :: * -> *} {a} {a}.
(MonadIO m, MonadQuery m) =>
String
-> String
-> (SExpr -> (Maybe [String] -> m a) -> m (Maybe a))
-> m (Maybe a)
askFor (String
"OptionKeyword" forall a. [a] -> [a] -> [a]
++ String
nm)     String
nm                             forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *} {a} {p}.
Monad m =>
([String] -> a) -> SExpr -> p -> m (Maybe a)
stringList (String -> [String] -> SMTOption
OptionKeyword String
nm)
                 SetLogic{}                  -> 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{}                   -> 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 " forall a. [a] -> [a] -> [a]
++ String
smtLibName forall a. [a] -> [a] -> [a]
++ String
")"
                    bad :: String -> Maybe [String] -> m a
bad = forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected (String
"getOption " forall a. [a] -> [a] -> [a]
++ String
sbvName) String
cmd String
"a valid option value" forall a. Maybe a
Nothing

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

                forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r forall {a}. String -> Maybe [String] -> m a
bad forall a b. (a -> b) -> a -> b
$ \case ECon String
"unsupported" -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
                                    SExpr
e                  -> SExpr -> (Maybe [String] -> m a) -> m (Maybe a)
continue SExpr
e (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)
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just 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 forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [String
"Expected string, but got: " forall a. [a] -> [a] -> [a]
++ 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)
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just 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)
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just 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 forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [String
"Expected boolean, but got: " forall a. [a] -> [a] -> [a]
++ 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)
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just 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 forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [String
"Expected integer, but got: " forall a. [a] -> [a] -> [a]
++ 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
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [String] -> a
c 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 <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
SMTInfoFlag -> m SMTInfoResponse
getInfo SMTInfoFlag
ReasonUnknown
                      case SMTInfoResponse
ru of
                        SMTInfoResponse
Resp_Unsupported     -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ String -> SMTReasonUnknown
UnknownOther String
"Solver responded: Unsupported."
                        Resp_ReasonUnknown SMTReasonUnknown
r -> forall (m :: * -> *) a. Monad m => a -> m a
return SMTReasonUnknown
r
                        -- Shouldn't happen, but just in case:
                        SMTInfoResponse
_                    -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Unexpected reason value received: " forall a. [a] -> [a] -> [a]
++ 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 <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
               CheckSatResult
cs <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m CheckSatResult
checkSatUsing forall a b. (a -> b) -> a -> b
$ SMTConfig -> String
satCmd SMTConfig
cfg
               case CheckSatResult
cs of
                 CheckSatResult
Sat    -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
                 DSat{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
                 CheckSatResult
Unk    -> do SMTReasonUnknown
s <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
                              forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                              , String
"*** Data.SBV.ensureSat: Solver reported Unknown!"
                                              , String
"*** Reason: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SMTReasonUnknown
s
                                              ]
                 CheckSatResult
Unsat  -> 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 <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
                  CheckSatResult
cs  <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
                  case CheckSatResult
cs of
                    CheckSatResult
Unsat  -> SMTConfig -> Maybe [String] -> SMTResult
Unsatisfiable SMTConfig
cfg   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m (Maybe [String])
getUnsatCoreIfRequested
                    CheckSatResult
Sat    -> SMTConfig -> SMTModel -> SMTResult
Satisfiable   SMTConfig
cfg   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
                    DSat Maybe String
p -> SMTConfig -> Maybe String -> SMTModel -> SMTResult
DeltaSat      SMTConfig
cfg Maybe String
p forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
                    CheckSatResult
Unk    -> SMTConfig -> SMTReasonUnknown -> SMTResult
Unknown       SMTConfig
cfg   forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
  | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any 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 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 <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
                                CheckSatResult
cs  <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
                                case CheckSatResult
cs of
                                  CheckSatResult
Unsat  -> SMTConfig -> Maybe [String] -> SMTResult
Unsatisfiable SMTConfig
cfg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m (Maybe [String])
getUnsatCoreIfRequested
                                  CheckSatResult
Sat    -> SMTConfig -> SMTModel -> SMTResult
classifyModel SMTConfig
cfg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTModel
getModelWithObjectives
                                  DSat{} -> SMTConfig -> SMTModel -> SMTResult
classifyModel SMTConfig
cfg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m SMTModel
getModelWithObjectives
                                  CheckSatResult
Unk    -> SMTConfig -> SMTReasonUnknown -> SMTResult
Unknown       SMTConfig
cfg forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
   where getModelWithObjectives :: m SMTModel
getModelWithObjectives = do [(String, GeneralizedCV)]
objectiveValues <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, GeneralizedCV)]
getObjectiveValues
                                     SMTModel
m               <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
                                     forall (m :: * -> *) a. Monad m => a -> m a
return SMTModel
m {modelObjectives :: [(String, GeneralizedCV)]
modelObjectives = [(String, GeneralizedCV)]
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 <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
                                       CheckSatResult
cs  <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat

                                       case CheckSatResult
cs of
                                         CheckSatResult
Unsat  -> forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m (Maybe [String])
getUnsatCoreIfRequested forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \Maybe [String]
mbUC -> 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    -> forall {b}. (SMTModel -> b) -> m [(String, b)]
continue (SMTConfig -> SMTModel -> SMTResult
classifyModel SMTConfig
cfg)
                                         DSat{} -> 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
                                                      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 <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, GeneralizedCV)]
getObjectiveValues
                               [(String, SMTModel)]
nms <- 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
                               forall (m :: * -> *) a. Monad m => a -> m a
return [(String
n, SMTModel -> b
classify (SMTModel
m {modelObjectives :: [(String, GeneralizedCV)]
modelObjectives = [(String, GeneralizedCV)]
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 <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> m SMTModel
getModelAtIndex (forall a. a -> Maybe a
Just Int
i)
                                      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 forall a. Ord a => a -> a -> Bool
<= Int
0             = forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [])
getParetoOptResults Maybe Int
mbN      = do SMTConfig
cfg <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
                                  CheckSatResult
cs  <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat

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

  where continue :: (SMTModel -> a) -> m (Bool, [a])
continue SMTModel -> a
classify = do SMTModel
m <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
                               (Bool
limReached, [SMTModel]
fronts) <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
getParetoFronts (forall a. Num a => a -> a -> a
subtract Int
1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
mbN) [SMTModel
m]
                               forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
limReached, forall a. [a] -> [a]
reverse (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 forall a. Ord a => a -> a -> Bool
<= Int
0 = forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [SMTModel]
sofar)
        getParetoFronts Maybe Int
mbi      [SMTModel]
sofar          = do CheckSatResult
cs <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
                                                     let more :: m (Bool, [SMTModel])
more = forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SMTModel
m -> forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> [SMTModel] -> m (Bool, [SMTModel])
getParetoFronts (forall a. Num a => a -> a -> a
subtract Int
1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int
mbi) (SMTModel
m forall a. a -> [a] -> [a]
: [SMTModel]
sofar)
                                                     case CheckSatResult
cs of
                                                       CheckSatResult
Unsat  -> 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 = forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> m SMTModel
getModelAtIndex 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 :: State -> IORef SBVRunMode
runMode :: IORef SBVRunMode
runMode} <- forall (m :: * -> *). MonadQuery m => m State
queryState
    SBVRunMode
rm <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef SBVRunMode
runMode
    case SBVRunMode
rm of
      m :: SBVRunMode
m@SBVRunMode
CodeGen           -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.getModel: Model is not available in mode: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SBVRunMode
m
      m :: SBVRunMode
m@Concrete{}        -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.getModel: Model is not available in mode: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SBVRunMode
m
      SMTMode QueryContext
_ IStage
_ Bool
isSAT SMTConfig
_ -> do
          SMTConfig
cfg   <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
          UserInputs
qinps <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m UserInputs
getQuantifiedInputs
          [(String, SBVType)]
uis   <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, SBVType)]
getUIs

           -- for "sat", display the prefix existentials. for "proof", display the prefix universals
          let allModelInputs :: UserInputs
allModelInputs = if Bool
isSAT then UserInputs -> UserInputs
prefixExistentials UserInputs
qinps
                                        else UserInputs -> UserInputs
prefixUniversals   UserInputs
qinps

              -- Add on observables only if we're not in a quantified context
              grabObservables :: Bool
grabObservables = forall a. Seq a -> Int
S.length UserInputs
allModelInputs forall a. Eq a => a -> a -> Bool
== forall a. Seq a -> Int
S.length UserInputs
qinps -- i.e., we didn't drop anything

          [(Name, CV)]
obsvs <- if Bool
grabObservables
                      then forall (m :: * -> *). (MonadIO m, MonadQuery m) => m [(Name, CV)]
getObservables
                      else do forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"*** In a quantified context, obvservables will not be printed."]
                              forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Monoid a => a
mempty

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

          Seq (SV, (Name, CV))
inputAssocs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall {f :: * -> *}.
(MonadIO f, MonadQuery f) =>
NamedSymVar -> f (SV, (Name, CV))
grab forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Quantifier, NamedSymVar) -> NamedSymVar
namedSymVar) UserInputs
allModelInputs

          let name :: (a, (c, b)) -> c
name     = forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd
              removeSV :: (a, b) -> b
removeSV = forall a b. (a, b) -> b
snd
              prepare :: Seq (SV, (Name, CV)) -> Seq (SV, (Name, CV))
prepare  = forall a. Ord a => Seq a -> Seq a
S.unstableSort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> Seq a -> Seq a
S.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTConfig -> String -> Bool
isNonModelVar SMTConfig
cfg forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> String
T.unpack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a} {c} {b}. (a, (c, b)) -> c
name)
              assocs :: Seq (Name, CV)
assocs   = forall a. [a] -> Seq a
S.fromList (forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn forall a b. (a, b) -> a
fst [(Name, CV)]
obsvs) forall a. Semigroup a => a -> a -> a
<> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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, SBVType)]
uiFuns = [(String, SBVType)
ui | ui :: (String, SBVType)
ui@(String
nm, SBVType [Kind]
as) <- [(String, SBVType)]
uis, forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
as forall a. Ord a => a -> a -> Bool
>  Int
1, SMTConfig -> Bool
satTrackUFs SMTConfig
cfg, Bool -> Bool
not (SMTConfig -> String -> Bool
isNonModelVar SMTConfig
cfg String
nm)] -- functions have at least two things in their type!
              uiRegs :: [(String, SBVType)]
uiRegs = [(String, SBVType)
ui | ui :: (String, SBVType)
ui@(String
nm, SBVType [Kind]
as) <- [(String, SBVType)]
uis, forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
as forall a. Eq a => a -> a -> Bool
== Int
1,                  Bool -> Bool
not (SMTConfig -> String -> Bool
isNonModelVar 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
          forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, SBVType)]
uiFuns) 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   -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
                  Just [String]
cmds -> forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True) [String]
cmds

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

                          flipQ :: (Quantifier, b) -> (Quantifier, b)
flipQ i :: (Quantifier, b)
i@(Quantifier
q, b
sv) = case (Bool
isSAT, Quantifier
q) of
                                             (Bool
True,  Quantifier
_ )  -> (Quantifier, b)
i
                                             (Bool
False, Quantifier
EX)  -> (Quantifier
ALL, b
sv)
                                             (Bool
False, Quantifier
ALL) -> (Quantifier
EX,  b
sv)

                      in if SMTConfig -> Bool
validationRequested SMTConfig
cfg
                         then forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall {m :: * -> *}.
(MonadIO m, MonadQuery m) =>
(Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV)
get forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {b}. (Quantifier, b) -> (Quantifier, b)
flipQ) UserInputs
qinps
                         else forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

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

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

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

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

                        [NamedSymVar]
inputs <- forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Quantifier, NamedSymVar) -> NamedSymVar
namedSymVar forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (MonadIO m, MonadQuery m) => m UserInputs
getQuantifiedInputs

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

          where locate :: String -> SExpr -> m (Maybe (String, GeneralizedCV))
locate String
nm SExpr
v = case forall a. [a] -> Maybe a
listToMaybe [NamedSymVar
p | p :: NamedSymVar
p@(NamedSymVar SV
sv Name
_) <- [NamedSymVar]
inputs, forall a. Show a => a -> String
show SV
sv forall a. Eq a => a -> a -> Bool
== String
nm] of
                                Maybe NamedSymVar
Nothing                          -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \GeneralizedCV
val -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (Name -> String
T.unpack Name
actualName, GeneralizedCV
val)

                dontUnderstand :: String -> m a
dontUnderstand String
s = forall a. Maybe [String] -> m a
bailOut forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [ String
"Unable to understand solver output."
                                                  , String
"While trying to process: " 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CV -> GeneralizedCV
RegularCV CV
v
                  | Bool
True                                   = ExtCV -> GeneralizedCV
ExtendedCV 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 = 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")                    = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Kind -> ExtCV
Infinite  Kind
k
                        cvt (ECon String
"epsilon")               = forall (m :: * -> *) a. Monad m => a -> m a
return 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  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> m ExtCV
cvt SExpr
x 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
_))               = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CV -> ExtCV
BoundedCV forall a b. (a -> b) -> a -> b
$ forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k Integer
i
                        cvt (EReal   AlgReal
r)                    = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CV -> ExtCV
BoundedCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k forall a b. (a -> b) -> a -> b
$ AlgReal -> CVal
CAlgReal AlgReal
r
                        cvt (EFloat  Float
f)                    = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CV -> ExtCV
BoundedCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k forall a b. (a -> b) -> a -> b
$ Float -> CVal
CFloat   Float
f
                        cvt (EDouble Double
d)                    = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CV -> ExtCV
BoundedCV forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k forall a b. (a -> b) -> a -> b
$ Double -> CVal
CDouble  Double
d
                        cvt (EApp [ECon String
"+", SExpr
x, SExpr
y])        =          ExtCV -> ExtCV -> ExtCV
AddExtCV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> m ExtCV
cvt SExpr
x 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> m ExtCV
cvt SExpr
x 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 = forall {a}. String -> m a
dontUnderstand (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 (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 = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = 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 <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\SBool
sb -> do SV
sv <- forall a. State -> SBV a -> IO SV
sbvToSV State
st SBool
sb
                                                                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
_) <- forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst) [(SV, SBool)]
swsOriginal, SV
sv forall a. Eq a => a -> a -> Bool
/= SV
trueSV]

                                 -- get a unique proxy name for each
                                 [(SV, (Int, SBool))]
uniqueSWBs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(SV
sv, SBool
sb) -> do Int
unique <- State -> IO Int
incrementInternalCounter State
st
                                                                     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    = forall a. Show a => a -> String
show a
sv
                                              proxy :: String
proxy = String
"__assumption_proxy_" forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
"_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
unique
                                              decls :: [String]
decls = [ String
"(declare-const " forall a. [a] -> [a] -> [a]
++ String
proxy forall a. [a] -> [a] -> [a]
++ String
" Bool)"
                                                      , String
"(assert (= " forall a. [a] -> [a] -> [a]
++ String
proxy forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
"))"
                                                      ]

                                 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map 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 <- 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) = forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 [(String, [String], (String, SBool))]
assumptions

        let cmd :: String
cmd = String
"(check-sat-assuming (" forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(String, SBool)]
proxyMap) forall a. [a] -> [a] -> [a]
++ String
"))"
            bad :: String -> Maybe [String] -> m a
bad = 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"
                           forall a b. (a -> b) -> a -> b
$ 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."
                                  ]

        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
declss
        String
r <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd

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

        forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r forall {a}. String -> Maybe [String] -> m a
bad forall a b. (a -> b) -> a -> b
$ \case ECon String
"sat"     -> forall (m :: * -> *) a. Monad m => a -> m a
return (CheckSatResult
Sat, forall a. Maybe a
Nothing)
                            ECon String
"unsat"   -> m (CheckSatResult, Maybe [SBool])
grabUnsat
                            ECon String
"unknown" -> forall (m :: * -> *) a. Monad m => a -> m a
return (CheckSatResult
Unk, forall a. Maybe a
Nothing)
                            SExpr
_              -> forall {a}. String -> Maybe [String] -> m a
bad String
r 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 <- forall (m :: * -> *). MonadQuery m => m State
queryState

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

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

                            case [String]
inits of
                              []  -> forall (m :: * -> *) a. Monad m => a -> m a
return ()   -- Nothing to do
                              [String
x] -> forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True forall a b. (a -> b) -> a -> b
$ String
"(assert " forall a. [a] -> [a] -> [a]
++ String
x forall a. [a] -> [a] -> [a]
++ String
")"
                              [String]
xs  -> forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True forall a b. (a -> b) -> a -> b
$ String
"(assert (and " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
xs 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 forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
push Int
1
                           a
r <- m a
q
                           forall (m :: * -> *). (MonadIO m, MonadQuery m) => Int -> m ()
pop Int
1
                           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 forall a. Ord a => a -> a -> Bool
<= Int
0 = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: push requires a strictly positive level argument, received: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
 | Bool
True   = do Int
depth <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m Int
getAssertionStackDepth
               forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True forall a b. (a -> b) -> a -> b
$ String
"(push " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
")"
               forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(QueryState -> QueryState) -> m ()
modifyQueryState forall a b. (a -> b) -> a -> b
$ \QueryState
s -> QueryState
s{queryAssertionStackDepth :: Int
queryAssertionStackDepth = Int
depth forall a. Num a => a -> a -> a
+ Int
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 forall a. Ord a => a -> a -> Bool
<= Int
0 = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: pop requires a strictly positive level argument, received: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
 | Bool
True   = do Int
depth <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m Int
getAssertionStackDepth
               if Int
i forall a. Ord a => a -> a -> Bool
> Int
depth
                  then forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: Illegally trying to pop " forall a. [a] -> [a] -> [a]
++ forall {a}. (Eq a, Num a, Show a) => a -> String
shl Int
i forall a. [a] -> [a] -> [a]
++ String
", at current level: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
depth
                  else do QueryState{SMTConfig
queryConfig :: QueryState -> SMTConfig
queryConfig :: SMTConfig
queryConfig} <- 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 forall a. HasCallStack => String -> a
error 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 forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True forall a b. (a -> b) -> a -> b
$ String
"(pop " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
")"
                                     forall (m :: * -> *). (MonadIO m, MonadQuery m) => m ()
restoreTablesAndArrays
                                     forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(QueryState -> QueryState) -> m ()
modifyQueryState forall a b. (a -> b) -> a -> b
$ \QueryState
s -> QueryState
s{queryAssertionStackDepth :: Int
queryAssertionStackDepth = Int
depth forall a. Num a => a -> a -> a
- Int
i}
   where shl :: a -> String
shl a
1 = String
"one level"
         shl a
n = forall a. Show a => a -> String
show a
n 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 <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
                                SMTConfig -> [(String, SBool)] -> m (Maybe (String, SMTResult))
go SMTConfig
cfg ([(String, SBool)]
cases forall a. [a] -> [a] -> [a]
++ [(String
"Coverage", SBool -> SBool
sNot ([SBool] -> SBool
sOr (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(String, SBool)]
cases)))])
  where msg :: String -> m ()
msg = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
printCases forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn

        go :: SMTConfig -> [(String, SBool)] -> m (Maybe (String, SMTResult))
go SMTConfig
_ []            = forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall a b. (a -> b) -> a -> b
$ String
"Case " forall a. [a] -> [a] -> [a]
++ String
n forall a. [a] -> [a] -> [a]
++ String
": " forall a. [a] -> [a] -> [a]
++ String
s

                                String -> m ()
notify String
"Starting"
                                CheckSatResult
r <- 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
                                                 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (String
n, SMTResult
res)

                                  DSat Maybe String
mbP -> do String -> m ()
notify forall a b. (a -> b) -> a -> b
$ String
"Delta satisfiable" forall a. [a] -> [a] -> [a]
++ forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (String
" (precision: " forall a. [a] -> [a] -> [a]
++) Maybe String
mbP
                                                 SMTResult
res <- SMTConfig -> Maybe String -> SMTModel -> SMTResult
DeltaSat SMTConfig
cfg Maybe String
mbP forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTModel
getModel
                                                 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m SMTReasonUnknown
getUnknownReason
                                                 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True String
"(reset-assertions)"
                     forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(QueryState -> QueryState) -> m ()
modifyQueryState forall a b. (a -> b) -> a -> b
$ \QueryState
s -> QueryState
s{ queryAssertionStackDepth :: Int
queryAssertionStackDepth = Int
0 }

                     -- Make sure we restore tables and arrays after resetAssertions: See: https://github.com/LeventErkok/sbv/issues/535
                     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 \"" forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
sanitize String
s 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
_ <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd

            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 forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True String
"(exit)"
          forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(QueryState -> QueryState) -> m ()
modifyQueryState forall a b. (a -> b) -> a -> b
$ \QueryState
s -> QueryState
s{queryAssertionStackDepth :: Int
queryAssertionStackDepth = Int
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 = 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"
                           forall a b. (a -> b) -> a -> b
$ 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 <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd

        forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r forall {a}. String -> Maybe [String] -> m a
bad forall a b. (a -> b) -> a -> b
$ \case
           EApp [SExpr]
es | Just [String]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SExpr -> Maybe String
fromECon [SExpr]
es -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map String -> String
unBar [String]
xs
           SExpr
_                                     -> forall {a}. String -> Maybe [String] -> m a
bad String
r 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 <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
        if forall (t :: * -> *). Foldable t => t Bool -> Bool
or [Bool
b | ProduceUnsatCores Bool
b <- SMTConfig -> [SMTOption]
solverSetOptions SMTConfig
cfg]
           then forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (MonadIO m, MonadQuery m) => m [String]
getUnsatCore
           else forall (m :: * -> *) a. Monad m => a -> m a
return 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 = 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"
                           forall a b. (a -> b) -> a -> b
$ 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 <- 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.
        forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r forall {a}. String -> Maybe [String] -> m a
bad forall a b. (a -> b) -> a -> b
$ \SExpr
_ -> 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
  | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
fs
  = 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
'|' forall a. a -> [a] -> [a]
: String
s forall a. [a] -> [a] -> [a]
++ String
"|"
           cmd :: String
cmd = String
"(get-interpolant (" forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (forall a b. (a -> b) -> [a] -> [b]
map String -> String
bar [String]
fs) forall a. [a] -> [a] -> [a]
++ String
"))"
           bad :: String -> Maybe [String] -> m a
bad = 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"
                          forall a b. (a -> b) -> a -> b
$ 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 <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd

       forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r forall {a}. String -> Maybe [String] -> m a
bad forall a b. (a -> b) -> a -> b
$ \SExpr
e -> forall (m :: * -> *) a. Monad m => a -> m a
return 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
  | forall (t :: * -> *) a. Foldable t => t a -> Int
length [SBool]
fs forall a. Ord a => a -> a -> Bool
< Int
2
  = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.getInterpolantZ3 requires at least two booleans, received: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [SBool]
fs
  | Bool
True
  = do [SV]
ss <- let fAll :: [SBV a] -> [SV] -> m [SV]
fAll []     [SV]
sofar = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [SV]
sofar
                 fAll (SBV a
b:[SBV a]
bs) [SV]
sofar = do SV
sv <- forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext (forall a. State -> SBV a -> IO SV
`sbvToSV` SBV a
b)
                                        [SBV a] -> [SV] -> m [SV]
fAll [SBV a]
bs (SV
sv forall a. a -> [a] -> [a]
: [SV]
sofar)
             in forall {m :: * -> *} {a}.
(MonadIO m, MonadQuery m) =>
[SBV a] -> [SV] -> m [SV]
fAll [SBool]
fs []

       let cmd :: String
cmd = String
"(get-interpolant " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [SV]
ss) forall a. [a] -> [a] -> [a]
++ String
")"
           bad :: String -> Maybe [String] -> m a
bad = 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" forall a. Maybe a
Nothing

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

       forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r forall {a}. String -> Maybe [String] -> m a
bad forall a b. (a -> b) -> a -> b
$ \SExpr
e -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 = 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"
                           forall a b. (a -> b) -> a -> b
$ 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 <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd

        forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r forall {a}. String -> Maybe [String] -> m a
bad forall a b. (a -> b) -> a -> b
$ \SExpr
pe -> case SExpr
pe of
                                EApp [SExpr]
xs -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map SExpr -> String
render [SExpr]
xs
                                SExpr
_       -> 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 = 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"
                           forall a b. (a -> b) -> a -> b
$ 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
_)]) = forall a. a -> Maybe a
Just (String -> String
unQuote String
s, Bool
False)
            grab (EApp [ECon String
s, ENum (Integer
1, Maybe Int
_)]) = forall a. a -> Maybe a
Just (String -> String
unQuote String
s, Bool
True)
            grab SExpr
_                            = forall a. Maybe a
Nothing

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

        forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r forall {a}. String -> Maybe [String] -> m a
bad forall a b. (a -> b) -> a -> b
$ \case EApp [SExpr]
ps | Just [(String, Bool)]
vs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SExpr -> Maybe (String, Bool)
grab [SExpr]
ps -> forall (m :: * -> *) a. Monad m => a -> m a
return [(String, Bool)]
vs
                            SExpr
_                                 -> forall {a}. String -> Maybe [String] -> m a
bad String
r 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 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                      -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: Impossible happened in |->: Cannot construct a CV with literal: " forall a. [a] -> [a] -> [a]
++ 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 :: SMTConfig
queryConfig :: QueryState -> SMTConfig
queryConfig} <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState
             [(Quantifier, NamedSymVar)]
inps <- UserInputs -> [(Quantifier, NamedSymVar)]
userInputsToList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (MonadIO m, MonadQuery m) => m UserInputs
getQuantifiedInputs

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

                                    [(SV, CV)]
modelAssignment <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t 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 = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(SV, CV)]
modelAssignment

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

                                    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([String]
missing forall a. [a] -> [a] -> [a]
++ [String]
extra forall a. [a] -> [a] -> [a]
++ [String]
dup)) 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 = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum forall a b. (a -> b) -> a -> b
$  Int
0
                                                                forall a. a -> [a] -> [a]
: [forall (t :: * -> *) a. Foldable t => t a -> Int
length String
misTag | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
missing)]
                                                               forall a. [a] -> [a] -> [a]
++ [forall (t :: * -> *) a. Foldable t => t a -> Int
length String
extTag | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
extra)]
                                                               forall a. [a] -> [a] -> [a]
++ [forall (t :: * -> *) a. Foldable t => t a -> Int
length String
dupTag | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
dup)]

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

                                          forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines forall a b. (a -> b) -> a -> b
$ [String
""
                                                            , String
"*** Data.SBV: Query model construction has a faulty assignment."
                                                            , String
"***"
                                                            ]
                                                         forall a. [a] -> [a] -> [a]
++ [ String -> String
align String
misTag forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", "  [String]
missing | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
missing)]
                                                         forall a. [a] -> [a] -> [a]
++ [ String -> String
align String
extTag forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", "  [String]
extra   | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
extra)  ]
                                                         forall a. [a] -> [a] -> [a]
++ [ String -> String
align String
dupTag forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", "  [String]
dup     | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
dup)    ]
                                                         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 | (Quantifier
_, NamedSymVar SV
i Name
nm) <- [(Quantifier, NamedSymVar)]
inps, SV
s forall a. Eq a => a -> a -> Bool
== SV
i] of
                                                        [String
nm] -> String
nm
                                                        []   -> forall a. HasCallStack => String -> a
error String
"*** Data.SBV: Impossible happened: Cannot find " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SV
s forall a. [a] -> [a] -> [a]
++ String
" in the input list"
                                                        [String]
nms  -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                                                , String
"*** Data.SBV: Impossible happened: Multiple matches for: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SV
s
                                                                                , String
"***   Candidates: " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
nms
                                                                                ]

                                    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 <- 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 [((Quantifier, NamedSymVar), Maybe CV)]
modelBindings   = forall a. Maybe a
Nothing
                              , modelAssocs :: [(String, CV)]
modelAssocs     = [(String, CV)]
assocs
                              , modelUIFuns :: [(String, (SBVType, ([([CV], CV)], CV)))]
modelUIFuns     = []
                              }

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

{-# ANN getModelAtIndex ("HLint: ignore Use forM_" :: String) #-}