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

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

-- Remove one pair of surrounding 'c's, if present
noSurrounding :: Char -> String -> String
noSurrounding :: Char -> String -> String
noSurrounding Char
c (Char
c':cs :: String
cs@(Char
_:String
_)) | Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
c' Bool -> Bool -> Bool
&& Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Char
forall a. [a] -> a
last String
cs  = String -> String
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) = String -> Maybe String
forall a. a -> Maybe a
Just String
s
fromECon SExpr
_        = Maybe String
forall a. Maybe a
Nothing

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

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

        -- be careful with negative number printing in SMT-Lib..
        shNN :: (Show a, Num a, Ord a) => a -> String
        shNN :: a -> String
shNN a
i
          | a
i a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
0 = String
"(- " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show (-a
i) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
          | Bool
True  = a -> String
forall a. Show a => a -> String
show a
i

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  where continue :: (SMTModel -> b) -> m [(String, b)]
continue SMTModel -> b
classify = do [(String, GeneralizedCV)]
objectiveValues <- m [(String, GeneralizedCV)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, GeneralizedCV)]
getObjectiveValues
                               [(String, SMTModel)]
nms <- (Int -> String -> m (String, SMTModel))
-> [Int] -> [String] -> m [(String, SMTModel)]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Int -> String -> m (String, SMTModel)
getIndependentResult [Int
0..] [String]
objNames
                               [(String, b)] -> m [(String, b)]
forall (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 <- Maybe Int -> m SMTModel
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> m SMTModel
getModelAtIndex (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i)
                                      (String, SMTModel) -> m (String, SMTModel)
forall (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 :: Maybe Int -> m (Bool, [SMTResult])
getParetoOptResults (Just Int
i)
        | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0             = (Bool, [SMTResult]) -> m (Bool, [SMTResult])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, [])
getParetoOptResults Maybe Int
mbN      = do SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
                                  CheckSatResult
cs  <- m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat

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

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

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

-- | Get a model stored at an index. This is likely very Z3 specific!
getModelAtIndex :: (MonadIO m, MonadQuery m) => Maybe Int -> m SMTModel
getModelAtIndex :: Maybe Int -> m SMTModel
getModelAtIndex Maybe Int
mbi = do
    State{IORef SBVRunMode
runMode :: State -> IORef SBVRunMode
runMode :: IORef SBVRunMode
runMode} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
    SBVRunMode
rm <- IO SBVRunMode -> m SBVRunMode
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO SBVRunMode -> m SBVRunMode) -> IO SBVRunMode -> m SBVRunMode
forall a b. (a -> b) -> a -> b
$ IORef SBVRunMode -> IO SBVRunMode
forall a. IORef a -> IO a
readIORef IORef SBVRunMode
runMode
    case SBVRunMode
rm of
      m :: SBVRunMode
m@SBVRunMode
CodeGen           -> String -> m SMTModel
forall a. HasCallStack => String -> a
error (String -> m SMTModel) -> String -> m SMTModel
forall a b. (a -> b) -> a -> b
$ String
"SBV.getModel: Model is not available in mode: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVRunMode -> String
forall a. Show a => a -> String
show SBVRunMode
m
      m :: SBVRunMode
m@Concrete{}        -> String -> m SMTModel
forall a. HasCallStack => String -> a
error (String -> m SMTModel) -> String -> m SMTModel
forall a b. (a -> b) -> a -> b
$ String
"SBV.getModel: Model is not available in mode: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVRunMode -> String
forall a. Show a => a -> String
show SBVRunMode
m
      SMTMode QueryContext
_ IStage
_ Bool
isSAT SMTConfig
_ -> do
          SMTConfig
cfg   <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
          UserInputs
qinps <- m UserInputs
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m UserInputs
getQuantifiedInputs
          [(String, SBVType)]
uis   <- m [(String, SBVType)]
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 = UserInputs -> Int
forall a. Seq a -> Int
S.length UserInputs
allModelInputs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== UserInputs -> Int
forall a. Seq a -> Int
S.length UserInputs
qinps -- i.e., we didn't drop anything

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

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

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

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

          -- collect UIs, and UI functions if requested
          let uiFuns :: [(String, SBVType)]
uiFuns = [(String, SBVType)
ui | ui :: (String, SBVType)
ui@(String
nm, SBVType [Kind]
as) <- [(String, SBVType)]
uis, [Kind] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
as Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>  Int
1, SMTConfig -> Bool
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, [Kind] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
as Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1,                  Bool -> Bool
not (SMTConfig -> String -> Bool
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
          Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(String, SBVType)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, SBVType)]
uiFuns) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
             let solverCaps :: SolverCapabilities
solverCaps = SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)
             in case SolverCapabilities -> Maybe [String]
