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

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

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

module Data.SBV.Control.Utils (
       io
     , ask, send, getValue, getFunction, getUninterpretedValue
     , getValueCV, getUICVal, getUIFunCVAssoc, getUnsatAssumptions
     , 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.List  (sortBy, sortOn, elemIndex, partition, groupBy, tails, intercalate, nub, sort)

import Data.Char      (isPunctuation, isSpace, isDigit)
import Data.Function  (on)
import Data.Bifunctor (first)

import Data.Proxy

import qualified Data.Foldable      as F (toList)
import qualified Data.Map.Strict    as Map
import qualified Data.IntMap.Strict as IMap
import qualified Data.Sequence      as S
import qualified Data.Text          as T

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

import Data.Maybe (isNothing, isJust)

import Data.IORef (readIORef, writeIORef, IORef, newIORef, modifyIORef')

import Data.Time (getZonedTime)
import Data.Ratio

import Data.SBV.Core.Data     ( SV(..), trueSV, falseSV, CV(..), trueCV, falseCV, SBV, 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(..), VarContext(..)
                              , registerLabel, svMkSymVar, validationRequested
                              , isSafetyCheckingIStage, isSetupIStage, isRunIStage, IStage(..), QueryT(..)
                              , extractSymbolicSimulationState, MonadSymbolic(..), newUninterpreted
                              , UserInputs, getInputs, prefixExistentials, getSV, quantifier, getUserName
                              , namedSymVar, NamedSymVar(..), lookupInput, userInputs, userInputsToList
                              , getUserName', Name, CnstMap
                              )

import Data.SBV.Core.AlgReals    (mergeAlgReals, AlgReal(..), RealPoint(..))
import Data.SBV.Core.SizedFloats (fpZero, fpFromInteger, fpFromFloat, fpFromDouble)
import Data.SBV.Core.Kind        (smtType, hasUninterpretedSorts)
import Data.SBV.Core.Operations  (svNot, svNotEqual, svOr, svEqual)

import Data.SBV.SMT.SMT     (showModel, parseCVs, SatModel, AllSatResult(..))
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)
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)

import qualified Control.Exception as C

import GHC.Stack

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

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

   addSMTDefinition :: String -> [String] -> QueryT m ()
addSMTDefinition String
nm [String]
_ = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                           , String
"*** Data.SBV: '" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
nm forall a. [a] -> [a] -> [a]
++ String
"' must be defined in regular (non-query) mode."
                                           , String
"*** Hint: Define all functions before starting the query."
                                           ]

-- | 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 :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> [(String, String)] -> SBool -> m ()
addQueryConstraint Bool
isSoft [(String, String)]
atts SBool
b = do SV
sv <- forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext (\State
st -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ do forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> State -> String -> IO ()
registerLabel String
"Constraint" State
st) [String
nm | (String
":named", String
nm) <- [(String, String)]
atts]
                                                                             forall a. State -> SBV a -> IO SV
sbvToSV State
st SBool
b)

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

addQueryAxiom :: (MonadIO m, MonadQuery m) => String -> [String] -> m ()
addQueryAxiom :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> [String] -> m ()
addQueryAxiom String
nm [String]
ls = do forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True forall a b. (a -> b) -> a -> b
$ String
"; -- user given axiom: " forall a. [a] -> [a] -> [a]
++ String
nm
                         forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String]
ls

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

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

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

-- | Get the assertions put in via 'Data.SBV.sAssert'
getSBVAssertions :: (MonadIO m, MonadQuery m) => m [(String, Maybe CallStack, SV)]
getSBVAssertions :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
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} <- forall (m :: * -> *). MonadQuery m => m State
queryState
                      forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 :: forall (m :: * -> *) a. MonadIO m => IO a -> m a
io = 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) => IORef CnstMap -> IncState -> m ()
syncUpSolver :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
IORef CnstMap -> IncState -> m ()
syncUpSolver IORef CnstMap
rGlobalConsts IncState
is = do
        SMTConfig
cfg <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig

        -- update global consts to have the new ones
        (CnstMap
newConsts, CnstMap
allConsts) <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ do CnstMap
nc <- forall a. IORef a -> IO a
readIORef (IncState -> IORef CnstMap
rNewConsts IncState
is)
                                              CnstMap
oc <- forall a. IORef a -> IO a
readIORef IORef CnstMap
rGlobalConsts
                                              let allConsts :: CnstMap
allConsts = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union CnstMap
nc CnstMap
oc
                                              forall a. IORef a -> a -> IO ()
writeIORef IORef CnstMap
rGlobalConsts CnstMap
allConsts
                                              forall (f :: * -> *) a. Applicative f => a -> f a
pure (CnstMap
nc, CnstMap
allConsts)

        [String]
ls  <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ do let swap :: (b, a) -> (a, b)
swap  (b
a, a
b)        = (a
b, b
a)
                           cmp :: (a, b) -> (a, b) -> Ordering
cmp   (a
a, b
_) (a
b, b
_) = a
a forall a. Ord a => a -> a -> Ordering
`compare` a
b
                           arrange :: (a, (b, c, b)) -> ((a, b, c), b)
arrange (a
i, (b
at, c
rt, b
es)) = ((a
i, b
at, c
rt), b
es)
                       [NamedSymVar]
inps        <- forall a. [a] -> [a]
reverse forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. IORef a -> IO a
readIORef (IncState -> IORef [NamedSymVar]
rNewInps IncState
is)
                       KindSet
ks          <- forall a. IORef a -> IO a
readIORef (IncState -> IORef KindSet
rNewKinds IncState
is)
                       [(Int, ArrayInfo)]
arrs        <- forall a. IntMap a -> [(Int, a)]
IMap.toAscList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. IORef a -> IO a
readIORef (IncState -> IORef ArrayMap
rNewArrs IncState
is)
                       [((Int, Kind, Kind), [SV])]
tbls        <- forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c} {b}. (a, (b, c, b)) -> ((a, b, c), b)
arrange forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy forall {a} {b} {b}. Ord a => (a, b) -> (a, b) -> Ordering
cmp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {b} {a}. (b, a) -> (a, b)
swap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
Map.toList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. IORef a -> IO a
readIORef (IncState -> IORef (Map (Kind, Kind, [SV]) Int)
rNewTbls IncState
is)
                       [(String, SBVType)]
uis         <- forall k a. Map k a -> [(k, a)]
Map.toAscList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. IORef a -> IO a
readIORef (IncState -> IORef UIMap
rNewUIs IncState
is)
                       SBVPgm
as          <- forall a. IORef a -> IO a
readIORef (IncState -> IORef SBVPgm
rNewAsgns IncState
is)
                       Seq (Bool, [(String, String)], SV)
constraints <- forall a. IORef a -> IO a
readIORef (IncState -> IORef (Seq (Bool, [(String, String)], SV))
rNewConstraints IncState
is)

                       let cnsts :: [(SV, CV)]
cnsts = forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy forall {a} {b} {b}. Ord a => (a, b) -> (a, b) -> Ordering
cmp forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {b} {a}. (b, a) -> (a, b)
swap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [(k, a)]
Map.toList forall a b. (a -> b) -> a -> b
$ CnstMap
newConsts

                       forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SMTConfig -> SMTLibIncConverter [String]
toIncSMTLib SMTConfig
cfg [NamedSymVar]
inps KindSet
ks (CnstMap
allConsts, [(SV, CV)]
cnsts) [(Int, ArrayInfo)]
arrs [((Int, Kind, Kind), [SV])]
tbls [(String, SBVType)]
uis SBVPgm
as Seq (Bool, [(String, String)], SV)
constraints SMTConfig
cfg
        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True) forall a b. (a -> b) -> a -> b
$ [String] -> [String]
mergeSExpr [String]
ls

-- | Retrieve the query context
getQueryState :: (MonadIO m, MonadQuery m) => m QueryState
getQueryState :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState = do State
state <- forall (m :: * -> *). MonadQuery m => m State
queryState
                   Maybe QueryState
mbQS  <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef (State -> IORef (Maybe QueryState)
rQueryState State
state)
                   case Maybe QueryState
mbQS of
                     Maybe QueryState
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                , String
"*** Data.SBV: Impossible happened: Query context required in a non-query mode."
                                                , String
"Please report this as a bug!"
                                                ]
                     Just QueryState
qs -> 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 :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(QueryState -> QueryState) -> m ()
modifyQueryState QueryState -> QueryState
f = do State
state <- forall (m :: * -> *). MonadQuery m => m State
queryState
                        Maybe QueryState
mbQS  <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef (State -> IORef (Maybe QueryState)
rQueryState State
state)
                        case Maybe QueryState
mbQS of
                          Maybe QueryState
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                     , String
"*** Data.SBV: Impossible happened: Query context required in a non-query mode."
                                                     , String
"Please report this as a bug!"
                                                     ]
                          Just QueryState
qs -> let fqs :: QueryState
fqs = QueryState -> QueryState
f QueryState
qs
                                     in QueryState
fqs seq :: forall a b. a -> b -> b
`seq` forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> a -> IO ()
writeIORef (State -> IORef (Maybe QueryState)
rQueryState State
state) forall a b. (a -> b) -> a -> b
$ 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 :: forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext State -> IO a
act = do st :: State
st@State{IORef CnstMap
rconstMap :: State -> IORef CnstMap
rconstMap :: IORef CnstMap
rconstMap} <- forall (m :: * -> *). MonadQuery m => m State
queryState
                      (IncState
is, a
r) <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ forall a. State -> (State -> IO a) -> IO (IncState, a)
withNewIncState State
st State -> IO a
act
                      forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
IORef CnstMap -> IncState -> m ()
syncUpSolver IORef CnstMap
rconstMap IncState
is
                      forall (m :: * -> *) a. Monad m => a -> m a
return a
r

-- | Generic 'Queriable' instance for 'SymVal' values
instance (MonadIO m, SymVal a) => Queriable m (SBV a) a where
  create :: QueryT m (SBV a)
create  = forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_
  project :: SBV a -> QueryT m a
project = forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, SymVal a) =>
SBV a -> m a
getValue
  embed :: a -> QueryT m (SBV a)
embed   = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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, Foldable t, Traversable t, Fresh m (t (SBV a))) => Queriable m (t (SBV a)) (t a) where
  create :: QueryT m (t (SBV a))
create  = forall (m :: * -> *) a. Fresh m a => QueryT m a
fresh
  project :: t (SBV a) -> QueryT m (t a)
project = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, SymVal a) =>
SBV a -> m a
getValue
  embed :: t a -> QueryT m (t (SBV a))
embed   = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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_ :: forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_ = forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. SVal -> SBV a
SBV forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarContext -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar VarContext
QueryVar Kind
k forall a. Maybe a
Nothing
  where k :: Kind
