-----------------------------------------------------------------------------
-- |
-- Module    : Data.SBV.SMT.SMTLib2
-- Copyright : (c) Levent Erkok
-- License   : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Conversion of symbolic programs to SMTLib format, Using v2 of the standard
-----------------------------------------------------------------------------

{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE PatternGuards       #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns        #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.SMT.SMTLib2(cvt, cvtExp, cvtCV, cvtInc, declUserFuns, constructTables, setSMTOption) where

import Crypto.Hash.SHA512 (hash)
import qualified Data.ByteString.Base16 as B
import qualified Data.ByteString.Char8  as BC

import Data.List  (intercalate, partition, nub, elemIndex)
import Data.Maybe (listToMaybe, catMaybes)

import qualified Data.Foldable as F (toList)
import qualified Data.Map.Strict      as M
import qualified Data.IntMap.Strict   as IM
import           Data.Set             (Set)
import qualified Data.Set             as Set

import Data.SBV.Core.Data
import Data.SBV.Core.Kind (smtType, needsFlattening, expandKinds)
import Data.SBV.SMT.Utils
import Data.SBV.Control.Types

import Data.SBV.Core.Symbolic ( QueryContext(..), SetOp(..), getUserName', getSV, regExpToSMTString, NROp(..)
                              , SMTDef(..), ResultInp(..), ProgInfo(..), SpecialRelOp(..), SMTLambda(..)
                              )

import Data.SBV.Utils.PrettyNum (smtRoundingMode, cvToSMTLib)

import qualified Data.Generics.Uniplate.Data as G

import qualified Data.Graph as DG

-- | For higher-order functions, we firstify them. This requires a uniqu name creation. Here,
-- we create a firstified name based on the operation. The suffix appended will have at most uniqLen length.
firstify :: Int -> Op -> String
firstify :: Int -> Op -> String
firstify Int
uniqLen Op
o = Op -> String
prefix Op
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
forall a. Int -> [a] -> [a]
take Int
uniqLen (ByteString -> String
BC.unpack (ByteString -> ByteString
B.encode (ByteString -> ByteString
hash (String -> ByteString
BC.pack (String -> String
compress (Op -> String
forall a. Show a => a -> String
show Op
o))))))
  where prefix :: Op -> String
prefix (SeqOp SBVReverse   {}) = String
"sbv.reverse"
        prefix (SeqOp SBVZip       {}) = String
"sbv.zip"
        prefix (SeqOp SBVZipWith   {}) = String
"sbv.zipWith"
        prefix (SeqOp SBVPartition {}) = String
"sbv.partition"
        prefix (SeqOp SBVMap       {}) = String
"sbv.map"
        prefix (SeqOp SBVFoldl     {}) = String
"sbv.foldl"
        prefix (SeqOp SBVFoldr     {}) = String
"sbv.foldr"
        prefix (SeqOp SBVFilter    {}) = String
"sbv.filter"
        prefix (SeqOp SBVAll       {}) = String
"sbv.all"
        prefix (SeqOp SBVAny       {}) = String
"sbv.any"
        prefix (SeqOp SBVConcat    {}) = String
"sbv.concat"
        prefix Op
_                       = 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.firstify: Didn't expect firstification to be called."
                                                         , String
"***"
                                                         , String
"***   Operator: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
forall a. Show a => a -> String
show Op
o
                                                         , String
"***"
                                                         , String
"*** Please report this as a bug."
                                                         ]

        -- compress and make spaces uniform; get words, and then unwords
        compress :: String -> String
compress = [String] -> String
unwords ([String] -> String) -> (String -> [String]) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> [String]
words

-- | Translate a problem into an SMTLib2 script
cvt :: SMTLibConverter ([String], [String])
cvt :: SMTLibConverter ([String], [String])
cvt QueryContext
ctx ProgInfo
curProgInfo Set Kind
kindInfo Bool
isSat [String]
comments ResultInp
allInputs (CnstMap
_, [(SV, CV)]
consts) [((Int, Kind, Kind), [SV])]
tbls [(String, (Bool, Maybe [String], SBVType))]
uis [(SMTDef, SBVType)]
defs (SBVPgm Seq (SV, SBVExpr)
asgnsSeq) Seq (Bool, [(String, String)], SV)
cstrs SV
out SMTConfig
cfg = ([String]
pgm, [String]
exportedDefs)
  where allKinds :: [Kind]
allKinds       = Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList Set Kind
kindInfo

        -- Below can simply be defined as: nub (sort (G.universeBi asgnsSeq))
        -- Alas, it turns out this is really expensive when we have nested lambdas, so we do an explicit walk
        allTopOps :: [Op]
allTopOps = Set Op -> [Op]
forall a. Set a -> [a]
Set.toList (Set Op -> [Op]) -> Set Op -> [Op]
forall a b. (a -> b) -> a -> b
$ (Set Op -> (SV, SBVExpr) -> Set Op)
-> Set Op -> Seq (SV, SBVExpr) -> Set Op
forall b a. (b -> a -> b) -> b -> Seq a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Set Op
sofar (SV
_, SBVApp Op
o [SV]
_) -> Op -> Set Op -> Set Op
forall a. Ord a => a -> Set a -> Set a
Set.insert Op
o Set Op
sofar) Set Op
forall a. Set a
Set.empty Seq (SV, SBVExpr)
asgnsSeq

        hasInteger :: Bool
hasInteger     = Kind
KUnbounded Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
        hasArrays :: Bool
hasArrays      = Bool -> Bool
not ([()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [() | KArray{}     <- [Kind]
allKinds])
        hasNonBVArrays :: Bool
hasNonBVArrays = Bool -> Bool
not ([()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [() | KArray Kind
k1 Kind
k2 <- [Kind]
allKinds, Bool -> Bool
not (Kind -> Bool
forall a. HasKind a => a -> Bool
isBounded Kind
k1 Bool -> Bool -> Bool
&& Kind -> Bool
forall a. HasKind a => a -> Bool
isBounded Kind
k2)])
        hasReal :: Bool
hasReal        = Kind
KReal      Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
        hasFP :: Bool
hasFP          =  Bool -> Bool
not ([()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [() | KFP{} <- [Kind]
allKinds])
                       Bool -> Bool -> Bool
|| Kind
KFloat     Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
                       Bool -> Bool -> Bool
|| Kind
KDouble    Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
        hasString :: Bool
hasString      = Kind
KString     Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
        hasRegExp :: Bool
hasRegExp      = (Bool -> Bool
not (Bool -> Bool) -> ([()] -> Bool) -> [()] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [() | (RegExOp
_ :: RegExOp) <- [Op] -> [RegExOp]
forall from to. Biplate from to => from -> [to]
G.universeBi [Op]
allTopOps]
        hasChar :: Bool
hasChar        = Kind
KChar      Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
        hasRounding :: Bool
hasRounding    = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String
s | (String
s, Maybe [String]
_) <- [(String, Maybe [String])]
usorts, String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"RoundingMode"]
        hasBVs :: Bool
hasBVs         = Bool -> Bool
not ([()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [() | KBounded{} <- [Kind]
allKinds])
        usorts :: [(String, Maybe [String])]
usorts         = [(String
s, Maybe [String]
dt) | KUserSort String
s Maybe [String]
dt <- [Kind]
allKinds]
        trueUSorts :: [String]
trueUSorts     = [String
s | (String
s, Maybe [String]
_) <- [(String, Maybe [String])]
usorts, String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"RoundingMode"]
        tupleArities :: [Int]
tupleArities   = Set Kind -> [Int]
findTupleArities Set Kind
kindInfo
        hasOverflows :: Bool
hasOverflows   = (Bool -> Bool
not (Bool -> Bool) -> ([()] -> Bool) -> [()] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [() | (OvOp
_ :: OvOp) <- [Op] -> [OvOp]
forall from to. Biplate from to => from -> [to]
G.universeBi [Op]
allTopOps]
        hasQuantBools :: Bool
hasQuantBools  = (Bool -> Bool
not (Bool -> Bool) -> ([()] -> Bool) -> [()] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [() | QuantifiedBool{} <- [Op] -> [Op]
forall from to. Biplate from to => from -> [to]
G.universeBi [Op]
allTopOps]
        hasList :: Bool
hasList        = (Kind -> Bool) -> Set Kind -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
forall a. HasKind a => a -> Bool
isList Set Kind
kindInfo
        hasSets :: Bool
hasSets        = (Kind -> Bool) -> Set Kind -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
forall a. HasKind a => a -> Bool
isSet Set Kind
kindInfo
        hasTuples :: Bool
hasTuples      = Bool -> Bool
not (Bool -> Bool) -> ([Int] -> Bool) -> [Int] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Int] -> Bool) -> [Int] -> Bool
forall a b. (a -> b) -> a -> b
$ [Int]
tupleArities
        hasEither :: Bool
hasEither      = (Kind -> Bool) -> Set Kind -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
forall a. HasKind a => a -> Bool
isEither Set Kind
kindInfo
        hasMaybe :: Bool
hasMaybe       = (Kind -> Bool) -> Set Kind -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
forall a. HasKind a => a -> Bool
isMaybe  Set Kind
kindInfo
        hasRational :: Bool
hasRational    = (Kind -> Bool) -> Set Kind -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
forall a. HasKind a => a -> Bool
isRational Set Kind
kindInfo
        rm :: RoundingMode
rm             = SMTConfig -> RoundingMode
roundingMode SMTConfig
cfg
        solverCaps :: SolverCapabilities
solverCaps     = SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)
        hasLambdas :: Bool
hasLambdas     = let needsLambda :: SeqOp -> Bool
needsLambda SBVZipWith{}   = Bool
True
                             needsLambda SBVPartition{} = Bool
True
                             needsLambda SBVMap{}       = Bool
True
                             needsLambda SBVFoldl{}     = Bool
True
                             needsLambda SBVFoldr{}     = Bool
True
                             needsLambda SBVFilter{}    = Bool
True
                             needsLambda SBVAll{}       = Bool
True
                             needsLambda SBVAny{}       = Bool
True
                             needsLambda SeqOp
_              = Bool
False
                         in (Bool -> Bool
not (Bool -> Bool) -> ([()] -> Bool) -> [()] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [() | SeqOp
o :: SeqOp <- [Op] -> [SeqOp]
forall from to. Biplate from to => from -> [to]
G.universeBi [Op]
allTopOps, SeqOp -> Bool
needsLambda SeqOp
o]

        (Bool
needsQuantifiers, Bool
needsSpecialRels, [Op]
specialFuncs) = case ProgInfo
curProgInfo of
           ProgInfo Bool
hasQ [SpecialRelOp]
srs [(String, String)]
tcs [Op]
sf -> (Bool
hasQ, Bool -> Bool
not ([SpecialRelOp] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SpecialRelOp]
srs Bool -> Bool -> Bool
&& [(String, String)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, String)]
tcs), [Op]
sf)

        -- Is there a reason why we can't handle this problem?
        -- NB. There's probably a lot more checking we can do here, but this is a start:
        doesntHandle :: Maybe [String]
doesntHandle = [[String]] -> Maybe [String]
forall a. [a] -> Maybe a
listToMaybe [String -> [String]
nope String
w | (String
w, SolverCapabilities -> Bool
have, Bool
need) <- [(String, SolverCapabilities -> Bool, Bool)]
checks, Bool
need Bool -> Bool -> Bool
&& Bool -> Bool
not (SolverCapabilities -> Bool
have SolverCapabilities
solverCaps)]
           where checks :: [(String, SolverCapabilities -> Bool, Bool)]
checks = [ (String
"data types",             SolverCapabilities -> Bool
supportsDataTypes,          Bool
hasTuples Bool -> Bool -> Bool
|| Bool
hasEither Bool -> Bool -> Bool
|| Bool
hasMaybe)
                          , (String
"needs lambdas",          SolverCapabilities -> Bool
supportsLambdas,            Bool
hasLambdas)
                          , (String
"set operations",         SolverCapabilities -> Bool
supportsSets,               Bool
hasSets)
                          , (String
"bit vectors",            SolverCapabilities -> Bool
supportsBitVectors,         Bool
hasBVs)
                          , (String
"special relations",      SolverCapabilities -> Bool
supportsSpecialRels,        Bool
needsSpecialRels)
                          , (String
"needs quantifiers",      SolverCapabilities -> Bool
supportsQuantifiers,        Bool
needsQuantifiers)
                          , (String
"unbounded integers",     SolverCapabilities -> Bool
supportsUnboundedInts,      Bool
hasInteger)
                          , (String
"algebraic reals",        SolverCapabilities -> Bool
supportsReals,              Bool
hasReal)
                          , (String
"floating-point numbers", SolverCapabilities -> Bool
supportsIEEE754,            Bool
hasFP)
                          , (String
"uninterpreted sorts",    SolverCapabilities -> Bool
supportsUninterpretedSorts, Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
trueUSorts))
                          ]

                 nope :: String -> [String]
nope String
w = [ String
"***     Given problem requires support for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w
                          , 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 (SMTConfig -> SMTSolver
solver SMTConfig
cfg)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") doesn't support this feature."
                          ]

        -- Some cases require all, some require none. Sigh.. Also, if there're lambdas CVC5 needs HO_ALL
        setAll :: String -> [String]
setAll String
reason = [String
"(set-logic " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
allName String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") ; "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
reason String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
", using catch-all."]
          where allName :: String
allName | Bool
hasLambdas Bool -> Bool -> Bool
&& Bool
isCVC5 = String
"HO_ALL"
                        | Bool
True                 = String
"ALL"

                isCVC5 :: Bool
isCVC5 = case SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
cfg) of
                           Solver
CVC5 -> Bool
True
                           Solver
_    -> Bool
False

        -- Determining the logic is surprisingly tricky!
        logic :: [String]
logic
           -- user told us what to do: so just take it:
           | Just Logic
l <- case [Logic
l | SetLogic Logic
l <- SMTConfig -> [SMTOption]
solverSetOptions SMTConfig
cfg] of
                         []  -> Maybe Logic
forall a. Maybe a
Nothing
                         [Logic
l] -> Logic -> Maybe Logic
forall a. a -> Maybe a
Just Logic
l
                         [Logic]
ls  -> String -> Maybe Logic
forall a. HasCallStack => String -> a
error (String -> Maybe Logic) -> String -> Maybe Logic
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                , String
"*** Only one setOption call to 'setLogic' is allowed, found: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Logic] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Logic]
ls)
                                                , String
"***  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Logic -> String) -> [Logic] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Logic -> String
forall a. Show a => a -> String
show [Logic]
ls)
                                                ]
           = case Logic
l of
               Logic
Logic_NONE -> [String
"; NB. Not setting the logic per user request of Logic_NONE"]
               Logic
_          -> [String
"(set-logic " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Logic -> String
forall a. Show a => a -> String
show Logic
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") ; NB. User specified."]

           -- There's a reason why we can't handle this problem:
           | Just [String]
cantDo <- Maybe [String]
doesntHandle
           = String -> [String]
forall a. HasCallStack => String -> a
error (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$   [ String
""
                                 , String
"*** SBV is unable to choose a proper solver configuration:"
                                 , String
"***"
                                 ]
                             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
cantDo
                             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"***"
                                , String
"*** Please report this as a feature request, either for SBV or the backend solver."
                                ]

           -- Otherwise, we try to determine the most suitable logic.
           -- NB. This isn't really fool proof!

           -- we never set QF_S (ALL seems to work better in all cases)

           | Bool
needsSpecialRels      = [String
"; has special relations, no logic set."]

           -- Things that require ALL
           | Bool
hasLambdas            = String -> [String]
setAll String
"has lambda expressions"
           | Bool
hasInteger            = String -> [String]
setAll String
"has unbounded values"
           | Bool
hasRational           = String -> [String]
setAll String
"has rational values"
           | Bool
hasReal               = String -> [String]
setAll String
"has algebraic reals"
           | Bool -> Bool
not ([String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
trueUSorts) = String -> [String]
setAll String
"has user-defined sorts"
           | Bool
hasNonBVArrays        = String -> [String]
setAll String
"has non-bitvector arrays"
           | Bool
hasTuples             = String -> [String]
setAll String
"has tuples"
           | Bool
hasEither             = String -> [String]
setAll String
"has either type"
           | Bool
hasMaybe              = String -> [String]
setAll String
"has maybe type"
           | Bool
hasSets               = String -> [String]
setAll String
"has sets"
           | Bool
hasList               = String -> [String]
setAll String
"has lists"
           | Bool
hasChar               = String -> [String]
setAll String
"has chars"
           | Bool
hasString             = String -> [String]
setAll String
"has strings"
           | Bool
hasRegExp             = String -> [String]
setAll String
"has regular expressions"
           | Bool
hasOverflows          = String -> [String]
setAll String
"has overflow checks"
           | Bool
hasQuantBools         = String -> [String]
setAll String
"has quantified booleans"

           | Bool
hasFP Bool -> Bool -> Bool
|| Bool
hasRounding
           = if Bool
needsQuantifiers
             then [String
"(set-logic ALL)"]
             else if Bool
hasBVs
                  then [String
"(set-logic QF_FPBV)"]
                  else [String
"(set-logic QF_FP)"]

           -- If we're in a user query context, we'll pick ALL, otherwise
           -- we'll stick to some bit-vector logic based on what we see in the problem.
           -- This is controversial, but seems to work well in practice.
           | Bool
True
           = case QueryContext
ctx of
               QueryContext
QueryExternal -> [String
"(set-logic ALL) ; external query, using all logics."]
               QueryContext
QueryInternal -> if SolverCapabilities -> Bool
supportsBitVectors SolverCapabilities
solverCaps
                                then [String
"(set-logic " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
qs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
as String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ufs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"BV)"]
                                else [String
"(set-logic ALL)"] -- fall-thru
          where qs :: String
qs  | Bool -> Bool
not Bool
needsQuantifiers  = String
"QF_"
                    | Bool
True                  = String
""
                as :: String
as  | Bool -> Bool
not Bool
hasArrays         = String
""
                    | Bool
True                  = String
"A"
                ufs :: String
ufs | [(String, (Bool, Maybe [String], SBVType))] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, (Bool, Maybe [String], SBVType))]
uis Bool -> Bool -> Bool
&& [((Int, Kind, Kind), [SV])] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((Int, Kind, Kind), [SV])]
tbls = String
""     -- we represent tables as UFs
                    | Bool
True                  = String
"UF"

        -- SBV always requires the production of models!
        getModels :: [String]
getModels   = String
"(set-option :produce-models true)"
                    String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]
flattenConfig | (Kind -> Bool) -> Set Kind -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
needsFlattening Set Kind
kindInfo, Just [String]
flattenConfig <- [SolverCapabilities -> Maybe [String]
supportsFlattenedModels SolverCapabilities
solverCaps]]

        -- process all other settings we're given. If an option cannot be repeated, we only take the last one.
        userSettings :: [String]
userSettings = (SMTOption -> String) -> [SMTOption] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (SMTConfig -> SMTOption -> String
setSMTOption SMTConfig
cfg) ([SMTOption] -> [String]) -> [SMTOption] -> [String]
forall a b. (a -> b) -> a -> b
$ (SMTOption -> Bool) -> [SMTOption] -> [SMTOption]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (SMTOption -> Bool) -> SMTOption -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTOption -> Bool
isLogic) ([SMTOption] -> [SMTOption]) -> [SMTOption] -> [SMTOption]
forall a b. (a -> b) -> a -> b
$ (SMTOption -> [SMTOption] -> [SMTOption])
-> [SMTOption] -> [SMTOption] -> [SMTOption]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SMTOption -> [SMTOption] -> [SMTOption]
comb [] ([SMTOption] -> [SMTOption]) -> [SMTOption] -> [SMTOption]
forall a b. (a -> b) -> a -> b
$ SMTConfig -> [SMTOption]
solverSetOptions SMTConfig
cfg
           where -- Logic is already processed, so drop it:
                 isLogic :: SMTOption -> Bool
isLogic SetLogic{} = Bool
True
                 isLogic SMTOption
_          = Bool
False

                 -- SBV sets diagnostic-output channel on some solvers. If the user also gives it, let's just
                 -- take it by only taking the last one
                 isDiagOutput :: SMTOption -> Bool
isDiagOutput DiagnosticOutputChannel{} = Bool
True
                 isDiagOutput SMTOption
_                         = Bool
False

                 comb :: SMTOption -> [SMTOption] -> [SMTOption]
comb SMTOption
o [SMTOption]
rest
                   | SMTOption -> Bool
isDiagOutput SMTOption
o Bool -> Bool -> Bool
&& (SMTOption -> Bool) -> [SMTOption] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SMTOption -> Bool
isDiagOutput [SMTOption]
rest =     [SMTOption]
rest
                   | Bool
True                                    = SMTOption
o SMTOption -> [SMTOption] -> [SMTOption]
forall a. a -> [a] -> [a]
: [SMTOption]
rest

        settings :: [String]
settings =  [String]
userSettings        -- NB. Make sure this comes first!
                 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
getModels
                 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
logic

        ([NamedSymVar]
inputs, [NamedSymVar]
trackerVars)
            = case ResultInp
allInputs of
                ResultTopInps ([NamedSymVar], [NamedSymVar])
ists -> ([NamedSymVar], [NamedSymVar])
ists
                ResultLamInps [(Quantifier, NamedSymVar)]
ps   -> String -> ([NamedSymVar], [NamedSymVar])
forall a. HasCallStack => String -> a
error (String -> ([NamedSymVar], [NamedSymVar]))
-> String -> ([NamedSymVar], [NamedSymVar])
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                      , String
"*** Data.SBV.smtLib2: Unexpected lambda inputs in conversion"
                                                      , String
"***"
                                                      , String
"*** Saw: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(Quantifier, NamedSymVar)] -> String
forall a. Show a => a -> String
show [(Quantifier, NamedSymVar)]
ps
                                                      ]

        pgm :: [String]
