-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.Control.Utils
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Query related utils.
-----------------------------------------------------------------------------

{-# LANGUAGE BangPatterns           #-}
{-# LANGUAGE DefaultSignatures      #-}
{-# LANGUAGE FlexibleContexts       #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE LambdaCase             #-}
{-# LANGUAGE NamedFieldPuns         #-}
{-# LANGUAGE ScopedTypeVariables    #-}
{-# LANGUAGE TupleSections          #-}
{-# LANGUAGE TypeApplications       #-}

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

module Data.SBV.Control.Utils (
       io
     , ask, send, getValue, getFunction, getUninterpretedValue
     , getValueCV, getUIFunCVAssoc, getUnsatAssumptions
     , SMTValue(..), SMTFunction(..), registerUISMTFunction
     , getQueryState, modifyQueryState, getConfig, getObjectives, getUIs
     , getSBVAssertions, getSBVPgm, getQuantifiedInputs, getObservables
     , checkSat, checkSatUsing, getAllSatResult
     , inNewContext, freshVar, freshVar_, freshArray, freshArray_
     , parse
     , unexpected
     , timeout
     , queryDebug
     , retrieveResponse
     , recoverKindedValue
     , runProofOn
     , executeQuery
     ) where

import Data.Maybe (isJust)
import Data.List  (sortBy, sortOn, elemIndex, partition, groupBy, tails, intercalate, nub, sort, isPrefixOf)

import Data.Char     (isPunctuation, isSpace, chr, ord, isDigit)
import Data.Function (on)

import Data.Proxy
import Data.Typeable (Typeable)

import Data.Int
import Data.Word

import qualified Data.Map.Strict    as Map
import qualified Data.IntMap.Strict as IMap
import qualified Data.Sequence      as S

import Control.Monad            (join, unless, zipWithM, when, replicateM)
import Control.Monad.IO.Class   (MonadIO, liftIO)
import Control.Monad.Trans      (lift)
import Control.Monad.Reader     (runReaderT)

import Data.IORef (readIORef, writeIORef)

import Data.Time (getZonedTime)

import Data.SBV.Core.Data     ( SV(..), trueSV, falseSV, CV(..), trueCV, falseCV, SBV, AlgReal, sbvToSV, kindOf, Kind(..)
                              , HasKind(..), mkConstCV, CVal(..), SMTResult(..)
                              , NamedSymVar, SMTConfig(..), SMTModel(..)
                              , QueryState(..), SVal(..), Quantifier(..), cache
                              , newExpr, SBVExpr(..), Op(..), FPOp(..), SBV(..), SymArray(..)
                              , SolverContext(..), SBool, Objective(..), SolverCapabilities(..), capabilities
                              , Result(..), SMTProblem(..), trueSV, SymVal(..), SBVPgm(..), SMTSolver(..), SBVRunMode(..)
                              , SBVType(..), forceSVArg, RoundingMode(RoundNearestTiesToEven), (.=>)
                              , RCSet(..)
                              )

import Data.SBV.Core.Symbolic ( IncState(..), withNewIncState, State(..), svToSV, symbolicEnv, SymbolicT
                              , MonadQuery(..), QueryContext(..), Queriable(..), Fresh(..)
                              , registerLabel, svMkSymVar, validationRequested
                              , isSafetyCheckingIStage, isSetupIStage, isRunIStage, IStage(..), QueryT(..)
                              , extractSymbolicSimulationState, MonadSymbolic(..), newUninterpreted
                              )

import Data.SBV.Core.AlgReals   (mergeAlgReals)
import Data.SBV.Core.Kind       (smtType, hasUninterpretedSorts)
import Data.SBV.Core.Operations (svNot, svNotEqual, svOr)

import Data.SBV.SMT.SMT     (showModel, parseCVs, SatModel)
import Data.SBV.SMT.SMTLib  (toIncSMTLib, toSMTLib)
import Data.SBV.SMT.Utils   (showTimeoutValue, addAnnotations, alignPlain, debug, mergeSExpr, SBVException(..))

import Data.SBV.Utils.ExtractIO
import Data.SBV.Utils.Lib       (qfsToString, isKString)
import Data.SBV.Utils.SExpr
import Data.SBV.Utils.PrettyNum (cvToSMTLib)

import Data.SBV.Control.Types

import qualified Data.Set as Set (empty, fromList, toAscList, map)

import qualified Control.Exception as C

import GHC.Stack

import Unsafe.Coerce (unsafeCoerce) -- Only used safely!

-- | 'Data.SBV.Trans.Control.QueryT' as a 'SolverContext'.
instance MonadIO m => SolverContext (QueryT m) where
   constrain :: SBool -> QueryT m ()
constrain              = Bool -> [(String, String)] -> SBool -> QueryT m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> [(String, String)] -> SBool -> m ()
addQueryConstraint Bool
False []
   softConstrain :: SBool -> QueryT m ()
softConstrain          = Bool -> [(String, String)] -> SBool -> QueryT m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> [(String, String)] -> SBool -> m ()
addQueryConstraint Bool
True  []
   namedConstraint :: String -> SBool -> QueryT m ()
namedConstraint nm :: String
nm     = Bool -> [(String, String)] -> SBool -> QueryT m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> [(String, String)] -> SBool -> m ()
addQueryConstraint Bool
False [(":named", String
nm)]
   constrainWithAttribute :: [(String, String)] -> SBool -> QueryT m ()
constrainWithAttribute = Bool -> [(String, String)] -> SBool -> QueryT m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> [(String, String)] -> SBool -> m ()
addQueryConstraint Bool
False
   contextState :: QueryT m State
contextState           = QueryT m State
forall (m :: * -> *). MonadQuery m => m State
queryState

   setOption :: SMTOption -> QueryT m ()
setOption o :: SMTOption
o
     | SMTOption -> Bool
isStartModeOption SMTOption
o = String -> QueryT m ()
forall a. HasCallStack => String -> a
error (String -> QueryT m ()) -> String -> QueryT m ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ ""
                                             , "*** Data.SBV: '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SMTOption -> String
forall a. Show a => a -> String
show SMTOption
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ "' can only be set at start-up time."
                                             , "*** Hint: Move the call to 'setOption' before the query."
                                             ]
     | Bool
True                = Bool -> String -> QueryT m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True (String -> QueryT m ()) -> String -> QueryT m ()
forall a b. (a -> b) -> a -> b
$ SMTOption -> String
setSMTOption SMTOption
o

-- | Adding a constraint, possibly with attributes and possibly soft. Only used internally.
-- Use 'constrain' and 'namedConstraint' from user programs.
addQueryConstraint :: (MonadIO m, MonadQuery m) => Bool -> [(String, String)] -> SBool -> m ()
addQueryConstraint :: Bool -> [(String, String)] -> SBool -> m ()
addQueryConstraint isSoft :: Bool
isSoft atts :: [(String, String)]
atts b :: SBool
b = do SV
sv <- (State -> IO SV) -> m SV
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext (\st :: State
st -> IO SV -> IO SV
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SV -> IO SV) -> IO SV -> IO SV
forall a b. (a -> b) -> a -> b
$ do (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> State -> String -> IO ()
registerLabel "Constraint" State
st) [String
nm | (":named", nm :: String
nm) <- [(String, String)]
atts]
                                                                             State -> SBool -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBool
b)

                                      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(String, String)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, String)]
atts Bool -> Bool -> Bool
&& SV
sv SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
                                             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 -> String
forall a. [a] -> [a] -> [a]
++ String
asrt String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(String, String)] -> String -> String
addAnnotations [(String, String)]
atts (SV -> String
forall a. Show a => a -> String
show SV
sv)  String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
   where asrt :: String
asrt | Bool
isSoft = "assert-soft"
              | Bool
True   = "assert"

-- | Get the current configuration
getConfig :: (MonadIO m, MonadQuery m) => m SMTConfig
getConfig :: m SMTConfig
getConfig = QueryState -> SMTConfig
queryConfig (QueryState -> SMTConfig) -> m QueryState -> m SMTConfig
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState

-- | Get the objectives
getObjectives :: (MonadIO m, MonadQuery m) => m [Objective (SV, SV)]
getObjectives :: m [Objective (SV, SV)]
getObjectives = do State{IORef [Objective (SV, SV)]
rOptGoals :: State -> IORef [Objective (SV, SV)]
rOptGoals :: IORef [Objective (SV, SV)]
rOptGoals} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
                   IO [Objective (SV, SV)] -> m [Objective (SV, SV)]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO [Objective (SV, SV)] -> m [Objective (SV, SV)])
-> IO [Objective (SV, SV)] -> m [Objective (SV, SV)]
forall a b. (a -> b) -> a -> b
$ [Objective (SV, SV)] -> [Objective (SV, SV)]
forall a. [a] -> [a]
reverse ([Objective (SV, SV)] -> [Objective (SV, SV)])
-> IO [Objective (SV, SV)] -> IO [Objective (SV, SV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef [Objective (SV, SV)] -> IO [Objective (SV, SV)]
forall a. IORef a -> IO a
readIORef IORef [Objective (SV, SV)]
rOptGoals

-- | Get the program
getSBVPgm :: (MonadIO m, MonadQuery m) => m SBVPgm
getSBVPgm :: m SBVPgm
getSBVPgm = do State{IORef SBVPgm
spgm :: State -> IORef SBVPgm
spgm :: IORef SBVPgm
spgm} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
               IO SBVPgm -> m SBVPgm
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO SBVPgm -> m SBVPgm) -> IO SBVPgm -> m SBVPgm
forall a b. (a -> b) -> a -> b
$ IORef SBVPgm -> IO SBVPgm
forall a. IORef a -> IO a
readIORef IORef SBVPgm
spgm

-- | Get the assertions put in via 'Data.SBV.sAssert'
getSBVAssertions :: (MonadIO m, MonadQuery m) => m [(String, Maybe CallStack, SV)]
getSBVAssertions :: m [(String, Maybe CallStack, SV)]
getSBVAssertions = do State{IORef [(String, Maybe CallStack, SV)]
rAsserts :: State -> IORef [(String, Maybe CallStack, SV)]
rAsserts :: IORef [(String, Maybe CallStack, SV)]
rAsserts} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
                      IO [(String, Maybe CallStack, SV)]
-> m [(String, Maybe CallStack, SV)]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO [(String, Maybe CallStack, SV)]
 -> m [(String, Maybe CallStack, SV)])
-> IO [(String, Maybe CallStack, SV)]
-> m [(String, Maybe CallStack, SV)]
forall a b. (a -> b) -> a -> b
$ [(String, Maybe CallStack, SV)] -> [(String, Maybe CallStack, SV)]
forall a. [a] -> [a]
reverse ([(String, Maybe CallStack, SV)]
 -> [(String, Maybe CallStack, SV)])
-> IO [(String, Maybe CallStack, SV)]
-> IO [(String, Maybe CallStack, SV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef [(String, Maybe CallStack, SV)]
-> IO [(String, Maybe CallStack, SV)]
forall a. IORef a -> IO a
readIORef IORef [(String, Maybe CallStack, SV)]
rAsserts

-- | Generalization of 'Data.SBV.Control.io'
io :: MonadIO m => IO a -> m a
io :: IO a -> m a
io = IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO

-- | Sync-up the external solver with new context we have generated
syncUpSolver :: (MonadIO m, MonadQuery m) => Bool -> IncState -> m ()
syncUpSolver :: Bool -> IncState -> m ()
syncUpSolver afterAPush :: Bool
afterAPush is :: IncState
is = do
        SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
        [String]
ls  <- IO [String] -> m [String]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO [String] -> m [String]) -> IO [String] -> m [String]
forall a b. (a -> b) -> a -> b
$ do let swap :: (b, a) -> (a, b)
swap  (a :: b
a, b :: a
b)        = (a
b, b
a)
                           cmp :: (a, b) -> (a, b) -> Ordering
cmp   (a :: a
a, _) (b :: a
b, _) = a
a a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
b
                           arrange :: (a, (b, c, b)) -> ((a, b, c), b)
arrange (i :: a
i, (at :: b
at, rt :: c
rt, es :: b
es)) = ((a
i, b
at, c
rt), b
es)
                       [NamedSymVar]
inps        <- [NamedSymVar] -> [NamedSymVar]
forall a. [a] -> [a]
reverse ([NamedSymVar] -> [NamedSymVar])
-> IO [NamedSymVar] -> IO [NamedSymVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef [NamedSymVar] -> IO [NamedSymVar]
forall a. IORef a -> IO a
readIORef (IncState -> IORef [NamedSymVar]
rNewInps IncState
is)
                       KindSet
ks          <- IORef KindSet -> IO KindSet
forall a. IORef a -> IO a
readIORef (IncState -> IORef KindSet
rNewKinds IncState
is)
                       [(SV, CV)]
cnsts       <- ((SV, CV) -> (SV, CV) -> Ordering) -> [(SV, CV)] -> [(SV, CV)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (SV, CV) -> (SV, CV) -> Ordering
forall a b b. Ord a => (a, b) -> (a, b) -> Ordering
cmp ([(SV, CV)] -> [(SV, CV)])
-> (Map CV SV -> [(SV, CV)]) -> Map CV SV -> [(SV, CV)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((CV, SV) -> (SV, CV)) -> [(CV, SV)] -> [(SV, CV)]
forall a b. (a -> b) -> [a] -> [b]
map (CV, SV) -> (SV, CV)
forall b a. (b, a) -> (a, b)
swap ([(CV, SV)] -> [(SV, CV)])
-> (Map CV SV -> [(CV, SV)]) -> Map CV SV -> [(SV, CV)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map CV SV -> [(CV, SV)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map CV SV -> [(SV, CV)]) -> IO (Map CV SV) -> IO [(SV, CV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (Map CV SV) -> IO (Map CV SV)
forall a. IORef a -> IO a
readIORef (IncState -> IORef (Map CV SV)
rNewConsts IncState
is)
                       [(Key, ArrayInfo)]
arrs        <- IntMap ArrayInfo -> [(Key, ArrayInfo)]
forall a. IntMap a -> [(Key, a)]
IMap.toAscList (IntMap ArrayInfo -> [(Key, ArrayInfo)])
-> IO (IntMap ArrayInfo) -> IO [(Key, ArrayInfo)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (IntMap ArrayInfo) -> IO (IntMap ArrayInfo)
forall a. IORef a -> IO a
readIORef (IncState -> IORef (IntMap ArrayInfo)
rNewArrs IncState
is)
                       [((Key, Kind, Kind), [SV])]
tbls        <- ((Key, (Kind, Kind, [SV])) -> ((Key, Kind, Kind), [SV]))
-> [(Key, (Kind, Kind, [SV]))] -> [((Key, Kind, Kind), [SV])]
forall a b. (a -> b) -> [a] -> [b]
map (Key, (Kind, Kind, [SV])) -> ((Key, Kind, Kind), [SV])
forall a b c b. (a, (b, c, b)) -> ((a, b, c), b)
arrange ([(Key, (Kind, Kind, [SV]))] -> [((Key, Kind, Kind), [SV])])
-> (Map (Kind, Kind, [SV]) Key -> [(Key, (Kind, Kind, [SV]))])
-> Map (Kind, Kind, [SV]) Key
-> [((Key, Kind, Kind), [SV])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Key, (Kind, Kind, [SV]))
 -> (Key, (Kind, Kind, [SV])) -> Ordering)
-> [(Key, (Kind, Kind, [SV]))] -> [(Key, (Kind, Kind, [SV]))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Key, (Kind, Kind, [SV])) -> (Key, (Kind, Kind, [SV])) -> Ordering
forall a b b. Ord a => (a, b) -> (a, b) -> Ordering
cmp ([(Key, (Kind, Kind, [SV]))] -> [(Key, (Kind, Kind, [SV]))])
-> (Map (Kind, Kind, [SV]) Key -> [(Key, (Kind, Kind, [SV]))])
-> Map (Kind, Kind, [SV]) Key
-> [(Key, (Kind, Kind, [SV]))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Kind, Kind, [SV]), Key) -> (Key, (Kind, Kind, [SV])))
-> [((Kind, Kind, [SV]), Key)] -> [(Key, (Kind, Kind, [SV]))]
forall a b. (a -> b) -> [a] -> [b]
map ((Kind, Kind, [SV]), Key) -> (Key, (Kind, Kind, [SV]))
forall b a. (b, a) -> (a, b)
swap ([((Kind, Kind, [SV]), Key)] -> [(Key, (Kind, Kind, [SV]))])
-> (Map (Kind, Kind, [SV]) Key -> [((Kind, Kind, [SV]), Key)])
-> Map (Kind, Kind, [SV]) Key
-> [(Key, (Kind, Kind, [SV]))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Kind, Kind, [SV]) Key -> [((Kind, Kind, [SV]), Key)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map (Kind, Kind, [SV]) Key -> [((Key, Kind, Kind), [SV])])
-> IO (Map (Kind, Kind, [SV]) Key)
-> IO [((Key, Kind, Kind), [SV])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (Map (Kind, Kind, [SV]) Key)
-> IO (Map (Kind, Kind, [SV]) Key)
forall a. IORef a -> IO a
readIORef (IncState -> IORef (Map (Kind, Kind, [SV]) Key)
rNewTbls IncState
is)
                       [(String, SBVType)]
uis         <- Map String SBVType -> [(String, SBVType)]
forall k a. Map k a -> [(k, a)]
Map.toAscList (Map String SBVType -> [(String, SBVType)])
-> IO (Map String SBVType) -> IO [(String, SBVType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (Map String SBVType) -> IO (Map String SBVType)
forall a. IORef a -> IO a
readIORef (IncState -> IORef (Map String SBVType)
rNewUIs IncState
is)
                       SBVPgm
as          <- IORef SBVPgm -> IO SBVPgm
forall a. IORef a -> IO a
readIORef (IncState -> IORef SBVPgm
rNewAsgns IncState
is)
                       Seq (Bool, [(String, String)], SV)
constraints <- IORef (Seq (Bool, [(String, String)], SV))
-> IO (Seq (Bool, [(String, String)], SV))
forall a. IORef a -> IO a
readIORef (IncState -> IORef (Seq (Bool, [(String, String)], SV))
rNewConstraints IncState
is)

                       [String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ Bool -> SMTConfig -> SMTLibIncConverter [String]
toIncSMTLib Bool
afterAPush SMTConfig
cfg [NamedSymVar]
inps KindSet
ks [(SV, CV)]
cnsts [(Key, ArrayInfo)]
arrs [((Key, Kind, Kind), [SV])]
tbls [(String, SBVType)]
uis SBVPgm
as Seq (Bool, [(String, String)], SV)
constraints SMTConfig
cfg
        (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]
mergeSExpr [String]
ls

-- | Retrieve the query context
getQueryState :: (MonadIO m, MonadQuery m) => m QueryState
getQueryState :: m QueryState
getQueryState = do State
state <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
                   Maybe QueryState
mbQS  <- IO (Maybe QueryState) -> m (Maybe QueryState)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (Maybe QueryState) -> m (Maybe QueryState))
-> IO (Maybe QueryState) -> m (Maybe QueryState)
forall a b. (a -> b) -> a -> b
$ IORef (Maybe QueryState) -> IO (Maybe QueryState)
forall a. IORef a -> IO a
readIORef (State -> IORef (Maybe QueryState)
rQueryState State
state)
                   case Maybe QueryState
mbQS of
                     Nothing -> String -> m QueryState
forall a. HasCallStack => String -> a
error (String -> m QueryState) -> String -> m QueryState
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ ""
                                                , "*** Data.SBV: Impossible happened: Query context required in a non-query mode."
                                                , "Please report this as a bug!"
                                                ]
                     Just qs :: QueryState
qs -> QueryState -> m QueryState
forall (m :: * -> *) a. Monad m => a -> m a
return QueryState
qs

-- | Generalization of 'Data.SBV.Control.modifyQueryState'
modifyQueryState :: (MonadIO m, MonadQuery m) => (QueryState -> QueryState) -> m ()
modifyQueryState :: (QueryState -> QueryState) -> m ()
modifyQueryState f :: QueryState -> QueryState
f = do State
state <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
                        Maybe QueryState
mbQS  <- IO (Maybe QueryState) -> m (Maybe QueryState)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (Maybe QueryState) -> m (Maybe QueryState))
-> IO (Maybe QueryState) -> m (Maybe QueryState)
forall a b. (a -> b) -> a -> b
$ IORef (Maybe QueryState) -> IO (Maybe QueryState)
forall a. IORef a -> IO a
readIORef (State -> IORef (Maybe QueryState)
rQueryState State
state)
                        case Maybe QueryState
mbQS of
                          Nothing -> String -> m ()
forall a. HasCallStack => String -> a
error (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ ""
                                                     , "*** Data.SBV: Impossible happened: Query context required in a non-query mode."
                                                     , "Please report this as a bug!"
                                                     ]
                          Just qs :: QueryState
qs -> let fqs :: QueryState
fqs = QueryState -> QueryState
f QueryState
qs
                                     in QueryState
fqs QueryState -> m () -> m ()
forall a b. a -> b -> b
`seq` IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IORef (Maybe QueryState) -> Maybe QueryState -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (State -> IORef (Maybe QueryState)
rQueryState State
state) (Maybe QueryState -> IO ()) -> Maybe QueryState -> IO ()
forall a b. (a -> b) -> a -> b
$ QueryState -> Maybe QueryState
forall a. a -> Maybe a
Just QueryState
fqs

-- | Generalization of 'Data.SBV.Control.inNewContext'
inNewContext :: (MonadIO m, MonadQuery m) => (State -> IO a) -> m a
inNewContext :: (State -> IO a) -> m a
inNewContext act :: State -> IO a
act = do State
st <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
                      (is :: IncState
is, r :: a
r) <- IO (IncState, a) -> m (IncState, a)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (IncState, a) -> m (IncState, a))
-> IO (IncState, a) -> m (IncState, a)
forall a b. (a -> b) -> a -> b
$ State -> (State -> IO a) -> IO (IncState, a)
forall a. State -> (State -> IO a) -> IO (IncState, a)
withNewIncState State
st State -> IO a
act
                      Maybe QueryState
mbQS <- IO (Maybe QueryState) -> m (Maybe QueryState)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (Maybe QueryState) -> m (Maybe QueryState))
-> (State -> IO (Maybe QueryState))
-> State
-> m (Maybe QueryState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IORef (Maybe QueryState) -> IO (Maybe QueryState)
forall a. IORef a -> IO a
readIORef (IORef (Maybe QueryState) -> IO (Maybe QueryState))
-> (State -> IORef (Maybe QueryState))
-> State
-> IO (Maybe QueryState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State -> IORef (Maybe QueryState)
rQueryState (State -> m (Maybe QueryState)) -> State -> m (Maybe QueryState)
forall a b. (a -> b) -> a -> b
$ State
st
                      let afterAPush :: Bool
afterAPush = case Maybe QueryState
mbQS of
                                         Nothing -> Bool
False
                                         Just qs :: QueryState
qs -> Maybe (Key, Key) -> Bool
forall a. Maybe a -> Bool
isJust (QueryState -> Maybe (Key, Key)
queryTblArrPreserveIndex QueryState
qs)
                      Bool -> IncState -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> IncState -> m ()
syncUpSolver Bool
afterAPush IncState
is
                      a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r

-- | Generic 'Queriable' instance for 'SymVal'/'SMTValue' values
instance (MonadIO m, SymVal a, SMTValue a) => Queriable m (SBV a) a where
  create :: QueryT m (SBV a)
create  = QueryT m (SBV a)
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_
  project :: SBV a -> QueryT m a
project = SBV a -> QueryT m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, SMTValue a) =>
SBV a -> m a
getValue
  embed :: a -> QueryT m (SBV a)
embed   = SBV a -> QueryT m (SBV a)
forall (m :: * -> *) a. Monad m => a -> m a
return (SBV a -> QueryT m (SBV a))
-> (a -> SBV a) -> a -> QueryT m (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SBV a
forall a. SymVal a => a -> SBV a
literal

-- | Generic 'Queriable' instance for things that are 'Fresh' and look like containers:
instance (MonadIO m, SymVal a, SMTValue a, Foldable t, Traversable t, Fresh m (t (SBV a))) => Queriable m (t (SBV a)) (t a) where
  create :: QueryT m (t (SBV a))
create  = QueryT m (t (SBV a))
forall (m :: * -> *) a. Fresh m a => QueryT m a
fresh
  project :: t (SBV a) -> QueryT m (t a)
project = (SBV a -> QueryT m a) -> t (SBV a) -> QueryT m (t a)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SBV a -> QueryT m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, SMTValue a) =>
SBV a -> m a
getValue
  embed :: t a -> QueryT m (t (SBV a))
embed   = t (SBV a) -> QueryT m (t (SBV a))
forall (m :: * -> *) a. Monad m => a -> m a
return (t (SBV a) -> QueryT m (t (SBV a)))
-> (t a -> t (SBV a)) -> t a -> QueryT m (t (SBV a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> SBV a) -> t a -> t (SBV a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> SBV a
forall a. SymVal a => a -> SBV a
literal

-- | Generalization of 'Data.SBV.Control.freshVar_'
freshVar_ :: forall a m. (MonadIO m, MonadQuery m, SymVal a) => m (SBV a)
freshVar_ :: m (SBV a)
freshVar_ = (State -> IO (SBV a)) -> m (SBV a)
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext ((State -> IO (SBV a)) -> m (SBV a))
-> (State -> IO (SBV a)) -> m (SBV a)
forall a b. (a -> b) -> a -> b
$ (SVal -> SBV a) -> IO SVal -> IO (SBV a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBV a
forall a. SVal -> SBV a
SBV (IO SVal -> IO (SBV a))
-> (State -> IO SVal) -> State -> IO (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
EX) Kind
k Maybe String
forall a. Maybe a
Nothing
  where k :: Kind
k = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)

-- | Generalization of 'Data.SBV.Control.freshVar'
freshVar :: forall a m. (MonadIO m, MonadQuery m, SymVal a) => String -> m (SBV a)
freshVar :: String -> m (SBV a)
freshVar nm :: String
nm = (State -> IO (SBV a)) -> m (SBV a)
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext ((State -> IO (SBV a)) -> m (SBV a))
-> (State -> IO (SBV a)) -> m (SBV a)
forall a b. (a -> b) -> a -> b
$ (SVal -> SBV a) -> IO SVal -> IO (SBV a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBV a
forall a. SVal -> SBV a
SBV (IO SVal -> IO (SBV a))
-> (State -> IO SVal) -> State -> IO (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe Quantifier -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar (Quantifier -> Maybe Quantifier
forall a. a -> Maybe a
Just Quantifier
EX) Kind
k (String -> Maybe String
forall a. a -> Maybe a
Just String
nm)
  where k :: Kind
k = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)

-- | Generalization of 'Data.SBV.Control.freshArray_'
freshArray_ :: (MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) => Maybe (SBV b) -> m (array a b)
freshArray_ :: Maybe (SBV b) -> m (array a b)
freshArray_ = Maybe String -> Maybe (SBV b) -> m (array a b)
forall (m :: * -> *) (array :: * -> * -> *) a b.
(MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) =>
Maybe String -> Maybe (SBV b) -> m (array a b)
mkFreshArray Maybe String
forall a. Maybe a
Nothing

-- | Generalization of 'Data.SBV.Control.freshArray'
freshArray :: (MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (array a b)
freshArray :: String -> Maybe (SBV b) -> m (array a b)
freshArray nm :: String
nm = Maybe String -> Maybe (SBV b) -> m (array a b)
forall (m :: * -> *) (array :: * -> * -> *) a b.
(MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) =>
Maybe String -> Maybe (SBV b) -> m (array a b)
mkFreshArray (String -> Maybe String
forall a. a -> Maybe a
Just String
nm)

-- | Creating arrays, internal use only.
mkFreshArray :: (MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> m (array a b)
mkFreshArray :: Maybe String -> Maybe (SBV b) -> m (array a b)
mkFreshArray mbNm :: Maybe String
mbNm mbVal :: Maybe (SBV b)
mbVal = (State -> IO (array a b)) -> m (array a b)
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext ((State -> IO (array a b)) -> m (array a b))
-> (State -> IO (array a b)) -> m (array a b)
forall a b. (a -> b) -> a -> b
$ Maybe String -> Maybe (SBV b) -> State -> IO (array a b)
forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, HasKind b) =>
Maybe String -> Maybe (SBV b) -> State -> IO (array a b)
newArrayInState Maybe String
mbNm Maybe (SBV b)
mbVal

-- | Generalization of 'Data.SBV.Control.queryDebug'
queryDebug :: (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug :: [String] -> m ()
queryDebug msgs :: [String]
msgs = do QueryState{SMTConfig
queryConfig :: SMTConfig
queryConfig :: QueryState -> SMTConfig
queryConfig} <- m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState
                     IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ SMTConfig -> [String] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
debug SMTConfig
queryConfig [String]
msgs

-- | Generalization of 'Data.SBV.Control.ask'
ask :: (MonadIO m, MonadQuery m) => String -> m String
ask :: String -> m String
ask s :: String
s = do QueryState{Maybe Key -> String -> IO String
queryAsk :: QueryState -> Maybe Key -> String -> IO String
queryAsk :: Maybe Key -> String -> IO String
queryAsk, Maybe Key
queryTimeOutValue :: QueryState -> Maybe Key
queryTimeOutValue :: Maybe Key
queryTimeOutValue} <- m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState

           case Maybe Key
queryTimeOutValue of
             Nothing -> [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["[SEND] " String -> String -> String
`alignPlain` String
s]
             Just i :: Key
i  -> [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["[SEND, TimeOut: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
showTimeoutValue Key
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ "] " String -> String -> String
`alignPlain` String
s]
           String
r <- IO String -> m String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO String -> m String) -> IO String -> m String
forall a b. (a -> b) -> a -> b
$ Maybe Key -> String -> IO String
queryAsk Maybe Key
queryTimeOutValue String
s
           [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["[RECV] " String -> String -> String
`alignPlain` String
r]

           String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return String
r

-- | Send a string to the solver, and return the response. Except, if the response
-- is one of the "ignore" ones, keep querying.
askIgnoring :: (MonadIO m, MonadQuery m) => String -> [String] -> m String
askIgnoring :: String -> [String] -> m String
askIgnoring s :: String
s ignoreList :: [String]
ignoreList = do

           QueryState{Maybe Key -> String -> IO String
queryAsk :: Maybe Key -> String -> IO String
queryAsk :: QueryState -> Maybe Key -> String -> IO String
queryAsk, Maybe Key -> IO String
queryRetrieveResponse :: QueryState -> Maybe Key -> IO String
queryRetrieveResponse :: Maybe Key -> IO String
queryRetrieveResponse, Maybe Key
queryTimeOutValue :: Maybe Key
queryTimeOutValue :: QueryState -> Maybe Key
queryTimeOutValue} <- m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState

           case Maybe Key
queryTimeOutValue of
             Nothing -> [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["[SEND] " String -> String -> String
`alignPlain` String
s]
             Just i :: Key
i  -> [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["[SEND, TimeOut: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
showTimeoutValue Key
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ "] " String -> String -> String
`alignPlain` String
s]
           String
r <- IO String -> m String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO String -> m String) -> IO String -> m String
forall a b. (a -> b) -> a -> b
$ Maybe Key -> String -> IO String
queryAsk Maybe Key
queryTimeOutValue String
s
           [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["[RECV] " String -> String -> String
`alignPlain` String
r]

           let loop :: String -> m String
loop currentResponse :: String
currentResponse
                 | String
currentResponse String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
ignoreList
                 = String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return String
currentResponse
                 | Bool
True
                 = do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["[WARN] Previous response is explicitly ignored, beware!"]
                      String
newResponse <- IO String -> m String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO String -> m String) -> IO String -> m String
forall a b. (a -> b) -> a -> b
$ Maybe Key -> IO String
queryRetrieveResponse Maybe Key
queryTimeOutValue
                      [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["[RECV] " String -> String -> String
`alignPlain` String
newResponse]
                      String -> m String
loop String
newResponse

           String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
loop String
r

-- | Generalization of 'Data.SBV.Control.send'
send :: (MonadIO m, MonadQuery m) => Bool -> String -> m ()
send :: Bool -> String -> m ()
send requireSuccess :: Bool
requireSuccess s :: String
s = do

            QueryState{Maybe Key -> String -> IO String
queryAsk :: Maybe Key -> String -> IO String
queryAsk :: QueryState -> Maybe Key -> String -> IO String
queryAsk, Maybe Key -> String -> IO ()
querySend :: QueryState -> Maybe Key -> String -> IO ()
querySend :: Maybe Key -> String -> IO ()
querySend, SMTConfig
queryConfig :: SMTConfig
queryConfig :: QueryState -> SMTConfig
queryConfig, Maybe Key
queryTimeOutValue :: Maybe Key
queryTimeOutValue :: QueryState -> Maybe Key
queryTimeOutValue} <- m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState

            if Bool
requireSuccess Bool -> Bool -> Bool
&& SolverCapabilities -> Bool
supportsCustomQueries (SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
queryConfig))
               then do String
r <- IO String -> m String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO String -> m String) -> IO String -> m String
forall a b. (a -> b) -> a -> b
$ Maybe Key -> String -> IO String
queryAsk Maybe Key
queryTimeOutValue String
s

                       case String -> [String]
words String
r of
                         ["success"] -> [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["[GOOD] " String -> String -> String
`alignPlain` String
s]
                         _           -> do case Maybe Key
queryTimeOutValue of
                                             Nothing -> [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["[FAIL] " String -> String -> String
`alignPlain` String
s]
                                             Just i :: Key
i  -> [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [("[FAIL, TimeOut: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
showTimeoutValue Key
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ "]  ") String -> String -> String
`alignPlain` String
s]


                                           let cmd :: String
cmd = case String -> [String]
words ((Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
dropWhile (\c :: Char
c -> Char -> Bool
isSpace Char
c Bool -> Bool -> Bool
|| Char -> Bool
isPunctuation Char
c) String
s) of
                                                       (c :: String
c:_) -> String
c
                                                       _     -> "Command"

                                           String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m ()
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
cmd String
s "success" Maybe [String]
forall a. Maybe a
Nothing String
r Maybe [String]
forall a. Maybe a
Nothing

               else do -- fire and forget. if you use this, you're on your own!
                       [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["[FIRE] " String -> String -> String
`alignPlain` String
s]
                       IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Maybe Key -> String -> IO ()
querySend Maybe Key
queryTimeOutValue String
s

-- | Generalization of 'Data.SBV.Control.retrieveResponse'
retrieveResponse :: (MonadIO m, MonadQuery m) => String -> Maybe Int -> m [String]
retrieveResponse :: String -> Maybe Key -> m [String]
retrieveResponse userTag :: String
userTag mbTo :: Maybe Key
mbTo = do
             String
ts  <- IO String -> m String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (ZonedTime -> String
forall a. Show a => a -> String
show (ZonedTime -> String) -> IO ZonedTime -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO ZonedTime
getZonedTime)

             let synchTag :: String
synchTag = String -> String
forall a. Show a => a -> String
show (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
userTag String -> String -> String
forall a. [a] -> [a] -> [a]
++ " (at: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ts String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                 cmd :: String
cmd = "(echo " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
synchTag String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

             [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["[SYNC] Attempting to synchronize with tag: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
synchTag]

             Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
False String
cmd

             QueryState{Maybe Key -> IO String
queryRetrieveResponse :: Maybe Key -> IO String
queryRetrieveResponse :: QueryState -> Maybe Key -> IO String
queryRetrieveResponse} <- m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState

             let loop :: [String] -> m [String]
loop sofar :: [String]
sofar = do
                  String
s <- IO String -> m String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO String -> m String) -> IO String -> m String
forall a b. (a -> b) -> a -> b
$ Maybe Key -> IO String
queryRetrieveResponse Maybe Key
mbTo

                  -- strictly speaking SMTLib requires solvers to print quotes around
                  -- echo'ed strings, but they don't always do. Accommodate for that
                  -- here, though I wish we didn't have to.
                  if String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
synchTag Bool -> Bool -> Bool
|| String -> String
forall a. Show a => a -> String
show String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
synchTag
                     then do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["[SYNC] Synchronization achieved using tag: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
synchTag]
                             [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]
forall a. [a] -> [a]
reverse [String]
sofar
                     else do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["[RECV] " String -> String -> String
`alignPlain` String
s]
                             [String] -> m [String]
loop (String
s String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)

             [String] -> m [String]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
[String] -> m [String]
loop []

-- | A class which allows for sexpr-conversion to values
class SMTValue a where
  sexprToVal :: SExpr -> Maybe a

  default sexprToVal :: Read a => SExpr -> Maybe a
  sexprToVal (ECon c :: String
c) = case ReadS a
forall a. Read a => ReadS a
reads String
c of
                          [(v :: a
v, "")] -> a -> Maybe a
forall a. a -> Maybe a
Just a
v
                          _         -> Maybe a
forall a. Maybe a
Nothing
  sexprToVal _        = Maybe a
forall a. Maybe a
Nothing

-- | Integral values are easy to convert:
fromIntegralToVal :: Integral a => SExpr -> Maybe a
fromIntegralToVal :: SExpr -> Maybe a
fromIntegralToVal (ENum (i :: Integer
i, _)) = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ Integer -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i
fromIntegralToVal _             = Maybe a
forall a. Maybe a
Nothing

instance SMTValue Int8    where sexprToVal :: SExpr -> Maybe Int8
sexprToVal = SExpr -> Maybe Int8
forall a. Integral a => SExpr -> Maybe a
fromIntegralToVal
instance SMTValue Int16   where sexprToVal :: SExpr -> Maybe Int16
sexprToVal = SExpr -> Maybe Int16
forall a. Integral a => SExpr -> Maybe a
fromIntegralToVal
instance SMTValue Int32   where sexprToVal :: SExpr -> Maybe Int32
sexprToVal = SExpr -> Maybe Int32
forall a. Integral a => SExpr -> Maybe a
fromIntegralToVal
instance SMTValue Int64   where sexprToVal :: SExpr -> Maybe Int64
sexprToVal = SExpr -> Maybe Int64
forall a. Integral a => SExpr -> Maybe a
fromIntegralToVal
instance SMTValue Word8   where sexprToVal :: SExpr -> Maybe Word8
sexprToVal = SExpr -> Maybe Word8
forall a. Integral a => SExpr -> Maybe a
fromIntegralToVal
instance SMTValue Word16  where sexprToVal :: SExpr -> Maybe Word16
sexprToVal = SExpr -> Maybe Word16
forall a. Integral a => SExpr -> Maybe a
fromIntegralToVal
instance SMTValue Word32  where sexprToVal :: SExpr -> Maybe Word32
sexprToVal = SExpr -> Maybe Word32
forall a. Integral a => SExpr -> Maybe a
fromIntegralToVal
instance SMTValue Word64  where sexprToVal :: SExpr -> Maybe Word64
sexprToVal = SExpr -> Maybe Word64
forall a. Integral a => SExpr -> Maybe a
fromIntegralToVal
instance SMTValue Integer where sexprToVal :: SExpr -> Maybe Integer
sexprToVal = SExpr -> Maybe Integer
forall a. Integral a => SExpr -> Maybe a
fromIntegralToVal

instance SMTValue Float where
   sexprToVal :: SExpr -> Maybe Float
sexprToVal (EFloat f :: Float
f)    = Float -> Maybe Float
forall a. a -> Maybe a
Just Float
f
   sexprToVal (ENum (v :: Integer
v, _)) = Float -> Maybe Float
forall a. a -> Maybe a
Just (Integer -> Float
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
v)
   sexprToVal _             = Maybe Float
forall a. Maybe a
Nothing

instance SMTValue Double where
   sexprToVal :: SExpr -> Maybe Double
sexprToVal (EDouble f :: Double
f)   = Double -> Maybe Double
forall a. a -> Maybe a
Just Double
f
   sexprToVal (ENum (v :: Integer
v, _)) = Double -> Maybe Double
forall a. a -> Maybe a
Just (Integer -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
v)
   sexprToVal _             = Maybe Double
forall a. Maybe a
Nothing

instance SMTValue Bool where
   sexprToVal :: SExpr -> Maybe Bool
sexprToVal (ENum (1, _)) = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
   sexprToVal (ENum (0, _)) = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
   sexprToVal _             = Maybe Bool
forall a. Maybe a
Nothing

instance SMTValue AlgReal where
   sexprToVal :: SExpr -> Maybe AlgReal
sexprToVal (EReal a :: AlgReal
a)     = AlgReal -> Maybe AlgReal
forall a. a -> Maybe a
Just AlgReal
a
   sexprToVal (ENum (v :: Integer
v, _)) = AlgReal -> Maybe AlgReal
forall a. a -> Maybe a
Just (Integer -> AlgReal
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
v)
   sexprToVal _             = Maybe AlgReal
forall a. Maybe a
Nothing

instance SMTValue Char where
   sexprToVal :: SExpr -> Maybe Char
sexprToVal (ENum (i :: Integer
i, _)) = Char -> Maybe Char
forall a. a -> Maybe a
Just (Key -> Char
chr (Integer -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i))
   sexprToVal _             = Maybe Char
forall a. Maybe a
Nothing

instance (SMTValue a, Typeable a) => SMTValue [a] where
   -- NB. The conflation of String/[Char] forces us to have this bastard case here
   -- with unsafeCoerce to cast back to a regular string. This is unfortunate,
   -- and the ice is thin here. But it works, and is much better than a plethora
   -- of overlapping instances. Sigh.
   sexprToVal :: SExpr -> Maybe [a]
sexprToVal (ECon s :: String
s)
    | [a] -> Bool
forall a. Typeable a => a -> Bool
isKString @[a] [a]
forall a. HasCallStack => a
undefined Bool -> Bool -> Bool
&& String -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length String
s Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
>= 2 Bool -> Bool -> Bool
&& String -> Char
forall a. [a] -> a
head String
s Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '"' Bool -> Bool -> Bool
&& String -> Char
forall a. [a] -> a
last String
s Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '"'
    = [a] -> Maybe [a]
forall a. a -> Maybe a
Just ([a] -> Maybe [a]) -> [a] -> Maybe [a]
forall a b. (a -> b) -> a -> b
$ (Char -> a) -> String -> [a]
forall a b. (a -> b) -> [a] -> [b]
map Char -> a
forall a b. a -> b
unsafeCoerce String
s'
    | Bool
True
    = [a] -> Maybe [a]
forall a. a -> Maybe a
Just ([a] -> Maybe [a]) -> [a] -> Maybe [a]
forall a b. (a -> b) -> a -> b
$ (Char -> a) -> String -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (Word8 -> a
forall a b. a -> b
unsafeCoerce (Word8 -> a) -> (Char -> Word8) -> Char -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Word8
c2w8) String
s'
    where s' :: String
s' = String -> String
qfsToString (String -> String
forall a. [a] -> [a]
tail (String -> String
forall a. [a] -> [a]
init String
s))
          c2w8  :: Char -> Word8
          c2w8 :: Char -> Word8
c2w8 = Key -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Key -> Word8) -> (Char -> Key) -> Char -> Word8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Key
ord

   -- Otherwise we have a good old sequence, just parse it simply:
   sexprToVal (EApp (ECon "seq.++" : rest :: [SExpr]
rest))           = do [[a]]
elts <- (SExpr -> Maybe [a]) -> [SExpr] -> Maybe [[a]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SExpr -> Maybe [a]
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal [SExpr]
rest
                                                           [a] -> Maybe [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ([a] -> Maybe [a]) -> [a] -> Maybe [a]
forall a b. (a -> b) -> a -> b
$ [[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[a]]
elts
   sexprToVal (EApp [ECon "seq.unit", a :: SExpr
a])             = do a
a' <- SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a
                                                           [a] -> Maybe [a]
forall (m :: * -> *) a. Monad m => a -> m a
return [a
a']
   sexprToVal (EApp [ECon "as", ECon "seq.empty", _]) = [a] -> Maybe [a]
forall (m :: * -> *) a. Monad m => a -> m a
return []

   sexprToVal _                                       = Maybe [a]
forall a. Maybe a
Nothing

instance (SMTValue a, SMTValue b) => SMTValue (Either a b) where
  sexprToVal :: SExpr -> Maybe (Either a b)
sexprToVal (EApp [ECon "left_SBVEither",  a :: SExpr
a])                      = a -> Either a b
forall a b. a -> Either a b
Left  (a -> Either a b) -> Maybe a -> Maybe (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a
  sexprToVal (EApp [ECon "right_SBVEither", b :: SExpr
b])                      = b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> Maybe b -> Maybe (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe b
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
b
  sexprToVal (EApp [EApp [ECon "as", ECon "left_SBVEither",  _], a :: SExpr
a]) = a -> Either a b
forall a b. a -> Either a b
Left  (a -> Either a b) -> Maybe a -> Maybe (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a   -- CVC4 puts full ascriptions
  sexprToVal (EApp [EApp [ECon "as", ECon "right_SBVEither", _], b :: SExpr
b]) = b -> Either a b
forall a b. b -> Either a b
Right (b -> Either a b) -> Maybe b -> Maybe (Either a b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe b
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
b   -- CVC4 puts full ascriptions
  sexprToVal _                                                       = Maybe (Either a b)
forall a. Maybe a
Nothing

instance SMTValue a => SMTValue (Maybe a) where
  sexprToVal :: SExpr -> Maybe (Maybe a)
sexprToVal (ECon "nothing_SBVMaybe")                                = Maybe a -> Maybe (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing
  sexprToVal (EApp [ECon "just_SBVMaybe", a :: SExpr
a])                         = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> Maybe a -> Maybe (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a
  sexprToVal (      EApp [ECon "as", ECon "nothing_SBVMaybe", _])     = Maybe a -> Maybe (Maybe a)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
forall a. Maybe a
Nothing          -- Ditto here for CVC4
  sexprToVal (EApp [EApp [ECon "as", ECon "just_SBVMaybe",    _], a :: SExpr
a]) = a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> Maybe a -> Maybe (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a
  sexprToVal _                                                        = Maybe (Maybe a)
forall a. Maybe a
Nothing

instance SMTValue () where
   sexprToVal :: SExpr -> Maybe ()
sexprToVal (ECon "mkSBVTuple0") = () -> Maybe ()
forall a. a -> Maybe a
Just ()
   sexprToVal _                    = Maybe ()
forall a. Maybe a
Nothing

instance (Ord a, SymVal a) => SMTValue (RCSet a) where
   sexprToVal :: SExpr -> Maybe (RCSet a)
sexprToVal e :: SExpr
e = Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
k SExpr
e Maybe CV -> (CV -> Maybe (RCSet a)) -> Maybe (RCSet a)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= CVal -> Maybe (RCSet a)
forall a. (Ord a, SymVal a) => CVal -> Maybe (RCSet a)
cvt (CVal -> Maybe (RCSet a)) -> (CV -> CVal) -> CV -> Maybe (RCSet a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> CVal
cvVal
     where ke :: Kind
ke = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)
           k :: Kind
k  = Kind -> Kind
KSet Kind
ke

           cvt :: CVal -> Maybe (RCSet a)
cvt (CSet (RegularSet s :: Set CVal
s))    = RCSet a -> Maybe (RCSet a)
forall a. a -> Maybe a
Just (RCSet a -> Maybe (RCSet a)) -> RCSet a -> Maybe (RCSet a)
forall a b. (a -> b) -> a -> b
$ Set a -> RCSet a
forall a. Set a -> RCSet a
RegularSet    (Set a -> RCSet a) -> Set a -> RCSet a
forall a b. (a -> b) -> a -> b
$ (CVal -> a) -> Set CVal -> Set a
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (CV -> a
forall a. SymVal a => CV -> a
fromCV (CV -> a) -> (CVal -> CV) -> CVal -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
ke) Set CVal
s
           cvt (CSet (ComplementSet s :: Set CVal
s)) = RCSet a -> Maybe (RCSet a)
forall a. a -> Maybe a
Just (RCSet a -> Maybe (RCSet a)) -> RCSet a -> Maybe (RCSet a)
forall a b. (a -> b) -> a -> b
$ Set a -> RCSet a
forall a. Set a -> RCSet a
ComplementSet (Set a -> RCSet a) -> Set a -> RCSet a
forall a b. (a -> b) -> a -> b
$ (CVal -> a) -> Set CVal -> Set a
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (CV -> a
forall a. SymVal a => CV -> a
fromCV (CV -> a) -> (CVal -> CV) -> CVal -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> CVal -> CV
CV Kind
ke) Set CVal
s
           cvt _                        = Maybe (RCSet a)
forall a. Maybe a
Nothing

-- | Convert a sexpr of n-tuple to constituent sexprs. Z3 and CVC4 differ here on how they
-- present tuples, so we accommodate both:
sexprToTuple :: Int -> SExpr -> [SExpr]
sexprToTuple :: Key -> SExpr -> [SExpr]
sexprToTuple n :: Key
n e :: SExpr
e = SExpr -> [SExpr]
try SExpr
e
  where -- Z3 way
        try :: SExpr -> [SExpr]
try (EApp (ECon f :: String
f : args :: [SExpr]
args)) = case Key -> String -> (String, String)
forall a. Key -> [a] -> ([a], [a])
splitAt (String -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length "mkSBVTuple") String
f of
                                       ("mkSBVTuple", c :: String
c) | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit String
c Bool -> Bool -> Bool
&& String -> Key
forall a. Read a => String -> a
read String
c Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
n Bool -> Bool -> Bool
&& [SExpr] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [SExpr]
args Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
n -> [SExpr]
args
                                       _  -> [SExpr]
forall a. a
bad
        -- CVC4 way
        try  (EApp (EApp [ECon "as", ECon f :: String
f, _] : args :: [SExpr]
args)) = SExpr -> [SExpr]
try ([SExpr] -> SExpr
EApp (String -> SExpr
ECon String
f SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: [SExpr]
args))
        try  _ = [SExpr]
forall a. a
bad
        bad :: a
bad = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ "Data.SBV.sexprToTuple: Impossible: Expected a constructor for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ " tuple, but got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
e

-- 2-tuple
instance (SMTValue a, SMTValue b) => SMTValue (a, b) where
   sexprToVal :: SExpr -> Maybe (a, b)
sexprToVal s :: SExpr
s = case Key -> SExpr -> [SExpr]
sexprToTuple 2 SExpr
s of
                    [a :: SExpr
a, b :: SExpr
b] -> (,) (a -> b -> (a, b)) -> Maybe a -> Maybe (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a Maybe (b -> (a, b)) -> Maybe b -> Maybe (a, b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
b
                    _      -> Maybe (a, b)
forall a. Maybe a
Nothing

-- 3-tuple
instance (SMTValue a, SMTValue b, SMTValue c) => SMTValue (a, b, c) where
   sexprToVal :: SExpr -> Maybe (a, b, c)
sexprToVal s :: SExpr
s = case Key -> SExpr -> [SExpr]
sexprToTuple 3 SExpr
s of
                    [a :: SExpr
a, b :: SExpr
b, c :: SExpr
c] -> (,,) (a -> b -> c -> (a, b, c))
-> Maybe a -> Maybe (b -> c -> (a, b, c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a Maybe (b -> c -> (a, b, c)) -> Maybe b -> Maybe (c -> (a, b, c))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
b Maybe (c -> (a, b, c)) -> Maybe c -> Maybe (a, b, c)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe c
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
c
                    _         -> Maybe (a, b, c)
forall a. Maybe a
Nothing

-- 4-tuple
instance (SMTValue a, SMTValue b, SMTValue c, SMTValue d) => SMTValue (a, b, c, d) where
   sexprToVal :: SExpr -> Maybe (a, b, c, d)
sexprToVal s :: SExpr
s = case Key -> SExpr -> [SExpr]
sexprToTuple 4 SExpr
s of
                    [a :: SExpr
a, b :: SExpr
b, c :: SExpr
c, d :: SExpr
d] -> (,,,) (a -> b -> c -> d -> (a, b, c, d))
-> Maybe a -> Maybe (b -> c -> d -> (a, b, c, d))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a Maybe (b -> c -> d -> (a, b, c, d))
-> Maybe b -> Maybe (c -> d -> (a, b, c, d))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
b Maybe (c -> d -> (a, b, c, d))
-> Maybe c -> Maybe (d -> (a, b, c, d))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe c
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
c Maybe (d -> (a, b, c, d)) -> Maybe d -> Maybe (a, b, c, d)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe d
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
d
                    _            -> Maybe (a, b, c, d)
forall a. Maybe a
Nothing

-- 5-tuple
instance (SMTValue a, SMTValue b, SMTValue c, SMTValue d, SMTValue e) => SMTValue (a, b, c, d, e) where
   sexprToVal :: SExpr -> Maybe (a, b, c, d, e)
sexprToVal s :: SExpr
s = case Key -> SExpr -> [SExpr]
sexprToTuple 5 SExpr
s of
                    [a :: SExpr
a, b :: SExpr
b, c :: SExpr
c, d :: SExpr
d, e :: SExpr
e] -> (,,,,) (a -> b -> c -> d -> e -> (a, b, c, d, e))
-> Maybe a -> Maybe (b -> c -> d -> e -> (a, b, c, d, e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a Maybe (b -> c -> d -> e -> (a, b, c, d, e))
-> Maybe b -> Maybe (c -> d -> e -> (a, b, c, d, e))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
b Maybe (c -> d -> e -> (a, b, c, d, e))
-> Maybe c -> Maybe (d -> e -> (a, b, c, d, e))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe c
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
c Maybe (d -> e -> (a, b, c, d, e))
-> Maybe d -> Maybe (e -> (a, b, c, d, e))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe d
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
d Maybe (e -> (a, b, c, d, e)) -> Maybe e -> Maybe (a, b, c, d, e)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe e
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
e
                    _               -> Maybe (a, b, c, d, e)
forall a. Maybe a
Nothing

-- 6-tuple
instance (SMTValue a, SMTValue b, SMTValue c, SMTValue d, SMTValue e, SMTValue f) => SMTValue (a, b, c, d, e, f) where
   sexprToVal :: SExpr -> Maybe (a, b, c, d, e, f)
sexprToVal s :: SExpr
s = case Key -> SExpr -> [SExpr]
sexprToTuple 6 SExpr
s of
                    [a :: SExpr
a, b :: SExpr
b, c :: SExpr
c, d :: SExpr
d, e :: SExpr
e, f :: SExpr
f] -> (,,,,,) (a -> b -> c -> d -> e -> f -> (a, b, c, d, e, f))
-> Maybe a -> Maybe (b -> c -> d -> e -> f -> (a, b, c, d, e, f))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a Maybe (b -> c -> d -> e -> f -> (a, b, c, d, e, f))
-> Maybe b -> Maybe (c -> d -> e -> f -> (a, b, c, d, e, f))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
b Maybe (c -> d -> e -> f -> (a, b, c, d, e, f))
-> Maybe c -> Maybe (d -> e -> f -> (a, b, c, d, e, f))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe c
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
c Maybe (d -> e -> f -> (a, b, c, d, e, f))
-> Maybe d -> Maybe (e -> f -> (a, b, c, d, e, f))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe d
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
d Maybe (e -> f -> (a, b, c, d, e, f))
-> Maybe e -> Maybe (f -> (a, b, c, d, e, f))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe e
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
e Maybe (f -> (a, b, c, d, e, f))
-> Maybe f -> Maybe (a, b, c, d, e, f)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe f
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
f
                    _                  -> Maybe (a, b, c, d, e, f)
forall a. Maybe a
Nothing

-- 7-tuple
instance (SMTValue a, SMTValue b, SMTValue c, SMTValue d, SMTValue e, SMTValue f, SMTValue g) => SMTValue (a, b, c, d, e, f, g) where
   sexprToVal :: SExpr -> Maybe (a, b, c, d, e, f, g)
sexprToVal s :: SExpr
s = case Key -> SExpr -> [SExpr]
sexprToTuple 7 SExpr
s of
                    [a :: SExpr
a, b :: SExpr
b, c :: SExpr
c, d :: SExpr
d, e :: SExpr
e, f :: SExpr
f, g :: SExpr
g] -> (,,,,,,) (a -> b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> Maybe a
-> Maybe (b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a Maybe (b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> Maybe b
-> Maybe (c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
b Maybe (c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> Maybe c -> Maybe (d -> e -> f -> g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe c
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
c Maybe (d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> Maybe d -> Maybe (e -> f -> g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe d
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
d Maybe (e -> f -> g -> (a, b, c, d, e, f, g))
-> Maybe e -> Maybe (f -> g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe e
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
e Maybe (f -> g -> (a, b, c, d, e, f, g))
-> Maybe f -> Maybe (g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe f
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
f Maybe (g -> (a, b, c, d, e, f, g))
-> Maybe g -> Maybe (a, b, c, d, e, f, g)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe g
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
g
                    _                     -> Maybe (a, b, c, d, e, f, g)
forall a. Maybe a
Nothing

-- 8-tuple
instance (SMTValue a, SMTValue b, SMTValue c, SMTValue d, SMTValue e, SMTValue f, SMTValue g, SMTValue h) => SMTValue (a, b, c, d, e, f, g, h) where
   sexprToVal :: SExpr -> Maybe (a, b, c, d, e, f, g, h)
sexprToVal s :: SExpr
s = case Key -> SExpr -> [SExpr]
sexprToTuple 8 SExpr
s of
                    [a :: SExpr
a, b :: SExpr
b, c :: SExpr
c, d :: SExpr
d, e :: SExpr
e, f :: SExpr
f, g :: SExpr
g, h :: SExpr
h] -> (,,,,,,,) (a -> b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe a
-> Maybe
     (b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a Maybe (b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe b
-> Maybe (c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
b Maybe (c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe c
-> Maybe (d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe c
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
c Maybe (d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe d -> Maybe (e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe d
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
d Maybe (e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe e -> Maybe (f -> g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe e
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
e Maybe (f -> g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe f -> Maybe (g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe f
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
f Maybe (g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe g -> Maybe (h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe g
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
g Maybe (h -> (a, b, c, d, e, f, g, h))
-> Maybe h -> Maybe (a, b, c, d, e, f, g, h)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe h
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
h
                    _                        -> Maybe (a, b, c, d, e, f, g, h)
forall a. Maybe a
Nothing

-- | Generalization of 'Data.SBV.Control.getValue'
getValue :: (MonadIO m, MonadQuery m, SMTValue a) => SBV a -> m a
getValue :: SBV a -> m a
getValue s :: SBV a
s = 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
s)
                let nm :: String
nm  = SV -> String
forall a. Show a => a -> String
show SV
sv
                    cmd :: String
cmd = "(get-value (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))"
                    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 "getValue" String
cmd "a model 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

                let extract :: SExpr -> m a
extract v :: SExpr
v = case SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
v of
                                  Nothing -> String -> Maybe [String] -> m a
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
                                  Just c :: a
c  -> a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
c

                -- Along with regular extractions, also handle the oddball case of true/false request. These
                -- can come from queries, so we have to handle it specifically here.
                String
-> (String -> Maybe [String] -> m a) -> (SExpr -> m a) -> m a
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m a
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m a) -> m a) -> (SExpr -> m a) -> m a
forall a b. (a -> b) -> a -> b
$ \case EApp [EApp [ECon o :: String
o,  v :: SExpr
v]]                   | String
o String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== SV -> String
forall a. Show a => a -> String
show SV
sv                                             -> SExpr -> m a
forall a. SMTValue a => SExpr -> m a
extract SExpr
v
                                    EApp [EApp [ENum (i :: Integer
i, _), v :: SExpr
v@(ENum (j :: Integer
j, _))]] | SV
sv SV -> [SV] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SV
falseSV, SV
trueSV] Bool -> Bool -> Bool
&& Integer
i Integer -> [Integer] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [0, 1] Bool -> Bool -> Bool
&& Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j -> SExpr -> m a
forall a. SMTValue a => SExpr -> m a
extract SExpr
v
                                    _                                                                                                     -> String -> Maybe [String] -> m a
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing

-- | A class which allows for sexpr-conversion to functions
class (HasKind r, SatModel r, SMTValue r) => SMTFunction fun a r | fun -> a r where
  sexprToArg     :: fun -> [SExpr] -> Maybe a
  smtFunName     :: (MonadIO m, SolverContext m, MonadSymbolic m) => fun -> m String
  smtFunSaturate :: fun -> SBV r
  smtFunType     :: fun -> SBVType
  smtFunDefault  :: fun -> Maybe r
  sexprToFun     :: (MonadIO m, SolverContext m, MonadQuery m, MonadSymbolic m) => fun -> SExpr -> m (Maybe ([(a, r)], r))

  {-# MINIMAL sexprToArg, smtFunSaturate, smtFunType  #-}

  -- Given the function, figure out a default "return value"
  smtFunDefault _
    | Just v :: CV
v <- Kind -> Maybe CV
defaultKindedValue (Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)), Just (res :: r
res, []) <- [CV] -> Maybe (r, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV
v]
    = r -> Maybe r
forall a. a -> Maybe a
Just r
res
    | Bool
True
    = Maybe r
forall a. Maybe a
Nothing

  -- Given the function, determine what its name is and do some sanity checks
  smtFunName f :: fun
f = do st :: State
st@State{IORef (Map String SBVType)
rUIMap :: State -> IORef (Map String SBVType)
rUIMap :: IORef (Map String SBVType)
rUIMap} <- m State
forall (m :: * -> *). SolverContext m => m State
contextState
                    Map String SBVType
uiMap <- IO (Map String SBVType) -> m (Map String SBVType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Map String SBVType) -> m (Map String SBVType))
-> IO (Map String SBVType) -> m (Map String SBVType)
forall a b. (a -> b) -> a -> b
$ IORef (Map String SBVType) -> IO (Map String SBVType)
forall a. IORef a -> IO a
readIORef IORef (Map String SBVType)
rUIMap
                    State -> Map String SBVType -> m String
forall (m :: * -> *) b.
MonadIO m =>
State -> Map String b -> m String
findName State
st Map String SBVType
uiMap
    where findName :: State -> Map String b -> m String
findName st :: State
st@State{IORef SBVPgm
spgm :: IORef SBVPgm
spgm :: State -> IORef SBVPgm
spgm} uiMap :: Map String b
uiMap = do
             SV
r <- IO SV -> m SV
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SV -> m SV) -> IO SV -> m SV
forall a b. (a -> b) -> a -> b
$ State -> SBV r -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st (fun -> SBV r
forall fun a r. SMTFunction fun a r => fun -> SBV r
smtFunSaturate fun
f)
             IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ SV -> IO ()
forceSVArg SV
r
             SBVPgm asgns :: Seq (SV, SBVExpr)
asgns <- IO SBVPgm -> m SBVPgm
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SBVPgm -> m SBVPgm) -> IO SBVPgm -> m SBVPgm
forall a b. (a -> b) -> a -> b
$ IORef SBVPgm -> IO SBVPgm
forall a. IORef a -> IO a
readIORef IORef SBVPgm
spgm

             let cantFind :: a
cantFind = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$    [ ""
                                                 , "*** Data.SBV.getFunction: Must be called on an uninterpreted function!"
                                                 , "***"
                                                 , "***    Expected to receive a function created by \"uninterpret\""
                                                 ]
                                              [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
tag
                                              [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ "***"
                                                 , "*** Make sure to call getFunction on uninterpreted functions only!"
                                                 , "*** If that is already the case, please report this as a bug."
                                                 ]
                      where tag :: [String]
tag = case ((String, b) -> String) -> [(String, b)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, b) -> String
forall a b. (a, b) -> a
fst (Map String b -> [(String, b)]
forall k a. Map k a -> [(k, a)]
Map.toList Map String b
uiMap) of
                                    []    -> [ "***    But, there are no matching uninterpreted functions in the context." ]
                                    [x :: String
x]   -> [ "***    The only possible candidate is: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x ]
                                    cands :: [String]
cands -> [ "***    Candidates are:"
                                             , "***        " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " [String]
cands
                                             ]

             case ((SV, SBVExpr) -> Bool) -> Seq (SV, SBVExpr) -> Maybe Key
forall a. (a -> Bool) -> Seq a -> Maybe Key
S.findIndexR ((SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
r) (SV -> Bool) -> ((SV, SBVExpr) -> SV) -> (SV, SBVExpr) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SV, SBVExpr) -> SV
forall a b. (a, b) -> a
fst) Seq (SV, SBVExpr)
asgns of
               Nothing -> m String
forall a. a
cantFind
               Just i :: Key
i  -> case Seq (SV, SBVExpr)
asgns Seq (SV, SBVExpr) -> Key -> (SV, SBVExpr)
forall a. Seq a -> Key -> a
`S.index` Key
i of
                            (sv :: SV
sv, SBVApp (Uninterpreted nm :: String
nm) _) | SV
r SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
sv -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return String
nm
                            _                                           -> m String
forall a. a
cantFind

  sexprToFun f :: fun
f e :: SExpr
e = do String
nm <- fun -> m String
forall fun a r (m :: * -> *).
(SMTFunction fun a r, MonadIO m, SolverContext m,
 MonadSymbolic m) =>
fun -> m String
smtFunName fun
f
                      case SExpr -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
parseSExprFunction SExpr
e of
                        Just (Left nm' :: String
nm') -> case (String
nm String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
nm', fun -> Maybe r
forall fun a r. SMTFunction fun a r => fun -> Maybe r
smtFunDefault fun
f) of
                                             (True, Just v :: r
v)  -> Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r)))
-> Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r))
forall a b. (a -> b) -> a -> b
$ ([(a, r)], r) -> Maybe ([(a, r)], r)
forall a. a -> Maybe a
Just ([], r
v)
                                             _               -> String -> m (Maybe ([(a, r)], r))
forall a a. Show a => a -> a
bailOut String
nm
                        Just (Right v :: ([([SExpr], SExpr)], SExpr)
v)  -> Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r)))
-> Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r))
forall a b. (a -> b) -> a -> b
$ ([([SExpr], SExpr)], SExpr) -> Maybe ([(a, r)], r)
forall (t :: * -> *) a r a a.
(Traversable t, SMTFunction fun a r, SMTValue a, SMTValue a) =>
(t ([SExpr], SExpr), SExpr) -> Maybe (t (a, a), a)
convert ([([SExpr], SExpr)], SExpr)
v
                        Nothing         -> do Maybe ([([SExpr], SExpr)], SExpr)
mbPVS <- String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
pointWiseExtract String
nm (fun -> SBVType
forall fun a r. SMTFunction fun a r => fun -> SBVType
smtFunType fun
f)
                                              Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r)))
-> Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r))
forall a b. (a -> b) -> a -> b
$ Maybe ([([SExpr], SExpr)], SExpr)
mbPVS Maybe ([([SExpr], SExpr)], SExpr)
-> (([([SExpr], SExpr)], SExpr) -> Maybe ([(a, r)], r))
-> Maybe ([(a, r)], r)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([([SExpr], SExpr)], SExpr) -> Maybe ([(a, r)], r)
forall (t :: * -> *) a r a a.
(Traversable t, SMTFunction fun a r, SMTValue a, SMTValue a) =>
(t ([SExpr], SExpr), SExpr) -> Maybe (t (a, a), a)
convert
    where convert :: (t ([SExpr], SExpr), SExpr) -> Maybe (t (a, a), a)
convert    (vs :: t ([SExpr], SExpr)
vs, d :: SExpr
d) = (,) (t (a, a) -> a -> (t (a, a), a))
-> Maybe (t (a, a)) -> Maybe (a -> (t (a, a), a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (([SExpr], SExpr) -> Maybe (a, a))
-> t ([SExpr], SExpr) -> Maybe (t (a, a))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([SExpr], SExpr) -> Maybe (a, a)
forall a r a.
(SMTFunction fun a r, SMTValue a) =>
([SExpr], SExpr) -> Maybe (a, a)
sexprPoint t ([SExpr], SExpr)
vs Maybe (a -> (t (a, a), a)) -> Maybe a -> Maybe (t (a, a), a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
d
          sexprPoint :: ([SExpr], SExpr) -> Maybe (a, a)
sexprPoint (as :: [SExpr]
as, v :: SExpr
v) = (,) (a -> a -> (a, a)) -> Maybe a -> Maybe (a -> (a, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> fun -> [SExpr] -> Maybe a
forall fun a r. SMTFunction fun a r => fun -> [SExpr] -> Maybe a
sexprToArg fun
f [SExpr]
as    Maybe (a -> (a, a)) -> Maybe a -> Maybe (a, a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
v

          bailOut :: a -> a
bailOut nm :: a
nm = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ ""
                                       , "*** Data.SBV.getFunction: Unable to extract an interpretation for function " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
nm
                                       , "***"
                                       , "*** Failed while trying to extract a pointwise interpretation."
                                       , "***"
                                       , "*** This could be a bug with SBV or the backend solver. Please report!"
                                       ]

-- | Registering an uninterpreted SMT function. This is typically not necessary as uses of the UI
-- function itself will register it automatically. But there are cases where doing this explicitly can
-- come in handy.
registerUISMTFunction :: (MonadIO m, SolverContext m, MonadSymbolic m) => SMTFunction fun a r => fun -> m ()
registerUISMTFunction :: fun -> m ()
registerUISMTFunction f :: fun
f = do State
st <- m State
forall (m :: * -> *). SolverContext m => m State
contextState
                             String
nm <- fun -> m String
forall fun a r (m :: * -> *).
(SMTFunction fun a r, MonadIO m, SolverContext m,
 MonadSymbolic m) =>
fun -> m String
smtFunName fun
f
                             IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ State -> String -> SBVType -> Maybe [String] -> IO ()
newUninterpreted State
st String
nm (fun -> SBVType
forall fun a r. SMTFunction fun a r => fun -> SBVType
smtFunType fun
f) Maybe [String]
forall a. Maybe a
Nothing

-- | Pointwise function value extraction. If we get unlucky and can't parse z3's output (happens
-- when we have all booleans and z3 decides to spit out an expression), just brute force our
-- way out of it. Note that we only do this if we have a pure boolean type, as otherwise we'd blow
-- up. And I think it'll only be necessary then, I haven't seen z3 try anything smarter in other scenarios.
pointWiseExtract ::  forall m. (MonadIO m, MonadQuery m) => String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
pointWiseExtract :: String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
pointWiseExtract nm :: String
nm typ :: SBVType
typ
   | Bool
isBoolFunc
   = m (Maybe ([([SExpr], SExpr)], SExpr))
tryPointWise
   | Bool
True
   = String -> m (Maybe ([([SExpr], SExpr)], SExpr))
forall a. HasCallStack => String -> a
error (String -> m (Maybe ([([SExpr], SExpr)], SExpr)))
-> String -> m (Maybe ([([SExpr], SExpr)], SExpr))
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ ""
                     , "*** Data.SBV.getFunction: Unsupported: Extracting interpretation for function:"
                     , "***"
                     , "***     " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVType -> String
forall a. Show a => a -> String
show SBVType
typ
                     , "***"
                     , "*** At this time, the expression returned by the solver is too complicated for SBV!"
                     , "***"
                     , "*** You can ignore uninterpreted function models for sat models using the 'satTrackUFs' parameter:"
                     , "***"
                     , "***             satWith    z3{satTrackUFs = False}"
                     , "***             allSatWith z3{satTrackUFs = False}"
                     , "***"
                     , "*** You can see the response from the solver by running with '{verbose = True}' option."
                     , "***"
                     , "*** NB. If this is a use case you'd like SBV to support, please get in touch!"
                     ]
  where trueSExpr :: SExpr
trueSExpr  = (Integer, Maybe Key) -> SExpr
ENum (1, Maybe Key
forall a. Maybe a
Nothing)
        falseSExpr :: SExpr
falseSExpr = (Integer, Maybe Key) -> SExpr
ENum (0, Maybe Key
forall a. Maybe a
Nothing)

        isTrueSExpr :: SExpr -> Bool
isTrueSExpr (ENum (1, Nothing)) = Bool
True
        isTrueSExpr (ENum (0, Nothing)) = Bool
False
        isTrueSExpr s :: SExpr
s                   = String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ "Data.SBV.pointWiseExtract: Impossible happened: Received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
s

        (nArgs :: Key
nArgs, isBoolFunc :: Bool
isBoolFunc) = case SBVType
typ of
                                SBVType ts :: [Kind]
ts -> ([Kind] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [Kind]
ts Key -> Key -> Key
forall a. Num a => a -> a -> a
- 1, (Kind -> Bool) -> [Kind] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KBool) [Kind]
ts)

        getBVal :: [SExpr] -> m ([SExpr], SExpr)
        getBVal :: [SExpr] -> m ([SExpr], SExpr)
getBVal args :: [SExpr]
args = do let shc :: SExpr -> String
shc c :: SExpr
c | SExpr -> Bool
isTrueSExpr SExpr
c = "true"
                                    | Bool
True          = "false"

                              as :: String
as = [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (SExpr -> String) -> [SExpr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SExpr -> String
shc [SExpr]
args

                              cmd :: String
cmd   = "(get-value ((" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
as String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")))"

                              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 "get-value" String
cmd ("pointwise value of boolean function " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " on " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
as) 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 ([SExpr], SExpr))
-> (SExpr -> m ([SExpr], SExpr))
-> m ([SExpr], SExpr)
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m ([SExpr], SExpr)
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m ([SExpr], SExpr)) -> m ([SExpr], SExpr))
-> (SExpr -> m ([SExpr], SExpr)) -> m ([SExpr], SExpr)
forall a b. (a -> b) -> a -> b
$ \case EApp [EApp [_, e :: SExpr
e]] -> ([SExpr], SExpr) -> m ([SExpr], SExpr)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SExpr]
args, SExpr
e)
                                              _                  -> String -> Maybe [String] -> m ([SExpr], SExpr)
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing

        getBVals :: m [([SExpr], SExpr)]
        getBVals :: m [([SExpr], SExpr)]
getBVals = ([SExpr] -> m ([SExpr], SExpr))
-> [[SExpr]] -> m [([SExpr], SExpr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM [SExpr] -> m ([SExpr], SExpr)
getBVal ([[SExpr]] -> m [([SExpr], SExpr)])
-> [[SExpr]] -> m [([SExpr], SExpr)]
forall a b. (a -> b) -> a -> b
$ Key -> [SExpr] -> [[SExpr]]
forall (m :: * -> *) a. Applicative m => Key -> m a -> m [a]
replicateM Key
nArgs [SExpr
falseSExpr, SExpr
trueSExpr]

        tryPointWise :: m (Maybe ([([SExpr], SExpr)], SExpr))
tryPointWise
          | Bool -> Bool
not Bool
isBoolFunc
          = Maybe ([([SExpr], SExpr)], SExpr)
-> m (Maybe ([([SExpr], SExpr)], SExpr))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([([SExpr], SExpr)], SExpr)
forall a. Maybe a
Nothing
          | Key
nArgs Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
< 1
          = String -> m (Maybe ([([SExpr], SExpr)], SExpr))
forall a. HasCallStack => String -> a
error (String -> m (Maybe ([([SExpr], SExpr)], SExpr)))
-> String -> m (Maybe ([([SExpr], SExpr)], SExpr))
forall a b. (a -> b) -> a -> b
$ "Data.SBV.pointWiseExtract: Impossible happened, nArgs < 1: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
nArgs String -> String -> String
forall a. [a] -> [a] -> [a]
++ " type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVType -> String
forall a. Show a => a -> String
show SBVType
typ
          | Bool
True
          = do [([SExpr], SExpr)]
vs <- m [([SExpr], SExpr)]
getBVals
               -- Pick the value that will give us the fewer entries
               let (trues :: [([SExpr], SExpr)]
trues, falses :: [([SExpr], SExpr)]
falses) = (([SExpr], SExpr) -> Bool)
-> [([SExpr], SExpr)] -> ([([SExpr], SExpr)], [([SExpr], SExpr)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(_, v :: SExpr
v) -> SExpr -> Bool
isTrueSExpr SExpr
v) [([SExpr], SExpr)]
vs
               Maybe ([([SExpr], SExpr)], SExpr)
-> m (Maybe ([([SExpr], SExpr)], SExpr))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([([SExpr], SExpr)], SExpr)
 -> m (Maybe ([([SExpr], SExpr)], SExpr)))
-> Maybe ([([SExpr], SExpr)], SExpr)
-> m (Maybe ([([SExpr], SExpr)], SExpr))
forall a b. (a -> b) -> a -> b
$ ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
forall a. a -> Maybe a
Just (([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr))
-> ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
forall a b. (a -> b) -> a -> b
$ if [([SExpr], SExpr)] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [([SExpr], SExpr)]
trues Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
<= [([SExpr], SExpr)] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [([SExpr], SExpr)]
falses
                               then ([([SExpr], SExpr)]
trues,  SExpr
falseSExpr)
                               else ([([SExpr], SExpr)]
falses, SExpr
trueSExpr)

-- | For saturation purposes, get a proper argument. The forall quantification
-- is safe here since we only use in smtFunSaturate calls, which looks at the
-- kind stored inside only.
mkArg :: forall a. Kind -> SBV a
mkArg :: Kind -> SBV a
mkArg k :: Kind
k = case Kind -> Maybe CV
defaultKindedValue Kind
k of
            Nothing -> String -> SBV a
forall a. HasCallStack => String -> a
error (String -> SBV a) -> String -> SBV a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ ""
                                       , "*** Data.SBV.smtFunSaturate: Impossible happened!"
                                       , "*** Unable to create a valid parameter for kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
                                       , "*** Please report this as an SBV bug!"
                                       ]
            Just c :: CV
c -> SVal -> SBV a
forall a. SVal -> SBV a
SBV (SVal -> SBV a) -> SVal -> SBV a
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left CV
c)

-- | Functions of arity 1
instance ( SymVal a, HasKind a, SMTValue a
         , SatModel r, HasKind r, SMTValue r
         ) => SMTFunction (SBV a -> SBV r) a r
         where
  sexprToArg :: (SBV a -> SBV r) -> [SExpr] -> Maybe a
sexprToArg _ [a0 :: SExpr
a0] = SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a0
  sexprToArg _ _    = Maybe a
forall a. Maybe a
Nothing

  smtFunType :: (SBV a -> SBV r) -> SBVType
smtFunType _ = [Kind] -> SBVType
SBVType [Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a), Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)]

  smtFunSaturate :: (SBV a -> SBV r) -> SBV r
smtFunSaturate f :: SBV a -> SBV r
f = SBV a -> SBV r
f (SBV a -> SBV r) -> SBV a -> SBV r
forall a b. (a -> b) -> a -> b
$ Kind -> SBV a
forall a. Kind -> SBV a
mkArg (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a))

-- | Functions of arity 2
instance ( SymVal a,  HasKind a, SMTValue a
         , SymVal b,  HasKind b, SMTValue b
         , SatModel r, HasKind r, SMTValue r
         ) => SMTFunction (SBV a -> SBV b -> SBV r) (a, b) r
         where
  sexprToArg :: (SBV a -> SBV b -> SBV r) -> [SExpr] -> Maybe (a, b)
sexprToArg _ [a0 :: SExpr
a0, a1 :: SExpr
a1] = (,) (a -> b -> (a, b)) -> Maybe a -> Maybe (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a0 Maybe (b -> (a, b)) -> Maybe b -> Maybe (a, b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a1
  sexprToArg _ _        = Maybe (a, b)
forall a. Maybe a
Nothing

  smtFunType :: (SBV a -> SBV b -> SBV r) -> SBVType
smtFunType _ = [Kind] -> SBVType
SBVType [Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b), Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)]

  smtFunSaturate :: (SBV a -> SBV b -> SBV r) -> SBV r
smtFunSaturate f :: SBV a -> SBV b -> SBV r
f = SBV a -> SBV b -> SBV r
f (Kind -> SBV a
forall a. Kind -> SBV a
mkArg (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)))
                       (Kind -> SBV b
forall a. Kind -> SBV a
mkArg (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)))

-- | Functions of arity 3
instance ( SymVal a,   HasKind a, SMTValue a
         , SymVal b,   HasKind b, SMTValue b
         , SymVal c,   HasKind c, SMTValue c
         , SatModel r, HasKind r, SMTValue r
         ) => SMTFunction (SBV a -> SBV b -> SBV c -> SBV r) (a, b, c) r
         where
  sexprToArg :: (SBV a -> SBV b -> SBV c -> SBV r) -> [SExpr] -> Maybe (a, b, c)
sexprToArg _ [a0 :: SExpr
a0, a1 :: SExpr
a1, a2 :: SExpr
a2] = (,,) (a -> b -> c -> (a, b, c))
-> Maybe a -> Maybe (b -> c -> (a, b, c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a0 Maybe (b -> c -> (a, b, c)) -> Maybe b -> Maybe (c -> (a, b, c))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a1 Maybe (c -> (a, b, c)) -> Maybe c -> Maybe (a, b, c)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe c
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a2
  sexprToArg _ _            = Maybe (a, b, c)
forall a. Maybe a
Nothing

  smtFunType :: (SBV a -> SBV b -> SBV c -> SBV r) -> SBVType
smtFunType _ = [Kind] -> SBVType
SBVType [Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b), Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c), Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)]

  smtFunSaturate :: (SBV a -> SBV b -> SBV c -> SBV r) -> SBV r
smtFunSaturate f :: SBV a -> SBV b -> SBV c -> SBV r
f = SBV a -> SBV b -> SBV c -> SBV r
f (Kind -> SBV a
forall a. Kind -> SBV a
mkArg (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)))
                       (Kind -> SBV b
forall a. Kind -> SBV a
mkArg (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)))
                       (Kind -> SBV c
forall a. Kind -> SBV a
mkArg (Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c)))

-- | Functions of arity 4
instance ( SymVal a,   HasKind a, SMTValue a
         , SymVal b,   HasKind b, SMTValue b
         , SymVal c,   HasKind c, SMTValue c
         , SymVal d,   HasKind d, SMTValue d
         , SatModel r, HasKind r, SMTValue r
         ) => SMTFunction (SBV a -> SBV b -> SBV c -> SBV d -> SBV r) (a, b, c, d) r
         where
  sexprToArg :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV r)
-> [SExpr] -> Maybe (a, b, c, d)
sexprToArg _ [a0 :: SExpr
a0, a1 :: SExpr
a1, a2 :: SExpr
a2, a3 :: SExpr
a3] = (,,,) (a -> b -> c -> d -> (a, b, c, d))
-> Maybe a -> Maybe (b -> c -> d -> (a, b, c, d))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a0 Maybe (b -> c -> d -> (a, b, c, d))
-> Maybe b -> Maybe (c -> d -> (a, b, c, d))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a1 Maybe (c -> d -> (a, b, c, d))
-> Maybe c -> Maybe (d -> (a, b, c, d))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe c
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a2 Maybe (d -> (a, b, c, d)) -> Maybe d -> Maybe (a, b, c, d)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe d
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a3
  sexprToArg _ _               = Maybe (a, b, c, d)
forall a. Maybe a
Nothing

  smtFunType :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV r) -> SBVType
smtFunType _ = [Kind] -> SBVType
SBVType [Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b), Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c), Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d), Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)]

  smtFunSaturate :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV r) -> SBV r
smtFunSaturate f :: SBV a -> SBV b -> SBV c -> SBV d -> SBV r
f = SBV a -> SBV b -> SBV c -> SBV d -> SBV r
f (Kind -> SBV a
forall a. Kind -> SBV a
mkArg (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)))
                       (Kind -> SBV b
forall a. Kind -> SBV a
mkArg (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)))
                       (Kind -> SBV c
forall a. Kind -> SBV a
mkArg (Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c)))
                       (Kind -> SBV d
forall a. Kind -> SBV a
mkArg (Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d)))

-- | Functions of arity 5
instance ( SymVal a,   HasKind a, SMTValue a
         , SymVal b,   HasKind b, SMTValue b
         , SymVal c,   HasKind c, SMTValue c
         , SymVal d,   HasKind d, SMTValue d
         , SymVal e,   HasKind e, SMTValue e
         , SatModel r, HasKind r, SMTValue r
         ) => SMTFunction (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r) (a, b, c, d, e) r
         where
  sexprToArg :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r)
-> [SExpr] -> Maybe (a, b, c, d, e)
sexprToArg _ [a0 :: SExpr
a0, a1 :: SExpr
a1, a2 :: SExpr
a2, a3 :: SExpr
a3, a4 :: SExpr
a4] = (,,,,) (a -> b -> c -> d -> e -> (a, b, c, d, e))
-> Maybe a -> Maybe (b -> c -> d -> e -> (a, b, c, d, e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a0 Maybe (b -> c -> d -> e -> (a, b, c, d, e))
-> Maybe b -> Maybe (c -> d -> e -> (a, b, c, d, e))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a1 Maybe (c -> d -> e -> (a, b, c, d, e))
-> Maybe c -> Maybe (d -> e -> (a, b, c, d, e))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe c
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a2 Maybe (d -> e -> (a, b, c, d, e))
-> Maybe d -> Maybe (e -> (a, b, c, d, e))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe d
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a3 Maybe (e -> (a, b, c, d, e)) -> Maybe e -> Maybe (a, b, c, d, e)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe e
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a4
  sexprToArg _ _                    = Maybe (a, b, c, d, e)
forall a. Maybe a
Nothing

  smtFunType :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r) -> SBVType
smtFunType _ = [Kind] -> SBVType
SBVType [Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b), Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c), Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d), Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy e
forall k (t :: k). Proxy t
Proxy @e), Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)]

  smtFunSaturate :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r) -> SBV r
smtFunSaturate f :: SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r
f = SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r
f (Kind -> SBV a
forall a. Kind -> SBV a
mkArg (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)))
                       (Kind -> SBV b
forall a. Kind -> SBV a
mkArg (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)))
                       (Kind -> SBV c
forall a. Kind -> SBV a
mkArg (Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c)))
                       (Kind -> SBV d
forall a. Kind -> SBV a
mkArg (Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d)))
                       (Kind -> SBV e
forall a. Kind -> SBV a
mkArg (Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy e
forall k (t :: k). Proxy t
Proxy @e)))

-- | Functions of arity 6
instance ( SymVal a,   HasKind a, SMTValue a
         , SymVal b,   HasKind b, SMTValue b
         , SymVal c,   HasKind c, SMTValue c
         , SymVal d,   HasKind d, SMTValue d
         , SymVal e,   HasKind e, SMTValue e
         , SymVal f,   HasKind f, SMTValue f
         , SatModel r, HasKind r, SMTValue r
         ) => SMTFunction (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r) (a, b, c, d, e, f) r
         where
  sexprToArg :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r)
-> [SExpr] -> Maybe (a, b, c, d, e, f)
sexprToArg _ [a0 :: SExpr
a0, a1 :: SExpr
a1, a2 :: SExpr
a2, a3 :: SExpr
a3, a4 :: SExpr
a4, a5 :: SExpr
a5] = (,,,,,) (a -> b -> c -> d -> e -> f -> (a, b, c, d, e, f))
-> Maybe a -> Maybe (b -> c -> d -> e -> f -> (a, b, c, d, e, f))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a0 Maybe (b -> c -> d -> e -> f -> (a, b, c, d, e, f))
-> Maybe b -> Maybe (c -> d -> e -> f -> (a, b, c, d, e, f))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a1 Maybe (c -> d -> e -> f -> (a, b, c, d, e, f))
-> Maybe c -> Maybe (d -> e -> f -> (a, b, c, d, e, f))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe c
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a2 Maybe (d -> e -> f -> (a, b, c, d, e, f))
-> Maybe d -> Maybe (e -> f -> (a, b, c, d, e, f))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe d
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a3 Maybe (e -> f -> (a, b, c, d, e, f))
-> Maybe e -> Maybe (f -> (a, b, c, d, e, f))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe e
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a4 Maybe (f -> (a, b, c, d, e, f))
-> Maybe f -> Maybe (a, b, c, d, e, f)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe f
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a5
  sexprToArg _ _                        = Maybe (a, b, c, d, e, f)
forall a. Maybe a
Nothing

  smtFunType :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r)
-> SBVType
smtFunType _ = [Kind] -> SBVType
SBVType [Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b), Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c), Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d), Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy e
forall k (t :: k). Proxy t
Proxy @e), Proxy f -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy f
forall k (t :: k). Proxy t
Proxy @f), Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)]

  smtFunSaturate :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r)