k = forall a. HasKind a => a -> Kind
kindOf (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 :: forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
String -> m (SBV a)
freshVar String
nm = forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. SVal -> SBV a
SBV forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarContext -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar VarContext
QueryVar Kind
k (forall a. a -> Maybe a
Just String
nm)
  where k :: Kind
k = forall a. HasKind a => a -> Kind
kindOf (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_ :: forall (m :: * -> *) (array :: * -> * -> *) a b.
(MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) =>
Maybe (SBV b) -> m (array a b)
freshArray_ = 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 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 :: forall (m :: * -> *) (array :: * -> * -> *) a b.
(MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) =>
String -> Maybe (SBV b) -> m (array a b)
freshArray String
nm = 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 (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 :: 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
mbNm Maybe (SBV b)
mbVal = forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext forall a b. (a -> b) -> 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 :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String]
msgs = do QueryState{SMTConfig
queryConfig :: SMTConfig
queryConfig :: QueryState -> SMTConfig
queryConfig} <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState
                     forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ 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 :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
s = do QueryState{Maybe Int -> String -> IO String
queryAsk :: QueryState -> Maybe Int -> String -> IO String
queryAsk :: Maybe Int -> String -> IO String
queryAsk, Maybe Int
queryTimeOutValue :: QueryState -> Maybe Int
queryTimeOutValue :: Maybe Int
queryTimeOutValue} <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState

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

           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 :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> [String] -> m String
askIgnoring String
s [String]
ignoreList = do

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

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

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

           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 :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
requireSuccess String
s = do

            QueryState{Maybe Int -> String -> IO String
queryAsk :: Maybe Int -> String -> IO String
queryAsk :: QueryState -> Maybe Int -> String -> IO String
queryAsk, Maybe Int -> String -> IO ()
querySend :: QueryState -> Maybe Int -> String -> IO ()
querySend :: Maybe Int -> String -> IO ()
querySend, SMTConfig
queryConfig :: SMTConfig
queryConfig :: QueryState -> SMTConfig
queryConfig, Maybe Int
queryTimeOutValue :: Maybe Int
queryTimeOutValue :: QueryState -> Maybe Int
queryTimeOutValue} <- 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 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ Maybe Int -> String -> IO String
queryAsk Maybe Int
queryTimeOutValue String
s

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


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

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

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

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

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

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

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

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

             let loop :: [String] -> m [String]
loop [String]
sofar = do
                  String
s <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ Maybe Int -> IO String
queryRetrieveResponse Maybe Int
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 forall a. Eq a => a -> a -> Bool
== String
synchTag Bool -> Bool -> Bool
|| forall a. Show a => a -> String
show String
s forall a. Eq a => a -> a -> Bool
== String
synchTag
                     then do forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"[SYNC] Synchronization achieved using tag: " forall a. [a] -> [a] -> [a]
++ String
synchTag]
                             forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [String]
sofar
                     else do forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"[RECV] " String -> String -> String
`alignPlain` String
s]
                             [String] -> m [String]
loop (String
s forall a. a -> [a] -> [a]
: [String]
sofar)

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

-- | Generalization of 'Data.SBV.Control.getValue'
getValue :: (MonadIO m, MonadQuery m, SymVal a) => SBV a -> m a
getValue :: forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, SymVal a) =>
SBV a -> m a
getValue SBV a
s = do SV
sv <- forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext (forall a. State -> SBV a -> IO SV
`sbvToSV` SBV a
s)
                CV
cv <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> SV -> m CV
getValueCV forall a. Maybe a
Nothing SV
sv
                forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. SymVal a => CV -> a
fromCV CV
cv

-- | A class which allows for sexpr-conversion to functions
class (HasKind r, SatModel 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, SymVal r) => fun -> SExpr -> m (Maybe ([(a, r)], r))

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

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

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

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

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

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

          bailOut :: a -> a
bailOut a
nm = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                       , String
"*** Data.SBV.getFunction: Unable to extract an interpretation for function " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
nm
                                       , String
"***"
                                       , String
"*** Failed while trying to extract a pointwise interpretation."
                                       , String
"***"
                                       , String
"*** 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 :: forall (m :: * -> *) fun a r.
(MonadIO m, SolverContext m, MonadSymbolic m,
 SMTFunction fun a r) =>
fun -> m ()
registerUISMTFunction fun
f = do State
st <- forall (m :: * -> *). SolverContext m => m State
contextState
                             String
nm <- forall fun a r (m :: * -> *).
(SMTFunction fun a r, MonadIO m, SolverContext m,
 MonadSymbolic m) =>
fun -> m String
smtFunName fun
f
                             forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ State -> String -> SBVType -> Maybe [String] -> IO ()
newUninterpreted State
st String
nm (forall fun a r. SMTFunction fun a r => fun -> SBVType
smtFunType fun
f) 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 :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
pointWiseExtract String
nm SBVType
typ
   | Bool
isBoolFunc
   = m (Maybe ([([SExpr], SExpr)], SExpr))
tryPointWise
   | Bool
True
   = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                     , String
"*** Data.SBV.getFunction: Unsupported: Extracting interpretation for function:"
                     , String
"***"
                     , String
"***     " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
" :: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SBVType
typ
                     , String
"***"
                     , String
"*** At this time, the expression returned by the solver is too complicated for SBV!"
                     , String
"***"
                     , String
"*** You can ignore uninterpreted function models for sat models using the 'satTrackUFs' parameter:"
                     , String
"***"
                     , String
"***             satWith    z3{satTrackUFs = False}"
                     , String
"***             allSatWith z3{satTrackUFs = False}"
                     , String
"***"
                     , String
"*** You can see the response from the solver by running with '{verbose = True}' option."
                     , String
"***"
                     , String
"*** NB. If this is a use case you'd like SBV to support, please get in touch!"
                     ]
  where trueSExpr :: SExpr
trueSExpr  = (Integer, Maybe Int) -> SExpr
ENum (Integer
1, forall a. Maybe a
Nothing)
        falseSExpr :: SExpr
falseSExpr = (Integer, Maybe Int) -> SExpr
ENum (Integer
0, forall a. Maybe a
Nothing)

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

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

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

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

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

                              bad :: String -> Maybe [String] -> m a
bad   = forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"get-value" String
cmd (String
"pointwise value of boolean function " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
" on " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
as) forall a. Maybe a
Nothing

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

                          forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r forall {a}. String -> Maybe [String] -> m a
bad forall a b. (a -> b) -> a -> b
$ \case EApp [EApp [SExpr
_, SExpr
e]] -> forall (m :: * -> *) a. Monad m => a -> m a
return ([SExpr]
args, SExpr
e)
                                              SExpr
_                  -> forall {a}. String -> Maybe [String] -> m a
bad String
r forall a. Maybe a
Nothing

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

        tryPointWise :: m (Maybe ([([SExpr], SExpr)], SExpr))
tryPointWise
          | Bool -> Bool
not Bool
isBoolFunc
          = forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
          | Int
nArgs forall a. Ord a => a -> a -> Bool
< Int
1
          = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.pointWiseExtract: Impossible happened, nArgs < 1: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
nArgs forall a. [a] -> [a] -> [a]
++ String
" type: " forall a. [a] -> [a] -> [a]
++ 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 ([([SExpr], SExpr)]
trues, [([SExpr], SExpr)]
falses) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\([SExpr]
_, SExpr
v) -> SExpr -> Bool
isTrueSExpr SExpr
v) [([SExpr], SExpr)]
vs
               forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ if forall (t :: * -> *) a. Foldable t => t a -> Int
length [([SExpr], SExpr)]
trues forall a. Ord a => a -> a -> Bool
<= forall (t :: * -> *) a. Foldable t => t a -> Int
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 :: forall a. Kind -> SBV a
mkArg Kind
k = case Kind -> Maybe CV
defaultKindedValue Kind
k of
            Maybe CV
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                       , String
"*** Data.SBV.smtFunSaturate: Impossible happened!"
                                       , String
"*** Unable to create a valid parameter for kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
k
                                       , String
"*** Please report this as an SBV bug!"
                                       ]
            Just CV
c -> forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (forall a b. a -> Either a b
Left CV
c)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

  smtFunSaturate :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r) -> SBV r
smtFunSaturate 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 (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @a)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @b)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @c)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @d)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @e)))

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

  smtFunType :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r)
-> SBVType
smtFunType SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r
_ = [Kind] -> SBVType
SBVType [forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @a), forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @b), forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @c), forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @d), forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @e), forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @f), forall a. HasKind a => a -> Kind
kindOf (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 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 (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @a)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @b)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @c)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @d)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @e)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @f)))

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

  smtFunType :: (SBV a
 -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r)
-> SBVType
smtFunType SBV a
-> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r
_ = [Kind] -> SBVType
SBVType [forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @a), forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @b), forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @c), forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @d), forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @e), forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @f), forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @g), forall a. HasKind a => a -> Kind
kindOf (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 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 (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @a)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @b)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @c)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @d)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @e)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @f)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @g)))

-- | Functions of arity 8
instance ( SymVal a,   HasKind a
         , SymVal b,   HasKind b
         , SymVal c,   HasKind c
         , SymVal d,   HasKind d
         , SymVal e,   HasKind e
         , SymVal f,   HasKind f
         , SymVal g,   HasKind g
         , SymVal h,   HasKind h
         , SatModel r, HasKind 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 SBV a
-> SBV b
-> SBV c
-> SBV d
-> SBV e
-> SBV f
-> SBV g
-> SBV h
-> SBV r
_ [SExpr
a0, SExpr
a1, SExpr
a2, SExpr
a3, SExpr
a4, SExpr
a5, SExpr
a6, SExpr
a7] = (,,,,,,,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a0 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a2 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a3 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a4 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a5 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a6 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a7
  sexprToArg SBV a
-> SBV b
-> SBV c
-> SBV d
-> SBV e
-> SBV f
-> SBV g
-> SBV h
-> SBV r
_ [SExpr]
_                                = 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 SBV a
-> SBV b
-> SBV c
-> SBV d
-> SBV e
-> SBV f
-> SBV g
-> SBV h
-> SBV r
_ = [Kind] -> SBVType
SBVType [forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @a), forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @b), forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @c), forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @d), forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @e), forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @f), forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @g), forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @h), forall a. HasKind a => a -> Kind
kindOf (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 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 (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @a)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @b)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @c)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @d)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @e)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @f)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @g)))
                       (forall a. Kind -> SBV a
mkArg (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @h)))

-- | Generalization of 'Data.SBV.Control.getFunction'
getFunction :: (MonadIO m, MonadQuery m, SolverContext m, MonadSymbolic m, SymVal a, SymVal r, SMTFunction fun a r) => fun -> m ([(a, r)], r)
getFunction :: forall (m :: * -> *) a r fun.
(MonadIO m, MonadQuery m, SolverContext m, MonadSymbolic m,
 SymVal a, SymVal r, SMTFunction fun a r) =>
fun -> m ([(a, r)], r)
getFunction fun
f = do String
nm <- 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 = String
"(get-value (" forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
"))"
                       bad :: String -> Maybe [String] -> m a
bad = forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getFunction" String
cmd String
"a function value" forall a. Maybe a
Nothing

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

                   forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r forall {a}. String -> Maybe [String] -> m a
bad forall a b. (a -> b) -> a -> b
$ \case EApp [EApp [ECon String
o, SExpr
e]] | String
o forall a. Eq a => a -> a -> Bool
== String
nm -> do Maybe ([(a, r)], r)
mbAssocs <- forall fun a r (m :: * -> *).
(SMTFunction fun a r, MonadIO m, SolverContext m, MonadQuery m,
 MonadSymbolic m, SymVal r) =>
fun -> SExpr -> m (Maybe ([(a, r)], r))
sexprToFun fun
f SExpr
e
                                                                               case Maybe ([(a, r)], r)
mbAssocs of
                                                                                 Just ([(a, r)], r)
assocs -> forall (m :: * -> *) a. Monad m => a -> m a
return ([(a, r)], r)
assocs
                                                                                 Maybe ([(a, r)], r)
