{-# 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
instance MonadIO m => SolverContext (QueryT m) where
constrain :: SBool -> QueryT m ()
constrain = Bool -> [(String, String)] -> SBool -> QueryT m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> [(String, String)] -> SBool -> m ()
addQueryConstraint Bool
False []
softConstrain :: SBool -> QueryT m ()
softConstrain = Bool -> [(String, String)] -> SBool -> QueryT m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> [(String, String)] -> SBool -> m ()
addQueryConstraint Bool
True []
namedConstraint :: String -> SBool -> QueryT m ()
namedConstraint String
nm = Bool -> [(String, String)] -> SBool -> QueryT m ()
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 = Bool -> [(String, String)] -> SBool -> QueryT m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> [(String, String)] -> SBool -> m ()
addQueryConstraint Bool
False
addAxiom :: String -> [String] -> QueryT m ()
addAxiom = String -> [String] -> QueryT m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> [String] -> m ()
addQueryAxiom
contextState :: QueryT m State
contextState = QueryT m State
forall (m :: * -> *). MonadQuery m => m State
queryState
setOption :: SMTOption -> QueryT m ()
setOption SMTOption
o
| SMTOption -> Bool
isStartModeOption SMTOption
o = String -> QueryT m ()
forall a. HasCallStack => String -> a
error (String -> QueryT m ()) -> String -> QueryT m ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
, String
"*** Data.SBV: '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SMTOption -> String
forall a. Show a => a -> String
show SMTOption
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' can only be set at start-up time."
, String
"*** Hint: Move the call to 'setOption' before the query."
]
| Bool
True = Bool -> String -> QueryT m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True (String -> QueryT m ()) -> String -> QueryT m ()
forall a b. (a -> b) -> a -> b
$ SMTOption -> String
setSMTOption SMTOption
o
addSMTDefinition :: String -> [String] -> QueryT m ()
addSMTDefinition String
nm [String]
_ = String -> QueryT m ()
forall a. HasCallStack => String -> a
error (String -> QueryT m ()) -> String -> QueryT m ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
, String
"*** Data.SBV: '" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"' must be defined in regular (non-query) mode."
, String
"*** Hint: Define all functions before starting the query."
]
addQueryConstraint :: (MonadIO m, MonadQuery m) => Bool -> [(String, String)] -> SBool -> m ()
addQueryConstraint :: Bool -> [(String, String)] -> SBool -> m ()
addQueryConstraint Bool
isSoft [(String, String)]
atts SBool
b = do SV
sv <- (State -> IO SV) -> m SV
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext (\State
st -> IO SV -> IO SV
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SV -> IO SV) -> IO SV -> IO SV
forall a b. (a -> b) -> a -> b
$ do (String -> IO ()) -> [String] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (String -> State -> String -> IO ()
registerLabel String
"Constraint" State
st) [String
nm | (String
":named", String
nm) <- [(String, String)]
atts]
State -> SBool -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st SBool
b)
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([(String, String)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, String)]
atts Bool -> Bool -> Bool
&& SV
sv SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
asrt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(String, String)] -> String -> String
addAnnotations [(String, String)]
atts (SV -> String
forall a. Show a => a -> String
show SV
sv) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
where asrt :: String
asrt | Bool
isSoft = String
"assert-soft"
| Bool
True = String
"assert"
addQueryAxiom :: (MonadIO m, MonadQuery m) => String -> [String] -> m ()
addQueryAxiom :: String -> [String] -> m ()
addQueryAxiom String
nm [String]
ls = do Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"; -- user given axiom: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm
Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String]
ls
getConfig :: (MonadIO m, MonadQuery m) => m SMTConfig
getConfig :: m SMTConfig
getConfig = QueryState -> SMTConfig
queryConfig (QueryState -> SMTConfig) -> m QueryState -> m SMTConfig
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState
getObjectives :: (MonadIO m, MonadQuery m) => m [Objective (SV, SV)]
getObjectives :: m [Objective (SV, SV)]
getObjectives = do State{IORef [Objective (SV, SV)]
rOptGoals :: State -> IORef [Objective (SV, SV)]
rOptGoals :: IORef [Objective (SV, SV)]
rOptGoals} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
IO [Objective (SV, SV)] -> m [Objective (SV, SV)]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO [Objective (SV, SV)] -> m [Objective (SV, SV)])
-> IO [Objective (SV, SV)] -> m [Objective (SV, SV)]
forall a b. (a -> b) -> a -> b
$ [Objective (SV, SV)] -> [Objective (SV, SV)]
forall a. [a] -> [a]
reverse ([Objective (SV, SV)] -> [Objective (SV, SV)])
-> IO [Objective (SV, SV)] -> IO [Objective (SV, SV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef [Objective (SV, SV)] -> IO [Objective (SV, SV)]
forall a. IORef a -> IO a
readIORef IORef [Objective (SV, SV)]
rOptGoals
getSBVPgm :: (MonadIO m, MonadQuery m) => m SBVPgm
getSBVPgm :: m SBVPgm
getSBVPgm = do State{IORef SBVPgm
spgm :: State -> IORef SBVPgm
spgm :: IORef SBVPgm
spgm} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
IO SBVPgm -> m SBVPgm
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO SBVPgm -> m SBVPgm) -> IO SBVPgm -> m SBVPgm
forall a b. (a -> b) -> a -> b
$ IORef SBVPgm -> IO SBVPgm
forall a. IORef a -> IO a
readIORef IORef SBVPgm
spgm
getSBVAssertions :: (MonadIO m, MonadQuery m) => m [(String, Maybe CallStack, SV)]
getSBVAssertions :: m [(String, Maybe CallStack, SV)]
getSBVAssertions = do State{IORef [(String, Maybe CallStack, SV)]
rAsserts :: State -> IORef [(String, Maybe CallStack, SV)]
rAsserts :: IORef [(String, Maybe CallStack, SV)]
rAsserts} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
IO [(String, Maybe CallStack, SV)]
-> m [(String, Maybe CallStack, SV)]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO [(String, Maybe CallStack, SV)]
-> m [(String, Maybe CallStack, SV)])
-> IO [(String, Maybe CallStack, SV)]
-> m [(String, Maybe CallStack, SV)]
forall a b. (a -> b) -> a -> b
$ [(String, Maybe CallStack, SV)] -> [(String, Maybe CallStack, SV)]
forall a. [a] -> [a]
reverse ([(String, Maybe CallStack, SV)]
-> [(String, Maybe CallStack, SV)])
-> IO [(String, Maybe CallStack, SV)]
-> IO [(String, Maybe CallStack, SV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef [(String, Maybe CallStack, SV)]
-> IO [(String, Maybe CallStack, SV)]
forall a. IORef a -> IO a
readIORef IORef [(String, Maybe CallStack, SV)]
rAsserts
io :: MonadIO m => IO a -> m a
io :: IO a -> m a
io = IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO
syncUpSolver :: (MonadIO m, MonadQuery m) => IORef CnstMap -> IncState -> m ()
syncUpSolver :: IORef CnstMap -> IncState -> m ()
syncUpSolver IORef CnstMap
rGlobalConsts IncState
is = do
SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
(CnstMap
newConsts, CnstMap
allConsts) <- IO (CnstMap, CnstMap) -> m (CnstMap, CnstMap)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (CnstMap, CnstMap) -> m (CnstMap, CnstMap))
-> IO (CnstMap, CnstMap) -> m (CnstMap, CnstMap)
forall a b. (a -> b) -> a -> b
$ do CnstMap
nc <- IORef CnstMap -> IO CnstMap
forall a. IORef a -> IO a
readIORef (IncState -> IORef CnstMap
rNewConsts IncState
is)
CnstMap
oc <- IORef CnstMap -> IO CnstMap
forall a. IORef a -> IO a
readIORef IORef CnstMap
rGlobalConsts
let allConsts :: CnstMap
allConsts = CnstMap -> CnstMap -> CnstMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union CnstMap
nc CnstMap
oc
IORef CnstMap -> CnstMap -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef CnstMap
rGlobalConsts CnstMap
allConsts
(CnstMap, CnstMap) -> IO (CnstMap, CnstMap)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CnstMap
nc, CnstMap
allConsts)
[String]
ls <- IO [String] -> m [String]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO [String] -> m [String]) -> IO [String] -> m [String]
forall a b. (a -> b) -> a -> b
$ do let swap :: (b, a) -> (a, b)
swap (b
a, a
b) = (a
b, b
a)
cmp :: (a, b) -> (a, b) -> Ordering
cmp (a
a, b
_) (a
b, b
_) = a
a a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
`compare` a
b
arrange :: (a, (b, c, b)) -> ((a, b, c), b)
arrange (a
i, (b
at, c
rt, b
es)) = ((a
i, b
at, c
rt), b
es)
[NamedSymVar]
inps <- [NamedSymVar] -> [NamedSymVar]
forall a. [a] -> [a]
reverse ([NamedSymVar] -> [NamedSymVar])
-> IO [NamedSymVar] -> IO [NamedSymVar]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef [NamedSymVar] -> IO [NamedSymVar]
forall a. IORef a -> IO a
readIORef (IncState -> IORef [NamedSymVar]
rNewInps IncState
is)
KindSet
ks <- IORef KindSet -> IO KindSet
forall a. IORef a -> IO a
readIORef (IncState -> IORef KindSet
rNewKinds IncState
is)
[(Key, ArrayInfo)]
arrs <- IntMap ArrayInfo -> [(Key, ArrayInfo)]
forall a. IntMap a -> [(Key, a)]
IMap.toAscList (IntMap ArrayInfo -> [(Key, ArrayInfo)])
-> IO (IntMap ArrayInfo) -> IO [(Key, ArrayInfo)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (IntMap ArrayInfo) -> IO (IntMap ArrayInfo)
forall a. IORef a -> IO a
readIORef (IncState -> IORef (IntMap ArrayInfo)
rNewArrs IncState
is)
[((Key, Kind, Kind), [SV])]
tbls <- ((Key, (Kind, Kind, [SV])) -> ((Key, Kind, Kind), [SV]))
-> [(Key, (Kind, Kind, [SV]))] -> [((Key, Kind, Kind), [SV])]
forall a b. (a -> b) -> [a] -> [b]
map (Key, (Kind, Kind, [SV])) -> ((Key, Kind, Kind), [SV])
forall a b c b. (a, (b, c, b)) -> ((a, b, c), b)
arrange ([(Key, (Kind, Kind, [SV]))] -> [((Key, Kind, Kind), [SV])])
-> (Map (Kind, Kind, [SV]) Key -> [(Key, (Kind, Kind, [SV]))])
-> Map (Kind, Kind, [SV]) Key
-> [((Key, Kind, Kind), [SV])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Key, (Kind, Kind, [SV]))
-> (Key, (Kind, Kind, [SV])) -> Ordering)
-> [(Key, (Kind, Kind, [SV]))] -> [(Key, (Kind, Kind, [SV]))]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Key, (Kind, Kind, [SV])) -> (Key, (Kind, Kind, [SV])) -> Ordering
forall a b b. Ord a => (a, b) -> (a, b) -> Ordering
cmp ([(Key, (Kind, Kind, [SV]))] -> [(Key, (Kind, Kind, [SV]))])
-> (Map (Kind, Kind, [SV]) Key -> [(Key, (Kind, Kind, [SV]))])
-> Map (Kind, Kind, [SV]) Key
-> [(Key, (Kind, Kind, [SV]))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Kind, Kind, [SV]), Key) -> (Key, (Kind, Kind, [SV])))
-> [((Kind, Kind, [SV]), Key)] -> [(Key, (Kind, Kind, [SV]))]
forall a b. (a -> b) -> [a] -> [b]
map ((Kind, Kind, [SV]), Key) -> (Key, (Kind, Kind, [SV]))
forall b a. (b, a) -> (a, b)
swap ([((Kind, Kind, [SV]), Key)] -> [(Key, (Kind, Kind, [SV]))])
-> (Map (Kind, Kind, [SV]) Key -> [((Kind, Kind, [SV]), Key)])
-> Map (Kind, Kind, [SV]) Key
-> [(Key, (Kind, Kind, [SV]))]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (Kind, Kind, [SV]) Key -> [((Kind, Kind, [SV]), Key)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map (Kind, Kind, [SV]) Key -> [((Key, Kind, Kind), [SV])])
-> IO (Map (Kind, Kind, [SV]) Key)
-> IO [((Key, Kind, Kind), [SV])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (Map (Kind, Kind, [SV]) Key)
-> IO (Map (Kind, Kind, [SV]) Key)
forall a. IORef a -> IO a
readIORef (IncState -> IORef (Map (Kind, Kind, [SV]) Key)
rNewTbls IncState
is)
[(String, SBVType)]
uis <- Map String SBVType -> [(String, SBVType)]
forall k a. Map k a -> [(k, a)]
Map.toAscList (Map String SBVType -> [(String, SBVType)])
-> IO (Map String SBVType) -> IO [(String, SBVType)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (Map String SBVType) -> IO (Map String SBVType)
forall a. IORef a -> IO a
readIORef (IncState -> IORef (Map String SBVType)
rNewUIs IncState
is)
SBVPgm
as <- IORef SBVPgm -> IO SBVPgm
forall a. IORef a -> IO a
readIORef (IncState -> IORef SBVPgm
rNewAsgns IncState
is)
Seq (Bool, [(String, String)], SV)
constraints <- IORef (Seq (Bool, [(String, String)], SV))
-> IO (Seq (Bool, [(String, String)], SV))
forall a. IORef a -> IO a
readIORef (IncState -> IORef (Seq (Bool, [(String, String)], SV))
rNewConstraints IncState
is)
let cnsts :: [(SV, CV)]
cnsts = ((SV, CV) -> (SV, CV) -> Ordering) -> [(SV, CV)] -> [(SV, CV)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (SV, CV) -> (SV, CV) -> Ordering
forall a b b. Ord a => (a, b) -> (a, b) -> Ordering
cmp ([(SV, CV)] -> [(SV, CV)])
-> (CnstMap -> [(SV, CV)]) -> CnstMap -> [(SV, CV)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((CV, SV) -> (SV, CV)) -> [(CV, SV)] -> [(SV, CV)]
forall a b. (a -> b) -> [a] -> [b]
map (CV, SV) -> (SV, CV)
forall b a. (b, a) -> (a, b)
swap ([(CV, SV)] -> [(SV, CV)])
-> (CnstMap -> [(CV, SV)]) -> CnstMap -> [(SV, CV)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CnstMap -> [(CV, SV)]
forall k a. Map k a -> [(k, a)]
Map.toList (CnstMap -> [(SV, CV)]) -> CnstMap -> [(SV, CV)]
forall a b. (a -> b) -> a -> b
$ CnstMap
newConsts
[String] -> IO [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> IO [String]) -> [String] -> IO [String]
forall a b. (a -> b) -> a -> b
$ SMTConfig -> SMTLibIncConverter [String]
toIncSMTLib SMTConfig
cfg [NamedSymVar]
inps KindSet
ks (CnstMap
allConsts, [(SV, CV)]
cnsts) [(Key, ArrayInfo)]
arrs [((Key, Kind, Kind), [SV])]
tbls [(String, SBVType)]
uis SBVPgm
as Seq (Bool, [(String, String)], SV)
constraints SMTConfig
cfg
(String -> m ()) -> [String] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True) ([String] -> m ()) -> [String] -> m ()
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
mergeSExpr [String]
ls
getQueryState :: (MonadIO m, MonadQuery m) => m QueryState
getQueryState :: m QueryState
getQueryState = do State
state <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
Maybe QueryState
mbQS <- IO (Maybe QueryState) -> m (Maybe QueryState)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (Maybe QueryState) -> m (Maybe QueryState))
-> IO (Maybe QueryState) -> m (Maybe QueryState)
forall a b. (a -> b) -> a -> b
$ IORef (Maybe QueryState) -> IO (Maybe QueryState)
forall a. IORef a -> IO a
readIORef (State -> IORef (Maybe QueryState)
rQueryState State
state)
case Maybe QueryState
mbQS of
Maybe QueryState
Nothing -> String -> m QueryState
forall a. HasCallStack => String -> a
error (String -> m QueryState) -> String -> m QueryState
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
, String
"*** Data.SBV: Impossible happened: Query context required in a non-query mode."
, String
"Please report this as a bug!"
]
Just QueryState
qs -> QueryState -> m QueryState
forall (m :: * -> *) a. Monad m => a -> m a
return QueryState
qs
modifyQueryState :: (MonadIO m, MonadQuery m) => (QueryState -> QueryState) -> m ()
modifyQueryState :: (QueryState -> QueryState) -> m ()
modifyQueryState QueryState -> QueryState
f = do State
state <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
Maybe QueryState
mbQS <- IO (Maybe QueryState) -> m (Maybe QueryState)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (Maybe QueryState) -> m (Maybe QueryState))
-> IO (Maybe QueryState) -> m (Maybe QueryState)
forall a b. (a -> b) -> a -> b
$ IORef (Maybe QueryState) -> IO (Maybe QueryState)
forall a. IORef a -> IO a
readIORef (State -> IORef (Maybe QueryState)
rQueryState State
state)
case Maybe QueryState
mbQS of
Maybe QueryState
Nothing -> String -> m ()
forall a. HasCallStack => String -> a
error (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
, String
"*** Data.SBV: 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 QueryState -> m () -> m ()
`seq` IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IORef (Maybe QueryState) -> Maybe QueryState -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (State -> IORef (Maybe QueryState)
rQueryState State
state) (Maybe QueryState -> IO ()) -> Maybe QueryState -> IO ()
forall a b. (a -> b) -> a -> b
$ QueryState -> Maybe QueryState
forall a. a -> Maybe a
Just QueryState
fqs
inNewContext :: (MonadIO m, MonadQuery m) => (State -> IO a) -> m a
inNewContext :: (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} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
(IncState
is, a
r) <- IO (IncState, a) -> m (IncState, a)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (IncState, a) -> m (IncState, a))
-> IO (IncState, a) -> m (IncState, a)
forall a b. (a -> b) -> a -> b
$ State -> (State -> IO a) -> IO (IncState, a)
forall a. State -> (State -> IO a) -> IO (IncState, a)
withNewIncState State
st State -> IO a
act
IORef CnstMap -> IncState -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
IORef CnstMap -> IncState -> m ()
syncUpSolver IORef CnstMap
rconstMap IncState
is
a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r
instance (MonadIO m, SymVal a) => Queriable m (SBV a) a where
create :: QueryT m (SBV a)
create = QueryT m (SBV a)
forall a (m :: * -> *).
(MonadIO m, MonadQuery m, SymVal a) =>
m (SBV a)
freshVar_
project :: SBV a -> QueryT m a
project = SBV a -> QueryT m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, SymVal a) =>
SBV a -> m a
getValue
embed :: a -> QueryT m (SBV a)
embed = SBV a -> QueryT m (SBV a)
forall (m :: * -> *) a. Monad m => a -> m a
return (SBV a -> QueryT m (SBV a))
-> (a -> SBV a) -> a -> QueryT m (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SBV a
forall a. SymVal a => a -> SBV a
literal
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 = QueryT m (t (SBV a))
forall (m :: * -> *) a. Fresh m a => QueryT m a
fresh
project :: t (SBV a) -> QueryT m (t a)
project = (SBV a -> QueryT m a) -> t (SBV a) -> QueryT m (t a)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SBV a -> QueryT m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m, SymVal a) =>
SBV a -> m a
getValue
embed :: t a -> QueryT m (t (SBV a))
embed = t (SBV a) -> QueryT m (t (SBV a))
forall (m :: * -> *) a. Monad m => a -> m a
return (t (SBV a) -> QueryT m (t (SBV a)))
-> (t a -> t (SBV a)) -> t a -> QueryT m (t (SBV a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> SBV a) -> t a -> t (SBV a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> SBV a
forall a. SymVal a => a -> SBV a
literal
freshVar_ :: forall a m. (MonadIO m, MonadQuery m, SymVal a) => m (SBV a)
freshVar_ :: m (SBV a)
freshVar_ = (State -> IO (SBV a)) -> m (SBV a)
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext ((State -> IO (SBV a)) -> m (SBV a))
-> (State -> IO (SBV a)) -> m (SBV a)
forall a b. (a -> b) -> a -> b
$ (SVal -> SBV a) -> IO SVal -> IO (SBV a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBV a
forall a. SVal -> SBV a
SBV (IO SVal -> IO (SBV a))
-> (State -> IO SVal) -> State -> IO (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarContext -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar VarContext
QueryVar Kind
k Maybe String
forall a. Maybe a
Nothing
where k :: Kind
k = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)
freshVar :: forall a m. (MonadIO m, MonadQuery m, SymVal a) => String -> m (SBV a)
freshVar :: String -> m (SBV a)
freshVar String
nm = (State -> IO (SBV a)) -> m (SBV a)
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext ((State -> IO (SBV a)) -> m (SBV a))
-> (State -> IO (SBV a)) -> m (SBV a)
forall a b. (a -> b) -> a -> b
$ (SVal -> SBV a) -> IO SVal -> IO (SBV a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap SVal -> SBV a
forall a. SVal -> SBV a
SBV (IO SVal -> IO (SBV a))
-> (State -> IO SVal) -> State -> IO (SBV a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarContext -> Kind -> Maybe String -> State -> IO SVal
svMkSymVar VarContext
QueryVar Kind
k (String -> Maybe String
forall a. a -> Maybe a
Just String
nm)
where k :: Kind
k = Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)
freshArray_ :: (MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) => Maybe (SBV b) -> m (array a b)
freshArray_ :: Maybe (SBV b) -> m (array a b)
freshArray_ = Maybe String -> Maybe (SBV b) -> m (array a b)
forall (m :: * -> *) (array :: * -> * -> *) a b.
(MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) =>
Maybe String -> Maybe (SBV b) -> m (array a b)
mkFreshArray Maybe String
forall a. Maybe a
Nothing
freshArray :: (MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) => String -> Maybe (SBV b) -> m (array a b)
freshArray :: String -> Maybe (SBV b) -> m (array a b)
freshArray String
nm = Maybe String -> Maybe (SBV b) -> m (array a b)
forall (m :: * -> *) (array :: * -> * -> *) a b.
(MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) =>
Maybe String -> Maybe (SBV b) -> m (array a b)
mkFreshArray (String -> Maybe String
forall a. a -> Maybe a
Just String
nm)
mkFreshArray :: (MonadIO m, MonadQuery m, SymArray array, HasKind a, HasKind b) => Maybe String -> Maybe (SBV b) -> m (array a b)
mkFreshArray :: Maybe String -> Maybe (SBV b) -> m (array a b)
mkFreshArray Maybe String
mbNm Maybe (SBV b)
mbVal = (State -> IO (array a b)) -> m (array a b)
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext ((State -> IO (array a b)) -> m (array a b))
-> (State -> IO (array a b)) -> m (array a b)
forall a b. (a -> b) -> a -> b
$ Maybe String -> Maybe (SBV b) -> State -> IO (array a b)
forall (array :: * -> * -> *) a b.
(SymArray array, HasKind a, HasKind b) =>
Maybe String -> Maybe (SBV b) -> State -> IO (array a b)
newArrayInState Maybe String
mbNm Maybe (SBV b)
mbVal
queryDebug :: (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug :: [String] -> m ()
queryDebug [String]
msgs = do QueryState{SMTConfig
queryConfig :: SMTConfig
queryConfig :: QueryState -> SMTConfig
queryConfig} <- m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState
IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ SMTConfig -> [String] -> IO ()
forall (m :: * -> *). MonadIO m => SMTConfig -> [String] -> m ()
debug SMTConfig
queryConfig [String]
msgs
ask :: (MonadIO m, MonadQuery m) => String -> m String
ask :: String -> m String
ask String
s = do QueryState{Maybe Key -> String -> IO String
queryAsk :: QueryState -> Maybe Key -> String -> IO String
queryAsk :: Maybe Key -> String -> IO String
queryAsk, Maybe Key
queryTimeOutValue :: QueryState -> Maybe Key
queryTimeOutValue :: Maybe Key
queryTimeOutValue} <- m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState
case Maybe Key
queryTimeOutValue of
Maybe Key
Nothing -> [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"[SEND] " String -> String -> String
`alignPlain` String
s]
Just Key
i -> [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"[SEND, TimeOut: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
showTimeoutValue Key
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"] " String -> String -> String
`alignPlain` String
s]
String
r <- IO String -> m String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO String -> m String) -> IO String -> m String
forall a b. (a -> b) -> a -> b
$ Maybe Key -> String -> IO String
queryAsk Maybe Key
queryTimeOutValue String
s
[String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"[RECV] " String -> String -> String
`alignPlain` String
r]
String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return String
r
askIgnoring :: (MonadIO m, MonadQuery m) => String -> [String] -> m String
askIgnoring :: String -> [String] -> m String
askIgnoring String
s [String]
ignoreList = do
QueryState{Maybe Key -> String -> IO String
queryAsk :: Maybe Key -> String -> IO String
queryAsk :: QueryState -> Maybe Key -> String -> IO String
queryAsk, Maybe Key -> IO String
queryRetrieveResponse :: QueryState -> Maybe Key -> IO String
queryRetrieveResponse :: Maybe Key -> IO String
queryRetrieveResponse, Maybe Key
queryTimeOutValue :: Maybe Key
queryTimeOutValue :: QueryState -> Maybe Key
queryTimeOutValue} <- m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState
case Maybe Key
queryTimeOutValue of
Maybe Key
Nothing -> [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"[SEND] " String -> String -> String
`alignPlain` String
s]
Just Key
i -> [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"[SEND, TimeOut: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
showTimeoutValue Key
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"] " String -> String -> String
`alignPlain` String
s]
String
r <- IO String -> m String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO String -> m String) -> IO String -> m String
forall a b. (a -> b) -> a -> b
$ Maybe Key -> String -> IO String
queryAsk Maybe Key
queryTimeOutValue String
s
[String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"[RECV] " String -> String -> String
`alignPlain` String
r]
let loop :: String -> m String
loop String
currentResponse
| String
currentResponse String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
ignoreList
= String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return String
currentResponse
| Bool
True
= do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"[WARN] Previous response is explicitly ignored, beware!"]
String
newResponse <- IO String -> m String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO String -> m String) -> IO String -> m String
forall a b. (a -> b) -> a -> b
$ Maybe Key -> IO String
queryRetrieveResponse Maybe Key
queryTimeOutValue
[String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"[RECV] " String -> String -> String
`alignPlain` String
newResponse]
String -> m String
loop String
newResponse
String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
loop String
r
send :: (MonadIO m, MonadQuery m) => Bool -> String -> m ()
send :: Bool -> String -> m ()
send Bool
requireSuccess String
s = do
QueryState{Maybe Key -> String -> IO String
queryAsk :: Maybe Key -> String -> IO String
queryAsk :: QueryState -> Maybe Key -> String -> IO String
queryAsk, Maybe Key -> String -> IO ()
querySend :: QueryState -> Maybe Key -> String -> IO ()
querySend :: Maybe Key -> String -> IO ()
querySend, SMTConfig
queryConfig :: SMTConfig
queryConfig :: QueryState -> SMTConfig
queryConfig, Maybe Key
queryTimeOutValue :: Maybe Key
queryTimeOutValue :: QueryState -> Maybe Key
queryTimeOutValue} <- m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState
if Bool
requireSuccess Bool -> Bool -> Bool
&& SolverCapabilities -> Bool
supportsCustomQueries (SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
queryConfig))
then do String
r <- IO String -> m String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO String -> m String) -> IO String -> m String
forall a b. (a -> b) -> a -> b
$ Maybe Key -> String -> IO String
queryAsk Maybe Key
queryTimeOutValue String
s
case String -> [String]
words String
r of
[String
"success"] -> [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"[GOOD] " String -> String -> String
`alignPlain` String
s]
[String]
_ -> do case Maybe Key
queryTimeOutValue of
Maybe Key
Nothing -> [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"[FAIL] " String -> String -> String
`alignPlain` String
s]
Just Key
i -> [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [(String
"[FAIL, TimeOut: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
showTimeoutValue Key
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"] ") String -> String -> String
`alignPlain` String
s]
let cmd :: String
cmd = case String -> [String]
words ((Char -> Bool) -> String -> String
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"
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m ()
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
cmd String
s String
"success" Maybe [String]
forall a. Maybe a
Nothing String
r Maybe [String]
forall a. Maybe a
Nothing
else do
[String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"[FIRE] " String -> String -> String
`alignPlain` String
s]
IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ Maybe Key -> String -> IO ()
querySend Maybe Key
queryTimeOutValue String
s
retrieveResponse :: (MonadIO m, MonadQuery m) => String -> Maybe Int -> m [String]
retrieveResponse :: String -> Maybe Key -> m [String]
retrieveResponse String
userTag Maybe Key
mbTo = do
String
ts <- IO String -> m String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (ZonedTime -> String
forall a. Show a => a -> String
show (ZonedTime -> String) -> IO ZonedTime -> IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO ZonedTime
getZonedTime)
let synchTag :: String
synchTag = String -> String
forall a. Show a => a -> String
show (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
userTag String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (at: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ts String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
cmd :: String
cmd = String
"(echo " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
synchTag String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
[String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"[SYNC] Attempting to synchronize with tag: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
synchTag]
Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
False String
cmd
QueryState{Maybe Key -> IO String
queryRetrieveResponse :: Maybe Key -> IO String
queryRetrieveResponse :: QueryState -> Maybe Key -> IO String
queryRetrieveResponse} <- m QueryState
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m QueryState
getQueryState
let loop :: [String] -> m [String]
loop [String]
sofar = do
String
s <- IO String -> m String
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO String -> m String) -> IO String -> m String
forall a b. (a -> b) -> a -> b
$ Maybe Key -> IO String
queryRetrieveResponse Maybe Key
mbTo
if String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
synchTag Bool -> Bool -> Bool
|| String -> String
forall a. Show a => a -> String
show String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
synchTag
then do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"[SYNC] Synchronization achieved using tag: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
synchTag]
[String] -> m [String]
forall (m :: * -> *) a. Monad m => a -> m a
return ([String] -> m [String]) -> [String] -> m [String]
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
forall a. [a] -> [a]
reverse [String]
sofar
else do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"[RECV] " String -> String -> String
`alignPlain` String
s]
[String] -> m [String]
loop (String
s String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)
[String] -> m [String]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
[String] -> m [String]
loop []
getValue :: (MonadIO m, MonadQuery m, SymVal a) => SBV a -> m a
getValue :: SBV a -> m a
getValue SBV a
s = do SV
sv <- (State -> IO SV) -> m SV
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext (State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
`sbvToSV` SBV a
s)
CV
cv <- Maybe Key -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> SV -> m CV
getValueCV Maybe Key
forall a. Maybe a
Nothing SV
sv
a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> m a) -> a -> m a
forall a b. (a -> b) -> a -> b
$ CV -> a
forall a. SymVal a => CV -> a
fromCV CV
cv
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 #-}
smtFunDefault fun
_
| Just CV
v <- Kind -> Maybe CV
defaultKindedValue (Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)), Just (r
res, []) <- [CV] -> Maybe (r, [CV])
forall a. SatModel a => [CV] -> Maybe (a, [CV])
parseCVs [CV
v]
= r -> Maybe r
forall a. a -> Maybe a
Just r
res
| Bool
True
= Maybe r
forall a. Maybe a
Nothing
smtFunName fun
f = do st :: State
st@State{IORef (Map String SBVType)
rUIMap :: State -> IORef (Map String SBVType)
rUIMap :: IORef (Map String SBVType)
rUIMap} <- m State
forall (m :: * -> *). SolverContext m => m State
contextState
Map String SBVType
uiMap <- IO (Map String SBVType) -> m (Map String SBVType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Map String SBVType) -> m (Map String SBVType))
-> IO (Map String SBVType) -> m (Map String SBVType)
forall a b. (a -> b) -> a -> b
$ IORef (Map String SBVType) -> IO (Map String SBVType)
forall a. IORef a -> IO a
readIORef IORef (Map String SBVType)
rUIMap
State -> Map String SBVType -> m String
forall (m :: * -> *) b.
MonadIO m =>
State -> Map String b -> m String
findName State
st Map String SBVType
uiMap
where findName :: State -> Map String b -> m String
findName st :: State
st@State{IORef SBVPgm
spgm :: IORef SBVPgm
spgm :: State -> IORef SBVPgm
spgm} Map String b
uiMap = do
SV
r <- IO SV -> m SV
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SV -> m SV) -> IO SV -> m SV
forall a b. (a -> b) -> a -> b
$ State -> SBV r -> IO SV
forall a. State -> SBV a -> IO SV
sbvToSV State
st (fun -> SBV r
forall fun a r. SMTFunction fun a r => fun -> SBV r
smtFunSaturate fun
f)
IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ SV -> IO ()
forceSVArg SV
r
SBVPgm Seq (SV, SBVExpr)
asgns <- IO SBVPgm -> m SBVPgm
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SBVPgm -> m SBVPgm) -> IO SBVPgm -> m SBVPgm
forall a b. (a -> b) -> a -> b
$ IORef SBVPgm -> IO SBVPgm
forall a. IORef a -> IO a
readIORef IORef SBVPgm
spgm
let cantFind :: a
cantFind = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [ String
""
, String
"*** Data.SBV.getFunction: Must be called on an uninterpreted function!"
, String
"***"
, String
"*** Expected to receive a function created by \"uninterpret\""
]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
tag
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ 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 ((String, b) -> String) -> [(String, b)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, b) -> String
forall a b. (a, b) -> a
fst (Map String b -> [(String, b)]
forall k a. Map k a -> [(k, a)]
Map.toList Map String b
uiMap) of
[] -> [ String
"*** But, there are no matching uninterpreted functions in the context." ]
[String
x] -> [ String
"*** The only possible candidate is: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x ]
[String]
cands -> [ String
"*** Candidates are:"
, String
"*** " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
cands
]
case ((SV, SBVExpr) -> Bool) -> Seq (SV, SBVExpr) -> Maybe Key
forall a. (a -> Bool) -> Seq a -> Maybe Key
S.findIndexR ((SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
r) (SV -> Bool) -> ((SV, SBVExpr) -> SV) -> (SV, SBVExpr) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SV, SBVExpr) -> SV
forall a b. (a, b) -> a
fst) Seq (SV, SBVExpr)
asgns of
Maybe Key
Nothing -> m String
forall a. a
cantFind
Just Key
i -> case Seq (SV, SBVExpr)
asgns Seq (SV, SBVExpr) -> Key -> (SV, SBVExpr)
forall a. Seq a -> Key -> a
`S.index` Key
i of
(SV
sv, SBVApp (Uninterpreted String
nm) [SV]
_) | SV
r SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
sv -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return String
nm
(SV, SBVExpr)
_ -> m String
forall a. a
cantFind
sexprToFun fun
f SExpr
e = do String
nm <- fun -> m String
forall fun a r (m :: * -> *).
(SMTFunction fun a r, MonadIO m, SolverContext m,
MonadSymbolic m) =>
fun -> m String
smtFunName fun
f
case SExpr -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
parseSExprFunction SExpr
e of
Just (Left String
nm') -> case (String
nm String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
nm', fun -> Maybe r
forall fun a r. SMTFunction fun a r => fun -> Maybe r
smtFunDefault fun
f) of
(Bool
True, Just r
v) -> Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r)))
-> Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r))
forall a b. (a -> b) -> a -> b
$ ([(a, r)], r) -> Maybe ([(a, r)], r)
forall a. a -> Maybe a
Just ([], r
v)
(Bool, Maybe r)
_ -> String -> m (Maybe ([(a, r)], r))
forall a a. Show a => a -> a
bailOut String
nm
Just (Right ([([SExpr], SExpr)], SExpr)
v) -> Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r)))
-> Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r))
forall a b. (a -> b) -> a -> b
$ ([([SExpr], SExpr)], SExpr) -> Maybe ([(a, r)], r)
forall (t :: * -> *) a r a a.
(Traversable t, SMTFunction fun a r, 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 <- String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
pointWiseExtract String
nm (fun -> SBVType
forall fun a r. SMTFunction fun a r => fun -> SBVType
smtFunType fun
f)
Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r)))
-> Maybe ([(a, r)], r) -> m (Maybe ([(a, r)], r))
forall a b. (a -> b) -> a -> b
$ Maybe ([([SExpr], SExpr)], SExpr)
mbPVS Maybe ([([SExpr], SExpr)], SExpr)
-> (([([SExpr], SExpr)], SExpr) -> Maybe ([(a, r)], r))
-> Maybe ([(a, r)], r)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([([SExpr], SExpr)], SExpr) -> Maybe ([(a, r)], r)
forall (t :: * -> *) a r a a.
(Traversable t, SMTFunction fun a r, 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) = (,) (t (a, a) -> a -> (t (a, a), a))
-> Maybe (t (a, a)) -> Maybe (a -> (t (a, a), a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (([SExpr], SExpr) -> Maybe (a, a))
-> t ([SExpr], SExpr) -> Maybe (t (a, a))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([SExpr], SExpr) -> Maybe (a, a)
forall a r a.
(SMTFunction fun a r, SymVal a) =>
([SExpr], SExpr) -> Maybe (a, a)
sexprPoint t ([SExpr], SExpr)
vs Maybe (a -> (t (a, a), a)) -> Maybe a -> Maybe (t (a, a), a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe a
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
d
sexprPoint :: ([SExpr], SExpr) -> Maybe (a, a)
sexprPoint ([SExpr]
as, SExpr
v) = (,) (a -> a -> (a, a)) -> Maybe a -> Maybe (a -> (a, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> fun -> [SExpr] -> Maybe a
forall fun a r. SMTFunction fun a r => fun -> [SExpr] -> Maybe a
sexprToArg fun
f [SExpr]
as Maybe (a -> (a, a)) -> Maybe a -> Maybe (a, a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe a
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
v
bailOut :: a -> a
bailOut a
nm = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
, String
"*** Data.SBV.getFunction: Unable to extract an interpretation for function " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
nm
, 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!"
]
registerUISMTFunction :: (MonadIO m, SolverContext m, MonadSymbolic m) => SMTFunction fun a r => fun -> m ()
registerUISMTFunction :: fun -> m ()
registerUISMTFunction fun
f = do State
st <- m State
forall (m :: * -> *). SolverContext m => m State
contextState
String
nm <- fun -> m String
forall fun a r (m :: * -> *).
(SMTFunction fun a r, MonadIO m, SolverContext m,
MonadSymbolic m) =>
fun -> m String
smtFunName fun
f
IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ State -> String -> SBVType -> Maybe [String] -> IO ()
newUninterpreted State
st String
nm (fun -> SBVType
forall fun a r. SMTFunction fun a r => fun -> SBVType
smtFunType fun
f) Maybe [String]
forall a. Maybe a
Nothing
pointWiseExtract :: forall m. (MonadIO m, MonadQuery m) => String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
String
nm SBVType
typ
| Bool
isBoolFunc
= m (Maybe ([([SExpr], SExpr)], SExpr))
tryPointWise
| Bool
True
= String -> m (Maybe ([([SExpr], SExpr)], SExpr))
forall a. HasCallStack => String -> a
error (String -> m (Maybe ([([SExpr], SExpr)], SExpr)))
-> String -> m (Maybe ([([SExpr], SExpr)], SExpr))
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
, String
"*** Data.SBV.getFunction: Unsupported: Extracting interpretation for function:"
, String
"***"
, String
"*** " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVType -> String
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 Key) -> SExpr
ENum (Integer
1, Maybe Key
forall a. Maybe a
Nothing)
falseSExpr :: SExpr
falseSExpr = (Integer, Maybe Key) -> SExpr
ENum (Integer
0, Maybe Key
forall a. Maybe a
Nothing)
isTrueSExpr :: SExpr -> Bool
isTrueSExpr (ENum (Integer
1, Maybe Key
Nothing)) = Bool
True
isTrueSExpr (ENum (Integer
0, Maybe Key
Nothing)) = Bool
False
isTrueSExpr SExpr
s = String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.pointWiseExtract: Impossible happened: Received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
s
(Key
nArgs, Bool
isBoolFunc) = case SBVType
typ of
SBVType [Kind]
ts -> ([Kind] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [Kind]
ts Key -> Key -> Key
forall a. Num a => a -> a -> a
- Key
1, (Kind -> Bool) -> [Kind] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
KBool) [Kind]
ts)
getBVal :: [SExpr] -> m ([SExpr], SExpr)
getBVal :: [SExpr] -> m ([SExpr], SExpr)
getBVal [SExpr]
args = do let shc :: SExpr -> p
shc SExpr
c | SExpr -> Bool
isTrueSExpr SExpr
c = p
"true"
| Bool
True = p
"false"
as :: String
as = [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (SExpr -> String) -> [SExpr] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SExpr -> String
forall p. IsString p => SExpr -> p
shc [SExpr]
args
cmd :: String
cmd = String
"(get-value ((" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
as String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")))"
bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"get-value" String
cmd (String
"pointwise value of boolean function " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" on " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
as) Maybe [String]
forall a. Maybe a
Nothing
String
r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd
String
-> (String -> Maybe [String] -> m ([SExpr], SExpr))
-> (SExpr -> m ([SExpr], SExpr))
-> m ([SExpr], SExpr)
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m ([SExpr], SExpr)
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m ([SExpr], SExpr)) -> m ([SExpr], SExpr))
-> (SExpr -> m ([SExpr], SExpr)) -> m ([SExpr], SExpr)
forall a b. (a -> b) -> a -> b
$ \case EApp [EApp [SExpr
_, SExpr
e]] -> ([SExpr], SExpr) -> m ([SExpr], SExpr)
forall (m :: * -> *) a. Monad m => a -> m a
return ([SExpr]
args, SExpr
e)
SExpr
_ -> String -> Maybe [String] -> m ([SExpr], SExpr)
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
getBVals :: m [([SExpr], SExpr)]
getBVals :: m [([SExpr], SExpr)]
getBVals = ([SExpr] -> m ([SExpr], SExpr))
-> [[SExpr]] -> m [([SExpr], SExpr)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM [SExpr] -> m ([SExpr], SExpr)
getBVal ([[SExpr]] -> m [([SExpr], SExpr)])
-> [[SExpr]] -> m [([SExpr], SExpr)]
forall a b. (a -> b) -> a -> b
$ Key -> [SExpr] -> [[SExpr]]
forall (m :: * -> *) a. Applicative m => Key -> m a -> m [a]
replicateM Key
nArgs [SExpr
falseSExpr, SExpr
trueSExpr]
tryPointWise :: m (Maybe ([([SExpr], SExpr)], SExpr))
tryPointWise
| Bool -> Bool
not Bool
isBoolFunc
= Maybe ([([SExpr], SExpr)], SExpr)
-> m (Maybe ([([SExpr], SExpr)], SExpr))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe ([([SExpr], SExpr)], SExpr)
forall a. Maybe a
Nothing
| Key
nArgs Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
< Key
1
= String -> m (Maybe ([([SExpr], SExpr)], SExpr))
forall a. HasCallStack => String -> a
error (String -> m (Maybe ([([SExpr], SExpr)], SExpr)))
-> String -> m (Maybe ([([SExpr], SExpr)], SExpr))
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.pointWiseExtract: Impossible happened, nArgs < 1: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
nArgs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVType -> String
forall a. Show a => a -> String
show SBVType
typ
| Bool
True
= do [([SExpr], SExpr)]
vs <- m [([SExpr], SExpr)]
getBVals
let ([([SExpr], SExpr)]
trues, [([SExpr], SExpr)]
falses) = (([SExpr], SExpr) -> Bool)
-> [([SExpr], SExpr)] -> ([([SExpr], SExpr)], [([SExpr], SExpr)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\([SExpr]
_, SExpr
v) -> SExpr -> Bool
isTrueSExpr SExpr
v) [([SExpr], SExpr)]
vs
Maybe ([([SExpr], SExpr)], SExpr)
-> m (Maybe ([([SExpr], SExpr)], SExpr))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe ([([SExpr], SExpr)], SExpr)
-> m (Maybe ([([SExpr], SExpr)], SExpr)))
-> Maybe ([([SExpr], SExpr)], SExpr)
-> m (Maybe ([([SExpr], SExpr)], SExpr))
forall a b. (a -> b) -> a -> b
$ ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
forall a. a -> Maybe a
Just (([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr))
-> ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
forall a b. (a -> b) -> a -> b
$ if [([SExpr], SExpr)] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [([SExpr], SExpr)]
trues Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
<= [([SExpr], SExpr)] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [([SExpr], SExpr)]
falses
then ([([SExpr], SExpr)]
trues, SExpr
falseSExpr)
else ([([SExpr], SExpr)]
falses, SExpr
trueSExpr)
mkArg :: forall a. Kind -> SBV a
mkArg :: Kind -> SBV a
mkArg Kind
k = case Kind -> Maybe CV
defaultKindedValue Kind
k of
Maybe CV
Nothing -> String -> SBV a
forall a. HasCallStack => String -> a
error (String -> SBV a) -> String -> SBV a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
, String
"*** Data.SBV.smtFunSaturate: Impossible happened!"
, String
"*** Unable to create a valid parameter for kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
, String
"*** Please report this as an SBV bug!"
]
Just CV
c -> SVal -> SBV a
forall a. SVal -> SBV a
SBV (SVal -> SBV a) -> SVal -> SBV a
forall a b. (a -> b) -> a -> b
$ Kind -> Either CV (Cached SV) -> SVal
SVal Kind
k (CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left CV
c)
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] = SExpr -> Maybe a
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a0
sexprToArg SBV a -> SBV r
_ [SExpr]
_ = Maybe a
forall a. Maybe a
Nothing
smtFunType :: (SBV a -> SBV r) -> SBVType
smtFunType SBV a -> SBV r
_ = [Kind] -> SBVType
SBVType [Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a), Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)]
smtFunSaturate :: (SBV a -> SBV r) -> SBV r
smtFunSaturate SBV a -> SBV r
f = SBV a -> SBV r
f (SBV a -> SBV r) -> SBV a -> SBV r
forall a b. (a -> b) -> a -> b
$ Kind -> SBV a
forall a. Kind -> SBV a
mkArg (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a))
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] = (,) (a -> b -> (a, b)) -> Maybe a -> Maybe (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a0 Maybe (b -> (a, b)) -> Maybe b -> Maybe (a, b)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a1
sexprToArg SBV a -> SBV b -> SBV r
_ [SExpr]
_ = Maybe (a, b)
forall a. Maybe a
Nothing
smtFunType :: (SBV a -> SBV b -> SBV r) -> SBVType
smtFunType SBV a -> SBV b -> SBV r
_ = [Kind] -> SBVType
SBVType [Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b), Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)]
smtFunSaturate :: (SBV a -> SBV b -> SBV r) -> SBV r
smtFunSaturate SBV a -> SBV b -> SBV r
f = SBV a -> SBV b -> SBV r
f (Kind -> SBV a
forall a. Kind -> SBV a
mkArg (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)))
(Kind -> SBV b
forall a. Kind -> SBV a
mkArg (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)))
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] = (,,) (a -> b -> c -> (a, b, c))
-> Maybe a -> Maybe (b -> c -> (a, b, c))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a0 Maybe (b -> c -> (a, b, c)) -> Maybe b -> Maybe (c -> (a, b, c))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a1 Maybe (c -> (a, b, c)) -> Maybe c -> Maybe (a, b, c)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe c
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a2
sexprToArg SBV a -> SBV b -> SBV c -> SBV r
_ [SExpr]
_ = Maybe (a, b, c)
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 [Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b), Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c), Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)]
smtFunSaturate :: (SBV a -> SBV b -> SBV c -> SBV r) -> SBV r
smtFunSaturate SBV a -> SBV b -> SBV c -> SBV r
f = SBV a -> SBV b -> SBV c -> SBV r
f (Kind -> SBV a
forall a. Kind -> SBV a
mkArg (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)))
(Kind -> SBV b
forall a. Kind -> SBV a
mkArg (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)))
(Kind -> SBV c
forall a. Kind -> SBV a
mkArg (Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c)))
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] = (,,,) (a -> b -> c -> d -> (a, b, c, d))
-> Maybe a -> Maybe (b -> c -> d -> (a, b, c, d))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a0 Maybe (b -> c -> d -> (a, b, c, d))
-> Maybe b -> Maybe (c -> d -> (a, b, c, d))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a1 Maybe (c -> d -> (a, b, c, d))
-> Maybe c -> Maybe (d -> (a, b, c, d))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe c
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a2 Maybe (d -> (a, b, c, d)) -> Maybe d -> Maybe (a, b, c, d)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe d
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a3
sexprToArg SBV a -> SBV b -> SBV c -> SBV d -> SBV r
_ [SExpr]
_ = Maybe (a, b, c, d)
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 [Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b), Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c), Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d), Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)]
smtFunSaturate :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV r) -> SBV r
smtFunSaturate SBV a -> SBV b -> SBV c -> SBV d -> SBV r
f = SBV a -> SBV b -> SBV c -> SBV d -> SBV r
f (Kind -> SBV a
forall a. Kind -> SBV a
mkArg (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)))
(Kind -> SBV b
forall a. Kind -> SBV a
mkArg (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)))
(Kind -> SBV c
forall a. Kind -> SBV a
mkArg (Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c)))
(Kind -> SBV d
forall a. Kind -> SBV a
mkArg (Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d)))
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] = (,,,,) (a -> b -> c -> d -> e -> (a, b, c, d, e))
-> Maybe a -> Maybe (b -> c -> d -> e -> (a, b, c, d, e))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a0 Maybe (b -> c -> d -> e -> (a, b, c, d, e))
-> Maybe b -> Maybe (c -> d -> e -> (a, b, c, d, e))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a1 Maybe (c -> d -> e -> (a, b, c, d, e))
-> Maybe c -> Maybe (d -> e -> (a, b, c, d, e))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe c
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a2 Maybe (d -> e -> (a, b, c, d, e))
-> Maybe d -> Maybe (e -> (a, b, c, d, e))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe d
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a3 Maybe (e -> (a, b, c, d, e)) -> Maybe e -> Maybe (a, b, c, d, e)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe e
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a4
sexprToArg SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r
_ [SExpr]
_ = Maybe (a, b, c, d, e)
forall a. Maybe a
Nothing
smtFunType :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r) -> SBVType
smtFunType SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r
_ = [Kind] -> SBVType
SBVType [Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b), Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c), Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d), Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy e
forall k (t :: k). Proxy t
Proxy @e), Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)]
smtFunSaturate :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r) -> SBV r
smtFunSaturate SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r
f = SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV r
f (Kind -> SBV a
forall a. Kind -> SBV a
mkArg (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)))
(Kind -> SBV b
forall a. Kind -> SBV a
mkArg (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)))
(Kind -> SBV c
forall a. Kind -> SBV a
mkArg (Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c)))
(Kind -> SBV d
forall a. Kind -> SBV a
mkArg (Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d)))
(Kind -> SBV e
forall a. Kind -> SBV a
mkArg (Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy e
forall k (t :: k). Proxy t
Proxy @e)))
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] = (,,,,,) (a -> b -> c -> d -> e -> f -> (a, b, c, d, e, f))
-> Maybe a -> Maybe (b -> c -> d -> e -> f -> (a, b, c, d, e, f))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a0 Maybe (b -> c -> d -> e -> f -> (a, b, c, d, e, f))
-> Maybe b -> Maybe (c -> d -> e -> f -> (a, b, c, d, e, f))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a1 Maybe (c -> d -> e -> f -> (a, b, c, d, e, f))
-> Maybe c -> Maybe (d -> e -> f -> (a, b, c, d, e, f))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe c
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a2 Maybe (d -> e -> f -> (a, b, c, d, e, f))
-> Maybe d -> Maybe (e -> f -> (a, b, c, d, e, f))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe d
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a3 Maybe (e -> f -> (a, b, c, d, e, f))
-> Maybe e -> Maybe (f -> (a, b, c, d, e, f))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe e
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a4 Maybe (f -> (a, b, c, d, e, f))
-> Maybe f -> Maybe (a, b, c, d, e, f)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe f
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a5
sexprToArg SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r
_ [SExpr]
_ = Maybe (a, b, c, d, e, f)
forall a. Maybe a
Nothing
smtFunType :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r)
-> SBVType
smtFunType SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r
_ = [Kind] -> SBVType
SBVType [Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b), Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c), Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d), Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy e
forall k (t :: k). Proxy t
Proxy @e), Proxy f -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy f
forall k (t :: k). Proxy t
Proxy @f), Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)]
smtFunSaturate :: (SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r)
-> SBV r
smtFunSaturate SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r
f = SBV a -> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV r
f (Kind -> SBV a
forall a. Kind -> SBV a
mkArg (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)))
(Kind -> SBV b
forall a. Kind -> SBV a
mkArg (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)))
(Kind -> SBV c
forall a. Kind -> SBV a
mkArg (Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c)))
(Kind -> SBV d
forall a. Kind -> SBV a
mkArg (Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d)))
(Kind -> SBV e
forall a. Kind -> SBV a
mkArg (Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy e
forall k (t :: k). Proxy t
Proxy @e)))
(Kind -> SBV f
forall a. Kind -> SBV a
mkArg (Proxy f -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy f
forall k (t :: k). Proxy t
Proxy @f)))
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] = (,,,,,,) (a -> b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> Maybe a
-> Maybe (b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a0 Maybe (b -> c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> Maybe b
-> Maybe (c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a1 Maybe (c -> d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> Maybe c -> Maybe (d -> e -> f -> g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe c
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a2 Maybe (d -> e -> f -> g -> (a, b, c, d, e, f, g))
-> Maybe d -> Maybe (e -> f -> g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe d
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a3 Maybe (e -> f -> g -> (a, b, c, d, e, f, g))
-> Maybe e -> Maybe (f -> g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe e
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a4 Maybe (f -> g -> (a, b, c, d, e, f, g))
-> Maybe f -> Maybe (g -> (a, b, c, d, e, f, g))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe f
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a5 Maybe (g -> (a, b, c, d, e, f, g))
-> Maybe g -> Maybe (a, b, c, d, e, f, g)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe g
forall a. 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]
_ = Maybe (a, b, c, d, e, f, g)
forall a. Maybe a
Nothing
smtFunType :: (SBV a
-> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r)
-> SBVType
smtFunType SBV a
-> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r
_ = [Kind] -> SBVType
SBVType [Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b), Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c), Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d), Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy e
forall k (t :: k). Proxy t
Proxy @e), Proxy f -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy f
forall k (t :: k). Proxy t
Proxy @f), Proxy g -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy g
forall k (t :: k). Proxy t
Proxy @g), Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)]
smtFunSaturate :: (SBV a
-> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r)
-> SBV r
smtFunSaturate SBV a
-> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r
f = SBV a
-> SBV b -> SBV c -> SBV d -> SBV e -> SBV f -> SBV g -> SBV r
f (Kind -> SBV a
forall a. Kind -> SBV a
mkArg (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)))
(Kind -> SBV b
forall a. Kind -> SBV a
mkArg (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)))
(Kind -> SBV c
forall a. Kind -> SBV a
mkArg (Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c)))
(Kind -> SBV d
forall a. Kind -> SBV a
mkArg (Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d)))
(Kind -> SBV e
forall a. Kind -> SBV a
mkArg (Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy e
forall k (t :: k). Proxy t
Proxy @e)))
(Kind -> SBV f
forall a. Kind -> SBV a
mkArg (Proxy f -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy f
forall k (t :: k). Proxy t
Proxy @f)))
(Kind -> SBV g
forall a. Kind -> SBV a
mkArg (Proxy g -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy g
forall k (t :: k). Proxy t
Proxy @g)))
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] = (,,,,,,,) (a -> b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe a
-> Maybe
(b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SExpr -> Maybe a
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a0 Maybe (b -> c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe b
-> Maybe (c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe b
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a1 Maybe (c -> d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe c
-> Maybe (d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe c
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a2 Maybe (d -> e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe d -> Maybe (e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe d
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a3 Maybe (e -> f -> g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe e -> Maybe (f -> g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe e
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a4 Maybe (f -> g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe f -> Maybe (g -> h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe f
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a5 Maybe (g -> h -> (a, b, c, d, e, f, g, h))
-> Maybe g -> Maybe (h -> (a, b, c, d, e, f, g, h))
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe g
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
a6 Maybe (h -> (a, b, c, d, e, f, g, h))
-> Maybe h -> Maybe (a, b, c, d, e, f, g, h)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe h
forall a. 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]
_ = Maybe (a, b, c, d, e, f, g, h)
forall a. Maybe a
Nothing
smtFunType :: (SBV a
-> SBV b
-> SBV c
-> SBV d
-> SBV e
-> SBV f
-> SBV g
-> SBV h
-> SBV r)
-> SBVType
smtFunType SBV a
-> SBV b
-> SBV c
-> SBV d
-> SBV e
-> SBV f
-> SBV g
-> SBV h
-> SBV r
_ = [Kind] -> SBVType
SBVType [Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a), Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b), Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c), Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d), Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy e
forall k (t :: k). Proxy t
Proxy @e), Proxy f -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy f
forall k (t :: k). Proxy t
Proxy @f), Proxy g -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy g
forall k (t :: k). Proxy t
Proxy @g), Proxy h -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy h
forall k (t :: k). Proxy t
Proxy @h), Proxy r -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy r
forall k (t :: k). Proxy t
Proxy @r)]
smtFunSaturate :: (SBV a
-> SBV b
-> SBV c
-> SBV d
-> SBV e
-> SBV f
-> SBV g
-> SBV h
-> SBV r)
-> SBV r
smtFunSaturate SBV a
-> SBV b
-> SBV c
-> SBV d
-> SBV e
-> SBV f
-> SBV g
-> SBV h
-> SBV r
f = SBV a
-> SBV b
-> SBV c
-> SBV d
-> SBV e
-> SBV f
-> SBV g
-> SBV h
-> SBV r
f (Kind -> SBV a
forall a. Kind -> SBV a
mkArg (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)))
(Kind -> SBV b
forall a. Kind -> SBV a
mkArg (Proxy b -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy b
forall k (t :: k). Proxy t
Proxy @b)))
(Kind -> SBV c
forall a. Kind -> SBV a
mkArg (Proxy c -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy c
forall k (t :: k). Proxy t
Proxy @c)))
(Kind -> SBV d
forall a. Kind -> SBV a
mkArg (Proxy d -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy d
forall k (t :: k). Proxy t
Proxy @d)))
(Kind -> SBV e
forall a. Kind -> SBV a
mkArg (Proxy e -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy e
forall k (t :: k). Proxy t
Proxy @e)))
(Kind -> SBV f
forall a. Kind -> SBV a
mkArg (Proxy f -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy f
forall k (t :: k). Proxy t
Proxy @f)))
(Kind -> SBV g
forall a. Kind -> SBV a
mkArg (Proxy g -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy g
forall k (t :: k). Proxy t
Proxy @g)))
(Kind -> SBV h
forall a. Kind -> SBV a
mkArg (Proxy h -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy h
forall k (t :: k). Proxy t
Proxy @h)))
getFunction :: (MonadIO m, MonadQuery m, SolverContext m, MonadSymbolic m, SymVal a, SymVal r, SMTFunction fun a r) => fun -> m ([(a, r)], r)
getFunction :: fun -> m ([(a, r)], r)
getFunction fun
f = do String
nm <- fun -> m String
forall fun a r (m :: * -> *).
(SMTFunction fun a r, MonadIO m, SolverContext m,
MonadSymbolic m) =>
fun -> m String
smtFunName fun
f
let cmd :: String
cmd = String
"(get-value (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getFunction" String
cmd String
"a function value" Maybe [String]
forall a. Maybe a
Nothing
String
r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd
String
-> (String -> Maybe [String] -> m ([(a, r)], r))
-> (SExpr -> m ([(a, r)], r))
-> m ([(a, r)], r)
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m ([(a, r)], r)
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m ([(a, r)], r)) -> m ([(a, r)], r))
-> (SExpr -> m ([(a, r)], r)) -> m ([(a, r)], r)
forall a b. (a -> b) -> a -> b
$ \case EApp [EApp [ECon String
o, SExpr
e]] | String
o String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
nm -> do Maybe ([(a, r)], r)
mbAssocs <- fun -> SExpr -> m (Maybe ([(a, r)], r))
forall fun a r (m :: * -> *).
(SMTFunction fun a r, MonadIO m, SolverContext m, MonadQuery m,
MonadSymbolic m, 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 -> ([(a, r)], r) -> m ([(a, r)], r)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(a, r)], r)
assocs
Maybe ([(a, r)], r)
Nothing -> do Maybe ([([SExpr], SExpr)], SExpr)
mbPVS <- String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
pointWiseExtract String
nm (fun -> SBVType
forall fun a r. SMTFunction fun a r => fun -> SBVType
smtFunType fun
f)
case Maybe ([([SExpr], SExpr)], SExpr)
mbPVS Maybe ([([SExpr], SExpr)], SExpr)
-> (([([SExpr], SExpr)], SExpr) -> Maybe ([(a, r)], r))
-> Maybe ([(a, r)], r)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= ([([SExpr], SExpr)], SExpr) -> Maybe ([(a, r)], r)
forall (t :: * -> *) a r a a.
(Traversable t, SMTFunction fun a r, SymVal a, SymVal a) =>
(t ([SExpr], SExpr), SExpr) -> Maybe (t (a, a), a)
convert of
Just ([(a, r)], r)
x -> ([(a, r)], r) -> m ([(a, r)], r)
forall (m :: * -> *) a. Monad m => a -> m a
return ([(a, r)], r)
x
Maybe ([(a, r)], r)
Nothing -> String -> Maybe [String] -> m ([(a, r)], r)
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
SExpr
_ -> String -> Maybe [String] -> m ([(a, r)], r)
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
where convert :: (t ([SExpr], SExpr), SExpr) -> Maybe (t (a, a), a)
convert (t ([SExpr], SExpr)
vs, SExpr
d) = (,) (t (a, a) -> a -> (t (a, a), a))
-> Maybe (t (a, a)) -> Maybe (a -> (t (a, a), a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (([SExpr], SExpr) -> Maybe (a, a))
-> t ([SExpr], SExpr) -> Maybe (t (a, a))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([SExpr], SExpr) -> Maybe (a, a)
forall a r a.
(SMTFunction fun a r, SymVal a) =>
([SExpr], SExpr) -> Maybe (a, a)
sexprPoint t ([SExpr], SExpr)
vs Maybe (a -> (t (a, a), a)) -> Maybe a -> Maybe (t (a, a), a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe a
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
d
sexprPoint :: ([SExpr], SExpr) -> Maybe (a, a)
sexprPoint ([SExpr]
as, SExpr
v) = (,) (a -> a -> (a, a)) -> Maybe a -> Maybe (a -> (a, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> fun -> [SExpr] -> Maybe a
forall fun a r. SMTFunction fun a r => fun -> [SExpr] -> Maybe a
sexprToArg fun
f [SExpr]
as Maybe (a -> (a, a)) -> Maybe a -> Maybe (a, a)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe a
forall a. SymVal a => SExpr -> Maybe a
sexprToVal SExpr
v
getUninterpretedValue :: (MonadIO m, MonadQuery m, HasKind a) => SBV a -> m String
getUninterpretedValue :: SBV a -> m String
getUninterpretedValue SBV a
s =
case SBV a -> Kind
forall a. HasKind a => a -> Kind
kindOf SBV a
s of
KUserSort String
_ Maybe [String]
Nothing -> do SV
sv <- (State -> IO SV) -> m SV
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
(State -> IO a) -> m a
inNewContext (State -> SBV a -> IO SV
forall a. State -> SBV a -> IO SV
`sbvToSV` SBV a
s)
let nm :: String
nm = SV -> String
forall a. Show a => a -> String
show SV
sv
cmd :: String
cmd = String
"(get-value (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getValue" String
cmd String
"a model value" Maybe [String]
forall a. Maybe a
Nothing
String
r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd
String
-> (String -> Maybe [String] -> m String)
-> (SExpr -> m String)
-> m String
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m String
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m String) -> m String)
-> (SExpr -> m String) -> m String
forall a b. (a -> b) -> a -> b
$ \case EApp [EApp [ECon String
o, ECon String
v]] | String
o String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== SV -> String
forall a. Show a => a -> String
show SV
sv -> String -> m String
forall (m :: * -> *) a. Monad m => a -> m a
return String
v
SExpr
_ -> String -> Maybe [String] -> m String
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
Kind
k -> String -> m String
forall a. HasCallStack => String -> a
error (String -> m String) -> String -> m String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String
""
, String
"*** SBV.getUninterpretedValue: Called on an 'interpreted' kind"
, String
"*** "
, String
"*** Kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
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.'"
]
getValueCVHelper :: (MonadIO m, MonadQuery m) => Maybe Int -> SV -> m CV
getValueCVHelper :: Maybe Key -> SV -> m CV
getValueCVHelper Maybe Key
mbi SV
s
| SV
s SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV
= CV -> m CV
forall (m :: * -> *) a. Monad m => a -> m a
return CV
trueCV
| SV
s SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV
= CV -> m CV
forall (m :: * -> *) a. Monad m => a -> m a
return CV
falseCV
| Bool
True
= Maybe Key -> String -> Kind -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> String -> Kind -> m CV
extractValue Maybe Key
mbi (SV -> String
forall a. Show a => a -> String
show SV
s) (SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
s)
defaultKindedValue :: Kind -> Maybe CV
defaultKindedValue :: Kind -> Maybe CV
defaultKindedValue Kind
k = Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> Maybe CVal -> Maybe CV
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind -> Maybe CVal
cvt Kind
k
where cvt :: Kind -> Maybe CVal
cvt :: Kind -> Maybe CVal
cvt Kind
KBool = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ Integer -> CVal
CInteger Integer
0
cvt KBounded{} = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ Integer -> CVal
CInteger Integer
0
cvt Kind
KUnbounded = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ Integer -> CVal
CInteger Integer
0
cvt Kind
KReal = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ AlgReal -> CVal
CAlgReal AlgReal
0
cvt (KUserSort String
_ Maybe [String]
ui) = Maybe [String] -> Maybe CVal
uninterp Maybe [String]
ui
cvt Kind
KFloat = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ Float -> CVal
CFloat Float
0
cvt Kind
KDouble = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ Double -> CVal
CDouble Double
0
cvt Kind
KRational = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ Rational -> CVal
CRational Rational
0
cvt (KFP Key
eb Key
sb) = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ FP -> CVal
CFP (Bool -> Key -> Key -> FP
fpZero Bool
False Key
eb Key
sb)
cvt Kind
KChar = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ Char -> CVal
CChar Char
'\NUL'
cvt Kind
KString = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ String -> CVal
CString String
""
cvt (KList Kind
_) = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ [CVal] -> CVal
CList []
cvt (KSet Kind
_) = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ RCSet CVal -> CVal
CSet (RCSet CVal -> CVal) -> RCSet CVal -> CVal
forall a b. (a -> b) -> a -> b
$ Set CVal -> RCSet CVal
forall a. Set a -> RCSet a
RegularSet Set CVal
forall a. Set a
Set.empty
cvt (KTuple [Kind]
ks) = [CVal] -> CVal
CTuple ([CVal] -> CVal) -> Maybe [CVal] -> Maybe CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Kind -> Maybe CVal) -> [Kind] -> Maybe [CVal]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM Kind -> Maybe CVal
cvt [Kind]
ks
cvt (KMaybe Kind
_) = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ Maybe CVal -> CVal
CMaybe Maybe CVal
forall a. Maybe a
Nothing
cvt (KEither Kind
k1 Kind
_) = Either CVal CVal -> CVal
CEither (Either CVal CVal -> CVal)
-> (CVal -> Either CVal CVal) -> CVal -> CVal
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CVal -> Either CVal CVal
forall a b. a -> Either a b
Left (CVal -> CVal) -> Maybe CVal -> Maybe CVal
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind -> Maybe CVal
cvt Kind
k1
uninterp :: Maybe [String] -> Maybe CVal
uninterp (Just (String
c:[String]
_)) = CVal -> Maybe CVal
forall a. a -> Maybe a
Just (CVal -> Maybe CVal) -> CVal -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ (Maybe Key, String) -> CVal
CUserSort (Key -> Maybe Key
forall a. a -> Maybe a
Just Key
1, String
c)
uninterp (Just []) = Maybe CVal
forall a. Maybe a
Nothing
uninterp Maybe [String]
Nothing = Maybe CVal
forall a. Maybe a
Nothing
sexprToVal :: forall a. SymVal a => SExpr -> Maybe a
sexprToVal :: SExpr -> Maybe a
sexprToVal SExpr
e = CV -> a
forall a. SymVal a => CV -> a
fromCV (CV -> a) -> Maybe CV -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Kind -> SExpr -> Maybe CV
recoverKindedValue (Proxy a -> Kind
forall a. HasKind a => a -> Kind
kindOf (Proxy a
forall k (t :: k). Proxy t
Proxy @a)) SExpr
e
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 Key
_) <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k Integer
i
| Bool
True -> Maybe CV
forall a. Maybe a
Nothing
KBounded{} | ENum (Integer
i, Maybe Key
_) <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k Integer
i
| Bool
True -> Maybe CV
forall a. Maybe a
Nothing
Kind
KUnbounded | ENum (Integer
i, Maybe Key
_) <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k Integer
i
| Bool
True -> Maybe CV
forall a. Maybe a
Nothing
Kind
KReal | ENum (Integer
i, Maybe Key
_) <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k Integer
i
| EReal AlgReal
i <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KReal (AlgReal -> CVal
CAlgReal AlgReal
i)
| Bool
True -> SExpr -> Maybe CV
interpretInterval SExpr
e
KUserSort{} | ECon String
s <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ (Maybe Key, String) -> CVal
CUserSort (Kind -> String -> Maybe Key
getUIIndex Kind
k String
s, String
s)
| Bool
True -> Maybe CV
forall a. Maybe a
Nothing
Kind
KFloat | ENum (Integer
i, Maybe Key
_) <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k Integer
i
| EFloat Float
i <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KFloat (Float -> CVal
CFloat Float
i)
| Bool
True -> Maybe CV
forall a. Maybe a
Nothing
Kind
KDouble | ENum (Integer
i, Maybe Key
_) <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k Integer
i
| EDouble Double
i <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KDouble (Double -> CVal
CDouble Double
i)
| Bool
True -> Maybe CV
forall a. Maybe a
Nothing
KFP Key
eb Key
sb | ENum (Integer
i, Maybe Key
_) <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ FP -> CVal
CFP (FP -> CVal) -> FP -> CVal
forall a b. (a -> b) -> a -> b
$ Key -> Key -> Integer -> FP
fpFromInteger Key
eb Key
sb Integer
i
| EFloat Float
f <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ FP -> CVal
CFP (FP -> CVal) -> FP -> CVal
forall a b. (a -> b) -> a -> b
$ Key -> Key -> Float -> FP
fpFromFloat Key
eb Key
sb Float
f
| EDouble Double
d <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ FP -> CVal
CFP (FP -> CVal) -> FP -> CVal
forall a b. (a -> b) -> a -> b
$ Key -> Key -> Double -> FP
fpFromDouble Key
eb Key
sb Double
d
| EFloatingPoint FP
c <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ FP -> CVal
CFP FP
c
| Bool
True -> Maybe CV
forall a. Maybe a
Nothing
Kind
KChar | ECon String
s <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KChar (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ Char -> CVal
CChar (Char -> CVal) -> Char -> CVal
forall a b. (a -> b) -> a -> b
$ String -> Char
interpretChar String
s
| Bool
True -> Maybe CV
forall a. Maybe a
Nothing
Kind
KString | ECon String
s <- SExpr
e -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KString (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ String -> CVal
CString (String -> CVal) -> String -> CVal
forall a b. (a -> b) -> a -> b
$ String -> String
interpretString String
s
| Bool
True -> Maybe CV
forall a. Maybe a
Nothing
Kind
KRational -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ Rational -> CVal
CRational (Rational -> CVal) -> Rational -> CVal
forall a b. (a -> b) -> a -> b
$ SExpr -> Rational
interpretRational SExpr
e
KList Kind
ek -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ [CVal] -> CVal
CList ([CVal] -> CVal) -> [CVal] -> CVal
forall a b. (a -> b) -> a -> b
$ Kind -> SExpr -> [CVal]
interpretList Kind
ek SExpr
e
KSet Kind
ek -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ RCSet CVal -> CVal
CSet (RCSet CVal -> CVal) -> RCSet CVal -> CVal
forall a b. (a -> b) -> a -> b
$ Kind -> SExpr -> RCSet CVal
interpretSet Kind
ek SExpr
e
KTuple{} -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ [CVal] -> CVal
CTuple ([CVal] -> CVal) -> [CVal] -> CVal
forall a b. (a -> b) -> a -> b
$ SExpr -> [CVal]
interpretTuple SExpr
e
KMaybe{} -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ Maybe CVal -> CVal
CMaybe (Maybe CVal -> CVal) -> Maybe CVal -> CVal
forall a b. (a -> b) -> a -> b
$ Kind -> SExpr -> Maybe CVal
interpretMaybe Kind
k SExpr
e
KEither{} -> CV -> Maybe CV
forall a. a -> Maybe a
Just (CV -> Maybe CV) -> CV -> Maybe CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
k (CVal -> CV) -> CVal -> CV
forall a b. (a -> b) -> a -> b
$ Either CVal CVal -> CVal
CEither (Either CVal CVal -> CVal) -> Either CVal CVal -> CVal
forall a b. (a -> b) -> a -> b
$ Kind -> SExpr -> Either CVal CVal
interpretEither Kind
k SExpr
e
where getUIIndex :: Kind -> String -> Maybe Key
getUIIndex (KUserSort String
_ (Just [String]
xs)) String
i = String
i String -> [String] -> Maybe Key
forall a. Eq a => a -> [a] -> Maybe Key
`elemIndex` [String]
xs
getUIIndex Kind
_ String
_ = Maybe Key
forall a. Maybe a
Nothing
stringLike :: String -> Bool
stringLike String
xs = String -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length String
xs Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
>= Key
2 Bool -> Bool -> Bool
&& String -> Char
forall a. [a] -> a
head String
xs Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'"' Bool -> Bool -> Bool
&& String -> Char
forall a. [a] -> a
last String
xs Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'"'
interpretString :: String -> String
interpretString String
xs
| Bool -> Bool
not (String -> Bool
stringLike String
xs)
= String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"Expected a string constant with quotes, received: <" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
">"
| Bool
True
= String -> String
qfsToString (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String
forall a. [a] -> [a]
tail (String -> String
forall a. [a] -> [a]
init String
xs)
interpretChar :: String -> Char
interpretChar String
xs = case String -> String
interpretString String
xs of
[Char
c] -> Char
c
String
_ -> String -> Char
forall a. HasCallStack => String -> a
error (String -> Char) -> String -> Char
forall a b. (a -> b) -> a -> b
$ String
"Expected a singleton char constant, received: <" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
xs String -> String -> String
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 Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
d
interpretRational SExpr
xs = String -> Rational
forall a. HasCallStack => String -> a
error (String -> Rational) -> String -> Rational
forall a b. (a -> b) -> a -> b
$ String
"Expected a rational constant, received: <" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
xs String -> String -> String
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 -> String -> [CVal]
forall a. HasCallStack => String -> a
error (String -> [CVal]) -> String -> [CVal]
forall a b. (a -> b) -> a -> b
$ String
"Cannot parse a sequence item of kind " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
ek String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" from: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
extra SExpr
v
walk (EApp (ECon String
"seq.++" : [SExpr]
rest)) = (SExpr -> [CVal]) -> [SExpr] -> [CVal]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SExpr -> [CVal]
walk [SExpr]
rest
walk SExpr
cur = String -> [CVal]
forall a. HasCallStack => String -> a
error (String -> [CVal]) -> String -> [CVal]
forall a b. (a -> b) -> a -> b
$ String
"Expected a sequence constant, but received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
cur String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
extra SExpr
cur
extra :: a -> String
extra a
cur | a -> String
forall a. Show a => a -> String
show a
cur String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
t = String
""
| Bool
True = String
"\nWhile parsing: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
where t :: String
t = SExpr -> String
forall a. Show a => a -> String
show SExpr
topExpr
interpretSet :: Kind -> SExpr -> RCSet CVal
interpretSet Kind
ke SExpr
setExpr
| SExpr -> Bool
isUniversal SExpr
setExpr = Set CVal -> RCSet CVal
forall a. Set a -> RCSet a
ComplementSet Set CVal
forall a. Set a
Set.empty
| SExpr -> Bool
isEmpty SExpr
setExpr = Set CVal -> RCSet CVal
forall a. Set a -> RCSet a
RegularSet Set CVal
forall a. Set a
Set.empty
| Just (Right ([([SExpr], SExpr)], SExpr)
assocs) <- Maybe (Either String ([([SExpr], SExpr)], SExpr))
mbAssocs = ([([SExpr], SExpr)], SExpr) -> RCSet CVal
forall (t :: * -> *).
Foldable t =>
(t ([SExpr], SExpr), SExpr) -> RCSet CVal
decode ([([SExpr], SExpr)], SExpr)
assocs
| Bool
True = String -> RCSet CVal
forall a. String -> a
tbd String
"Expected a set value, but couldn't decipher the solver output."
where tbd :: String -> a
tbd String
w = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
, String
"*** Data.SBV.interpretSet: Unable to process solver output."
, String
"***"
, String
"*** Kind : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show (Kind -> Kind
KSet Kind
ke)
, String
"*** Received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
setExpr
, String
"*** Reason : " String -> String -> String
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 Key
Nothing)) = Bool
True
isTrue (ENum (Integer
0, Maybe Key
Nothing)) = Bool
False
isTrue SExpr
bad = String -> Bool
forall a. String -> a
tbd (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"Non-boolean membership value seen: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
bad
isUniversal :: SExpr -> Bool
isUniversal (EApp [EApp [ECon 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 (Bool -> Bool) -> Bool -> Bool
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 = Set CVal -> RCSet CVal
forall a. Set a -> RCSet a
ComplementSet (Set CVal -> RCSet CVal) -> Set CVal -> RCSet CVal
forall a b. (a -> b) -> a -> b
$ [CVal] -> Set CVal
forall a. Ord a => [a] -> Set a
Set.fromList [CVal
x | (CVal
x, Bool
False) <- (([SExpr], SExpr) -> [(CVal, Bool)])
-> t ([SExpr], SExpr) -> [(CVal, Bool)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Bool -> ([SExpr], SExpr) -> [(CVal, Bool)]
contents Bool
True) t ([SExpr], SExpr)
args]
| Bool
True = Set CVal -> RCSet CVal
forall a. Set a -> RCSet a
RegularSet (Set CVal -> RCSet CVal) -> Set CVal -> RCSet CVal
forall a b. (a -> b) -> a -> b
$ [CVal] -> Set CVal
forall a. Ord a => [a] -> Set a
Set.fromList [CVal
x | (CVal
x, Bool
True) <- (([SExpr], SExpr) -> [(CVal, Bool)])
-> t ([SExpr], SExpr) -> [(CVal, Bool)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Bool -> ([SExpr], SExpr) -> [(CVal, Bool)]
contents Bool
False) t ([SExpr], SExpr)
args]
contents :: Bool -> ([SExpr], SExpr) -> [(CVal, Bool)]
contents Bool
cvt ([SExpr
v], SExpr
r) = let t :: Bool
t = SExpr -> Bool
isTrue SExpr
r in (CVal -> (CVal, Bool)) -> [CVal] -> [(CVal, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map (, Bool
t) (Bool -> SExpr -> [CVal]
element Bool
cvt SExpr
v)
contents Bool
_ ([SExpr], SExpr)
bad = String -> [(CVal, Bool)]
forall a. String -> a
tbd (String -> [(CVal, Bool)]) -> String -> [(CVal, Bool)]
forall a b. (a -> b) -> a -> b
$ String
"Multi-valued set member seen: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([SExpr], SExpr) -> String
forall a. Show a => a -> String
show ([SExpr], SExpr)
bad
element :: 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
_ -> String -> [CVal]
forall a. String -> a
tbd (String -> [CVal]) -> String -> [CVal]
forall a b. (a -> b) -> a -> b
$ String
"Unexpected value for kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (SExpr, Kind) -> String
forall a. Show a => a -> String
show (SExpr
x, Kind
ke)
Maybe CV
Nothing -> String -> [CVal]
forall a. String -> a
tbd (String -> [CVal]) -> String -> [CVal]
forall a b. (a -> b) -> a -> b
$ String
"Unexpected value for kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (SExpr, Kind) -> String
forall a. Show a => a -> String
show (SExpr
x, Kind
ke)
(Bool, Kind)
_ -> case Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
ke SExpr
x of
Just CV
v -> [CV -> CVal
cvVal CV
v]
Maybe CV
Nothing -> String -> [CVal]
forall a. String -> a
tbd (String -> [CVal]) -> String -> [CVal]
forall a b. (a -> b) -> a -> b
$ String
"Unexpected value for kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (SExpr, Kind) -> String
forall a. Show a => a -> String
show (SExpr
x, Kind
ke)
interpretTuple :: SExpr -> [CVal]
interpretTuple SExpr
te = Key -> [Maybe CV] -> [CVal] -> [CVal]
forall a. (Num a, Show a) => a -> [Maybe CV] -> [CVal] -> [CVal]
walk (Key
1 :: Int) ((Kind -> SExpr -> Maybe CV) -> [Kind] -> [SExpr] -> [Maybe CV]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Kind -> SExpr -> Maybe CV
recoverKindedValue [Kind]
ks [SExpr]
args) []
where ([Kind]
ks, Key
n) = case Kind
k of
KTuple [Kind]
eks -> ([Kind]
eks, [Kind] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [Kind]
eks)
Kind
_ -> String -> ([Kind], Key)
forall a. HasCallStack => String -> a
error (String -> ([Kind], Key)) -> String -> ([Kind], Key)
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Impossible: Expected a tuple kind, but got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
, String
"While trying to parse: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
te
]
args :: [SExpr]
args = SExpr -> [SExpr]
try SExpr
te
where
try :: SExpr -> [SExpr]
try (EApp (ECon String
f : [SExpr]
as)) = case Key -> String -> (String, String)
forall a. Key -> [a] -> ([a], [a])
splitAt (Text -> Key
T.length Text
"mkSBVTuple") String
f of
(String
"mkSBVTuple", String
c) | (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit String
c Bool -> Bool -> Bool
&& String -> Key
forall a. Read a => String -> a
read String
c Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
n Bool -> Bool -> Bool
&& [SExpr] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [SExpr]
as Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
n -> [SExpr]
as
(String, String)
_ -> [SExpr]
forall a. a
bad
try (EApp (EApp [ECon String
"as", ECon String
f, SExpr
_] : [SExpr]
as)) = SExpr -> [SExpr]
try ([SExpr] -> SExpr
EApp (String -> SExpr
ECon String
f SExpr -> [SExpr] -> [SExpr]
forall a. a -> [a] -> [a]
: [SExpr]
as))
try SExpr
_ = [SExpr]
forall a. a
bad
bad :: a
bad = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.sexprToTuple: Impossible: Expected a constructor for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" tuple, but got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
te
walk :: a -> [Maybe CV] -> [CVal] -> [CVal]
walk a
_ [] [CVal]
sofar = [CVal] -> [CVal]
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
ia -> a -> a
forall a. Num a => a -> a -> a
+a
1) [Maybe CV]
es (CV -> CVal
cvVal CV
el CVal -> [CVal] -> [CVal]
forall a. a -> [a] -> [a]
: [CVal]
sofar)
walk a
i (Maybe CV
Nothing:[Maybe CV]
_) [CVal]
_ = String -> [CVal]
forall a. HasCallStack => String -> a
error (String -> [CVal]) -> String -> [CVal]
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Couldn't parse a tuple element at position " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i
, String
"Kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
, String
"Expr: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
te
]
interpretMaybe :: Kind -> SExpr -> Maybe CVal
interpretMaybe (KMaybe Kind
_) (ECon String
"nothing_SBVMaybe") = Maybe CVal
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) -> CVal -> Maybe CVal
forall a. a -> Maybe a
Just CVal
v
Maybe CV
Nothing -> String -> Maybe CVal
forall a. HasCallStack => String -> a
error (String -> Maybe CVal) -> String -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Couldn't parse a maybe just value"
, String
"Kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
ek
, String
"Expr: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
a
]
interpretMaybe Kind
_ ( EApp [ECon String
"as", ECon String
"nothing_SBVMaybe", SExpr
_]) = Maybe CVal
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 = String -> Maybe CVal
forall a. HasCallStack => String -> a
error (String -> Maybe CVal) -> String -> Maybe CVal
forall a b. (a -> b) -> a -> b
$ String
"Expected an SMaybe sexpr, but received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Kind, SExpr) -> String
forall a. Show a => a -> String
show (Kind
k, SExpr
other)
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) -> CVal -> Either CVal CVal
forall a b. a -> Either a b
Left CVal
v
Maybe CV
Nothing -> String -> Either CVal CVal
forall a. HasCallStack => String -> a
error (String -> Either CVal CVal) -> String -> Either CVal CVal
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Couldn't parse an either value on the left"
, String
"Kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k1
, String
"Expr: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
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) -> CVal -> Either CVal CVal
forall a b. b -> Either a b
Right CVal
v
Maybe CV
Nothing -> String -> Either CVal CVal
forall a. HasCallStack => String -> a
error (String -> Either CVal CVal) -> String -> Either CVal CVal
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Couldn't parse an either value on the right"
, String
"Kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k2
, String
"Expr: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SExpr -> String
forall a. Show a => a -> String
show SExpr
b
]
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 = String -> Either CVal CVal
forall a. HasCallStack => String -> a
error (String -> Either CVal CVal) -> String -> Either CVal CVal
forall a b. (a -> b) -> a -> b
$ String
"Expected an SEither sexpr, but received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Kind, SExpr) -> String
forall a. Show a => a -> String
show (Kind
k, SExpr
other)
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
CV -> Maybe CV
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CV -> Maybe CV) -> CV -> Maybe CV
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
_ -> Maybe CV
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 Maybe CV
-> (CV -> Maybe (RealPoint Rational)) -> Maybe (RealPoint Rational)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Rational -> RealPoint Rational)
-> CV -> Maybe (RealPoint Rational)
forall (f :: * -> *) a.
Applicative f =>
(Rational -> a) -> CV -> f a
border Rational -> RealPoint Rational
forall a. a -> RealPoint a
OpenPoint
getBorder (EApp [ECon String
"closed", SExpr
v]) = Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
KReal SExpr
v Maybe CV
-> (CV -> Maybe (RealPoint Rational)) -> Maybe (RealPoint Rational)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (Rational -> RealPoint Rational)
-> CV -> Maybe (RealPoint Rational)
forall (f :: * -> *) a.
Applicative f =>
(Rational -> a) -> CV -> f a
border Rational -> RealPoint Rational
forall a. a -> RealPoint a
ClosedPoint
getBorder SExpr
_ = Maybe (RealPoint Rational)
forall a. Maybe a
Nothing
border :: (Rational -> a) -> CV -> f a
border Rational -> a
b (CV Kind
KReal (CAlgReal (AlgRational Bool
True Rational
v))) = a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> f a) -> a -> f a
forall a b. (a -> b) -> a -> b
$ Rational -> a
b Rational
v
border Rational -> a
_ CV
other = String -> f a
forall a. HasCallStack => String -> a
error (String -> f a) -> String -> f a
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.interpretInterval.border: Expected a real-valued sexp, but received: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
forall a. Show a => a -> String
show CV
other
getValueCV :: (MonadIO m, MonadQuery m) => Maybe Int -> SV -> m CV
getValueCV :: Maybe Key -> SV -> m CV
getValueCV Maybe Key
mbi SV
s
| SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
s Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind
KReal
= Maybe Key -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> SV -> m CV
getValueCVHelper Maybe Key
mbi SV
s
| Bool
True
= do SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
if Bool -> Bool
not (SolverCapabilities -> Bool
supportsApproxReals (SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)))
then Maybe Key -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> SV -> m CV
getValueCVHelper Maybe Key
mbi SV
s
else do Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True String
"(set-option :pp.decimal false)"
CV
rep1 <- Maybe Key -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> SV -> m CV
getValueCVHelper Maybe Key
mbi SV
s
Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True String
"(set-option :pp.decimal true)"
Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"(set-option :pp.decimal_precision " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show (SMTConfig -> Key
printRealPrec SMTConfig
cfg) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
CV
rep2 <- Maybe Key -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> SV -> m CV
getValueCVHelper Maybe Key
mbi SV
s
let bad :: m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getValueCV" String
"get-value" (String
"a real-valued binding for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
s) Maybe [String]
forall a. Maybe a
Nothing ((CV, CV) -> String
forall a. Show a => a -> String
show (CV
rep1, CV
rep2)) Maybe [String]
forall a. Maybe a
Nothing
case (CV
rep1, CV
rep2) of
(CV Kind
KReal (CAlgReal AlgReal
a), CV Kind
KReal (CAlgReal AlgReal
b)) -> CV -> m CV
forall (m :: * -> *) a. Monad m => a -> m a
return (CV -> m CV) -> CV -> m CV
forall a b. (a -> b) -> a -> b
$ Kind -> CVal -> CV
CV Kind
KReal (AlgReal -> CVal
CAlgReal (String -> AlgReal -> AlgReal -> AlgReal
mergeAlgReals (String
"Cannot merge real-values for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
s) AlgReal
a AlgReal
b))
(CV, CV)
_ -> m CV
forall a. m a
bad
extractValue :: forall m. (MonadIO m, MonadQuery m) => Maybe Int -> String -> Kind -> m CV
Maybe Key
mbi String
nm Kind
k = do
let modelIndex :: String
modelIndex = case Maybe Key
mbi of
Maybe Key
Nothing -> String
""
Just Key
i -> String
" :model_index " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
i
cmd :: String
cmd = String
"(get-value (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
modelIndex String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getModel" String
cmd (String
"a value binding for kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k) Maybe [String]
forall a. Maybe a
Nothing
String
r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd
let recover :: SExpr -> m CV
recover SExpr
val = case Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
k SExpr
val of
Just CV
cv -> CV -> m CV
forall (m :: * -> *) a. Monad m => a -> m a
return CV
cv
Maybe CV
Nothing -> String -> Maybe [String] -> m CV
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
String
-> (String -> Maybe [String] -> m CV) -> (SExpr -> m CV) -> m CV
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m CV
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m CV) -> m CV) -> (SExpr -> m CV) -> m CV
forall a b. (a -> b) -> a -> b
$ \case EApp [EApp [ECon String
v, SExpr
val]] | String
v String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
nm -> SExpr -> m CV
recover SExpr
val
SExpr
_ -> String -> Maybe [String] -> m CV
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
getUICVal :: forall m. (MonadIO m, MonadQuery m) => Maybe Int -> (String, SBVType) -> m CV
getUICVal :: Maybe Key -> (String, SBVType) -> m CV
getUICVal Maybe Key
mbi (String
nm, SBVType
t) = case SBVType
t of
SBVType [Kind
k] -> Maybe Key -> String -> Kind -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> String -> Kind -> m CV
extractValue Maybe Key
mbi String
nm Kind
k
SBVType
_ -> String -> m CV
forall a. HasCallStack => String -> a
error (String -> m CV) -> String -> m CV
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: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String, SBVType) -> String
forall a. Show a => a -> String
show (String
nm, SBVType
t)
getUIFunCVAssoc :: forall m. (MonadIO m, MonadQuery m) => Maybe Int -> (String, SBVType) -> m ([([CV], CV)], CV)
getUIFunCVAssoc :: Maybe Key -> (String, SBVType) -> m ([([CV], CV)], CV)
getUIFunCVAssoc Maybe Key
mbi (String
nm, SBVType
typ) = do
let modelIndex :: String
modelIndex = case Maybe Key
mbi of
Maybe Key
Nothing -> String
""
Just Key
i -> String
" :model_index " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
i
cmd :: String
cmd = String
"(get-value (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
modelIndex String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"get-value" String
cmd String
"a function value" Maybe [String]
forall a. Maybe a
Nothing
String
r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd
let ([Kind]
ats, Kind
rt) = case SBVType
typ of
SBVType [Kind]
as | [Kind] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [Kind]
as Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
> Key
1 -> ([Kind] -> [Kind]
forall a. [a] -> [a]
init [Kind]
as, [Kind] -> Kind
forall a. [a] -> a
last [Kind]
as)
SBVType
_ -> String -> ([Kind], Kind)
forall a. HasCallStack => String -> a
error (String -> ([Kind], Kind)) -> String -> ([Kind], Kind)
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.getUIFunCVAssoc: Expected a function type, got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVType -> String
forall a. Show a => a -> String
show SBVType
typ
let convert :: (t ([SExpr], SExpr), SExpr) -> Maybe (t ([CV], CV), CV)
convert (t ([SExpr], SExpr)
vs, SExpr
d) = (,) (t ([CV], CV) -> CV -> (t ([CV], CV), CV))
-> Maybe (t ([CV], CV)) -> Maybe (CV -> (t ([CV], CV), CV))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (([SExpr], SExpr) -> Maybe ([CV], CV))
-> t ([SExpr], SExpr) -> Maybe (t ([CV], CV))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ([SExpr], SExpr) -> Maybe ([CV], CV)
toPoint t ([SExpr], SExpr)
vs Maybe (CV -> (t ([CV], CV), CV))
-> Maybe CV -> Maybe (t ([CV], CV), CV)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe CV
toRes SExpr
d
toPoint :: ([SExpr], SExpr) -> Maybe ([CV], CV)
toPoint ([SExpr]
as, SExpr
v)
| [SExpr] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [SExpr]
as Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== [Kind] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [Kind]
ats = (,) ([CV] -> CV -> ([CV], CV))
-> Maybe [CV] -> Maybe (CV -> ([CV], CV))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Kind -> SExpr -> Maybe CV) -> [Kind] -> [SExpr] -> Maybe [CV]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Kind -> SExpr -> Maybe CV
recoverKindedValue [Kind]
ats [SExpr]
as Maybe (CV -> ([CV], CV)) -> Maybe CV -> Maybe ([CV], CV)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> SExpr -> Maybe CV
toRes SExpr
v
| Bool
True = String -> Maybe ([CV], CV)
forall a. HasCallStack => String -> a
error (String -> Maybe ([CV], CV)) -> String -> Maybe ([CV], CV)
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.getUIFunCVAssoc: Mismatching type/value arity, got: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([SExpr], [Kind]) -> String
forall a. Show a => a -> String
show ([SExpr]
as, [Kind]
ats)
toRes :: SExpr -> Maybe CV
toRes :: SExpr -> Maybe CV
toRes = Kind -> SExpr -> Maybe CV
recoverKindedValue Kind
rt
tryPointWise :: m ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
tryPointWise m ([([CV], CV)], CV)
bailOut = do Maybe ([([SExpr], SExpr)], SExpr)
mbSExprs <- String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> SBVType -> m (Maybe ([([SExpr], SExpr)], SExpr))
pointWiseExtract String
nm SBVType
typ
case Maybe ([([SExpr], SExpr)], SExpr)
mbSExprs of
Maybe ([([SExpr], SExpr)], SExpr)
Nothing -> m ([([CV], CV)], CV)
bailOut
Just ([([SExpr], SExpr)], SExpr)
sExprs -> m ([([CV], CV)], CV)
-> (([([CV], CV)], CV) -> m ([([CV], CV)], CV))
-> Maybe ([([CV], CV)], CV)
-> m ([([CV], CV)], CV)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe m ([([CV], CV)], CV)
bailOut ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
forall (m :: * -> *) a. Monad m => a -> m a
return (([([SExpr], SExpr)], SExpr) -> Maybe ([([CV], CV)], CV)
forall (t :: * -> *).
Traversable t =>
(t ([SExpr], SExpr), SExpr) -> Maybe (t ([CV], CV), CV)
convert ([([SExpr], SExpr)], SExpr)
sExprs)
String
-> (String -> Maybe [String] -> m ([([CV], CV)], CV))
-> (SExpr -> m ([([CV], CV)], CV))
-> m ([([CV], CV)], CV)
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m ([([CV], CV)], CV)
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m ([([CV], CV)], CV)) -> m ([([CV], CV)], CV))
-> (SExpr -> m ([([CV], CV)], CV)) -> m ([([CV], CV)], CV)
forall a b. (a -> b) -> a -> b
$ \case EApp [EApp [ECon String
o, SExpr
e]] | String
o String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
nm -> let bailOut :: m a
bailOut = String -> Maybe [String] -> m a
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
in case SExpr -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
parseSExprFunction SExpr
e of
Just (Right ([([SExpr], SExpr)], SExpr)
assocs) | Just ([([CV], CV)], CV)
res <- ([([SExpr], SExpr)], SExpr) -> Maybe ([([CV], CV)], CV)
forall (t :: * -> *).
Traversable t =>
(t ([SExpr], SExpr), SExpr) -> Maybe (t ([CV], CV), CV)
convert ([([SExpr], SExpr)], SExpr)
assocs -> ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ([([CV], CV)], CV)
res
| Bool
True -> m ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
tryPointWise m ([([CV], CV)], CV)
forall a. m a
bailOut
Just (Left String
nm') | String
nm String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
nm', Just CV
res <- Kind -> Maybe CV
defaultKindedValue Kind
rt -> ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ([], CV
res)
| Bool
True -> String -> Maybe [String] -> m ([([CV], CV)], CV)
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
Maybe (Either String ([([SExpr], SExpr)], SExpr))
Nothing -> m ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m ([([CV], CV)], CV) -> m ([([CV], CV)], CV)
tryPointWise m ([([CV], CV)], CV)
forall a. m a
bailOut
SExpr
_ -> String -> Maybe [String] -> m ([([CV], CV)], CV)
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
checkSat :: (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat :: m CheckSatResult
checkSat = do SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
String -> m CheckSatResult
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m CheckSatResult
checkSatUsing (String -> m CheckSatResult) -> String -> m CheckSatResult
forall a b. (a -> b) -> a -> b
$ SMTConfig -> String
satCmd SMTConfig
cfg
checkSatUsing :: (MonadIO m, MonadQuery m) => String -> m CheckSatResult
checkSatUsing :: String -> m CheckSatResult
checkSatUsing String
cmd = do let bad :: String -> Maybe [String] -> m a
bad = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"checkSat" String
cmd String
"one of sat/unsat/unknown" Maybe [String]
forall a. Maybe a
Nothing
ignoreList :: [String]
ignoreList = [String
"WARNING: optimization with quantified constraints is not supported"]
String
r <- String -> [String] -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> [String] -> m String
askIgnoring String
cmd [String]
ignoreList
let getPrecision :: m (Maybe String)
getPrecision = do SMTConfig
cfg <- m SMTConfig
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 -> Maybe String -> m (Maybe String)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe String
forall a. Maybe a
Nothing
Just String
o -> String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> m String -> m (Maybe String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
o
String
-> (String -> Maybe [String] -> m CheckSatResult)
-> (SExpr -> m CheckSatResult)
-> m CheckSatResult
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m CheckSatResult
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m CheckSatResult) -> m CheckSatResult)
-> (SExpr -> m CheckSatResult) -> m CheckSatResult
forall a b. (a -> b) -> a -> b
$ \case ECon String
"sat" -> CheckSatResult -> m CheckSatResult
forall (m :: * -> *) a. Monad m => a -> m a
return CheckSatResult
Sat
ECon String
"unsat" -> CheckSatResult -> m CheckSatResult
forall (m :: * -> *) a. Monad m => a -> m a
return CheckSatResult
Unsat
ECon String
"unknown" -> CheckSatResult -> m CheckSatResult
forall (m :: * -> *) a. Monad m => a -> m a
return CheckSatResult
Unk
ECon String
"delta-sat" -> Maybe String -> CheckSatResult
DSat (Maybe String -> CheckSatResult)
-> m (Maybe String) -> m CheckSatResult
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (Maybe String)
getPrecision
SExpr
_ -> String -> Maybe [String] -> m CheckSatResult
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
getQuantifiedInputs :: (MonadIO m, MonadQuery m) => m UserInputs
getQuantifiedInputs :: m UserInputs
getQuantifiedInputs = do State{IORef Inputs
rinps :: State -> IORef Inputs
rinps :: IORef Inputs
rinps} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
(UserInputs
rQinps, InternInps
rTrackers) <- IO (UserInputs, InternInps) -> m (UserInputs, InternInps)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (UserInputs, InternInps) -> m (UserInputs, InternInps))
-> IO (UserInputs, InternInps) -> m (UserInputs, InternInps)
forall a b. (a -> b) -> a -> b
$ Inputs -> (UserInputs, InternInps)
getInputs (Inputs -> (UserInputs, InternInps))
-> IO Inputs -> IO (UserInputs, InternInps)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef Inputs -> IO Inputs
forall a. IORef a -> IO a
readIORef IORef Inputs
rinps
let trackers :: UserInputs
trackers = (Quantifier
EX,) (NamedSymVar -> (Quantifier, NamedSymVar))
-> InternInps -> UserInputs
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> InternInps
rTrackers
(UserInputs
preQs, UserInputs
postQs) = ((Quantifier, NamedSymVar) -> Bool)
-> UserInputs -> (UserInputs, UserInputs)
forall a. (a -> Bool) -> Seq a -> (Seq a, Seq a)
S.spanl (\(Quantifier
q, NamedSymVar
_) -> Quantifier
q Quantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
== Quantifier
EX) UserInputs
rQinps
UserInputs -> m UserInputs
forall (m :: * -> *) a. Monad m => a -> m a
return (UserInputs -> m UserInputs) -> UserInputs -> m UserInputs
forall a b. (a -> b) -> a -> b
$ UserInputs
preQs UserInputs -> UserInputs -> UserInputs
forall a. Semigroup a => a -> a -> a
<> UserInputs
trackers UserInputs -> UserInputs -> UserInputs
forall a. Semigroup a => a -> a -> a
<> UserInputs
postQs
getObservables :: (MonadIO m, MonadQuery m) => m [(Name, CV)]
getObservables :: 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} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
Seq (Text, CV -> Bool, SV)
rObs <- IO (Seq (Text, CV -> Bool, SV)) -> m (Seq (Text, CV -> Bool, SV))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (Seq (Text, CV -> Bool, SV)) -> m (Seq (Text, CV -> Bool, SV)))
-> IO (Seq (Text, CV -> Bool, SV))
-> m (Seq (Text, CV -> Bool, SV))
forall a b. (a -> b) -> a -> b
$ IORef (Seq (Text, CV -> Bool, SV))
-> IO (Seq (Text, CV -> Bool, SV))
forall a. IORef a -> IO a
readIORef IORef (Seq (Text, CV -> Bool, SV))
rObservables
let walk :: [(a, CV -> Bool, SV)] -> [(a, CV)] -> m [(a, CV)]
walk [] ![(a, CV)]
sofar = [(a, CV)] -> m [(a, CV)]
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 <- Maybe Key -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> SV -> m CV
getValueCV Maybe Key
forall a. Maybe a
Nothing SV
s
if CV -> Bool
f CV
cv
then [(a, CV -> Bool, SV)] -> [(a, CV)] -> m [(a, CV)]
walk [(a, CV -> Bool, SV)]
os ((a
n, CV
cv) (a, CV) -> [(a, CV)] -> [(a, CV)]
forall a. a -> [a] -> [a]
: [(a, CV)]
sofar)
else [(a, CV -> Bool, SV)] -> [(a, CV)] -> m [(a, CV)]
walk [(a, CV -> Bool, SV)]
os [(a, CV)]
sofar
[(Text, CV -> Bool, SV)] -> [(Text, CV)] -> m [(Text, CV)]
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
[(a, CV -> Bool, SV)] -> [(a, CV)] -> m [(a, CV)]
walk (Seq (Text, CV -> Bool, SV) -> [(Text, CV -> Bool, SV)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (Text, CV -> Bool, SV)
rObs) []
getUIs :: forall m. (MonadIO m, MonadQuery m) => m [(String, SBVType)]
getUIs :: m [(String, SBVType)]
getUIs = do State{IORef (Map String SBVType)
rUIMap :: IORef (Map String SBVType)
rUIMap :: State -> IORef (Map String SBVType)
rUIMap, IORef [(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} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
[String]
defines <- do [(Bool, String, [String])]
allAxs <- IO [(Bool, String, [String])] -> m [(Bool, String, [String])]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO [(Bool, String, [String])] -> m [(Bool, String, [String])])
-> IO [(Bool, String, [String])] -> m [(Bool, String, [String])]
forall a b. (a -> b) -> a -> b
$ IORef [(Bool, String, [String])] -> IO [(Bool, String, [String])]
forall a. IORef a -> IO a
readIORef IORef [(Bool, String, [String])]
raxioms
[String] -> m [String]
forall (f :: * -> *) a. Applicative f => a -> f a
pure [String
nm | (Bool
True, String
nm, [String]
_) <- [(Bool, String, [String])]
allAxs]
Map String SBVType
prior <- IO (Map String SBVType) -> m (Map String SBVType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (Map String SBVType) -> m (Map String SBVType))
-> IO (Map String SBVType) -> m (Map String SBVType)
forall a b. (a -> b) -> a -> b
$ IORef (Map String SBVType) -> IO (Map String SBVType)
forall a. IORef a -> IO a
readIORef IORef (Map String SBVType)
rUIMap
Map String SBVType
new <- IO (Map String SBVType) -> m (Map String SBVType)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (Map String SBVType) -> m (Map String SBVType))
-> IO (Map String SBVType) -> m (Map String SBVType)
forall a b. (a -> b) -> a -> b
$ IORef IncState -> IO IncState
forall a. IORef a -> IO a
readIORef IORef IncState
rIncState IO IncState
-> (IncState -> IO (Map String SBVType)) -> IO (Map String SBVType)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= IORef (Map String SBVType) -> IO (Map String SBVType)
forall a. IORef a -> IO a
readIORef (IORef (Map String SBVType) -> IO (Map String SBVType))
-> (IncState -> IORef (Map String SBVType))
-> IncState
-> IO (Map String SBVType)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IncState -> IORef (Map String SBVType)
rNewUIs
[(String, SBVType)] -> m [(String, SBVType)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([(String, SBVType)] -> m [(String, SBVType)])
-> [(String, SBVType)] -> m [(String, SBVType)]
forall a b. (a -> b) -> a -> b
$ [(String, SBVType)] -> [(String, SBVType)]
forall a. Eq a => [a] -> [a]
nub ([(String, SBVType)] -> [(String, SBVType)])
-> [(String, SBVType)] -> [(String, SBVType)]
forall a b. (a -> b) -> a -> b
$ [(String, SBVType)] -> [(String, SBVType)]
forall a. Ord a => [a] -> [a]
sort [(String, SBVType)
p | p :: (String, SBVType)
p@(String
n, SBVType
_) <- Map String SBVType -> [(String, SBVType)]
forall k a. Map k a -> [(k, a)]
Map.toList Map String SBVType
prior [(String, SBVType)] -> [(String, SBVType)] -> [(String, SBVType)]
forall a. [a] -> [a] -> [a]
++ Map String SBVType -> [(String, SBVType)]
forall k a. Map k a -> [(k, a)]
Map.toList Map String SBVType
new, String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
defines]
getAllSatResult :: forall m. (MonadIO m, MonadQuery m, SolverContext m) => m AllSatResult
getAllSatResult :: m AllSatResult
getAllSatResult = do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"*** Checking Satisfiability, all solutions.."]
SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (SolverCapabilities -> Bool
supportsCustomQueries (SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg))) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
String -> m ()
forall a. HasCallStack => String -> a
error (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
, String
"*** Data.SBV: Backend solver " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Solver -> String
forall a. Show a => a -> String
show (SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
cfg)) String -> String -> String
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} <- m State
forall (m :: * -> *). MonadQuery m => m State
queryState
KindSet
ki <- IO KindSet -> m KindSet
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO KindSet -> m KindSet) -> IO KindSet -> m KindSet
forall a b. (a -> b) -> a -> b
$ IORef KindSet -> IO KindSet
forall a. IORef a -> IO a
readIORef IORef KindSet
rUsedKinds
UserInputs
qinps <- m UserInputs
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m UserInputs
getQuantifiedInputs
[(String, SBVType)]
allUninterpreteds <- m [(String, SBVType)]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
m [(String, SBVType)]
getUIs
let allUiFuns :: [(String, SBVType)]
allUiFuns = [(String, SBVType)
u | SMTConfig -> Bool
satTrackUFs SMTConfig
cfg
, u :: (String, SBVType)
u@(String
nm, SBVType [Kind]
as) <- [(String, SBVType)]
allUninterpreteds, [Kind] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [Kind]
as Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
> Key
1
, Bool -> Bool
not (SMTConfig -> String -> Bool
isNonModelVar SMTConfig
cfg String
nm)
]
allUiRegs :: [(String, SBVType)]
allUiRegs = [(String, SBVType)
u | u :: (String, SBVType)
u@(String
nm, SBVType [Kind]
as) <- [(String, SBVType)]
allUninterpreteds, [Kind] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [Kind]
as Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
== Key
1
, Bool -> Bool
not (SMTConfig -> String -> Bool
isNonModelVar SMTConfig
cfg String
nm)
]
collectAcceptable :: [(String, SBVType)] -> [String] -> m [String]
collectAcceptable [] [String]
sofar = [String] -> m [String]
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 ((Kind -> Bool) -> [Kind] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
hasUninterpretedSorts [Kind]
ats)
= [(String, SBVType)] -> [String] -> m [String]
collectAcceptable [(String, SBVType)]
rest (String
nm String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)
| Bool
True
= do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [ String
"*** SBV.allSat: Uninterpreted function: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVType -> String
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 <- [String] -> [String]
forall a. [a] -> [a]
reverse ([String] -> [String]) -> m [String] -> m [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(String, SBVType)] -> [String] -> m [String]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
[(String, SBVType)] -> [String] -> m [String]
collectAcceptable [(String, SBVType)]
allUiFuns []
[String]
_ <- [(String, SBVType)] -> [String] -> m [String]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
[(String, SBVType)] -> [String] -> m [String]
collectAcceptable [(String, SBVType)]
allUiRegs []
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
uiFuns) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
let solverCaps :: SolverCapabilities
solverCaps = SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)
in case SolverCapabilities -> Maybe [String]
supportsFlattenedModels SolverCapabilities
solverCaps of
Maybe [String]
Nothing -> () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just [String]
cmds -> (String -> m ()) -> [String] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True) [String]
cmds
let usorts :: [String]
usorts = [String
s | us :: Kind
us@(KUserSort String
s Maybe [String]
_) <- KindSet -> [Kind]
forall a. Set a -> [a]
Set.toAscList KindSet
ki, Kind -> Bool
isFree Kind
us]
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
usorts) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [ String
"*** SBV.allSat: Uninterpreted sorts present: " String -> String -> String
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
hasQuantifiers :: Bool
hasQuantifiers = UserInputs -> Key
forall a. Seq a -> Key
S.length UserInputs
allModelInputs Key -> Key -> Bool
forall a. Eq a => a -> a -> Bool
/= UserInputs -> Key
forall a. Seq a -> Key
S.length UserInputs
qinps
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 (SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
sv) (Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right ((State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache (IO SV -> State -> IO SV
forall a b. a -> b -> a
const (SV -> IO SV
forall (m :: * -> *) a. Monad m => a -> m a
return SV
sv)))), NamedSymVar
nm)
ignored :: 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 ((Quantifier, NamedSymVar) -> (SVal, NamedSymVar))
-> UserInputs -> Seq (SVal, NamedSymVar)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (NamedSymVar -> (SVal, NamedSymVar)
mkSVal (NamedSymVar -> (SVal, NamedSymVar))
-> ((Quantifier, NamedSymVar) -> NamedSymVar)
-> (Quantifier, NamedSymVar)
-> (SVal, NamedSymVar)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Quantifier, NamedSymVar) -> NamedSymVar
namedSymVar)
(UserInputs -> Seq (SVal, NamedSymVar))
-> (UserInputs -> UserInputs)
-> UserInputs
-> Seq (SVal, NamedSymVar)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Quantifier, NamedSymVar) -> Bool) -> UserInputs -> UserInputs
forall a. (a -> Bool) -> Seq a -> Seq a
S.filter (Bool -> Bool
not (Bool -> Bool)
-> ((Quantifier, NamedSymVar) -> Bool)
-> (Quantifier, NamedSymVar)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Bool
ignored (Text -> Bool)
-> ((Quantifier, NamedSymVar) -> Text)
-> (Quantifier, NamedSymVar)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedSymVar -> Text
getUserName (NamedSymVar -> Text)
-> ((Quantifier, NamedSymVar) -> NamedSymVar)
-> (Quantifier, NamedSymVar)
-> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Quantifier, NamedSymVar) -> NamedSymVar
namedSymVar)
(UserInputs -> Seq (SVal, NamedSymVar))
-> UserInputs -> Seq (SVal, NamedSymVar)
forall a b. (a -> b) -> a -> b
$ UserInputs
allModelInputs
w :: Bool
w = Quantifier
ALL Quantifier -> [Quantifier] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Seq Quantifier -> [Quantifier]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList ((Quantifier, NamedSymVar) -> Quantifier
quantifier ((Quantifier, NamedSymVar) -> Quantifier)
-> UserInputs -> Seq Quantifier
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> UserInputs
qinps)
let isSimple :: Bool
isSimple = [(String, SBVType)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, SBVType)]
allUiFuns Bool -> Bool -> Bool
&& [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
usorts Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
hasQuantifiers
start :: AllSatResult
start = AllSatResult :: Bool -> Bool -> Bool -> Bool -> [SMTResult] -> AllSatResult
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 (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache ((State -> IO SV) -> Cached SV) -> (State -> IO SV) -> Cached SV
forall a b. (a -> b) -> a -> b
$ \State
_ -> SV -> IO SV
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)
(SVal, NamedSymVar) -> IO (SVal, NamedSymVar)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SVal
sval, NamedSymVar
nsv)
mkVar (String, SBVType)
nmt = String -> IO (SVal, NamedSymVar)
forall a. HasCallStack => String -> a
error (String -> IO (SVal, NamedSymVar))
-> String -> IO (SVal, NamedSymVar)
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: Impossible happened; allSat.mkVar. Unexpected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String, SBVType) -> String
forall a. Show a => a -> String
show (String, SBVType)
nmt
Seq (SVal, NamedSymVar)
uiVars <- IO (Seq (SVal, NamedSymVar)) -> m (Seq (SVal, NamedSymVar))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (Seq (SVal, NamedSymVar)) -> m (Seq (SVal, NamedSymVar)))
-> IO (Seq (SVal, NamedSymVar)) -> m (Seq (SVal, NamedSymVar))
forall a b. (a -> b) -> a -> b
$ [(SVal, NamedSymVar)] -> Seq (SVal, NamedSymVar)
forall a. [a] -> Seq a
S.fromList ([(SVal, NamedSymVar)] -> Seq (SVal, NamedSymVar))
-> IO [(SVal, NamedSymVar)] -> IO (Seq (SVal, NamedSymVar))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((String, SBVType) -> IO (SVal, NamedSymVar))
-> [(String, SBVType)] -> IO [(SVal, NamedSymVar)]
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 Seq (SVal, NamedSymVar)
-> Seq (SVal, NamedSymVar) -> Seq (SVal, NamedSymVar)
forall a. Seq a -> Seq a -> Seq a
S.>< Seq (SVal, NamedSymVar)
vars) SMTConfig
cfg AllSatResult
start
else Bool
-> State
-> ([(String, SBVType)], [String])
-> [(String, SBVType)]
-> UserInputs
-> Seq (SVal, NamedSymVar)
-> SMTConfig
-> AllSatResult
-> m AllSatResult
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
= Bool -> f () -> f ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SMTConfig -> Bool
allSatPrintAlong SMTConfig
cfg Bool -> Bool -> Bool
&& Bool -> Bool
not ([SMTResult] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (AllSatResult -> [SMTResult]
allSatResults AllSatResult
sofar))) (f () -> f ()) -> f () -> f ()
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 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" different solutions."
IO () -> f ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> f ()) -> (String -> IO ()) -> String -> f ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> IO ()
putStrLn (String -> f ()) -> String -> f ()
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. (Eq a, Num a, Show a) => a -> String
msg (a
cnt a -> a -> a
forall a. Num a => a -> a -> a
- a
1)
case Maybe String
extra of
Maybe String
Nothing -> () -> f ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Just String
m -> IO () -> f ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> f ()) -> IO () -> f ()
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 (Key, AllSatResult, Bool, Maybe String)
result <- IO (IORef (Key, AllSatResult, Bool, Maybe String))
-> m (IORef (Key, AllSatResult, Bool, Maybe String))
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (IORef (Key, AllSatResult, Bool, Maybe String))
-> m (IORef (Key, AllSatResult, Bool, Maybe String)))
-> IO (IORef (Key, AllSatResult, Bool, Maybe String))
-> m (IORef (Key, AllSatResult, Bool, Maybe String))
forall a b. (a -> b) -> a -> b
$ (Key, AllSatResult, Bool, Maybe String)
-> IO (IORef (Key, AllSatResult, Bool, Maybe String))
forall a. a -> IO (IORef a)
newIORef (Key
0, AllSatResult
start, Bool
False, Maybe String
forall a. Maybe a
Nothing)
IORef (Key, AllSatResult, Bool, Maybe String)
-> Seq (SVal, NamedSymVar) -> m ()
go IORef (Key, AllSatResult, Bool, Maybe String)
result Seq (SVal, NamedSymVar)
vars
(Key
found, AllSatResult
sofar, Bool
_, Maybe String
extra) <- IO (Key, AllSatResult, Bool, Maybe String)
-> m (Key, AllSatResult, Bool, Maybe String)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (Key, AllSatResult, Bool, Maybe String)
-> m (Key, AllSatResult, Bool, Maybe String))
-> IO (Key, AllSatResult, Bool, Maybe String)
-> m (Key, AllSatResult, Bool, Maybe String)
forall a b. (a -> b) -> a -> b
$ IORef (Key, AllSatResult, Bool, Maybe String)
-> IO (Key, AllSatResult, Bool, Maybe String)
forall a. IORef a -> IO a
readIORef IORef (Key, AllSatResult, Bool, Maybe String)
result
Key -> SMTConfig -> AllSatResult -> Maybe String -> m ()
forall (f :: * -> *) a.
(MonadIO f, Eq a, Num a, Show a) =>
a -> SMTConfig -> AllSatResult -> Maybe String -> f ()
finalize (Key
foundKey -> Key -> Key
forall a. Num a => a -> a -> a
+Key
1) SMTConfig
cfg AllSatResult
sofar Maybe String
extra
AllSatResult -> m AllSatResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure AllSatResult
sofar
where haveEnough :: Key -> Bool
haveEnough Key
have = case SMTConfig -> Maybe Key
allSatMaxModelCount SMTConfig
cfg of
Just Key
maxModels -> Key
have Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
>= Key
maxModels
Maybe Key
_ -> Bool
False
go :: IORef (Int, AllSatResult, Bool, Maybe String) -> S.Seq (SVal, NamedSymVar) -> m ()
go :: IORef (Key, AllSatResult, Bool, Maybe String)
-> Seq (SVal, NamedSymVar) -> m ()
go IORef (Key, AllSatResult, Bool, Maybe String)
finalResult = Bool -> Seq (SVal, NamedSymVar) -> m ()
walk Bool
True
where shouldContinue :: m Bool
shouldContinue = do (Key
have, AllSatResult
_, Bool
exitLoop, Maybe String
_) <- IO (Key, AllSatResult, Bool, Maybe String)
-> m (Key, AllSatResult, Bool, Maybe String)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (Key, AllSatResult, Bool, Maybe String)
-> m (Key, AllSatResult, Bool, Maybe String))
-> IO (Key, AllSatResult, Bool, Maybe String)
-> m (Key, AllSatResult, Bool, Maybe String)
forall a b. (a -> b) -> a -> b
$ IORef (Key, AllSatResult, Bool, Maybe String)
-> IO (Key, AllSatResult, Bool, Maybe String)
forall a. IORef a -> IO a
readIORef IORef (Key, AllSatResult, Bool, Maybe String)
finalResult
Bool -> m Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> m Bool) -> Bool -> m Bool
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool
exitLoop Bool -> Bool -> Bool
|| Key -> Bool
haveEnough Key
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
&& Seq (SVal, NamedSymVar) -> Bool
forall a. Seq a -> Bool
S.null Seq (SVal, NamedSymVar)
terms
= () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
| Bool
True
= do Maybe Key
mbCont <- do (Key
have, AllSatResult
sofar, Bool
exitLoop, Maybe String
_) <- IO (Key, AllSatResult, Bool, Maybe String)
-> m (Key, AllSatResult, Bool, Maybe String)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO (Key, AllSatResult, Bool, Maybe String)
-> m (Key, AllSatResult, Bool, Maybe String))
-> IO (Key, AllSatResult, Bool, Maybe String)
-> m (Key, AllSatResult, Bool, Maybe String)
forall a b. (a -> b) -> a -> b
$ IORef (Key, AllSatResult, Bool, Maybe String)
-> IO (Key, AllSatResult, Bool, Maybe String)
forall a. IORef a -> IO a
readIORef IORef (Key, AllSatResult, Bool, Maybe String)
finalResult
if Bool
exitLoop
then Maybe Key -> m (Maybe Key)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Key
forall a. Maybe a
Nothing
else case SMTConfig -> Maybe Key
allSatMaxModelCount SMTConfig
cfg of
Just Key
maxModels
| Key
have Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
>= Key
maxModels -> do Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (AllSatResult -> Bool
allSatMaxModelCountReached AllSatResult
sofar) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
[String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"*** Maximum model count request of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
maxModels String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" reached, stopping the search."]
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SMTConfig -> Bool
allSatPrintAlong SMTConfig
cfg) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Search stopped since model count request was reached."
IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IORef (Key, AllSatResult, Bool, Maybe String)
-> ((Key, AllSatResult, Bool, Maybe String)
-> (Key, AllSatResult, Bool, Maybe String))
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Key, AllSatResult, Bool, Maybe String)
finalResult (((Key, AllSatResult, Bool, Maybe String)
-> (Key, AllSatResult, Bool, Maybe String))
-> IO ())
-> ((Key, AllSatResult, Bool, Maybe String)
-> (Key, AllSatResult, Bool, Maybe String))
-> IO ()
forall a b. (a -> b) -> a -> b
$ \(Key
h, AllSatResult
s, Bool
_, Maybe String
m) -> (Key
h, AllSatResult
s{ allSatMaxModelCountReached :: Bool
allSatMaxModelCountReached = Bool
True }, Bool
True, Maybe String
m)
Maybe Key -> m (Maybe Key)
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Key
forall a. Maybe a
Nothing
Maybe Key
_ -> Maybe Key -> m (Maybe Key)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe Key -> m (Maybe Key)) -> Maybe Key -> m (Maybe Key)
forall a b. (a -> b) -> a -> b
$ Key -> Maybe Key
forall a. a -> Maybe a
Just (Key -> Maybe Key) -> Key -> Maybe Key
forall a b. (a -> b) -> a -> b
$ Key
haveKey -> Key -> Key
forall a. Num a => a -> a -> a
+Key
1
case Maybe Key
mbCont of
Maybe Key
Nothing -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
Just Key
cnt -> do
[String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"Fast allSat, Looking for solution " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
cnt]
CheckSatResult
cs <- m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
case CheckSatResult
cs of
CheckSatResult
Unsat -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
CheckSatResult
Unk -> do let m :: String
m = String
"Solver returned unknown, terminating query."
[String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"*** " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
m]
IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IORef (Key, AllSatResult, Bool, Maybe String)
-> ((Key, AllSatResult, Bool, Maybe String)
-> (Key, AllSatResult, Bool, Maybe String))
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Key, AllSatResult, Bool, Maybe String)
finalResult (((Key, AllSatResult, Bool, Maybe String)
-> (Key, AllSatResult, Bool, Maybe String))
-> IO ())
-> ((Key, AllSatResult, Bool, Maybe String)
-> (Key, AllSatResult, Bool, Maybe String))
-> IO ()
forall a b. (a -> b) -> a -> b
$ \(Key
h, AllSatResult
s, Bool
_, Maybe String
_) -> (Key
h, AllSatResult
s{allSatSolverReturnedUnknown :: Bool
allSatSolverReturnedUnknown = Bool
True}, Bool
True, String -> Maybe String
forall a. a -> Maybe a
Just (String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"))
DSat Maybe String
_ -> do let m :: String
m = String
"Solver returned delta-sat, terminating query."
[String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"*** " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
m]
IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IORef (Key, AllSatResult, Bool, Maybe String)
-> ((Key, AllSatResult, Bool, Maybe String)
-> (Key, AllSatResult, Bool, Maybe String))
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Key, AllSatResult, Bool, Maybe String)
finalResult (((Key, AllSatResult, Bool, Maybe String)
-> (Key, AllSatResult, Bool, Maybe String))
-> IO ())
-> ((Key, AllSatResult, Bool, Maybe String)
-> (Key, AllSatResult, Bool, Maybe String))
-> IO ()
forall a b. (a -> b) -> a -> b
$ \(Key
h, AllSatResult
s, Bool
_, Maybe String
_) -> (Key
h, AllSatResult
s{allSatSolverReturnedDSat :: Bool
allSatSolverReturnedDSat = Bool
True}, Bool
True, String -> Maybe String
forall a. a -> Maybe a
Just (String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"))
CheckSatResult
Sat -> do Seq (SV, (Text, (SVal, CV)))
assocs <- ((SVal, NamedSymVar) -> m (SV, (Text, (SVal, CV))))
-> Seq (SVal, NamedSymVar) -> m (Seq (SV, (Text, (SVal, CV))))
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 <- Maybe Key -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> SV -> m CV
getValueCV Maybe Key
forall a. Maybe a
Nothing SV
sv
(SV, (Text, (SVal, CV))) -> m (SV, (Text, (SVal, CV)))
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
_) = ((Quantifier, NamedSymVar), Maybe CV)
-> m ((Quantifier, NamedSymVar), Maybe CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, NamedSymVar)
i, Maybe CV
forall a. Maybe a
Nothing)
grab i :: (Quantifier, NamedSymVar)
i@(Quantifier
EX, NamedSymVar -> SV
getSV -> SV
sv) = case ((SV, (Text, (SVal, CV))) -> SV)
-> SV
-> Seq (SV, (Text, (SVal, CV)))
-> Maybe (SV, (Text, (SVal, CV)))
forall a. Eq a => (a -> SV) -> SV -> Seq a -> Maybe a
lookupInput (SV, (Text, (SVal, CV))) -> SV
forall a b. (a, b) -> a
fst SV
sv Seq (SV, (Text, (SVal, CV)))
assocs of
Just (SV
_, (Text
_, (SVal
_, CV
cv))) -> ((Quantifier, NamedSymVar), Maybe CV)
-> m ((Quantifier, NamedSymVar), Maybe CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, NamedSymVar)
i, CV -> Maybe CV
forall a. a -> Maybe a
Just CV
cv)
Maybe (SV, (Text, (SVal, CV)))
Nothing -> do !CV
cv <- Maybe Key -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> SV -> m CV
getValueCV Maybe Key
forall a. Maybe a
Nothing SV
sv
((Quantifier, NamedSymVar), Maybe CV)
-> m ((Quantifier, NamedSymVar), Maybe CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, NamedSymVar)
i, CV -> Maybe CV
forall a. a -> Maybe a
Just CV
cv)
in if SMTConfig -> Bool
validationRequested SMTConfig
cfg
then Seq ((Quantifier, NamedSymVar), Maybe CV)
-> Maybe (Seq ((Quantifier, NamedSymVar), Maybe CV))
forall a. a -> Maybe a
Just (Seq ((Quantifier, NamedSymVar), Maybe CV)
-> Maybe (Seq ((Quantifier, NamedSymVar), Maybe CV)))
-> m (Seq ((Quantifier, NamedSymVar), Maybe CV))
-> m (Maybe (Seq ((Quantifier, NamedSymVar), Maybe CV)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV))
-> UserInputs -> m (Seq ((Quantifier, NamedSymVar), Maybe CV))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV)
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV)
grab UserInputs
qinps
else Maybe (Seq ((Quantifier, NamedSymVar), Maybe CV))
-> m (Maybe (Seq ((Quantifier, NamedSymVar), Maybe CV)))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Seq ((Quantifier, NamedSymVar), Maybe CV))
forall a. Maybe a
Nothing
[(Text, CV)]
obsvs <- if Bool
grabObservables
then m [(Text, CV)]
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m [(Text, CV)]
getObservables
else do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"*** In a quantified context, observables will not be printed."]
[(Text, CV)] -> m [(Text, CV)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Text, CV)]
forall a. Monoid a => a
mempty
let lassocs :: [(SV, (Text, (SVal, CV)))]
lassocs = Seq (SV, (Text, (SVal, CV))) -> [(SV, (Text, (SVal, CV)))]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (SV, (Text, (SVal, CV)))
assocs
model :: SMTModel
model = SMTModel :: [(String, GeneralizedCV)]
-> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
-> [(String, CV)]
-> [(String, (SBVType, ([([CV], CV)], CV)))]
-> SMTModel
SMTModel { modelObjectives :: [(String, GeneralizedCV)]
modelObjectives = []
, modelBindings :: Maybe [((Quantifier, NamedSymVar), Maybe CV)]
modelBindings = Seq ((Quantifier, NamedSymVar), Maybe CV)
-> [((Quantifier, NamedSymVar), Maybe CV)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList (Seq ((Quantifier, NamedSymVar), Maybe CV)
-> [((Quantifier, NamedSymVar), Maybe CV)])
-> Maybe (Seq ((Quantifier, NamedSymVar), Maybe CV))
-> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Seq ((Quantifier, NamedSymVar), Maybe CV))
bindings
, modelAssocs :: [(String, CV)]
modelAssocs = ((Text -> String) -> (Text, CV) -> (String, CV)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Text -> String
T.unpack ((Text, CV) -> (String, CV)) -> [(Text, CV)] -> [(String, CV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Text, CV) -> Text) -> [(Text, CV)] -> [(Text, CV)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (Text, CV) -> Text
forall a b. (a, b) -> a
fst [(Text, CV)]
obsvs)
[(String, CV)] -> [(String, CV)] -> [(String, CV)]
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
IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IORef (Key, AllSatResult, Bool, Maybe String)
-> ((Key, AllSatResult, Bool, Maybe String)
-> (Key, AllSatResult, Bool, Maybe String))
-> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef (Key, AllSatResult, Bool, Maybe String)
finalResult (((Key, AllSatResult, Bool, Maybe String)
-> (Key, AllSatResult, Bool, Maybe String))
-> IO ())
-> ((Key, AllSatResult, Bool, Maybe String)
-> (Key, AllSatResult, Bool, Maybe String))
-> IO ()
forall a b. (a -> b) -> a -> b
$ \(Key
h, AllSatResult
s, Bool
e, Maybe String
m) -> let h' :: Key
h' = Key
hKey -> Key -> Key
forall a. Num a => a -> a -> a
+Key
1 in Key
h' Key
-> (Key, AllSatResult, Bool, Maybe String)
-> (Key, AllSatResult, Bool, Maybe String)
`seq` (Key
h', AllSatResult
s{allSatResults :: [SMTResult]
allSatResults = SMTResult
currentResult SMTResult -> [SMTResult] -> [SMTResult]
forall a. a -> [a] -> [a]
: AllSatResult -> [SMTResult]
allSatResults AllSatResult
s}, Bool
e, Maybe String
m)
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SMTConfig -> Bool
allSatPrintAlong SMTConfig
cfg) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Solution #" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
cnt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":"
IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SMTConfig -> SMTModel -> String
showModel SMTConfig
cfg SMTModel
model
let findVal :: (SVal, NamedSymVar) -> (SVal, CV)
findVal :: (SVal, NamedSymVar) -> (SVal, CV)
findVal (SVal
_, NamedSymVar SV
sv Text
nm) = case Seq (SV, (Text, (SVal, CV))) -> [(SV, (Text, (SVal, CV)))]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList (((SV, (Text, (SVal, CV))) -> Bool)
-> Seq (SV, (Text, (SVal, CV))) -> Seq (SV, (Text, (SVal, CV)))
forall a. (a -> Bool) -> Seq a -> Seq a
S.filter (\(SV
sv', (Text, (SVal, CV))
_) -> SV
sv SV -> SV -> Bool
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)))]
_ -> String -> (SVal, CV)
forall a. HasCallStack => String -> a
error (String -> (SVal, CV)) -> String -> (SVal, CV)
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: Cannot uniquely determine " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Text -> String
forall a. Show a => a -> String
show Text
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Seq (SV, (Text, (SVal, CV))) -> String
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) = SBool -> m ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> m ()) -> SBool -> m ()
forall a b. (a -> b) -> a -> b
$ SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal -> SBool) -> SVal -> SBool
forall a b. (a -> b) -> a -> b
$ Kind -> SVal -> SVal -> SVal
mkEq (SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
sv) SVal
sv (Kind -> Either CV (Cached SV) -> SVal
SVal (SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
sv) (CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left CV
cv))
where mkEq :: Kind -> SVal -> SVal -> SVal
mkEq :: Kind -> SVal -> SVal -> SVal
mkEq Kind
k SVal
a SVal
b
| Kind -> Bool
forall a. HasKind a => a -> Bool
isDouble Kind
k Bool -> Bool -> Bool
|| Kind -> Bool
forall a. HasKind a => a -> Bool
isFloat Kind
k Bool -> Bool -> Bool
|| Kind -> 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 (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
where r :: State -> IO SV
r 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 ((SVal, CV) -> m ())
-> ((SVal, NamedSymVar) -> (SVal, CV))
-> (SVal, NamedSymVar)
-> m ()
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 ((SVal, CV) -> m ())
-> ((SVal, NamedSymVar) -> (SVal, CV))
-> (SVal, NamedSymVar)
-> m ()
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
Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True String
"(push 1)"
(SVal, NamedSymVar) -> m ()
reject (SVal, NamedSymVar)
cur
((SVal, NamedSymVar) -> m ()) -> Seq (SVal, NamedSymVar) -> m ()
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
Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True String
"(pop 1)"
() -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
r
[Key] -> (Key -> m ()) -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Key
0 .. Seq (SVal, NamedSymVar) -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length Seq (SVal, NamedSymVar)
terms Key -> Key -> Key
forall a. Num a => a -> a -> a
- Key
1] ((Key -> m ()) -> m ()) -> (Key -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \Key
i -> do
Bool
sc <- m Bool
shouldContinue
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
sc (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do case Key
-> Seq (SVal, NamedSymVar)
-> (Seq (SVal, NamedSymVar), Seq (SVal, NamedSymVar))
forall a. Key -> Seq a -> (Seq a, Seq a)
S.splitAt Key
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 (m () -> m ()) -> m () -> m ()
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))
_ -> String -> m ()
forall a. HasCallStack => String -> a
error String
"Data.SBV.allSat: Impossible happened, ran out of terms!"
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 = Key -> AllSatResult -> m AllSatResult
go (Key
1::Int)
where go :: Int -> AllSatResult -> m AllSatResult
go :: Key -> AllSatResult -> m AllSatResult
go !Key
cnt !AllSatResult
sofar
| Just Key
maxModels <- SMTConfig -> Maybe Key
allSatMaxModelCount SMTConfig
cfg, Key
cnt Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
> Key
maxModels
= do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"*** Maximum model count request of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
maxModels String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" reached, stopping the search."]
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SMTConfig -> Bool
allSatPrintAlong SMTConfig
cfg) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn String
"Search stopped since model count request was reached."
AllSatResult -> m AllSatResult
forall (m :: * -> *) a. Monad m => a -> m a
return (AllSatResult -> m AllSatResult) -> AllSatResult -> m AllSatResult
forall a b. (a -> b) -> a -> b
$! AllSatResult
sofar { allSatMaxModelCountReached :: Bool
allSatMaxModelCountReached = Bool
True }
| Bool
True
= do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"Looking for solution " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
cnt]
CheckSatResult
cs <- m CheckSatResult
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m CheckSatResult
checkSat
let endMsg :: Maybe String -> m ()
endMsg = Key -> SMTConfig -> AllSatResult -> Maybe String -> m ()
forall (f :: * -> *) a.
(MonadIO f, Eq a, Num a, Show a) =>
a -> SMTConfig -> AllSatResult -> Maybe String -> f ()
finalize Key
cnt SMTConfig
cfg AllSatResult
sofar
case CheckSatResult
cs of
CheckSatResult
Unsat -> do Maybe String -> m ()
endMsg Maybe String
forall a. Maybe a
Nothing
AllSatResult -> m AllSatResult
forall (m :: * -> *) a. Monad m => a -> m a
return AllSatResult
sofar
CheckSatResult
Unk -> do let m :: String
m = String
"Solver returned unknown, terminating query."
[String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"*** " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
m]
Maybe String -> m ()
endMsg (Maybe String -> m ()) -> Maybe String -> m ()
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"
AllSatResult -> m AllSatResult
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."
[String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"*** " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
m]
Maybe String -> m ()
endMsg (Maybe String -> m ()) -> Maybe String -> m ()
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"
AllSatResult -> m AllSatResult
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 <- ((SVal, NamedSymVar) -> m (SV, (Text, (SVal, CV))))
-> Seq (SVal, NamedSymVar) -> m (Seq (SV, (Text, (SVal, CV))))
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 <- Maybe Key -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> SV -> m CV
getValueCV Maybe Key
forall a. Maybe a
Nothing SV
sv
(SV, (Text, (SVal, CV))) -> m (SV, (Text, (SVal, CV)))
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 <- Maybe Key -> (String, SBVType) -> m ([([CV], CV)], CV)
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> (String, SBVType) -> m ([([CV], CV)], CV)
getUIFunCVAssoc Maybe Key
forall a. Maybe a
Nothing (String, SBVType)
ui
(String, (SBVType, ([([CV], CV)], CV)))
-> m (String, (SBVType, ([([CV], CV)], CV)))
forall (m :: * -> *) a. Monad m => a -> m a
return (String
nm, (SBVType
t, ([([CV], CV)], CV)
cvs))
[(String, (SBVType, ([([CV], CV)], CV)))]
uiFunVals <- ((String, SBVType) -> m (String, (SBVType, ([([CV], CV)], CV))))
-> [(String, SBVType)]
-> m [(String, (SBVType, ([([CV], CV)], CV)))]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (String, SBVType) -> m (String, (SBVType, ([([CV], CV)], CV)))
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(String, SBVType) -> m (String, (SBVType, ([([CV], CV)], CV)))
getUIFun [(String, SBVType)]
allUiFuns
[(String, CV)]
uiRegVals <- ((String, SBVType) -> m (String, CV))
-> [(String, SBVType)] -> m [(String, CV)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\ui :: (String, SBVType)
ui@(String
nm, SBVType
_) -> (String
nm,) (CV -> (String, CV)) -> m CV -> m (String, CV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Key -> (String, SBVType) -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> (String, SBVType) -> m CV
getUICVal Maybe Key
forall a. Maybe a
Nothing (String, SBVType)
ui) [(String, SBVType)]
allUiRegs
[(Text, CV)]
obsvs <- if Bool
grabObservables
then m [(Text, CV)]
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m [(Text, CV)]
getObservables
else do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [String
"*** In a quantified context, observables will not be printed."]
[(Text, CV)] -> m [(Text, CV)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(Text, CV)]
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
_) = ((Quantifier, NamedSymVar), Maybe CV)
-> m ((Quantifier, NamedSymVar), Maybe CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, NamedSymVar)
i, Maybe CV
forall a. Maybe a
Nothing)
grab i :: (Quantifier, NamedSymVar)
i@(Quantifier
EX, NamedSymVar -> SV
getSV -> SV
sv) = case ((SV, (Text, (SVal, CV))) -> SV)
-> SV
-> Seq (SV, (Text, (SVal, CV)))
-> Maybe (SV, (Text, (SVal, CV)))
forall a. Eq a => (a -> SV) -> SV -> Seq a -> Maybe a
lookupInput (SV, (Text, (SVal, CV))) -> SV
forall a b. (a, b) -> a
fst SV
sv Seq (SV, (Text, (SVal, CV)))
assocs of
Just (SV
_, (Text
_, (SVal
_, CV
cv))) -> ((Quantifier, NamedSymVar), Maybe CV)
-> m ((Quantifier, NamedSymVar), Maybe CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, NamedSymVar)
i, CV -> Maybe CV
forall a. a -> Maybe a
Just CV
cv)
Maybe (SV, (Text, (SVal, CV)))
Nothing -> do !CV
cv <- Maybe Key -> SV -> m CV
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Maybe Key -> SV -> m CV
getValueCV Maybe Key
forall a. Maybe a
Nothing SV
sv
((Quantifier, NamedSymVar), Maybe CV)
-> m ((Quantifier, NamedSymVar), Maybe CV)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Quantifier, NamedSymVar)
i, CV -> Maybe CV
forall a. a -> Maybe a
Just CV
cv)
in if SMTConfig -> Bool
validationRequested SMTConfig
cfg
then t ((Quantifier, NamedSymVar), Maybe CV)
-> Maybe (t ((Quantifier, NamedSymVar), Maybe CV))
forall a. a -> Maybe a
Just (t ((Quantifier, NamedSymVar), Maybe CV)
-> Maybe (t ((Quantifier, NamedSymVar), Maybe CV)))
-> m (t ((Quantifier, NamedSymVar), Maybe CV))
-> m (Maybe (t ((Quantifier, NamedSymVar), Maybe CV)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV))
-> t (Quantifier, NamedSymVar)
-> m (t ((Quantifier, NamedSymVar), Maybe CV))
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV)
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(Quantifier, NamedSymVar)
-> m ((Quantifier, NamedSymVar), Maybe CV)
grab t (Quantifier, NamedSymVar)
qinps
else Maybe (t ((Quantifier, NamedSymVar), Maybe CV))
-> m (Maybe (t ((Quantifier, NamedSymVar), Maybe CV)))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (t ((Quantifier, NamedSymVar), Maybe CV))
forall a. Maybe a
Nothing
let model :: SMTModel
model = SMTModel :: [(String, GeneralizedCV)]
-> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
-> [(String, CV)]
-> [(String, (SBVType, ([([CV], CV)], CV)))]
-> SMTModel
SMTModel { modelObjectives :: [(String, GeneralizedCV)]
modelObjectives = []
, modelBindings :: Maybe [((Quantifier, NamedSymVar), Maybe CV)]
modelBindings = t ((Quantifier, NamedSymVar), Maybe CV)
-> [((Quantifier, NamedSymVar), Maybe CV)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList (t ((Quantifier, NamedSymVar), Maybe CV)
-> [((Quantifier, NamedSymVar), Maybe CV)])
-> Maybe (t ((Quantifier, NamedSymVar), Maybe CV))
-> Maybe [((Quantifier, NamedSymVar), Maybe CV)]
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
[(String, CV)] -> [(String, CV)] -> [(String, CV)]
forall a. Semigroup a => a -> a -> a
<> ((Text -> String) -> (Text, CV) -> (String, CV)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first Text -> String
T.unpack ((Text, CV) -> (String, CV)) -> [(Text, CV)] -> [(String, CV)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Text, CV) -> Text) -> [(Text, CV)] -> [(Text, CV)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (Text, CV) -> Text
forall a b. (a, b) -> a
fst [(Text, CV)]
obsvs)
[(String, CV)] -> [(String, CV)] -> [(String, CV)]
forall a. Semigroup a => a -> a -> a
<> [(Text -> String
T.unpack Text
n, CV
cv) | (SV
_, (Text
n, (SVal
_, CV
cv))) <- Seq (SV, (Text, (SVal, CV))) -> [(SV, (Text, (SVal, 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) = ((SVal, CV) -> Bool)
-> Seq (SVal, CV) -> (Seq (SVal, CV), Seq (SVal, CV))
forall a. (a -> Bool) -> Seq a -> (Seq a, Seq a)
S.partition (Bool -> Bool
not (Bool -> Bool) -> ((SVal, CV) -> Bool) -> (SVal, CV) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Bool
isFree (Kind -> Bool) -> ((SVal, CV) -> Kind) -> (SVal, CV) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf (SVal -> Kind) -> ((SVal, CV) -> SVal) -> (SVal, CV) -> Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SVal, CV) -> SVal
forall a b. (a, b) -> a
fst) (((SV, (Text, (SVal, CV))) -> (SVal, CV))
-> Seq (SV, (Text, (SVal, CV))) -> Seq (SVal, CV)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Text, (SVal, CV)) -> (SVal, CV)
forall a b. (a, b) -> b
snd ((Text, (SVal, CV)) -> (SVal, CV))
-> ((SV, (Text, (SVal, CV))) -> (Text, (SVal, CV)))
-> (SV, (Text, (SVal, CV)))
-> (SVal, CV)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SV, (Text, (SVal, CV))) -> (Text, (SVal, CV))
forall a b. (a, b) -> b
snd) Seq (SV, (Text, (SVal, CV)))
assocs)
interpretedRegUis :: [(String, CV)]
interpretedRegUis = ((String, CV) -> Bool) -> [(String, CV)] -> [(String, CV)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> ((String, CV) -> Bool) -> (String, CV) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Bool
isFree (Kind -> Bool) -> ((String, CV) -> Kind) -> (String, CV) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CV -> Kind
forall a. HasKind a => a -> Kind
kindOf (CV -> Kind) -> ((String, CV) -> CV) -> (String, CV) -> Kind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, CV) -> CV
forall a b. (a, b) -> b
snd) [(String, CV)]
uiRegVals
interpretedRegUiSVs :: [(SVal, CV)]
interpretedRegUiSVs = [(String -> Kind -> SVal
cvt String
n (CV -> Kind
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 (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
where r :: State -> IO SV
r State
st = State -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
k (Op -> [SV] -> SBVExpr
SBVApp (String -> Op
Uninterpreted String
nm) [])
interpretedEqs :: [SVal]
interpretedEqs :: [SVal]
interpretedEqs = [Kind -> SVal -> SVal -> SVal
forall a. HasKind a => a -> SVal -> SVal -> SVal
mkNotEq (SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
sv) SVal
sv (Kind -> Either CV (Cached SV) -> SVal
SVal (SVal -> Kind
forall a. HasKind a => a -> Kind
kindOf SVal
sv) (CV -> Either CV (Cached SV)
forall a b. a -> Either a b
Left CV
cv)) | (SVal
sv, CV
cv) <- [(SVal, CV)]
interpretedRegUiSVs [(SVal, CV)] -> [(SVal, CV)] -> [(SVal, CV)]
forall a. Semigroup a => a -> a -> a
<> Seq (SVal, CV) -> [(SVal, CV)]
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
| a -> Bool
forall a. HasKind a => a -> Bool
isDouble a
k Bool -> Bool -> Bool
|| a -> Bool
forall a. HasKind a => a -> Bool
isFloat a
k Bool -> Bool -> Bool
|| a -> 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 (Either CV (Cached SV) -> SVal) -> Either CV (Cached SV) -> SVal
forall a b. (a -> b) -> a -> b
$ Cached SV -> Either CV (Cached SV)
forall a b. b -> Either a b
Right (Cached SV -> Either CV (Cached SV))
-> Cached SV -> Either CV (Cached SV)
forall a b. (a -> b) -> a -> b
$ (State -> IO SV) -> Cached SV
forall a. (State -> IO a) -> Cached a
cache State -> IO SV
r
where r :: State -> IO SV
r 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])
uninterpretedEqs :: [SVal]
uninterpretedEqs :: [SVal]
uninterpretedEqs = ([SVal] -> [SVal]) -> [[SVal]] -> [SVal]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [SVal] -> [SVal]
pwDistinct
([[SVal]] -> [SVal])
-> ([(SVal, CV)] -> [[SVal]]) -> [(SVal, CV)] -> [SVal]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([SVal] -> Bool) -> [[SVal]] -> [[SVal]]
forall a. (a -> Bool) -> [a] -> [a]
filter (\[SVal]
l -> [SVal] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [SVal]
l Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
> Key
1)
([[SVal]] -> [[SVal]])
-> ([(SVal, CV)] -> [[SVal]]) -> [(SVal, CV)] -> [[SVal]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(SVal, CV)] -> [SVal]) -> [[(SVal, CV)]] -> [[SVal]]
forall a b. (a -> b) -> [a] -> [b]
map (((SVal, CV) -> SVal) -> [(SVal, CV)] -> [SVal]
forall a b. (a -> b) -> [a] -> [b]
map (SVal, CV) -> SVal
forall a b. (a, b) -> a
fst)
([[(SVal, CV)]] -> [[SVal]])
-> ([(SVal, CV)] -> [[(SVal, CV)]]) -> [(SVal, CV)] -> [[SVal]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SVal, CV) -> (SVal, CV) -> Bool)
-> [(SVal, CV)] -> [[(SVal, CV)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (CV -> CV -> Bool
forall a. Eq a => a -> a -> Bool
(==) (CV -> CV -> Bool)
-> ((SVal, CV) -> CV) -> (SVal, CV) -> (SVal, CV) -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (SVal, CV) -> CV
forall a b. (a, b) -> b
snd)
([(SVal, CV)] -> [[(SVal, CV)]])
-> ([(SVal, CV)] -> [(SVal, CV)]) -> [(SVal, CV)] -> [[(SVal, CV)]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((SVal, CV) -> CV) -> [(SVal, CV)] -> [(SVal, CV)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (SVal, CV) -> CV
forall a b. (a, b) -> b
snd
([(SVal, CV)] -> [SVal]) -> [(SVal, CV)] -> [SVal]
forall a b. (a -> b) -> a -> b
$ Seq (SVal, CV) -> [(SVal, CV)]
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) <- [SVal] -> [[SVal]]
forall a. [a] -> [[a]]
tails [SVal]
ss, SVal
y <- [SVal]
ys]
uninterpretedReject :: Maybe [String]
uninterpretedFuns :: [String]
(Maybe [String]
uninterpretedReject, [String]
uninterpretedFuns) = (Maybe [String]
uiReject, [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
defs)
where uiReject :: Maybe [String]
uiReject = case [String]
rejects of
[] -> Maybe [String]
forall a. Maybe a
Nothing
[String]
xs -> [String] -> Maybe [String]
forall a. a -> Maybe a
Just [String]
xs
([String]
rejects, [[String]]
defs) = [(String, [String])] -> ([String], [[String]])
forall a b. [(a, b)] -> ([a], [b])
unzip [(String, (SBVType, ([([CV], CV)], CV))) -> (String, [String])
mkNotEq (String, (SBVType, ([([CV], CV)], CV)))
ui | ui :: (String, (SBVType, ([([CV], CV)], CV)))
ui@(String
nm, (SBVType, ([([CV], CV)], CV))
_) <- [(String, (SBVType, ([([CV], CV)], CV)))]
uiFunVals, String
nm String -> t String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t String
uiFunsToReject]
mkNotEq :: (String, (SBVType, ([([CV], CV)], CV))) -> (String, [String])
mkNotEq (String
nm, (SBVType [Kind]
ts, ([([CV], CV)], CV)
vs)) = (String
reject, [String]
def [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
dif)
where nm' :: String
nm' = String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_model" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
cnt
reject :: String
reject = String
nm' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_reject"
scv :: CV -> String
scv = RoundingMode -> CV -> String
cvToSMTLib RoundingMode
RoundNearestTiesToEven
([Kind]
ats, Kind
rt) = ([Kind] -> [Kind]
forall a. [a] -> [a]
init [Kind]
ts, [Kind] -> Kind
forall a. [a] -> a
last [Kind]
ts)
args :: String
args = [String] -> String
unwords [String
"(x!" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" | (Kind
t, Key
i) <- [Kind] -> [Key] -> [(Kind, Key)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Kind]
ats [(Key
0::Int)..]]
res :: String
res = Kind -> String
smtType Kind
rt
params :: [String]
params = [String
"x!" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
i | (Kind
_, Key
i) <- [Kind] -> [Key] -> [(Kind, Key)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Kind]
ats [(Key
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
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
scv CV
fallThru String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> Char -> String
forall a. Key -> a -> [a]
replicate ([([CV], CV)] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [([CV], CV)]
vals) Char
')']
walk (([CV]
as, CV
r) : [([CV], CV)]
rest) = (String
" (ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [CV] -> String
cond [CV]
as String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
scv CV
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"") String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [([CV], CV)] -> [String]
walk [([CV], CV)]
rest
cond :: [CV] -> String
cond [CV]
as = String
"(and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((String -> CV -> String) -> [String] -> [CV] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith String -> CV -> String
eq [String]
params [CV]
as) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
eq :: String -> CV -> String
eq String
p CV
a = String
"(= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CV -> String
scv CV
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
def :: [String]
def = (String
"(define-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
res)
String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ([([CV], CV)], CV) -> [String]
chain ([([CV], CV)], CV)
vs
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
")"]
pad :: String
pad = Key -> Char -> String
forall a. Key -> a -> [a]
replicate (Key
1 Key -> Key -> Key
forall a. Num a => a -> a -> a
+ String -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length String
nm' Key -> Key -> Key
forall a. Num a => a -> a -> a
- String -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length String
nm) Char
' '
dif :: [String]
dif = [ String
"(define-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
reject String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" () Bool"
, String
" (exists (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
, String
" (distinct (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
pad String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
uparams String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
, String
" (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
uparams String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))))"
]
eqs :: [SVal]
eqs = [SVal]
interpretedEqs [SVal] -> [SVal] -> [SVal]
forall a. [a] -> [a] -> [a]
++ [SVal]
uninterpretedEqs
disallow :: Maybe (SBV a)
disallow = case [SVal]
eqs of
[] -> Maybe (SBV a)
forall a. Maybe a
Nothing
[SVal]
_ -> SBV a -> Maybe (SBV a)
forall a. a -> Maybe a
Just (SBV a -> Maybe (SBV a)) -> SBV a -> Maybe (SBV a)
forall a b. (a -> b) -> a -> b
$ SVal -> SBV a
forall a. SVal -> SBV a
SBV (SVal -> SBV a) -> SVal -> SBV a
forall a b. (a -> b) -> a -> b
$ (SVal -> SVal -> SVal) -> [SVal] -> SVal
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 SVal -> SVal -> SVal
svOr [SVal]
eqs
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (SMTConfig -> Bool
allSatPrintAlong SMTConfig
cfg) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ String
"Solution #" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
cnt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
":"
IO () -> m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ SMTConfig -> SMTModel -> String
showModel SMTConfig
cfg SMTModel
model
let resultsSoFar :: AllSatResult
resultsSoFar = AllSatResult
sofar { allSatResults :: [SMTResult]
allSatResults = SMTResult
m SMTResult -> [SMTResult] -> [SMTResult]
forall a. a -> [a] -> [a]
: AllSatResult -> [SMTResult]
allSatResults AllSatResult
sofar }
needMoreIterations :: Bool
needMoreIterations
| Just Key
maxModels <- SMTConfig -> Maybe Key
allSatMaxModelCount SMTConfig
cfg, (Key
cntKey -> Key -> Key
forall a. Num a => a -> a -> a
+Key
1) Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
> Key
maxModels = Bool
False
| Bool
True = Bool
True
if Bool -> Bool
not Bool
needMoreIterations
then Key -> AllSatResult -> m AllSatResult
go (Key
cntKey -> Key -> Key
forall a. Num a => a -> a -> a
+Key
1) AllSatResult
resultsSoFar
else do let uiFunRejector :: String
uiFunRejector = String
"uiFunRejector_model_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Key -> String
forall a. Show a => a -> String
show Key
cnt
header :: String
header = String
"define-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
uiFunRejector String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" () Bool "
defineRejector :: [String] -> m ()
defineRejector [] = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
defineRejector [String
x] = Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
header String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
defineRejector (String
x:[String]
xs) = (String -> m ()) -> [String] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True) ([String] -> m ()) -> [String] -> m ()
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
mergeSExpr ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ (String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
header)
String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String
" (or " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x)
String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
e | String
e <- [String]
xs]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
" ))"]
Maybe String
rejectFuncs <- case Maybe [String]
uninterpretedReject of
Maybe [String]
Nothing -> Maybe String -> m (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe String
forall a. Maybe a
Nothing
Just [String]
fs -> do (String -> m ()) -> [String] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True) ([String] -> m ()) -> [String] -> m ()
forall a b. (a -> b) -> a -> b
$ [String] -> [String]
mergeSExpr [String]
uninterpretedFuns
[String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
defineRejector [String]
fs
Maybe String -> m (Maybe String)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe String -> m (Maybe String))
-> Maybe String -> m (Maybe String)
forall a b. (a -> b) -> a -> b
$ String -> Maybe String
forall a. a -> Maybe a
Just String
uiFunRejector
case (Maybe SBool
forall a. Maybe (SBV a)
disallow, Maybe String
rejectFuncs) of
(Maybe SBool
Nothing, Maybe String
Nothing) -> AllSatResult -> m AllSatResult
forall (f :: * -> *) a. Applicative f => a -> f a
pure AllSatResult
resultsSoFar
(Just SBool
d, Maybe String
Nothing) -> do SBool -> m ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain SBool
d
Key -> AllSatResult -> m AllSatResult
go (Key
cntKey -> Key -> Key
forall a. Num a => a -> a -> a
+Key
1) AllSatResult
resultsSoFar
(Maybe SBool
Nothing, Just String
f) -> do Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
Key -> AllSatResult -> m AllSatResult
go (Key
cntKey -> Key -> Key
forall a. Num a => a -> a -> a
+Key
1) AllSatResult
resultsSoFar
(Just SBool
d, Just String
f) ->
do SBool -> m ()
forall (m :: * -> *). SolverContext m => SBool -> m ()
constrain (SBool -> m ()) -> SBool -> m ()
forall a b. (a -> b) -> a -> b
$ SBool
d SBool -> SBool -> SBool
.=> SBool
d
SV
svd <- IO SV -> m SV
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO SV -> m SV) -> IO SV -> m SV
forall a b. (a -> b) -> a -> b
$ State -> SVal -> IO SV
svToSV State
topState (SBool -> SVal
forall a. SBV a -> SVal
unSBV SBool
d)
Bool -> String -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
Bool -> String -> m ()
send Bool
True (String -> m ()) -> String -> m ()
forall a b. (a -> b) -> a -> b
$ String
"(assert (or " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
svd String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
Key -> AllSatResult -> m AllSatResult
go (Key
cntKey -> Key -> Key
forall a. Num a => a -> a -> a
+Key
1) AllSatResult
resultsSoFar
getUnsatAssumptions :: (MonadIO m, MonadQuery m) => [String] -> [(String, a)] -> m [a]
getUnsatAssumptions :: [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 = String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
forall (m :: * -> *) a.
(MonadIO m, MonadQuery m) =>
String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
"getUnsatAssumptions" String
cmd String
"a list of unsatisfiable assumptions"
(Maybe [String] -> String -> Maybe [String] -> m a)
-> Maybe [String] -> String -> Maybe [String] -> m a
forall a b. (a -> b) -> a -> b
$ [String] -> Maybe [String]
forall a. a -> Maybe a
Just [ 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) = String -> Maybe String
forall a. a -> Maybe a
Just String
s
fromECon SExpr
_ = Maybe String
forall a. Maybe a
Nothing
String
r <- String -> m String
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> m String
ask String
cmd
let walk :: [String] -> [a] -> m [a]
walk [] [a]
sofar = [a] -> m [a]
forall (m :: * -> *) a. Monad m => a -> m a
return ([a] -> m [a]) -> [a] -> m [a]
forall a b. (a -> b) -> a -> b
$ [a] -> [a]
forall a. [a] -> [a]
reverse [a]
sofar
walk (String
a:[String]
as) [a]
sofar = case String
a String -> [(String, a)] -> Maybe a
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(String, a)]
proxyMap of
Just a
v -> [String] -> [a] -> m [a]
walk [String]
as (a
va -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
sofar)
Maybe a
Nothing -> do [String] -> m ()
forall (m :: * -> *). (MonadIO m, MonadQuery m) => [String] -> m ()
queryDebug [ String
"*** In call to 'getUnsatAssumptions'"
, String
"***"
, String
"*** Unexpected assumption named: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
a
, String
"*** Was expecting one of : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
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
String
-> (String -> Maybe [String] -> m [a]) -> (SExpr -> m [a]) -> m [a]
forall a.
String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse String
r String -> Maybe [String] -> m [a]
forall a. String -> Maybe [String] -> m a
bad ((SExpr -> m [a]) -> m [a]) -> (SExpr -> m [a]) -> m [a]
forall a b. (a -> b) -> a -> b
$ \case
EApp [SExpr]
es | Just [String]
xs <- (SExpr -> Maybe String) -> [SExpr] -> Maybe [String]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SExpr -> Maybe String
fromECon [SExpr]
es -> [String] -> [a] -> m [a]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
[String] -> [a] -> m [a]
walk [String]
xs []
SExpr
_ -> String -> Maybe [String] -> m [a]
forall a. String -> Maybe [String] -> m a
bad String
r Maybe [String]
forall a. Maybe a
Nothing
timeout :: (MonadIO m, MonadQuery m) => Int -> m a -> m a
timeout :: Key -> m a -> m a
timeout Key
n m a
q = do (QueryState -> QueryState) -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(QueryState -> QueryState) -> m ()
modifyQueryState (\QueryState
qs -> QueryState
qs {queryTimeOutValue :: Maybe Key
queryTimeOutValue = Key -> Maybe Key
forall a. a -> Maybe a
Just Key
n})
a
r <- m a
q
(QueryState -> QueryState) -> m ()
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
(QueryState -> QueryState) -> m ()
modifyQueryState (\QueryState
qs -> QueryState
qs {queryTimeOutValue :: Maybe Key
queryTimeOutValue = Maybe Key
forall a. Maybe a
Nothing})
a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return a
r
parse :: String -> (String -> Maybe [String] -> a) -> (SExpr -> a) -> a
parse :: 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 ([String] -> Maybe [String]
forall a. a -> Maybe a
Just [String
e])
Right SExpr
res -> SExpr -> a
sCont SExpr
res
unexpected :: (MonadIO m, MonadQuery m) => String -> String -> String -> Maybe [String] -> String -> Maybe [String] -> m a
unexpected :: String
-> String
-> String
-> Maybe [String]
-> String
-> Maybe [String]
-> m a
unexpected String
ctx String
sent String
expected Maybe [String]
mbHint String
received Maybe [String]
mbReason = do
[String]
extras <- String -> Maybe Key -> m [String]
forall (m :: * -> *).
(MonadIO m, MonadQuery m) =>
String -> Maybe Key -> m [String]
retrieveResponse String
"terminating upon unexpected response" (Key -> Maybe Key
forall a. a -> Maybe a
Just Key
5000000)
SMTConfig
cfg <- m SMTConfig
forall (m :: * -> *). (MonadIO m, MonadQuery m) => m SMTConfig
getConfig
let exc :: SBVException
exc = SBVException :: String
-> Maybe String
-> Maybe String
-> Maybe String
-> Maybe String
-> Maybe String
-> Maybe ExitCode
-> SMTConfig
-> Maybe [String]
-> Maybe [String]
-> SBVException
SBVException { sbvExceptionDescription :: String
sbvExceptionDescription = String
"Unexpected response from the solver, context: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ctx
, sbvExceptionSent :: Maybe String
sbvExceptionSent = String -> Maybe String
forall a. a -> Maybe a
Just String
sent
, sbvExceptionExpected :: Maybe String
sbvExceptionExpected = String -> Maybe String
forall a. a -> Maybe a
Just String
expected
, sbvExceptionReceived :: Maybe String
sbvExceptionReceived = String -> Maybe String
forall a. a -> Maybe a
Just String
received
, sbvExceptionStdOut :: Maybe String
sbvExceptionStdOut = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [String]
extras
, sbvExceptionStdErr :: Maybe String
sbvExceptionStdErr = Maybe String
forall a. Maybe a
Nothing
, sbvExceptionExitCode :: Maybe ExitCode
sbvExceptionExitCode = Maybe ExitCode
forall a. Maybe a
Nothing
, sbvExceptionConfig :: SMTConfig
sbvExceptionConfig = SMTConfig
cfg
, sbvExceptionReason :: Maybe [String]
sbvExceptionReason = Maybe [String]
mbReason
, sbvExceptionHint :: Maybe [String]
sbvExceptionHint = Maybe [String]
mbHint
}
IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
io (IO a -> m a) -> IO a -> m a
forall a b. (a -> b) -> a -> b
$ SBVException -> IO a
forall e a. Exception e => e -> IO a
C.throwIO SBVException
exc
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 [((Key, Kind, Kind), [SV])]
tbls [(Key, 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
_ -> String -> (SMTConfig, Bool, Bool, Bool)
forall a. HasCallStack => String -> a
error (String -> (SMTConfig, Bool, Bool, Bool))
-> String -> (SMTConfig, Bool, Bool, Bool)
forall a b. (a -> b) -> a -> b
$ String
"runProofOn: Unexpected run mode: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVRunMode -> String
forall a. Show a => a -> String
show SBVRunMode
rm
flipQ :: (Quantifier, b) -> (Quantifier, b)
flipQ (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) = [Either SV (SV, [SV])] -> [Either SV (SV, [SV])]
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
vSV -> [SV] -> [SV]
forall a. a -> [a] -> [a]
:[SV]
us, SV -> Either SV (SV, [SV])
forall a b. a -> Either a b
Left SV
v Either SV (SV, [SV])
-> [Either SV (SV, [SV])] -> [Either SV (SV, [SV])]
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, (SV, [SV]) -> Either SV (SV, [SV])
forall a b. b -> Either a b
Right (SV
v, [SV] -> [SV]
forall a. [a] -> [a]
reverse [SV]
us) Either SV (SV, [SV])
-> [Either SV (SV, [SV])] -> [Either SV (SV, [SV])]
forall a. a -> [a] -> [a]
: [Either SV (SV, [SV])]
sofar)
qinps :: [(Quantifier, NamedSymVar)]
qinps = if Bool
isSat then ([(Quantifier, NamedSymVar)], [NamedSymVar])
-> [(Quantifier, NamedSymVar)]
forall a b. (a, b) -> a
fst ([(Quantifier, NamedSymVar)], [NamedSymVar])
is else ((Quantifier, NamedSymVar) -> (Quantifier, NamedSymVar))
-> [(Quantifier, NamedSymVar)] -> [(Quantifier, NamedSymVar)]
forall a b. (a -> b) -> [a] -> [b]
map (Quantifier, NamedSymVar) -> (Quantifier, NamedSymVar)
forall b. (Quantifier, b) -> (Quantifier, b)
flipQ (([(Quantifier, NamedSymVar)], [NamedSymVar])
-> [(Quantifier, NamedSymVar)]
forall a b. (a, b) -> a
fst ([(Quantifier, NamedSymVar)], [NamedSymVar])
is)
skolemMap :: [Either SV (SV, [SV])]
skolemMap = [(Quantifier, NamedSymVar)] -> [Either SV (SV, [SV])]
skolemize [(Quantifier, NamedSymVar)]
qinps
o :: SV
o | Bool
isSafe = SV
trueSV
| Bool
True = case [SV]
outputs of
[] | Bool
isSetup -> SV
trueSV
[SV
so] -> case SV
so of
SV Kind
KBool NodeId
_ -> SV
so
SV
_ -> String -> SV
forall a. HasCallStack => String -> a
error (String -> SV) -> String -> SV
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Impossible happened, non-boolean output: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
so
, String
"Detected while generating the trace:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Result -> String
forall a. Show a => a -> String
show Result
res
]
[SV]
os -> String -> SV
forall a. HasCallStack => String -> a
error (String -> SV) -> String -> SV
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"User error: Multiple output values detected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SV] -> String
forall a. Show a => a -> String
show [SV]
os
, String
"Detected while generating the trace:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Result -> String
forall a. Show a => a -> String
show Result
res
, String
"*** Check calls to \"output\", they are typically not needed!"
]
in SMTProblem :: (SMTConfig -> SMTLibPgm) -> SMTProblem
SMTProblem { smtLibPgm :: SMTConfig -> SMTLibPgm
smtLibPgm = SMTConfig -> SMTLibConverter SMTLibPgm
toSMTLib SMTConfig
config QueryContext
context KindSet
ki Bool
isSat [String]
comments ([(Quantifier, NamedSymVar)], [NamedSymVar])
is [Either SV (SV, [SV])]
skolemMap (CnstMap, [(SV, CV)])
consts [((Key, Kind, Kind), [SV])]
tbls [(Key, ArrayInfo)]
arrs [(String, SBVType)]
uis [(Bool, String, [String])]
axs SBVPgm
pgm Seq (Bool, [(String, String)], SV)
cstrs SV
o }
executeQuery :: forall m a. ExtractIO m => QueryContext -> QueryT m a -> SymbolicT m a
executeQuery :: QueryContext -> QueryT m a -> SymbolicT m a
executeQuery QueryContext
queryContext (QueryT ReaderT State m a
userQuery) = do
State
st <- SymbolicT m State
forall (m :: * -> *). MonadSymbolic m => m State
symbolicEnv
SBVRunMode
rm <- IO SBVRunMode -> SymbolicT m SBVRunMode
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO SBVRunMode -> SymbolicT m SBVRunMode)
-> IO SBVRunMode -> SymbolicT m SBVRunMode
forall a b. (a -> b) -> a -> b
$ IORef SBVRunMode -> IO SBVRunMode
forall a. IORef a -> IO a
readIORef (State -> IORef SBVRunMode
runMode State
st)
() <- IO () -> SymbolicT m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> SymbolicT m ()) -> IO () -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ case (QueryContext
queryContext, SBVRunMode
rm) of
(QueryContext
QueryInternal, SBVRunMode
_) -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(QueryContext
QueryExternal, SMTMode QueryContext
QueryExternal IStage
ISetup Bool
_ SMTConfig
_) -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
(QueryContext, SBVRunMode)
_ -> SBVRunMode -> IO ()
forall a a. Show a => a -> a
invalidQuery SBVRunMode
rm
let allowQQs :: Bool
allowQQs = case SBVRunMode
rm of
SMTMode QueryContext
_ IStage
_ Bool
_ SMTConfig
cfg -> SMTConfig -> Bool
allowQuantifiedQueries SMTConfig
cfg
SBVRunMode
CodeGen -> Bool
False
Concrete{} -> Bool
False
() <- Bool -> SymbolicT m () -> SymbolicT m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
allowQQs (SymbolicT m () -> SymbolicT m ())
-> SymbolicT m () -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ IO () -> SymbolicT m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> SymbolicT m ()) -> IO () -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$
case QueryContext
queryContext of
QueryContext
QueryInternal -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
QueryContext
QueryExternal -> do
[(Quantifier, NamedSymVar)]
userInps <- UserInputs -> [(Quantifier, NamedSymVar)]
userInputsToList (UserInputs -> [(Quantifier, NamedSymVar)])
-> (Inputs -> UserInputs) -> Inputs -> [(Quantifier, NamedSymVar)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Inputs -> UserInputs
userInputs (Inputs -> [(Quantifier, NamedSymVar)])
-> IO Inputs -> IO [(Quantifier, NamedSymVar)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef Inputs -> IO Inputs
forall a. IORef a -> IO a
readIORef (State -> IORef Inputs
rinps State
st)
let badInps :: [String]
badInps = [String] -> [String]
forall a. [a] -> [a]
reverse [String
n | (Quantifier
ALL, NamedSymVar -> String
getUserName' -> String
n) <- [(Quantifier, NamedSymVar)]
userInps]
case [String]
badInps of
[] -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
[String]
_ -> let plu :: String
plu | [String] -> Key
forall (t :: * -> *) a. Foldable t => t a -> Key
length [String]
badInps Key -> Key -> Bool
forall a. Ord a => a -> a -> Bool
> Key
1 = String
"s require"
| Bool
True = String
" requires"
in String -> IO ()
forall a. HasCallStack => String -> a
error (String -> IO ()) -> String -> IO ()
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" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
plu String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" explicit quantification: "
, String
"***"
, String
"*** " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
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
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
-> forall res.
SMTConfig -> State -> String -> (State -> IO res) -> IO res
engine SMTSolver
slvr
let dsatOK :: Bool
dsatOK = Maybe Double -> Bool
forall a. Maybe a -> Bool
isNothing (SMTConfig -> Maybe Double
dsatPrecision SMTConfig
cfg)
Bool -> Bool -> Bool
|| Maybe String -> Bool
forall a. Maybe a -> Bool
isJust (SolverCapabilities -> Maybe String
supportsDeltaSat (SMTSolver -> SolverCapabilities
capabilities SMTSolver
slvr))
Bool -> SymbolicT m () -> SymbolicT m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
dsatOK (SymbolicT m () -> SymbolicT m ())
-> SymbolicT m () -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ String -> SymbolicT m ()
forall a. HasCallStack => String -> a
error (String -> SymbolicT m ()) -> String -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
[ String
""
, String
"*** Data.SBV: Delta-sat precision is specified."
, String
"*** But the chosen solver (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Solver -> String
forall a. Show a => a -> String
show (SMTSolver -> Solver
name SMTSolver
slvr) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") does not support"
, String
"*** delta-satisfiability."
]
Result
res <- IO Result -> SymbolicT m Result
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Result -> SymbolicT m Result)
-> IO Result -> SymbolicT m Result
forall a b. (a -> b) -> a -> b
$ State -> IO Result
extractSymbolicSimulationState State
st
[SMTOption]
setOpts <- IO [SMTOption] -> SymbolicT m [SMTOption]
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO [SMTOption] -> SymbolicT m [SMTOption])
-> IO [SMTOption] -> SymbolicT m [SMTOption]
forall a b. (a -> b) -> a -> b
$ [SMTOption] -> [SMTOption]
forall a. [a] -> [a]
reverse ([SMTOption] -> [SMTOption]) -> IO [SMTOption] -> IO [SMTOption]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef [SMTOption] -> IO [SMTOption]
forall a. IORef a -> IO a
readIORef (State -> IORef [SMTOption]
rSMTOptions State
st)
let SMTProblem{SMTConfig -> SMTLibPgm
smtLibPgm :: SMTConfig -> SMTLibPgm
smtLibPgm :: SMTProblem -> SMTConfig -> SMTLibPgm
smtLibPgm} = SBVRunMode -> QueryContext -> [String] -> Result -> SMTProblem
runProofOn SBVRunMode
rm QueryContext
queryContext [] Result
res
cfg' :: SMTConfig
cfg' = SMTConfig
cfg { solverSetOptions :: [SMTOption]
solverSetOptions = SMTConfig -> [SMTOption]
solverSetOptions SMTConfig
cfg [SMTOption] -> [SMTOption] -> [SMTOption]
forall a. [a] -> [a] -> [a]
++ [SMTOption]
setOpts }
pgm :: SMTLibPgm
pgm = SMTConfig -> SMTLibPgm
smtLibPgm SMTConfig
cfg'
IO () -> SymbolicT m ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> SymbolicT m ()) -> IO () -> SymbolicT m ()
forall a b. (a -> b) -> a -> b
$ IORef SBVRunMode -> SBVRunMode -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef (State -> IORef SBVRunMode
runMode State
st) (SBVRunMode -> IO ()) -> SBVRunMode -> IO ()
forall a b. (a -> b) -> a -> b
$ QueryContext -> IStage -> Bool -> SMTConfig -> SBVRunMode
SMTMode QueryContext
qc IStage
IRun Bool
isSAT SMTConfig
cfg
m a -> SymbolicT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> SymbolicT m a) -> m a -> SymbolicT m a
forall a b. (a -> b) -> a -> b
$ m (m a) -> m a
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (m (m a) -> m a) -> m (m a) -> m a
forall a b. (a -> b) -> a -> b
$ IO (m a) -> m (m a)
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (m a) -> m (m a)) -> IO (m a) -> m (m a)
forall a b. (a -> b) -> a -> b
$ SMTConfig -> State -> String -> (State -> IO (m a)) -> IO (m a)
forall res.
SMTConfig -> State -> String -> (State -> IO res) -> IO res
backend SMTConfig
cfg' State
st (SMTLibPgm -> String
forall a. Show a => a -> String
show SMTLibPgm
pgm) ((State -> IO (m a)) -> IO (m a))
-> (State -> IO (m a)) -> IO (m a)
forall a b. (a -> b) -> a -> b
$ m a -> IO (m a)
forall (m :: * -> *) a. ExtractIO m => m a -> IO (m a)
extractIO (m a -> IO (m a)) -> (State -> m a) -> State -> IO (m a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReaderT State m a -> State -> m a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT State m a
userQuery
SMTMode QueryContext
_ IStage
IRun Bool
_ SMTConfig
_ -> String -> SymbolicT m a
forall a. HasCallStack => String -> a
error (String -> SymbolicT m a) -> String -> SymbolicT m a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ 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."
]
SBVRunMode
_ -> SBVRunMode -> SymbolicT m a
forall a a. Show a => a -> a
invalidQuery SBVRunMode
rm
where invalidQuery :: a -> a
invalidQuery a
rm = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
, String
"*** Data.SBV: Invalid query call."
, String
"***"
, String
"*** Current mode: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
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) #-}