-> SBV r
smtFunSaturate f :: SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r
f = SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r
f (Kind -> SBV a
forall a. Kind -> SBV a
mkArg (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)))
                       (Kind -> SBV b
forall a. Kind -> SBV a
mkArg (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)))
                       (Kind -> SBV c
forall a. Kind -> SBV a
mkArg (Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c)))
                       (Kind -> SBV d
forall a. Kind -> SBV a
mkArg (Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d)))
                       (Kind -> SBV e
forall a. Kind -> SBV a
mkArg (Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy e
forall k (t :: k). Proxy t
Proxy @e)))
                       (Kind -> SBV f
forall a. Kind -> SBV a
mkArg (Proxy f -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy f
forall k (t :: k). Proxy t
Proxy @f)))

-- | Functions of arity 7
instance ( SymVal a,   HasKind a, SMTValue a
         , SymVal b,   HasKind b, SMTValue b
         , SymVal c,   HasKind c, SMTValue c
         , SymVal d,   HasKind d, SMTValue d
         , SymVal e,   HasKind e, SMTValue e
         , SymVal f,   HasKind f, SMTValue f
         , SymVal g,   HasKind g, SMTValue g
         , SatModel r, HasKind r, SMTValue r
         ) => SMTFunction (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r) (a, b, c, d, e, f, g) r
         where
  sexprToArg :: (SBV a
 -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r)