pgm  =  (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"; " String -> String -> String
forall a. [a] -> [a] -> [a]
++) [String]
comments
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
settings
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- uninterpreted sorts ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((String, Maybe [String]) -> [String])
-> [(String, Maybe [String])] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String, Maybe [String]) -> [String]
declSort [(String, Maybe [String])]
usorts
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- tuples ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Int -> [String]) -> [Int] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Int -> [String]
declTuple [Int]
tupleArities
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- sums ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (if Set Kind -> Bool
containsSum       Set Kind
kindInfo then [String]
declSum       else [])
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (if Set Kind -> Bool
containsMaybe     Set Kind
kindInfo then [String]
declMaybe     else [])
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (if Set Kind -> Bool
containsRationals Set Kind
kindInfo then [String]
declRationals else [])
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- literal constants ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((SV, CV) -> [String]) -> [(SV, CV)] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SMTConfig -> (SV, CV) -> [String]
declConst SMTConfig
cfg) [(SV, CV)]
consts
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- top level inputs ---"]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [SV -> SBVType -> Maybe String -> [String]
declareFun SV
s ([Kind] -> SBVType
SBVType [SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
s]) (SV -> Maybe String
userName SV
s) | NamedSymVar
var <- [NamedSymVar]
inputs, let s :: SV
s = NamedSymVar -> SV
getSV NamedSymVar
var]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- optimization tracker variables ---" | Bool -> Bool
not ([NamedSymVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedSymVar]
trackerVars) ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [SV -> SBVType -> Maybe String -> [String]
declareFun SV
s ([Kind] -> SBVType
SBVType [SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
s]) (String -> Maybe String
forall a. a -> Maybe a
Just (String
"tracks " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
nm)) | NamedSymVar
var <- [NamedSymVar]
trackerVars, let s :: SV
s = NamedSymVar -> SV
getSV NamedSymVar
var, let nm :: String
nm = NamedSymVar -> String
getUserName' NamedSymVar
var]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- constant tables ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((((Int, Kind, Kind), [SV]), [String]) -> [String])
-> [(((Int, Kind, Kind), [SV]), [String])] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((String -> [String] -> [String]) -> (String, [String]) -> [String]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (:) ((String, [String]) -> [String])
-> ((((Int, Kind, Kind), [SV]), [String]) -> (String, [String]))
-> (((Int, Kind, Kind), [SV]), [String])
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Int, Kind, Kind), [SV]), [String]) -> (String, [String])
mkTable) [(((Int, Kind, Kind), [SV]), [String])]
constTables
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- non-constant tables ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((((Int, Kind, Kind), [SV]), [String]) -> String)
-> [(((Int, Kind, Kind), [SV]), [String])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (((Int, Kind, Kind), [SV]), [String]) -> String
nonConstTable [(((Int, Kind, Kind), [SV]), [String])]
nonConstTables
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- uninterpreted constants ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((String, (Bool, Maybe [String], SBVType)) -> [String])
-> [(String, (Bool, Maybe [String], SBVType))] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ProgInfo -> (String, (Bool, Maybe [String], SBVType)) -> [String]
declUI ProgInfo
curProgInfo) [(String, (Bool, Maybe [String], SBVType))]
uis
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- Firstified function definitions" | Bool -> Bool
not ([Op] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Op]
specialFuncs) ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
firstifiedDefs
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- Firstified equivalences"         | Bool -> Bool
not ([[String]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[String]]
exportedFirstifiedEqualities) ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
exportedFirstifiedEqualities
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; -- NB. Skipping firstified equivalences, due to generateHOEquivs setting." | Bool -> Bool
not ([[String]] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [[String]]
firstifiedEqualities Bool -> Bool -> Bool
|| Bool
generateHOEquivs)]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- user defined functions ---"]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
userDefs
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- assignments ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((SV, SBVExpr) -> [String]) -> [(SV, SBVExpr)] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ProgInfo -> SMTConfig -> TableMap -> (SV, SBVExpr) -> [String]
declDef ProgInfo
curProgInfo SMTConfig
cfg TableMap
tableMap) [(SV, SBVExpr)]
asgns
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- delayedEqualities ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\String
s -> String
"(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")") [String]
delayedEqualities
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- formula ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
finalAssert

        SMTConfig{Bool
generateHOEquivs :: Bool
generateHOEquivs :: SMTConfig -> Bool
generateHOEquivs, kdOptions :: SMTConfig -> KDOptions
kdOptions = KDOptions{Int
firstifyUniqueLen :: Int
firstifyUniqueLen :: KDOptions -> Int
firstifyUniqueLen}} = SMTConfig
cfg

        ([[String]]
firstifiedDefs, [(Op, String)]
firstifiedFuncs)
           = case [(Op, (String, [String]))] -> Maybe (Op, Op, String)
forall {c} {b} {b}. Eq c => [(b, (c, b))] -> Maybe (b, b, c)
dup [(Op, (String, [String]))]
res of
               Maybe (Op, Op, String)
Nothing         -> ([[String]
def | (Op
_, (String
_, [String]
def)) <- [(Op, (String, [String]))]
res], [(Op
op, String
nm) | (Op
op, (String
nm, [String]
_)) <- [(Op, (String, [String]))]
res])
               Just (Op
o, Op
o', String
n) -> String -> ([[String]], [(Op, String)])
forall a. HasCallStack => String -> a
error (String -> ([[String]], [(Op, String)]))
-> String -> ([[String]], [(Op, String)])
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                  , String
"*** Data.SBV: Insufficient unique length in firstification."
                                                  , String
"***"
                                                  , String
"***   Operator 1 : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
forall a. Show a => a -> String
show Op
o
                                                  , String
"***   Operator 2 : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
forall a. Show a => a -> String
show Op
o'
                                                  , String
"***   Mapped name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
n
                                                  , String
"***   Unique len : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
firstifyUniqueLen
                                                  , String
"***"
                                                  , String
"*** Such collisions should be rare, but looks like you ran into one!"
                                                  , String
"*** Try running with an increased unique-length:"
                                                  , String
"***"
                                                  , String
"***     solver{firstifyUniqueLen = N}"
                                                  , String
"***"
                                                  , String
"*** where N is larger than " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
firstifyUniqueLen
                                                  , String
"***"
                                                  , String
"*** For instance:"
                                                  , String
"***"
                                                  , String
"***     satWith z3{firstUniqueLen = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
firstifyUniqueLen Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"
                                                  , String
"***"
                                                  , String
"*** If that doesn't resolve the problem, or if you believe this is caused by some"
                                                  , String
"*** other problem, please report his as a bug."
                                                  ]
           where res :: [(Op, (String, [String]))]
res = [(Op
op, SMTConfig -> Op -> (String, [String])
declSBVFunc SMTConfig
cfg Op
op) | Op
op <- [Op] -> [Op]
forall a. [a] -> [a]
reverse [Op]
specialFuncs]
                 dup :: [(b, (c, b))] -> Maybe (b, b, c)
dup []                = Maybe (b, b, c)
forall a. Maybe a
Nothing
                 dup ((b
o, (c
n, b
_)): [(b, (c, b))]
xs) = case [b
o' | (b
o', (c
n', b
_)) <- [(b, (c, b))]
xs, c
n c -> c -> Bool
forall a. Eq a => a -> a -> Bool
== c
n'] of
                                           []       -> [(b, (c, b))] -> Maybe (b, b, c)
dup [(b, (c, b))]
xs
                                           (b
o' : [b]
_) -> (b, b, c) -> Maybe (b, b, c)
forall a. a -> Maybe a
Just (b
o, b
o', c
n)

        exportedFirstifiedEqualities :: [[String]]
exportedFirstifiedEqualities
           | Bool
generateHOEquivs
           = [[String]]
firstifiedEqualities
           | Bool
True
           = []

        firstifiedEqualities :: [[String]]
firstifiedEqualities = ((Op, (String, SMTLambda), (String, SMTLambda)) -> [String])
-> [(Op, (String, SMTLambda), (String, SMTLambda))] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map (Op, (String, SMTLambda), (String, SMTLambda)) -> [String]
equate ([(Op, (String, SMTLambda), (String, SMTLambda))] -> [[String]])
-> [(Op, (String, SMTLambda), (String, SMTLambda))] -> [[String]]
forall a b. (a -> b) -> a -> b
$ [(Op, String)] -> [(Op, (String, SMTLambda), (String, SMTLambda))]
combs [(Op, String)]
firstifiedFuncs
           where combs :: [(Op, String)] -> [(Op, (String, SMTLambda), (String, SMTLambda))]
                 combs :: [(Op, String)] -> [(Op, (String, SMTLambda), (String, SMTLambda))]
combs []             = []
                 combs ((Op
o1, String
nm1):[(Op, String)]
fs) = [(Op
o1, (String
nm1, SMTLambda
l1), (String
nm2, SMTLambda
l2)) | (Op
o2, String
nm2) <- [(Op, String)]
fs, Just (SMTLambda
l1, SMTLambda
l2) <- [Op -> Op -> Maybe (SMTLambda, SMTLambda)
getFuncs Op
o1 Op
o2]] [(Op, (String, SMTLambda), (String, SMTLambda))]
-> [(Op, (String, SMTLambda), (String, SMTLambda))]
-> [(Op, (String, SMTLambda), (String, SMTLambda))]
forall a. [a] -> [a] -> [a]
++ [(Op, String)] -> [(Op, (String, SMTLambda), (String, SMTLambda))]
combs [(Op, String)]
fs

                 -- same if the same op sans the lambda
                 getFuncs :: Op -> Op -> Maybe (SMTLambda, SMTLambda)
                 getFuncs :: Op -> Op -> Maybe (SMTLambda, SMTLambda)
getFuncs (SeqOp (SBVZipWith   Kind
a Kind
b Kind
c SMTLambda
f)) (SeqOp (SBVZipWith   Kind
x Kind
y Kind
z SMTLambda
g)) | [Kind
a, Kind
b, Kind
c] [Kind] -> [Kind] -> Bool
forall a. Eq a => a -> a -> Bool
== [Kind
x, Kind
y, Kind
z] = (SMTLambda, SMTLambda) -> Maybe (SMTLambda, SMTLambda)
forall a. a -> Maybe a
Just (SMTLambda
f, SMTLambda
g)
                 getFuncs (SeqOp (SBVPartition Kind
a     SMTLambda
f)) (SeqOp (SBVPartition Kind
x     SMTLambda
g)) | [Kind
a      ] [Kind] -> [Kind] -> Bool
forall a. Eq a => a -> a -> Bool
== [Kind
x      ] = (SMTLambda, SMTLambda) -> Maybe (SMTLambda, SMTLambda)
forall a. a -> Maybe a
Just (SMTLambda
f, SMTLambda
g)
                 getFuncs (SeqOp (SBVMap       Kind
a Kind
b   SMTLambda
f)) (SeqOp (SBVMap       Kind
x Kind
y   SMTLambda
g)) | [Kind
a, Kind
b   ] [Kind] -> [Kind] -> Bool
forall a. Eq a => a -> a -> Bool
== [Kind
x, Kind
y   ] = (SMTLambda, SMTLambda) -> Maybe (SMTLambda, SMTLambda)
forall a. a -> Maybe a
Just (SMTLambda
f, SMTLambda
g)
                 getFuncs (SeqOp (SBVFoldl     Kind
a Kind
b   SMTLambda
f)) (SeqOp (SBVFoldl     Kind
x Kind
y   SMTLambda
g)) | [Kind
a, Kind
b   ] [Kind] -> [Kind] -> Bool
forall a. Eq a => a -> a -> Bool
== [Kind
x, Kind
y   ] = (SMTLambda, SMTLambda) -> Maybe (SMTLambda, SMTLambda)
forall a. a -> Maybe a
Just (SMTLambda
f, SMTLambda
g)
                 getFuncs (SeqOp (SBVFoldr     Kind
a Kind
b   SMTLambda
f)) (SeqOp (SBVFoldr     Kind
x Kind
y   SMTLambda
g)) | [Kind
a, Kind
b   ] [Kind] -> [Kind] -> Bool
forall a. Eq a => a -> a -> Bool
== [Kind
x, Kind
y   ] = (SMTLambda, SMTLambda) -> Maybe (SMTLambda, SMTLambda)
forall a. a -> Maybe a
Just (SMTLambda
f, SMTLambda
g)
                 getFuncs (SeqOp (SBVFilter    Kind
a     SMTLambda
f)) (SeqOp (SBVFilter    Kind
x     SMTLambda
g)) | [Kind
a      ] [Kind] -> [Kind] -> Bool
forall a. Eq a => a -> a -> Bool
== [Kind
x      ] = (SMTLambda, SMTLambda) -> Maybe (SMTLambda, SMTLambda)
forall a. a -> Maybe a
Just (SMTLambda
f, SMTLambda
g)
                 getFuncs (SeqOp (SBVAll       Kind
a     SMTLambda
f)) (SeqOp (SBVAll       Kind
x     SMTLambda
g)) | [Kind
a      ] [Kind] -> [Kind] -> Bool
forall a. Eq a => a -> a -> Bool
== [Kind
x      ] = (SMTLambda, SMTLambda) -> Maybe (SMTLambda, SMTLambda)
forall a. a -> Maybe a
Just (SMTLambda
f, SMTLambda
g)
                 getFuncs (SeqOp (SBVAny       Kind
a     SMTLambda
f)) (SeqOp (SBVAny       Kind
x     SMTLambda
g)) | [Kind
a      ] [Kind] -> [Kind] -> Bool
forall a. Eq a => a -> a -> Bool
== [Kind
x      ] = (SMTLambda, SMTLambda) -> Maybe (SMTLambda, SMTLambda)
forall a. a -> Maybe a
Just (SMTLambda
f, SMTLambda
g)
                 getFuncs Op
_                              Op
_                                                     = Maybe (SMTLambda, SMTLambda)
forall a. Maybe a
Nothing

                 equate :: (Op, (String, SMTLambda), (String, SMTLambda)) -> [String]
                 equate :: (Op, (String, SMTLambda), (String, SMTLambda)) -> [String]
equate (Op
o, (String
nm1, SMTLambda
f), (String
nm2, SMTLambda
g)) = [ String
"; Equality for " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" vs. " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm2
                                                  , String
"(assert (forall (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
decls String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                                                  , String
"                (=> (= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SMTLambda -> String
forall a. Show a => a -> String
show SMTLambda
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SMTLambda -> String
forall a. Show a => a -> String
show SMTLambda
g String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                                                  , String
"                    (= (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm1 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
nm2 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
")))))"
                                                  ]
                      where params :: [(String, Kind)]
params = Op -> [(String, Kind)]
paramsOf Op
o
                            args :: String
args   = [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ((String, Kind) -> String) -> [(String, Kind)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Kind) -> String
forall a b. (a, b) -> a
fst [(String, Kind)]
params
                            decls :: String
decls  = [String] -> String
unwords [Char
'(' Char -> String -> String
forall a. a -> [a] -> [a]
: String
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" | (String
n, Kind
k) <- [(String, Kind)]
params]

                            paramsOf :: Op -> [(String, Kind)]
paramsOf (SeqOp (SBVZipWith   Kind
k1 Kind
k2 Kind
_ SMTLambda
_)) = [           (String
"xs", Kind -> Kind
KList Kind
k1), (String
"ys", Kind -> Kind
KList Kind
k2)]
                            paramsOf (SeqOp (SBVPartition Kind
k1      SMTLambda
_)) = [           (String
"xs", Kind -> Kind
KList Kind
k1)]
                            paramsOf (SeqOp (SBVMap       Kind
k1    Kind
_ SMTLambda
_)) = [           (String
"xs", Kind -> Kind
KList Kind
k1)]
                            paramsOf (SeqOp (SBVFoldl     Kind
k1 Kind
k2   SMTLambda
_)) = [(String
"b", Kind
k2), (String
"xs", Kind -> Kind
KList Kind
k1)]
                            paramsOf (SeqOp (SBVFoldr     Kind
k1 Kind
k2   SMTLambda
_)) = [(String
"b", Kind
k2), (String
"xs", Kind -> Kind
KList Kind
k1)]
                            paramsOf (SeqOp (SBVFilter    Kind
k1      SMTLambda
_)) = [           (String
"xs", Kind -> Kind
KList Kind
k1)]
                            paramsOf (SeqOp (SBVAll       Kind
k1      SMTLambda
_)) = [           (String
"xs", Kind -> Kind
KList Kind
k1)]
                            paramsOf (SeqOp (SBVAny       Kind
k1      SMTLambda
_)) = [           (String
"xs", Kind -> Kind
KList Kind
k1)]
                            paramsOf Op
op                               = String -> [(String, Kind)]
forall a. HasCallStack => String -> a
error (String -> [(String, Kind)]) -> String -> [(String, Kind)]
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.firstifiedEqualities: Unexpected op: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
forall a. Show a => a -> String
show Op
op

        userDefs :: [String]
userDefs = [(SMTDef, SBVType)] -> [String]
declUserFuns [(SMTDef, SBVType)]
defs
        exportedDefs :: [String]
exportedDefs
          | [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
userDefs
          = [String
"; No calls to 'smtFunction' found."]
          | Bool
True
          = String
"; Automatically generated by SBV. Do not modify!" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
userDefs


        (TableMap
tableMap, [(((Int, Kind, Kind), [SV]), [String])]
constTables, [(((Int, Kind, Kind), [SV]), [String])]
nonConstTables) = RoundingMode
-> [(SV, CV)]
-> [((Int, Kind, Kind), [SV])]
-> (TableMap, [(((Int, Kind, Kind), [SV]), [String])],
    [(((Int, Kind, Kind), [SV]), [String])])
constructTables RoundingMode
rm [(SV, CV)]
consts [((Int, Kind, Kind), [SV])]
tbls

        delayedEqualities :: [String]
delayedEqualities = ((((Int, Kind, Kind), [SV]), [String]) -> [String])
-> [(((Int, Kind, Kind), [SV]), [String])] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (((Int, Kind, Kind), [SV]), [String]) -> [String]
forall a b. (a, b) -> b
snd [(((Int, Kind, Kind), [SV]), [String])]
nonConstTables

        finalAssert :: [String]
finalAssert
          | Bool
noConstraints = []
          | Bool
True          =    (([(String, String)], Either SV SV) -> String)
-> [([(String, String)], Either SV SV)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\([(String, String)]
attr, Either SV SV
v) -> String
"(assert "      String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(String, String)] -> String -> String
addAnnotations [(String, String)]
attr (Either SV SV -> String
mkLiteral Either SV SV
v) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")") [([(String, String)], Either SV SV)]
hardAsserts
                            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (([(String, String)], Either SV SV) -> String)
-> [([(String, String)], Either SV SV)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\([(String, String)]
attr, Either SV SV
v) -> String
"(assert-soft " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(String, String)] -> String -> String
addAnnotations [(String, String)]
attr (Either SV SV -> String
mkLiteral Either SV SV
v) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")") [([(String, String)], Either SV SV)]
softAsserts
          where mkLiteral :: Either SV SV -> String
mkLiteral (Left  SV
v) =            SV -> String
cvtSV SV
v
                mkLiteral (Right SV
v) = String
"(not " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

                (Bool
noConstraints, [(Bool, [(String, String)], Either SV SV)]
assertions) = (Bool, [(Bool, [(String, String)], Either SV SV)])
finalAssertions

                hardAsserts, softAsserts :: [([(String, String)], Either SV SV)]
                hardAsserts :: [([(String, String)], Either SV SV)]
hardAsserts = [([(String, String)]
attr, Either SV SV
v) | (Bool
False, [(String, String)]
attr, Either SV SV
v) <- [(Bool, [(String, String)], Either SV SV)]
assertions]
                softAsserts :: [([(String, String)], Either SV SV)]
softAsserts = [([(String, String)]
attr, Either SV SV
v) | (Bool
True,  [(String, String)]
attr, Either SV SV
v) <- [(Bool, [(String, String)], Either SV SV)]
assertions]

        finalAssertions :: (Bool, [(Bool, [(String, String)], Either SV SV)])  -- If Left: positive, Right: negative
        finalAssertions :: (Bool, [(Bool, [(String, String)], Either SV SV)])
finalAssertions
           | [(Bool, [(String, String)], Either SV SV)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Bool, [(String, String)], Either SV SV)]
finals = (Bool
True,  [(Bool
False, [], SV -> Either SV SV
forall a b. a -> Either a b
Left SV
trueSV)])
           | Bool
True        = (Bool
False, [(Bool, [(String, String)], Either SV SV)]
finals)

           where finals :: [(Bool, [(String, String)], Either SV SV)]
finals  = [(Bool, [(String, String)], Either SV SV)]
forall {b}. [(Bool, [(String, String)], Either SV b)]
cstrs' [(Bool, [(String, String)], Either SV SV)]
-> [(Bool, [(String, String)], Either SV SV)]
-> [(Bool, [(String, String)], Either SV SV)]
forall a. [a] -> [a] -> [a]
++ [(Bool, [(String, String)], Either SV SV)]
-> (Either SV SV -> [(Bool, [(String, String)], Either SV SV)])
-> Maybe (Either SV SV)
-> [(Bool, [(String, String)], Either SV SV)]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] (\Either SV SV
r -> [(Bool
False, [], Either SV SV
r)]) Maybe (Either SV SV)
mbO

                 cstrs' :: [(Bool, [(String, String)], Either SV b)]
cstrs' =  [(Bool
isSoft, [(String, String)]
attrs, Either SV b
c') | (Bool
isSoft, [(String, String)]
attrs, SV
c) <- Seq (Bool, [(String, String)], SV)
-> [(Bool, [(String, String)], SV)]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (Bool, [(String, String)], SV)
cstrs, Just Either SV b
c' <- [SV -> Maybe (Either SV b)
forall {b}. SV -> Maybe (Either SV b)
pos SV
c]]

                 mbO :: Maybe (Either SV SV)
mbO | Bool
isSat = SV -> Maybe (Either SV SV)
forall {b}. SV -> Maybe (Either SV b)
pos SV
out
                     | Bool
True  = SV -> Maybe (Either SV SV)
neg SV
out

                 neg :: SV -> Maybe (Either SV SV)
neg SV
s
                  | SV
s SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV = Maybe (Either SV SV)
forall a. Maybe a
Nothing
                  | SV
s SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV  = Either SV SV -> Maybe (Either SV SV)
forall a. a -> Maybe a
Just (Either SV SV -> Maybe (Either SV SV))
-> Either SV SV -> Maybe (Either SV SV)
forall a b. (a -> b) -> a -> b
$ SV -> Either SV SV
forall a b. a -> Either a b
Left SV
falseSV
                  | Bool