Nothing     -> do Maybe ([([SExpr], SExpr)], SExpr)
mbPVS <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
pointWiseExtract String
nm (forall fun a r. SMTFunction fun a r => fun -> SBVType
smtFunType fun
f)
                                                                                                   case Maybe ([([SExpr], SExpr)], SExpr)
mbPVS forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {t :: * -> *} {a} {r} {a} {a}.
(Traversable t, SMTFunction fun a r, SymVal a, SymVal a) =>
(t ([SExpr], SExpr), SExpr) -> Maybe (t (a, a), a)
convert of
                                                                                                     Just ([(a, r)], r)
x  -> forall (m :: * -> *) a. Monad m => a -> m a
return ([(a, r)], r)
x
                                                                                                     Maybe ([(a, r)], r)
Nothing -> forall {a}. String -> Maybe [String] -> m a
bad String
r forall a. Maybe a
Nothing
                                       SExpr
_                                 -> forall {a}. String -> Maybe [String] -> m a
bad String
r forall a. Maybe a
Nothing
    where convert :: (t ([SExpr], SExpr), SExpr) -> Maybe (t (a, a), a)
convert    (t ([SExpr], SExpr)
vs, SExpr
d) = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {a} {r} {a}.
(SMTFunction fun a r, SymVal a) =>
([SExpr], SExpr) -> Maybe (a, a)
sexprPoint t ([SExpr], SExpr)
vs forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
d
          sexprPoint :: ([SExpr], SExpr) -> Maybe (a, a)
sexprPoint ([SExpr]
as, SExpr
v) = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall fun a r. SMTFunction fun a r => fun -> [SExpr] -> Maybe a
sexprToArg fun
f [SExpr]
as    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. SymVal 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 :: forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, HasKind a) =>
SBV a -> m String
getUninterpretedValue SBV a
s =
        case forall a. HasKind a => a -> Kind
kindOf SBV a
s of
          KUserSort String
_ Maybe [String]
Nothing -> do SV
sv <- forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext (forall a. State -> SBV a -> IO SV
`sbvToSV` SBV a
s)

                                    let nm :: String
nm  = forall a. Show a => a -> String
show SV
sv
                                        cmd :: String
cmd = String
"(get-value (" forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
"))"
                                        bad :: String -> Maybe [String] -> m a
bad = forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getValue" String
cmd String
"a model value" forall a. Maybe a
Nothing

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

                                    forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r forall {a}. String -> Maybe [String] -> m a
bad forall a b. (a -> b) -> a -> b
$ \case EApp [EApp [ECon String
o,  ECon String
v]] | String
o forall a. Eq a => a -> a -> Bool
== forall a. Show a => a -> String
show SV
sv -> forall (m :: * -> *) a. Monad m => a -> m a
return String
v
                                                        SExpr
_                                            -> forall {a}. String -> Maybe [String] -> m a
bad String
r forall a. Maybe a
Nothing

          Kind
k                   -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String
""
                                                 , String
"*** SBV.getUninterpretedValue: Called on an 'interpreted' kind"
                                                 , String
"*** "
                                                 , String
"***    Kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
k
                                                 , String
"***    Hint: Use 'getValue' to extract value for interpreted kinds."
                                                 , String
"*** "
                                                 , String
"*** 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 :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> SV -> m CV
getValueCVHelper Maybe Int
mbi SV
s
  | SV
s forall a. Eq a => a -> a -> Bool
== SV
trueSV
  = forall (m :: * -> *) a. Monad m => a -> m a
return CV
trueCV
  | SV
s forall a. Eq a => a -> a -> Bool
== SV
falseSV
  = forall (m :: * -> *) a. Monad m => a -> m a
return CV
falseCV
  | Bool
True
  = forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> String -> Kind -> m CV
extractValue Maybe Int
mbi (forall a. Show a => a -> String
show SV
s) (forall a. HasKind a => a -> Kind
kindOf SV
s)

-- | "Make up" a CV for this type. Like zero, but smarter.
defaultKindedValue :: Kind -> Maybe CV
defaultKindedValue :: Kind -> Maybe CV
defaultKindedValue Kind
k = Kind -> CVal -> CV
CV Kind
k 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 Kind
KBool            = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Integer -> CVal
CInteger Integer
0
        cvt KBounded{}       = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Integer -> CVal
CInteger Integer
0
        cvt Kind
KUnbounded       = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Integer -> CVal
CInteger Integer
0
        cvt Kind
KReal            = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ AlgReal -> CVal
CAlgReal AlgReal
0
        cvt (KUserSort String
_ Maybe [String]
ui) = Maybe [String] -> Maybe CVal
uninterp Maybe [String]
ui
        cvt Kind
KFloat           = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Float -> CVal
CFloat Float
0
        cvt Kind
KDouble          = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Double -> CVal
CDouble Double
0
        cvt Kind
KRational        = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Rational -> CVal
CRational Rational
0
        cvt (KFP Int
eb Int
sb)      = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ FP -> CVal
CFP (Bool -> Int -> Int -> FP
fpZero Bool
False Int
eb Int
sb)
        cvt Kind
KChar            = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Char -> CVal
CChar Char
'\NUL'                -- why not?
        cvt Kind
KString          = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ String -> CVal
CString String
""
        cvt (KList  Kind
_)       = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ [CVal] -> CVal
CList []
        cvt (KSet  Kind
_)        = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ RCSet CVal -> CVal
CSet forall a b. (a -> b) -> a -> b
$ forall a. Set a -> RCSet a
RegularSet forall a. Set a
Set.empty -- why not? Arguably, could be the universal set
        cvt (KTuple [Kind]
ks)      = [CVal] -> CVal
CTuple forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Kind -> Maybe CVal
cvt [Kind]
ks
        cvt (KMaybe Kind
_)       = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Maybe CVal -> CVal
CMaybe forall a. Maybe a
Nothing
        cvt (KEither Kind
k1 Kind
_)   = Either CVal CVal -> CVal
CEither forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left 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 :: Maybe [String] -> Maybe CVal
uninterp (Just (String
c:[String]
_)) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ (Maybe Int, String) -> CVal
CUserSort (forall a. a -> Maybe a
Just Int
1, String
c)
        uninterp (Just [])    = forall a. Maybe a
Nothing                       -- I don't think this can actually happen, but just in case
        uninterp Maybe [String]
Nothing      = forall a. Maybe a
Nothing                       -- Out of luck, truly uninterpreted; we don't even know if it's inhabited.

-- | Go from an SExpr directly to a value
sexprToVal :: forall a. SymVal a => SExpr -> Maybe a
sexprToVal :: forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
e = forall a. SymVal a => CV -> a
fromCV forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind -> SExpr -> Maybe CV
recoverKindedValue (forall a. HasKind a => a -> Kind
kindOf (forall {k} (t :: k). Proxy t
Proxy @a)) SExpr
e

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

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

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

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

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

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

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

                           KFP Int
eb Int
sb   | ENum (Integer
i, Maybe Int
_)      <- SExpr
e -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k forall a b. (a -> b) -> a -> b
$ FP -> CVal
CFP forall a b. (a -> b) -> a -> b
$ Int -> Int -> Integer -> FP
fpFromInteger Int
eb Int
sb Integer
i
                                       | EFloat Float
f         <- SExpr
e -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k forall a b. (a -> b) -> a -> b
$ FP -> CVal
CFP forall a b. (a -> b) -> a -> b
$ Int -> Int -> Float -> FP
fpFromFloat   Int
eb Int
sb Float
f
                                       | EDouble Double
d        <- SExpr
e -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k forall a b. (a -> b) -> a -> b
$ FP -> CVal
CFP forall a b. (a -> b) -> a -> b
$ Int -> Int -> Double -> FP
fpFromDouble  Int
eb Int
sb Double
d
                                       | EFloatingPoint FP
c <- SExpr
e -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k forall a b. (a -> b) -> a -> b
$ FP -> CVal
CFP FP
c
                                       | Bool
True                  -> forall a. Maybe a
Nothing

                           Kind
KChar       | ECon String
s      <- SExpr
e      -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KChar forall a b. (a -> b) -> a -> b
$ Char -> CVal
CChar forall a b. (a -> b) -> a -> b
$ String -> Char
interpretChar String
s
                                       | Bool
True                  -> forall a. Maybe a
Nothing

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

                           Kind
KRational                           -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k forall a b. (a -> b) -> a -> b
$ Rational -> CVal
CRational forall a b. (a -> b) -> a -> b
$ SExpr -> Rational
interpretRational SExpr
e

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

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

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

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

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

  where getUIIndex :: Kind -> String -> Maybe Int
getUIIndex (KUserSort  String
_ (Just [String]
xs)) String
i = String
i forall a. Eq a => a -> [a] -> Maybe Int
`elemIndex` [String]
xs
        getUIIndex Kind
_                        String
_ = forall a. Maybe a
Nothing

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

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

        interpretChar :: String -> Char
interpretChar String
xs = case String -> String
interpretString String
xs of
                             [Char
c] -> Char
c
                             String
_   -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Expected a singleton char constant, received: <" forall a. [a] -> [a] -> [a]
++ String
xs forall a. [a] -> [a] -> [a]
++ String
">"

        interpretRational :: SExpr -> Rational
interpretRational (EApp [ECon String
"SBV.Rational", SExpr
v1, SExpr
v2])
           | Just (CV Kind
_ (CInteger Integer
n)) <- Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
KUnbounded SExpr
v1
           , Just (CV Kind
_ (CInteger Integer
d)) <- Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
KUnbounded SExpr
v2
           = Integer
n forall a. Integral a => a -> a -> Ratio a
% Integer
d
        interpretRational SExpr
xs = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Expected a rational constant, received: <" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExpr
xs forall a. [a] -> [a] -> [a]
++ String
">"

        interpretList :: Kind -> SExpr -> [CVal]
interpretList Kind
ek SExpr
topExpr = SExpr -> [CVal]
walk SExpr
topExpr
          where walk :: SExpr -> [CVal]
walk (EApp [ECon String
"as", ECon String
"seq.empty", SExpr
_]) = []
                walk (EApp [ECon String
"seq.unit", SExpr
v])             = case Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
ek SExpr
v of
                                                                 Just CV
w -> [CV -> CVal
cvVal CV
w]
                                                                 Maybe CV
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Cannot parse a sequence item of kind " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
ek forall a. [a] -> [a] -> [a]
++ String
" from: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExpr
v forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
extra SExpr
v
                walk (EApp (ECon String
"seq.++" : [SExpr]
rest))           = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SExpr -> [CVal]
walk [SExpr]
rest
                walk SExpr
cur                                     = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Expected a sequence constant, but received: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExpr
cur forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
extra SExpr
cur

                extra :: a -> String
extra a
cur | forall a. Show a => a -> String
show a
cur forall a. Eq a => a -> a -> Bool
== String
t = String
""
                          | Bool
True          = String
"\nWhile parsing: " forall a. [a] -> [a] -> [a]
++ String
t
                          where t :: String
t = 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 Kind
ke SExpr
setExpr
             | SExpr -> Bool
isUniversal SExpr
setExpr             = forall a. Set a -> RCSet a
ComplementSet forall a. Set a
Set.empty
             | SExpr -> Bool
isEmpty     SExpr
setExpr             = forall a. Set a -> RCSet a
RegularSet    forall a. Set a
Set.empty
             | Just (Right ([([SExpr], SExpr)], SExpr)
assocs) <- Maybe (Either String ([([SExpr], SExpr)], SExpr))
mbAssocs = forall {t :: * -> *}.
Foldable t =>
(t ([SExpr], SExpr), SExpr) -> RCSet CVal
decode ([([SExpr], SExpr)], SExpr)
assocs
             | Bool
