{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}
module Data.SBV.Lambda (
lambda, lambdaStr
, namedLambda, namedLambdaStr
, constraint, constraintStr
) where
import Control.Monad (join)
import Control.Monad.Trans (liftIO, MonadIO)
import Data.SBV.Core.Data
import Data.SBV.Core.Kind
import Data.SBV.SMT.SMTLib2
import Data.SBV.Utils.PrettyNum
import Data.SBV.Core.Symbolic hiding (mkNewState, fresh)
import qualified Data.SBV.Core.Symbolic as S (mkNewState)
import Data.IORef (readIORef, modifyIORef')
import Data.List
import qualified Data.Foldable as F
import qualified Data.Map.Strict as M
import qualified Data.Generics.Uniplate.Data as G
data Defn = Defn [String]
(Maybe [(Quantifier, String)])
(Int -> String)
inSubState :: MonadIO m => State -> (State -> m b) -> m b
inSubState :: forall (m :: * -> *) b. MonadIO m => State -> (State -> m b) -> m b
inSubState State
inState State -> m b
comp = do
Int
ll <- IO Int -> m Int
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Int -> m Int) -> IO Int -> m Int
forall a b. (a -> b) -> a -> b
$ IORef Int -> IO Int
forall a. IORef a -> IO a
readIORef (State -> IORef Int
rLambdaLevel State
inState)
State
stEmpty <- SMTConfig -> SBVRunMode -> m State
forall (m :: * -> *).
MonadIO m =>
SMTConfig -> SBVRunMode -> m State
S.mkNewState (State -> SMTConfig
stCfg State
inState) (Int -> SBVRunMode
LambdaGen (Int
ll Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))
let share :: (State -> t) -> t
share State -> t
fld = State -> t
fld State
inState
fresh :: (State -> t) -> t
fresh State -> t
fld = State -> t
fld State
stEmpty
State -> m b
comp State {
sbvContext :: SBVContext
sbvContext = (State -> SBVContext) -> SBVContext
forall {t}. (State -> t) -> t
share State -> SBVContext
sbvContext
, pathCond :: SVal
pathCond = (State -> SVal) -> SVal
forall {t}. (State -> t) -> t
share State -> SVal
pathCond
, startTime :: UTCTime
startTime = (State -> UTCTime) -> UTCTime
forall {t}. (State -> t) -> t
share State -> UTCTime
startTime
, rProgInfo :: IORef ProgInfo
rProgInfo = (State -> IORef ProgInfo) -> IORef ProgInfo
forall {t}. (State -> t) -> t
share State -> IORef ProgInfo
rProgInfo
, rIncState :: IORef IncState
rIncState = (State -> IORef IncState) -> IORef IncState
forall {t}. (State -> t) -> t
share State -> IORef IncState
rIncState
, rCInfo :: IORef [(String, CV)]
rCInfo = (State -> IORef [(String, CV)]) -> IORef [(String, CV)]
forall {t}. (State -> t) -> t
share State -> IORef [(String, CV)]
rCInfo
, rUsedKinds :: IORef KindSet
rUsedKinds = (State -> IORef KindSet) -> IORef KindSet
forall {t}. (State -> t) -> t
share State -> IORef KindSet
rUsedKinds
, rUsedLbls :: IORef (Set String)
rUsedLbls = (State -> IORef (Set String)) -> IORef (Set String)
forall {t}. (State -> t) -> t
share State -> IORef (Set String)
rUsedLbls
, rUIMap :: IORef UIMap
rUIMap = (State -> IORef UIMap) -> IORef UIMap
forall {t}. (State -> t) -> t
share State -> IORef UIMap
rUIMap
, rUserFuncs :: IORef (Set String)
rUserFuncs = (State -> IORef (Set String)) -> IORef (Set String)
forall {t}. (State -> t) -> t
share State -> IORef (Set String)
rUserFuncs
, rCgMap :: IORef CgMap
rCgMap = (State -> IORef CgMap) -> IORef CgMap
forall {t}. (State -> t) -> t
share State -> IORef CgMap
rCgMap
, rDefns :: IORef [(SMTDef, SBVType)]
rDefns = (State -> IORef [(SMTDef, SBVType)]) -> IORef [(SMTDef, SBVType)]
forall {t}. (State -> t) -> t
share State -> IORef [(SMTDef, SBVType)]
rDefns
, rSMTOptions :: IORef [SMTOption]
rSMTOptions = (State -> IORef [SMTOption]) -> IORef [SMTOption]
forall {t}. (State -> t) -> t
share State -> IORef [SMTOption]
rSMTOptions
, rOptGoals :: IORef [Objective (SV, SV)]
rOptGoals = (State -> IORef [Objective (SV, SV)]) -> IORef [Objective (SV, SV)]
forall {t}. (State -> t) -> t
share State -> IORef [Objective (SV, SV)]
rOptGoals
, rAsserts :: IORef [(String, Maybe CallStack, SV)]
rAsserts = (State -> IORef [(String, Maybe CallStack, SV)])
-> IORef [(String, Maybe CallStack, SV)]
forall {t}. (State -> t) -> t
share State -> IORef [(String, Maybe CallStack, SV)]
rAsserts
, rOutstandingAsserts :: IORef Bool
rOutstandingAsserts = (State -> IORef Bool) -> IORef Bool
forall {t}. (State -> t) -> t
share State -> IORef Bool
rOutstandingAsserts
, rPartitionVars :: IORef [String]
rPartitionVars = (State -> IORef [String]) -> IORef [String]
forall {t}. (State -> t) -> t
share State -> IORef [String]
rPartitionVars
, stCfg :: SMTConfig
stCfg = (State -> SMTConfig) -> SMTConfig
forall {t}. (State -> t) -> t
fresh State -> SMTConfig
stCfg
, runMode :: IORef SBVRunMode
runMode = (State -> IORef SBVRunMode) -> IORef SBVRunMode
forall {t}. (State -> t) -> t
fresh State -> IORef SBVRunMode
runMode
, rctr :: IORef Int
rctr = (State -> IORef Int) -> IORef Int
forall {t}. (State -> t) -> t
fresh State -> IORef Int
rctr
, rLambdaLevel :: IORef Int
rLambdaLevel = (State -> IORef Int) -> IORef Int
forall {t}. (State -> t) -> t
fresh State -> IORef Int
rLambdaLevel
, rtblMap :: IORef TableMap
rtblMap = (State -> IORef TableMap) -> IORef TableMap
forall {t}. (State -> t) -> t
fresh State -> IORef TableMap
rtblMap
, rArrayMap :: IORef ArrayMap
rArrayMap = (State -> IORef ArrayMap) -> IORef ArrayMap
forall {t}. (State -> t) -> t
fresh State -> IORef ArrayMap
rArrayMap
, rAICache :: IORef (Cache ArrayIndex)
rAICache = (State -> IORef (Cache ArrayIndex)) -> IORef (Cache ArrayIndex)
forall {t}. (State -> t) -> t
fresh State -> IORef (Cache ArrayIndex)
rAICache
, rinps :: IORef Inputs
rinps = (State -> IORef Inputs) -> IORef Inputs
forall {t}. (State -> t) -> t
fresh State -> IORef Inputs
rinps
, rlambdaInps :: IORef LambdaInputs
rlambdaInps = (State -> IORef LambdaInputs) -> IORef LambdaInputs
forall {t}. (State -> t) -> t
fresh State -> IORef LambdaInputs
rlambdaInps
, rConstraints :: IORef (Seq (Bool, [(String, String)], SV))
rConstraints = (State -> IORef (Seq (Bool, [(String, String)], SV)))
-> IORef (Seq (Bool, [(String, String)], SV))
forall {t}. (State -> t) -> t
fresh State -> IORef (Seq (Bool, [(String, String)], SV))
rConstraints
, rObservables :: IORef (Seq (Name, CV -> Bool, SV))
rObservables = (State -> IORef (Seq (Name, CV -> Bool, SV)))
-> IORef (Seq (Name, CV -> Bool, SV))
forall {t}. (State -> t) -> t
fresh State -> IORef (Seq (Name, CV -> Bool, SV))
rObservables
, routs :: IORef [SV]
routs = (State -> IORef [SV]) -> IORef [SV]
forall {t}. (State -> t) -> t
fresh State -> IORef [SV]
routs
, spgm :: IORef SBVPgm
spgm = (State -> IORef SBVPgm) -> IORef SBVPgm
forall {t}. (State -> t) -> t
fresh State -> IORef SBVPgm
spgm
, rconstMap :: IORef CnstMap
rconstMap = (State -> IORef CnstMap) -> IORef CnstMap
forall {t}. (State -> t) -> t
fresh State -> IORef CnstMap
rconstMap
, rexprMap :: IORef ExprMap
rexprMap = (State -> IORef ExprMap) -> IORef ExprMap
forall {t}. (State -> t) -> t
fresh State -> IORef ExprMap
rexprMap
, rSVCache :: IORef (Cache SV)
rSVCache = (State -> IORef (Cache SV)) -> IORef (Cache SV)
forall {t}. (State -> t) -> t
fresh State -> IORef (Cache SV)
rSVCache
, rQueryState :: IORef (Maybe QueryState)
rQueryState = (State -> IORef (Maybe QueryState)) -> IORef (Maybe QueryState)
forall {t}. (State -> t) -> t
fresh State -> IORef (Maybe QueryState)
rQueryState
, parentState :: Maybe State
parentState = State -> Maybe State
forall a. a -> Maybe a
Just State
inState
}
extractAllUniversals :: [(Quantifier, String)] -> String
[(Quantifier
ALL, String
s)] = String
s
extractAllUniversals [(Quantifier, String)]
other = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
, String
"*** Data.SBV.Lambda: Impossible happened. Got existential quantifiers."
, String
"***"
, String
"*** Params: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Quantifier, String)] -> String
forall a. Show a => a -> String
show [(Quantifier, String)]
other
, String
"***"
, String
"*** Please report this as a bug!"
]
lambdaGen :: (MonadIO m, Lambda (SymbolicT m) a) => (Defn -> b) -> State -> Kind -> a -> m b
lambdaGen :: forall (m :: * -> *) a b.
(MonadIO m, Lambda (SymbolicT m) a) =>
(Defn -> b) -> State -> Kind -> a -> m b
lambdaGen Defn -> b
trans State
inState Kind
fk a
f = State -> (State -> m b) -> m b
forall (m :: * -> *) b. MonadIO m => State -> (State -> m b) -> m b
inSubState State
inState ((State -> m b) -> m b) -> (State -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ \State
st -> Defn -> b
trans (Defn -> b) -> m Defn -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State -> Kind -> SymbolicT m () -> m Defn
forall (m :: * -> *).
MonadIO m =>
State -> Kind -> SymbolicT m () -> m Defn
convert State
st Kind
fk (State -> a -> SymbolicT m ()
forall (m :: * -> *) a. Lambda m a => State -> a -> m ()
mkLambda State
st a
f)
lambda :: (MonadIO m, Lambda (SymbolicT m) a) => State -> Kind -> a -> m SMTDef
lambda :: forall (m :: * -> *) a.
(MonadIO m, Lambda (SymbolicT m) a) =>
State -> Kind -> a -> m SMTDef
lambda State
inState Kind
fk = (Defn -> SMTDef) -> State -> Kind -> a -> m SMTDef
forall (m :: * -> *) a b.
(MonadIO m, Lambda (SymbolicT m) a) =>
(Defn -> b) -> State -> Kind -> a -> m b
lambdaGen Defn -> SMTDef
mkLam State
inState Kind
fk
where mkLam :: Defn -> SMTDef
mkLam (Defn [String]
frees Maybe [(Quantifier, String)]
params Int -> String
body) = Kind -> [String] -> Maybe String -> (Int -> String) -> SMTDef
SMTLam Kind
fk [String]
frees ([(Quantifier, String)] -> String
extractAllUniversals ([(Quantifier, String)] -> String)
-> Maybe [(Quantifier, String)] -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [(Quantifier, String)]
params) Int -> String
body
lambdaStr :: (MonadIO m, Lambda (SymbolicT m) a) => State -> Kind -> a -> m String
lambdaStr :: forall (m :: * -> *) a.
(MonadIO m, Lambda (SymbolicT m) a) =>
State -> Kind -> a -> m String
lambdaStr = (Defn -> String) -> State -> Kind -> a -> m String
forall (m :: * -> *) a b.
(MonadIO m, Lambda (SymbolicT m) a) =>
(Defn -> b) -> State -> Kind -> a -> m b
lambdaGen Defn -> String
mkLam
where mkLam :: Defn -> String
mkLam (Defn [String]
_frees Maybe [(Quantifier, String)]
Nothing Int -> String
body) = Int -> String
body Int
0
mkLam (Defn [String]
_frees (Just [(Quantifier, String)]
params) Int -> String
body) = String
"(lambda " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Quantifier, String)] -> String
extractAllUniversals [(Quantifier, String)]
params String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
body Int
2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
namedLambdaGen :: (MonadIO m, Lambda (SymbolicT m) a) => (Defn -> b) -> State -> Kind -> a -> m b
namedLambdaGen :: forall (m :: * -> *) a b.
(MonadIO m, Lambda (SymbolicT m) a) =>
(Defn -> b) -> State -> Kind -> a -> m b
namedLambdaGen Defn -> b
trans State
inState Kind
fk a
f = State -> (State -> m b) -> m b
forall (m :: * -> *) b. MonadIO m => State -> (State -> m b) -> m b
inSubState State
inState ((State -> m b) -> m b) -> (State -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ \State
st -> Defn -> b
trans (Defn -> b) -> m Defn -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State -> Kind -> SymbolicT m () -> m Defn
forall (m :: * -> *).
MonadIO m =>
State -> Kind -> SymbolicT m () -> m Defn
convert State
st Kind
fk (State -> a -> SymbolicT m ()
forall (m :: * -> *) a. Lambda m a => State -> a -> m ()
mkLambda State
st a
f)
namedLambda :: (MonadIO m, Lambda (SymbolicT m) a) => State -> String -> Kind -> a -> m SMTDef
namedLambda :: forall (m :: * -> *) a.
(MonadIO m, Lambda (SymbolicT m) a) =>
State -> String -> Kind -> a -> m SMTDef
namedLambda State
inState String
nm Kind
fk = (Defn -> SMTDef) -> State -> Kind -> a -> m SMTDef
forall (m :: * -> *) a b.
(MonadIO m, Lambda (SymbolicT m) a) =>
(Defn -> b) -> State -> Kind -> a -> m b
namedLambdaGen Defn -> SMTDef
mkDef State
inState Kind
fk
where mkDef :: Defn -> SMTDef
mkDef (Defn [String]
frees Maybe [(Quantifier, String)]
params Int -> String
body) = String
-> Kind -> [String] -> Maybe String -> (Int -> String) -> SMTDef
SMTDef String
nm Kind
fk [String]
frees ([(Quantifier, String)] -> String
extractAllUniversals ([(Quantifier, String)] -> String)
-> Maybe [(Quantifier, String)] -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [(Quantifier, String)]
params) Int -> String
body
namedLambdaStr :: (MonadIO m, Lambda (SymbolicT m) a) => State -> String -> SBVType -> a -> m String
namedLambdaStr :: forall (m :: * -> *) a.
(MonadIO m, Lambda (SymbolicT m) a) =>
State -> String -> SBVType -> a -> m String
namedLambdaStr State
inState String
nm SBVType
t = (Defn -> String) -> State -> Kind -> a -> m String
forall (m :: * -> *) a b.
(MonadIO m, Lambda (SymbolicT m) a) =>
(Defn -> b) -> State -> Kind -> a -> m b
namedLambdaGen Defn -> String
mkDef State
inState Kind
fk
where mkDef :: Defn -> String
mkDef (Defn [String]
frees Maybe [(Quantifier, String)]
params Int -> String
body) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ [(SMTDef, SBVType)] -> [String]
declUserFuns [(String
-> Kind -> [String] -> Maybe String -> (Int -> String) -> SMTDef
SMTDef String
nm Kind
fk [String]
frees ([(Quantifier, String)] -> String
extractAllUniversals ([(Quantifier, String)] -> String)
-> Maybe [(Quantifier, String)] -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [(Quantifier, String)]
params) Int -> String
body, SBVType
t)]
fk :: Kind
fk = case SBVType
t of
SBVType [] -> String -> Kind
forall a. HasCallStack => String -> a
error (String -> Kind) -> String -> Kind
forall a b. (a -> b) -> a -> b
$ String
"namedLambdaStr: Invalid type for " 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
", empty!"
SBVType [Kind]
xs -> [Kind] -> Kind
forall a. HasCallStack => [a] -> a
last [Kind]
xs
constraintGen :: (MonadIO m, Constraint (SymbolicT m) a) => ([String] -> (Int -> String) -> b) -> State -> a -> m b
constraintGen :: forall (m :: * -> *) a b.
(MonadIO m, Constraint (SymbolicT m) a) =>
([String] -> (Int -> String) -> b) -> State -> a -> m b
constraintGen [String] -> (Int -> String) -> b
trans inState :: State
inState@State{IORef ProgInfo
rProgInfo :: State -> IORef ProgInfo
rProgInfo :: IORef ProgInfo
rProgInfo} a
f = do
IO () -> m ()
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> m ()) -> IO () -> m ()
forall a b. (a -> b) -> a -> b
$ IORef ProgInfo -> (ProgInfo -> ProgInfo) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef ProgInfo
rProgInfo (\ProgInfo
u -> ProgInfo
u{hasQuants = True})
let mkDef :: Defn -> b
mkDef (Defn [String]
deps Maybe [(Quantifier, String)]
Nothing Int -> String
body) = [String] -> (Int -> String) -> b
trans [String]
deps Int -> String
body
mkDef (Defn [String]
deps (Just [(Quantifier, String)]
params) Int -> String
body) = [String] -> (Int -> String) -> b
trans [String]
deps ((Int -> String) -> b) -> (Int -> String) -> b
forall a b. (a -> b) -> a -> b
$ \Int
i -> [String] -> String
unwords (((Quantifier, String) -> String)
-> [(Quantifier, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Quantifier, String) -> String
mkGroup [(Quantifier, String)]
params) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
body (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
2)
String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate ([(Quantifier, String)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Quantifier, String)]
params) Char
')'
mkGroup :: (Quantifier, String) -> String
mkGroup (Quantifier
ALL, String
s) = String
"(forall " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
mkGroup (Quantifier
EX, String
s) = String
"(exists " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
State -> (State -> m b) -> m b
forall (m :: * -> *) b. MonadIO m => State -> (State -> m b) -> m b
inSubState State
inState ((State -> m b) -> m b) -> (State -> m b) -> m b
forall a b. (a -> b) -> a -> b
$ \State
st -> Defn -> b
mkDef (Defn -> b) -> m Defn -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State -> Kind -> SymbolicT m () -> m Defn
forall (m :: * -> *).
MonadIO m =>
State -> Kind -> SymbolicT m () -> m Defn
convert State
st Kind
KBool (State -> a -> SymbolicT m ()
forall (m :: * -> *) a. Constraint m a => State -> a -> m ()
mkConstraint State
st a
f SymbolicT m () -> (() -> SymbolicT m ()) -> SymbolicT m ()
forall a b. SymbolicT m a -> (a -> SymbolicT m b) -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= () -> SymbolicT m ()
forall a (m :: * -> *).
(Outputtable a, MonadSymbolic m) =>
a -> m a
forall (m :: * -> *). MonadSymbolic m => () -> m ()
output SymbolicT m () -> SymbolicT m () -> SymbolicT m ()
forall a b. SymbolicT m a -> SymbolicT m b -> SymbolicT m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> SymbolicT m ()
forall a. a -> SymbolicT m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
instance Constraint Symbolic a => QuantifiedBool a where
quantifiedBool :: a -> SBool
quantifiedBool a
qb = SVal -> SBool
forall a. SVal -> SBV a
SBV (SVal -> SBool) -> SVal -> SBool
forall a b. (a -> b) -> a -> 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
forall {m :: * -> *}. MonadIO m => State -> m SV
f
where f :: State -> m SV
f State
st = IO SV -> m SV
forall a. IO a -> m a
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 -> a -> IO SV
forall (m :: * -> *) a.
(MonadIO m, Constraint (SymbolicT m) a) =>
State -> a -> m SV
constraint State
st a
qb
constraint :: (MonadIO m, Constraint (SymbolicT m) a) => State -> a -> m SV
constraint :: forall (m :: * -> *) a.
(MonadIO m, Constraint (SymbolicT m) a) =>
State -> a -> m SV
constraint State
st = m (m SV) -> m SV
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (m (m SV) -> m SV) -> (a -> m (m SV)) -> a -> m SV
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([String] -> (Int -> String) -> m SV) -> State -> a -> m (m SV)
forall (m :: * -> *) a b.
(MonadIO m, Constraint (SymbolicT m) a) =>
([String] -> (Int -> String) -> b) -> State -> a -> m b
constraintGen [String] -> (Int -> String) -> m SV
forall {m :: * -> *} {t} {p}.
(MonadIO m, Num t) =>
p -> (t -> String) -> m SV
mkSV State
st
where mkSV :: p -> (t -> String) -> m SV
mkSV p
_deps t -> String
d = IO SV -> m SV
forall a. IO a -> m a
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 -> Kind -> SBVExpr -> IO SV
newExpr State
st Kind
KBool (Op -> [SV] -> SBVExpr
SBVApp (String -> Op
QuantifiedBool (t -> String
d t
0)) [])
constraintStr :: (MonadIO m, Constraint (SymbolicT m) a) => State -> a -> m String
constraintStr :: forall (m :: * -> *) a.
(MonadIO m, Constraint (SymbolicT m) a) =>
State -> a -> m String
constraintStr = ([String] -> (Int -> String) -> String) -> State -> a -> m String
forall (m :: * -> *) a b.
(MonadIO m, Constraint (SymbolicT m) a) =>
([String] -> (Int -> String) -> b) -> State -> a -> m b
constraintGen [String] -> (Int -> String) -> String
forall {t}. Num t => [String] -> (t -> String) -> String
toStr
where toStr :: [String] -> (t -> String) -> String
toStr [String]
deps t -> String
body = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [ String
"; user defined axiom: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
depInfo [String]
deps
, String
"(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ t -> String
body t
2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
]
depInfo :: [String] -> String
depInfo [] = String
""
depInfo [String]
ds = String
"[Refers to: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
ds String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"
convert :: MonadIO m => State -> Kind -> SymbolicT m () -> m Defn
convert :: forall (m :: * -> *).
MonadIO m =>
State -> Kind -> SymbolicT m () -> m Defn
convert State
st Kind
expectedKind SymbolicT m ()
comp = do
((), Result
res) <- State -> SymbolicT m () -> m ((), Result)
forall (m :: * -> *) a.
MonadIO m =>
State -> SymbolicT m a -> m (a, Result)
runSymbolicInState State
st SymbolicT m ()
comp
ProgInfo
curProgInfo <- IO ProgInfo -> m ProgInfo
forall a. IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO ProgInfo -> m ProgInfo) -> IO ProgInfo -> m ProgInfo
forall a b. (a -> b) -> a -> b
$ IORef ProgInfo -> IO ProgInfo
forall a. IORef a -> IO a
readIORef (State -> IORef ProgInfo
rProgInfo State
st)
Defn -> m Defn
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Defn -> m Defn) -> Defn -> m Defn
forall a b. (a -> b) -> a -> b
$ ProgInfo -> SMTConfig -> Kind -> Result -> Defn
toLambda ProgInfo
curProgInfo (State -> SMTConfig
stCfg State
st) Kind
expectedKind Result
res
toLambda :: ProgInfo -> SMTConfig -> Kind -> Result -> Defn
toLambda :: ProgInfo -> SMTConfig -> Kind -> Result -> Defn
toLambda ProgInfo
curProgInfo SMTConfig
cfg Kind
expectedKind result :: Result
result@Result{resAsgns :: Result -> SBVPgm
resAsgns = SBVPgm Seq (SV, SBVExpr)
asgnsSeq} = Result -> Defn
sh Result
result
where tbd :: [String] -> a
tbd [String]
xs = 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
"*** Data.SBV.lambda: Unsupported construct." String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"*** " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String
"" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
xs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"", String
report])
bad :: [String] -> a
bad [String]
xs = 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
"*** Data.SBV.lambda: Impossible happened." String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"*** " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String
"" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
xs [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"", String
bugReport])
report :: String
report = String
"Please request this as a feature at https://github.com/LeventErkok/sbv/issues"
bugReport :: String
bugReport = String
"Please report this at https://github.com/LeventErkok/sbv/issues"
sh :: Result -> Defn
sh (Result ProgInfo
_hasQuants
KindSet
_ki
[(String, CV)]
_qcInfo
[(String, CV -> Bool, SV)]
observables
[(String, [String])]
_codeSegs
ResultInp
is
( CnstMap
_allConsts
, [(SV, CV)]
consts
)
[((Int, Kind, Kind), [SV])]
tbls
[(Int, ArrayInfo)]
_arrs
[(String, (Bool, Maybe [String], SBVType))]
_uis
[(SMTDef, SBVType)]
_axs
SBVPgm
pgm
Seq (Bool, [(String, String)], SV)
cstrs
[(String, Maybe CallStack, SV)]
assertions
[SV]
outputs
)
| Bool -> Bool
not (Seq (Bool, [(String, String)], SV) -> Bool
forall a. Seq a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Seq (Bool, [(String, String)], SV)
cstrs)
= [String] -> Defn
forall {a}. [String] -> a
tbd [ String
"Constraints."
, String
" Saw: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Seq (Bool, [(String, String)], SV) -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq (Bool, [(String, String)], SV)
cstrs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" additional constraint(s)."
]
| Bool -> Bool
not ([(String, Maybe CallStack, SV)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, Maybe CallStack, SV)]
assertions)
= [String] -> Defn
forall {a}. [String] -> a
tbd [ String
"Assertions."
, String
" Saw: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String
n | (String
n, Maybe CallStack
_, SV
_) <- [(String, Maybe CallStack, SV)]
assertions]
]
| Bool -> Bool
not ([(String, CV -> Bool, SV)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, CV -> Bool, SV)]
observables)
= [String] -> Defn
forall {a}. [String] -> a
tbd [ String
"Observables."
, String
" Saw: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String
n | (String
n, CV -> Bool
_, SV
_) <- [(String, CV -> Bool, SV)]
observables]
]
| SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
out Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
/= Kind
expectedKind
= [String] -> Defn
forall {a}. [String] -> a
bad [ String
"Expected kind and final kind do not match"
, String
" Saw : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show (SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
out)
, String
" Expected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
expectedKind
]
| Bool
True
= Defn
res
where res :: Defn
res = [String] -> Maybe [(Quantifier, String)] -> (Int -> String) -> Defn
Defn ([String] -> [String]
forall a. Eq a => [a] -> [a]
nub [String
nm | Uninterpreted String
nm <- Seq (SV, SBVExpr) -> [Op]
forall from to. Biplate from to => from -> [to]
G.universeBi Seq (SV, SBVExpr)
asgnsSeq])
Maybe [(Quantifier, String)]
mbParam
(String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> (Int -> [String]) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [String]
body)
params :: [(Quantifier, SV)]
params = case ResultInp
is of
ResultTopInps ([NamedSymVar], [NamedSymVar])
as -> [String] -> [(Quantifier, SV)]
forall {a}. [String] -> a
bad [ String
"Top inputs"
, String
" Saw: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([NamedSymVar], [NamedSymVar]) -> String
forall a. Show a => a -> String
show ([NamedSymVar], [NamedSymVar])
as
]
ResultLamInps [(Quantifier, NamedSymVar)]
xs -> ((Quantifier, NamedSymVar) -> (Quantifier, SV))
-> [(Quantifier, NamedSymVar)] -> [(Quantifier, SV)]
forall a b. (a -> b) -> [a] -> [b]
map (\(Quantifier
q, NamedSymVar
v) -> (Quantifier
q, NamedSymVar -> SV
getSV NamedSymVar
v)) [(Quantifier, NamedSymVar)]
xs
mbParam :: Maybe [(Quantifier, String)]
mbParam
| [(Quantifier, SV)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Quantifier, SV)]
params = Maybe [(Quantifier, String)]
forall a. Maybe a
Nothing
| Bool
True = [(Quantifier, String)] -> Maybe [(Quantifier, String)]
forall a. a -> Maybe a
Just [(Quantifier
q, [SV] -> String
forall {a}. (Show a, HasKind a) => [a] -> String
paramList (((Quantifier, SV) -> SV) -> [(Quantifier, SV)] -> [SV]
forall a b. (a -> b) -> [a] -> [b]
map (Quantifier, SV) -> SV
forall a b. (a, b) -> b
snd [(Quantifier, SV)]
l)) | l :: [(Quantifier, SV)]
l@((Quantifier
q, SV
_) : [(Quantifier, SV)]
_) <- [[(Quantifier, SV)]]
pGroups]
where pGroups :: [[(Quantifier, SV)]]
pGroups = ((Quantifier, SV) -> (Quantifier, SV) -> Bool)
-> [(Quantifier, SV)] -> [[(Quantifier, SV)]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\(Quantifier
q1, SV
_) (Quantifier
q2, SV
_) -> Quantifier
q1 Quantifier -> Quantifier -> Bool
forall a. Eq a => a -> a -> Bool
== Quantifier
q2) [(Quantifier, SV)]
params
paramList :: [a] -> String
paramList [a]
ps = Char
'(' Char -> String -> String
forall a. a -> [a] -> [a]
: [String] -> String
unwords ((a -> String) -> [a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\a
p -> Char
'(' Char -> String -> String
forall a. a -> [a] -> [a]
: a -> String
forall a. Show a => a -> String
show a
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType (a -> Kind
forall a. HasKind a => a -> Kind
kindOf a
p) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")") [a]
ps) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
body :: Int -> [String]
body Int
tabAmnt
| [(((Int, Kind, Kind), [SV]), [String])] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(((Int, Kind, Kind), [SV]), [String])]
constTables
, [((Int, Int), (((Int, Kind, Kind), [SV]), [String]))] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((Int, Int), (((Int, Kind, Kind), [SV]), [String]))]
nonConstTables
, Just String
e <- [(SV, String)] -> SV -> Maybe String
simpleBody ([(SV, String)]
constBindings [(SV, String)] -> [(SV, String)] -> [(SV, String)]
forall a. [a] -> [a] -> [a]
++ [(SV, String)]
svBindings) SV
out
= [String
tab String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
e]
| Bool
True
= (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
tab String -> String -> String
forall a. [a] -> [a] -> [a]
++) ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [(SV, String) -> String
forall {a}. Show a => (a, String) -> String
mkLet (SV, String)
sv | (SV, String)
sv <- [(SV, String)]
constBindings]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [(((Int, Kind, Kind), [SV]), [String]) -> String
forall {a} {b}. Show a => (((a, Kind, Kind), [SV]), b) -> String
mkTable (((Int, Kind, Kind), [SV]), [String])
t | (((Int, Kind, Kind), [SV]), [String])
t <- [(((Int, Kind, Kind), [SV]), [String])]
constTables]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [(SV, String)]
-> [((Int, Int), (((Int, Kind, Kind), [SV]), [String]))]
-> [String]
forall {a} {b}.
(Show a, Show b) =>
[(SV, String)]
-> [((Int, Int), (((a, Kind, Kind), [SV]), b))] -> [String]
walk [(SV, String)]
svBindings [((Int, Int), (((Int, Kind, Kind), [SV]), [String]))]
nonConstTables
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [SV -> String
forall a. Show a => a -> String
show SV
out String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
totalClose Char
')']
where tab :: String
tab = Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
tabAmnt Char
' '
mkBind :: String -> String -> String
mkBind String
l String
r = String
"(let ((" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
mkLet :: (a, String) -> String
mkLet (a
s, String
v) = String -> String -> String
mkBind (a -> String
forall a. Show a => a -> String
show a
s) String
v
mkTable :: (((a, Kind, Kind), [SV]), b) -> String
mkTable (((a
i, Kind
ak, Kind
rk), [SV]
elts), b
_) = String -> String -> String
mkBind String
nm (String -> Kind -> Kind -> [SV] -> String
lambdaTable ((Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map (Char -> Char -> Char
forall a b. a -> b -> a
const Char
' ') String
nm) Kind
ak Kind
rk [SV]
elts)
where nm :: String
nm = String
"table" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i
totalClose :: Int
totalClose = [(SV, String)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(SV, String)]
constBindings
Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [(SV, String)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(SV, String)]
svBindings
Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [(((Int, Kind, Kind), [SV]), [String])] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(((Int, Kind, Kind), [SV]), [String])]
constTables
Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [((Int, Int), (((Int, Kind, Kind), [SV]), [String]))] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [((Int, Int), (((Int, Kind, Kind), [SV]), [String]))]
nonConstTables
walk :: [(SV, String)]
-> [((Int, Int), (((a, Kind, Kind), [SV]), b))] -> [String]
walk [] [] = []
walk [] [((Int, Int), (((a, Kind, Kind), [SV]), b))]
remaining = String -> [String]
forall a. HasCallStack => String -> a
error (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: Impossible: Ran out of bindings, but tables remain: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [((Int, Int), (((a, Kind, Kind), [SV]), b))] -> String
forall a. Show a => a -> String
show [((Int, Int), (((a, Kind, Kind), [SV]), b))]
remaining
walk (cur :: (SV, String)
cur@(SV Kind
_ NodeId
nd, String
_) : [(SV, String)]
rest) [((Int, Int), (((a, Kind, Kind), [SV]), b))]
remaining = (((Int, Int), (((a, Kind, Kind), [SV]), b)) -> String)
-> [((Int, Int), (((a, Kind, Kind), [SV]), b))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((((a, Kind, Kind), [SV]), b) -> String
forall {a} {b}. Show a => (((a, Kind, Kind), [SV]), b) -> String
mkTable ((((a, Kind, Kind), [SV]), b) -> String)
-> (((Int, Int), (((a, Kind, Kind), [SV]), b))
-> (((a, Kind, Kind), [SV]), b))
-> ((Int, Int), (((a, Kind, Kind), [SV]), b))
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Int, Int), (((a, Kind, Kind), [SV]), b))
-> (((a, Kind, Kind), [SV]), b)
forall a b. (a, b) -> b
snd) [((Int, Int), (((a, Kind, Kind), [SV]), b))]
ready
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [(SV, String) -> String
forall {a}. Show a => (a, String) -> String
mkLet (SV, String)
cur]
[String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [(SV, String)]
-> [((Int, Int), (((a, Kind, Kind), [SV]), b))] -> [String]
walk [(SV, String)]
rest [((Int, Int), (((a, Kind, Kind), [SV]), b))]
notReady
where ([((Int, Int), (((a, Kind, Kind), [SV]), b))]
ready, [((Int, Int), (((a, Kind, Kind), [SV]), b))]
notReady) = (((Int, Int), (((a, Kind, Kind), [SV]), b)) -> Bool)
-> [((Int, Int), (((a, Kind, Kind), [SV]), b))]
-> ([((Int, Int), (((a, Kind, Kind), [SV]), b))],
[((Int, Int), (((a, Kind, Kind), [SV]), b))])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\((Int, Int)
need, (((a, Kind, Kind), [SV]), b)
_) -> (Int, Int)
need (Int, Int) -> (Int, Int) -> Bool
forall a. Ord a => a -> a -> Bool
< NodeId -> (Int, Int)
getLLI NodeId
nd) [((Int, Int), (((a, Kind, Kind), [SV]), b))]
remaining
getLLI :: NodeId -> (Int, Int)
getLLI :: NodeId -> (Int, Int)
getLLI (NodeId (SBVContext
_, Int
l, Int
i)) = (Int
l, Int
i)
simpleBody :: [(SV, String)] -> SV -> Maybe String
simpleBody :: [(SV, String)] -> SV -> Maybe String
simpleBody [(SV
v, String
e)] SV
o | SV
v SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
o = String -> Maybe String
forall a. a -> Maybe a
Just String
e
simpleBody [(SV, String)]
_ SV
_ = Maybe String
forall a. Maybe a
Nothing
assignments :: [(SV, SBVExpr)]
assignments = Seq (SV, SBVExpr) -> [(SV, SBVExpr)]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList (SBVPgm -> Seq (SV, SBVExpr)
pgmAssignments SBVPgm
pgm)
constants :: [(SV, CV)]
constants = ((SV, CV) -> Bool) -> [(SV, CV)] -> [(SV, CV)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((SV -> [SV] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [SV
falseSV, SV
trueSV]) (SV -> Bool) -> ((SV, CV) -> SV) -> (SV, CV) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SV, CV) -> SV
forall a b. (a, b) -> a
fst) [(SV, CV)]
consts
constBindings, svBindings :: [(SV, String)]
constBindings :: [(SV, String)]
constBindings = ((SV, CV) -> (SV, String)) -> [(SV, CV)] -> [(SV, String)]
forall a b. (a -> b) -> [a] -> [b]
map (SV, CV) -> (SV, String)
mkConst [(SV, CV)]
constants
svBindings :: [(SV, String)]
svBindings = ((SV, SBVExpr) -> (SV, String))
-> [(SV, SBVExpr)] -> [(SV, String)]
forall a b. (a -> b) -> [a] -> [b]
map (SV, SBVExpr) -> (SV, String)
forall {a}. (a, SBVExpr) -> (a, String)
mkAsgn [(SV, SBVExpr)]
assignments
mkConst :: (SV, CV) -> (SV, String)
mkConst :: (SV, CV) -> (SV, String)
mkConst (SV
sv, CV
cv) = (SV
sv, RoundingMode -> CV -> String
cvToSMTLib (SMTConfig -> RoundingMode
roundingMode SMTConfig
cfg) CV
cv)
out :: SV
out :: SV
out = case [SV]
outputs of
[SV
o] -> SV
o
[SV]
_ -> [String] -> SV
forall {a}. [String] -> a
bad [ String
"Unexpected non-singular output"
, String
" Saw: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SV] -> String
forall a. Show a => a -> String
show [SV]
outputs
]
rm :: RoundingMode
rm = SMTConfig -> RoundingMode
roundingMode SMTConfig
cfg
(IntMap String
tableMap, [(((Int, Kind, Kind), [SV]), [String])]
constTables, [(((Int, Kind, Kind), [SV]), [String])]
nonConstTablesUnindexed) = RoundingMode
-> [(SV, CV)]
-> [((Int, Kind, Kind), [SV])]
-> (IntMap String, [(((Int, Kind, Kind), [SV]), [String])],
[(((Int, Kind, Kind), [SV]), [String])])
constructTables RoundingMode
rm [(SV, CV)]
consts [((Int, Kind, Kind), [SV])]
tbls
nonConstTables :: [((Int, Int), (((Int, Kind, Kind), [SV]), [String]))]
nonConstTables = [ ([(Int, Int)] -> (Int, Int)
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ((Int
0, Int
0) (Int, Int) -> [(Int, Int)] -> [(Int, Int)]
forall a. a -> [a] -> [a]
: [NodeId -> (Int, Int)
getLLI NodeId
n | SV Kind
_ NodeId
n <- [SV]
elts]), (((Int, Kind, Kind), [SV]), [String])
nct)
| nct :: (((Int, Kind, Kind), [SV]), [String])
nct@(((Int, Kind, Kind)
_, [SV]
elts), [String]
_) <- [(((Int, Kind, Kind), [SV]), [String])]
nonConstTablesUnindexed]
lambdaTable :: String -> Kind -> Kind -> [SV] -> String
lambdaTable :: String -> Kind -> Kind -> [SV] -> String
lambdaTable String
extraSpace Kind
ak Kind
rk [SV]
elts = String
"(lambda ((" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
lv String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
ak String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
space String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> [SV] -> String
forall {a}. Show a => Integer -> [a] -> String
chain Integer
0 [SV]
elts String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
where cnst :: Kind -> Integer -> String
cnst Kind
k Integer
i = RoundingMode -> CV -> String
cvtCV RoundingMode
rm (Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
k (Integer
i::Integer))
lv :: String
lv = String
"idx"
long :: Bool
long = Bool -> Bool
not ([SV] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Int -> [SV] -> [SV]
forall a. Int -> [a] -> [a]
drop Int
5 [SV]
elts))
space :: String
space
| Bool
long
= String
"\n " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
extraSpace
| Bool
True
= String
" "
chain :: Integer -> [a] -> String
chain Integer
_ [] = Kind -> Integer -> String
cnst Kind
rk Integer
0
chain Integer
_ [a
x] = a -> String
forall a. Show a => a -> String
show a
x
chain Integer
i (a
x:[a]
xs) = String
"(ite (= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
lv String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> Integer -> String
cnst Kind
ak Integer
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
space
String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> [a] -> String
chain (Integer
iInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+Integer
1) [a]
xs
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
mkAsgn :: (a, SBVExpr) -> (a, String)
mkAsgn (a
sv, SBVExpr
e) = (a
sv, SBVExpr -> String
converter SBVExpr
e)
converter :: SBVExpr -> String
converter = ProgInfo
-> SolverCapabilities
-> RoundingMode
-> IntMap String
-> FunctionMap
-> SBVExpr
-> String
cvtExp ProgInfo
curProgInfo SolverCapabilities
solverCaps RoundingMode
rm IntMap String
tableMap FunctionMap
forall {k} {a}. Map k a
funcMap
where solverCaps :: SolverCapabilities
solverCaps = SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)
funcMap :: Map k a
funcMap = Map k a
forall {k} {a}. Map k a
M.empty