True         = Either SV SV -> Maybe (Either SV SV)
forall a. a -> Maybe a
Just (Either SV SV -> Maybe (Either SV SV))
-> Either SV SV -> Maybe (Either SV SV)
forall a b. (a -> b) -> a -> b
$ SV -> Either SV SV
forall a b. b -> Either a b
Right SV
s

                 pos :: SV -> Maybe (Either SV b)
pos SV
s
                  | SV
s SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV  = Maybe (Either SV b)
forall a. Maybe a
Nothing
                  | SV
s SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV = Either SV b -> Maybe (Either SV b)
forall a. a -> Maybe a
Just (Either SV b -> Maybe (Either SV b))
-> Either SV b -> Maybe (Either SV b)
forall a b. (a -> b) -> a -> b
$ SV -> Either SV b
forall a b. a -> Either a b
Left SV
falseSV
                  | Bool
True         = Either SV b -> Maybe (Either SV b)
forall a. a -> Maybe a
Just (Either SV b -> Maybe (Either SV b))
-> Either SV b -> Maybe (Either SV b)
forall a b. (a -> b) -> a -> b
$ SV -> Either SV b
forall a b. a -> Either a b
Left SV
s

        asgns :: [(SV, SBVExpr)]
asgns = Seq (SV, SBVExpr) -> [(SV, SBVExpr)]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (SV, SBVExpr)
asgnsSeq

        userNameMap :: Map SV String
userNameMap = [(SV, String)] -> Map SV String
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList ([(SV, String)] -> Map SV String)
-> [(SV, String)] -> Map SV String
forall a b. (a -> b) -> a -> b
$ (NamedSymVar -> (SV, String)) -> [NamedSymVar] -> [(SV, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\NamedSymVar
nSymVar -> (NamedSymVar -> SV
getSV NamedSymVar
nSymVar, NamedSymVar -> String
getUserName' NamedSymVar
nSymVar)) [NamedSymVar]
inputs
        userName :: SV -> Maybe String
userName SV
s = case SV -> Map SV String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup SV
s Map SV String
userNameMap of
                        Just String
u  | SV -> String
forall a. Show a => a -> String
show SV
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
u -> String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"tracks user variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
u
                        Maybe String
_                     -> Maybe String
forall a. Maybe a
Nothing

-- Declare "known" SBV functions here
declSBVFunc :: SMTConfig -> Op -> (String, [String])
declSBVFunc :: SMTConfig -> Op -> (String, [String])
declSBVFunc SMTConfig
cfg Op
op = (String
nm, [String]
comment [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
body)
  where nm :: String
nm = Int -> Op -> String
firstify (KDOptions -> Int
firstifyUniqueLen (SMTConfig -> KDOptions
kdOptions SMTConfig
cfg)) Op
op

        comment :: [String]
comment = [String
"; Firstified function: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
htyp]

        body :: [String]
body = case Op
op of
                 SeqOp (SBVReverse   Kind
KString)                -> [String]
mkStringRev
                 SeqOp (SBVReverse   (KList Kind
k))              -> Kind -> [String]
mkSeqRev    (Kind -> Kind
KList Kind
k)
                 SeqOp (SBVZip       Kind
k1 Kind
k2)                  -> Kind -> Kind -> Maybe (Kind, String) -> [String]
mkZip       Kind
k1 Kind
k2 Maybe (Kind, String)
forall a. Maybe a
Nothing
                 SeqOp (SBVZipWith   Kind
k1 Kind
k2 Kind
k3 (SMTLambda String
f)) -> Kind -> Kind -> Maybe (Kind, String) -> [String]
mkZip       Kind
k1 Kind
k2 ((Kind, String) -> Maybe (Kind, String)
forall a. a -> Maybe a
Just (Kind
k3, String
f))
                 SeqOp (SBVPartition Kind
ek       (SMTLambda String
f)) -> Kind -> String -> [String]
mkPartition Kind
ek String
f
                 SeqOp (SBVMap       Kind
k1 Kind
k2    (SMTLambda String
f)) -> Kind -> Kind -> String -> [String]
mkMap       Kind
k1 Kind
k2 String
f
                 SeqOp (SBVFoldl     Kind
k1 Kind
k2    (SMTLambda String
f)) -> Kind -> Kind -> String -> [String]
mkFoldl     Kind
k1 Kind
k2 String
f
                 SeqOp (SBVFoldr     Kind
k1 Kind
k2    (SMTLambda String
f)) -> Kind -> Kind -> String -> [String]
mkFoldr     Kind
k1 Kind
k2 String
f
                 SeqOp (SBVFilter    Kind
ek       (SMTLambda String
f)) -> Kind -> String -> [String]
mkFilter    Kind
ek    String
f
                 SeqOp (SBVAll       Kind
ek       (SMTLambda String
f)) -> Bool -> Kind -> String -> [String]
mkAnyAll    Bool
True  Kind
ek String
f
                 SeqOp (SBVAny       Kind
ek       (SMTLambda String
f)) -> Bool -> Kind -> String -> [String]
mkAnyAll    Bool
False Kind
ek String
f
                 SeqOp (SBVConcat    Kind
ek)                     -> Kind -> [String]
mkConcat    Kind
ek
                 Op
_                                           -> String -> [String]
forall a. HasCallStack => String -> a
error (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.declSBVFunc.body: Unexpected internal function: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Op, String) -> String
forall a. Show a => a -> String
show (Op
op, String
nm)

        -- helper when there's no higher order arg
        shf :: String -> [Kind] -> Kind -> String
        shf :: String -> [Kind] -> Kind -> String
shf String
f [Kind]
args Kind
rt = String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" -> " ((Kind -> String) -> [Kind] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Kind -> String
forall a. Show a => a -> String
show ([Kind]
args [Kind] -> [Kind] -> [Kind]
forall a. [a] -> [a] -> [a]
++ [Kind
rt]))

        -- helper when there's a function arg
        shh :: String -> ([Kind], Kind) -> ([Kind], Kind) -> String
        shh :: String -> ([Kind], Kind) -> ([Kind], Kind) -> String
shh String
f ([Kind]
fargs, Kind
fret) ([Kind]
args, Kind
rt) = String
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :: (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" -> " ((Kind -> String) -> [Kind] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Kind -> String
forall a. Show a => a -> String
show ([Kind]
fargs [Kind] -> [Kind] -> [Kind]
forall a. [a] -> [a] -> [a]
++ [Kind
fret])) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") -> "
                                           String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
" -> " ((Kind -> String) -> [Kind] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Kind -> String
forall a. Show a => a -> String
show ([Kind]
args [Kind] -> [Kind] -> [Kind]
forall a. [a] -> [a] -> [a]
++ [Kind
rt]))

        -- This is the haskell type
        htyp :: String
htyp = case Op
op of
                 SeqOp (SBVReverse   Kind
KString)   -> String -> [Kind] -> Kind -> String
shf String
"reverse"   [Kind
KString] Kind
KString
                 SeqOp (SBVReverse   k :: Kind
k@KList{}) -> String -> [Kind] -> Kind -> String
shf String
"reverse"   [Kind
k] Kind
k
                 SeqOp (SBVZip       Kind
a Kind
b)       -> String -> [Kind] -> Kind -> String
shf String
"zip"       [Kind -> Kind
KList Kind
a, Kind -> Kind
KList Kind
b] (Kind -> Kind
KList ([Kind] -> Kind
KTuple [Kind
a, Kind
b]))
                 SeqOp (SBVZipWith   Kind
a Kind
b Kind
c SMTLambda
_)   -> String -> ([Kind], Kind) -> ([Kind], Kind) -> String
shh String
"zipWith"   ([Kind
a, Kind
b], Kind
c)  ([Kind -> Kind
KList Kind
a, Kind -> Kind
KList Kind
b], Kind -> Kind
KList Kind
c)
                 SeqOp (SBVPartition Kind
a     SMTLambda
_)   -> String -> ([Kind], Kind) -> ([Kind], Kind) -> String
shh String
"partition" ([Kind
a], Kind
KBool) ([Kind -> Kind
KList Kind
a], [Kind] -> Kind
KTuple [Kind -> Kind
KList Kind
a, Kind -> Kind
KList Kind
a])
                 SeqOp (SBVMap       Kind
a Kind
b   SMTLambda
_)   -> String -> ([Kind], Kind) -> ([Kind], Kind) -> String
shh String
"map"       ([Kind
a], Kind
b)     ([Kind -> Kind
KList Kind
a], Kind -> Kind
KList Kind
b)
                 SeqOp (SBVFoldl     Kind
a Kind
b   SMTLambda
_)   -> String -> ([Kind], Kind) -> ([Kind], Kind) -> String
shh String
"foldl"     ([Kind
b, Kind
a], Kind
b)  ([Kind
b, Kind -> Kind
KList Kind
a], Kind
b)
                 SeqOp (SBVFoldr     Kind
a Kind
b   SMTLambda
_)   -> String -> ([Kind], Kind) -> ([Kind], Kind) -> String
shh String
"foldr"     ([Kind
a, Kind
b], Kind
b)  ([Kind
b, Kind -> Kind
KList Kind
a], Kind
b)
                 SeqOp (SBVFilter    Kind
a     SMTLambda
_)   -> String -> ([Kind], Kind) -> ([Kind], Kind) -> String
shh String
"filter"    ([Kind
a], Kind
KBool) ([Kind -> Kind
KList Kind
a], Kind -> Kind
KList Kind
a)
                 SeqOp (SBVAll       Kind
a     SMTLambda
_)   -> String -> ([Kind], Kind) -> ([Kind], Kind) -> String
shh String
"all"       ([Kind
a], Kind
KBool) ([Kind -> Kind
KList Kind
a], Kind
KBool)
                 SeqOp (SBVAny       Kind
a     SMTLambda
_)   -> String -> ([Kind], Kind) -> ([Kind], Kind) -> String
shh String
"any"       ([Kind
a], Kind
KBool) ([Kind -> Kind
KList Kind
a], Kind
KBool)
                 SeqOp (SBVConcat    Kind
a)         -> String -> [Kind] -> Kind -> String
shf String
"concat"    [Kind -> Kind
KList (Kind -> Kind
KList Kind
a)] (Kind -> Kind
KList Kind
a)
                 Op
_                              -> String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.declSBVFunc.htyp: Unexpected internal function: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Op, String) -> String
forall a. Show a => a -> String
show (Op
op, String
nm)

        -- in Z3, lambdas are applied with select. In CVC5, it's @. This might change with higher-order features being added to SMTLib in v3
        par :: String -> String
par String
x = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        app :: String -> [String] -> String
app String
f [String]
args = String -> String
par (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
f String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
args

        happ :: String -> [String] -> String
happ String
f [String]
args | Bool
isCVC5 = String -> [String] -> String
app String
"@"      (String
f String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
args)
                    | Bool
True   = String -> [String] -> String
app String
"select" (String
f String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
args)

        hd :: String -> String
hd String
l = String -> [String] -> String
app String
"seq.nth"     [String
l, String
"0"]
        tl :: String -> String
tl String
l = String -> [String] -> String
app String
"seq.extract" [String
l, String
"1", String -> [String] -> String
app String
"-" [String -> [String] -> String
app String
"seq.len" [String
l], String
"1"]]

        empty :: String -> String
empty   String
typ     = String -> [String] -> String
app String
"as seq.empty" [String
typ]
        isEmpty :: String -> String -> String
isEmpty String
arg String
typ = String -> [String] -> String
app String
"=" [String
arg, String -> String
empty String
typ]

        isCVC5 :: Bool
isCVC5 = case SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
cfg) of
                   Solver
CVC5 -> Bool
True
                   Solver
_    -> Bool
False

        mkStringRev :: [String]
mkStringRev = [ String
"(define-fun-rec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ((str String)) String"
                      , String
"                (ite (= str \"\")"
                      , String
"                     \"\""
                      , String
"                     (str.++ (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (str.substr str 1 (- (str.len str) 1)))"
                      , String
"                             (str.substr str 0 1))))"
                      ]


        mkSeqRev :: Kind -> [String]
mkSeqRev Kind
k = [ String
"(define-fun-rec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ((lst " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t
                     , String
"                (ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String -> String
isEmpty String
"lst" String
t
                     , String
"                     " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
empty String
t
                     , String
"                     (seq.++ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
app String
nm [String -> String
tl String
"lst"] String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (seq.unit " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
hd String
"lst" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))))"
                     ]
          where t :: String
t = Kind -> String
smtType Kind
k

        -- [a] -> [b] -> [(a, b)]
        -- [a] -> [b] -> (a -> b -> c) -> [c]
        mkZip :: Kind -> Kind -> Maybe (Kind, String) -> [String]
mkZip Kind
a Kind
b Maybe (Kind, String)
mbcF = [ String
"(define-fun-rec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ((lst1 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tla String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") (lst2 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tlb String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tlr
                         , String
"               (ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
app String
"or" [String -> String -> String
isEmpty String
"lst1" String
tla, String -> String -> String
isEmpty String
"lst2" String
tlb]
                         , String
"                    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
empty String
tlr
                         , String
"                    (seq.++ (seq.unit " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String -> String
mkTup (String -> String
hd String
"lst1") (String -> String
hd String
"lst2") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
app String
nm [String -> String
tl String
"lst1", String -> String
tl String
"lst2"] String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")))"
                         ]
         where tla :: String
tla = Kind -> String
smtType (Kind -> Kind
KList Kind
a)
               tlb :: String
tlb = Kind -> String
smtType (Kind -> Kind
KList Kind
b)
               tlr :: String
tlr = case Maybe (Kind, String)
mbcF of
                       Maybe (Kind, String)
Nothing     -> Kind -> String
smtType (Kind -> Kind
KList ([Kind] -> Kind
KTuple [Kind
a, Kind
b]))
                       Just (Kind
c, String
_) -> Kind -> String
smtType (Kind -> Kind
KList Kind
c)

               mkTup :: String -> String -> String
mkTup String
x String
y = case Maybe (Kind, String)
mbcF of
                             Just (Kind
_, String
f) -> String -> [String] -> String
happ String
f   [String
x, String
y]
                             Maybe (Kind, String)
Nothing     -> String -> [String] -> String
app  String
tup [String
x, String
y]
               tup :: String
tup = String -> [String] -> String
app String
"as" [String
"mkSBVTuple2", String -> [String] -> String
app String
"SBVTuple2" [Kind -> String
smtType Kind
a, Kind -> String
smtType Kind
b]]

        -- (a -> Bool) -> [a] -> ([a], [a])
        mkPartition :: Kind -> String -> [String]
mkPartition Kind
a String
f = [ String
"(define-fun-rec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ((lst " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tla String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tpla
                          , String
"                (ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String -> String
isEmpty String
"lst" String
tla
                          , String
"                     " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
base
                          , String
"                     (let ((a    " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
hd String
"lst" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
                          , String
"                     (let ((ua   (seq.unit a)))"
                          , String
"                     (let ((rest " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
app String
nm [String -> String
tl String
"lst"] String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
                          , String
"                     (let ((ts   (proj_1_SBVTuple2 rest)))"
                          , String
"                     (let ((fs   (proj_2_SBVTuple2 rest)))"
                          , String
"                     (ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
happ String
f [String -> String
hd String
"lst"]
                          , String
"                          " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String -> String
pair String
"(seq.++ ua ts)" String
"fs"
                          , String
"                          " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String -> String
pair String
"ts" String
"(seq.++ ua fs)" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))))))))"
                          ]
           where tla :: String
tla  = Kind -> String
smtType (Kind -> Kind
KList Kind
a)
                 tpla :: String
tpla = Kind -> String
smtType ([Kind] -> Kind
KTuple [Kind -> Kind
KList Kind
a, Kind -> Kind
KList Kind
a])
                 base :: String
base       = String
"(mkSBVTuple2 (as seq.empty " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tla String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") (as seq.empty " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tla String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
                 pair :: String -> String -> String
pair String
ts String
fs = String
"((as mkSBVTuple2 (SBVTuple2 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tla String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tla String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ts String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        -- (b -> a -> b) -> b -> [a] -> b
        mkFoldl :: Kind -> Kind -> String -> [String]
mkFoldl Kind
a Kind
b String
f = [ String
"(define-fun-rec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ((base " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tb String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") (lst " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tla String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tb
                        , String
"                (ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String -> String
isEmpty String
"lst" String
tla
                        , String
"                     base"
                        , String
"                     " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
app String
nm [String -> [String] -> String
happ String
f [String
"base", String -> String
hd String
"lst"], String -> String
tl String
"lst"] String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
                        ]
           where tla :: String
tla = Kind -> String
smtType (Kind -> Kind
KList Kind
a)
                 tb :: String
tb  = Kind -> String
smtType Kind
b

        -- (a -> b -> b) -> b -> [a] -> b
        mkFoldr :: Kind -> Kind -> String -> [String]
mkFoldr Kind
a Kind
b String
f = [ String
"(define-fun-rec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ((base " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tb String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") (lst " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tla String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tb
                        , String
"                (ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String -> String
isEmpty String
"lst" String
tla
                        , String
"                     base"
                        , String
"                     " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
happ String
f [String -> String
hd String
"lst", String -> [String] -> String
app String
nm [String
"base", String -> String
tl String
"lst"]] String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
                        ]
           where tla :: String
tla = Kind -> String
smtType (Kind -> Kind
KList Kind
a)
                 tb :: String
tb  = Kind -> String
smtType Kind
b

        -- (a -> b) -> [a] -> [b]
        mkMap :: Kind -> Kind -> String -> [String]
mkMap Kind
a Kind
b String
f = [ String
"(define-fun-rec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ((lst " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tla String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tlb
                      , String
"              (ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String -> String
isEmpty String
"lst" String
tla
                      , String
"                   " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
empty String
tlb
                      , String
"                   (seq.++ (seq.unit " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
happ String
f [String -> String
hd String
"lst"] String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                      , String
"                           " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
app String
nm [String -> String
tl String
"lst"] String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")))"
                      ]
           where tla :: String
tla = Kind -> String
smtType (Kind -> Kind
KList Kind
a)
                 tlb :: String
tlb = Kind -> String
smtType (Kind -> Kind
KList Kind
b)

        -- (a -> Bool) -> [a] -> [a]
        mkFilter :: Kind -> String -> [String]
mkFilter Kind
a String
f = [ String
"(define-fun-rec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ((lst " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tla String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tla
                       , String
"                (ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String -> String
isEmpty String
"lst" String
tla
                       , String
"                     " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
empty String
tla
                       , String
"                     (let ((rest (" 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 -> String
tl String
"lst" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")))"
                       , String
"                          (ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
happ String
f [String -> String
hd String
"lst"]
                       , String
"                               (seq.++ (seq.unit " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
hd String
"lst" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") rest)"
                       , String
"                                       rest))))"
                       ]
          where tla :: String
tla = Kind -> String
smtType (Kind -> Kind
KList Kind
a)

        -- (a -> Bool) -> [a] -> Bool
        mkAnyAll :: Bool -> Kind -> String -> [String]
mkAnyAll Bool
isAll Kind
a String
f = [ String
"(define-fun-rec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ((lst " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tla String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) Bool"
                             , String
"                (ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String -> String
isEmpty String
"lst" String
tla
                             , String
"                     " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
base
                             , String
"                     " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
app String
conn [String -> [String] -> String
happ String
f [String -> String
hd String
"lst"], String -> [String] -> String
app String
nm [String -> String
tl String
"lst"]] String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
                             ]
          where tla :: String
tla = Kind -> String
smtType (Kind -> Kind
KList Kind
a)
                (String
base, String
conn) | Bool
isAll = (String
"true",  String
"and")
                             | Bool
True  = (String
"false", String
"or")

        -- [[a]] -> [a]
        mkConcat :: Kind -> [String]
mkConcat Kind
a = [ String
"(define-fun-rec " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ((lst " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tlla String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tla
                     , String
"                (ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String -> String
isEmpty String
"lst" String
tlla
                     , String
"                     " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
empty String
tla
                     , String
"                     (seq.++ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
hd String
"lst" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
tl String
"lst" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))))"
                     ]
         where tla :: String
tla  = Kind -> String
smtType (Kind -> Kind
KList Kind
a)
               tlla :: String
tlla = Kind -> String
smtType (Kind -> Kind
KList (Kind -> Kind
KList Kind
a))

-- | Declare new sorts
declSort :: (String, Maybe [String]) -> [String]
declSort :: (String, Maybe [String]) -> [String]
declSort (String
s, Maybe [String]
_)
  | String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"RoundingMode" -- built-in-sort; so don't declare.
  = []
declSort (String
s, Maybe [String]
Nothing) = [ String
"(declare-sort " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" 0)  ; N.B. Uninterpreted sort."
                        , String
"(declare-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
witnessName String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" () " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                        ]
declSort (String
s, Just [String]
fs) = [ String
"(declare-datatypes ((" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" 0)) ((" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\String
c -> String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")") [String]
fs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")))"
                        , String
"(define-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_constrIndex ((x " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) Int"
                        ] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"   " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> Int -> String
forall {t}. (Show t, Num t) => [String] -> t -> String
body [String]
fs (Int
0::Int)] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
")"]
        where body :: [String] -> t -> String
body []     t
_ = String
""
              body [String
_]    t
i = t -> String
forall a. Show a => a -> String
show t
i
              body (String
c:[String]
cs) t
i = String
"(ite (= x " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ t -> String
forall a. Show a => a -> String
show t
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> t -> String
body [String]
cs (t
it -> t -> t
forall a. Num a => a -> a -> a
+t
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

-- | Declare tuple datatypes
--
-- eg:
--
-- @
-- (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2)
--                                     ((mkSBVTuple2 (proj_1_SBVTuple2 T1)
--                                                   (proj_2_SBVTuple2 T2))))))
-- @
declTuple :: Int -> [String]
declTuple :: Int -> [String]
declTuple Int
arity
  | Int
arity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 = [String
"(declare-datatypes ((SBVTuple0 0)) (((mkSBVTuple0))))"]
  | Int
arity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = String -> [String]
forall a. HasCallStack => String -> a
error String
"Data.SBV.declTuple: Unexpected one-tuple"
  | Bool
True       =    (String
l1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"(par (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [Int -> String
forall a. Show a => a -> String
param Int
i | Int
i <- [Int
1..Int
arity]] String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")")
                 String -> [String] -> [String]
forall a. a -> [a] -> [a]
:  [Int -> String
forall {a}. (Eq a, Num a) => a -> String
pre Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
proj Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
post Int
i    | Int
i <- [Int
1..Int
arity]]
  where l1 :: String