-> [SExpr] -> Maybe (a, b, c, d, e, f, g)
sexprToArg _ [a0 :: SExpr
a0, a1 :: SExpr
a1, a2 :: SExpr
a2, a3 :: SExpr
a3, a4 :: SExpr
a4, a5 :: SExpr
a5, a6 :: SExpr
a6] = (,,,,,,) (a -> b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> Maybe a
-> Maybe (b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a0 Maybe (b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> Maybe b
-> Maybe (c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a1 Maybe (c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> Maybe c -> Maybe (d -> e -> f -> g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe c
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a2 Maybe (d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> Maybe d -> Maybe (e -> f -> g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe d
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a3 Maybe (e -> f -> g -> (a, b, c, d, e, f, g))
-> Maybe e -> Maybe (f -> g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe e
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a4 Maybe (f -> g -> (a, b, c, d, e, f, g))
-> Maybe f -> Maybe (g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe f
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a5 Maybe (g -> (a, b, c, d, e, f, g))
-> Maybe g -> Maybe (a, b, c, d, e, f, g)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe g
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a6
  sexprToArg _ _                            = Maybe (a, b, c, d, e, f, g)
forall a. Maybe a
Nothing

  smtFunType :: (SBV a
 -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r)
-> SBVType
smtFunType _ = [Kind] -> SBVType
SBVType [Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b), Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c), Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d), Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy e
forall k (t :: k). Proxy t
Proxy @e), Proxy f -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy f
forall k (t :: k). Proxy t
Proxy @f), Proxy g -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy g
forall k (t :: k). Proxy t
Proxy @g), Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)]

  smtFunSaturate :: (SBV a
 -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r)
-> SBV r
smtFunSaturate f :: SBV a
-> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r
f = SBV a
-> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r
f (Kind -> SBV a
forall a. Kind -> SBV a
mkArg (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)))
                       (Kind -> SBV b
forall a. Kind -> SBV a
mkArg (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)))
                       (Kind -> SBV c
forall a. Kind -> SBV a
mkArg (Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c)))
                       (Kind -> SBV d
forall a. Kind -> SBV a
mkArg (Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d)))
                       (Kind -> SBV e
forall a. Kind -> SBV a
mkArg (Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy e
forall k (t :: k). Proxy t
Proxy @e)))
                       (Kind -> SBV f
forall a. Kind -> SBV a
mkArg (Proxy f -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy f
forall k (t :: k). Proxy t
Proxy @f)))
                       (Kind -> SBV g
forall a. Kind -> SBV a
mkArg (Proxy g -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy g
forall k (t :: k). Proxy t
Proxy @g)))