True                            = forall {a}. String -> a
tbd String
"Expected a set value, but couldn't decipher the solver output."

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


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

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

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

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

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

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

                 element :: Bool -> SExpr -> [CVal]
element Bool
cvt SExpr
x = case (Bool
cvt, Kind
ke) of
                                   (Bool
True, Kind
KChar) -> case Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
KString SExpr
x of
                                                      Just CV
v  -> case CV -> CVal
cvVal CV
v of
                                                                  CString [Char
c] -> [Char -> CVal
CChar Char
c]
                                                                  CString String
_   -> []
                                                                  CVal
_           -> forall {a}. String -> a
tbd forall a b. (a -> b) -> a -> b
$ String
"Unexpected value for kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (SExpr
x, Kind
ke)
                                                      Maybe CV
Nothing -> forall {a}. String -> a
tbd forall a b. (a -> b) -> a -> b
$ String
"Unexpected value for kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (SExpr
x, Kind
ke)
                                   (Bool, Kind)
_             -> case Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
ke SExpr
x of
                                                      Just CV
v  -> [CV -> CVal
cvVal CV
v]
                                                      Maybe CV
Nothing -> forall {a}. String -> a
tbd forall a b. (a -> b) -> a -> b
$ String
"Unexpected value for kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (SExpr
x, Kind
ke)

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

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

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

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

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

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

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

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

        -- Intervals, for dReal
        interpretInterval :: SExpr -> Maybe CV
interpretInterval SExpr
expr = case SExpr
expr of
                                   EApp [ECon String
"interval", SExpr
lo, SExpr
hi] -> do RealPoint Rational
vlo <- SExpr -> Maybe (RealPoint Rational)
getBorder SExpr
lo
                                                                        RealPoint Rational
vhi <- SExpr -> Maybe (RealPoint Rational)
getBorder SExpr
hi
                                                                        forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KReal (AlgReal -> CVal
CAlgReal (RealPoint Rational -> RealPoint Rational -> AlgReal
AlgInterval RealPoint Rational
vlo RealPoint Rational
vhi))
                                   SExpr
_                              -> forall a. Maybe a
Nothing
          where getBorder :: SExpr -> Maybe (RealPoint Rational)
getBorder (EApp [ECon String
"open",   SExpr
v]) = Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
KReal SExpr
v forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {f :: * -> *} {a}.
Applicative f =>
(Rational -> a) -> CV -> f a
border forall a. a -> RealPoint a
OpenPoint
                getBorder (EApp [ECon String
"closed", SExpr
v]) = Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
KReal SExpr
v forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall {f :: * -> *} {a}.
Applicative f =>
(Rational -> a) -> CV -> f a
border forall a. a -> RealPoint a
ClosedPoint
                getBorder SExpr
_                         = forall a. Maybe a
Nothing

                border :: (Rational -> a) -> CV -> f a
border Rational -> a
b (CV Kind
KReal (CAlgReal (AlgRational Bool
True Rational
v))) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Rational -> a
b Rational
v
                border Rational -> a
_ CV
other                                      = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.interpretInterval.border: Expected a real-valued sexp, but received: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show CV
other


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

                  let bad :: m a
bad = forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getValueCV" String
"get-value" (String
"a real-valued binding for " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SV
s) forall a. Maybe a
Nothing (forall a. Show a => a -> String
show (CV
rep1, CV
rep2)) forall a. Maybe a
Nothing

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

-- | Retrieve value from the solver
extractValue :: forall m. (MonadIO m, MonadQuery m) => Maybe Int -> String -> Kind -> m CV
extractValue :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> String -> Kind -> m CV
extractValue Maybe Int
mbi String
nm Kind
k = do
       let modelIndex :: String
modelIndex = case Maybe Int
mbi of
                          Maybe Int
Nothing -> String
""
                          Just Int
i  -> String
" :model_index " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i

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

           bad :: String -> Maybe [String] -> m a
bad = forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getModel" String
cmd (String
"a value binding for kind: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Kind
k) forall a. Maybe a
Nothing

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

       let recover :: SExpr -> m CV
recover SExpr
val = case Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
k SExpr
val of
                           Just CV
cv -> forall (m :: * -> *) a. Monad m => a -> m a
return CV
cv
                           Maybe CV
Nothing -> forall {a}. String -> Maybe [String] -> m a
bad String
r forall a. Maybe a
Nothing

       forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r forall {a}. String -> Maybe [String] -> m a
bad forall a b. (a -> b) -> a -> b
$ \case EApp [EApp [ECon String
v, SExpr
val]] | String
v forall a. Eq a => a -> a -> Bool
== String
nm -> SExpr -> m CV
recover SExpr
val
                           SExpr
_                                   -> forall {a}. String -> Maybe [String] -> m a
bad String
r forall a. Maybe a
Nothing

-- | Generalization of 'Data.SBV.Control.getUICVal'
getUICVal :: forall m. (MonadIO m, MonadQuery m) => Maybe Int -> (String, SBVType) -> m CV
getUICVal :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> (String, SBVType) -> m CV
getUICVal Maybe Int
mbi (String
nm, SBVType
t) = case SBVType
t of
                          SBVType [Kind
k] -> forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> String -> Kind -> m CV
extractValue Maybe Int
mbi String
nm Kind
k
                          SBVType
_           -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.getUICVal: Expected to be called on an uninterpeted value of a base type, received something else: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (String
nm, SBVType
t)

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

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

      bad :: String -> Maybe [String] -> m a
bad        = forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"get-value" String
cmd String
"a function value" forall a. Maybe a
Nothing

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

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

  let convert :: (t ([SExpr], SExpr), SExpr) -> Maybe (t ([CV], CV), CV)
convert (t ([SExpr], SExpr)
vs, SExpr
d) = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([SExpr], SExpr) -> Maybe ([CV], CV)
toPoint t ([SExpr], SExpr)
vs 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 ([SExpr]
as, SExpr
v)
         | forall (t :: * -> *) a. Foldable t => t a -> Int
length [SExpr]
as forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
ats = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe CV
toRes SExpr
v
         | Bool
True                    = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.getUIFunCVAssoc: Mismatching type/value arity, got: " forall a. [a] -> [a] -> [a]
++ 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 scenario, boolify the result
      -- as that's the only type we support here.
      tryPointWise :: m ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
tryPointWise m ([([CV], CV)], CV)
bailOut = do Maybe ([([SExpr], SExpr)], SExpr)
mbSExprs <- 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
                                  Maybe ([([SExpr], SExpr)], SExpr)
Nothing     -> m ([([CV], CV)], CV)
bailOut
                                  Just ([([SExpr], SExpr)], SExpr)
sExprs -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe m ([([CV], CV)], CV)
bailOut forall (m :: * -> *) a. Monad m => a -> m a
return (forall {t :: * -> *}.
Traversable t =>
(t ([SExpr], SExpr), SExpr) -> Maybe (t ([CV], CV), CV)
convert ([([SExpr], SExpr)], SExpr)
sExprs)

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

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

                                                                Maybe (Either String ([([SExpr], SExpr)], SExpr))
Nothing                                                            -> forall {m :: * -> *}.
(MonadIO m, MonadQuery m) =>
m ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
tryPointWise forall {a}. m a
bailOut

                      SExpr
_                                 -> forall {a}. String -> Maybe [String] -> m a
bad String
r forall a. Maybe a
Nothing

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

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

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

                       -- query for the precision if supported
                       let getPrecision :: m (Maybe String)
getPrecision = do SMTConfig
cfg <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
                                             case SolverCapabilities -> Maybe String
supportsDeltaSat (SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)) of
                                               Maybe String
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
                                               Just String
o  -> forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
o

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

-- | What are the top level inputs? Trackers are returned as top level existentials
getQuantifiedInputs :: (MonadIO m, MonadQuery m) => m UserInputs
getQuantifiedInputs :: forall (m :: * -> *). (MonadIO m, MonadQuery m) => m UserInputs
getQuantifiedInputs = do State{IORef Inputs
rinps :: State -> IORef Inputs
rinps :: IORef Inputs
rinps} <- forall (m :: * -> *). MonadQuery m => m State
queryState
                         (UserInputs
rQinps, InternInps
rTrackers) <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Inputs -> (UserInputs, InternInps)
getInputs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. IORef a -> IO a
readIORef IORef Inputs
rinps

                         let trackers :: UserInputs
trackers = (Quantifier
EX,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InternInps
rTrackers
                             -- separate the existential prefix, which will go first
                             (UserInputs
preQs, UserInputs
postQs) = forall a. (a -> Bool) -> Seq a -> (Seq a, Seq a)
S.spanl (\(Quantifier
q, NamedSymVar
_) -> Quantifier
q forall a. Eq a => a -> a -> Bool
== Quantifier
EX) UserInputs
rQinps

                         forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ UserInputs
preQs forall a. Semigroup a => a -> a -> a
<> UserInputs
trackers forall a. Semigroup a => a -> a -> a
<> UserInputs
postQs

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

                    Seq (Text, CV -> Bool, SV)
rObs <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef (Seq (Text, 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 []             ![(a, CV)]
sofar = forall (m :: * -> *) a. Monad m => a -> m a
return [(a, CV)]
sofar
                        walk ((a
n, CV -> Bool
f, SV
s):[(a, CV -> Bool, SV)]
os) ![(a, CV)]
sofar = do CV
cv <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> SV -> m CV
getValueCV 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) 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

                    forall {m :: * -> *} {a}.
(MonadIO m, MonadQuery m) =>
[(a, CV -> Bool, SV)] -> [(a, CV)] -> m [(a, CV)]
walk (forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (Text, 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'. Note that if we have an defined axiom, then it
-- is not really a UI, so we drop those.
getUIs :: forall m. (MonadIO m, MonadQuery m) => m [(String, SBVType)]
getUIs :: forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, SBVType)]
getUIs = do State{IORef UIMap
rUIMap :: IORef UIMap
rUIMap :: State -> IORef UIMap
rUIMap, IORef [(Bool, String, [String])]
raxioms :: State -> IORef [(Bool, String, [String])]
raxioms :: IORef [(Bool, String, [String])]
raxioms, IORef IncState
rIncState :: State -> IORef IncState
rIncState :: IORef IncState
rIncState} <- forall (m :: * -> *). MonadQuery m => m State
queryState
            -- NB. no need to worry about new-defines, because we don't allow definitions once query mode starts
            [String]
defines <- do [(Bool, String, [String])]
allAxs <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef [(Bool, String, [String])]
raxioms
                          forall (f :: * -> *) a. Applicative f => a -> f a
pure [String
nm | (Bool
True, String
nm, [String]
_) <- [(Bool, String, [String])]
allAxs]

            UIMap
prior <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef UIMap
rUIMap
            UIMap
new   <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef IncState
rIncState forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a. IORef a -> IO a
readIORef forall b c a. (b -> c) -> (a -> b) -> a -> c
. IncState -> IORef UIMap
rNewUIs
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> [a]
sort [(String, SBVType)
p | p :: (String, SBVType)
p@(String
n, SBVType
_) <- forall k a. Map k a -> [(k, a)]
Map.toList UIMap
prior forall a. [a] -> [a] -> [a]
++ forall k a. Map k a -> [(k, a)]
Map.toList UIMap
new, String
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
defines]

-- | Return all satisfying models.
getAllSatResult :: forall m. (MonadIO m, MonadQuery m, SolverContext m) => m AllSatResult
getAllSatResult :: forall (m :: * -> *).
(MonadIO m, MonadQuery m, SolverContext m) =>
m AllSatResult
getAllSatResult = do forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"*** Checking Satisfiability, all solutions.."]

                     SMTConfig
cfg <- forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
                     forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (SolverCapabilities -> Bool
supportsCustomQueries (SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg))) forall a b. (a -> b) -> a -> b
$
                        forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                        , String