l1     = String
"(declare-datatypes ((SBVTuple" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
arity String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
arity String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) ("
        l2 :: String
l2     = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
l1) Char
' ' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"((mkSBVTuple" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
arity String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
        tab :: String
tab    = Int -> Char -> String
forall a. Int -> a -> [a]
replicate (String -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
l2) Char
' '

        pre :: a -> String
pre a
1  = String
l2
        pre a
_  = String
tab

        proj :: a -> String
proj a
i = String
"(proj_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_SBVTuple" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
arity 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
param a
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        post :: Int -> String
post Int
i = if Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
arity then String
")))))" else String
""

        param :: a -> String
param a
i = String
"T" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i

-- | Find the set of tuple sizes to declare, eg (2-tuple, 5-tuple).
-- NB. We do *not* need to recursively go into list/tuple kinds here,
-- because register-kind function automatically registers all subcomponent
-- kinds, thus everything we need is available at the top-level.
findTupleArities :: Set Kind -> [Int]
findTupleArities :: Set Kind -> [Int]
findTupleArities Set Kind
ks = Set Int -> [Int]
forall a. Set a -> [a]
Set.toAscList
                    (Set Int -> [Int]) -> Set Int -> [Int]
forall a b. (a -> b) -> a -> b
$ ([Kind] -> Int) -> Set [Kind] -> Set Int
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map [Kind] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
                    (Set [Kind] -> Set Int) -> Set [Kind] -> Set Int
forall a b. (a -> b) -> a -> b
$ [[Kind]] -> Set [Kind]
forall a. Ord a => [a] -> Set a
Set.fromList [ [Kind]
tupKs | KTuple [Kind]
tupKs <- Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList Set Kind
ks ]

-- | Is @Either@ being used?
containsSum :: Set Kind -> Bool
containsSum :: Set Kind -> Bool
containsSum = Bool -> Bool
not (Bool -> Bool) -> (Set Kind -> Bool) -> Set Kind -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Kind -> Bool
forall a. Set a -> Bool
Set.null (Set Kind -> Bool) -> (Set Kind -> Set Kind) -> Set Kind -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Kind -> Bool) -> Set Kind -> Set Kind
forall a. (a -> Bool) -> Set a -> Set a
Set.filter Kind -> Bool
forall a. HasKind a => a -> Bool
isEither

-- | Is @Maybe@ being used?
containsMaybe :: Set Kind -> Bool
containsMaybe :: Set Kind -> Bool
containsMaybe = Bool -> Bool
not (Bool -> Bool) -> (Set Kind -> Bool) -> Set Kind -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Kind -> Bool
forall a. Set a -> Bool
Set.null (Set Kind -> Bool) -> (Set Kind -> Set Kind) -> Set Kind -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Kind -> Bool) -> Set Kind -> Set Kind
forall a. (a -> Bool) -> Set a -> Set a
Set.filter Kind -> Bool
forall a. HasKind a => a -> Bool
isMaybe

-- | Is @Rational@ being used?
containsRationals :: Set Kind -> Bool
containsRationals :: Set Kind -> Bool
containsRationals = Bool -> Bool
not (Bool -> Bool) -> (Set Kind -> Bool) -> Set Kind -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Kind -> Bool
forall a. Set a -> Bool
Set.null (Set Kind -> Bool) -> (Set Kind -> Set Kind) -> Set Kind -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Kind -> Bool) -> Set Kind -> Set Kind
forall a. (a -> Bool) -> Set a -> Set a
Set.filter Kind -> Bool
forall a. HasKind a => a -> Bool
isRational

declSum :: [String]
declSum :: [String]
declSum = [ String
"(declare-datatypes ((SBVEither 2)) ((par (T1 T2)"
          , String
"                                    ((left_SBVEither  (get_left_SBVEither  T1))"
          , String
"                                     (right_SBVEither (get_right_SBVEither T2))))))"
          ]

declMaybe :: [String]
declMaybe :: [String]
declMaybe = [ String
"(declare-datatypes ((SBVMaybe 1)) ((par (T)"
            , String
"                                    ((nothing_SBVMaybe)"
            , String
"                                     (just_SBVMaybe (get_just_SBVMaybe T))))))"
            ]

-- Internally, we do *not* keep the rationals in reduced form! So, the boolean operators explicitly do the math
-- to make sure equivalent values are treated correctly.
declRationals :: [String]
declRationals :: [String]
declRationals = [ String
"(declare-datatype SBVRational ((SBV.Rational (sbv.rat.numerator Int) (sbv.rat.denominator Int))))"
                , String
""
                , String
"(define-fun sbv.rat.eq ((x SBVRational) (y SBVRational)) Bool"
                , String
"   (= (* (sbv.rat.numerator   x) (sbv.rat.denominator y))"
                , String
"      (* (sbv.rat.denominator x) (sbv.rat.numerator   y)))"
                , String
")"
                , String
""
                , String
"(define-fun sbv.rat.notEq ((x SBVRational) (y SBVRational)) Bool"
                , String
"   (not (sbv.rat.eq x y))"
                , String
")"
                , String
""
                , String
"(define-fun sbv.rat.lt ((x SBVRational) (y SBVRational)) Bool"
                , String
"   (<  (* (sbv.rat.numerator   x) (sbv.rat.denominator y))"
                , String
"       (* (sbv.rat.denominator x) (sbv.rat.numerator   y)))"
                , String
")"
                , String
""
                , String
"(define-fun sbv.rat.leq ((x SBVRational) (y SBVRational)) Bool"
                , String
"   (<= (* (sbv.rat.numerator   x) (sbv.rat.denominator y))"
                , String
"       (* (sbv.rat.denominator x) (sbv.rat.numerator   y)))"
                , String
")"
                , String
""
                , String
"(define-fun sbv.rat.plus ((x SBVRational) (y SBVRational)) SBVRational"
                , String
"   (SBV.Rational (+ (* (sbv.rat.numerator   x) (sbv.rat.denominator y))"
                , String
"                    (* (sbv.rat.denominator x) (sbv.rat.numerator   y)))"
                , String
"                 (* (sbv.rat.denominator x) (sbv.rat.denominator y)))"
                , String
")"
                , String
""
                , String
"(define-fun sbv.rat.minus ((x SBVRational) (y SBVRational)) SBVRational"
                , String
"   (SBV.Rational (- (* (sbv.rat.numerator   x) (sbv.rat.denominator y))"
                , String
"                    (* (sbv.rat.denominator x) (sbv.rat.numerator   y)))"
                , String
"                 (* (sbv.rat.denominator x) (sbv.rat.denominator y)))"
                , String
")"
                , String
""
                , String
"(define-fun sbv.rat.times ((x SBVRational) (y SBVRational)) SBVRational"
                , String
"   (SBV.Rational (* (sbv.rat.numerator   x) (sbv.rat.numerator y))"
                , String
"                 (* (sbv.rat.denominator x) (sbv.rat.denominator y)))"
                , String
")"
                , String
""
                , String
"(define-fun sbv.rat.uneg ((x SBVRational)) SBVRational"
                , String
"   (SBV.Rational (* (- 1) (sbv.rat.numerator x)) (sbv.rat.denominator x))"
                , String
")"
                , String
""
                , String
"(define-fun sbv.rat.abs ((x SBVRational)) SBVRational"
                , String
"   (SBV.Rational (abs (sbv.rat.numerator x)) (sbv.rat.denominator x))"
                , String
")"
                ]

-- | Convert in a query context.
-- NB. We do not store everything in @newKs@ below, but only what we need
-- to do as an extra in the incremental context. See `Data.SBV.Core.Symbolic.registerKind`
-- for a list of what we include, in case something doesn't show up
-- and you need it!
cvtInc :: SMTLibIncConverter [String]
cvtInc :: SMTLibIncConverter [String]
cvtInc ProgInfo
curProgInfo [NamedSymVar]
inps Set Kind
newKs (CnstMap
_, [(SV, CV)]
consts) [((Int, Kind, Kind), [SV])]
tbls [(String, (Bool, Maybe [String], SBVType))]
uis (SBVPgm Seq (SV, SBVExpr)
asgnsSeq) Seq (Bool, [(String, String)], SV)
cstrs SMTConfig
cfg =
            -- any new settings?
               [String]
settings
            -- sorts
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((String, Maybe [String]) -> [String])
-> [(String, Maybe [String])] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String, Maybe [String]) -> [String]
declSort [(String
s, Maybe [String]
dt) | KUserSort String
s Maybe [String]
dt <- [Kind]
newKinds]
            -- tuples. NB. Only declare the new sizes, old sizes persist.
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Int -> [String]) -> [Int] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Int -> [String]
declTuple (Set Kind -> [Int]
findTupleArities Set Kind
newKs)
            -- sums
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (if Set Kind -> Bool
containsSum   Set Kind
newKs then [String]
declSum   else [])
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (if Set Kind -> Bool
containsMaybe Set Kind
newKs then [String]
declMaybe else [])
            -- constants
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((SV, CV) -> [String]) -> [(SV, CV)] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SMTConfig -> (SV, CV) -> [String]
declConst SMTConfig
cfg) [(SV, CV)]
consts
            -- inputs
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (NamedSymVar -> [String]) -> [NamedSymVar] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NamedSymVar -> [String]
declInp [NamedSymVar]
inps
            -- uninterpreteds
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((String, (Bool, Maybe [String], SBVType)) -> [String])
-> [(String, (Bool, Maybe [String], SBVType))] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ProgInfo -> (String, (Bool, Maybe [String], SBVType)) -> [String]
declUI ProgInfo
curProgInfo) [(String, (Bool, Maybe [String], SBVType))]
uis
            -- table declarations
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
tableDecls
            -- expressions
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((SV, SBVExpr) -> [String]) -> Seq (SV, SBVExpr) -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ProgInfo -> SMTConfig -> TableMap -> (SV, SBVExpr) -> [String]
declDef ProgInfo
curProgInfo SMTConfig
cfg TableMap
tableMap) Seq (SV, SBVExpr)
asgnsSeq
            -- table setups
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
tableAssigns
            -- extra constraints
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((Bool, [(String, String)], SV) -> String)
-> [(Bool, [(String, String)], SV)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(Bool
isSoft, [(String, String)]
attr, SV
v) -> String
"(assert" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
isSoft then String
"-soft " else String
" ") String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(String, String)] -> String -> String
addAnnotations [(String, String)]
attr (SV -> String
cvtSV SV
v) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")") (Seq (Bool, [(String, String)], SV)
-> [(Bool, [(String, String)], SV)]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (Bool, [(String, String)], SV)
cstrs)
  where rm :: RoundingMode
rm = SMTConfig -> RoundingMode
roundingMode SMTConfig
cfg

        newKinds :: [Kind]
newKinds = Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList Set Kind
newKs

        declInp :: NamedSymVar -> [String]
declInp (NamedSymVar -> SV
getSV -> SV
s) = SV -> SBVType -> Maybe String -> [String]
declareFun SV
s ([Kind] -> SBVType
SBVType [SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
s]) Maybe String
forall a. Maybe a
Nothing

        (TableMap
tableMap, [(((Int, Kind, Kind), [SV]), [String])]
allTables) = (TableMap
tm, [(((Int, Kind, Kind), [SV]), [String])]
ct [(((Int, Kind, Kind), [SV]), [String])]
-> [(((Int, Kind, Kind), [SV]), [String])]
-> [(((Int, Kind, Kind), [SV]), [String])]
forall a. [a] -> [a] -> [a]
++ [(((Int, Kind, Kind), [SV]), [String])]
nct)
            where (TableMap
tm, [(((Int, Kind, Kind), [SV]), [String])]
ct, [(((Int, Kind, Kind), [SV]), [String])]
nct) = RoundingMode
-> [(SV, CV)]
-> [((Int, Kind, Kind), [SV])]
-> (TableMap, [(((Int, Kind, Kind), [SV]), [String])],
    [(((Int, Kind, Kind), [SV]), [String])])
constructTables RoundingMode
rm [(SV, CV)]
consts [((Int, Kind, Kind), [SV])]
tbls

        ([String]
tableDecls, [[String]]
tableAssigns) = [(String, [String])] -> ([String], [[String]])
forall a b. [(a, b)] -> ([a], [b])
unzip ([(String, [String])] -> ([String], [[String]]))
-> [(String, [String])] -> ([String], [[String]])
forall a b. (a -> b) -> a -> b
$ ((((Int, Kind, Kind), [SV]), [String]) -> (String, [String]))
-> [(((Int, Kind, Kind), [SV]), [String])] -> [(String, [String])]
forall a b. (a -> b) -> [a] -> [b]
map (((Int, Kind, Kind), [SV]), [String]) -> (String, [String])
mkTable [(((Int, Kind, Kind), [SV]), [String])]
allTables

        -- If we need flattening in models, do emit the required lines if preset
        settings :: [String]
settings
          | (Kind -> Bool) -> [Kind] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
needsFlattening [Kind]
newKinds
          = [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([Maybe [String]] -> [[String]]
forall a. [Maybe a] -> [a]
catMaybes [SolverCapabilities -> Maybe [String]
supportsFlattenedModels SolverCapabilities
solverCaps])
          | Bool
True
          = []
          where solverCaps :: SolverCapabilities
solverCaps = SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)

declDef :: ProgInfo -> SMTConfig -> TableMap -> (SV, SBVExpr) -> [String]
declDef :: ProgInfo -> SMTConfig -> TableMap -> (SV, SBVExpr) -> [String]
declDef ProgInfo
curProgInfo SMTConfig
cfg TableMap
tableMap (SV
s, SBVExpr
expr) =
        case SBVExpr
expr of
          SBVApp  (Label String
m) [SV
e] -> SMTConfig -> (SV, String) -> Maybe String -> [String]
defineFun SMTConfig
cfg (SV
s, SV -> String
cvtSV                                   SV
e) (String -> Maybe String
forall a. a -> Maybe a
Just String
m)
          SBVExpr
e                     -> SMTConfig -> (SV, String) -> Maybe String -> [String]
defineFun SMTConfig
cfg (SV
s, SMTConfig
-> ProgInfo
-> SolverCapabilities
-> RoundingMode
-> TableMap
-> SBVExpr
-> String
cvtExp SMTConfig
cfg ProgInfo
curProgInfo SolverCapabilities
caps RoundingMode
rm TableMap
tableMap SBVExpr
e) Maybe String
forall a. Maybe a
Nothing
  where caps :: SolverCapabilities
caps = SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)
        rm :: RoundingMode
rm   = SMTConfig -> RoundingMode
roundingMode SMTConfig
cfg

defineFun :: SMTConfig -> (SV, String) -> Maybe String -> [String]
defineFun :: SMTConfig -> (SV, String) -> Maybe String -> [String]
defineFun SMTConfig
cfg (SV
s, String
def) Maybe String
mbComment
   | Bool
hasDefFun = [String
"(define-fun "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
varT String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
def String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cmnt]
   | Bool
True      = [ String
"(declare-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
varT String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cmnt
                 , String
"(assert (= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
var String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
def String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
                 ]
  where var :: String
var  = SV -> String
forall a. Show a => a -> String
show SV
s
        varT :: String
varT = String
var String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SV] -> SV -> String
svFunType [] SV
s
        cmnt :: String
cmnt = String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (String
" ; " String -> String -> String
forall a. [a] -> [a] -> [a]
++) Maybe String
mbComment

        hasDefFun :: Bool
hasDefFun = SolverCapabilities -> Bool
supportsDefineFun (SolverCapabilities -> Bool) -> SolverCapabilities -> Bool
forall a b. (a -> b) -> a -> b
$ SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)

-- Declare constants. NB. We don't declare true/false; but just inline those as necessary
declConst :: SMTConfig -> (SV, CV) -> [String]
declConst :: SMTConfig -> (SV, CV) -> [String]
declConst SMTConfig
cfg (SV
s, CV
c)
  | SV
s SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV Bool -> Bool -> Bool
|| SV
s SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV
  = []
  | Bool
True
  = SMTConfig -> (SV, String) -> Maybe String -> [String]
defineFun SMTConfig
cfg (SV
s, RoundingMode -> CV -> String
cvtCV (SMTConfig -> RoundingMode
roundingMode SMTConfig
cfg) CV
c) Maybe String
forall a. Maybe a
Nothing

-- Make a function equality of nm against the internal function fun
mkRelEq :: String -> (String, String) -> Kind -> String
mkRelEq :: String -> (String, String) -> Kind -> String
mkRelEq String
nm (String
fun, String
order) Kind
ak = String
res
   where lhs :: String
lhs = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" x y)"
         rhs :: String
rhs = String
"((_ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fun String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
order String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") x y)"
         tk :: String
tk  = Kind -> String
smtType Kind
ak
         res :: String