-- | Functions of arity 8
instance ( SymVal a,   HasKind a, SMTValue a
         , SymVal b,   HasKind b, SMTValue b
         , SymVal c,   HasKind c, SMTValue c
         , SymVal d,   HasKind d, SMTValue d
         , SymVal e,   HasKind e, SMTValue e
         , SymVal f,   HasKind f, SMTValue f
         , SymVal g,   HasKind g, SMTValue g
         , SymVal h,   HasKind h, SMTValue h
         , SatModel r, HasKind r, SMTValue r
         ) => SMTFunction (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV h -> SBV r) (a, b, c, d, e, f, g, h) r
         where
  sexprToArg :: (SBV a
 -> SBV b
 -> SBV c
 -> SBV d
 -> SBV e
 -> SBV f
 -> SBV g
 -> SBV h
 -> SBV r)
-> [SExpr] -> Maybe (a, b, c, d, e, f, g, h)
sexprToArg _ [a0 :: SExpr
a0, a1 :: SExpr
a1, a2 :: SExpr
a2, a3 :: SExpr
a3, a4 :: SExpr
a4, a5 :: SExpr
a5, a6 :: SExpr
a6, a7 :: SExpr
a7] = (,,,,,,,) (a -> b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe a
-> Maybe
     (b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a0 Maybe (b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe b
-> Maybe (c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a1 Maybe (c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe c
-> Maybe (d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe c
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a2 Maybe (d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe d -> Maybe (e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe d
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a3 Maybe (e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe e -> Maybe (f -> g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe e
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a4 Maybe (f -> g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe f -> Maybe (g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe f
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a5 Maybe (g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe g -> Maybe (h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe g
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a6 Maybe (h -> (a, b, c, d, e, f, g, h))
-> Maybe h -> Maybe (a, b, c, d, e, f, g, h)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe h
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
a7
  sexprToArg _ _                                = Maybe (a, b, c, d, e, f, g, h)
forall a. Maybe a
Nothing

  smtFunType :: (SBV a
 -> SBV b
 -> SBV c
 -> SBV d
 -> SBV e
 -> SBV f
 -> SBV g
 -> SBV h
 -> SBV r)
-> SBVType
smtFunType _ = [Kind] -> SBVType
SBVType [Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b), Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c), Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d), Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy e
forall k (t :: k). Proxy t
Proxy @e), Proxy f -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy f
forall k (t :: k). Proxy t
Proxy @f), Proxy g -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy g
forall k (t :: k). Proxy t
Proxy @g), Proxy h -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy h
forall k (t :: k). Proxy t
Proxy @h), Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)]

  smtFunSaturate :: (SBV a
 -> SBV b
 -> SBV c
 -> SBV d
 -> SBV e
 -> SBV f
 -> SBV g
 -> SBV h
 -> SBV r)
-> SBV r
smtFunSaturate f :: SBV a
-> SBV b
-> SBV c
-> SBV d
-> SBV e
-> SBV f
-> SBV g
-> SBV h
-> SBV r
f = SBV a
-> SBV b
-> SBV c
-> SBV d
-> SBV e
-> SBV f
-> SBV g
-> SBV h
-> SBV r
f (Kind -> SBV a
forall a. Kind -> SBV a
mkArg (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)))
                       (Kind -> SBV b
forall a. Kind -> SBV a
mkArg (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)))
                       (Kind -> SBV c
forall a. Kind -> SBV a
mkArg (Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c)))
                       (Kind -> SBV d
forall a. Kind -> SBV a
mkArg (Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d)))
                       (Kind -> SBV e
forall a. Kind -> SBV a
mkArg (Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy e
forall k (t :: k). Proxy t
Proxy @e)))
                       (Kind -> SBV f
forall a. Kind -> SBV a
mkArg (Proxy f -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy f
forall k (t :: k). Proxy t
Proxy @f)))
                       (Kind -> SBV g
forall a. Kind -> SBV a
mkArg (Proxy g -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy g
forall k (t :: k). Proxy t
Proxy @g)))
                       (Kind -> SBV h
forall a. Kind -> SBV a
mkArg (Proxy h -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy h
forall k (t :: k). Proxy t
Proxy @h)))

-- | Generalization of 'Data.SBV.Control.getFunction'
getFunction :: (MonadIO m, MonadQuery m, SolverContext m, MonadSymbolic m, SMTFunction fun a r) => fun -> m ([(a, r)], r)
getFunction :: fun -> m ([(a, r)], r)
getFunction f :: fun
f = do String
nm <- fun -> m String
forall fun a r (m :: * -> *).
(SMTFunction fun a r, MonadIO m, SolverContext m,
 MonadSymbolic m) =>
fun -> m String
smtFunName fun
f

                   let cmd :: String
cmd = "(get-value (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))"
                       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 "getFunction" String
cmd "a function 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 ([(a, r)], r))
-> (SExpr -> m ([(a, r)], r))
-> m ([(a, r)], r)
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m ([(a, r)], r)
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m ([(a, r)], r)) -> m ([(a, r)], r))
-> (SExpr -> m ([(a, r)], r)) -> m ([(a, r)], r)
forall a b. (a -> b) -> a -> b
$ \case EApp [EApp [ECon o :: String
o, e :: SExpr
e]] | String
o String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
nm -> do Maybe ([(a, r)], r)
mbAssocs <- fun -> SExpr -> m (Maybe ([(a, r)], r))
forall fun a r (m :: * -> *).
(SMTFunction fun a r, MonadIO m, SolverContext m, MonadQuery m,
 MonadSymbolic m) =>
fun -> SExpr -> m (Maybe ([(a, r)], r))
sexprToFun fun
f SExpr
e
                                                                               case Maybe ([(a, r)], r)
mbAssocs of
                                                                                 Just assocs :: ([(a, r)], r)
assocs -> ([(a, r)], r) -> m ([(a, r)], r)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(a, r)], r)
assocs
                                                                                 Nothing     -> do Maybe ([([SExpr], SExpr)], SExpr)
mbPVS <- String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
pointWiseExtract String
nm (fun -> SBVType
forall fun a r. SMTFunction fun a r => fun -> SBVType
smtFunType fun
f)
                                                                                                   case Maybe ([([SExpr], SExpr)], SExpr)
mbPVS Maybe ([([SExpr], SExpr)], SExpr)
-> (([([SExpr], SExpr)], SExpr) -> Maybe ([(a, r)], r))
-> Maybe ([(a, r)], r)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([([SExpr], SExpr)], SExpr) -> Maybe ([(a, r)], r)
forall (t :: * -> *) a r a a.
(Traversable t, SMTFunction fun a r, SMTValue a, SMTValue a) =>
(t ([SExpr], SExpr), SExpr) -> Maybe (t (a, a), a)
convert of
                                                                                                     Just x :: ([(a, r)], r)
x  -> ([(a, r)], r) -> m ([(a, r)], r)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(a, r)], r)
x
                                                                                                     Nothing -> String -> Maybe [String] -> m ([(a, r)], r)
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
                                       _                                 -> String -> Maybe [String] -> m ([(a, r)], r)
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
    where convert :: (t ([SExpr], SExpr), SExpr) -> Maybe (t (a, a), a)