supportsFlattenedModels SolverCapabilities
solverCaps of
                  Maybe [String]
Nothing   -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                  Just [String]
cmds -> (String -> m ()) -> [String] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True) [String]
cmds

          Maybe (Seq ((Quantifier, NamedSymVar), Maybe CV))
bindings <- let get :: (Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV)
get i :: (Quantifier, NamedSymVar)
i@(Quantifier
ALL, NamedSymVar
_)      = ((Quantifier, NamedSymVar), Maybe CV)
-> m ((Quantifier, NamedSymVar), Maybe CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, NamedSymVar)
i, Maybe CV
forall a. Maybe a
Nothing)
                          get i :: (Quantifier, NamedSymVar)
i@(Quantifier
EX, NamedSymVar -> SV
getSV -> SV
sv) = case ((SV, (Name, CV)) -> SV)
-> SV -> Seq (SV, (Name, CV)) -> Maybe (SV, (Name, CV))
forall a. Eq a => (a -> SV) -> SV -> Seq a -> Maybe a
lookupInput (SV, (Name, CV)) -> SV
forall a b. (a, b) -> a
fst SV
sv Seq (SV, (Name, CV))
inputAssocs of
                                                      Just (SV
_, (Name
_, CV
cv)) -> ((Quantifier, NamedSymVar), Maybe CV)
-> m ((Quantifier, NamedSymVar), Maybe CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, NamedSymVar)
i, CV -> Maybe CV
forall a. a -> Maybe a
Just CV
cv)
                                                      Maybe (SV, (Name, CV))
Nothing           -> do CV
cv <- Maybe Int -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> SV -> m CV
getValueCV Maybe Int
mbi SV
sv
                                                                              ((Quantifier, NamedSymVar), Maybe CV)
-> m ((Quantifier, NamedSymVar), Maybe CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, NamedSymVar)
i, CV -> Maybe CV
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 Seq ((Quantifier, NamedSymVar), Maybe CV)
-> Maybe (Seq ((Quantifier, NamedSymVar), Maybe CV))
forall a. a -> Maybe a
Just (Seq ((Quantifier, NamedSymVar), Maybe CV)
 -> Maybe (Seq ((Quantifier, NamedSymVar), Maybe CV)))
-> m (Seq ((Quantifier, NamedSymVar), Maybe CV))
-> m (Maybe (Seq ((Quantifier, NamedSymVar), Maybe CV)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Quantifier, NamedSymVar)
 -> m ((Quantifier, NamedSymVar), Maybe CV))
-> UserInputs -> m (Seq ((Quantifier, NamedSymVar), Maybe CV))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV)
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV)
get ((Quantifier, NamedSymVar)
 -> m ((Quantifier, NamedSymVar), Maybe CV))
-> ((Quantifier, NamedSymVar) -> (Quantifier, NamedSymVar))
-> (Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Quantifier, NamedSymVar) -> (Quantifier, NamedSymVar)
forall b. (Quantifier, b) -> (Quantifier, b)
flipQ) UserInputs
qinps
                         else Maybe (Seq ((Quantifier, NamedSymVar), Maybe CV))
-> m (Maybe (Seq ((Quantifier, NamedSymVar), Maybe CV)))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Seq ((Quantifier, NamedSymVar), Maybe CV))
forall a. Maybe a
Nothing

          [(String, (SBVType, ([([CV], CV)], CV)))]
uiFunVals <- ((String, SBVType) -> m (String, (SBVType, ([([CV], CV)], CV))))
-> [(String, SBVType)]
-> m [(String, (SBVType, ([([CV], CV)], CV)))]
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))) (([([CV], CV)], CV) -> (String, (SBVType, ([([CV], CV)], CV))))
-> m ([([CV], CV)], CV)
-> m (String, (SBVType, ([([CV], CV)], CV)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int -> (String, SBVType) -> m ([([CV], CV)], CV)
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    <- ((String, SBVType) -> m (String, CV))
-> [(String, SBVType)] -> m [(String, CV)]
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,) (CV -> (String, CV)) -> m CV -> m (String, CV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Int -> (String, SBVType) -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> (String, SBVType) -> m CV
getUICVal Maybe Int
mbi (String, SBVType)
ui) [(String, SBVType)]
uiRegs

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                 -- get a unique proxy name for each
                                 [(SV, (Int, SBool))]
uniqueSWBs <- ((SV, SBool) -> IO (SV, (Int, SBool)))
-> [(SV, SBool)] -> IO [(SV, (Int, SBool))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(SV
sv, SBool
sb) -> do Int
unique <- State -> IO Int
incrementInternalCounter State
st
                                                                     (SV, (Int, SBool)) -> IO (SV, (Int, SBool))
forall (m :: * -> *) a. Monad m => a -> m a
return (SV
sv, (Int
unique, SBool
sb))) [(SV, SBool)]
swbs

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

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

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

        let ([String]
origNames, [[String]]
declss, [(String, SBool)]
proxyMap) = [(String, [String], (String, SBool))]
-> ([String], [[String]], [(String, SBool)])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 [(String, [String], (String, SBool))]
assumptions

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


                                  ]

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

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

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

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


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

        -- we only care about the fact that we can parse the output, so the
        -- result of parsing is ignored.
        String