"*** Data.SBV: Backend solver " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
cfg)) forall a. [a] -> [a] -> [a]
++ String
" does not support custom queries."
                                        , String
"***"
                                        , String
"*** Custom query support is needed for allSat functionality."
                                        , String
"*** Please use a solver that supports this feature."
                                        ]

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

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

                     [(String, SBVType)]
allUninterpreteds <- 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@(String
nm, SBVType [Kind]
as) <- [(String, SBVType)]
allUninterpreteds, forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
as forall a. Ord a => a -> a -> Bool
> Int
1  -- get the function ones
                                        , Bool -> Bool
not (SMTConfig -> String -> Bool
isNonModelVar SMTConfig
cfg String
nm)                              -- make sure they aren't explicitly ignored
                                     ]

                         allUiRegs :: [(String, SBVType)]
allUiRegs = [(String, SBVType)
u | u :: (String, SBVType)
u@(String
nm, SBVType [Kind]
as) <- [(String, SBVType)]
allUninterpreteds, forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
as forall a. Eq a => a -> a -> Bool
== Int
1  -- non-function ones
                                        , Bool -> Bool
not (SMTConfig -> String -> Bool
isNonModelVar SMTConfig
cfg String
nm)                               -- make sure not 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 []                           [String]
sofar = forall (m :: * -> *) a. Monad m => a -> m a
return [String]
sofar
                         collectAcceptable ((String
nm, t :: SBVType
t@(SBVType [Kind]
ats)):[(String, SBVType)]
rest) [String]
sofar
                           | Bool -> Bool
not (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 forall a. a -> [a] -> [a]
: [String]
sofar)
                           | Bool
True
                           = do forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [ String
"*** SBV.allSat: Uninterpreted function: " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
" :: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SBVType
t
                                           , String
"*** Will *not* be used in allSat considerations since its type"
                                           , String
"*** has uninterpreted sorts present."
                                           ]
                                [(String, SBVType)] -> [String] -> m [String]
collectAcceptable [(String, SBVType)]
rest [String]
sofar

                     [String]
uiFuns <- forall a. [a] -> [a]
reverse forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall {m :: * -> *}.
(MonadIO m, MonadQuery m) =>
[(String, SBVType)] -> [String] -> m [String]
collectAcceptable [(String, SBVType)]
allUiFuns []
                     [String]
_      <- forall {m :: * -> *}.
(MonadIO m, MonadQuery m) =>
[(String, SBVType)] -> [String] -> m [String]
collectAcceptable [(String, SBVType)]
allUiRegs [] -- only done to get the queryDebug output. Actual result not needed/used

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

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

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

                     let allModelInputs :: UserInputs
allModelInputs  = UserInputs -> UserInputs
prefixExistentials UserInputs
qinps
                         -- Add on observables only if we're not in a quantified context:
                         hasQuantifiers :: Bool
hasQuantifiers  = forall a. Seq a -> Int
S.length UserInputs
allModelInputs forall a. Eq a => a -> a -> Bool
/= forall a. Seq a -> Int
S.length UserInputs
qinps -- i.e., we dropped something
                         grabObservables :: Bool
grabObservables = Bool -> Bool
not Bool
hasQuantifiers

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

                                    ignored :: Text -> Bool
ignored Text
n = SMTConfig -> String -> Bool
isNonModelVar SMTConfig
cfg (Text -> String
T.unpack Text
n) Bool -> Bool -> Bool
|| Text
"__internal_sbv" Text -> Text -> Bool
`T.isPrefixOf` Text
n

                                in forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (NamedSymVar -> (SVal, NamedSymVar)
mkSVal forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Quantifier, NamedSymVar) -> NamedSymVar
namedSymVar)
                                   forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> Seq a -> Seq a
S.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Bool
ignored forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedSymVar -> Text
getUserName forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Quantifier, NamedSymVar) -> NamedSymVar
namedSymVar)
                                   forall a b. (a -> b) -> a -> b
$ UserInputs
allModelInputs

                         -- If we have any universals, then the solutions are unique upto prefix existentials.
                         w :: Bool
w = Quantifier
ALL forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList ((Quantifier, NamedSymVar) -> Quantifier
quantifier forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UserInputs
qinps)


                     -- We can go fast using the disjoint model trick if things are simple enough:
                     --     - No quantifiers
                     --     - No uninterpreted functions (uninterpreted values are OK)
                     --     - No uninterpreted sorts
                     --
                     -- Why can't we support the above?
                     --     - Uninterpreted functions: There is no (standard) way to define a function as a literal in SMTLib.
                     --     Some solvers support lambda, but this isn't common/reliable yet.
                     --     - Uninterpreted sort: There's no way to access the value the solver assigns to an uninterpreted sort.
                     --
                     -- So, if these two things are present, we go the "slow" route, by repeatedly rejecting the
                     -- previous model and asking for a new one. If they don't exist (which is the common case anyhow)
                     -- we use an idea due to z3 folks <http://theory.stanford.edu/%7Enikolaj/programmingz3.html#sec-blocking-evaluations>
                     -- which splits the search space into disjoint models and can produce results much more quickly.
                     let isSimple :: Bool
isSimple = forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, SBVType)]
allUiFuns Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
usorts Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
hasQuantifiers

                         start :: AllSatResult
start = AllSatResult { allSatMaxModelCountReached :: Bool
allSatMaxModelCountReached  = Bool
False
                                              , allSatHasPrefixExistentials :: Bool
allSatHasPrefixExistentials = Bool
w
                                              , allSatSolverReturnedUnknown :: Bool
allSatSolverReturnedUnknown = Bool
False
                                              , allSatSolverReturnedDSat :: Bool
allSatSolverReturnedDSat    = Bool
False
                                              , allSatResults :: [SMTResult]
allSatResults               = []
                                              }

                     if Bool
isSimple
                        then do let mkVar :: (String, SBVType) -> IO (SVal, NamedSymVar)
                                    mkVar :: (String, SBVType) -> IO (SVal, NamedSymVar)
mkVar (String
nm, SBVType [Kind
k]) = do SV
sv <- State -> Kind -> SBVExpr -> IO SV
newExpr State
topState Kind
k (Op -> [SV] -> SBVExpr
SBVApp (String -> Op
Uninterpreted String
nm) [])
                                                                 let sval :: SVal
sval = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache forall a b. (a -> b) -> a -> b
$ \State
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure SV
sv
                                                                     nsv :: NamedSymVar
nsv  = SV -> Text -> NamedSymVar
NamedSymVar SV
sv (String -> Text
T.pack String
nm)
                                                                 forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal
sval, NamedSymVar
nsv)
                                    mkVar (String, SBVType)
nmt = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: Impossible happened; allSat.mkVar. Unexpected: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (String, SBVType)
nmt
                                Seq (SVal, NamedSymVar)
uiVars <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Seq a
S.fromList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String, SBVType) -> IO (SVal, NamedSymVar)
mkVar [(String, SBVType)]
allUiRegs
                                Bool
-> UserInputs
-> Seq (SVal, NamedSymVar)
-> SMTConfig
-> AllSatResult
-> m AllSatResult
fastAllSat Bool
grabObservables                                        UserInputs
qinps (Seq (SVal, NamedSymVar)
uiVars forall a. Seq a -> Seq a -> Seq a
S.>< Seq (SVal, NamedSymVar)
vars) SMTConfig
cfg AllSatResult
start
                        else    forall {t :: * -> *} {t :: * -> *}.
(Traversable t, Foldable t) =>
Bool
-> State
-> ([(String, SBVType)], t String)
-> [(String, SBVType)]
-> t (Quantifier, NamedSymVar)
-> Seq (SVal, NamedSymVar)
-> SMTConfig
-> AllSatResult
-> m AllSatResult
loop       Bool
grabObservables State
topState ([(String, SBVType)]
allUiFuns, [String]
uiFuns) [(String, SBVType)]
allUiRegs UserInputs
qinps              Seq (SVal, NamedSymVar)
vars  SMTConfig
cfg AllSatResult
start

   where isFree :: Kind -> Bool
isFree (KUserSort String
_ Maybe [String]
Nothing) = Bool
True
         isFree Kind
_                     = Bool
False

         finalize :: a -> SMTConfig -> AllSatResult -> Maybe String -> f ()
finalize a
cnt SMTConfig
cfg AllSatResult
sofar Maybe String
extra
                = forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SMTConfig -> Bool
allSatPrintAlong SMTConfig
cfg Bool -> Bool -> Bool
&& Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null (AllSatResult -> [SMTResult]
allSatResults AllSatResult
sofar))) forall a b. (a -> b) -> a -> b
$ do
                           let msg :: a -> String
msg a
0 = String
"No solutions found."
                               msg a
1 = String
"This is the only solution."
                               msg a
n = String
"Found " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
n forall a. [a] -> [a] -> [a]
++ String
" different solutions."
                           forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn forall a b. (a -> b) -> a -> b
$ forall {a}. (Eq a, Num a, Show a) => a -> String
msg (a
cnt forall a. Num a => a -> a -> a
- a
1)
                           case Maybe String
extra of
                             Maybe String
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                             Just String
m  -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
m

         fastAllSat :: Bool -> S.Seq (Quantifier, NamedSymVar) -> S.Seq (SVal, NamedSymVar) -> SMTConfig -> AllSatResult -> m AllSatResult
         fastAllSat :: Bool
-> UserInputs
-> Seq (SVal, NamedSymVar)
-> SMTConfig
-> AllSatResult
-> m AllSatResult
fastAllSat Bool
grabObservables UserInputs
qinps Seq (SVal, NamedSymVar)
vars SMTConfig
cfg AllSatResult
start = do
                IORef (Int, AllSatResult, Bool, Maybe String)
result <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ forall a. a -> IO (IORef a)
newIORef (Int
0, AllSatResult
start, Bool
False, forall a. Maybe a
Nothing)
                IORef (Int, AllSatResult, Bool, Maybe String)
-> Seq (SVal, NamedSymVar) -> m ()
go IORef (Int, AllSatResult, Bool, Maybe String)
result Seq (SVal, NamedSymVar)
vars
                (Int
found, AllSatResult
sofar, Bool
_, Maybe String
extra) <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef (Int, AllSatResult, Bool, Maybe String)
result
                forall {f :: * -> *} {a}.
(Eq a, Num a, Show a, MonadIO f) =>
a -> SMTConfig -> AllSatResult -> Maybe String -> f ()
finalize (Int
foundforall a. Num a => a -> a -> a
+Int
1) SMTConfig
cfg AllSatResult
sofar Maybe String
extra
                forall (f :: * -> *) a. Applicative f => a -> f a
pure AllSatResult
sofar

           where haveEnough :: Int -> Bool
haveEnough Int
have = case SMTConfig -> Maybe Int
allSatMaxModelCount SMTConfig
cfg of
                                     Just Int
maxModels -> Int
have forall a. Ord a => a -> a -> Bool
>= Int
maxModels
                                     Maybe Int