convert    (vs :: t ([SExpr], SExpr)
vs, d :: SExpr
d) = (,) (t (a, a) -> a -> (t (a, a), a))
-> Maybe (t (a, a)) -> Maybe (a -> (t (a, a), a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (([SExpr], SExpr) -> Maybe (a, a))
-> t ([SExpr], SExpr) -> Maybe (t (a, a))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([SExpr], SExpr) -> Maybe (a, a)
forall a r a.
(SMTFunction fun a r, SMTValue a) =>
([SExpr], SExpr) -> Maybe (a, a)
sexprPoint t ([SExpr], SExpr)
vs Maybe (a -> (t (a, a), a)) -> Maybe a -> Maybe (t (a, a), a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
d
          sexprPoint :: ([SExpr], SExpr) -> Maybe (a, a)
sexprPoint (as :: [SExpr]
as, v :: SExpr
v) = (,) (a -> a -> (a, a)) -> Maybe a -> Maybe (a -> (a, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> fun -> [SExpr] -> Maybe a
forall fun a r. SMTFunction fun a r => fun -> [SExpr] -> Maybe a
sexprToArg fun
f [SExpr]
as    Maybe (a -> (a, a)) -> Maybe a -> Maybe (a, a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe a
forall a. SMTValue a => SExpr -> Maybe a
sexprToVal SExpr
v

-- | Generalization of 'Data.SBV.Control.getUninterpretedValue'
getUninterpretedValue :: (MonadIO m, MonadQuery m, HasKind a) => SBV a -> m String
getUninterpretedValue :: SBV a -> m String
getUninterpretedValue s :: SBV a
s =
        case SBV a -> Kind
forall a. HasKind a => a -> Kind
kindOf SBV a
s of
          KUninterpreted _ (Left _) -> 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
s)

                                          let nm :: String
nm  = SV -> String
forall a. Show a => a -> String
show SV
sv
                                              cmd :: String
cmd = "(get-value (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))"
                                              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 "getValue" String
cmd "a model 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 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 [EApp [ECon o :: String
o,  ECon v :: String
v]] | String
o String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== SV -> String
forall a. Show a => a -> String
show SV
sv -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return String
v
                                                              _                                            -> String -> Maybe [String] -> m String
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing

          k :: Kind
k                         -> String -> m String
forall a. HasCallStack => String -> a
error (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [""
                                                       , "*** SBV.getUninterpretedValue: Called on an 'interpreted' kind"
                                                       , "*** "
                                                       , "***    Kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
                                                       , "***    Hint: Use 'getValue' to extract value for interpreted kinds."
                                                       , "*** "
                                                       , "*** Only truly uninterpreted sorts should be used with 'getUninterpretedValue.'"
                                                       ]

-- | Get the value of a term, but in CV form. Used internally. The model-index, in particular is extremely Z3 specific!
getValueCVHelper :: (MonadIO m, MonadQuery m) => Maybe Int -> SV -> m CV
getValueCVHelper :: Maybe Key -> SV -> m CV
getValueCVHelper mbi :: Maybe Key
mbi s :: SV
s
  | SV
s SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV
  = CV -> m CV
forall (m :: * -> *) a. Monad m => a -> m a
return CV
trueCV
  | SV
s SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV
  = CV -> m CV
forall (m :: * -> *) a. Monad m => a -> m a
return CV
falseCV
  | Bool
True
  = do let nm :: String
nm  = SV -> String
forall a. Show a => a -> String
show SV
s
           k :: Kind
k   = SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
s

           modelIndex :: String
modelIndex = case Maybe Key
mbi of
                          Nothing -> ""
                          Just i :: Key
i  -> " :model_index " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
i

           cmd :: String
cmd        = "(get-value (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
modelIndex String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

           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 "getModel" String
cmd ("a value binding for kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k) 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 CV) -> (SExpr -> m CV) -> m CV
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m CV
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m CV) -> m CV) -> (SExpr -> m CV) -> m CV
forall a b. (a -> b) -> a -> b
$ \case EApp [EApp [ECon v :: String
v, val :: SExpr
val]] | String
v String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
nm -> case Kind -> SExpr -> Maybe CV
recoverKindedValue (SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
s) SExpr
val of
                                                                    Just cv :: CV
cv -> CV -> m CV
forall (m :: * -> *) a. Monad m => a -> m a
return CV
cv
                                                                    Nothing -> String -> Maybe [String] -> m CV
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
                           _                                   -> String -> Maybe [String] -> m CV
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing

-- | "Make up" a CV for this type. Like zero, but smarter.
defaultKindedValue :: Kind -> Maybe CV
defaultKindedValue :: Kind -> Maybe CV
defaultKindedValue k :: Kind
k = Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> Maybe CVal -> Maybe CV
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind -> Maybe CVal
cvt Kind
k
  where cvt :: Kind -> Maybe CVal
        cvt :: Kind -> Maybe CVal
cvt KBool                 = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ Integer -> CVal
CInteger 0
        cvt KBounded{}            = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ Integer -> CVal
CInteger 0
        cvt KUnbounded            = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ Integer -> CVal
CInteger 0
        cvt KReal                 = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ AlgReal -> CVal
CAlgReal 0
        cvt (KUninterpreted _ ui :: Either String [String]
ui) = Either String [String] -> Maybe CVal
forall a. Either a [String] -> Maybe CVal
uninterp Either String [String]
ui
        cvt KFloat                = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ Float -> CVal
CFloat 0
        cvt KDouble               = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ Double -> CVal
CDouble 0
        cvt KChar                 = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ Char -> CVal
CChar '\NUL'                -- why not?
        cvt KString               = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ String -> CVal
CString ""
        cvt (KList  _)            = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ [CVal] -> CVal
CList []
        cvt (KSet  _)             = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ RCSet CVal -> CVal
CSet (RCSet CVal -> CVal) -> RCSet CVal -> CVal
forall a b. (a -> b) -> a -> b
$ Set CVal -> RCSet CVal
forall a. Set a -> RCSet a
RegularSet Set CVal
forall a. Set a
Set.empty -- why not? Arguably, could be the universal set
        cvt (KTuple ks :: [Kind]
ks)           = [CVal] -> CVal
CTuple ([CVal] -> CVal) -> Maybe [CVal] -> Maybe CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Kind -> Maybe CVal) -> [Kind] -> Maybe [CVal]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Kind -> Maybe CVal
cvt [Kind]
ks
        cvt (KMaybe _)            = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ Maybe CVal -> CVal
CMaybe Maybe CVal
forall a. Maybe a
Nothing
        cvt (KEither k1 :: Kind
k1 _)        = Either CVal CVal -> CVal
CEither (Either CVal CVal -> CVal)
-> (CVal -> Either CVal CVal) -> CVal -> CVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CVal -> Either CVal CVal
forall a b. a -> Either a b
Left (CVal -> CVal) -> Maybe CVal -> Maybe CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind -> Maybe CVal
cvt Kind
k1          -- why not?

        -- Tricky case of uninterpreted
        uninterp :: Either a [String] -> Maybe CVal
uninterp (Right (c :: String
c:_)) = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ (Maybe Key, String) -> CVal
CUserSort (Key -> Maybe Key
forall a. a -> Maybe a
Just 1, String
c)
        uninterp (Right [])    = Maybe CVal
forall a. Maybe a
Nothing                       -- I don't think this can actually happen, but just in case
        uninterp (Left _)      = Maybe CVal
forall a. Maybe a
Nothing                       -- Out of luck, truly uninterpreted; we don't even know if it's inhabited.

-- | Recover a given solver-printed value with a possible interpretation
recoverKindedValue :: Kind -> SExpr -> Maybe CV
recoverKindedValue :: Kind -> SExpr -> Maybe CV
recoverKindedValue k :: Kind
k e :: SExpr
e = case Kind
k of
                           KBool            | ENum (i :: Integer
i, _) <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k Integer
i
                                            | Bool
True             -> Maybe CV
forall a. Maybe a
Nothing

                           KBounded{}       | ENum (i :: Integer
i, _) <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k Integer
i
                                            | Bool
True             -> Maybe CV
forall a. Maybe a
Nothing

                           KUnbounded       | ENum (i :: Integer
i, _) <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k Integer
i
                                            | Bool
True             -> Maybe CV
forall a. Maybe a
Nothing

                           KReal            | ENum (i :: Integer
i, _) <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k Integer
i
                                            | EReal i :: AlgReal
i     <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KReal (AlgReal -> CVal
CAlgReal AlgReal
i)
                                            | Bool
True             -> Maybe CV
forall a. Maybe a
Nothing

                           KUninterpreted{} | ECon s :: String
s <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ (Maybe Key, String) -> CVal
CUserSort (Kind -> String -> Maybe Key
getUIIndex Kind
k String
s, String
s)
                                            | Bool
True             -> Maybe CV
forall a. Maybe a
Nothing

                           KFloat           | ENum (i :: Integer
i, _) <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k Integer
i
                                            | EFloat i :: Float
i    <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KFloat (Float -> CVal
CFloat Float
i)
                                            | Bool
True             -> Maybe CV
forall a. Maybe a
Nothing

                           KDouble          | ENum (i :: Integer
i, _) <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k Integer
i
                                            | EDouble i :: Double
i   <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KDouble (Double -> CVal
CDouble Double
i)
                                            | Bool
True             -> Maybe CV
forall a. Maybe a
Nothing

                           KChar            | ENum (i :: Integer
i, _) <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KChar (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ Char -> CVal
CChar (Char -> CVal) -> Char -> CVal
forall a b. (a -> b) -> a -> b
$ Key -> Char
chr (Key -> Char) -> Key -> Char
forall a b. (a -> b) -> a -> b
$ Integer -> Key
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
i
                                            | Bool
True             -> Maybe CV
forall a. Maybe a
Nothing

                           KString          | ECon s :: String
s      <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KString (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ String -> CVal
CString (String -> CVal) -> String -> CVal
forall a b. (a -> b) -> a -> b
$ String -> String
interpretString String
s
                                            | Bool
True             -> Maybe CV
forall a. Maybe a
Nothing

                           KList ek :: Kind
ek                            -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ [CVal] -> CVal
CList ([CVal] -> CVal) -> [CVal] -> CVal
forall a b. (a -> b) -> a -> b
$ Kind -> SExpr -> [CVal]
interpretList Kind
ek SExpr
e

                           KSet ek :: Kind
ek                             -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ RCSet CVal -> CVal
CSet (RCSet CVal -> CVal) -> RCSet CVal -> CVal
forall a b. (a -> b) -> a -> b
$ Kind -> SExpr -> RCSet CVal
interpretSet Kind
ek SExpr
e

                           KTuple{}                            -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ [CVal] -> CVal
CTuple ([CVal] -> CVal) -> [CVal] -> CVal
forall a b. (a -> b) -> a -> b
$ SExpr -> [CVal]
interpretTuple SExpr
e

                           KMaybe{}                            -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ Maybe CVal -> CVal
CMaybe (Maybe CVal -> CVal) -> Maybe CVal -> CVal
forall a b. (a -> b) -> a -> b
$ Kind -> SExpr -> Maybe CVal
interpretMaybe Kind
k SExpr
e

                           KEither{}                           -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ Either CVal CVal -> CVal
CEither (Either CVal CVal -> CVal) -> Either CVal CVal -> CVal
forall a b. (a -> b) -> a -> b
$ Kind -> SExpr -> Either CVal CVal
interpretEither Kind
k SExpr
e

  where getUIIndex :: Kind -> String -> Maybe Key
getUIIndex (KUninterpreted  _ (Right xs :: [String]
xs)) i :: String
i = String
i String -> [String] -> Maybe Key
forall a. Eq a => a -> [a] -> Maybe Key
`elemIndex` [String]
xs
        getUIIndex _                              _ = Maybe Key
forall a. Maybe a
Nothing

        stringLike :: String -> Bool
stringLike xs :: String
xs = String -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length String
xs Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
>= 2 Bool -> Bool -> Bool
&& String -> Char
forall a. [a] -> a
head String
xs Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '"' Bool -> Bool -> Bool
&& String -> Char
forall a. [a] -> a
last String
xs Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== '"'

        -- Make sure strings are really strings
        interpretString :: String -> String
interpretString xs :: String
xs
          | Bool -> Bool
not (String -> Bool
stringLike String
xs)
          = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "Expected a string constant with quotes, received: <" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ ">"
          | Bool
True
          = String -> String
qfsToString (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
tail (String -> String
forall a. [a] -> [a]
init String
xs)

        isStringSequence :: Kind -> Bool
isStringSequence (KList (KBounded _ 8)) = Bool
True
        isStringSequence _                      = Bool
False

        -- Lists are tricky since z3 prints the 8-bit variants as strings. See: <http://github.com/Z3Prover/z3/issues/1808>
        interpretList :: Kind -> SExpr -> [CVal]
interpretList _ (ECon s :: String
s)
          | Kind -> Bool
isStringSequence Kind
k Bool -> Bool -> Bool
&& String -> Bool
stringLike String
s
          = (Char -> CVal) -> String -> [CVal]
forall a b. (a -> b) -> [a] -> [b]
map (Integer -> CVal
CInteger (Integer -> CVal) -> (Char -> Integer) -> Char -> CVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Key -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Key -> Integer) -> (Char -> Key) -> Char -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Key
ord) (String -> [CVal]) -> String -> [CVal]
forall a b. (a -> b) -> a -> b
$ String -> String
interpretString String
s
        interpretList ek :: Kind
ek topExpr :: SExpr
topExpr = SExpr -> [CVal]
walk SExpr
topExpr
          where walk :: SExpr -> [CVal]
walk (EApp [ECon "as", ECon "seq.empty", _]) = []
                walk (EApp [ECon "seq.unit", v :: SExpr
v])             = case Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
ek SExpr
v of
                                                                 Just w :: CV
w -> [CV -> CVal
cvVal CV
w]
                                                                 Nothing -> String -> [CVal]
forall a. HasCallStack => String -> a
error (String -> [CVal]) -> String -> [CVal]
forall a b. (a -> b) -> a -> b
$ "Cannot parse a sequence item of kind " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
ek String -> String -> String
forall a. [a] -> [a] -> [a]
++ " from: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
extra SExpr
v
                walk (EApp (ECon "seq.++" : rest :: [SExpr]
rest))           = (SExpr -> [CVal]) -> [SExpr] -> [CVal]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SExpr -> [CVal]
walk [SExpr]
rest
                walk cur :: SExpr
cur                                     = String -> [CVal]
forall a. HasCallStack => String -> a
error (String -> [CVal]) -> String -> [CVal]
forall a b. (a -> b) -> a -> b
$ "Expected a sequence constant, but received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
cur String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
extra SExpr
cur

                extra :: a -> String
extra cur :: a
cur | a -> String
forall a. Show a => a -> String
show a
cur String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
t = ""
                          | Bool
True          = "\nWhile parsing: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
                          where t :: String
t = SExpr -> String
forall a. Show a => a -> String
show SExpr
topExpr

        -- Essentially treat sets as functions, since we do allow for store associations
        interpretSet :: Kind -> SExpr -> RCSet CVal
interpretSet ke :: Kind
ke setExpr :: SExpr
setExpr
             | SExpr -> Bool
isUniversal SExpr
setExpr             = Set CVal -> RCSet CVal
forall a. Set a -> RCSet a
ComplementSet Set CVal
forall a. Set a
Set.empty
             | SExpr -> Bool
isEmpty     SExpr
setExpr             = Set CVal -> RCSet CVal
forall a. Set a -> RCSet a
RegularSet    Set CVal
forall a. Set a
Set.empty
             | Just (Right assocs :: ([([SExpr], SExpr)], SExpr)
assocs) <- Maybe (Either String ([([SExpr], SExpr)], SExpr))
mbAssocs = ([([SExpr], SExpr)], SExpr) -> RCSet CVal
decode ([([SExpr], SExpr)], SExpr)
assocs
             | Bool
True                            = String -> RCSet CVal
forall a. String -> a
tbd "Expected a set value, but couldn't decipher the solver output."

           where tbd :: String -> a
tbd w :: String
w = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ ""
                                         , "*** Data.SBV.interpretSet: Unable to process solver output."
                                         , "***"
                                         , "*** Kind    : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show (Kind -> Kind
KSet Kind
ke)
                                         , "*** Received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
setExpr
                                         , "*** Reason  : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w
                                         , "***"
                                         , "*** This is either a bug or something SBV currently does not support."
                                         , "*** Please report this as a feature request!"
                                         ]


                 isTrue :: SExpr -> Bool
isTrue (ENum (1, Nothing)) = Bool
True
                 isTrue (ENum (0, Nothing)) = Bool
False
                 isTrue bad :: SExpr
bad                 = String -> Bool
forall a. String -> a
tbd (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ "Non-boolean membership value seen: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
bad

                 isUniversal :: SExpr -> Bool
isUniversal (EApp [EApp [ECon "as", ECon "const", EApp [ECon "Array", _, ECon "Bool"]], r :: SExpr
r]) = SExpr -> Bool
isTrue SExpr
r
                 isUniversal _                                                                               = Bool
False

                 isEmpty :: SExpr -> Bool
isEmpty     (EApp [EApp [ECon "as", ECon "const", EApp [ECon "Array", _, ECon "Bool"]], r :: SExpr
r]) = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ SExpr -> Bool
isTrue SExpr
r
                 isEmpty     _                                                                               = Bool
False

                 mbAssocs :: Maybe (Either String ([([SExpr], SExpr)], SExpr))
mbAssocs = SExpr -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
parseSExprFunction SExpr
setExpr

                 decode :: ([([SExpr], SExpr)], SExpr) -> RCSet CVal
decode (args :: [([SExpr], SExpr)]
args, r :: SExpr
r) | SExpr -> Bool
isTrue SExpr
r = Set CVal -> RCSet CVal
forall a. Set a -> RCSet a
ComplementSet (Set CVal -> RCSet CVal) -> Set CVal -> RCSet CVal
forall a b. (a -> b) -> a -> b
$ [CVal] -> Set CVal
forall a. Ord a => [a] -> Set a
Set.fromList [CVal
x | (x :: CVal
x, False) <- (([SExpr], SExpr) -> (CVal, Bool))
-> [([SExpr], SExpr)] -> [(CVal, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map ([SExpr], SExpr) -> (CVal, Bool)
contents [([SExpr], SExpr)]
args]  -- deletions from universal
                                  | Bool
True     = Set CVal -> RCSet CVal
forall a. Set a -> RCSet a
RegularSet    (Set CVal -> RCSet CVal) -> Set CVal -> RCSet CVal
forall a b. (a -> b) -> a -> b
$ [CVal] -> Set CVal
forall a. Ord a => [a] -> Set a
Set.fromList [CVal
x | (x :: CVal
x, True)  <- (([SExpr], SExpr) -> (CVal, Bool))
-> [([SExpr], SExpr)] -> [(CVal, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map ([SExpr], SExpr) -> (CVal, Bool)
contents [([SExpr], SExpr)]
args]  -- additions to empty

                 contents :: ([SExpr], SExpr) -> (CVal, Bool)
contents ([v :: SExpr
v], r :: SExpr
r) = (SExpr -> CVal
element SExpr
v, SExpr -> Bool
isTrue SExpr
r)
                 contents bad :: ([SExpr], SExpr)
bad      = String -> (CVal, Bool)
forall a. String -> a
tbd (String -> (CVal, Bool)) -> String -> (CVal, Bool)
forall a b. (a -> b) -> a -> b
$ "Multi-valued set member seen: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([SExpr], SExpr) -> String
forall a. Show a => a -> String
show ([SExpr], SExpr)
bad

                 element :: SExpr -> CVal
element x :: SExpr
x = case Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
ke SExpr
x of
                               Just v :: CV
v  -> CV -> CVal
cvVal CV
v
                               Nothing -> String -> CVal
forall a. String -> a
tbd (String -> CVal) -> String -> CVal
forall a b. (a -> b) -> a -> b
$ "Unexpected value for kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (SExpr, Kind) -> String
forall a. Show a => a -> String
show (SExpr
x, Kind
ke)

        interpretTuple :: SExpr -> [CVal]
interpretTuple te :: SExpr
te = Key -> [Maybe CV] -> [CVal] -> [CVal]
forall a. (Num a, Show a) => a -> [Maybe CV] -> [CVal] -> [CVal]
walk (1 :: Int) ((Kind -> SExpr -> Maybe CV) -> [Kind] -> [SExpr] -> [Maybe CV]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Kind -> SExpr -> Maybe CV
recoverKindedValue [Kind]
ks [SExpr]
args) []
                where (ks :: [Kind]
ks, n :: Key
n) = case Kind
k of
                                  KTuple eks :: [Kind]
eks -> ([Kind]
eks, [Kind] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [Kind]
eks)
                                  _          -> String -> ([Kind], Key)
forall a. HasCallStack => String -> a
error (String -> ([Kind], Key)) -> String -> ([Kind], Key)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ "Impossible: Expected a tuple kind, but got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
                                                                , "While trying to parse: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
te
                                                                ]

                      args :: [SExpr]
args = Key -> SExpr -> [SExpr]
sexprToTuple Key
n SExpr
te

                      walk :: a -> [Maybe CV] -> [CVal] -> [CVal]
walk _ []           sofar :: [CVal]
sofar = [CVal] -> [CVal]
forall a. [a] -> [a]
reverse [CVal]
sofar
                      walk i :: a
i (Just el :: CV
el:es :: [Maybe CV]
es) sofar :: [CVal]
sofar = a -> [Maybe CV] -> [CVal] -> [CVal]
walk (a
ia -> a -> a
forall a. Num a => a -> a -> a
+1) [Maybe CV]
es (CV -> CVal
cvVal CV
el CVal -> [CVal] -> [CVal]
forall a. a -> [a] -> [a]
: [CVal]
sofar)
                      walk i :: a
i (Nothing:_)  _     = String -> [CVal]
forall a. HasCallStack => String -> a
error (String -> [CVal]) -> String -> [CVal]
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ "Couldn't parse a tuple element at position " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i
                                                                  , "Kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
                                                                  , "Expr: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
te
                                                                  ]

        -- SMaybe
        interpretMaybe :: Kind -> SExpr -> Maybe CVal
interpretMaybe (KMaybe _)  (ECon "nothing_SBVMaybe")        = Maybe CVal
forall a. Maybe a
Nothing
        interpretMaybe (KMaybe ek :: Kind
ek) (EApp [ECon "just_SBVMaybe", a :: SExpr
a]) = case Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
ek SExpr
a of
                                                                        Just (CV _ v :: CVal
v) -> CVal -> Maybe CVal
forall a. a -> Maybe a
Just CVal
v
                                                                        Nothing       -> String -> Maybe CVal
forall a. HasCallStack => String -> a
error (String -> Maybe CVal) -> String -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ "Couldn't parse a maybe just value"
                                                                                                         , "Kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
ek
                                                                                                         , "Expr: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
a
                                                                                                         ]
        -- CVC4 puts in full ascriptions, handle those:
        interpretMaybe _  (      EApp [ECon "as", ECon "nothing_SBVMaybe", _])     = Maybe CVal
forall a. Maybe a
Nothing
        interpretMaybe mk :: Kind
mk (EApp [EApp [ECon "as", ECon "just_SBVMaybe",    _], a :: SExpr
a]) = Kind -> SExpr -> Maybe CVal
interpretMaybe Kind
mk ([SExpr] -> SExpr
EApp [String -> SExpr
ECon "just_SBVMaybe", SExpr
a])

        interpretMaybe _  other :: SExpr
other = String -> Maybe CVal
forall a. HasCallStack => String -> a
error (String -> Maybe CVal) -> String -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ "Expected an SMaybe sexpr, but received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Kind, SExpr) -> String
forall a. Show a => a -> String
show (Kind
k, SExpr
other)

        -- SEither
        interpretEither :: Kind -> SExpr -> Either CVal CVal
interpretEither (KEither k1 :: Kind
k1 _) (EApp [ECon "left_SBVEither",  a :: SExpr
a]) = case Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
k1 SExpr
a of
                                                                              Just (CV _ v :: CVal
v) -> CVal -> Either CVal CVal
forall a b. a -> Either a b
Left CVal
v
                                                                              Nothing       -> String -> Either CVal CVal
forall a. HasCallStack => String -> a
error (String -> Either CVal CVal) -> String -> Either CVal CVal
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ "Couldn't parse an either value on the left"
                                                                                                               , "Kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k1
                                                                                                               , "Expr: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
a
                                                                                                               ]
        interpretEither (KEither _ k2 :: Kind
k2) (EApp [ECon "right_SBVEither", b :: SExpr
b]) = case Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
k2 SExpr
b of
                                                                              Just (CV _ v :: CVal
v) -> CVal -> Either CVal CVal
forall a b. b -> Either a b
Right CVal
v
                                                                              Nothing       -> String -> Either CVal CVal
forall a. HasCallStack => String -> a
error (String -> Either CVal CVal) -> String -> Either CVal CVal
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ "Couldn't parse an either value on the right"
                                                                                                               , "Kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k2
                                                                                                               , "Expr: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
b
                                                                                                               ]

        -- CVC4 puts full ascriptions:
        interpretEither ek :: Kind
ek (EApp [EApp [ECon "as", ECon "left_SBVEither",  _], a :: SExpr
a]) = Kind -> SExpr -> Either CVal CVal
interpretEither Kind
ek ([SExpr] -> SExpr
EApp [String -> SExpr
ECon "left_SBVEither", SExpr
a])
        interpretEither ek :: Kind
ek (EApp [EApp [ECon "as", ECon "right_SBVEither", _], b :: SExpr
b]) = Kind -> SExpr -> Either CVal CVal
interpretEither Kind
ek ([SExpr] -> SExpr
EApp [String -> SExpr
ECon "right_SBVEither", SExpr
b])

        interpretEither _ other :: SExpr
other = String -> Either CVal CVal
forall a. HasCallStack => String -> a
error (String -> Either CVal CVal) -> String -> Either CVal CVal
forall a b. (a -> b) -> a -> b
$ "Expected an SEither sexpr, but received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Kind, SExpr) -> String
forall a. Show a => a -> String
show (Kind
k, SExpr
other)


-- | Generalization of 'Data.SBV.Control.getValueCV'
getValueCV :: (MonadIO m, MonadQuery m) => Maybe Int -> SV -> m CV
getValueCV :: Maybe Key -> SV -> m CV
getValueCV mbi :: Maybe Key
mbi s :: SV
s
  | SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
s Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind
KReal
  = Maybe Key -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> SV -> m CV
getValueCVHelper Maybe Key
mbi SV
s
  | Bool
True
  = do SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
       if Bool -> Bool
not (SolverCapabilities -> Bool
supportsApproxReals (SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)))
          then Maybe Key -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> SV -> m CV
getValueCVHelper Maybe Key
mbi SV
s
          else do Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True "(set-option :pp.decimal false)"
                  CV
rep1 <- Maybe Key -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> SV -> m CV
getValueCVHelper Maybe Key
mbi SV
s
                  Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True   "(set-option :pp.decimal true)"
                  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
$ "(set-option :pp.decimal_precision " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show (SMTConfig -> Key
printRealPrec SMTConfig
cfg) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                  CV
rep2 <- Maybe Key -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> SV -> m CV
getValueCVHelper Maybe Key
mbi SV
s

                  let bad :: 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 "getValueCV" "get-value" ("a real-valued binding for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
s) Maybe [String]
forall a. Maybe a
Nothing ((CV, CV) -> String
forall a. Show a => a -> String
show (CV
rep1, CV
rep2)) Maybe [String]
forall a. Maybe a
Nothing

                  case (CV
rep1, CV
rep2) of
                    (CV KReal (CAlgReal a :: AlgReal
a), CV KReal (CAlgReal b :: AlgReal
b)) -> CV -> m CV
forall (m :: * -> *) a. Monad m => a -> m a
return (CV -> m CV) -> CV -> m CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KReal (AlgReal -> CVal
CAlgReal (String -> AlgReal -> AlgReal -> AlgReal
mergeAlgReals ("Cannot merge real-values for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
s) AlgReal
a AlgReal
b))
                    _                                              -> m CV
forall a. m a
bad

-- | Generalization of 'Data.SBV.Control.getUIFunCVAssoc'
getUIFunCVAssoc :: forall m. (MonadIO m, MonadQuery m) => Maybe Int -> (String, SBVType) -> m ([([CV], CV)], CV)
getUIFunCVAssoc :: Maybe Key -> (String, SBVType) -> m ([([CV], CV)], CV)
getUIFunCVAssoc mbi :: Maybe Key
mbi (nm :: String
nm, typ :: SBVType
typ) = do
  let modelIndex :: String
modelIndex = case Maybe Key
mbi of
                     Nothing -> ""
                     Just i :: Key
i  -> " :model_index " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
i

      cmd :: String
cmd        = "(get-value (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
modelIndex String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

      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 "get-value" String
cmd "a function 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

  let (ats :: [Kind]
ats, rt :: Kind
rt) = case SBVType
typ of
                    SBVType as :: [Kind]
as | [Kind] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [Kind]
as Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
> 1 -> ([Kind] -> [Kind]
forall a. [a] -> [a]
init [Kind]
as, [Kind] -> Kind
forall a. [a] -> a
last [Kind]
as)
                    _                          -> String -> ([Kind], Kind)
forall a. HasCallStack => String -> a
error (String -> ([Kind], Kind)) -> String -> ([Kind], Kind)
forall a b. (a -> b) -> a -> b
$ "Data.SBV.getUIFunCVAssoc: Expected a function type, got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVType -> String
forall a. Show a => a -> String
show SBVType
typ

  let convert :: (t ([SExpr], SExpr), SExpr) -> Maybe (t ([CV], CV), CV)
convert (vs :: t ([SExpr], SExpr)
vs, d :: SExpr
d) = (,) (t ([CV], CV) -> CV -> (t ([CV], CV), CV))
-> Maybe (t ([CV], CV)) -> Maybe (CV -> (t ([CV], CV), CV))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (([SExpr], SExpr) -> Maybe ([CV], CV))
-> t ([SExpr], SExpr) -> Maybe (t ([CV], CV))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([SExpr], SExpr) -> Maybe ([CV], CV)
toPoint t ([SExpr], SExpr)
vs Maybe (CV -> (t ([CV], CV), CV))
-> Maybe CV -> Maybe (t ([CV], CV), CV)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe CV
toRes SExpr
d
      toPoint :: ([SExpr], SExpr) -> Maybe ([CV], CV)
toPoint (as :: [SExpr]
as, v :: SExpr
v)
         | [SExpr] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [SExpr]
as Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== [Kind] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [Kind]
ats = (,) ([CV] -> CV -> ([CV], CV))
-> Maybe [CV] -> Maybe (CV -> ([CV], CV))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Kind -> SExpr -> Maybe CV) -> [Kind] -> [SExpr] -> Maybe [CV]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Kind -> SExpr -> Maybe CV
recoverKindedValue [Kind]
ats [SExpr]
as Maybe (CV -> ([CV], CV)) -> Maybe CV -> Maybe ([CV], CV)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe CV
toRes SExpr
v
         | Bool