res = String
"(forall ((x " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tk String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") (y " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tk String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) (= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
lhs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rhs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"

declUI :: ProgInfo -> (String, (Bool, Maybe [String], SBVType)) -> [String]
declUI :: ProgInfo -> (String, (Bool, Maybe [String], SBVType)) -> [String]
declUI ProgInfo{[(String, String)]
progTransClosures :: [(String, String)]
progTransClosures :: ProgInfo -> [(String, String)]
progTransClosures} (String
i, (Bool
_, Maybe [String]
_, SBVType
t)) = String -> SBVType -> Maybe String -> [String]
declareName String
i SBVType
t Maybe String
forall a. Maybe a
Nothing [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
declClosure
  where declClosure :: [String]
declClosure | Just String
external <- String -> [(String, String)] -> Maybe String
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup String
i [(String, String)]
progTransClosures
                    =  String -> SBVType -> Maybe String -> [String]
declareName String
external SBVType
t Maybe String
forall a. Maybe a
Nothing
                    [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> (String, String) -> Kind -> String
mkRelEq String
external (String
"transitive-closure", String
i) (SBVType -> Kind
argKind SBVType
t) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"]
                    | Bool
True
                    = []

        argKind :: SBVType -> Kind
argKind (SBVType [Kind
ka, Kind
_, Kind
KBool]) = Kind
ka
        argKind SBVType
_                        = String -> Kind
forall a. HasCallStack => String -> a
error (String -> Kind) -> String -> Kind
forall a b. (a -> b) -> a -> b
$ String
"declUI: Unexpected type for name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String, SBVType) -> String
forall a. Show a => a -> String
show (String
i, SBVType
t)

-- Note that even though we get all user defined-functions here (i.e., lambda and axiom), we can only have defined-functions
-- and axioms. We spit axioms as is; and topologically sort the definitions.
declUserFuns :: [(SMTDef, SBVType)] -> [String]
declUserFuns :: [(SMTDef, SBVType)] -> [String]
declUserFuns [(SMTDef, SBVType)]
ds
  | Bool -> Bool
not ([(SMTDef, SBVType)] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(SMTDef, SBVType)]
lambdas)
  = String -> [String]
forall a. HasCallStack => String -> a
error (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.declUserFuns: Unexpected anonymous functions in declDef:" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: ((SMTDef, SBVType) -> String) -> [(SMTDef, SBVType)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (SMTDef, SBVType) -> String
forall a. Show a => a -> String
show [(SMTDef, SBVType)]
lambdas
  | Bool
True
  = [(SMTDef, SBVType)] -> [String]
declFuncs [(SMTDef, SBVType)]
others
  where ([(SMTDef, SBVType)]
lambdas, [(SMTDef, SBVType)]
others) = ((SMTDef, SBVType) -> Bool)
-> [(SMTDef, SBVType)]
-> ([(SMTDef, SBVType)], [(SMTDef, SBVType)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (SMTDef -> Bool
isLam (SMTDef -> Bool)
-> ((SMTDef, SBVType) -> SMTDef) -> (SMTDef, SBVType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SMTDef, SBVType) -> SMTDef
forall a b. (a, b) -> a
fst) [(SMTDef, SBVType)]
ds
        isLam :: SMTDef -> Bool
isLam SMTLam{} = Bool
True
        isLam SMTDef{} = Bool
False

-- We need to topologically sort the user given definitions and axioms and put them in the proper order and construct.
-- Note that there are no anonymous functions at this level.
declFuncs :: [(SMTDef, SBVType)] -> [String]
declFuncs :: [(SMTDef, SBVType)] -> [String]
declFuncs [(SMTDef, SBVType)]
ds = (SCC (SMTDef, SBVType) -> String)
-> [SCC (SMTDef, SBVType)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SCC (SMTDef, SBVType) -> String
forall {a}. Show a => SCC (SMTDef, a) -> String
declGroup [SCC (SMTDef, SBVType)]
sorted
  where mkNode :: (SMTDef, b) -> ((SMTDef, b), String, [String])
mkNode (SMTDef, b)
d = ((SMTDef, b)
d, (SMTDef, b) -> String
forall {b}. (SMTDef, b) -> String
getKey (SMTDef, b)
d, (SMTDef, b) -> [String]
forall {b}. Show b => (SMTDef, b) -> [String]
getDeps (SMTDef, b)
d)

        getKey :: (SMTDef, b) -> String
getKey (SMTDef
d, b
_) = case SMTDef
d of
                         SMTDef String
n Kind
_ [String]
_ Maybe String
_ Int -> String
_ -> String
n
                         SMTLam{}         -> String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.declFuns: Unexpected definition kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SMTDef -> String
forall a. Show a => a -> String
show SMTDef
d

        getDeps :: (SMTDef, b) -> [String]
getDeps (SMTDef String
_ Kind
_ [String]
d Maybe String
_ Int -> String
_, b
_) = [String]
d
        getDeps (l :: SMTDef
l@SMTLam{}, b
t)       = String -> [String]
forall a. HasCallStack => String -> a
error (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.declFuns: Unexpected definition: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (SMTDef, b) -> String
forall a. Show a => a -> String
show (SMTDef
l, b
t)

        mkDecl :: Maybe String -> String -> String
mkDecl Maybe String
Nothing  String
rt = String
"() "    String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rt
        mkDecl (Just String
p) String
rt = String
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rt

        sorted :: [SCC (SMTDef, SBVType)]
sorted = [((SMTDef, SBVType), String, [String])] -> [SCC (SMTDef, SBVType)]
forall key node. Ord key => [(node, key, [key])] -> [SCC node]
DG.stronglyConnComp (((SMTDef, SBVType) -> ((SMTDef, SBVType), String, [String]))
-> [(SMTDef, SBVType)] -> [((SMTDef, SBVType), String, [String])]
forall a b. (a -> b) -> [a] -> [b]
map (SMTDef, SBVType) -> ((SMTDef, SBVType), String, [String])
forall {b}.
Show b =>
(SMTDef, b) -> ((SMTDef, b), String, [String])
mkNode [(SMTDef, SBVType)]
ds)

        declGroup :: SCC (SMTDef, a) -> String
declGroup (DG.AcyclicSCC (SMTDef, a)
b)  = Bool -> (SMTDef, a) -> String
forall {a}. Show a => Bool -> (SMTDef, a) -> String
declUserDef Bool
False (SMTDef, a)
b
        declGroup (DG.CyclicSCC  [(SMTDef, a)]
bs) = case [(SMTDef, a)]
bs of
                                         []  -> String -> String
forall a. HasCallStack => String -> a
error String
"Data.SBV.declFuns: Impossible happened: an empty cyclic group was returned!"
                                         [(SMTDef, a)
x] -> Bool -> (SMTDef, a) -> String
forall {a}. Show a => Bool -> (SMTDef, a) -> String
declUserDef Bool
True (SMTDef, a)
x
                                         [(SMTDef, a)]
xs  -> [(SMTDef, a)] -> String
forall {a}. Show a => [(SMTDef, a)] -> String
declUserDefMulti [(SMTDef, a)]
xs

        declUserDef :: Bool -> (SMTDef, a) -> String
declUserDef Bool
_ d :: (SMTDef, a)
d@(SMTLam{}, a
_) = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.declFuns: Unexpected anonymous lambda in user-defined functions: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (SMTDef, a) -> String
forall a. Show a => a -> String
show (SMTDef, a)
d
        declUserDef Bool
isRec (SMTDef String
nm Kind
fk [String]
deps Maybe String
param Int -> String
body, a
ty) = (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]
++ a -> String
forall a. Show a => a -> String
show a
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
recursive String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
frees String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
           where (String
recursive, String
definer) | Bool
isRec = (String
" [Recursive]", String
"define-fun-rec")
                                      | Bool
True  = (String
"",             String
"define-fun")

                 otherDeps :: [String]
otherDeps = (String -> Bool) -> [String] -> [String]
forall a. (a -> Bool) -> [a] -> [a]
filter (String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
nm) [String]
deps
                 frees :: String
frees | [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
otherDeps = String
""
                       | Bool
True           = String
" [Refers to: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
otherDeps String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"

                 decl :: String
decl = Maybe String -> String -> String
mkDecl Maybe String
param (Kind -> String
smtType Kind
fk)

                 s :: String
s = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
definer String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
decl 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
")"

        -- declare a bunch of mutually-recursive functions
        declUserDefMulti :: [(SMTDef, a)] -> String
declUserDefMulti [(SMTDef, a)]
bs = [([String], String, a, String, String)] -> String
forall {a}.
Show a =>
[([String], String, a, String, String)] -> String
render ([([String], String, a, String, String)] -> String)
-> [([String], String, a, String, String)] -> String
forall a b. (a -> b) -> a -> b
$ ((SMTDef, a) -> ([String], String, a, String, String))
-> [(SMTDef, a)] -> [([String], String, a, String, String)]
forall a b. (a -> b) -> [a] -> [b]
map (SMTDef, a) -> ([String], String, a, String, String)
forall {c}.
Show c =>
(SMTDef, c) -> ([String], String, c, String, String)
collect [(SMTDef, a)]
bs
          where collect :: (SMTDef, c) -> ([String], String, c, String, String)
collect d :: (SMTDef, c)
d@(SMTLam{}, c
_) = String -> ([String], String, c, String, String)
forall a. HasCallStack => String -> a
error (String -> ([String], String, c, String, String))
-> String -> ([String], String, c, String, String)
forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.declFuns: Unexpected lambda in user-defined mutual-recursion group: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (SMTDef, c) -> String
forall a. Show a => a -> String
show (SMTDef, c)
d
                collect (SMTDef String
nm Kind
fk [String]
deps Maybe String
param Int -> String
body, c
ty) = ([String]
deps, String
nm, c
ty, Char
'(' Char -> 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
decl String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")", Int -> String
body Int
3)
                  where decl :: String
decl = Maybe String -> String -> String
mkDecl Maybe String
param (Kind -> String
smtType Kind
fk)

                render :: [([String], String, a, String, String)] -> String
render [([String], String, a, String, String)]
defs = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
                                  [ String
"; " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String
n 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
ty | ([String]
_, String
n, a
ty, String
_, String
_) <- [([String], String, a, String, String)]
defs]
                                  , String
"(define-funs-rec"
                                  ]
                               [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ Int -> String
forall {a}. (Eq a, Num a) => a -> String
open Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([String], String, a, String, String) -> String
forall {a} {b} {c} {d} {e}. (a, b, c, d, e) -> d
param ([String], String, a, String, String)
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
close1 Int
i | (Int
i, ([String], String, a, String, String)
d) <- [Int]
-> [([String], String, a, String, String)]
-> [(Int, ([String], String, a, String, String))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] [([String], String, a, String, String)]
defs]
                               [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ Int -> String
forall {a}. (Eq a, Num a) => a -> String
open Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ ([String], String, a, String, String) -> String
forall {a} {d}.
Show a =>
([String], String, a, d, String) -> String
dump  ([String], String, a, String, String)
d String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
close2 Int
i | (Int
i, ([String], String, a, String, String)
d) <- [Int]
-> [([String], String, a, String, String)]
-> [(Int, ([String], String, a, String, String))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] [([String], String, a, String, String)]
defs]
                     where open :: a -> String
open a
1 = String
"  ("
                           open a
_ = String
"   "

                           param :: (a, b, c, d, e) -> d
param (a
_deps, b
_nm, c
_ty, d
p, e
_body) = d
p

                           dump :: ([String], String, a, d, String) -> String
dump ([String]
deps, String
nm, a
ty, d
_, String
body) = String
"; Definition of: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
ty String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
". [Refers to: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " [String]
deps String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]"
                                                        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
body

                           ld :: Int
ld = [([String], String, a, String, String)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [([String], String, a, String, String)]
defs

                           close1 :: Int -> String
close1 Int
n = if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ld then String
")"  else String
""
                           close2 :: Int -> String
close2 Int
n = if Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
ld then String
"))" else String
""

mkTable :: (((Int, Kind, Kind), [SV]), [String]) -> (String, [String])
mkTable :: (((Int, Kind, Kind), [SV]), [String]) -> (String, [String])
mkTable (((Int
i, Kind
ak, Kind
rk), [SV]
_elts), [String]
is) = (String
decl, (Int -> String -> String) -> [Int] -> [String] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> String -> String
wrap [(Int
0::Int)..] [String]
is [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
setup)
  where t :: String
t       = String
"table" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
        decl :: String
decl    = String
"(declare-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t 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]
++ Kind -> String
smtType Kind
rk String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        -- Arrange for initializers
        mkInit :: Int -> String
mkInit Int
idx   = String
"table" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_initializer_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
idx :: Int)
        initializer :: String
initializer  = String
"table" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_initializer"

        wrap :: Int -> String -> String
wrap Int
index String
s = String
"(define-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
mkInit Int
index String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" () Bool " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        lis :: Int
lis  = [String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
is

        setup :: [String]
setup
          | Int
lis Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0       = [ String
"(define-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
initializer String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" () Bool true) ; no initialization needed"
                             ]
          | Int
lis Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1       = [ String
"(define-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
initializer String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" () Bool " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
mkInit Int
0 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                             , String
"(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
initializer String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                             ]
          | Bool
True           = [ String
"(define-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
initializer String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" () Bool (and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
mkInit [Int
0..Int
lis Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
                             , String
"(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
initializer String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                             ]
nonConstTable :: (((Int, Kind, Kind), [SV]), [String]) -> String
nonConstTable :: (((Int, Kind, Kind), [SV]), [String]) -> String
nonConstTable (((Int
i, Kind
ak, Kind
rk), [SV]
_elts), [String]
_) = String
decl
  where t :: String
t    = String
"table" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
        decl :: String
decl = String
"(declare-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t 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]
++ Kind -> String
smtType Kind
rk String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

constructTables :: RoundingMode -> [(SV, CV)] -> [((Int, Kind, Kind), [SV])]
                -> ( IM.IntMap String                            -- table enumeration
                   , [(((Int, Kind, Kind), [SV]), [String])]     -- constant tables
                   , [(((Int, Kind, Kind), [SV]), [String])]     -- non-constant tables
                   )
constructTables :: RoundingMode
-> [(SV, CV)]
-> [((Int, Kind, Kind), [SV])]
-> (TableMap, [(((Int, Kind, Kind), [SV]), [String])],
    [(((Int, Kind, Kind), [SV]), [String])])
constructTables RoundingMode
rm [(SV, CV)]
consts [((Int, Kind, Kind), [SV])]
tbls = (TableMap
tableMap, [(((Int, Kind, Kind), [SV]), [String])]
constTables, [(((Int, Kind, Kind), [SV]), [String])]
nonConstTables)
 where allTables :: [(((Int, Kind, Kind), [SV]), Either [String] [String])]
allTables      = [(((Int, Kind, Kind), [SV])
t, RoundingMode
-> [SV] -> ((Int, Kind, Kind), [SV]) -> Either [String] [String]
genTableData RoundingMode
rm (((SV, CV) -> SV) -> [(SV, CV)] -> [SV]
forall a b. (a -> b) -> [a] -> [b]
map (SV, CV) -> SV
forall a b. (a, b) -> a
fst [(SV, CV)]
consts) ((Int, Kind, Kind), [SV])
t) | ((Int, Kind, Kind), [SV])
t <- [((Int, Kind, Kind), [SV])]
tbls]
       constTables :: [(((Int, Kind, Kind), [SV]), [String])]
constTables    = [(((Int, Kind, Kind), [SV])
t, [String]
d) | (((Int, Kind, Kind), [SV])
t, Left  [String]
d) <- [(((Int, Kind, Kind), [SV]), Either [String] [String])]
allTables]
       nonConstTables :: [(((Int, Kind, Kind), [SV]), [String])]
nonConstTables = [(((Int, Kind, Kind), [SV])
t, [String]
d) | (((Int, Kind, Kind), [SV])
t, Right [String]
d) <- [(((Int, Kind, Kind), [SV]), Either [String] [String])]
allTables]
       tableMap :: TableMap
tableMap       = [(Int, String)] -> TableMap
forall a. [(Int, a)] -> IntMap a
IM.fromList ([(Int, String)] -> TableMap) -> [(Int, String)] -> TableMap
forall a b. (a -> b) -> a -> b
$ ((((Int, Kind, Kind), [SV]), Either [String] [String])
 -> (Int, String))
-> [(((Int, Kind, Kind), [SV]), Either [String] [String])]
-> [(Int, String)]
forall a b. (a -> b) -> [a] -> [b]
map (((Int, Kind, Kind), [SV]), Either [String] [String])
-> (Int, String)
forall {a} {b} {c} {b} {b}.
Show a =>
(((a, b, c), b), b) -> (a, String)
grab [(((Int, Kind, Kind), [SV]), Either [String] [String])]
allTables

       grab :: (((a, b, c), b), b) -> (a, String)
grab (((a
t, b
_, c
_), b
_), b
_) = (a
t, String
"table" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
t)

-- Left if all constants, Right if otherwise
genTableData :: RoundingMode -> [SV] -> ((Int, Kind, Kind), [SV]) -> Either [String] [String]
genTableData :: RoundingMode
-> [SV] -> ((Int, Kind, Kind), [SV]) -> Either [String] [String]
genTableData RoundingMode
rm [SV]
consts ((Int
i, Kind
aknd, Kind
_), [SV]
elts)
  | [(Bool, (String, String))] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Bool, (String, String))]
post = [String] -> Either [String] [String]
forall a b. a -> Either a b
Left  (((Bool, (String, String)) -> String)
-> [(Bool, (String, String))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String, String) -> String
mkEntry ((String, String) -> String)
-> ((Bool, (String, String)) -> (String, String))
-> (Bool, (String, String))
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool, (String, String)) -> (String, String)
forall a b. (a, b) -> b
snd) [(Bool, (String, String))]
pre)
  | Bool
True      = [String] -> Either [String] [String]
forall a b. b -> Either a b
Right (((Bool, (String, String)) -> String)
-> [(Bool, (String, String))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String, String) -> String
mkEntry ((String, String) -> String)
-> ((Bool, (String, String)) -> (String, String))
-> (Bool, (String, String))
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool, (String, String)) -> (String, String)
forall a b. (a, b) -> b
snd) ([(Bool, (String, String))]
pre [(Bool, (String, String))]
-> [(Bool, (String, String))] -> [(Bool, (String, String))]
forall a. [a] -> [a] -> [a]
++ [(Bool, (String, String))]
post))
  where ([(Bool, (String, String))]
pre, [(Bool, (String, String))]
post) = ((Bool, (String, String)) -> Bool)
-> [(Bool, (String, String))]
-> ([(Bool, (String, String))], [(Bool, (String, String))])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Bool, (String, String)) -> Bool
forall a b. (a, b) -> a
fst ((SV -> Int -> (Bool, (String, String)))
-> [SV] -> [Int] -> [(Bool, (String, String))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SV -> Int -> (Bool, (String, String))
forall {p}. Integral p => SV -> p -> (Bool, (String, String))
mkElt [SV]
elts [(Int
0::Int)..])
        t :: String
t           = String
"table" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i

        mkElt :: SV -> p -> (Bool, (String, String))
mkElt SV
x p
k   = (Bool
isReady, (String
idx, SV -> String
cvtSV SV
x))
          where idx :: String
idx = RoundingMode -> CV -> String
cvtCV RoundingMode
rm (Kind -> p -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV Kind
aknd p
k)
                isReady :: Bool
isReady = SV
x SV -> Set SV -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set SV
constsSet

        mkEntry :: (String, String) -> String
mkEntry (String
idx, String
v) = String
"(= (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
idx String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        constsSet :: Set SV
constsSet = [SV] -> Set SV
forall a. Ord a => [a] -> Set a
Set.fromList [SV]
consts

svType :: SV -> String
svType :: SV -> String
svType SV
s = Kind -> String
smtType (SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
s)

svFunType :: [SV] -> SV -> String
svFunType :: [SV] -> SV -> String
svFunType [SV]
ss SV
s = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
svType [SV]
ss) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
svType SV
s

cvtType :: SBVType -> String
cvtType :: SBVType -> String
cvtType (SBVType []) = String -> String
forall a. HasCallStack => String -> a
error String
"SBV.SMT.SMTLib2.cvtType: internal: received an empty type!"
cvtType (SBVType [Kind]
xs) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Kind -> String) -> [Kind] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Kind -> String
smtType [Kind]
body) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
ret
  where ([Kind]
body, Kind
ret) = ([Kind] -> [Kind]
forall a. HasCallStack => [a] -> [a]
init [Kind]
xs, [Kind] -> Kind
forall a. HasCallStack => [a] -> a
last [Kind]
xs)

type TableMap = IM.IntMap String

-- Present an SV, simply show
cvtSV :: SV -> String
cvtSV :: SV -> String
cvtSV = SV -> String
forall a. Show a => a -> String
show

cvtCV :: RoundingMode -> CV -> String
cvtCV :: RoundingMode -> CV -> String
cvtCV = RoundingMode -> CV -> String
cvToSMTLib

getTable :: TableMap -> Int -> String
getTable :: TableMap -> Int -> String
getTable TableMap
m Int
i
  | Just String
tn <- Int
i Int -> TableMap -> Maybe String
forall a. Int -> IntMap a -> Maybe a
`IM.lookup` TableMap
m = String
tn
  | Bool
True                       = String
"table" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i  -- constant tables are always named this way

cvtExp :: SMTConfig -> ProgInfo -> SolverCapabilities -> RoundingMode -> TableMap -> SBVExpr -> String
cvtExp :: SMTConfig
-> ProgInfo
-> SolverCapabilities
-> RoundingMode
-> TableMap
-> SBVExpr
-> String
cvtExp SMTConfig
cfg ProgInfo
curProgInfo SolverCapabilities
caps RoundingMode
rm TableMap
tableMap expr :: SBVExpr
expr@(SBVApp Op
_ [SV]
arguments) = SBVExpr -> String
sh SBVExpr
expr
  where hasPB :: Bool
hasPB       = SolverCapabilities -> Bool
supportsPseudoBooleans SolverCapabilities
caps
        hasDistinct :: Bool
hasDistinct = SolverCapabilities -> Bool
supportsDistinct       SolverCapabilities
caps
        specialRels :: [SpecialRelOp]
specialRels = ProgInfo -> [SpecialRelOp]
progSpecialRels        ProgInfo
curProgInfo

        bvOp :: Bool