_              -> Bool
False

                 go :: IORef (Int, AllSatResult, Bool, Maybe String) -> S.Seq (SVal, NamedSymVar) -> m ()
                 go :: IORef (Int, AllSatResult, Bool, Maybe String)
-> Seq (SVal, NamedSymVar) -> m ()
go IORef (Int, AllSatResult, Bool, Maybe String)
finalResult = Bool -> Seq (SVal, NamedSymVar) -> m ()
walk Bool
True
                   where shouldContinue :: m Bool
shouldContinue = do (Int
have, AllSatResult
_, Bool
exitLoop, Maybe String
_) <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef (Int, AllSatResult, Bool, Maybe String)
finalResult
                                             forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool
exitLoop Bool -> Bool -> Bool
|| Int -> Bool
haveEnough Int
have)

                         walk :: Bool -> S.Seq (SVal, NamedSymVar) -> m ()
                         walk :: Bool -> Seq (SVal, NamedSymVar) -> m ()
walk Bool
firstRun Seq (SVal, NamedSymVar)
terms
                           | Bool -> Bool
not Bool
firstRun Bool -> Bool -> Bool
&& forall a. Seq a -> Bool
S.null Seq (SVal, NamedSymVar)
terms
                           = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                           | Bool
True
                           = do Maybe Int
mbCont <- do (Int
have, AllSatResult
sofar, Bool
exitLoop, Maybe String
_) <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef IORef (Int, AllSatResult, Bool, Maybe String)
finalResult
                                             if Bool
exitLoop
                                                then forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
                                                else case SMTConfig -> Maybe Int
allSatMaxModelCount SMTConfig
cfg of
                                                       Just Int
maxModels
                                                         | Int
have forall a. Ord a => a -> a -> Bool
>= Int
maxModels -> do forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (AllSatResult -> Bool
allSatMaxModelCountReached AllSatResult
sofar) forall a b. (a -> b) -> a -> b
$ do
                                                                                      forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"*** Maximum model count request of " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
maxModels forall a. [a] -> [a] -> [a]
++ String
" reached, stopping the search."]
                                                                                      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SMTConfig -> Bool
allSatPrintAlong SMTConfig
cfg) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Search stopped since model count request was reached."
                                                                                      forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Int, AllSatResult, Bool, Maybe String)
finalResult forall a b. (a -> b) -> a -> b
$ \(Int
h, AllSatResult
s, Bool
_, Maybe String
m) -> (Int
h, AllSatResult
s{ allSatMaxModelCountReached :: Bool
allSatMaxModelCountReached = Bool
True }, Bool
True, Maybe String
m)
                                                                                   forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing
                                                       Maybe Int
_                     -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Int
haveforall a. Num a => a -> a -> a
+Int
1

                                case Maybe Int
mbCont of
                                  Maybe Int
Nothing  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
                                  Just Int
cnt -> do
                                    forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"Fast allSat, Looking for solution " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
cnt]

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

                                    case CheckSatResult
cs of
                                      CheckSatResult
Unsat  -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

                                      CheckSatResult
Unk    -> do let m :: String
m = String
"Solver returned unknown, terminating query."
                                                   forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"*** " forall a. [a] -> [a] -> [a]
++ String
m]
                                                   forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Int, AllSatResult, Bool, Maybe String)
finalResult forall a b. (a -> b) -> a -> b
$ \(Int
h, AllSatResult
s, Bool
_, Maybe String
_) -> (Int
h, AllSatResult
s{allSatSolverReturnedUnknown :: Bool
allSatSolverReturnedUnknown = Bool
True}, Bool
True, forall a. a -> Maybe a
Just (String
"[" forall a. [a] -> [a] -> [a]
++ String
m forall a. [a] -> [a] -> [a]
++ String
"]"))

                                      DSat Maybe String
_ -> do let m :: String
m = String
"Solver returned delta-sat, terminating query."
                                                   forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"*** " forall a. [a] -> [a] -> [a]
++ String
m]
                                                   forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Int, AllSatResult, Bool, Maybe String)
finalResult forall a b. (a -> b) -> a -> b
$ \(Int
h, AllSatResult
s, Bool
_, Maybe String
_) -> (Int
h, AllSatResult
s{allSatSolverReturnedDSat :: Bool
allSatSolverReturnedDSat = Bool
True}, Bool
True, forall a. a -> Maybe a
Just (String
"[" forall a. [a] -> [a] -> [a]
++ String
m forall a. [a] -> [a] -> [a]
++ String
"]"))

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

                                                   Maybe (Seq ((Quantifier, NamedSymVar), Maybe CV))
bindings <- let grab :: (Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV)
grab i :: (Quantifier, NamedSymVar)
i@(Quantifier
ALL, NamedSymVar
_)          = forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, NamedSymVar)
i, forall a. Maybe a
Nothing)
                                                                   grab i :: (Quantifier, NamedSymVar)
i@(Quantifier
EX, NamedSymVar -> SV
getSV -> SV
sv) = case forall a. Eq a => (a -> SV) -> SV -> Seq a -> Maybe a
lookupInput forall a b. (a, b) -> a
fst SV
sv Seq (SV, (Text, (SVal, CV)))
assocs of
                                                                                                Just (SV
_, (Text
_, (SVal
_, CV
cv))) -> forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, NamedSymVar)
i, forall a. a -> Maybe a
Just CV
cv)
                                                                                                Maybe (SV, (Text, (SVal, CV)))
Nothing                -> do !CV
cv <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> SV -> m CV
getValueCV forall a. Maybe a
Nothing SV
sv
                                                                                                                             forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, NamedSymVar)
i, forall a. a -> Maybe a
Just CV
cv)
                                                               in if SMTConfig -> Bool
validationRequested SMTConfig
cfg
                                                                  then forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {m :: * -> *}.
(MonadIO m, MonadQuery m) =>
(Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV)
grab UserInputs
qinps
                                                                  else forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

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

                                                   let lassocs :: [(SV, (Text, (SVal, CV)))]
lassocs = forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (SV, (Text, (SVal, CV)))
assocs
                                                       model :: SMTModel
model   = SMTModel { modelObjectives :: [(String, GeneralizedCV)]
modelObjectives = []
                                                                          , modelBindings :: Maybe [((Quantifier, NamedSymVar), Maybe CV)]
modelBindings   = forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Seq ((Quantifier, NamedSymVar), Maybe CV))
bindings
                                                                          , modelAssocs :: [(String, CV)]
modelAssocs     =    (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Text -> String
T.unpack forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn forall a b. (a, b) -> a
fst [(Text, CV)]
obsvs)
                                                                                              forall a. Semigroup a => a -> a -> a
<> [(Text -> String
T.unpack Text
n, CV
cv) | (SV
_, (Text
n, (SVal
_, CV
cv))) <- [(SV, (Text, (SVal, CV)))]
lassocs]
                                                                          , modelUIFuns :: [(String, (SBVType, ([([CV], CV)], CV)))]
modelUIFuns     = []
                                                                          }
                                                       currentResult :: SMTResult
currentResult = SMTConfig -> SMTModel -> SMTResult
Satisfiable SMTConfig
cfg SMTModel
model

                                                   forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Int, AllSatResult, Bool, Maybe String)
finalResult forall a b. (a -> b) -> a -> b
$ \(Int
h, AllSatResult
s, Bool
e, Maybe String
m) -> let h' :: Int
h' = Int
hforall a. Num a => a -> a -> a
+Int
1 in Int
h' seq :: forall a b. a -> b -> b
`seq` (Int
h', AllSatResult
s{allSatResults :: [SMTResult]
allSatResults = SMTResult
currentResult forall a. a -> [a] -> [a]
: AllSatResult -> [SMTResult]
allSatResults AllSatResult
s}, Bool
e, Maybe String
m)

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

                                                   let findVal :: (SVal, NamedSymVar) -> (SVal, CV)
                                                       findVal :: (SVal, NamedSymVar) -> (SVal, CV)
findVal (SVal
_, NamedSymVar SV
sv Text
nm) = case forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList (forall a. (a -> Bool) -> Seq a -> Seq a
S.filter (\(SV
sv', (Text, (SVal, CV))
_) -> SV
sv forall a. Eq a => a -> a -> Bool
== SV
sv') Seq (SV, (Text, (SVal, CV)))
assocs) of
                                                                                           [(SV
_, (Text
_, (SVal, CV)
scv))] -> (SVal, CV)
scv
                                                                                           [(SV, (Text, (SVal, CV)))]
_               -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: Cannot uniquely determine " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Text
nm forall a. [a] -> [a] -> [a]
++ String
" in " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Seq (SV, (Text, (SVal, CV)))
assocs

                                                       cstr :: Bool -> (SVal, CV) -> m ()
                                                       cstr :: Bool -> (SVal, CV) -> m ()
cstr Bool
shouldReject (SVal
sv, CV
cv) = forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain forall a b. (a -> b) -> a -> b
$ forall a. SVal -> SBV a
SBV forall a b. (a -> b) -> a -> b
$ Kind -> SVal -> SVal -> SVal
mkEq (forall a. HasKind a => a -> Kind
kindOf SVal
sv) SVal
sv (Kind -> Either CV (Cached SV) -> SVal
SVal (forall a. HasKind a => a -> Kind
kindOf SVal
sv) (forall a b. a -> Either a b
Left CV
cv))
                                                         where mkEq :: Kind -> SVal -> SVal -> SVal
                                                               mkEq :: Kind -> SVal -> SVal -> SVal
mkEq Kind
k SVal
a SVal
b
                                                                | forall a. HasKind a => a -> Bool
isDouble Kind
k Bool -> Bool -> Bool
|| forall a. HasKind a => a -> Bool
isFloat Kind
k Bool -> Bool -> Bool
|| forall a. HasKind a => a -> Bool
isFP Kind
k
                                                                = if Bool
shouldReject
                                                                     then SVal -> SVal
svNot  (SVal
a SVal -> SVal -> SVal
`fpEq` SVal
b)
                                                                     else         SVal
a SVal -> SVal -> SVal
`fpEq` SVal
b
                                                                | Bool
True
                                                                = if Bool
shouldReject
                                                                     then SVal
a SVal -> SVal -> SVal
`svNotEqual` SVal
b
                                                                     else SVal
a SVal -> SVal -> SVal
`svEqual`    SVal
b

                                                               fpEq :: SVal -> SVal -> SVal
fpEq SVal
a SVal
b = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
                                                                   where r :: State -> IO SV
r 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])

                                                       reject, accept :: (SVal, NamedSymVar) -> m ()
                                                       reject :: (SVal, NamedSymVar) -> m ()
reject = Bool -> (SVal, CV) -> m ()
cstr Bool
True  forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SVal, NamedSymVar) -> (SVal, CV)
findVal
                                                       accept :: (SVal, NamedSymVar) -> m ()
accept = Bool -> (SVal, CV) -> m ()
cstr Bool
False forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SVal, NamedSymVar) -> (SVal, CV)
findVal

                                                       scope :: (SVal, NamedSymVar) -> S.Seq (SVal, NamedSymVar) -> m () -> m ()
                                                       scope :: (SVal, NamedSymVar) -> Seq (SVal, NamedSymVar) -> m () -> m ()
scope (SVal, NamedSymVar)
cur Seq (SVal, NamedSymVar)
pres m ()
c = do
                                                                forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True String
"(push 1)"
                                                                (SVal, NamedSymVar) -> m ()