True                    = String -> Maybe ([CV], CV)
forall a. HasCallStack => String -> a
error (String -> Maybe ([CV], CV)) -> String -> Maybe ([CV], CV)
forall a b. (a -> b) -> a -> b
$ "Data.SBV.getUIFunCVAssoc: Mismatching type/value arity, got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([SExpr], [Kind]) -> String
forall a. Show a => a -> String
show ([SExpr]
as, [Kind]
ats)

      toRes :: SExpr -> Maybe CV
      toRes :: SExpr -> Maybe CV
toRes = Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
rt

      -- In case we end up in the pointwise scenerio, boolify the result
      -- as that's the only type we support here.
      tryPointWise :: m ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
tryPointWise bailOut :: m ([([CV], CV)], CV)
bailOut = do Maybe ([([SExpr], SExpr)], SExpr)
mbSExprs <- String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
pointWiseExtract String
nm SBVType
typ
                                case Maybe ([([SExpr], SExpr)], SExpr)
mbSExprs of
                                  Nothing     -> m ([([CV], CV)], CV)
bailOut
                                  Just sExprs :: ([([SExpr], SExpr)], SExpr)
sExprs -> m ([([CV], CV)], CV)
-> (([([CV], CV)], CV) -> m ([([CV], CV)], CV))
-> Maybe ([([CV], CV)], CV)
-> m ([([CV], CV)], CV)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m ([([CV], CV)], CV)
bailOut ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
forall (m :: * -> *) a. Monad m => a -> m a
return (([([SExpr], SExpr)], SExpr) -> Maybe ([([CV], CV)], CV)
forall (t :: * -> *).
Traversable t =>
(t ([SExpr], SExpr), SExpr) -> Maybe (t ([CV], CV), CV)
convert ([([SExpr], SExpr)], SExpr)
sExprs)

  String
-> (String -> Maybe [String] -> m ([([CV], CV)], CV))
-> (SExpr -> m ([([CV], CV)], CV))
-> m ([([CV], CV)], CV)
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m ([([CV], CV)], CV)
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m ([([CV], CV)], CV)) -> m ([([CV], CV)], CV))
-> (SExpr -> m ([([CV], CV)], CV)) -> m ([([CV], CV)], CV)
forall a b. (a -> b) -> a -> b
$ \case EApp [EApp [ECon o :: String
o, e :: SExpr
e]] | String
o String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
nm -> let bailOut :: m a
bailOut = String -> Maybe [String] -> m a
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
                                                           in case SExpr -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
parseSExprFunction SExpr
e of
                                                                Just (Right assocs :: ([([SExpr], SExpr)], SExpr)
assocs) | Just res :: ([([CV], CV)], CV)
res <- ([([SExpr], SExpr)], SExpr) -> Maybe ([([CV], CV)], CV)
forall (t :: * -> *).
Traversable t =>
(t ([SExpr], SExpr), SExpr) -> Maybe (t ([CV], CV), CV)
convert ([([SExpr], SExpr)], SExpr)
assocs                   -> ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ([([CV], CV)], CV)
res
                                                                                    | Bool
True                                         -> m ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
tryPointWise m ([([CV], CV)], CV)
forall a. m a
bailOut

                                                                Just (Left nm' :: String
nm')     | String
nm String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
nm', Just res :: CV
res <- Kind -> Maybe CV
defaultKindedValue Kind
rt -> ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], CV
res)
                                                                                    | Bool
True                                         -> String -> Maybe [String] -> m ([([CV], CV)], CV)
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing

                                                                Nothing                                                            -> m ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
tryPointWise m ([([CV], CV)], CV)
forall a. m a
bailOut

                      _                                 -> String -> Maybe [String] -> m ([([CV], CV)], CV)
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing

-- | Generalization of 'Data.SBV.Control.checkSat'
checkSat :: (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat :: m CheckSatResult
checkSat = do SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
              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

-- | Generalization of 'Data.SBV.Control.checkSatUsing'
checkSatUsing :: (MonadIO m, MonadQuery m) => String -> m CheckSatResult
checkSatUsing :: String -> m CheckSatResult
checkSatUsing cmd :: String
cmd = do let 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 "checkSat" String
cmd "one of sat/unsat/unknown" Maybe [String]
forall a. Maybe a
Nothing

                           -- Sigh.. Ignore some of the pesky warnings. We only do it as an exception here.
                           ignoreList :: [String]
ignoreList = ["WARNING: optimization with quantified constraints is not supported"]

                       String
r <- String -> [String] -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> [String] -> m String
askIgnoring String
cmd [String]
ignoreList

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

-- | What are the top level inputs? Trackers are returned as top level existentials
getQuantifiedInputs :: (MonadIO m, MonadQuery m) => m [(Quantifier, NamedSymVar)]
getQuantifiedInputs :: m [(Quantifier, NamedSymVar)]
getQuantifiedInputs = do State{IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
rinps :: State
-> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
rinps :: IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
rinps} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
                         ((rQinps :: [(Quantifier, NamedSymVar)]
rQinps, rTrackers :: [NamedSymVar]
rTrackers), _) <- IO (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
-> m (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
 -> m (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String))
-> IO (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
-> m (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
forall a b. (a -> b) -> a -> b
$ IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
-> IO (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
forall a. IORef a -> IO a
readIORef IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
rinps

                         let qinps :: [(Quantifier, NamedSymVar)]
qinps    = [(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
forall a. [a] -> [a]
reverse [(Quantifier, NamedSymVar)]
rQinps
                             trackers :: [(Quantifier, NamedSymVar)]
trackers = (NamedSymVar -> (Quantifier, NamedSymVar))
-> [NamedSymVar] -> [(Quantifier, NamedSymVar)]
forall a b. (a -> b) -> [a] -> [b]
map (Quantifier
EX,) ([NamedSymVar] -> [(Quantifier, NamedSymVar)])
-> [NamedSymVar] -> [(Quantifier, NamedSymVar)]
forall a b. (a -> b) -> a -> b
$ [NamedSymVar] -> [NamedSymVar]
forall a. [a] -> [a]
reverse [NamedSymVar]
rTrackers

                             -- separate the existential prefix, which will go first
                             (preQs :: [(Quantifier, NamedSymVar)]
preQs, postQs :: [(Quantifier, NamedSymVar)]
postQs) = ((Quantifier, NamedSymVar) -> Bool)
-> [(Quantifier, NamedSymVar)]
-> ([(Quantifier, NamedSymVar)], [(Quantifier, NamedSymVar)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (\(q :: Quantifier
q, _) -> Quantifier
q Quantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
== Quantifier
EX) [(Quantifier, NamedSymVar)]
qinps

                         [(Quantifier, NamedSymVar)] -> m [(Quantifier, NamedSymVar)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Quantifier, NamedSymVar)] -> m [(Quantifier, NamedSymVar)])
-> [(Quantifier, NamedSymVar)] -> m [(Quantifier, NamedSymVar)]
forall a b. (a -> b) -> a -> b
$ [(Quantifier, NamedSymVar)]
preQs [(Quantifier, NamedSymVar)]
-> [(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
forall a. [a] -> [a] -> [a]
++ [(Quantifier, NamedSymVar)]
trackers [(Quantifier, NamedSymVar)]
-> [(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
forall a. [a] -> [a] -> [a]
++ [(Quantifier, NamedSymVar)]
postQs

-- | Get observables, i.e., those explicitly labeled by the user with a call to 'Data.SBV.observe'.
getObservables :: (MonadIO m, MonadQuery m) => m [(String, CV)]
getObservables :: m [(String, CV)]
getObservables = do State{IORef [(String, CV -> Bool, SV)]
rObservables :: State -> IORef [(String, CV -> Bool, SV)]
rObservables :: IORef [(String, CV -> Bool, SV)]
rObservables} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState

                    [(String, CV -> Bool, SV)]
rObs <- IO [(String, CV -> Bool, SV)] -> m [(String, CV -> Bool, SV)]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [(String, CV -> Bool, SV)] -> m [(String, CV -> Bool, SV)])
-> IO [(String, CV -> Bool, SV)] -> m [(String, CV -> Bool, SV)]
forall a b. (a -> b) -> a -> b
$ IORef [(String, CV -> Bool, SV)] -> IO [(String, CV -> Bool, SV)]
forall a. IORef a -> IO a
readIORef IORef [(String, CV -> Bool, SV)]
rObservables

                    -- This intentionally reverses the result; since 'rObs' stores in reversed order
                    let walk :: [(a, CV -> Bool, SV)] -> [(a, CV)] -> m [(a, CV)]
walk []             sofar :: [(a, CV)]
sofar = [(a, CV)] -> m [(a, CV)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(a, CV)]
sofar
                        walk ((n :: a
n, f :: CV -> Bool
f, s :: SV
s):os :: [(a, CV -> Bool, SV)]
os) sofar :: [(a, CV)]
sofar = do CV
cv <- Maybe Key -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> SV -> m CV
getValueCV Maybe Key
forall a. Maybe a
Nothing SV
s
                                                       if CV -> Bool
f CV
cv
                                                          then [(a, CV -> Bool, SV)] -> [(a, CV)] -> m [(a, CV)]
walk [(a, CV -> Bool, SV)]
os ((a
n, CV
cv) (a, CV) -> [(a, CV)] -> [(a, CV)]
forall a. a -> [a] -> [a]
: [(a, CV)]
sofar)
                                                          else [(a, CV -> Bool, SV)] -> [(a, CV)] -> m [(a, CV)]
walk [(a, CV -> Bool, SV)]
os            [(a, CV)]
sofar

                    [(String, CV -> Bool, SV)] -> [(String, CV)] -> m [(String, CV)]
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
[(a, CV -> Bool, SV)] -> [(a, CV)] -> m [(a, CV)]
walk [(String, CV -> Bool, SV)]
rObs []

-- | Get UIs, both constants and functions. This call returns both the before and after query ones.
-- | Generalization of 'Data.SBV.Control.getUIs'.
getUIs :: forall m. (MonadIO m, MonadQuery m) => m [(String, SBVType)]
getUIs :: m [(String, SBVType)]
getUIs = do State{IORef (Map String SBVType)
rUIMap :: IORef (Map String SBVType)
rUIMap :: State -> IORef (Map String SBVType)
rUIMap, IORef IncState
rIncState :: State -> IORef IncState
rIncState :: IORef IncState
rIncState} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
            Map String SBVType
prior <- IO (Map String SBVType) -> m (Map String SBVType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (Map String SBVType) -> m (Map String SBVType))
-> IO (Map String SBVType) -> m (Map String SBVType)
forall a b. (a -> b) -> a -> b
$ IORef (Map String SBVType) -> IO (Map String SBVType)
forall a. IORef a -> IO a
readIORef IORef (Map String SBVType)
rUIMap
            Map String SBVType
new   <- IO (Map String SBVType) -> m (Map String SBVType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (Map String SBVType) -> m (Map String SBVType))
-> IO (Map String SBVType) -> m (Map String SBVType)
forall a b. (a -> b) -> a -> b
$ IORef IncState -> IO IncState
forall a. IORef a -> IO a
readIORef IORef IncState
rIncState IO IncState
-> (IncState -> IO (Map String SBVType)) -> IO (Map String SBVType)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IORef (Map String SBVType) -> IO (Map String SBVType)
forall a. IORef a -> IO a
readIORef (IORef (Map String SBVType) -> IO (Map String SBVType))
-> (IncState -> IORef (Map String SBVType))
-> IncState
-> IO (Map String SBVType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IncState -> IORef (Map String SBVType)
rNewUIs
            [(String, SBVType)] -> m [(String, SBVType)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(String, SBVType)] -> m [(String, SBVType)])
-> [(String, SBVType)] -> m [(String, SBVType)]
forall a b. (a -> b) -> a -> b
$ [(String, SBVType)] -> [(String, SBVType)]
forall a. Eq a => [a] -> [a]
nub ([(String, SBVType)] -> [(String, SBVType)])
-> [(String, SBVType)] -> [(String, SBVType)]
forall a b. (a -> b) -> a -> b
$ [(String, SBVType)] -> [(String, SBVType)]
forall a. Ord a => [a] -> [a]
sort ([(String, SBVType)] -> [(String, SBVType)])
-> [(String, SBVType)] -> [(String, SBVType)]
forall a b. (a -> b) -> a -> b
$ Map String SBVType -> [(String, SBVType)]
forall k a. Map k a -> [(k, a)]
Map.toList Map String SBVType
prior [(String, SBVType)] -> [(String, SBVType)] -> [(String, SBVType)]
forall a. [a] -> [a] -> [a]
++ Map String SBVType -> [(String, SBVType)]
forall k a. Map k a -> [(k, a)]
Map.toList Map String SBVType
new

-- | Repeatedly issue check-sat, after refuting the previous model.
-- The bool is true if the model is unique upto prefix existentials.
getAllSatResult :: forall m. (MonadIO m, MonadQuery m, SolverContext m) => m (Bool, Bool, Bool, [SMTResult])
getAllSatResult :: m (Bool, Bool, Bool, [SMTResult])
getAllSatResult = do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["*** Checking Satisfiability, all solutions.."]

                     SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig

                     topState :: State
topState@State{IORef KindSet
rUsedKinds :: State -> IORef KindSet
rUsedKinds :: IORef KindSet
rUsedKinds} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState

                     KindSet
ki    <- IO KindSet -> m KindSet
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO KindSet -> m KindSet) -> IO KindSet -> m KindSet
forall a b. (a -> b) -> a -> b
$ IORef KindSet -> IO KindSet
forall a. IORef a -> IO a
readIORef IORef KindSet
rUsedKinds
                     [(Quantifier, NamedSymVar)]
qinps <- m [(Quantifier, NamedSymVar)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(Quantifier, NamedSymVar)]
getQuantifiedInputs

                     [(String, SBVType)]
allUninterpreteds <- m [(String, SBVType)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, SBVType)]
getUIs

                      -- Functions have at least two kinds in their type and all components must be "interpreted"
                     let allUiFuns :: [(String, SBVType)]
allUiFuns = [(String, SBVType)
u | SMTConfig -> Bool
satTrackUFs SMTConfig
cfg                                         -- config says consider UIFs
                                        , u :: (String, SBVType)
u@(nm :: String
nm, SBVType as :: [Kind]
as) <- [(String, SBVType)]
allUninterpreteds, [Kind] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [Kind]
as Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
> 1  -- get the function ones
                                        , Bool -> Bool
not (SMTConfig -> String -> Bool
isNonModelVar SMTConfig
cfg String
nm)                              -- make sure they aren't explicitly ignored
                                     ]

                         -- We can only "allSat" if all component types themselves are interpreted. (Otherwise
                         -- there is no way to reflect back the values to the solver.)
                         collectAcceptable :: [(String, SBVType)] -> [String] -> m [String]
collectAcceptable []                              sofar :: [String]
sofar = [String] -> m [String]
forall (m :: * -> *) a. Monad m => a -> m a
return [String]
sofar
                         collectAcceptable ((nm :: String
nm, t :: SBVType
t@(SBVType ats :: [Kind]
ats)):rest :: [(String, SBVType)]
rest) sofar :: [String]
sofar
                           | Bool -> Bool
not ((Kind -> Bool) -> [Kind] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
hasUninterpretedSorts [Kind]
ats)
                           = [(String, SBVType)] -> [String] -> m [String]
collectAcceptable [(String, SBVType)]
rest (String
nm String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)
                           | Bool
True
                           = do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [ "*** SBV.allSat: Uninterpreted function: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVType -> String
forall a. Show a => a -> String
show SBVType
t
                                           , "*** Will *not* be used in allSat consideretions since its type"
                                           , "*** has uninterpreted sorts present."
                                           ]
                                [(String, SBVType)] -> [String] -> m [String]
collectAcceptable [(String, SBVType)]
rest [String]
sofar

                     [String]
uiFuns <- [String] -> [String]
forall a. [a] -> [a]
reverse ([String] -> [String]) -> m [String] -> m [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(String, SBVType)] -> [String] -> m [String]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
[(String, SBVType)] -> [String] -> m [String]
collectAcceptable [(String, SBVType)]
allUiFuns []

                     -- If there are uninterpreted functions, arrange so that z3's pretty-printer flattens things out
                     -- as cex's tend to get larger
                     Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
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
                             Nothing   -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                             Just cmds :: [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

                     let usorts :: [String]
usorts = [String
s | us :: Kind
us@(KUninterpreted s :: String
s _) <- KindSet -> [Kind]
forall a. Set a -> [a]
Set.toAscList KindSet
ki, Kind -> Bool
isFree Kind
us]

                     Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
usorts) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [ "*** SBV.allSat: Uninterpreted sorts present: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
usorts
                                                       , "***             SBV will use equivalence classes to generate all-satisfying instances."
                                                       ]

                     let allModelInputs :: [(Quantifier, NamedSymVar)]
allModelInputs  = ((Quantifier, NamedSymVar) -> Bool)
-> [(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile ((Quantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
/= Quantifier
ALL) (Quantifier -> Bool)
-> ((Quantifier, NamedSymVar) -> Quantifier)
-> (Quantifier, NamedSymVar)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Quantifier, NamedSymVar) -> Quantifier
forall a b. (a, b) -> a
fst) [(Quantifier, NamedSymVar)]
qinps
                         -- Add on observables only if we're not in a quantified context:
                         grabObservables :: Bool
grabObservables = [(Quantifier, NamedSymVar)] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [(Quantifier, NamedSymVar)]
allModelInputs Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== [(Quantifier, NamedSymVar)] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [(Quantifier, NamedSymVar)]
qinps -- i.e., we didn't drop anything

                         vars :: [(SVal, NamedSymVar)]
                         vars :: [(SVal, NamedSymVar)]
vars = let sortByNodeId :: [NamedSymVar] -> [NamedSymVar]
                                    sortByNodeId :: [NamedSymVar] -> [NamedSymVar]
sortByNodeId = (NamedSymVar -> NamedSymVar -> Ordering)
-> [NamedSymVar] -> [NamedSymVar]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (NodeId -> NodeId -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (NodeId -> NodeId -> Ordering)
-> (NamedSymVar -> NodeId)
-> NamedSymVar
-> NamedSymVar
-> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (\(SV _ n :: NodeId
n, _) -> NodeId
n))

                                    mkSVal :: NamedSymVar -> (SVal, NamedSymVar)
                                    mkSVal :: NamedSymVar -> (SVal, NamedSymVar)
mkSVal nm :: NamedSymVar
nm@(sv :: SV
sv, _) = (Kind -> Either CV (Cached SV) -> SVal
SVal (SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
sv) (Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right ((State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache (IO SV -> State -> IO SV
forall a b. a -> b -> a
const (SV -> IO SV
forall (m :: * -> *) a. Monad m => a -> m a
return SV
sv)))), NamedSymVar
nm)

                                    ignored :: String -> Bool
ignored n :: String
n = SMTConfig -> String -> Bool
isNonModelVar SMTConfig
cfg String
n Bool -> Bool -> Bool
|| "__internal_sbv" String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` String
n

                                in (NamedSymVar -> (SVal, NamedSymVar))
-> [NamedSymVar] -> [(SVal, NamedSymVar)]
forall a b. (a -> b) -> [a] -> [b]
map NamedSymVar -> (SVal, NamedSymVar)
mkSVal ([NamedSymVar] -> [(SVal, NamedSymVar)])
-> [NamedSymVar] -> [(SVal, NamedSymVar)]
forall a b. (a -> b) -> a -> b
$ [NamedSymVar] -> [NamedSymVar]
sortByNodeId [NamedSymVar
nv | (_, nv :: NamedSymVar
nv@(_, n :: String
n)) <- [(Quantifier, NamedSymVar)]
allModelInputs, Bool -> Bool
not (String -> Bool
ignored String
n)]

                         -- If we have any universals, then the solutions are unique upto prefix existentials.
                         w :: Bool
w = Quantifier
ALL Quantifier -> [Quantifier] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((Quantifier, NamedSymVar) -> Quantifier)
-> [(Quantifier, NamedSymVar)] -> [Quantifier]
forall a b. (a -> b) -> [a] -> [b]
map (Quantifier, NamedSymVar) -> Quantifier
forall a b. (a, b) -> a
fst [(Quantifier, NamedSymVar)]
qinps

                     (sc :: Bool
sc, unk :: Bool
unk, ms :: [SMTResult]
ms) <- Bool
-> State
-> ([(String, SBVType)], [String])
-> [(Quantifier, NamedSymVar)]
-> [(SVal, NamedSymVar)]
-> SMTConfig
-> m (Bool, Bool, [SMTResult])
forall (t :: * -> *).
Foldable t =>
Bool
-> State
-> ([(String, SBVType)], t String)
-> [(Quantifier, NamedSymVar)]
-> [(SVal, NamedSymVar)]
-> SMTConfig
-> m (Bool, Bool, [SMTResult])
loop Bool
grabObservables State
topState ([(String, SBVType)]
allUiFuns, [String]
uiFuns) [(Quantifier, NamedSymVar)]
qinps [(SVal, NamedSymVar)]
vars SMTConfig
cfg
                     (Bool, Bool, Bool, [SMTResult])
-> m (Bool, Bool, Bool, [SMTResult])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
sc, Bool
w, Bool
unk, [SMTResult] -> [SMTResult]
forall a. [a] -> [a]
reverse [SMTResult]
ms)

   where isFree :: Kind -> Bool
isFree (KUninterpreted _ (Left _)) = Bool
True
         isFree _                           = Bool
False

         loop :: Bool
-> State
-> ([(String, SBVType)], t String)
-> [(Quantifier, NamedSymVar)]
-> [(SVal, NamedSymVar)]
-> SMTConfig
-> m (Bool, Bool, [SMTResult])
loop grabObservables :: Bool
grabObservables topState :: State
topState (allUiFuns :: [(String, SBVType)]
allUiFuns, uiFunsToReject :: t String
uiFunsToReject) qinps :: [(Quantifier, NamedSymVar)]
qinps vars :: [(SVal, NamedSymVar)]
vars cfg :: SMTConfig
cfg = Key -> [SMTResult] -> m (Bool, Bool, [SMTResult])
go (1::Int) []
           where go :: Int -> [SMTResult] -> m (Bool, Bool, [SMTResult])
                 go :: Key -> [SMTResult] -> m (Bool, Bool, [SMTResult])
go !Key
cnt sofar :: [SMTResult]
sofar
                   | Just maxModels :: Key
maxModels <- SMTConfig -> Maybe Key
allSatMaxModelCount SMTConfig
cfg, Key
cnt Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
> Key
maxModels
                   = do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["*** Maximum model count request of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
maxModels String -> String -> String
forall a. [a] -> [a] -> [a]
++ " reached, stopping the search."]

                        Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SMTConfig -> Bool
allSatPrintAlong SMTConfig
cfg) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn "Search stopped since model count request was reached."

                        (Bool, Bool, [SMTResult]) -> m (Bool, Bool, [SMTResult])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
True, Bool
False, [SMTResult]
sofar)
                   | Bool
True
                   = do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["Looking for solution " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
cnt]

                        let endMsg :: m ()
endMsg = Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SMTConfig -> Bool
allSatPrintAlong SMTConfig
cfg Bool -> Bool -> Bool
&& Bool -> Bool
not ([SMTResult] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SMTResult]
sofar)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
                                             let msg :: a -> String
msg 0 = "No solutions found."
                                                 msg 1 = "This is the only solution."
                                                 msg n :: a
n = "Found " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ " different solutions."
                                             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 (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ Key -> String
forall a. (Eq a, Num a, Show a) => a -> String
msg (Key
cnt Key -> Key -> Key
forall a. Num a => a -> a -> a
- 1)

                        CheckSatResult
cs <- m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat

                        case CheckSatResult
cs of
                          Unsat -> do m ()
endMsg
                                      (Bool, Bool, [SMTResult]) -> m (Bool, Bool, [SMTResult])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Bool
False, [SMTResult]
sofar)

                          Unk   -> do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["*** Solver returned unknown, terminating query."]
                                      m ()
endMsg
                                      (Bool, Bool, [SMTResult]) -> m (Bool, Bool, [SMTResult])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Bool
True, [SMTResult]
sofar)

                          Sat   -> do [(SV, (String, (SVal, CV)))]
assocs <- ((SVal, NamedSymVar) -> m (SV, (String, (SVal, CV))))
-> [(SVal, NamedSymVar)] -> m [(SV, (String, (SVal, CV)))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\(sval :: SVal
sval, (sv :: SV
sv, n :: String
n)) -> do CV
cv <- Maybe Key -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> SV -> m CV
getValueCV Maybe Key
forall a. Maybe a
Nothing SV
sv
                                                                             (SV, (String, (SVal, CV))) -> m (SV, (String, (SVal, CV)))
forall (m :: * -> *) a. Monad m => a -> m a
return (SV
sv, (String
n, (SVal
sval, CV
cv)))) [(SVal, NamedSymVar)]
vars

                                      let getUIFun :: (String, SBVType) -> m (String, (SBVType, ([([CV], CV)], CV)))
getUIFun ui :: (String, SBVType)
ui@(nm :: String
nm, t :: SBVType
t) = do ([([CV], CV)], CV)
cvs <- Maybe Key -> (String, SBVType) -> m ([([CV], CV)], CV)
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> (String, SBVType) -> m ([([CV], CV)], CV)
getUIFunCVAssoc Maybe Key
forall a. Maybe a
Nothing (String, SBVType)
ui
                                                                   (String, (SBVType, ([([CV], CV)], CV)))
-> m (String, (SBVType, ([([CV], CV)], CV)))
forall (m :: * -> *) a. Monad m => a -> m a
return (String
nm, (SBVType
t, ([([CV], CV)], CV)
cvs))
                                      [(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 (String, SBVType) -> m (String, (SBVType, ([([CV], CV)], CV)))
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(String, SBVType) -> m (String, (SBVType, ([([CV], CV)], CV)))
getUIFun [(String, SBVType)]
allUiFuns

                                      -- Add on observables if we're asked to do so:
                                      [(String, CV)]
obsvs <- if Bool
grabObservables
                                                  then m [(String, CV)]
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m [(String, CV)]
getObservables
                                                  else do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug ["*** In a quantified context, obvservables will not be printed."]
                                                          [(String, CV)] -> m [(String, CV)]
forall (m :: * -> *) a. Monad m => a -> m a
return []

                                      Maybe [((Quantifier, NamedSymVar), Maybe CV)]
bindings <- let grab :: (Quantifier, (SV, b)) -> m ((Quantifier, (SV, b)), Maybe CV)
grab i :: (Quantifier, (SV, b))
i@(ALL, _)      = ((Quantifier, (SV, b)), Maybe CV)
-> m ((Quantifier, (SV, b)), Maybe CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, (SV, b))
i, Maybe CV
forall a. Maybe a
Nothing)
                                                      grab i :: (Quantifier, (SV, b))
i@(EX, (sv :: SV
sv, _)) = case SV
sv SV -> [(SV, (String, (SVal, CV)))] -> Maybe (String, (SVal, CV))
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(SV, (String, (SVal, CV)))]
assocs of
                                                                               Just (_, (_, cv :: CV
cv)) -> ((Quantifier, (SV, b)), Maybe CV)
-> m ((Quantifier, (SV, b)), Maybe CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, (SV, b))
i, CV -> Maybe CV
forall a. a -> Maybe a
Just CV
cv)
                                                                               Nothing           -> do CV
cv <- Maybe Key -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> SV -> m CV
getValueCV Maybe Key
forall a. Maybe a
Nothing SV
sv
                                                                                                       ((Quantifier, (SV, b)), Maybe CV)
-> m ((Quantifier, (SV, b)), Maybe CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, (SV, b))
i, CV -> Maybe CV
forall a. a -> Maybe a
Just CV
cv)
                                                  in if SMTConfig -> Bool
validationRequested SMTConfig
cfg
                                                        then [((Quantifier, NamedSymVar), Maybe CV)]
-> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
forall a. a -> Maybe a
Just ([((Quantifier, NamedSymVar), Maybe CV)]
 -> Maybe [((Quantifier, NamedSymVar), Maybe CV)])
-> m [((Quantifier, NamedSymVar), Maybe CV)]
-> m (Maybe [((Quantifier, NamedSymVar), Maybe CV)])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Quantifier, NamedSymVar)
 -> m ((Quantifier, NamedSymVar), Maybe CV))
-> [(Quantifier, NamedSymVar)]
-> m [((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 :: * -> *) b.
(MonadIO m, MonadQuery m) =>
(Quantifier, (SV, b)) -> m ((Quantifier, (SV, b)), Maybe CV)
grab [(Quantifier, NamedSymVar)]
qinps
                                                        else Maybe [((Quantifier, NamedSymVar), Maybe CV)]
-> m (Maybe [((Quantifier, NamedSymVar), Maybe CV)])
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe [((Quantifier, NamedSymVar), Maybe CV)]
forall a. Maybe a
Nothing

                                      let model :: SMTModel
model = 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)]
bindings
                                                           , modelAssocs :: [(String, CV)]
modelAssocs     = ((String, CV) -> String) -> [(String, CV)] -> [(String, CV)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (String, CV) -> String
forall a b. (a, b) -> a
fst [(String, CV)]
obsvs [(String, CV)] -> [(String, CV)] -> [(String, CV)]
forall a. [a] -> [a] -> [a]
++ [(String
n, CV
cv) | (_, (n :: String
n, (_, cv :: CV
cv))) <- [(SV, (String, (SVal, CV)))]
assocs]
                                                           , modelUIFuns :: [(String, (SBVType, ([([CV], CV)], CV)))]
modelUIFuns     = [(String, (SBVType, ([([CV], CV)], CV)))]
uiFunVals
                                                           }
                                          m :: SMTResult
m = SMTConfig -> SMTModel -> SMTResult
Satisfiable SMTConfig
cfg SMTModel
model

                                          (interpreteds :: [(SVal, CV)]
interpreteds, uninterpreteds :: [(SVal, CV)]
uninterpreteds) = ((SVal, CV) -> Bool)
-> [(SVal, CV)] -> ([(SVal, CV)], [(SVal, CV)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Bool -> Bool
not (Bool -> Bool) -> ((SVal, CV) -> Bool) -> (SVal, CV) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Bool
isFree (Kind -> Bool) -> ((SVal, CV) -> Kind) -> (SVal, CV) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf (SVal -> Kind) -> ((SVal, CV) -> SVal) -> (SVal, CV) -> Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SVal, CV) -> SVal
forall a b. (a, b) -> a
fst) (((SV, (String, (SVal, CV))) -> (SVal, CV))
-> [(SV, (String, (SVal, CV)))] -> [(SVal, CV)]
forall a b. (a -> b) -> [a] -> [b]
map ((String, (SVal, CV)) -> (SVal, CV)
forall a b. (a, b) -> b
snd ((String, (SVal, CV)) -> (SVal, CV))
-> ((SV, (String, (SVal, CV))) -> (String, (SVal, CV)))
-> (SV, (String, (SVal, CV)))
-> (SVal, CV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SV, (String, (SVal, CV))) -> (String, (SVal, CV))
forall a b. (a, b) -> b
snd) [(SV, (String, (SVal, CV)))]
assocs)

                                          -- For each interpreted variable, figure out the model equivalence
                                          -- NB. When the kind is floating, we *have* to be careful, since +/- zero, and NaN's
                                          -- and equality don't get along!
                                          interpretedEqs :: [SVal]
                                          interpretedEqs :: [SVal]
interpretedEqs = [Kind -> SVal -> SVal -> SVal
forall a. HasKind a => a -> SVal -> SVal -> SVal
mkNotEq (SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
sv) SVal
sv (Kind -> Either CV (Cached SV) -> SVal
SVal (SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
sv) (CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left CV
cv)) | (sv :: SVal
sv, cv :: CV
cv) <- [(SVal, CV)]
interpreteds]
                                             where mkNotEq :: a -> SVal -> SVal -> SVal
mkNotEq k :: a
k a :: SVal
a b :: SVal
b
                                                    | a -> Bool
forall a. HasKind a => a -> Bool
isDouble a
k Bool -> Bool -> Bool
|| a -> Bool
forall a. HasKind a => a -> Bool
isFloat a
k = SVal -> SVal
svNot (SVal
a SVal -> SVal -> SVal
`fpNotEq` SVal
b)
                                                    | Bool
True                    = SVal
a SVal -> SVal -> SVal
`svNotEqual` SVal
b

                                                   fpNotEq :: SVal -> SVal -> SVal
fpNotEq a :: SVal
a b :: SVal
b = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
                                                       where r :: State -> IO SV
r st :: State
st = do SV
sva <- State -> SVal -> IO SV
svToSV State
st SVal
a
                                                                       SV
svb <- State -> SVal -> IO SV
svToSV State
st SVal
b
                                                                       State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KBool (Op -> [SV] -> SBVExpr
SBVApp (FPOp -> Op
IEEEFP FPOp
FP_ObjEqual) [SV
sva, SV
svb])

                                          -- For each uninterpreted constant, use equivalence class
                                          uninterpretedEqs :: [SVal]
                                          uninterpretedEqs :: [SVal]
uninterpretedEqs = ([SVal] -> [SVal]) -> [[SVal]] -> [SVal]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [SVal] -> [SVal]
pwDistinct         -- Assert that they are pairwise distinct
                                                           ([[SVal]] -> [SVal])
-> ([(SVal, CV)] -> [[SVal]]) -> [(SVal, CV)] -> [SVal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([SVal] -> Bool) -> [[SVal]] -> [[SVal]]
forall a. (a -> Bool) -> [a] -> [a]
filter (\l :: [SVal]
l -> [SVal] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [SVal]
l Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
> 1)  -- Only need this class if it has at least two members
                                                           ([[SVal]] -> [[SVal]])
-> ([(SVal, CV)] -> [[SVal]]) -> [(SVal, CV)] -> [[SVal]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(SVal, CV)] -> [SVal]) -> [[(SVal, CV)]] -> [[SVal]]
forall a b. (a -> b) -> [a] -> [b]
map (((SVal, CV) -> SVal) -> [(SVal, CV)] -> [SVal]
forall a b. (a -> b) -> [a] -> [b]
map (SVal, CV) -> SVal
forall a b. (a, b) -> a
fst)                -- throw away values, we only need svals
                                                           ([[(SVal, CV)]] -> [[SVal]])
-> ([(SVal, CV)] -> [[(SVal, CV)]]) -> [(SVal, CV)] -> [[SVal]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SVal, CV) -> (SVal, CV) -> Bool)
-> [(SVal, CV)] -> [[(SVal, CV)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (CV -> CV -> Bool
forall a. Eq a => a -> a -> Bool
(==) (CV -> CV -> Bool)
-> ((SVal, CV) -> CV) -> (SVal, CV) -> (SVal, CV) -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (SVal, CV) -> CV
forall a b. (a, b) -> b
snd)      -- make sure they belong to the same sort and have the same value
                                                           ([(SVal, CV)] -> [[(SVal, CV)]])
-> ([(SVal, CV)] -> [(SVal, CV)]) -> [(SVal, CV)] -> [[(SVal, CV)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SVal, CV) -> CV) -> [(SVal, CV)] -> [(SVal, CV)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (SVal, CV) -> CV
forall a b. (a, b) -> b
snd                   -- sort them according to their CV (i.e., sort/value)
                                                           ([(SVal, CV)] -> [SVal]) -> [(SVal, CV)] -> [SVal]
forall a b. (a -> b) -> a -> b
$ [(SVal, CV)]
uninterpreteds
                                            where pwDistinct :: [SVal] -> [SVal]
                                                  pwDistinct :: [SVal] -> [SVal]
pwDistinct ss :: [SVal]
ss = [SVal
x SVal -> SVal -> SVal
`svNotEqual` SVal
y | (x :: SVal
x:ys :: [SVal]
ys) <- [SVal] -> [[SVal]]
forall a. [a] -> [[a]]
tails [SVal]
ss, SVal
y <- [SVal]
ys]

                                          -- For each uninterpreted function, create a disqualifying equation
                                          -- We do this rather brute-force, since we need to create a new function
                                          -- and do an existential assertion.
                                          uninterpretedReject :: Maybe [String]
                                          uninterpretedFuns    :: [String]
                                          (uninterpretedReject :: Maybe [String]
uninterpretedReject, uninterpretedFuns :: [String]
uninterpretedFuns) = (Maybe [String]
uiReject, [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
defs)
                                              where uiReject :: Maybe [String]
uiReject = case [String]
rejects of
                                                                 []  -> Maybe [String]
forall a. Maybe a
Nothing
                                                                 xs :: [String]
xs  -> [String] -> Maybe [String]
forall a. a -> Maybe a
Just [String]
xs

                                                    (rejects :: [String]
rejects, defs :: [[String]]
defs) = [(String, [String])] -> ([String], [[String]])
forall a b. [(a, b)] -> ([a], [b])
unzip [(String, (SBVType, ([([CV], CV)], CV))) -> (String, [String])
mkNotEq (String, (SBVType, ([([CV], CV)], CV)))
ui | ui :: (String, (SBVType, ([([CV], CV)], CV)))
ui@(nm :: String
nm, _) <- [(String, (SBVType, ([([CV], CV)], CV)))]
uiFunVals, String
nm String -> t String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t String
uiFunsToReject]

                                                    -- Otherwise, we have things to refute, go for it:
                                                    mkNotEq :: (String, (SBVType, ([([CV], CV)], CV))) -> (String, [String])
mkNotEq (nm :: String
nm, (SBVType ts :: [Kind]
ts, vs :: ([([CV], CV)], CV)
vs)) = (String
reject, [String]
def [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
dif)
                                                      where nm' :: String
nm' = String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_model" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
cnt

                                                            reject :: String
reject = String
nm' String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_reject"

                                                            -- rounding mode doesn't matter here, just pick one
                                                            scv :: CV -> String
scv = RoundingMode -> CV -> String
cvToSMTLib RoundingMode
RoundNearestTiesToEven

                                                            (ats :: [Kind]
ats, rt :: Kind
rt) = ([Kind] -> [Kind]
forall a. [a] -> [a]
init [Kind]
ts, [Kind] -> Kind
forall a. [a] -> a
last [Kind]
ts)

                                                            args :: String
args = [String] -> String
unwords ["(x!" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")" | (t :: Kind
t, i :: Key
i) <- [Kind] -> [Key] -> [(Kind, Key)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Kind]
ats [(0::Int)..]]
                                                            res :: String
res  = Kind -> String
smtType Kind
rt

                                                            params :: [String]
params = ["x!" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
i | (_, i :: Key
i) <- [Kind] -> [Key] -> [(Kind, Key)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Kind]
ats [(0::Int)..]]

                                                            uparams :: String
uparams = [String] -> String
unwords [String]
params

                                                            chain :: ([([CV], CV)], CV) -> [String]
chain (vals :: [([CV], CV)]
vals, fallThru :: CV
fallThru) = [([CV], CV)] -> [String]
walk [([CV], CV)]
vals
                                                              where walk :: [([CV], CV)] -> [String]
walk []               = ["   " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
scv CV
fallThru String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> Char -> String
forall a. Key -> a -> [a]
replicate ([([CV], CV)] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [([CV], CV)]
vals) ')']
                                                                    walk ((as :: [CV]
as, r :: CV
r) : rest :: [([CV], CV)]
rest) = ("   (ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [CV] -> String
cond [CV]
as String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
scv CV
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ "") String -> [String] -> [String]
forall a. a -> [a] -> [a]
:  [([CV], CV)] -> [String]
walk [([CV], CV)]
rest

                                                                    cond :: [CV] -> String
cond as :: [CV]
as = "(and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((String -> CV -> String) -> [String] -> [CV] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith String -> CV -> String
eq [String]
params [CV]
as) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                                                                    eq :: String -> CV -> String
eq p :: String
p a :: CV
a  = "(= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
scv CV
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

                                                            def :: [String]
def =    ("(define-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm' String -> String -> String
forall a. [a] -> [a] -> [a]
++ " (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
res)
                                                                  String -> [String] -> [String]
forall a. a -> [a] -> [a]
:  ([([CV], CV)], CV) -> [String]
chain ([([CV], CV)], CV)
vs
                                                                  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [")"]

                                                            pad :: String
pad = Key -> Char -> String
forall a. Key -> a -> [a]
replicate (1 Key -> Key -> Key
forall a. Num a => a -> a -> a
+ String -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length String
nm' Key -> Key -> Key
forall a. Num a => a -> a -> a
- String -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length String
nm) ' '

                                                            dif :: [String]
dif = [ "(define-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++  String
reject String -> String -> String
forall a. [a] -> [a] -> [a]
++ " () Bool"
                                                                  , "   (exists (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                                                                  , "           (distinct (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
pad String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
uparams String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                                                                  , "                     (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm' String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
uparams String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))))"
                                                                  ]

                                          eqs :: [SVal]
eqs = [SVal]
interpretedEqs [SVal] -> [SVal] -> [SVal]
forall a. [a] -> [a] -> [a]
++ [SVal]
uninterpretedEqs

                                          disallow :: Maybe (SBV a)
disallow = case [SVal]
eqs of
                                                       [] -> Maybe (SBV a)
forall a. Maybe a
Nothing
                                                       _  -> SBV a -> Maybe (SBV a)
forall a. a -> Maybe a
Just (SBV a -> Maybe (SBV a)) -> SBV a -> Maybe (SBV a)
forall a b. (a -> b) -> a -> b
$ SVal -> SBV a
forall a. SVal -> SBV a
SBV (SVal -> SBV a) -> SVal -> SBV a
forall a b. (a -> b) -> a -> b
$ (SVal -> SVal -> SVal) -> [SVal] -> SVal
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 SVal -> SVal -> SVal
svOr [SVal]
eqs

                                      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SMTConfig -> Bool
allSatPrintAlong SMTConfig
cfg) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
                                        IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ "Solution #" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
cnt String -> String -> String
forall a. [a] -> [a] -> [a]
++ ":"
                                        IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SMTConfig -> SMTModel -> String
showModel SMTConfig
cfg SMTModel
model

                                      let resultsSoFar :: [SMTResult]
resultsSoFar = SMTResult
m SMTResult -> [SMTResult] -> [SMTResult]
forall a. a -> [a] -> [a]
: [SMTResult]
sofar

                                          -- This is clunky, but let's not generate a rejector unless we really need it
                                          needMoreIterations :: Bool
needMoreIterations
                                                | Just maxModels :: Key
maxModels <- SMTConfig -> Maybe Key
allSatMaxModelCount SMTConfig
cfg, (Key
cntKey -> Key -> Key
forall a. Num a => a -> a -> a
+1) Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
> Key
maxModels = Bool
False
                                                | Bool
True                                                           = Bool
True

                                      -- Send function disequalities, if any:
                                      if Bool -> Bool
not Bool
needMoreIterations
                                         then Key -> [SMTResult] -> m (Bool, Bool, [SMTResult])
go (Key
cntKey -> Key -> Key
forall a. Num a => a -> a -> a
+1) [SMTResult]
resultsSoFar
                                         else do let uiFunRejector :: String
uiFunRejector   = "uiFunRejector_model_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
cnt
                                                     header :: String
header          = "define-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
uiFunRejector String -> String -> String
forall a. [a] -> [a] -> [a]
++ " () Bool "

                                                     defineRejector :: [String] -> m ()
defineRejector []     = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                                                     defineRejector [x :: 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 -> String -> String
forall a. [a] -> [a] -> [a]
++ String
header String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                                                     defineRejector (x :: String
x:xs :: [String]
xs) = (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]
mergeSExpr ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$  ("(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
header)
                                                                                                            String -> [String] -> [String]
forall a. a -> [a] -> [a]
:  ("        (or " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x)
                                                                                                            String -> [String] -> [String]
forall a. a -> [a] -> [a]
:  ["            " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
e | String
e <- [String]
xs]
                                                                                                            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["        ))"]
                                                 Maybe String
rejectFuncs <- case Maybe [String]
uninterpretedReject of
                                                                  Nothing -> Maybe String -> m (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing
                                                                  Just fs :: [String]
fs -> do (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]
mergeSExpr [String]
uninterpretedFuns
                                                                                [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
defineRejector [String]
fs
                                                                                Maybe String -> m (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> m (Maybe String))
-> Maybe String -> m (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
uiFunRejector

                                                 -- send the disallow clause and the uninterpreted rejector:
                                                 case (Maybe SBool
forall a. Maybe (SBV a)
disallow, Maybe String
rejectFuncs) of
                                                    (Nothing, Nothing) -> (Bool, Bool, [SMTResult]) -> m (Bool, Bool, [SMTResult])
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool
False, Bool
False, [SMTResult]
resultsSoFar)
                                                    (Just d :: SBool
d,  Nothing) -> do SBool -> m ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain SBool
d
                                                                             Key -> [SMTResult] -> m (Bool, Bool, [SMTResult])
go (Key
cntKey -> Key -> Key
forall a. Num a => a -> a -> a
+1) [SMTResult]
resultsSoFar
                                                    (Nothing, Just f :: String
f)  -> 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
$ "(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                                                                             Key -> [SMTResult] -> m (Bool, Bool, [SMTResult])
go (Key
cntKey -> Key -> Key
forall a. Num a => a -> a -> a
+1) [SMTResult]
resultsSoFar
                                                    (Just d :: SBool
d,  Just f :: String
f)  -> -- This is where it gets ugly. We have an SBV and a string and we need to "or" them.
                                                                          -- But we need a way to force 'd' to be produced. So, go ahead and force it:
                                                                          do SBool -> m ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> m ()) -> SBool -> m ()
forall a b. (a -> b) -> a -> b
$ SBool
d SBool -> SBool -> SBool
.=> SBool
d  -- NB: Redundant, but it makes sure the corresponding constraint gets shown
                                                                             SV
svd <- IO SV -> m SV
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO SV -> m SV) -> IO SV -> m SV
forall a b. (a -> b) -> a -> b
$ State -> SVal -> IO SV
svToSV State
topState (SBool -> SVal
forall a. SBV a -> SVal
unSBV SBool
d)
                                                                             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
$ "(assert (or " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
svd String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))"
                                                                             Key -> [SMTResult] -> m (Bool, Bool, [SMTResult])
go (Key
cntKey -> Key -> Key
forall a. Num a => a -> a -> a
+1) [SMTResult]
resultsSoFar

-- | Generalization of 'Data.SBV.Control.getUnsatAssumptions'
getUnsatAssumptions :: (MonadIO m, MonadQuery m) => [String] -> [(String, a)] -> m [a]
getUnsatAssumptions :: [String] -> [(String, a)] -> m [a]
getUnsatAssumptions originals :: [String]
originals proxyMap :: [(String, a)]
proxyMap = do
        let cmd :: String
cmd = "(get-unsat-assumptions)"

            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 "getUnsatAssumptions" String
cmd "a list of unsatisfiable assumptions"
                           (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 [ "Make sure you use:"
                                  , ""
                                  , "       setOption $ ProduceUnsatAssumptions True"
                                  , ""
                                  , "to make sure the solver is ready for producing unsat assumptions,"
                                  , "and that there is a model by first issuing a 'checkSat' call."
                                  ]

            fromECon :: SExpr -> Maybe String
fromECon (ECon s :: String
s) = String -> Maybe String
forall a. a -> Maybe a
Just String
s
            fromECon _        = Maybe String
forall a. Maybe a
Nothing

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

        -- If unsat-cores are enabled, z3 might end-up printing an assumption that wasn't
        -- in the original list of assumptions for `check-sat-assuming`. So, we walk over
        -- and ignore those that weren't in the original list, and put a warning for those
        -- we couldn't find.
        let walk :: [String] -> [a] -> m [a]
walk []     sofar :: [a]
sofar = [a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ([a] -> m [a]) -> [a] -> m [a]
forall a b. (a -> b) -> a -> b
$ [a] -> [a]
forall a. [a] -> [a]
reverse [a]
sofar
            walk (a :: String
a:as :: [String]
as) sofar :: [a]
sofar = case String
a String -> [(String, a)] -> Maybe a
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(String, a)]
proxyMap of
                                  Just v :: a
v  -> [String] -> [a] -> m [a]
walk [String]
as (a
va -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
sofar)
                                  Nothing -> do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [ "*** In call to 'getUnsatAssumptions'"
                                                           , "***"
                                                           , "***    Unexpected assumption named: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
a
                                                           , "***    Was expecting one of       : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
originals
                                                           , "***"
                                                           , "*** This can happen if unsat-cores are also enabled. Ignoring."
                                                           ]
                                                [String] -> [a] -> m [a]
walk [String]
as [a]
sofar

        String
-> (String -> Maybe [String] -> m [a]) -> (SExpr -> m [a]) -> m [a]
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m [a]
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m [a]) -> m [a]) -> (SExpr -> m [a]) -> m [a]
forall a b. (a -> b) -> a -> b
$ \case
           EApp es :: [SExpr]
es | Just xs :: [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] -> [a] -> m [a]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
[String] -> [a] -> m [a]
walk [String]
xs []
           _                                     -> String -> Maybe [String] -> m [a]
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing

-- | Generalization of 'Data.SBV.Control.timeout'
timeout :: (MonadIO m, MonadQuery m) => Int -> m a -> m a
timeout :: Key -> m a -> m a
timeout n :: Key
n q :: m a
q = do (QueryState -> QueryState) -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(QueryState -> QueryState) -> m ()
modifyQueryState (\qs :: QueryState
qs -> QueryState
qs {queryTimeOutValue :: Maybe Key
queryTimeOutValue = Key -> Maybe Key
forall a. a -> Maybe a
Just Key
n})
                 a
r <- m a
q
                 (QueryState -> QueryState) -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(QueryState -> QueryState) -> m ()
modifyQueryState (\qs :: QueryState
qs -> QueryState
qs {queryTimeOutValue :: Maybe Key
queryTimeOutValue = Maybe Key
forall a. Maybe a
Nothing})
                 a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r

-- | Bail out if a parse goes bad
parse :: String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse :: String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse r :: String
r fCont :: String -> Maybe [String] -> a
fCont sCont :: SExpr -> a
sCont = case String -> Either String SExpr
parseSExpr String
r of
                        Left  e :: String
e   -> String -> Maybe [String] -> a
fCont String
r ([String] -> Maybe [String]
forall a. a -> Maybe a
Just [String
e])
                        Right res :: SExpr
res -> SExpr -> a
sCont SExpr
res

-- | Generalization of 'Data.SBV.Control.unexpected'
unexpected :: (MonadIO m, MonadQuery m) => String -> String -> String -> Maybe [String] -> String -> Maybe [String] -> m a
unexpected :: String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected ctx :: String
ctx sent :: String
sent expected :: String
expected mbHint :: Maybe [String]
mbHint received :: String
received mbReason :: Maybe [String]
mbReason = do
        -- empty the response channel first
        [String]
extras <- String -> Maybe Key -> m [String]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> Maybe Key -> m [String]
retrieveResponse "terminating upon unexpected response" (Key -> Maybe Key
forall a. a -> Maybe a
Just 5000000)

        SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig

        let exc :: SBVException
exc = SBVException :: String
-> Maybe String
-> Maybe String
-> Maybe String
-> Maybe String
-> Maybe String
-> Maybe ExitCode
-> SMTConfig
-> Maybe [String]
-> Maybe [String]
-> SBVException
SBVException { sbvExceptionDescription :: String
sbvExceptionDescription = "Unexpected response from the solver, context: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ctx
                               , sbvExceptionSent :: Maybe String
sbvExceptionSent        = String -> Maybe String
forall a. a -> Maybe a
Just String
sent
                               , sbvExceptionExpected :: Maybe String
sbvExceptionExpected    = String -> Maybe String
forall a. a -> Maybe a
Just String
expected
                               , sbvExceptionReceived :: Maybe String
sbvExceptionReceived    = String -> Maybe String
forall a. a -> Maybe a
Just String
received
                               , sbvExceptionStdOut :: Maybe String
sbvExceptionStdOut      = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String]
extras
                               , sbvExceptionStdErr :: Maybe String
sbvExceptionStdErr      = Maybe String
forall a. Maybe a
Nothing
                               , sbvExceptionExitCode :: Maybe ExitCode
sbvExceptionExitCode    = Maybe ExitCode
forall a. Maybe a
Nothing
                               , sbvExceptionConfig :: SMTConfig
sbvExceptionConfig      = SMTConfig
cfg
                               , sbvExceptionReason :: Maybe [String]
sbvExceptionReason      = Maybe [String]
mbReason
                               , sbvExceptionHint :: Maybe [String]
sbvExceptionHint        = Maybe [String]
mbHint
                               }

        IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO a -> m a) -> IO a -> m a
forall a b. (a -> b) -> a -> b
$ SBVException -> IO a
forall e a. Exception e => e -> IO a
C.throwIO SBVException
exc

-- | Convert a query result to an SMT Problem
runProofOn :: SBVRunMode -> QueryContext -> [String] -> Result -> SMTProblem
runProofOn :: SBVRunMode -> QueryContext -> [String] -> Result -> SMTProblem
runProofOn rm :: SBVRunMode
rm context :: QueryContext
context comments :: [String]
comments res :: Result
res@(Result ki :: KindSet
ki _qcInfo :: [(String, CV)]
_qcInfo _observables :: [(String, CV -> Bool, SV)]
_observables _codeSegs :: [(String, [String])]
_codeSegs is :: ([(Quantifier, NamedSymVar)], [NamedSymVar])
is consts :: [(SV, CV)]
consts tbls :: [((Key, Kind, Kind), [SV])]
tbls arrs :: [(Key, ArrayInfo)]
arrs uis :: [(String, SBVType)]
uis axs :: [(String, [String])]
axs pgm :: SBVPgm
pgm cstrs :: Seq (Bool, [(String, String)], SV)
cstrs _assertions :: [(String, Maybe CallStack, SV)]
_assertions outputs :: [SV]
outputs) =
     let (config :: SMTConfig
config, isSat :: Bool
isSat, isSafe :: Bool
isSafe, isSetup :: Bool
isSetup) = case SBVRunMode
rm of
                                              SMTMode _ stage :: IStage
stage s :: Bool
s c :: SMTConfig
c -> (SMTConfig
c, Bool
s, IStage -> Bool
isSafetyCheckingIStage IStage
stage, IStage -> Bool
isSetupIStage IStage
stage)
                                              _                   -> String -> (SMTConfig, Bool, Bool, Bool)
forall a. HasCallStack => String -> a
error (String -> (SMTConfig, Bool, Bool, Bool))
-> String -> (SMTConfig, Bool, Bool, Bool)
forall a b. (a -> b) -> a -> b
$ "runProofOn: Unexpected run mode: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVRunMode -> String
forall a. Show a => a -> String
show SBVRunMode
rm

         flipQ :: (Quantifier, b) -> (Quantifier, b)
flipQ (ALL, x :: b
x) = (Quantifier
EX,  b
x)
         flipQ (EX,  x :: b
x) = (Quantifier
ALL, b
x)

         skolemize :: [(Quantifier, NamedSymVar)] -> [Either SV (SV, [SV])]
         skolemize :: [(Quantifier, NamedSymVar)] -> [Either SV (SV, [SV])]
skolemize quants :: [(Quantifier, NamedSymVar)]
quants = [(Quantifier, NamedSymVar)]
-> ([SV], [Either SV (SV, [SV])]) -> [Either SV (SV, [SV])]
forall a b.
[(Quantifier, (a, b))]
-> ([a], [Either a (a, [a])]) -> [Either a (a, [a])]
go [(Quantifier, NamedSymVar)]
quants ([], [])
           where go :: [(Quantifier, (a, b))]
-> ([a], [Either a (a, [a])]) -> [Either a (a, [a])]
go []                   (_,  sofar :: [Either a (a, [a])]
sofar) = [Either a (a, [a])] -> [Either a (a, [a])]
forall a. [a] -> [a]
reverse [Either a (a, [a])]
sofar
                 go ((ALL, (v :: a
v, _)):rest :: [(Quantifier, (a, b))]
rest) (us :: [a]
us, sofar :: [Either a (a, [a])]
sofar) = [(Quantifier, (a, b))]
-> ([a], [Either a (a, [a])]) -> [Either a (a, [a])]
go [(Quantifier, (a, b))]
rest (a
va -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
us, a -> Either a (a, [a])
forall a b. a -> Either a b
Left a
v Either a (a, [a]) -> [Either a (a, [a])] -> [Either a (a, [a])]
forall a. a -> [a] -> [a]
: [Either a (a, [a])]
sofar)
                 go ((EX,  (v :: a
v, _)):rest :: [(Quantifier, (a, b))]
rest) (us :: [a]
us, sofar :: [Either a (a, [a])]
sofar) = [(Quantifier, (a, b))]
-> ([a], [Either a (a, [a])]) -> [Either a (a, [a])]
go [(Quantifier, (a, b))]
rest ([a]
us,   (a, [a]) -> Either a (a, [a])
forall a b. b -> Either a b
Right (a
v, [a] -> [a]
forall a. [a] -> [a]
reverse [a]
us) Either a (a, [a]) -> [Either a (a, [a])] -> [Either a (a, [a])]
forall a. a -> [a] -> [a]
: [Either a (a, [a])]
sofar)

         qinps :: [(Quantifier, NamedSymVar)]
qinps      = if Bool
isSat then ([(Quantifier, NamedSymVar)], [NamedSymVar])
-> [(Quantifier, NamedSymVar)]
forall a b. (a, b) -> a
fst ([(Quantifier, NamedSymVar)], [NamedSymVar])
is else ((Quantifier, NamedSymVar) -> (Quantifier, NamedSymVar))
-> [(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
forall a b. (a -> b) -> [a] -> [b]
map (Quantifier, NamedSymVar) -> (Quantifier, NamedSymVar)
forall b. (Quantifier, b) -> (Quantifier, b)
flipQ (([(Quantifier, NamedSymVar)], [NamedSymVar])
-> [(Quantifier, NamedSymVar)]
forall a b. (a, b) -> a
fst ([(Quantifier, NamedSymVar)], [NamedSymVar])
is)
         skolemMap :: [Either SV (SV, [SV])]
skolemMap  = [(Quantifier, NamedSymVar)] -> [Either SV (SV, [SV])]
skolemize [(Quantifier, NamedSymVar)]
qinps

         o :: SV
o | Bool
isSafe = SV
trueSV
           | Bool
True   = case [SV]
outputs of
                        []  | Bool
isSetup -> SV
trueSV
                        [so :: SV
so]          -> case SV
so of
                                           SV KBool _ -> SV
so
                                           _          -> String -> SV
forall a. HasCallStack => String -> a
error (String -> SV) -> String -> SV
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ "Impossible happened, non-boolean output: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
so
                                                                         , "Detected while generating the trace:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Result -> String
forall a. Show a => a -> String
show Result
res
                                                                         ]
                        os :: [SV]
os  -> String -> SV
forall a. HasCallStack => String -> a
error (String -> SV) -> String -> SV
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ "User error: Multiple output values detected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SV] -> String
forall a. Show a => a -> String
show [SV]
os
                                               , "Detected while generating the trace:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Result -> String
forall a. Show a => a -> String
show Result
res
                                               , "*** Check calls to \"output\", they are typically not needed!"
                                               ]

     in SMTProblem :: (SMTConfig -> SMTLibPgm) -> SMTProblem
SMTProblem { smtLibPgm :: SMTConfig -> SMTLibPgm
smtLibPgm = SMTConfig -> SMTLibConverter SMTLibPgm
toSMTLib SMTConfig
config QueryContext
context KindSet
ki Bool
isSat [String]
comments ([(Quantifier, NamedSymVar)], [NamedSymVar])
is [Either SV (SV, [SV])]
skolemMap [(SV, CV)]
consts [((Key, Kind, Kind), [SV])]
tbls [(Key, ArrayInfo)]
arrs [(String, SBVType)]
uis [(String, [String])]
axs SBVPgm
pgm Seq (Bool, [(String, String)], SV)
cstrs SV
o }

-- | Generalization of 'Data.SBV.Control.executeQuery'
executeQuery :: forall m a. ExtractIO m => QueryContext -> QueryT m a -> SymbolicT m a
executeQuery :: QueryContext -> QueryT m a -> SymbolicT m a
executeQuery queryContext :: QueryContext
queryContext (QueryT userQuery :: ReaderT State m a
userQuery) = do
     State
st <- SymbolicT m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv
     SBVRunMode
rm <- IO SBVRunMode -> SymbolicT m SBVRunMode
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SBVRunMode -> SymbolicT m SBVRunMode)
-> IO SBVRunMode -> SymbolicT m SBVRunMode
forall a b. (a -> b) -> a -> b
$ IORef SBVRunMode -> IO SBVRunMode
forall a. IORef a -> IO a
readIORef (State -> IORef SBVRunMode
runMode State
st)

     -- Make sure the phases match:
     () <- IO () -> SymbolicT m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> SymbolicT m ()) -> IO () -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ case (QueryContext
queryContext, SBVRunMode
rm) of
                      (QueryInternal, _)                                -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- no worries, internal
                      (QueryExternal, SMTMode QueryExternal ISetup _ _) -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return () -- legitimate runSMT call
                      _                                                 -> SBVRunMode -> IO ()
forall a a. Show a => a -> a
invalidQuery SBVRunMode
rm

     -- If we're doing an external query, then we cannot allow quantifiers to be present. Why?
     -- Consider:
     --
     --      issue = do x :: SBool <- forall_
     --                 y :: SBool <- exists_
     --                 constrain y
     --                 query $ do checkSat
     --                         (,) <$> getValue x <*> getValue y
     --
     -- This is the (simplified/annotated SMTLib we would generate:)
     --
     --     (declare-fun s1 (Bool) Bool)   ; s1 is the function that corresponds to the skolemized 'y'
     --     (assert (forall ((s0 Bool))    ; s0 is 'x'
     --                 (s1 s0)))          ; s1 applied to s0 is the actual 'y'
     --     (check-sat)
     --     (get-value (s0))        ; s0 simply not visible here
     --     (get-value (s1))        ; s1 is visible, but only via 's1 s0', so it is also not available.
     --
     -- And that would be terrible! The scoping rules of our "quantified" variables and how they map to
     -- SMTLib is just not compatible. This is a historical design issue, but too late at this point. (We
     -- should've never allowed general quantification like this, but only in limited contexts.)
     --
     -- So, we check if this is an external-query, and if there are quantified variables. If so, we
     -- cowardly refuse to continue. For details, see: <http://github.com/LeventErkok/sbv/issues/407>
     --
     -- However, as discussed in <https://github.com/LeventErkok/sbv/issues/459>, we'll allow for this
     -- if the user explicitly asks as to do so. In that case, all bets are off!

     let allowQQs :: Bool
allowQQs = case SBVRunMode
rm of
                      SMTMode _ _ _ cfg :: SMTConfig
cfg -> SMTConfig -> Bool
allowQuantifiedQueries SMTConfig
cfg
                      CodeGen           -> Bool
False -- doesn't matter in these two
                      Concrete{}        -> Bool
False -- cases, but we're being careful

     () <- Bool -> SymbolicT m () -> SymbolicT m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
allowQQs (SymbolicT m () -> SymbolicT m ())
-> SymbolicT m () -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ IO () -> SymbolicT m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> SymbolicT m ()) -> IO () -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$
                    case QueryContext
queryContext of
                      QueryInternal -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()         -- we're good, internal usages don't mess with scopes
                      QueryExternal -> do
                        ((userInps :: [(Quantifier, NamedSymVar)]
userInps, _), _) <- IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
-> IO (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
forall a. IORef a -> IO a
readIORef (State
-> IORef (([(Quantifier, NamedSymVar)], [NamedSymVar]), Set String)
rinps State
st)
                        let badInps :: [String]
badInps = [String] -> [String]
forall a. [a] -> [a]
reverse [String
n | (ALL, (_, n :: String
n)) <- [(Quantifier, NamedSymVar)]
userInps]
                        case [String]
badInps of
                          [] -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                          _  -> let plu :: String
plu | [String] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [String]
badInps Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
> 1 = "s require"
                                        | Bool
True               = " requires"
                                in String -> IO ()
forall a. HasCallStack => String -> a
error (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ ""
                                                   , "*** Data.SBV: Unsupported query call in the presence of quantified inputs."
                                                   , "***"
                                                   , "*** The following variable" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
plu String -> String -> String
forall a. [a] -> [a] -> [a]
++ " explicit quantification: "
                                                   , "***"
                                                   , "***    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " [String]
badInps
                                                   , "***"
                                                   , "*** While quantification and queries can co-exist in principle, SBV currently"
                                                   , "*** does not support this scenario. Avoid using quantifiers with user queries"
                                                   , "*** if possible. Please do get in touch if your use case does require such"
                                                   , "*** a feature to see how we can accommodate such scenarios."
                                                   ]

     case SBVRunMode
rm of
        -- Transitioning from setup
        SMTMode qc :: QueryContext
qc stage :: IStage
stage isSAT :: Bool
isSAT cfg :: SMTConfig
cfg | Bool -> Bool
not (IStage -> Bool
isRunIStage IStage
stage) -> do

                                                let backend :: SMTConfig -> State -> String -> (State -> IO res) -> IO res
backend = SMTSolver
-> forall res.
   SMTConfig -> State -> String -> (State -> IO res) -> IO res
engine (SMTConfig -> SMTSolver
solver SMTConfig
cfg)

                                                Result
res     <- IO Result -> SymbolicT m Result
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Result -> SymbolicT m Result)
-> IO Result -> SymbolicT m Result
forall a b. (a -> b) -> a -> b
$ State -> IO Result
extractSymbolicSimulationState State
st
                                                [SMTOption]
setOpts <- IO [SMTOption] -> SymbolicT m [SMTOption]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [SMTOption] -> SymbolicT m [SMTOption])
-> IO [SMTOption] -> SymbolicT m [SMTOption]
forall a b. (a -> b) -> a -> b
$ [SMTOption] -> [SMTOption]
forall a. [a] -> [a]
reverse ([SMTOption] -> [SMTOption]) -> IO [SMTOption] -> IO [SMTOption]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef [SMTOption] -> IO [SMTOption]
forall a. IORef a -> IO a
readIORef (State -> IORef [SMTOption]
rSMTOptions State
st)

                                                let SMTProblem{SMTConfig -> SMTLibPgm
smtLibPgm :: SMTConfig -> SMTLibPgm
smtLibPgm :: SMTProblem -> SMTConfig -> SMTLibPgm
smtLibPgm} = SBVRunMode -> QueryContext -> [String] -> Result -> SMTProblem
runProofOn SBVRunMode
rm QueryContext
queryContext [] Result
res
                                                    cfg' :: SMTConfig
cfg' = SMTConfig
cfg { solverSetOptions :: [SMTOption]
solverSetOptions = SMTConfig -> [SMTOption]
solverSetOptions SMTConfig
cfg [SMTOption] -> [SMTOption] -> [SMTOption]
forall a. [a] -> [a] -> [a]
++ [SMTOption]
setOpts }
                                                    pgm :: SMTLibPgm
pgm  = SMTConfig -> SMTLibPgm
smtLibPgm SMTConfig
cfg'

                                                IO () -> SymbolicT m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> SymbolicT m ()) -> IO () -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ IORef SBVRunMode -> SBVRunMode -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (State -> IORef SBVRunMode
runMode State
st) (SBVRunMode -> IO ()) -> SBVRunMode -> IO ()
forall a b. (a -> b) -> a -> b
$ QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
SMTMode QueryContext
qc IStage
IRun Bool
isSAT SMTConfig
cfg

                                                m a -> SymbolicT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> SymbolicT m a) -> m a -> SymbolicT m a
forall a b. (a -> b) -> a -> b
$ m (m a) -> m a
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (m (m a) -> m a) -> m (m a) -> m a
forall a b. (a -> b) -> a -> b
$ IO (m a) -> m (m a)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (m a) -> m (m a)) -> IO (m a) -> m (m a)
forall a b. (a -> b) -> a -> b
$ SMTConfig -> State -> String -> (State -> IO (m a)) -> IO (m a)
forall res.
SMTConfig -> State -> String -> (State -> IO res) -> IO res
backend SMTConfig
cfg' State
st (SMTLibPgm -> String
forall a. Show a => a -> String
show SMTLibPgm
pgm) ((State -> IO (m a)) -> IO (m a))
-> (State -> IO (m a)) -> IO (m a)
forall a b. (a -> b) -> a -> b
$ m a -> IO (m a)
forall (m :: * -> *) a. ExtractIO m => m a -> IO (m a)
extractIO (m a -> IO (m a)) -> (State -> m a) -> State -> IO (m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReaderT State m a -> State -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT State m a
userQuery

        -- Already in a query, in theory we can just continue, but that causes use-case issues
        -- so we reject it. TODO: Review if we should actually support this. The issue arises with
        -- expressions like this:
        --
        -- In the following t0's output doesn't get recorded, as the output call is too late when we get
        -- here. (The output field isn't "incremental.") So, t0/t1 behave differently!
        --
        --   t0 = satWith z3{verbose=True, transcript=Just "t.smt2"} $ query (return (false::SBool))
        --   t1 = satWith z3{verbose=True, transcript=Just "t.smt2"} $ ((return (false::SBool)) :: Predicate)
        --
        -- Also, not at all clear what it means to go in an out of query mode:
        --
        -- r = runSMTWith z3{verbose=True} $ do
        --         a' <- sInteger "a"
        --
        --        (a, av) <- query $ do _ <- checkSat
        --                              av <- getValue a'
        --                              return (a', av)
        --
        --        liftIO $ putStrLn $ "Got: " ++ show av
        --        -- constrain $ a .> literal av + 1      -- Cant' do this since we're "out" of query. Sigh.
        --
        --        bv <- query $ do constrain $ a .> literal av + 1
        --                         _ <- checkSat
        --                         getValue a
        --
        --        return $ a' .== a' + 1
        --
        -- This would be one possible implementation, alas it has the problems above:
        --
        --    SMTMode IRun _ _ -> liftIO $ evalStateT userQuery st
        --
        -- So, we just reject it.

        SMTMode _ IRun _ _ -> String -> SymbolicT m a
forall a. HasCallStack => String -> a
error (String -> SymbolicT m a) -> String -> SymbolicT m a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ ""
                                              , "*** Data.SBV: Unsupported nested query is detected."
                                              , "***"
                                              , "*** Please group your queries into one block. Note that this"
                                              , "*** can also arise if you have a call to 'query' not within 'runSMT'"
                                              , "*** For instance, within 'sat'/'prove' calls with custom user queries."
                                              , "*** The solution is to do the sat/prove part in the query directly."
                                              , "***"
                                              , "*** While multiple/nested queries should not be necessary in general,"
                                              , "*** please do get in touch if your use case does require such a feature,"
                                              , "*** to see how we can accommodate such scenarios."
                                              ]

        -- Otherwise choke!
        _ -> SBVRunMode -> SymbolicT m a
forall a a. Show a => a -> a
invalidQuery SBVRunMode
rm

  where invalidQuery :: a -> a
invalidQuery rm :: a
rm = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ ""
                                          , "*** Data.SBV: Invalid query call."
                                          , "***"
                                          , "***   Current mode: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
rm
                                          , "***"
                                          , "*** Query calls are only valid within runSMT/runSMTWith calls"
                                          ]

{-# ANN module          ("HLint: ignore Reduce duplication" :: String) #-}
{-# ANN getAllSatResult ("HLint: ignore Use forM_"          :: String) #-}