bvOp     = (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SV -> Bool
forall a. HasKind a => a -> Bool
isBounded   [SV]
arguments
        intOp :: Bool
intOp    = (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SV -> Bool
forall a. HasKind a => a -> Bool
isUnbounded [SV]
arguments
        ratOp :: Bool
ratOp    = (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SV -> Bool
forall a. HasKind a => a -> Bool
isRational  [SV]
arguments
        realOp :: Bool
realOp   = (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SV -> Bool
forall a. HasKind a => a -> Bool
isReal      [SV]
arguments
        fpOp :: Bool
fpOp     = (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\SV
a -> SV -> Bool
forall a. HasKind a => a -> Bool
isDouble SV
a Bool -> Bool -> Bool
|| SV -> Bool
forall a. HasKind a => a -> Bool
isFloat SV
a Bool -> Bool -> Bool
|| SV -> Bool
forall a. HasKind a => a -> Bool
isFP SV
a) [SV]
arguments
        boolOp :: Bool
boolOp   = (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SV -> Bool
forall a. HasKind a => a -> Bool
isBoolean   [SV]
arguments
        charOp :: Bool
charOp   = (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SV -> Bool
forall a. HasKind a => a -> Bool
isChar      [SV]
arguments
        stringOp :: Bool
stringOp = (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SV -> Bool
forall a. HasKind a => a -> Bool
isString    [SV]
arguments
        listOp :: Bool
listOp   = (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SV -> Bool
forall a. HasKind a => a -> Bool
isList      [SV]
arguments

        bad :: b
bad | Bool
intOp = String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMTLib2: Unsupported operation on unbounded integers: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVExpr -> String
forall a. Show a => a -> String
show SBVExpr
expr
            | Bool
True  = String -> b
forall a. HasCallStack => String -> a
error (String -> b) -> String -> b
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMTLib2: Unsupported operation on real values: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVExpr -> String
forall a. Show a => a -> String
show SBVExpr
expr

        ensureBVOrBool :: Bool
ensureBVOrBool = Bool
bvOp Bool -> Bool -> Bool
|| Bool
boolOp Bool -> Bool -> Bool
|| Bool
forall {b}. b
bad
        ensureBV :: Bool
ensureBV       = Bool
bvOp Bool -> Bool -> Bool
|| Bool
forall {b}. b
bad

        addRM :: String -> String
addRM String
s = String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RoundingMode -> String
smtRoundingMode RoundingMode
rm

        isZ3 :: Bool
isZ3 = case SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
cfg) of
                 Solver
Z3 -> Bool
True
                 Solver
_  -> Bool
False

        isCVC5 :: Bool
isCVC5 = case SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
cfg) of
                   Solver
CVC5 -> Bool
True
                   Solver
_    -> Bool
False

        hd :: String -> [a] -> a
hd String
_ (a
a:[a]
_) = a
a
        hd String
w []    = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"Impossible: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
": Received empty list of args!"

        -- lift a binary op
        lift2 :: String -> p -> [String] -> String
lift2  String
o p
_ [String
x, String
y] = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " 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
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        lift2  String
o p
_ [String]
sbvs   = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMTLib2.sh.lift2: Unexpected arguments: "   String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String, [String]) -> String
forall a. Show a => a -> String
show (String
o, [String]
sbvs)

        -- lift an arbitrary arity operator
        liftN :: String -> p -> [String] -> String
liftN String
o p
_ [String]
xs = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        -- lift a binary operation with rounding-mode added; used for floating-point arithmetic
        lift2WM :: String -> String -> p -> [String] -> String
lift2WM String
o String
fo | Bool
fpOp = String -> p -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift2 (String -> String
addRM String
fo)
                     | Bool
True = String -> p -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift2 String
o

        lift1FP :: String -> String -> p -> [String] -> String
lift1FP String
o String
fo | Bool
fpOp = String -> p -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift1 String
fo
                     | Bool
True = String -> p -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift1 String
o

        liftAbs :: Bool -> [String] -> String
liftAbs Bool
sgned [String]
args | Bool
fpOp        = String -> Bool -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift1 String
"fp.abs" Bool
sgned [String]
args
                           | Bool
intOp       = String -> Bool -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift1 String
"abs"    Bool
sgned [String]
args
                           | Bool
bvOp, Bool
sgned = String -> String -> String -> String
mkAbs String
fArg String
"bvslt" String
"bvneg"
                           | Bool
bvOp        = String
fArg
                           | Bool
True        = String -> String -> String -> String
mkAbs String
fArg String
"<"     String
"-"
          where fArg :: String
fArg = String -> [String] -> String
forall {a}. String -> [a] -> a
hd String
"liftAbs" [String]
args
                mkAbs :: String -> String -> String -> String
mkAbs String
x String
cmp String
neg = String
"(ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ltz String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nx String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                  where ltz :: String
ltz = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cmp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " 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
z String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                        nx :: String
nx  = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
neg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                        z :: String
z   = RoundingMode -> CV -> String
cvtCV RoundingMode
rm (Kind -> Integer -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV (SV -> Kind
forall a. HasKind a => a -> Kind
kindOf (String -> [SV] -> SV
forall {a}. String -> [a] -> a
hd String
"liftAbs.arguments" [SV]
arguments)) (Integer
0::Integer))

        lift2B :: String -> String -> p -> [String] -> String
lift2B String
bOp String
vOp
          | Bool
boolOp = String -> p -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift2 String
bOp
          | Bool
True   = String -> p -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift2 String
vOp

        lift1B :: String -> String -> p -> [String] -> String
lift1B String
bOp String
vOp
          | Bool
boolOp = String -> p -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift1 String
bOp
          | Bool
True   = String -> p -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift1 String
vOp

        eqBV :: p -> [String] -> String
eqBV  = String -> p -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift2 String
"="
        neqBV :: p -> [String] -> String
neqBV = String -> p -> [String] -> String
forall {p}. String -> p -> [String] -> String
liftN String
"distinct"

        equal :: p -> [String] -> String
equal p
sgn [String]
sbvs
          | Bool
fpOp = String -> p -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift2 String
"fp.eq" p
sgn [String]
sbvs
          | Bool
True = String -> p -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift2 String
"="     p
sgn [String]
sbvs

        -- Do not use distinct on floats; because +0/-0, and NaNs mess
        -- up the meaning. Just go with reqular equals.
        notEqual :: p -> [String] -> String
notEqual p
sgn [String]
sbvs
          | Bool
fpOp Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
hasDistinct = [String] -> String
liftP [String]
sbvs
          | Bool
True                    = String -> p -> [String] -> String
forall {p}. String -> p -> [String] -> String
liftN String
"distinct" p
sgn [String]
sbvs
          where liftP :: [String] -> String
liftP xs :: [String]
xs@[String
_, String
_] = String
"(not " String -> String -> String
forall a. [a] -> [a] -> [a]
++ p -> [String] -> String
forall {p}. p -> [String] -> String
equal p
sgn [String]
xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                liftP [String]
args      = String
"(and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ([String] -> [String]
walk [String]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

                walk :: [String] -> [String]
walk []     = []
                walk (String
e:[String]
es) = (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\String
e' -> [String] -> String
liftP [String
e, String
e']) [String]
es [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String] -> [String]
walk [String]
es

        lift2S :: String -> String -> Bool -> [String] -> String
lift2S String
oU String
oS Bool
sgn = String -> Bool -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift2 (if Bool
sgn then String
oS else String
oU) Bool
sgn
        liftNS :: String -> String -> Bool -> [String] -> String
liftNS String
oU String
oS Bool
sgn = String -> Bool -> [String] -> String
forall {p}. String -> p -> [String] -> String
liftN (if Bool
sgn then String
oS else String
oU) Bool
sgn

        lift2Cmp :: String -> String -> p -> [String] -> String
lift2Cmp String
o String
fo | Bool
fpOp = String -> p -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift2 String
fo
                      | Bool
True = String -> p -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift2 String
o

        unintComp :: String -> [String] -> String
unintComp String
o [String
a, String
b]
          | KUserSort String
s (Just [String]
_) <- SV -> Kind
forall a. HasKind a => a -> Kind
kindOf (String -> [SV] -> SV
forall {a}. String -> [a] -> a
hd String
"unintComp" [SV]
arguments)
          = let idx :: String -> String
idx String
v = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_constrIndex " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" in String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
idx String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
idx String
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        unintComp String
o [String]
sbvs = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.sh.unintComp: Unexpected arguments: "   String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String, [String], [Kind]) -> String
forall a. Show a => a -> String
show (String
o, [String]
sbvs, (SV -> Kind) -> [SV] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Kind
forall a. HasKind a => a -> Kind
kindOf [SV]
arguments)

        stringOrChar :: Kind -> Bool
stringOrChar Kind
KString = Bool
True
        stringOrChar Kind
KChar   = Bool
True
        stringOrChar Kind
_       = Bool
False
        stringCmp :: Bool -> String -> [String] -> String
stringCmp Bool
swap String
o [String
a, String
b]
          | Kind -> Bool
stringOrChar (SV -> Kind
forall a. HasKind a => a -> Kind
kindOf (String -> [SV] -> SV
forall {a}. String -> [a] -> a
hd String
"stringCmp" [SV]
arguments))
          = let (String
a1, String
a2) | Bool
swap = (String
b, String
a)
                         | Bool
True = (String
a, String
b)
            in String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        stringCmp Bool
_ String
o [String]
sbvs = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.sh.stringCmp: Unexpected arguments: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String, [String]) -> String
forall a. Show a => a -> String
show (String
o, [String]
sbvs)

        -- NB. Likewise for sequences
        seqCmp :: Bool -> String -> [String] -> String
seqCmp Bool
swap String
o [String
a, String
b]
          | KList{} <- SV -> Kind
forall a. HasKind a => a -> Kind
kindOf (String -> [SV] -> SV
forall {a}. String -> [a] -> a
hd String
"seqCmp" [SV]
arguments)
          = let (String
a1, String
a2) | Bool
swap = (String
b, String
a)
                         | Bool
True = (String
a, String
b)
            in String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        seqCmp Bool
_ String
o [String]
sbvs = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.sh.seqCmp: Unexpected arguments: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String, [String]) -> String
forall a. Show a => a -> String
show (String
o, [String]
sbvs)

        lift1 :: String -> p -> [String] -> String
lift1  String
o p
_ [String
x]    = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        lift1  String
o p
_ [String]
sbvs   = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.sh.lift1: Unexpected arguments: "   String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String, [String]) -> String
forall a. Show a => a -> String
show (String
o, [String]
sbvs)

        -- We fully qualify the constructor with their types to work around type checking issues
        -- Note that this is rather bizarre, as we're tagging the constructor with its *result* type,
        -- not its full function type as one would expect. But this is per the spec: Pg. 27 of SMTLib 2.6 spec
        -- says:
        --
        --    To simplify sort checking, a function symbol in a term can be annotated with one of its result sorts sigma.
        --
        -- I wish it was the full type here not just the result, but we go with the spec. Also see: <http://github.com/Z3Prover/z3/issues/2135>
        -- and in particular <http://github.com/Z3Prover/z3/issues/2135#issuecomment-477636435>
        dtConstructor :: String -> [SV] -> Kind -> String
dtConstructor String
fld [SV]
args Kind
res = String
"((as " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fld String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        -- Similarly, we fully qualify the accessors with their types to work around type checking issues
        -- Unfortunately, z3 and CVC4 are behaving differently, so we tie this ascription to a solver capability.
        dtAccessor :: String -> [Kind] -> Kind -> String
dtAccessor String
fld [Kind]
params Kind
res
           | SolverCapabilities -> Bool
supportsDirectAccessors SolverCapabilities
caps = String
dResult
           | Bool
True                         = String
aResult
          where dResult :: String
dResult = String
"(_ is " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fld String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                ps :: String
ps      = String
" (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Kind -> String) -> [Kind] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Kind -> String
smtType [Kind]
params) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") "
                aResult :: String
aResult = String
"(_ is (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fld String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ps String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"

        firstifiedName :: Op -> String
firstifiedName = Int -> Op -> String
firstify (KDOptions -> Int
firstifyUniqueLen (SMTConfig -> KDOptions
kdOptions SMTConfig
cfg))

        sh :: SBVExpr -> String
sh (SBVApp Op
Ite [SV
a, SV
b, SV
c]) = String
"(ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        sh (SBVApp (LkUp (Int
t, Kind
aKnd, Kind
_, Int
l) SV
i SV
e) [])
          | Bool
needsCheck = String
"(ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cond String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
lkUp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
          | Bool
True       = String
lkUp
          where needsCheck :: Bool
needsCheck = case Kind
aKnd of
                              Kind
KBool         -> (Integer
2::Integer) Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l
                              KBounded Bool
_ Int
n  -> (Integer
2::Integer)Integer -> Int -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^Int
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
l
                              Kind
KUnbounded    -> Bool
True
                              KUserSort String
s Maybe [String]
_ -> String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
                              Kind
KReal         -> String -> Bool
forall a. HasCallStack => String -> a
error String
"SBV.SMT.SMTLib2.cvtExp: unexpected real valued index"
                              Kind
KFloat        -> String -> Bool
forall a. HasCallStack => String -> a
error String
"SBV.SMT.SMTLib2.cvtExp: unexpected float valued index"
                              Kind
KDouble       -> String -> Bool
forall a. HasCallStack => String -> a
error String
"SBV.SMT.SMTLib2.cvtExp: unexpected double valued index"
                              KFP{}         -> String -> Bool
forall a. HasCallStack => String -> a
error String
"SBV.SMT.SMTLib2.cvtExp: unexpected arbitrary float valued index"
                              KRational{}   -> String -> Bool
forall a. HasCallStack => String -> a
error String
"SBV.SMT.SMTLib2.cvtExp: unexpected rational valued index"
                              Kind
KChar         -> String -> Bool
forall a. HasCallStack => String -> a
error String
"SBV.SMT.SMTLib2.cvtExp: unexpected char valued index"
                              Kind
KString       -> String -> Bool
forall a. HasCallStack => String -> a
error String
"SBV.SMT.SMTLib2.cvtExp: unexpected string valued index"
                              KList Kind
k       -> String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: unexpected list valued: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
                              KSet  Kind
k       -> String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: unexpected set valued: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
                              KTuple [Kind]
k      -> String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: unexpected tuple valued: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Kind] -> String
forall a. Show a => a -> String
show [Kind]
k
                              KMaybe Kind
k      -> String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: unexpected maybe valued: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
                              KEither Kind
k1 Kind
k2 -> String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: unexpected sum valued: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Kind, Kind) -> String
forall a. Show a => a -> String
show (Kind
k1, Kind
k2)
                              KArray  Kind
k1 Kind
k2 -> String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: unexpected array valued: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Kind, Kind) -> String
forall a. Show a => a -> String
show (Kind
k1, Kind
k2)

                lkUp :: String
lkUp = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ TableMap -> Int -> String
getTable TableMap
tableMap Int
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

                cond :: String
cond
                 | SV -> Bool
forall a. HasKind a => a -> Bool
hasSign SV
i = String
"(or " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
le0 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
gtl String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") "
                 | Bool
True      = String
gtl String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "

                (String
less, String
leq) = case Kind
aKnd of
                                Kind
KBool         -> String -> (String, String)
forall a. HasCallStack => String -> a
error String
"SBV.SMT.SMTLib2.cvtExp: unexpected boolean valued index"
                                KBounded{}    -> if SV -> Bool
forall a. HasKind a => a -> Bool
hasSign SV
i then (String
"bvslt", String
"bvsle") else (String
"bvult", String
"bvule")
                                Kind
KUnbounded    -> (String
"<", String
"<=")
                                Kind
KReal         -> (String
"<", String
"<=")
                                Kind
KFloat        -> (String
"fp.lt", String
"fp.leq")
                                Kind
KDouble       -> (String
"fp.lt", String
"fp.leq")
                                Kind
KRational     -> (String
"sbv.rat.lt", String
"sbv.rat.leq")
                                KFP{}         -> (String
"fp.lt", String
"fp.leq")
                                Kind
KChar         -> String -> (String, String)
forall a. HasCallStack => String -> a
error String
"SBV.SMT.SMTLib2.cvtExp: unexpected string valued index"
                                Kind
KString       -> String -> (String, String)
forall a. HasCallStack => String -> a
error String
"SBV.SMT.SMTLib2.cvtExp: unexpected string valued index"
                                KUserSort String
s Maybe [String]
_ -> String -> (String, String)
forall a. HasCallStack => String -> a
error (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
                                KList Kind
k       -> String -> (String, String)
forall a. HasCallStack => String -> a
error (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: unexpected sequence valued index: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
                                KSet  Kind
k       -> String -> (String, String)
forall a. HasCallStack => String -> a
error (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: unexpected set valued index: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
                                KTuple [Kind]
k      -> String -> (String, String)
forall a. HasCallStack => String -> a
error (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: unexpected tuple valued index: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Kind] -> String
forall a. Show a => a -> String
show [Kind]
k
                                KMaybe Kind
k      -> String -> (String, String)
forall a. HasCallStack => String -> a
error (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: unexpected maybe valued index: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
k
                                KEither Kind
k1 Kind
k2 -> String -> (String, String)
forall a. HasCallStack => String -> a
error (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: unexpected sum valued index: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Kind, Kind) -> String
forall a. Show a => a -> String
show (Kind
k1, Kind
k2)
                                KArray  Kind
k1 Kind
k2 -> String -> (String, String)
forall a. HasCallStack => String -> a
error (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: unexpected array valued index: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Kind, Kind) -> String
forall a. Show a => a -> String
show (Kind
k1, Kind
k2)

                mkCnst :: Int -> String
mkCnst = RoundingMode -> CV -> String
cvtCV RoundingMode
rm (CV -> String) -> (Int -> CV) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Int -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV (SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
i)
                le0 :: String
le0  = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
less String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
mkCnst Int
0 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                gtl :: String
gtl  = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
leq  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
mkCnst Int
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        sh (SBVApp (KindCast Kind
f Kind
t) [SV
a]) = Kind -> Kind -> String -> String
handleKindCast Kind
f Kind
t (SV -> String
cvtSV SV
a)

        sh (SBVApp (ArrayLambda SMTLambda
s) [])        = SMTLambda -> String
forall a. Show a => a -> String
show SMTLambda
s
        sh (SBVApp Op
ReadArray       [SV
a, SV
i])    = String
"(select " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp Op
WriteArray      [SV
a, SV
i, SV
e]) = String
"(store "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        sh (SBVApp (Uninterpreted String
nm) [])   = String
nm
        sh (SBVApp (Uninterpreted String
nm) [SV]
args) = 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] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        sh (SBVApp (QuantifiedBool String
i) [])   = String
i
        sh (SBVApp (QuantifiedBool String
i) [SV]
args) = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: unexpected arguments to quantified boolean: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String, [SV]) -> String
forall a. Show a => a -> String
show (String
i, [SV]
args)

        sh a :: SBVExpr
a@(SBVApp (SpecialRelOp Kind
k SpecialRelOp
o) [SV]
args)
          | Bool -> Bool
not ([SV] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
args)
          = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: unexpected arguments to special op: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVExpr -> String
forall a. Show a => a -> String
show SBVExpr
a
          | Bool
True
          = let order :: Int
order = case SpecialRelOp
o SpecialRelOp -> [SpecialRelOp] -> Maybe Int
forall a. Eq a => a -> [a] -> Maybe Int
`elemIndex` [SpecialRelOp]
specialRels of
                          Just Int
i -> Int
i
                          Maybe Int
Nothing -> String -> Int
forall a. HasCallStack => String -> a
error (String -> Int) -> String -> Int
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"SBV.SMT.SMTLib2.cvtExp: Cannot find " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SpecialRelOp -> String
forall a. Show a => a -> String
show SpecialRelOp
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" in the special-relations list."
                                                     , String
"Known relations: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((SpecialRelOp -> String) -> [SpecialRelOp] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SpecialRelOp -> String
forall a. Show a => a -> String
show [SpecialRelOp]
specialRels)
                                                     ]
                asrt :: String -> String -> String
asrt String
nm String
fun = String -> (String, String) -> Kind -> String
mkRelEq String
nm (String
fun, Int -> String
forall a. Show a => a -> String
show Int
order) Kind
k
            in case SpecialRelOp
o of
                 IsPartialOrder         String
nm -> String -> String -> String
asrt String
nm String
"partial-order"
                 IsLinearOrder          String
nm -> String -> String -> String
asrt String
nm String
"linear-order"
                 IsTreeOrder            String
nm -> String -> String -> String
asrt String
nm String
"tree-order"
                 IsPiecewiseLinearOrder String
nm -> String -> String -> String
asrt String
nm String
"piecewise-linear-order"

        sh (SBVApp (Divides Integer
n) [SV
a]) = String
"((_ divisible " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        sh (SBVApp (Extract Int
i Int
j) [SV
a]) | Bool
ensureBV = String
"((_ extract " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
j String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        sh (SBVApp (Rol Int
i) [SV
a])
           | Bool
bvOp  = String -> Int -> SV -> String
rot String
"rotate_left"  Int
i SV
a
           | Bool
True  = String
forall {b}. b
bad

        sh (SBVApp (Ror Int
i) [SV
a])
           | Bool
bvOp  = String -> Int -> SV -> String
rot  String
"rotate_right" Int
i SV
a
           | Bool
True  = String
forall {b}. b
bad

        sh (SBVApp Op
Shl [SV
a, SV
i])
           | Bool
bvOp   = String -> String -> SV -> SV -> String
shft String
"bvshl"  String
"bvshl" SV
a SV
i
           | Bool
True   = String
forall {b}. b
bad

        sh (SBVApp Op
Shr [SV
a, SV
i])
           | Bool
bvOp  = String -> String -> SV -> SV -> String
shft String
"bvlshr" String
"bvashr" SV
a SV
i
           | Bool
True  = String
forall {b}. b
bad

        sh (SBVApp (ZeroExtend Int
i) [SV
a])
          | Bool
bvOp = String
"((_ zero_extend " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
          | Bool
True = String
forall {b}. b
bad

        sh (SBVApp (SignExtend Int
i) [SV
a])
          | Bool
bvOp = String
"((_ sign_extend " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
          | Bool
True = String
forall {b}. b
bad

        sh (SBVApp Op
op [SV]
args)
          | Just Bool -> [String] -> String
f <- Op
-> [(Op, Bool -> [String] -> String)]
-> Maybe (Bool -> [String] -> String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, Bool -> [String] -> String)]
forall {p}. [(Op, p -> [String] -> String)]
smtBVOpTable, Bool
ensureBVOrBool
          = Bool -> [String] -> String
f ((SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SV -> Bool
forall a. HasKind a => a -> Bool
hasSign [SV]
args) ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args)
          where -- The first 4 operators below do make sense for Integer's in Haskell, but there's
                -- no obvious counterpart for them in the SMTLib translation.
                -- TODO: provide support for these.
                smtBVOpTable :: [(Op, p -> [String] -> String)]