reject (SVal, NamedSymVar)
cur
                                                                forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (SVal, NamedSymVar) -> m ()
accept Seq (SVal, NamedSymVar)
pres
                                                                ()
r <- m ()
c
                                                                forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True String
"(pop 1)"
                                                                forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
r

                                                   forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
0 .. forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq (SVal, NamedSymVar)
terms forall a. Num a => a -> a -> a
- Int
1] forall a b. (a -> b) -> a -> b
$ \Int
i -> do
                                                        Bool
sc <- m Bool
shouldContinue
                                                        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
sc forall a b. (a -> b) -> a -> b
$ do case forall a. Int -> Seq a -> (Seq a, Seq a)
S.splitAt Int
i Seq (SVal, NamedSymVar)
terms of
                                                                       (Seq (SVal, NamedSymVar)
pre, rest :: Seq (SVal, NamedSymVar)
rest@((SVal, NamedSymVar)
cur S.:<| Seq (SVal, NamedSymVar)
_)) -> (SVal, NamedSymVar) -> Seq (SVal, NamedSymVar) -> m () -> m ()
scope (SVal, NamedSymVar)
cur Seq (SVal, NamedSymVar)
pre forall a b. (a -> b) -> a -> b
$ Bool -> Seq (SVal, NamedSymVar) -> m ()
walk Bool
False Seq (SVal, NamedSymVar)
rest
                                                                       (Seq (SVal, NamedSymVar), Seq (SVal, NamedSymVar))
_                         -> forall a. HasCallStack => String -> a
error String
"Data.SBV.allSat: Impossible happened, ran out of terms!"

         -- All sat loop. This is slower, as it implements the reject-the-previous model and loop around logic. But
         -- it can handle uninterpreted sorts; so we keep it here as a fall-back.
         loop :: Bool
-> State
-> ([(String, SBVType)], t String)
-> [(String, SBVType)]
-> t (Quantifier, NamedSymVar)
-> Seq (SVal, NamedSymVar)
-> SMTConfig
-> AllSatResult
-> m AllSatResult
loop Bool
grabObservables State
topState ([(String, SBVType)]
allUiFuns, t String
uiFunsToReject) [(String, SBVType)]
allUiRegs t (Quantifier, NamedSymVar)
qinps Seq (SVal, NamedSymVar)
vars SMTConfig
cfg = Int -> AllSatResult -> m AllSatResult
go (Int
1::Int)
           where go :: Int -> AllSatResult -> m AllSatResult
                 go :: Int -> AllSatResult -> m AllSatResult
go !Int
cnt !AllSatResult
sofar
                   | Just Int
maxModels <- SMTConfig -> Maybe Int
allSatMaxModelCount SMTConfig
cfg, Int
cnt forall a. Ord a => a -> a -> Bool
> Int
maxModels
                   = do forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"*** Maximum model count request of " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
maxModels forall a. [a] -> [a] -> [a]
++ String
" reached, stopping the search."]
                        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SMTConfig -> Bool
allSatPrintAlong SMTConfig
cfg) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Search stopped since model count request was reached."
                        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! AllSatResult
sofar { allSatMaxModelCountReached :: Bool
allSatMaxModelCountReached = Bool
True }
                   | Bool
True
                   = do forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"Looking for solution " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
cnt]

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

                        let endMsg :: Maybe String -> m ()
endMsg = forall {f :: * -> *} {a}.
(Eq a, Num a, Show a, MonadIO f) =>
a -> SMTConfig -> AllSatResult -> Maybe String -> f ()
finalize Int
cnt SMTConfig
cfg AllSatResult
sofar

                        case CheckSatResult
cs of
                          CheckSatResult
Unsat  -> do Maybe String -> m ()
endMsg forall a. Maybe a
Nothing
                                       forall (m :: * -> *) a. Monad m => a -> m a
return AllSatResult
sofar

                          CheckSatResult
Unk    -> do let m :: String
m = String
"Solver returned unknown, terminating query."
                                       forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"*** " forall a. [a] -> [a] -> [a]
++ String
m]
                                       Maybe String -> m ()
endMsg forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ String
"[" forall a. [a] -> [a] -> [a]
++ String
m forall a. [a] -> [a] -> [a]
++ String
"]"
                                       forall (m :: * -> *) a. Monad m => a -> m a
return AllSatResult
sofar{ allSatSolverReturnedUnknown :: Bool
allSatSolverReturnedUnknown = Bool
True }

                          DSat Maybe String
_ -> do let m :: String
m = String
"Solver returned delta-sat, terminating query."
                                       forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"*** " forall a. [a] -> [a] -> [a]
++ String
m]
                                       Maybe String -> m ()
endMsg forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ String
"[" forall a. [a] -> [a] -> [a]
++ String
m forall a. [a] -> [a] -> [a]
++ String
"]"
                                       forall (m :: * -> *) a. Monad m => a -> m a
return AllSatResult
sofar{ allSatSolverReturnedDSat :: Bool
allSatSolverReturnedDSat = Bool
True }

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

                                       let getUIFun :: (String, SBVType) -> m (String, (SBVType, ([([CV], CV)], CV)))
getUIFun ui :: (String, SBVType)
ui@(String
nm, SBVType
t) = do ([([CV], CV)], CV)
cvs <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> (String, SBVType) -> m ([([CV], CV)], CV)
getUIFunCVAssoc forall a. Maybe a
Nothing (String, SBVType)
ui
                                                                    forall (m :: * -> *) a. Monad m => a -> m a
return (String
nm, (SBVType
t, ([([CV], CV)], CV)
cvs))
                                       [(String, (SBVType, ([([CV], CV)], CV)))]
uiFunVals <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {m :: * -> *}.
(MonadIO m, MonadQuery m) =>
(String, SBVType) -> m (String, (SBVType, ([([CV], CV)], CV)))
getUIFun [(String, SBVType)]
allUiFuns

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

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

                                       Maybe (t ((Quantifier, NamedSymVar), Maybe CV))
bindings <- let grab :: (Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV)
grab i :: (Quantifier, NamedSymVar)
i@(Quantifier
ALL, NamedSymVar
_)          = forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, NamedSymVar)
i, forall a. Maybe a
Nothing)
                                                       grab i :: (Quantifier, NamedSymVar)
i@(Quantifier
EX, NamedSymVar -> SV
getSV -> SV
sv) = case forall a. Eq a => (a -> SV) -> SV -> Seq a -> Maybe a
lookupInput forall a b. (a, b) -> a
fst SV
sv Seq (SV, (Text, (SVal, CV)))
assocs of
                                                                                Just (SV
_, (Text
_, (SVal
_, CV
cv))) -> forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, NamedSymVar)
i, forall a. a -> Maybe a
Just CV
cv)
                                                                                Maybe (SV, (Text, (SVal, CV)))
Nothing                -> do !CV
cv <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Int -> SV -> m CV
getValueCV forall a. Maybe a
Nothing SV
sv
                                                                                                             forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, NamedSymVar)
i, forall a. a -> Maybe a
Just CV
cv)
                                                   in if SMTConfig -> Bool
validationRequested SMTConfig
cfg
                                                         then forall a. a -> Maybe a
Just forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall {m :: * -> *}.
(MonadIO m, MonadQuery m) =>
(Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV)
grab t (Quantifier, NamedSymVar)
qinps
                                                         else forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

                                       let model :: SMTModel
model = SMTModel { modelObjectives :: [(String, GeneralizedCV)]
modelObjectives = []
                                                            , modelBindings :: Maybe [((Quantifier, NamedSymVar), Maybe CV)]
modelBindings   = forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (t ((Quantifier, NamedSymVar), Maybe CV))
bindings
                                                            , modelAssocs :: [(String, CV)]
modelAssocs     =    [(String, CV)]
uiRegVals
                                                                                forall a. Semigroup a => a -> a -> a
<> (forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Text -> String
T.unpack forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn forall a b. (a, b) -> a
fst [(Text, CV)]
obsvs)
                                                                                forall a. Semigroup a => a -> a -> a
<> [(Text -> String
T.unpack Text
n, CV
cv) | (SV
_, (Text
n, (SVal
_, CV
cv))) <- forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (SV, (Text, (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

                                           (Seq (SVal, CV)
interpreteds, Seq (SVal, CV)
uninterpreteds) = forall a. (a -> Bool) -> Seq a -> (Seq a, Seq a)
S.partition (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Bool
isFree forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasKind a => a -> Kind
kindOf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) Seq (SV, (Text, (SVal, CV)))
assocs)

                                           interpretedRegUis :: [(String, CV)]
interpretedRegUis = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Bool
isFree forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. HasKind a => a -> Kind
kindOf forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(String, CV)]
uiRegVals

                                           interpretedRegUiSVs :: [(SVal, CV)]
interpretedRegUiSVs = [(String -> Kind -> SVal
cvt String
n (forall a. HasKind a => a -> Kind
kindOf CV
cv), CV
cv) | (String
n, CV
cv) <- [(String, CV)]
interpretedRegUis]
                                             where cvt :: String -> Kind -> SVal
                                                   cvt :: String -> Kind -> SVal
cvt String
nm Kind
k = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
                                                     where r :: State -> IO SV
r State
st = State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (String -> Op
Uninterpreted String
nm) [])

                                           -- 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 = [forall {a}. HasKind a => a -> SVal -> SVal -> SVal
mkNotEq (forall a. HasKind a => a -> Kind
kindOf SVal
sv) SVal
sv (Kind -> Either CV (Cached SV) -> SVal
SVal (forall a. HasKind a => a -> Kind
kindOf SVal
sv) (forall a b. a -> Either a b
Left CV
cv)) | (SVal
sv, CV
cv) <- [(SVal, CV)]
interpretedRegUiSVs forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (SVal, CV)
interpreteds]
                                              where mkNotEq :: a -> SVal -> SVal -> SVal
mkNotEq a
k SVal
a SVal
b
                                                     | forall a. HasKind a => a -> Bool
isDouble a
k Bool -> Bool -> Bool
|| forall a. HasKind a => a -> Bool
isFloat a
k Bool -> Bool -> Bool
|| forall a. HasKind a => a -> Bool
isFP a
k
                                                     = SVal -> SVal
svNot (SVal
a SVal -> SVal -> SVal
`fpEq` SVal
b)
                                                     | Bool
True
                                                     = SVal
a SVal -> SVal -> SVal
`svNotEqual` SVal
b

                                                    fpEq :: SVal -> SVal -> SVal
fpEq SVal
a SVal
b = Kind -> Either CV (Cached SV) -> SVal
SVal Kind
KBool forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
                                                        where r :: State -> IO SV
r 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 = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [SVal] -> [SVal]
pwDistinct         -- Assert that they are pairwise distinct
                                                            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> Bool) -> [a] -> [a]
filter (\[SVal]
l -> forall (t :: * -> *) a. Foldable t => t a -> Int
length [SVal]
l forall a. Ord a => a -> a -> Bool
> Int
1)  -- Only need this class if it has at least two members
                                                            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst)                -- throw away values, we only need svals
                                                            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> b
snd)      -- make sure they belong to the same sort and have the same value
                                                            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn forall a b. (a, b) -> b
snd                   -- sort them according to their CV (i.e., sort/value)
                                                            forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (SVal, CV)
uninterpreteds
                                             where pwDistinct :: [SVal] -> [SVal]
                                                   pwDistinct :: [SVal] -> [SVal]