-> (String -> Maybe [String] -> m String)
-> (SExpr -> m String)
-> m String
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m String
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m String) -> m String)
-> (SExpr -> m String) -> m String
forall a b. (a -> b) -> a -> b
$ \SExpr
_ -> String -> m String
forall (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 :: [String] -> m String
getInterpolantMathSAT [String]
fs
  | [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
fs
  = String -> m String
forall a. HasCallStack => String -> a
error String
"SBV.getInterpolantMathSAT requires at least one marked constraint, received none!"
  | Bool
True
  = do let bar :: String -> String
bar String
s = Char
'|' Char -> String -> String
forall a. a -> [a] -> [a]
: String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"|"
           cmd :: String
cmd = String
"(get-interpolant (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
bar [String]
fs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
           bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getInterpolant" String
cmd String
"a get-interpolant response"
                          (Maybe [String] -> String -> Maybe [String] -> m a)
-> Maybe [String] -> String -> Maybe [String] -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just [ String
"Make sure you use:"
                                 , String
""
                                 , String
"       setOption $ ProduceInterpolants True"
                                 , String
""
                                 , String
"to make sure the solver is ready for producing interpolants,"
                                 , String
"and that you have used the proper attributes using the"
                                 , String
"constrainWithAttribute function."
                                 ]

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

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


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

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

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

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

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

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

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

        String
-> (String -> Maybe [String] -> m [String])
-> (SExpr -> m [String])
-> m [String]
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m [String]
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m [String]) -> m [String])
-> (SExpr -> m [String]) -> m [String]
forall a b. (a -> b) -> a -> b
$ \SExpr
pe -> case SExpr
pe of
                                EApp [SExpr]
xs -> [String] -> m [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> m [String]) -> [String] -> m [String]
forall a b. (a -> b) -> a -> b
$ (SExpr -> String) -> [SExpr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SExpr -> String
render [SExpr]
xs
                                SExpr
_       -> [String] -> m [String]
forall (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 :: m [(String, Bool)]
getAssignment = do
        let cmd :: String
cmd = String
"(get-assignment)"
            bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getAssignment" String
cmd String
"a get-assignment response"
                           (Maybe [String] -> String -> Maybe [String] -> m a)
-> Maybe [String] -> String -> Maybe [String] -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just [ String
"Make sure you use:"
                                  , String
""
                                  , String
"       setOption $ ProduceAssignments True"
                                  , String
""
                                  , String
"to make sure the solver is ready for producing assignments,"
                                  , String
"and that there is a model by first issuing a 'checkSat' call."
                                  ]

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

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

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

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

-- | Generalization of 'Data.SBV.Control.mkSMTResult'
-- NB. This function does not allow users to create interpretations for UI-Funs. But that's
-- probably not a good idea anyhow. Also, if you use the 'validateModel' or 'optimizeValidateConstraints' features, SBV will
-- fail on models returned via this function.
mkSMTResult :: (MonadIO m, MonadQuery m) => [Assignment] -> m SMTResult
mkSMTResult :: [Assignment] -> m SMTResult
mkSMTResult [Assignment]
asgns = do
             QueryState{SMTConfig
queryConfig :: SMTConfig
queryConfig :: QueryState -> SMTConfig
queryConfig} <- m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState
             [(Quantifier, NamedSymVar)]
inps <- UserInputs -> [(Quantifier, NamedSymVar)]
userInputsToList (UserInputs -> [(Quantifier, NamedSymVar)])
-> m UserInputs -> m [(Quantifier, NamedSymVar)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m UserInputs
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) = State -> SBV Any -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st (SVal -> SBV Any
forall a. SVal -> SBV a
SBV SVal
s) IO SV -> (SV -> IO (SV, CV)) -> IO (SV, CV)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \SV
sv -> (SV, CV) -> IO (SV, CV)
forall (m :: * -> *) a. Monad m => a -> m a
return (SV
sv, CV
n)

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

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

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

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

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

                                              maxLen :: Int
maxLen = [Int] -> Int
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$  Int
0
                                                                Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
misTag | Bool -> Bool
not ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
missing)]
                                                               [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
extTag | Bool -> Bool
not ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
extra)]
                                                               [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
dupTag | Bool -> Bool
not ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
dup)]

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

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

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

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

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

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

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

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