smtBVOpTable = [ (Op
And,  String -> String -> p -> [String] -> String
forall {p}. String -> String -> p -> [String] -> String
lift2B String
"and" String
"bvand")
                               , (Op
Or,   String -> String -> p -> [String] -> String
forall {p}. String -> String -> p -> [String] -> String
lift2B String
"or"  String
"bvor")
                               , (Op
XOr,  String -> String -> p -> [String] -> String
forall {p}. String -> String -> p -> [String] -> String
lift2B String
"xor" String
"bvxor")
                               , (Op
Not,  String -> String -> p -> [String] -> String
forall {p}. String -> String -> p -> [String] -> String
lift1B String
"not" String
"bvnot")
                               , (Op
Join, String -> p -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift2 String
"concat")
                               ]

        sh (SBVApp (Label String
_) [SV
a]) = SV -> String
cvtSV SV
a  -- This won't be reached; but just in case!

        sh (SBVApp (IEEEFP (FP_Cast Kind
kFrom Kind
kTo SV
m)) [SV]
args) = Kind -> Kind -> String -> String -> String
handleFPCast Kind
kFrom Kind
kTo (SV -> String
cvtSV SV
m) ([String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args))
        sh (SBVApp (IEEEFP FPOp
w                    ) [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FPOp -> String
forall a. Show a => a -> String
show FPOp
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        -- Some non-linear operators are supported by z3/CVC5 specifically, so do the custom translation Otherwise
        -- we pass them along.
        sh (SBVApp (NonLinear NROp
NR_Sqrt) [SV
a])    | Bool
isZ3   = String
"(^ "    String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" 0.5)"
                                               | Bool
isCVC5 = String
"(sqrt " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
a String -> String -> String
forall a. [a] -> [a] -> [a]
++     String
")"

        sh (SBVApp (NonLinear NROp
NR_Pow)  [SV
a, SV
b]) | Bool
isZ3 Bool -> Bool -> Bool
|| Bool
isCVC5  = String
"(^  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        sh (SBVApp (NonLinear NROp
w) [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NROp -> String
forall a. Show a => a -> String
show NROp
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        sh (SBVApp (PseudoBoolean PBOp
pb) [SV]
args)
          | Bool
hasPB = PBOp -> [String] -> String
handlePB PBOp
pb [String]
args'
          | Bool
True  = PBOp -> [String] -> String
reducePB PBOp
pb [String]
args'
          where args' :: [String]
args' = (SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args

        sh (SBVApp (OverflowOp OvOp
op) [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ OvOp -> String
forall a. Show a => a -> String
show OvOp
op String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        -- Note the unfortunate reversal in StrInRe..
        sh (SBVApp (StrOp (StrInRe RegExp
r)) [SV]
args) = String
"(str.in.re " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RegExp -> String
regExpToSMTString RegExp
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        -- StrUnit is no-op, since a character in SMTLib is the same as a string
        sh (SBVApp (StrOp StrOp
StrUnit)     [SV
a])  = SV -> String
cvtSV SV
a
        sh (SBVApp (StrOp StrOp
op)          [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ StrOp -> String
forall a. Show a => a -> String
show StrOp
op String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        sh (SBVApp (RegExOp o :: RegExOp
o@RegExEq{})  []) = RegExOp -> String
forall a. Show a => a -> String
show RegExOp
o
        sh (SBVApp (RegExOp o :: RegExOp
o@RegExNEq{}) []) = RegExOp -> String
forall a. Show a => a -> String
show RegExOp
o

        -- Reverse and higher order functions are special
        sh (SBVApp o :: Op
o@(SeqOp SBVReverse{})   [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
firstifiedName Op
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp o :: Op
o@(SeqOp SBVZip{})       [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
firstifiedName Op
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp o :: Op
o@(SeqOp SBVZipWith{})   [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
firstifiedName Op
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp o :: Op
o@(SeqOp SBVPartition{}) [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
firstifiedName Op
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp o :: Op
o@(SeqOp SBVReverse{})   [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
firstifiedName Op
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp o :: Op
o@(SeqOp SBVMap{})       [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
firstifiedName Op
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp o :: Op
o@(SeqOp SBVFoldl{})     [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
firstifiedName Op
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp o :: Op
o@(SeqOp SBVFoldr{})     [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
firstifiedName Op
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp o :: Op
o@(SeqOp SBVFilter{})    [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
firstifiedName Op
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp o :: Op
o@(SeqOp SBVAll{} )      [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
firstifiedName Op
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp o :: Op
o@(SeqOp SBVAny{} )      [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
firstifiedName Op
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp o :: Op
o@(SeqOp SBVConcat{})    [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
firstifiedName Op
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        sh (SBVApp (SeqOp SeqOp
op) [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SeqOp -> String
forall a. Show a => a -> String
show SeqOp
op String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        sh (SBVApp (SetOp SetOp
SetEqual)      [SV]
args)   = String
"(= "      String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp (SetOp SetOp
SetMember)     [SV
e, SV
s]) = String
"(select " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp (SetOp SetOp
SetInsert)     [SV
e, SV
s]) = String
"(store "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" true)"
        sh (SBVApp (SetOp SetOp
SetDelete)     [SV
e, SV
s]) = String
"(store "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" false)"
        sh (SBVApp (SetOp SetOp
SetIntersect)  [SV]
args)   = String
"(intersection " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp (SetOp SetOp
SetUnion)      [SV]
args)   = String
"(union "        String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp (SetOp SetOp
SetSubset)     [SV]
args)   = String
"(subset "       String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp (SetOp SetOp
SetDifference) [SV]
args)   = String
"(setminus "     String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp (SetOp SetOp
SetComplement) [SV]
args)   = String
"(complement "   String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        sh (SBVApp (TupleConstructor Int
0)   [])    = String
"mkSBVTuple0"
        sh (SBVApp (TupleConstructor Int
n)   [SV]
args)  = String
"((as mkSBVTuple" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType ([Kind] -> Kind
KTuple ((SV -> Kind) -> [SV] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Kind
forall a. HasKind a => a -> Kind
kindOf [SV]
args)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp (TupleAccess      Int
i Int
n) [SV
tup]) = String
"(proj_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_SBVTuple" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
tup String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        sh (SBVApp (EitherConstructor Kind
k1 Kind
k2 Bool
False) [SV
arg]) =       String -> [SV] -> Kind -> String
dtConstructor String
"left_SBVEither"  [SV
arg] (Kind -> Kind -> Kind
KEither Kind
k1 Kind
k2)
        sh (SBVApp (EitherConstructor Kind
k1 Kind
k2 Bool
True ) [SV
arg]) =       String -> [SV] -> Kind -> String
dtConstructor String
"right_SBVEither" [SV
arg] (Kind -> Kind -> Kind
KEither Kind
k1 Kind
k2)
        sh (SBVApp (EitherIs          Kind
k1 Kind
k2 Bool
False) [SV
arg]) = Char
'(' Char -> String -> String
forall a. a -> [a] -> [a]
: String -> [Kind] -> Kind -> String
dtAccessor    String
"left_SBVEither"  [Kind
k1]  (Kind -> Kind -> Kind
KEither Kind
k1 Kind
k2) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp (EitherIs          Kind
k1 Kind
k2 Bool
True ) [SV
arg]) = Char
'(' Char -> String -> String
forall a. a -> [a] -> [a]
: String -> [Kind] -> Kind -> String
dtAccessor    String
"right_SBVEither" [Kind
k2]  (Kind -> Kind -> Kind
KEither Kind
k1 Kind
k2) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp (EitherAccess            Bool
False) [SV
arg]) = String
"(get_left_SBVEither "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp (EitherAccess            Bool
True ) [SV
arg]) = String
"(get_right_SBVEither " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        sh (SBVApp  Op
RationalConstructor    [SV
t, SV
b]) = String
"(SBV.Rational " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        sh (SBVApp (MaybeConstructor Kind
k Bool
False) [])    =       String -> [SV] -> Kind -> String
dtConstructor String
"nothing_SBVMaybe" []    (Kind -> Kind
KMaybe Kind
k)
        sh (SBVApp (MaybeConstructor Kind
k Bool
True)  [SV
arg]) =       String -> [SV] -> Kind -> String
dtConstructor String
"just_SBVMaybe"    [SV
arg] (Kind -> Kind
KMaybe Kind
k)
        sh (SBVApp (MaybeIs          Kind
k Bool
False) [SV
arg]) = Char
'(' Char -> String -> String
forall a. a -> [a] -> [a]
: String -> [Kind] -> Kind -> String
dtAccessor    String
"nothing_SBVMaybe" []    (Kind -> Kind
KMaybe Kind
k) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp (MaybeIs          Kind
k Bool
True ) [SV
arg]) = Char
'(' Char -> String -> String
forall a. a -> [a] -> [a]
: String -> [Kind] -> Kind -> String
dtAccessor    String
"just_SBVMaybe"    [Kind
k]   (Kind -> Kind
KMaybe Kind
k) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp Op
MaybeAccess                [SV
arg]) = String
"(get_just_SBVMaybe " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        sh (SBVApp Op
Implies [SV
a, SV
b]) = String
"(=> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        sh inp :: SBVExpr
inp@(SBVApp Op
op [SV]
args)
          | Bool
intOp, Just Bool -> [String] -> String
f <- Op
-> [(Op, Bool -> [String] -> String)]
-> Maybe (Bool -> [String] -> String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, Bool -> [String] -> String)]
smtOpIntTable
          = Bool -> [String] -> String
f Bool
True ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args)
          | Bool
boolOp, Just [String] -> String
f <- Op -> [(Op, [String] -> String)] -> Maybe ([String] -> String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, [String] -> String)]
boolComps
          = [String] -> String
f ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args)
          | Bool
bvOp, Just Bool -> [String] -> String
f <- Op
-> [(Op, Bool -> [String] -> String)]
-> Maybe (Bool -> [String] -> String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, Bool -> [String] -> String)]
smtOpBVTable
          = Bool -> [String] -> String
f ((SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SV -> Bool
forall a. HasKind a => a -> Bool
hasSign [SV]
args) ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args)
          | Bool
realOp, Just Bool -> [String] -> String
f <- Op
-> [(Op, Bool -> [String] -> String)]
-> Maybe (Bool -> [String] -> String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, Bool -> [String] -> String)]
smtOpRealTable
          = Bool -> [String] -> String
f ((SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SV -> Bool
forall a. HasKind a => a -> Bool
hasSign [SV]
args) ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args)
          | Bool
ratOp, Just [String] -> String
f <- Op -> [(Op, [String] -> String)] -> Maybe ([String] -> String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, [String] -> String)]
ratOpTable
          = [String] -> String
f ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args)
          | Bool
fpOp, Just Bool -> [String] -> String
f <- Op
-> [(Op, Bool -> [String] -> String)]
-> Maybe (Bool -> [String] -> String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, Bool -> [String] -> String)]
smtOpFloatDoubleTable
          = Bool -> [String] -> String
f ((SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SV -> Bool
forall a. HasKind a => a -> Bool
hasSign [SV]
args) ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args)
          | Bool
charOp Bool -> Bool -> Bool
|| Bool
stringOp, Just [String] -> String
f <- Op -> [(Op, [String] -> String)] -> Maybe ([String] -> String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, [String] -> String)]
smtStringTable
          = [String] -> String
f ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args)
          | Bool
listOp, Just [String] -> String
f <- Op -> [(Op, [String] -> String)] -> Maybe ([String] -> String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, [String] -> String)]
smtListTable
          = [String] -> String
f ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args)
          | Just [String] -> String
f <- Op -> [(Op, [String] -> String)] -> Maybe ([String] -> String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, [String] -> String)]
uninterpretedTable
          = [String] -> String
f ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
cvtSV [SV]
args)
          | Bool
True
          = if Bool -> Bool
not ([SV] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
args) Bool -> Bool -> Bool
&& SV -> Bool
forall a. HasKind a => a -> Bool
isUserSort (String -> [SV] -> SV
forall {a}. String -> [a] -> a
hd String
"isUserSort" [SV]
args)
            then String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                 , String
"*** Cannot translate operator        : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
forall a. Show a => a -> String
show Op
op
                                 , String
"*** When applied to arguments of kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ([String] -> [String]
forall a. Eq a => [a] -> [a]
nub ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Kind -> String
forall a. Show a => a -> String
show (Kind -> String) -> (SV -> Kind) -> SV -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SV -> Kind
forall a. HasKind a => a -> Kind
kindOf) [SV]
args))
                                 , String
"*** Found as part of the expression  : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVExpr -> String
forall a. Show a => a -> String
show SBVExpr
inp
                                 , String
"***"
                                 , String
"*** Note that uninterpreted kinds only support equality."
                                 , String
"*** If you believe this is in error, please report!"
                                 ]
            else String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                 , String
"*** SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVExpr -> String
forall a. Show a => a -> String
show SBVExpr
inp
                                 , String
"***"
                                 , String
"*** Applied to arguments of type: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ([String] -> [String]
forall a. Eq a => [a] -> [a]
nub ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Kind -> String
forall a. Show a => a -> String
show (Kind -> String) -> (SV -> Kind) -> SV -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SV -> Kind
forall a. HasKind a => a -> Kind
kindOf) [SV]
args))
                                 , String
"***"
                                 , String
"*** This can happen if the Num instance isn't properly defined for a lifted kind."
                                 , String
"*** (See https://github.com/LeventErkok/sbv/issues/698 for a discussion.)"
                                 , String
"***"
                                 , String
"*** If you believe this is in error, please report!"
                                 ]
          where smtOpBVTable :: [(Op, Bool -> [String] -> String)]
smtOpBVTable  = [ (Op
Plus,          String -> Bool -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift2   String
"bvadd")
                                , (Op
Minus,         String -> Bool -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift2   String
"bvsub")
                                , (Op
Times,         String -> Bool -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift2   String
"bvmul")
                                , (Op
UNeg,          String -> String -> Bool -> [String] -> String
forall {p}. String -> String -> p -> [String] -> String
lift1B  String
"not"    String
"bvneg")
                                , (Op
Abs,           Bool -> [String] -> String
liftAbs)
                                , (Op
Quot,          String -> String -> Bool -> [String] -> String
lift2S  String
"bvudiv" String
"bvsdiv")
                                , (Op
Rem,           String -> String -> Bool -> [String] -> String
lift2S  String
"bvurem" String
"bvsrem")
                                , (Op
Equal,         Bool -> [String] -> String
forall {p}. p -> [String] -> String
eqBV)
                                , (Op
NotEqual,      Bool -> [String] -> String
forall {p}. p -> [String] -> String
neqBV)
                                , (Op
LessThan,      String -> String -> Bool -> [String] -> String
lift2S  String
"bvult" String
"bvslt")
                                , (Op
GreaterThan,   String -> String -> Bool -> [String] -> String
lift2S  String
"bvugt" String
"bvsgt")
                                , (Op
LessEq,        String -> String -> Bool -> [String] -> String
lift2S  String
"bvule" String
"bvsle")
                                , (Op
GreaterEq,     String -> String -> Bool -> [String] -> String
lift2S  String
"bvuge" String
"bvsge")
                                ]

                -- Boolean comparisons.. SMTLib's bool type doesn't do comparisons, but Haskell does.. Sigh
                boolComps :: [(Op, [String] -> String)]
boolComps      = [ (Op
LessThan,      [String] -> String
blt)
                                 , (Op
GreaterThan,   [String] -> String
blt ([String] -> String)
-> ([String] -> [String]) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [String]
forall {a}. Show a => [a] -> [a]
swp)
                                 , (Op
LessEq,        [String] -> String
blq)
                                 , (Op
GreaterEq,     [String] -> String
blq ([String] -> String)
-> ([String] -> [String]) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [String]
forall {a}. Show a => [a] -> [a]
swp)
                                 ]
                               where blt :: [String] -> String
blt [String
x, String
y] = String
"(and (not " 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
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                                     blt [String]
xs     = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.boolComps.blt: Impossible happened, incorrect arity (expected 2): " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
xs
                                     blq :: [String] -> String
blq [String
x, String
y] = String
"(or (not " 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
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                                     blq [String]
xs     = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.boolComps.blq: Impossible happened, incorrect arity (expected 2): " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
forall a. Show a => a -> String
show [String]
xs
                                     swp :: [a] -> [a]
swp [a
x, a
y] = [a
y, a
x]
                                     swp [a]
xs     = String -> [a]
forall a. HasCallStack => String -> a
error (String -> [a]) -> String -> [a]
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.boolComps.swp: Impossible happened, incorrect arity (expected 2): " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [a] -> String
forall a. Show a => a -> String
show [a]
xs

                smtOpRealTable :: [(Op, Bool -> [String] -> String)]
smtOpRealTable =  [(Op, Bool -> [String] -> String)]
smtIntRealShared
                               [(Op, Bool -> [String] -> String)]
-> [(Op, Bool -> [String] -> String)]
-> [(Op, Bool -> [String] -> String)]
forall a. [a] -> [a] -> [a]
++ [ (Op
Quot,        String -> String -> Bool -> [String] -> String
forall {p}. String -> String -> p -> [String] -> String
lift2WM String
"/" String
"fp.div")
                                  ]

                smtOpIntTable :: [(Op, Bool -> [String] -> String)]
smtOpIntTable  = [(Op, Bool -> [String] -> String)]
smtIntRealShared
                               [(Op, Bool -> [String] -> String)]
-> [(Op, Bool -> [String] -> String)]
-> [(Op, Bool -> [String] -> String)]
forall a. [a] -> [a] -> [a]
++ [ (Op
Quot,        String -> Bool -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift2   String
"div")
                                  , (Op
Rem,         String -> Bool -> [String] -> String
forall {p}. String -> p -> [String] -> String
lift2   String
"mod")
                                  ]

                smtOpFloatDoubleTable :: [(Op, Bool -> [String] -> String)]
smtOpFloatDoubleTable = [(Op, Bool -> [String] -> String)]
smtIntRealShared
                                  [(Op, Bool -> [String] -> String)]
-> [(Op, Bool -> [String] -> String)]
-> [(Op, Bool -> [String] -> String)]
forall a. [a] -> [a] -> [a]
++ [(Op
Quot, String -> String -> Bool -> [String] -> String
forall {p}. String -> String -> p -> [String] -> String
lift2WM String
"/" String
"fp.div")]

                smtIntRealShared :: [(Op, Bool -> [String] -> String)]
smtIntRealShared  = [ (Op
Plus,          String -> String -> Bool -> [String] -> String
forall {p}. String -> String -> p -> [String] -> String
lift2WM String
"+" String
"fp.add")
                                    , (Op
Minus,         String -> String -> Bool -> [String] -> String
forall {p}. String -> String -> p -> [String] -> String
lift2WM String
"-" String
"fp.sub")
                                    , (Op
Times,         String -> String -> Bool -> [String] -> String
forall {p}. String -> String -> p -> [String] -> String
lift2WM String
"*" String
"fp.mul")
                                    , (Op
UNeg,          String -> String -> Bool -> [String] -> String
forall {p}. String -> String -> p -> [String] -> String
lift1FP String
"-" String
"fp.neg")
                                    , (Op
Abs,           Bool -> [String] -> String
liftAbs)
                                    , (Op
Equal,         Bool -> [String] -> String
forall {p}. p -> [String] -> String
equal)
                                    , (Op
NotEqual,      Bool -> [String] -> String
forall {p}. p -> [String] -> String
notEqual)
                                    , (Op
LessThan,      String -> String -> Bool -> [String] -> String
forall {p}. String -> String -> p -> [String] -> String
lift2Cmp  String
"<"  String
"fp.lt")
                                    , (Op
GreaterThan,   String -> String -> Bool -> [String] -> String
forall {p}. String -> String -> p -> [String] -> String
lift2Cmp  String
">"  String
"fp.gt")
                                    , (Op
LessEq,        String -> String -> Bool -> [String] -> String
forall {p}. String -> String -> p -> [String] -> String
lift2Cmp  String
"<=" String
"fp.leq")
                                    , (Op
GreaterEq,     String -> String -> Bool -> [String] -> String
forall {p}. String -> String -> p -> [String] -> String
lift2Cmp  String
">=" String
"fp.geq")
                                    ]

                ratOpTable :: [(Op, [String] -> String)]
ratOpTable = [ (Op
Plus,        String -> [String] -> String
lift2Rat String
"sbv.rat.plus")
                             , (Op
Minus,       String -> [String] -> String
lift2Rat String
"sbv.rat.minus")
                             , (Op
Times,       String -> [String] -> String
lift2Rat String
"sbv.rat.times")
                             , (Op
UNeg,        String -> [String] -> String
liftRat  String
"sbv.rat.uneg")
                             , (Op
Abs,         String -> [String] -> String
liftRat  String
"sbv.rat.abs")
                             , (Op
Equal,       String -> [String] -> String
lift2Rat String
"sbv.rat.eq")
                             , (Op
NotEqual,    String -> [String] -> String
lift2Rat String
"sbv.rat.notEq")
                             , (Op
LessThan,    String -> [String] -> String
lift2Rat String
"sbv.rat.lt")
                             , (Op
GreaterThan, String -> [String] -> String
lift2Rat String
"sbv.rat.lt" ([String] -> String)
-> ([String] -> [String]) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [String]
forall {a}. Show a => [a] -> [a]
swap)
                             , (Op
LessEq,      String -> [String] -> String
lift2Rat String
"sbv.rat.leq")
                             , (Op
GreaterEq,   String -> [String] -> String
lift2Rat String
"sbv.rat.leq" ([String] -> String)
-> ([String] -> [String]) -> [String] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> [String]
forall {a}. Show a => [a] -> [a]
swap)
                             ]
                        where lift2Rat :: String -> [String] -> String
lift2Rat String
o [String
x, String
y] = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " 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
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                              lift2Rat String
o [String]
sbvs   = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMTLib2.sh.lift2Rat: Unexpected arguments: "   String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String, [String]) -> String
forall a. Show a => a -> String
show (String
o, [String]
sbvs)
                              liftRat :: String -> [String] -> String
liftRat  String
o [String
x]    = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                              liftRat  String
o [String]
sbvs   = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMTLib2.sh.lift2Rat: Unexpected arguments: "   String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String, [String]) -> String
forall a. Show a => a -> String
show (String
o, [String]
sbvs)
                              swap :: [a] -> [a]
swap [a
x, a
y]       = [a
y, a
x]
                              swap [a]
sbvs         = String -> [a]
forall a. HasCallStack => String -> a
error (String -> [a]) -> String -> [a]
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMTLib2.sh.swap: Unexpected arguments: "   String -> String -> String
forall a. [a] -> [a] -> [a]
++ [a] -> String
forall a. Show a => a -> String
show [a]
sbvs

                -- equality and comparisons are the only thing that works on uninterpreted sorts and pretty much everything else
                uninterpretedTable :: [(Op, [String] -> String)]
uninterpretedTable = [ (Op
Equal,       String -> String -> Bool -> [String] -> String
lift2S String
"="        String
"="        Bool
True)
                                     , (Op
NotEqual,    String -> String -> Bool -> [String] -> String
liftNS String
"distinct" String
"distinct" Bool
True)
                                     , (Op
LessThan,    String -> [String] -> String
unintComp String
"<")
                                     , (Op
GreaterThan, String -> [String] -> String
unintComp String
">")
                                     , (Op
LessEq,      String -> [String] -> String
unintComp String
"<=")
                                     , (Op
GreaterEq,   String -> [String] -> String
unintComp String
">=")
                                     ]

                -- For strings, equality and comparisons are the only operators
                smtStringTable :: [(Op, [String] -> String)]
smtStringTable = [ (Op
Equal,       String -> String -> Bool -> [String] -> String
lift2S String
"="        String
"="        Bool
True)
                                 , (Op
NotEqual,    String -> String -> Bool -> [String] -> String
liftNS String
"distinct" String
"distinct" Bool
True)
                                 , (Op
LessThan,    Bool -> String -> [String] -> String
stringCmp Bool
False String
"str.<")
                                 , (Op
GreaterThan, Bool -> String -> [String] -> String
stringCmp Bool
True  String
"str.<")
                                 , (Op
LessEq,      Bool -> String -> [String] -> String
stringCmp Bool
False String
"str.<=")
                                 , (Op
GreaterEq,   Bool -> String -> [String] -> String
stringCmp Bool
True  String
"str.<=")
                                 ]

                -- For lists, equality is really the only operator
                -- Likewise here, things might change for comparisons
                smtListTable :: [(Op, [String] -> String)]
smtListTable = [ (Op
Equal,       String -> String -> Bool -> [String] -> String
lift2S String
"="        String
"="        Bool
True)
                               , (Op
NotEqual,    String -> String -> Bool -> [String] -> String
liftNS String
"distinct" String
"distinct" Bool
True)
                               , (Op
LessThan,    Bool -> String -> [String] -> String
seqCmp Bool
False String
"seq.<")
                               , (Op
GreaterThan, Bool -> String -> [String] -> String
seqCmp Bool
True  String
"seq.<")
                               , (Op
LessEq,      Bool -> String -> [String] -> String
seqCmp Bool
False String
"seq.<=")
                               , (Op
GreaterEq,   Bool -> String -> [String] -> String
seqCmp Bool
True  String
"seq.<=")
                               ]

declareFun :: SV -> SBVType -> Maybe String -> [String]
declareFun :: SV -> SBVType -> Maybe String -> [String]
declareFun = String -> SBVType -> Maybe String -> [String]
declareName (String -> SBVType -> Maybe String -> [String])
-> (SV -> String) -> SV -> SBVType -> Maybe String -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SV -> String
forall a. Show a => a -> String
show

-- If we have a char, we have to make sure it's and SMTLib string of length exactly one
-- If we have a rational, we have to make sure the denominator is > 0
-- Otherwise, we just declare the name
declareName :: String -> SBVType -> Maybe String -> [String]
declareName :: String -> SBVType -> Maybe String -> [String]
declareName String
s t :: SBVType
t@(SBVType [Kind]
inputKS) Maybe String
mbCmnt = String
decl String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
restrict
  where decl :: String
decl        = String
"(declare-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVType -> String
cvtType SBVType
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> (String -> String) -> Maybe String -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (String
" ; " String -> String -> String
forall a. [a] -> [a] -> [a]
++) Maybe String
mbCmnt

        ([Kind]
args, Kind
result) = case [Kind]
inputKS of
                          [] -> String -> ([Kind], Kind)
forall a. HasCallStack => String -> a
error (String -> ([Kind], Kind)) -> String -> ([Kind], Kind)
forall a b. (a -> b) -> a -> b
$ String
"SBV.declareName: Unexpected empty type for: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
s
                          [Kind]
_  -> ([Kind] -> [Kind]
forall a. HasCallStack => [a] -> [a]
init [Kind]
inputKS, [Kind] -> Kind
forall a. HasCallStack => [a] -> a
last [Kind]
inputKS)

        -- Does the kind KChar and KRational *not* occur in the kind anywhere?
        charRatFree :: Kind -> Bool