pwDistinct [SVal]
ss = [SVal
x SVal -> SVal -> SVal
`svNotEqual` SVal
y | (SVal
x:[SVal]
ys) <- 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]
                                           (Maybe [String]
uninterpretedReject, [String]
uninterpretedFuns) = (Maybe [String]
uiReject, forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
defs)
                                               where uiReject :: Maybe [String]
uiReject = case [String]
rejects of
                                                                  []  -> forall a. Maybe a
Nothing
                                                                  [String]
xs  -> forall a. a -> Maybe a
Just [String]
xs

                                                     ([String]
rejects, [[String]]
defs) = 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@(String
nm, (SBVType, ([([CV], CV)], CV))
_) <- [(String, (SBVType, ([([CV], CV)], CV)))]
uiFunVals, String
nm 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 (String
nm, (SBVType [Kind]
ts, ([([CV], CV)], CV)
vs)) = (String
reject, [String]
def forall a. [a] -> [a] -> [a]
++ [String]
dif)
                                                       where nm' :: String
nm' = String
nm forall a. [a] -> [a] -> [a]
++ String
"_model" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
cnt

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

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

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

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

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

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

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

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

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

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

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

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

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

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

                                       let resultsSoFar :: AllSatResult
resultsSoFar = AllSatResult
sofar { allSatResults :: [SMTResult]
allSatResults = SMTResult
m forall a. a -> [a] -> [a]
: AllSatResult -> [SMTResult]
allSatResults AllSatResult
sofar }

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

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

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

                                                  -- send the disallow clause and the uninterpreted rejector:
                                                  case (forall {a}. Maybe (SBV a)
disallow, Maybe String
rejectFuncs) of
                                                     (Maybe SBool
Nothing, Maybe String
Nothing) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure AllSatResult
resultsSoFar
                                                     (Just SBool
d,  Maybe String
Nothing) -> do forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain SBool
d
                                                                              Int -> AllSatResult -> m AllSatResult
go (Int
cntforall a. Num a => a -> a -> a
+Int
1) AllSatResult
resultsSoFar
                                                     (Maybe SBool
Nothing, Just String
f)  -> do forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True forall a b. (a -> b) -> a -> b
$ String
"(assert " forall a. [a] -> [a] -> [a]
++ String
f forall a. [a] -> [a] -> [a]
++ String
")"
                                                                              Int -> AllSatResult -> m AllSatResult
go (Int
cntforall a. Num a => a -> a -> a
+Int
1) AllSatResult
resultsSoFar
                                                     (Just SBool
d,  Just 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 forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain 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 <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ State -> SVal -> IO SV
svToSV State
topState (forall a. SBV a -> SVal
unSBV SBool
d)
                                                                              forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True forall a b. (a -> b) -> a -> b
$ String
"(assert (or " forall a. [a] -> [a] -> [a]
++ String
f forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SV
svd forall a. [a] -> [a] -> [a]
++ String
"))"
                                                                              Int -> AllSatResult -> m AllSatResult
go (Int
cntforall a. Num a => a -> a -> a
+Int
1) AllSatResult
resultsSoFar

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

            bad :: String -> Maybe [String] -> m a
bad = forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getUnsatAssumptions" String
cmd String
"a list of unsatisfiable assumptions"
                           forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just [ String
"Make sure you use:"
                                  , String
""
                                  , String
"       setOption $ ProduceUnsatAssumptions True"
                                  , String
""
                                  , String
"to make sure the solver is ready for producing unsat assumptions,"
                                  , String
"and that there is a model by first issuing a 'checkSat' call."
                                  ]

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

        String
r <- 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 []     [a]
sofar = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse [a]
sofar
            walk (String
a:[String]
as) [a]
sofar = case String
a forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(String, a)]
proxyMap of
                                  Just a
v  -> [String] -> [a] -> m [a]
walk [String]
as (a
vforall a. a -> [a] -> [a]
:[a]
sofar)
                                  Maybe a
Nothing -> do forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [ String
"*** In call to 'getUnsatAssumptions'"
                                                           , String
"***"
                                                           , String
"***    Unexpected assumption named: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show String
a
                                                           , String
"***    Was expecting one of       : " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [String]
originals
                                                           , String
"***"
                                                           , String
"*** This can happen if unsat-cores are also enabled. Ignoring."
                                                           ]
                                                [String] -> [a] -> m [a]
walk [String]
as [a]
sofar

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

-- | Generalization of 'Data.SBV.Control.timeout'
timeout :: (MonadIO m, MonadQuery m) => Int -> m a -> m a
timeout :: forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
Int -> m a -> m a
timeout Int
n m a
q = do forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(QueryState -> QueryState) -> m ()
modifyQueryState (\QueryState
qs -> QueryState
qs {queryTimeOutValue :: Maybe Int
queryTimeOutValue = forall a. a -> Maybe a
Just Int
n})
                 a
r <- m a
q
                 forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(QueryState -> QueryState) -> m ()
modifyQueryState (\QueryState
qs -> QueryState
qs {queryTimeOutValue :: Maybe Int
queryTimeOutValue = forall a. Maybe a
Nothing})
                 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 :: forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> a
fCont SExpr -> a
sCont = case String -> Either String SExpr
parseSExpr String
r of
                        Left  String
e   -> String -> Maybe [String] -> a
fCont String
r (forall a. a -> Maybe a
Just [String
e])
                        Right 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 :: forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
ctx String
sent String
expected Maybe [String]
mbHint String
received Maybe [String]
mbReason = do
        -- empty the response channel first
        [String]
extras <- forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> Maybe Int -> m [String]
retrieveResponse String
"terminating upon unexpected response" (forall a. a -> Maybe a
Just Int
5000000)

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

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

        forall (m :: * -> *) a. MonadIO m => IO a -> m a
io forall a b. (a -> b) -> a -> b
$ 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 SBVRunMode
rm QueryContext
context [String]
comments res :: Result
res@(Result KindSet
ki [(String, CV)]
_qcInfo [(String, CV -> Bool, SV)]
_observables [(String, [String])]
_codeSegs ([(Quantifier, NamedSymVar)], [NamedSymVar])
is (CnstMap, [(SV, CV)])
consts [((Int, Kind, Kind), [SV])]
tbls [(Int, ArrayInfo)]
arrs [(String, SBVType)]
uis [(Bool, String, [String])]
axs SBVPgm
pgm Seq (Bool, [(String, String)], SV)
cstrs [(String, Maybe CallStack, SV)]
_assertions [SV]
outputs) =
     let (SMTConfig
config, Bool
isSat, Bool
isSafe, Bool
isSetup) = case SBVRunMode
rm of
                                              SMTMode QueryContext
_ IStage
stage Bool
s SMTConfig
c -> (SMTConfig
c, Bool
s, IStage -> Bool
isSafetyCheckingIStage IStage
stage, IStage -> Bool
isSetupIStage IStage
stage)
                                              SBVRunMode
_                   -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"runProofOn: Unexpected run mode: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SBVRunMode
rm

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

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

         qinps :: [(Quantifier, NamedSymVar)]
qinps      = if Bool
isSat then forall a b. (a, b) -> a
fst ([(Quantifier, NamedSymVar)], [NamedSymVar])
is else forall a b. (a -> b) -> [a] -> [b]
map forall {b}. (Quantifier, b) -> (Quantifier, b)
flipQ (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
                        [SV
so]          -> case SV
so of
                                           SV Kind
KBool NodeId
_ -> SV
so
                                           SV
_          -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Impossible happened, non-boolean output: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SV
so
                                                                         , String
"Detected while generating the trace:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Result
res
                                                                         ]
                        [SV]
os  -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"User error: Multiple output values detected: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [SV]
os
                                               , String
"Detected while generating the trace:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Result
res
                                               , String
"*** Check calls to \"output\", they are typically not needed!"
                                               ]

     in 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 (CnstMap, [(SV, CV)])
consts [((Int, Kind, Kind), [SV])]
tbls [(Int, ArrayInfo)]
arrs [(String, SBVType)]
uis [(Bool, 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 :: forall (m :: * -> *) a.
ExtractIO m =>
QueryContext -> QueryT m a -> SymbolicT m a
executeQuery QueryContext
queryContext (QueryT ReaderT State m a
userQuery) = do
     State
st <- forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv
     SBVRunMode
rm <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef (State -> IORef SBVRunMode
runMode State
st)

     -- Make sure the phases match:
     () <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ case (QueryContext
queryContext, SBVRunMode
rm) of
                      (QueryContext
QueryInternal, SBVRunMode
_)                                -> forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- no worries, internal
                      (QueryContext
QueryExternal, SMTMode QueryContext
QueryExternal IStage
ISetup Bool
_ SMTConfig
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return () -- legitimate runSMT call
                      (QueryContext, SBVRunMode)
_                                                 -> 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 <- sbvForall_
     --                 y :: SBool <- sbvExists_
     --                 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 QueryContext
_ IStage
_ Bool
_ SMTConfig
cfg -> SMTConfig -> Bool
allowQuantifiedQueries SMTConfig
cfg
                      SBVRunMode
CodeGen           -> Bool
False -- doesn't matter in these two
                      Concrete{}        -> Bool
False -- cases, but we're being careful

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

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

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

                  -- make sure if we have dsat precision, then solver supports it
                  let dsatOK :: Bool
dsatOK =  forall a. Maybe a -> Bool
isNothing (SMTConfig -> Maybe Double
dsatPrecision SMTConfig
cfg)
                             Bool -> Bool -> Bool
|| forall a. Maybe a -> Bool
isJust    (SolverCapabilities -> Maybe String
supportsDeltaSat (SMTSolver -> SolverCapabilities
capabilities SMTSolver
slvr))

                  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
dsatOK forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
                                     [ String
""
                                     , String
"*** Data.SBV: Delta-sat precision is specified."
                                     , String
"***           But the chosen solver (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (SMTSolver -> Solver
name SMTSolver
slvr) forall a. [a] -> [a] -> [a]
++ String
") does not support"
                                     , String
"***           delta-satisfiability."
                                     ]

                  Result
res     <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ State -> IO Result
extractSymbolicSimulationState State
st
                  [SMTOption]
setOpts <- forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 forall a. [a] -> [a] -> [a]
++ [SMTOption]
setOpts }
                      pgm :: SMTLibPgm
pgm  = SMTConfig -> SMTLibPgm
smtLibPgm SMTConfig
cfg'

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

                  forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ SMTEngine
backend SMTConfig
cfg' State
st (forall a. Show a => a -> String
show SMTLibPgm
pgm) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. ExtractIO m => m a -> IO (m a)
extractIO forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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      -- Can't 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 QueryContext
_ IStage
IRun Bool
_ SMTConfig
_ -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                              , String
"*** Data.SBV: Unsupported nested query is detected."
                                              , String
"***"
                                              , String
"*** Please group your queries into one block. Note that this"
                                              , String
"*** can also arise if you have a call to 'query' not within 'runSMT'"
                                              , String
"*** For instance, within 'sat'/'prove' calls with custom user queries."
                                              , String
"*** The solution is to do the sat/prove part in the query directly."
                                              , String
"***"
                                              , String
"*** While multiple/nested queries should not be necessary in general,"
                                              , String
"*** please do get in touch if your use case does require such a feature,"
                                              , String
"*** to see how we can accommodate such scenarios."
                                              ]

        -- Otherwise choke!
        SBVRunMode
_ -> forall {a} {a}. Show a => a -> a
invalidQuery SBVRunMode
rm

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

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