charRatFree Kind
k = (Kind -> Bool) -> [Kind] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Kind -> Bool
notCharOrRat (Kind -> [Kind]
expandKinds Kind
k)
           where notCharOrRat :: Kind -> Bool
notCharOrRat Kind
KChar     = Bool
False
                 notCharOrRat Kind
KRational = Bool
False
                 notCharOrRat Kind
_         = Bool
True

        noCharOrRat :: Bool
noCharOrRat   = Kind -> Bool
charRatFree Kind
result
        needsQuant :: Bool
needsQuant    = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Kind] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Kind]
args

        resultVar :: String
resultVar | Bool
needsQuant = String
"result"
                  | Bool
True       = String
s

        argList :: [String]
argList   = [String
"a" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i | (Int
i, Kind
_) <- [Int] -> [Kind] -> [(Int, Kind)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1::Int ..] [Kind]
args]
        argTList :: [String]
argTList  = [String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" | (String
a, Kind
k) <- [String] -> [Kind] -> [(String, Kind)]
forall a b. [a] -> [b] -> [(a, b)]
zip [String]
argList [Kind]
args]
        resultExp :: String
resultExp = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
argList String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        restrict :: [String]
restrict | Bool
noCharOrRat = []
                 | Bool
needsQuant  =    [               String
"(assert (forall (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
argTList String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                                    ,               String
"                (let ((" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
resultVar String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
resultExp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
                                    ]
                                 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (case [String]
constraints of
                                       []     ->  [ String
"                     true"]
                                       [String
x]    ->  [ String
"                     " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x]
                                       (String
x:[String]
xs) ->  ( String
"                     (and " 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
c | String
c <- [String]
xs]
                                               [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"                     )"])
                                 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [        String
"                )))"]
                 | Bool
True        = case [String]
constraints of
                                  []     -> []
                                  [String
x]    -> [String
"(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"]
                                  (String
x:[String]
xs) -> ( String
"(assert (and " 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
c | String
c <- [String]
xs]
                                         [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"        ))"]

        constraints :: [String]
constraints = Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
walk Int
0 String
resultVar Kind -> String -> [String]
cstr Kind
result
          where cstr :: Kind -> String -> [String]
cstr Kind
KChar     String
nm = [String
"(= 1 (str.len " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"]
                cstr Kind
KRational String
nm = [String
"(< 0 (sbv.rat.denominator " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"]
                cstr Kind
_         String
_  = []

        mkAnd :: [String] -> (String -> [a]) -> [a]
mkAnd [] String -> [a]
_context = []
        mkAnd [String
c] String -> [a]
context = String -> [a]
context String
c
        mkAnd [String]
cs  String -> [a]
context = String -> [a]
context (String -> [a]) -> String -> [a]
forall a b. (a -> b) -> a -> b
$ String
"(and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
cs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        walk :: Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
        walk :: Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
walk Int
_d String
nm Kind -> String -> [String]
f k :: Kind
k@KBool     {}         = Kind -> String -> [String]
f Kind
k String
nm
        walk Int
_d String
nm Kind -> String -> [String]
f k :: Kind
k@KBounded  {}         = Kind -> String -> [String]
f Kind
k String
nm
        walk Int
_d String
nm Kind -> String -> [String]
f k :: Kind
k@KUnbounded{}         = Kind -> String -> [String]
f Kind
k String
nm
        walk Int
_d String
nm Kind -> String -> [String]
f k :: Kind
k@KReal     {}         = Kind -> String -> [String]
f Kind
k String
nm
        walk Int
_d String
nm Kind -> String -> [String]
f k :: Kind
k@KUserSort {}         = Kind -> String -> [String]
f Kind
k String
nm
        walk Int
_d String
nm Kind -> String -> [String]
f k :: Kind
k@KFloat    {}         = Kind -> String -> [String]
f Kind
k String
nm
        walk Int
_d String
nm Kind -> String -> [String]
f k :: Kind
k@KDouble   {}         = Kind -> String -> [String]
f Kind
k String
nm
        walk Int
_d String
nm Kind -> String -> [String]
f k :: Kind
k@KRational {}         = Kind -> String -> [String]
f Kind
k String
nm
        walk Int
_d String
nm Kind -> String -> [String]
f k :: Kind
k@KFP       {}         = Kind -> String -> [String]
f Kind
k String
nm
        walk Int
_d String
nm Kind -> String -> [String]
f k :: Kind
k@KChar     {}         = Kind -> String -> [String]
f Kind
k String
nm
        walk Int
_d String
nm Kind -> String -> [String]
f k :: Kind
k@KString   {}         = Kind -> String -> [String]
f Kind
k String
nm
        walk  Int
d String
nm Kind -> String -> [String]
f  (KList Kind
k)
          | Kind -> Bool
charRatFree Kind
k                 = []
          | Bool
True                          = let fnm :: String
fnm   = String
"seq" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
d
                                                cstrs :: [String]
cstrs = Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
walk (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (String
"(seq.nth " 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
fnm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")") Kind -> String -> [String]
f Kind
k
                                            in [String] -> (String -> [String]) -> [String]
forall {a}. [String] -> (String -> [a]) -> [a]
mkAnd [String]
cstrs ((String -> [String]) -> [String])
-> (String -> [String]) -> [String]
forall a b. (a -> b) -> a -> b
$ \String
hole -> [String
"(forall ((" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fnm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
KUnbounded String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) (=> (and (>= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fnm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" 0) (< " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fnm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (seq.len " 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
hole String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"]
        walk  Int
d  String
nm Kind -> String -> [String]
f (KSet Kind
k)
          | Kind -> Bool
charRatFree Kind
k                 = []
          | Bool
True                          = let fnm :: String
fnm    = String
"set" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
d
                                                cstrs :: [String]
cstrs  = Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
walk (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) String
nm (\Kind
sk String
snm -> [String
"(=> (select " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
snm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fnm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" | String
c <- Kind -> String -> [String]
f Kind
sk String
fnm]) Kind
k
                                            in [String] -> (String -> [String]) -> [String]
forall {a}. [String] -> (String -> [a]) -> [a]
mkAnd [String]
cstrs ((String -> [String]) -> [String])
-> (String -> [String]) -> [String]
forall a b. (a -> b) -> a -> b
$ \String
hole -> [String
"(forall ((" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fnm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
hole String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"]
        walk  Int
d  String
nm  Kind -> String -> [String]
f (KTuple [Kind]
ks)        = let tt :: String
tt        = String
"SBVTuple" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Kind] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
ks)
                                                project :: a -> String
project a
i = String
"(proj_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
tt String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                                                nmks :: [(String, Kind)]
nmks      = [(Int -> String
forall a. Show a => a -> String
project Int
i, Kind
k) | (Int
i, Kind
k) <- [Int] -> [Kind] -> [(Int, Kind)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1::Int ..] [Kind]
ks]
                                            in ((String, Kind) -> [String]) -> [(String, Kind)] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(String
n, Kind
k) -> Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
walk (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) String
n Kind -> String -> [String]
f Kind
k) [(String, Kind)]
nmks
        walk  Int
d  String
nm  Kind -> String -> [String]
f km :: Kind
km@(KMaybe Kind
k)      = let n :: String
n = String
"(get_just_SBVMaybe " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                                            in  [String
"(=> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"((_ is (just_SBVMaybe (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
km String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" | String
c <- Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
walk (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) String
n Kind -> String -> [String]
f Kind
k]
        walk  Int
d  String
nm  Kind -> String -> [String]
f ke :: Kind
ke@(KEither Kind
k1 Kind
k2) = let n1 :: String
n1 = String
"(get_left_SBVEither "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                                                n2 :: String
n2 = String
"(get_right_SBVEither " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                                                c1 :: [String]
c1 = [String
"(=> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"((_ is (left_SBVEither ("  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
k1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
ke String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" | String
c <- Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
walk (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) String
n1 Kind -> String -> [String]
f Kind
k1]
                                                c2 :: [String]
c2 = [String
"(=> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"((_ is (right_SBVEither (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
k2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
ke String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" | String
c <- Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
walk (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) String
n2 Kind -> String -> [String]
f Kind
k2]
                                            in [String]
c1 [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
c2
        walk Int
d  String
nm Kind -> String -> [String]
f  (KArray Kind
k1 Kind
k2)
          | (Kind -> Bool) -> [Kind] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Kind -> Bool
charRatFree [Kind
k1, Kind
k2]      = []
          | Bool
True                          = let fnm :: String
fnm   = String
"array" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
d
                                                cstrs :: [String]
cstrs = Int -> String -> (Kind -> String -> [String]) -> Kind -> [String]
walk (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (String
"(select " 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
fnm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")") Kind -> String -> [String]
f Kind
k2
                                            in [String] -> (String -> [String]) -> [String]
forall {a}. [String] -> (String -> [a]) -> [a]
mkAnd [String]
cstrs ((String -> [String]) -> [String])
-> (String -> [String]) -> [String]
forall a b. (a -> b) -> a -> b
$ \String
hole -> [String
"(forall ((" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fnm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
k1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
hole String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"]

-----------------------------------------------------------------------------------------------
-- Casts supported by SMTLib. (From: <https://smt-lib.org/theories-FloatingPoint.shtml>)
--   ; from another floating point sort
--   ((_ to_fp eb sb) RoundingMode (_ FloatingPoint mb nb) (_ FloatingPoint eb sb))
--
--   ; from real
--   ((_ to_fp eb sb) RoundingMode Real (_ FloatingPoint eb sb))
--
--   ; from signed machine integer, represented as a 2's complement bit vector
--   ((_ to_fp eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb))
--
--   ; from unsigned machine integer, represented as bit vector
--   ((_ to_fp_unsigned eb sb) RoundingMode (_ BitVec m) (_ FloatingPoint eb sb))
--
--   ; to unsigned machine integer, represented as a bit vector
--   ((_ fp.to_ubv m) RoundingMode (_ FloatingPoint eb sb) (_ BitVec m))
--
--   ; to signed machine integer, represented as a 2's complement bit vector
--   ((_ fp.to_sbv m) RoundingMode (_ FloatingPoint eb sb) (_ BitVec m))
--
--   ; to real
--   (fp.to_real (_ FloatingPoint eb sb) Real)
-----------------------------------------------------------------------------------------------

handleFPCast :: Kind -> Kind -> String -> String -> String
handleFPCast :: Kind -> Kind -> String -> String -> String
handleFPCast Kind
kFromIn Kind
kToIn String
rm String
input
  | Kind
kFrom Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
kTo
  = String
input
  | Bool
True
  = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> Kind -> String -> String
cast Kind
kFrom Kind
kTo String
input String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
  where addRM :: String -> String -> String
addRM String
a String
s = String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a

        kFrom :: Kind
kFrom = Kind -> Kind
simplify Kind
kFromIn
        kTo :: Kind
kTo   = Kind -> Kind
simplify Kind
kToIn

        simplify :: Kind -> Kind
simplify Kind
KFloat  = Int -> Int -> Kind
KFP   Int
8 Int
24
        simplify Kind
KDouble = Int -> Int -> Kind
KFP  Int
11 Int
53
        simplify Kind
k       = Kind
k

        size :: (a, a) -> String
size (a
eb, a
sb) = a -> String
forall a. Show a => a -> String
show a
eb 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
sb

        -- To go and back from Ints, we detour through reals
        cast :: Kind -> Kind -> String -> String
cast Kind
KUnbounded (KFP Int
eb Int
sb) String
a = String
"(_ to_fp " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall {a} {a}. (Show a, Show a) => (a, a) -> String
size (Int
eb, Int
sb) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (to_real " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        cast KFP{}      Kind
KUnbounded  String
a = String
"to_int (fp.to_real " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        -- To floats
        cast (KBounded Bool
False Int
_) (KFP Int
eb Int
sb) String
a = String -> String -> String
addRM String
a (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"(_ to_fp_unsigned " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall {a} {a}. (Show a, Show a) => (a, a) -> String
size (Int
eb, Int
sb) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        cast (KBounded Bool
True  Int
_) (KFP Int
eb Int
sb) String
a = String -> String -> String
addRM String
a (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"(_ to_fp "          String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall {a} {a}. (Show a, Show a) => (a, a) -> String
size (Int
eb, Int
sb) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        cast Kind
KReal              (KFP Int
eb Int
sb) String
a = String -> String -> String
addRM String
a (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"(_ to_fp "          String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall {a} {a}. (Show a, Show a) => (a, a) -> String
size (Int
eb, Int
sb) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        cast KFP{}              (KFP Int
eb Int
sb) String
a = String -> String -> String
addRM String
a (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"(_ to_fp "          String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall {a} {a}. (Show a, Show a) => (a, a) -> String
size (Int
eb, Int
sb) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        -- From float/double
        cast KFP{} (KBounded Bool
False Int
m) String
a = String -> String -> String
addRM String
a (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"(_ fp.to_ubv " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        cast KFP{} (KBounded Bool
True  Int
m) String
a = String -> String -> String
addRM String
a (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"(_ fp.to_sbv " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        -- To real
        cast KFP{} Kind
KReal String
a = String
"fp.to_real" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a

        -- Nothing else should come up:
        cast Kind
f  Kind
d  String
_ = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMTLib2: Unexpected FPCast from: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
f String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
d

rot :: String -> Int -> SV -> String
rot :: String -> Int -> SV -> String
rot String
o Int
c SV
x = String
"((_ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

shft :: String -> String -> SV -> SV -> String
shft :: String -> String -> SV -> SV -> String
shft String
oW String
oS SV
x SV
c = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
cvtSV SV
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
   where o :: String
o = if SV -> Bool
forall a. HasKind a => a -> Bool
hasSign SV
x then String
oS else String
oW

-- Various casts
handleKindCast :: Kind -> Kind -> String -> String
handleKindCast :: Kind -> Kind -> String -> String
handleKindCast Kind
kFrom Kind
kTo String
a
  | Kind
kFrom Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
kTo
  = String
a
  | Bool
True
  = case Kind
kFrom of
      KBounded Bool
s Int
m -> case Kind
kTo of
                        KBounded Bool
_ Int
n -> (Int -> String) -> Int -> Int -> String
forall {a}.
(Ord a, Num a, Show a) =>
(a -> String) -> a -> a -> String
fromBV (if Bool
s then Int -> String
forall a. Show a => a -> String
signExtend else Int -> String
forall a. Show a => a -> String
zeroExtend) Int
m Int
n
                        Kind
KUnbounded   -> if Bool
s then String
"(sbv_to_int " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                                             else String
"(ubv_to_int " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                        Kind
_            -> String
tryFPCast

      Kind
KUnbounded   -> case Kind
kTo of
                        Kind
KReal        -> String
"(to_real " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                        KBounded Bool
_ Int
n -> String
"((_ int_to_bv " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                        Kind
_            -> String
tryFPCast

      Kind
KReal        -> case Kind
kTo of
                        Kind
KUnbounded   -> String
"(to_int " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                        Kind
_            -> String
tryFPCast

      Kind
_            -> String
tryFPCast

  where -- See if we can push this down to a float-cast, using sRNE. This happens if one of the kinds is a float/double.
        -- Otherwise complain
        tryFPCast :: String
tryFPCast
          | (Kind -> Bool) -> [Kind] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\Kind
k -> Kind -> Bool
forall a. HasKind a => a -> Bool
isFloat Kind
k Bool -> Bool -> Bool
|| Kind -> Bool
forall a. HasKind a => a -> Bool
isDouble Kind
k) [Kind
kFrom, Kind
kTo]
          = Kind -> Kind -> String -> String -> String
handleFPCast Kind
kFrom Kind
kTo (RoundingMode -> String
smtRoundingMode RoundingMode
RoundNearestTiesToEven) String
a
          | Bool
True
          = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMTLib2: Unexpected cast from: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
kFrom String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" to " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
kTo

        fromBV :: (a -> String) -> a -> a -> String
fromBV a -> String
upConv a
m a
n
         | a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
m  = a -> String
upConv  (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
m)
         | a
m a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
n = String
a
         | Bool
True   = a -> String
forall a. Show a => a -> String
extract (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1)

        signExtend :: a -> String
signExtend a
i = String
"((_ sign_extend " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i String -> String -> String
forall a. [a] -> [a] -> [a]
++  String
") "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        zeroExtend :: a -> String
zeroExtend a
i = String
"((_ zero_extend " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i String -> String -> String
forall a. [a] -> [a] -> [a]
++  String
") "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        extract :: a -> String
extract    a
i = String
"((_ extract "     String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" 0) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

-- Translation of pseudo-booleans, in case the solver supports them
handlePB :: PBOp -> [String] -> String
handlePB :: PBOp -> [String] -> String
handlePB (PB_AtMost  Int
k) [String]
args = String
"((_ at-most "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k                                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
handlePB (PB_AtLeast Int
k) [String]
args = String
"((_ at-least " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k                                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
handlePB (PB_Exactly Int
k) [String]
args = String
"((_ pbeq "     String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show (Int
k Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: Int -> Int -> [Int]
forall a. Int -> a -> [a]
replicate ([String] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
args) Int
1)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
handlePB (PB_Eq [Int]
cs   Int
k) [String]
args = String
"((_ pbeq "     String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show (Int
k Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
cs))                        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
handlePB (PB_Le [Int]
cs   Int
k) [String]
args = String
"((_ pble "     String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show (Int
k Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
cs))                        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
handlePB (PB_Ge [Int]
cs   Int
k) [String]
args = String
"((_ pbge "     String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show (Int
k Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
cs))                        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

-- Translation of pseudo-booleans, in case the solver does *not* support them
reducePB :: PBOp -> [String] -> String
reducePB :: PBOp -> [String] -> String
reducePB PBOp
op [String]
args = case PBOp
op of
                     PB_AtMost  Int
k -> String
"(<= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Int] -> String
addIf (Int -> [Int]
forall a. a -> [a]
repeat Int
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                     PB_AtLeast Int
k -> String
"(>= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Int] -> String
addIf (Int -> [Int]
forall a. a -> [a]
repeat Int
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                     PB_Exactly Int
k -> String
"(=  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Int] -> String
addIf (Int -> [Int]
forall a. a -> [a]
repeat Int
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                     PB_Le [Int]
cs   Int
k -> String
"(<= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Int] -> String
addIf [Int]
cs         String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                     PB_Ge [Int]
cs   Int
k -> String
"(>= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Int] -> String
addIf [Int]
cs         String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                     PB_Eq [Int]
cs   Int
k -> String
"(=  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [Int] -> String
addIf [Int]
cs         String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

  where addIf :: [Int] -> String
        addIf :: [Int] -> String
addIf [Int]
cs = String
"(+ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String
"(ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" 0)" | (String
a, Int
c) <- [String] -> [Int] -> [(String, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [String]
args [Int]
cs] String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

-- | Translate an option setting to SMTLib. Note the SetLogic/SetInfo discrepancy.
setSMTOption :: SMTConfig -> SMTOption -> String
setSMTOption :: SMTConfig -> SMTOption -> String
setSMTOption SMTConfig
cfg = SMTOption -> String
set
  where set :: SMTOption -> String
set (DiagnosticOutputChannel   String
f) = [String] -> String
opt   [String
":diagnostic-output-channel",   String -> String
forall a. Show a => a -> String
show String
f]
        set (ProduceAssertions         Bool
b) = [String] -> String
opt   [String
":produce-assertions",          Bool -> String
smtBool Bool
b]
        set (ProduceAssignments        Bool
b) = [String] -> String
opt   [String
":produce-assignments",         Bool -> String
smtBool Bool
b]
        set (ProduceProofs             Bool
b) = [String] -> String
opt   [String
":produce-proofs",              Bool -> String
smtBool Bool
b]
        set (ProduceInterpolants       Bool
b) = [String] -> String
opt   [String
":produce-interpolants",        Bool -> String
smtBool Bool
b]
        set (ProduceUnsatAssumptions   Bool
b) = [String] -> String
opt   [String
":produce-unsat-assumptions",   Bool -> String
smtBool Bool
b]
        set (ProduceUnsatCores         Bool
b) = [String] -> String
opt   [String
":produce-unsat-cores",         Bool -> String
smtBool Bool
b]
        set (ProduceAbducts            Bool
b) = [String] -> String
opt   [String
":produce-abducts",             Bool -> String
smtBool Bool
b]
        set (RandomSeed                Integer
i) = [String] -> String
opt   [String
":random-seed",                 Integer -> String
forall a. Show a => a -> String
show Integer
i]
        set (ReproducibleResourceLimit Integer
i) = [String] -> String
opt   [String
":reproducible-resource-limit", Integer -> String
forall a. Show a => a -> String
show Integer
i]
        set (SMTVerbosity              Integer
i) = [String] -> String
opt   [String
":verbosity",                   Integer -> String
forall a. Show a => a -> String
show Integer
i]
        set (OptionKeyword          String
k [String]
as) = [String] -> String
opt   (String
k String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
as)
        set (SetLogic                  Logic
l) = Logic -> String
logic Logic
l
        set (SetInfo                String
k [String]
as) = [String] -> String
info  (String
k String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
as)
        set (SetTimeOut                Integer
i) = [String] -> String
opt   ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ Integer -> [String]
forall {a}. Show a => a -> [String]
timeOut Integer
i

        opt :: [String] -> String
opt   [String]
xs = String
"(set-option " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        info :: [String] -> String
info  [String]
xs = String
"(set-info "   String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        logic :: Logic -> String
logic Logic
Logic_NONE = String
"; NB. not setting the logic per user request of Logic_NONE"
        logic Logic
l          = String
"(set-logic " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Logic -> String
forall a. Show a => a -> String
show Logic
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        -- timeout is not standard. We distinguish between CVC/Z3. All else follows z3
        -- The value is in milliseconds, which is how z3/CVC interpret it
        timeOut :: a -> [String]
timeOut a
i = case SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
cfg) of
                     Solver
CVC4 -> [String
":tlimit-per", a -> String
forall a. Show a => a -> String
show a
i]
                     Solver
CVC5 -> [String
":tlimit-per", a -> String
forall a. Show a => a -> String
show a
i]
                     Solver
_    -> [String
":timeout",    a -> String
forall a. Show a => a -> String
show a
i]

        -- SMTLib's True/False is spelled differently than Haskell's.
        smtBool :: Bool -> String
        smtBool :: Bool -> String
smtBool Bool
True  = String
"true"
        smtBool Bool
False = String
"false"