-----------------------------------------------------------------------------
-- |
-- 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 OverloadedStrings   #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns        #-}

{-# OPTIONS_GHC -Wall -Werror #-}

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

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

import qualified Data.Foldable as F (toList, foldl')
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 qualified Data.Text            as T
import           Data.Text            (Text)

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

import Data.SBV.SMT.Utils

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

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

import qualified Data.Generics.Uniplate.Data as G

import qualified Data.Graph as DG


-- Check that all ADT subkinds are registered. If not, tell the user to do so
-- NB. This should not be the case as we "automatically" register the subkinds
-- as we encounter them. But this is mostly a if-something-goes-wrong check.
checkKinds :: [Kind] -> Maybe String
checkKinds :: [Kind] -> Maybe String
checkKinds [Kind]
ks = case [(String, Int)
m | m :: (String, Int)
m@(String
n, Int
_) <- [(String, Int)]
apps, String
n String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` [String]
defs] of
                  []       -> Maybe String
forall a. Maybe a
Nothing
                  xs :: [(String, Int)]
xs@((String, Int)
f:[(String, Int)]
_) -> let (String
h, Int
cnt) = case [(String, Int)
p | p :: (String, Int)
p@(String
_, Int
i) <- [(String, Int)]
xs, Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0] of
                                               ((String, Int)
p:[(String, Int)]
_) -> (String, Int)
p
                                               [(String, Int)]
_     -> (String, Int)
f
                                  plu :: Text
plu | [(String, Int)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(String, Int)]
xs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 = Text
"s are"
                                      | Bool
True          = Text
" is"
                                  msg :: Text
msg = [Text] -> Text
T.unlines ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ [
                                      Text
"Data.SBV.mkSymbolic: Impossible happened! Unregistered subkinds."
                                    , Text
"***"
                                    , Text
"*** The following kind" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
plu Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" not registered: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords (((String, Int) -> Text) -> [(String, Int)] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Text
T.pack (String -> Text)
-> ((String, Int) -> String) -> (String, Int) -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Int) -> String
forall a b. (a, b) -> a
fst) [(String, Int)]
xs)
                                    , Text
"***"
                                    , Text
"*** Please report this as a bug."
                                    , Text
"***"
                                    , Text
"*** As a workaround, you can try registering each ADT subfield, using: "
                                    , Text
"***"
                                    , Text
"***    {-# LANGUAGE TypeApplications #-}"
                                    , Text
"***"
                                    , Text
"***    import Data.Proxy"
                                    , Text
"***    registerType (Proxy @" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Int -> Text
mkProxy String
h Int
cnt Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
                                    ]
                                    [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++ Int -> [Text]
forall {a} {a}. (Eq a, Num a, IsString a) => a -> [a]
extras Int
cnt
                                    [Text] -> [Text] -> [Text]
forall a. [a] -> [a] -> [a]
++ [ Text
"***"
                                       , Text
"*** Even if the workaround does the trick for you, it should not"
                                       , Text
"*** be needed. Please report this as a bug!"
                                       ]
                              in String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
msg


  where apps :: [(String, Int)]
apps = [(String, Int)] -> [(String, Int)]
forall a. Eq a => [a] -> [a]
nub [(String
n, [Kind] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Kind]
as) | KApp String
n [Kind]
as <- (Kind -> [Kind]) -> [Kind] -> [Kind]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Kind -> [Kind]
expandKinds [Kind]
ks]
        defs :: [String]
defs = [String] -> [String]
forall a. Eq a => [a] -> [a]
nub [String
n | KADT String
n [(String, Kind)]
_ [(String, [Kind])]
_ <- [Kind]
ks]
        mkProxy :: String -> Int -> Text
mkProxy String
h Int
0 = String -> Text
T.pack String
h
        mkProxy String
h Int
n = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords (String -> Text
T.pack String
h Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: Int -> Text -> [Text]
forall a. Int -> a -> [a]
replicate Int
n Text
"Integer") Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

        extras :: a -> [a]
extras a
0 = []
        extras a
_ = [ a
"***"
                   , a
"*** NB. You can use any base type as arguments, not just 'Integer'."
                   , a
"*** It does not need to match the actual use cases, just one instance"
                   , a
"*** at some base type is sufficent."
                   ]

-- | Translate a problem into an SMTLib2 script
cvt :: SMTLibConverter (Text, Text)
cvt :: SMTLibConverter (Text, Text)
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 [(String, (SMTDef, SBVType))]
defs (SBVPgm Seq (SV, SBVExpr)
asgnsSeq) Seq (Bool, [(String, String)], SV)
cstrs SV
out SMTConfig
cfg
   | Just String
s <- [Kind] -> Maybe String
checkKinds [Kind]
allKinds
   = String -> (Text, Text)
forall a. HasCallStack => String -> a
error String
s
   | Bool
True
   = (Text -> [Text] -> Text
T.intercalate Text
"\n" [Text]
pgm, Text -> [Text] -> Text
T.intercalate Text
"\n" [Text]
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
F.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    = (Kind -> Bool) -> [Kind] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
forall a. HasKind a => a -> Bool
isRoundingMode [Kind]
allKinds
        hasBVs :: Bool
hasBVs         = Bool -> Bool
not ([()] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [() | KBounded{} <- [Kind]
allKinds])
        adtsNoRM :: [(String, [(String, Kind)], [(String, [Kind])])]
adtsNoRM       = [(String
s, [(String, Kind)]
ps, [(String, [Kind])]
cs) | k :: Kind
k@(KADT String
s [(String, Kind)]
ps [(String, [Kind])]
cs) <- [Kind]
allKinds, Bool -> Bool
not (Kind -> Bool
forall a. HasKind a => a -> Bool
isRoundingMode Kind
k)]
        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
        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
        hasADTs :: Bool
hasADTs        = Bool -> Bool
not (Bool -> Bool)
-> ([(String, [(String, Kind)], [(String, [Kind])])] -> Bool)
-> [(String, [(String, Kind)], [(String, [Kind])])]
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(String, [(String, Kind)], [(String, [Kind])])] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([(String, [(String, Kind)], [(String, [Kind])])] -> Bool)
-> [(String, [(String, Kind)], [(String, [Kind])])] -> Bool
forall a b. (a -> b) -> a -> b
$ [(String, [(String, Kind)], [(String, [Kind])])]
adtsNoRM
        rm :: RoundingMode
rm             = SMTConfig -> RoundingMode
roundingMode SMTConfig
cfg
        solverCaps :: SolverCapabilities
solverCaps     = SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)

        (Bool
needsQuantifiers, Bool
needsSpecialRels) = case ProgInfo
curProgInfo of
           ProgInfo Bool
hasQ [SpecialRelOp]
srs [(String, String)]
tcs -> (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))

        -- 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 [Text]
doesntHandle = [[Text]] -> Maybe [Text]
forall a. [a] -> Maybe a
listToMaybe [String -> [Text]
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
hasADTs)
                          , (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
"has data-types/sorts",   SolverCapabilities -> Bool
supportsADTs,               Bool -> Bool
not ([(String, [(String, Kind)], [(String, [Kind])])] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, [(String, Kind)], [(String, [Kind])])]
adtsNoRM))
                          ]

                 nope :: String -> [Text]
nope String
w = [ Text
"***     Given problem requires support for " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack String
w
                          , Text
"***     But the chosen solver (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Solver -> String
forall a. Show a => a -> String
show (SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
cfg))) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") doesn't support this feature."
                          ]

        -- Some cases require all, some require none.
        setAll :: String -> [Text]
setAll String
reason = [Text
"(set-logic " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Logic -> String
showLogic Logic
Logic_ALL) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") ; "  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack String
reason Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
", using catch-all."]

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

        -- If ALL is selected, use HO_ALL for CVC5 to get support for higher-order features. Yet another discrepancy.
        showLogic :: Logic -> String
showLogic Logic
Logic_ALL | Bool
isCVC5 = String
"HO_ALL"
        showLogic Logic
l                  = Logic -> String
forall a. Show a => a -> String
show Logic
l

        -- Determining the logic is surprisingly tricky!
        logic :: [Text]
        logic :: [Text]
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  -> let msg :: Text
msg = [Text] -> Text
T.unlines [ Text
""
                                                , Text
"*** Only one setOption call to 'setLogic' is allowed, found: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (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))
                                                , Text
"***  " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords ((Logic -> Text) -> [Logic] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Text
T.pack (String -> Text) -> (Logic -> String) -> Logic -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Logic -> String
forall a. Show a => a -> String
show) [Logic]
ls)
                                                ]
                                in String -> Maybe Logic
forall a. HasCallStack => String -> a
error (String -> Maybe Logic) -> String -> Maybe Logic
forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
msg
           = case Logic
l of
               Logic
Logic_NONE -> [Text
"; NB. Not setting the logic per user request of Logic_NONE"]
               Logic
_          -> [Text
"(set-logic " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Logic -> String
showLogic Logic
l) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") ; NB. User specified."]

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

           -- 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      = [Text
"; has special relations, no logic set."]

           -- Things that require ALL
           | Bool
hasInteger            = String -> [Text]
setAll String
"has unbounded values"
           | Bool
hasRational           = String -> [Text]
setAll String
"has rational values"
           | Bool
hasReal               = String -> [Text]
setAll String
"has algebraic reals"
           | Bool
hasADTs               = String -> [Text]
setAll String
"has user-defined data-types"
           | Bool
hasNonBVArrays        = String -> [Text]
setAll String
"has non-bitvector arrays"
           | Bool
hasTuples             = String -> [Text]
setAll String
"has tuples"
           | Bool
hasSets               = String -> [Text]
setAll String
"has sets"
           | Bool
hasList               = String -> [Text]
setAll String
"has lists"
           | Bool
hasChar               = String -> [Text]
setAll String
"has chars"
           | Bool
hasString             = String -> [Text]
setAll String
"has strings"
           | Bool
hasRegExp             = String -> [Text]
setAll String
"has regular expressions"
           | Bool
hasOverflows          = String -> [Text]
setAll String
"has overflow checks"
           | Bool
hasQuantBools         = String -> [Text]
setAll String
"has quantified booleans"

           | Bool
hasFP Bool -> Bool -> Bool
|| Bool
hasRounding
           = if Bool
needsQuantifiers
             then [Text
"(set-logic ALL)"]
             else if Bool
hasBVs
                  then [Text
"(set-logic QF_FPBV)"]
                  else [Text
"(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 -> [Text
"(set-logic ALL) ; external query, using all logics."]
               QueryContext
QueryInternal -> if SolverCapabilities -> Bool
supportsBitVectors SolverCapabilities
solverCaps
                                then [Text
"(set-logic " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Text -> String
T.unpack Text
qs String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Text -> String
T.unpack Text
as String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Text -> String
T.unpack Text
ufs) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"BV)"]
                                else [Text
"(set-logic ALL)"] -- fall-thru
          where qs :: Text
qs  | Bool -> Bool
not Bool
needsQuantifiers  = Text
"QF_"
                    | Bool
True                  = Text
""
                as :: Text
as  | Bool -> Bool
not Bool
hasArrays         = Text
""
                    | Bool
True                  = Text
"A"
                ufs :: Text
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 = Text
""     -- we represent tables as UFs
                    | Bool
True                  = Text
"UF"

        -- SBV always requires the production of models!
        getModels :: [Text]
        getModels :: [Text]
getModels   = Text
"(set-option :produce-models true)"
                    Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [[Text]] -> [Text]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [(String -> Text) -> [String] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map String -> Text
T.pack [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 :: [Text]
userSettings = (SMTOption -> Text) -> [SMTOption] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (SMTConfig -> SMTOption -> Text
setSMTOption SMTConfig
cfg) ([SMTOption] -> [Text]) -> [SMTOption] -> [Text]
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 :: [Text]
settings =  [Text]
userSettings        -- NB. Make sure this comes first!
                 [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [Text]
getModels
                 [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [Text]
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 :: [Text]
pgm  =  (String -> Text) -> [String] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Text
T.pack (String -> Text) -> (String -> String) -> String -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String
"; " String -> String -> String
forall a. Semigroup a => a -> a -> a
<>)) [String]
comments
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [Text]
settings
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [ Text
"; --- tuples ---" ]
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> (Int -> [Text]) -> [Int] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Int -> [Text]
declTuple [Int]
tupleArities
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [ Text
"; --- sums ---" ]
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> (if Set Kind -> Bool
containsRationals Set Kind
kindInfo then [Text]
declRationals else [])
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [ Text
"; --- ADTs  --- " | Bool -> Bool
not ([(String, [(String, Kind)], [(String, [Kind])])] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, [(String, Kind)], [(String, [Kind])])]
adtsNoRM)]
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [(String, [(String, Kind)], [(String, [Kind])])] -> [Text]
declADT [(String, [(String, Kind)], [(String, [Kind])])]
adtsNoRM
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [ Text
"; --- literal constants ---" ]
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> ((SV, CV) -> [Text]) -> [(SV, CV)] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SMTConfig -> (SV, CV) -> [Text]
declConst SMTConfig
cfg) [(SV, CV)]
consts
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [ Text
"; --- top level inputs ---"]
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [[Text]] -> [Text]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [SV -> SBVType -> Maybe Text -> [Text]
declareFun SV
s ([Kind] -> SBVType
SBVType [SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
s]) (SV -> Maybe Text
userName SV
s) | NamedSymVar
var <- [NamedSymVar]
inputs, let s :: SV
s = NamedSymVar -> SV
getSV NamedSymVar
var]
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [ Text
"; --- optimization tracker variables ---" | Bool -> Bool
not ([NamedSymVar] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedSymVar]
trackerVars) ]
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [[Text]] -> [Text]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [SV -> SBVType -> Maybe Text -> [Text]
declareFun SV
s ([Kind] -> SBVType
SBVType [SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
s]) (Text -> Maybe Text
forall a. a -> Maybe a
Just (Text
"tracks " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack String
nm)) | NamedSymVar
var <- [NamedSymVar]
trackerVars, let s :: SV
s = NamedSymVar -> SV
getSV NamedSymVar
var, let nm :: String
nm = NamedSymVar -> String
getUserName' NamedSymVar
var]
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [ Text
"; --- constant tables ---" ]
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> ((((Int, Kind, Kind), [SV]), [Text]) -> [Text])
-> [(((Int, Kind, Kind), [SV]), [Text])] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Text -> [Text] -> [Text]) -> (Text, [Text]) -> [Text]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (:) ((Text, [Text]) -> [Text])
-> ((((Int, Kind, Kind), [SV]), [Text]) -> (Text, [Text]))
-> (((Int, Kind, Kind), [SV]), [Text])
-> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Int, Kind, Kind), [SV]), [Text]) -> (Text, [Text])
mkTable) [(((Int, Kind, Kind), [SV]), [Text])]
constTables
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [ Text
"; --- non-constant tables ---" ]
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> ((((Int, Kind, Kind), [SV]), [Text]) -> Text)
-> [(((Int, Kind, Kind), [SV]), [Text])] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (((Int, Kind, Kind), [SV]), [Text]) -> Text
nonConstTable [(((Int, Kind, Kind), [SV]), [Text])]
nonConstTables
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [ Text
"; --- uninterpreted constants ---" ]
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> ((String, (Bool, Maybe [String], SBVType)) -> [Text])
-> [(String, (Bool, Maybe [String], SBVType))] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ProgInfo -> (String, (Bool, Maybe [String], SBVType)) -> [Text]
declUI ProgInfo
curProgInfo) [(String, (Bool, Maybe [String], SBVType))]
uis
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [ Text
"; --- user defined functions ---"]
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [Text]
userDefs
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [ Text
"; --- assignments ---" ]
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> ((SV, SBVExpr) -> [Text]) -> [(SV, SBVExpr)] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ProgInfo -> SMTConfig -> TableMap -> (SV, SBVExpr) -> [Text]
declDef ProgInfo
curProgInfo SMTConfig
cfg TableMap
tableMap) [(SV, SBVExpr)]
asgns
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [ Text
"; --- delayedEqualities ---" ]
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> (Text -> Text) -> [Text] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (\Text
s -> Text
"(assert " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
s Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")") [Text]
delayedEqualities
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [ Text
"; --- formula ---" ]
             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [Text]
finalAssert

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


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

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

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

                (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 Text
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 -> Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ Text
"tracks user variable " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (String -> String
forall a. Show a => a -> String
show String
u)
                        Maybe String
_                     -> Maybe Text
forall a. Maybe a
Nothing

-- | Declare ADTs
declADT :: [(String, [(String, Kind)], [(String, [Kind])])] -> [Text]
declADT :: [(String, [(String, Kind)], [(String, [Kind])])] -> [Text]
declADT = (SCC (String, [(String, Kind)], [(String, [Kind])]) -> [Text])
-> [SCC (String, [(String, Kind)], [(String, [Kind])])] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SCC (String, [(String, Kind)], [(String, [Kind])]) -> [Text]
declGroup ([SCC (String, [(String, Kind)], [(String, [Kind])])] -> [Text])
-> ([(String, [(String, Kind)], [(String, [Kind])])]
    -> [SCC (String, [(String, Kind)], [(String, [Kind])])])
-> [(String, [(String, Kind)], [(String, [Kind])])]
-> [Text]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [((String, [(String, Kind)], [(String, [Kind])]), String,
  [String])]
-> [SCC (String, [(String, Kind)], [(String, [Kind])])]
forall key node. Ord key => [(node, key, [key])] -> [SCC node]
DG.stronglyConnComp ([((String, [(String, Kind)], [(String, [Kind])]), String,
   [String])]
 -> [SCC (String, [(String, Kind)], [(String, [Kind])])])
-> ([(String, [(String, Kind)], [(String, [Kind])])]
    -> [((String, [(String, Kind)], [(String, [Kind])]), String,
         [String])])
-> [(String, [(String, Kind)], [(String, [Kind])])]
-> [SCC (String, [(String, Kind)], [(String, [Kind])])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((String, [(String, Kind)], [(String, [Kind])])
 -> ((String, [(String, Kind)], [(String, [Kind])]), String,
     [String]))
-> [(String, [(String, Kind)], [(String, [Kind])])]
-> [((String, [(String, Kind)], [(String, [Kind])]), String,
     [String])]
forall a b. (a -> b) -> [a] -> [b]
map (String, [(String, Kind)], [(String, [Kind])])
-> ((String, [(String, Kind)], [(String, [Kind])]), String,
    [String])
forall {t :: * -> *} {b} {a} {a}.
Foldable t =>
(b, [(a, Kind)], t (a, [Kind]))
-> ((b, [(a, Kind)], t (a, [Kind])), b, [String])
mkNode
  where mkNode :: (b, [(a, Kind)], t (a, [Kind]))
-> ((b, [(a, Kind)], t (a, [Kind])), b, [String])
mkNode adt :: (b, [(a, Kind)], t (a, [Kind]))
adt@(b
n, [(a, Kind)]
pks, t (a, [Kind])
cstrs) = ((b, [(a, Kind)], t (a, [Kind]))
adt, b
n, [String
s | KApp String
s [Kind]
_ <- (Kind -> [Kind]) -> [Kind] -> [Kind]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Kind -> [Kind]
expandKinds (((a, Kind) -> Kind) -> [(a, Kind)] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map (a, Kind) -> Kind
forall a b. (a, b) -> b
snd [(a, Kind)]
pks [Kind] -> [Kind] -> [Kind]
forall a. [a] -> [a] -> [a]
++ ((a, [Kind]) -> [Kind]) -> t (a, [Kind]) -> [Kind]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (a, [Kind]) -> [Kind]
forall a b. (a, b) -> b
snd t (a, [Kind])
cstrs)])

        declGroup :: SCC (String, [(String, Kind)], [(String, [Kind])]) -> [Text]
declGroup (DG.AcyclicSCC (String, [(String, Kind)], [(String, [Kind])])
d )  = (String, [(String, Kind)], [(String, [Kind])]) -> [Text]
singleADT (String, [(String, Kind)], [(String, [Kind])])
d
        declGroup (DG.CyclicSCC  [(String, [(String, Kind)], [(String, [Kind])])]
ds)
            = case [(String, [(String, Kind)], [(String, [Kind])])]
ds of
                []  -> String -> [Text]
forall a. HasCallStack => String -> a
error String
"Data.SBV.declADT: Impossible happened: an empty cyclic group was returned!"
                [(String, [(String, Kind)], [(String, [Kind])])
d] -> (String, [(String, Kind)], [(String, [Kind])]) -> [Text]
singleADT (String, [(String, Kind)], [(String, [Kind])])
d
                [(String, [(String, Kind)], [(String, [Kind])])]
_   -> [(String, [(String, Kind)], [(String, [Kind])])] -> [Text]
multiADT [(String, [(String, Kind)], [(String, [Kind])])]
ds

        parParens :: [(String, Kind)] -> (Text, Text)
        parParens :: [(String, Kind)] -> (Text, Text)
parParens [] = (Text
"", Text
"")
        parParens [(String, Kind)]
ps = (Text
" (par (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords (((String, Kind) -> Text) -> [(String, Kind)] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Text
T.pack (String -> Text)
-> ((String, Kind) -> String) -> (String, Kind) -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Kind) -> String
forall a b. (a, b) -> a
fst) [(String, Kind)]
ps) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")", Text
")")

        mkC :: (String, [Kind]) -> Text
mkC (String
nm, []) = String -> Text
T.pack String
nm
        mkC (String
nm, [Kind]
ts) = String -> Text
T.pack String
nm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords [Char
'(' Char -> Text -> Text
`T.cons` String -> Kind -> Text
mkF (String
nm String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
"_" String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i) Kind
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")" | (Int
i, Kind
t) <- [Int] -> [Kind] -> [(Int, Kind)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Int
1::Int)..] [Kind]
ts]
          where mkF :: String -> Kind -> Text
mkF String
a Kind
t  = Text
"get" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack String
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Kind -> String
smtType Kind
t)

        singleADT :: (String, [(String, Kind)], [(String, [Kind])]) -> [Text]
        singleADT :: (String, [(String, Kind)], [(String, [Kind])]) -> [Text]
singleADT (String
tName, [], []) = [Text
"(declare-sort " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack String
tName Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" 0) ; N.B. Uninterpreted sort."]
        singleADT (String
tName, [(String, Kind)]
pks, [(String, [Kind])]
cstrs) = (Text
"; User defined ADT: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack String
tName) Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
decl
          where decl :: [Text]
decl =  (Text
"(declare-datatype " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack String
tName Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
parOpen Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" (")
                     Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
:  [Text
"    (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (String, [Kind]) -> Text
mkC (String, [Kind])
c Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")" | (String, [Kind])
c <- [(String, [Kind])]
cstrs]
                     [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [Text
"))" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
parClose]

                (Text
parOpen, Text
parClose) = [(String, Kind)] -> (Text, Text)
parParens [(String, Kind)]
pks

        multiADT :: [(String, [(String, Kind)], [(String, [Kind])])] -> [Text]
        multiADT :: [(String, [(String, Kind)], [(String, [Kind])])] -> [Text]
multiADT [(String, [(String, Kind)], [(String, [Kind])])]
adts = (Text
"; User defined mutually-recursive ADTs: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
T.intercalate Text
", " (((String, [(String, Kind)], [(String, [Kind])]) -> Text)
-> [(String, [(String, Kind)], [(String, [Kind])])] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (\(String
a, [(String, Kind)]
_, [(String, [Kind])]
_) -> String -> Text
T.pack String
a) [(String, [(String, Kind)], [(String, [Kind])])]
adts)) Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
decl
          where decl :: [Text]
decl = (Text
"(declare-datatypes (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
typeDecls Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") (")
                     Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: ((String, [(String, Kind)], [(String, [Kind])]) -> [Text])
-> [(String, [(String, Kind)], [(String, [Kind])])] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String, [(String, Kind)], [(String, [Kind])]) -> [Text]
forall {a}. (a, [(String, Kind)], [(String, [Kind])]) -> [Text]
adtBody [(String, [(String, Kind)], [(String, [Kind])])]
adts
                    [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [Text
"))"]

                typeDecls :: Text
typeDecls = [Text] -> Text
T.unwords [Char
'(' Char -> Text -> Text
`T.cons` String -> Text
T.pack String
name Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Int -> String
forall a. Show a => a -> String
show ([(String, Kind)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(String, Kind)]
pks)) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")" | (String
name, [(String, Kind)]
pks, [(String, [Kind])]
_) <- [(String, [(String, Kind)], [(String, [Kind])])]
adts]

                adtBody :: (a, [(String, Kind)], [(String, [Kind])]) -> [Text]
adtBody (a
_, [(String, Kind)]
pks, [(String, [Kind])]
cstrs) = [Text]
body
                  where (Text
parOpen, Text
parClose) = [(String, Kind)] -> (Text, Text)
parParens [(String, Kind)]
pks
                        body :: [Text]
body =  (Text
"    " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
parOpen Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" (")
                             Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
:  [Text
"        (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (String, [Kind]) -> Text
mkC (String, [Kind])
c Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")" | (String, [Kind])
c <- [(String, [Kind])]
cstrs]
                             [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [Text
"     )" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
parClose]

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

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

        proj :: a -> Text
proj a
i = Text
"(proj_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (a -> String
forall a. Show a => a -> String
show a
i) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_SBVTuple" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Int -> String
forall a. Show a => a -> String
show Int
arity) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall {a}. Show a => a -> Text
param a
i Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

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

        param :: a -> Text
param a
i = Text
"T" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (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 @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

-- 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 :: [Text]
declRationals :: [Text]
declRationals = [ Text
"(declare-datatype SBVRational ((SBV.Rational (sbv.rat.numerator Int) (sbv.rat.denominator Int))))"
                , Text
""
                , Text
"(define-fun sbv.rat.eq ((x SBVRational) (y SBVRational)) Bool"
                , Text
"   (= (* (sbv.rat.numerator   x) (sbv.rat.denominator y))"
                , Text
"      (* (sbv.rat.denominator x) (sbv.rat.numerator   y)))"
                , Text
")"
                , Text
""
                , Text
"(define-fun sbv.rat.notEq ((x SBVRational) (y SBVRational)) Bool"
                , Text
"   (not (sbv.rat.eq x y))"
                , Text
")"
                ]

-- | 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 [Text]
cvtInc :: SMTLibIncConverter [Text]
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?
               [Text]
settings
            -- sorts
            [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [(String, [(String, Kind)], [(String, [Kind])])] -> [Text]
declADT [(String
s, [(String, Kind)]
pks, [(String, [Kind])]
cs) | k :: Kind
k@(KADT String
s [(String, Kind)]
pks [(String, [Kind])]
cs) <- [Kind]
newKinds, Bool -> Bool
not (Kind -> Bool
forall a. HasKind a => a -> Bool
isRoundingMode Kind
k)]
            -- tuples. NB. Only declare the new sizes, old sizes persist.
            [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> (Int -> [Text]) -> [Int] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Int -> [Text]
declTuple (Set Kind -> [Int]
findTupleArities Set Kind
newKs)
            -- constants
            [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> ((SV, CV) -> [Text]) -> [(SV, CV)] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SMTConfig -> (SV, CV) -> [Text]
declConst SMTConfig
cfg) [(SV, CV)]
consts
            -- inputs
            [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> (NamedSymVar -> [Text]) -> [NamedSymVar] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap NamedSymVar -> [Text]
declInp [NamedSymVar]
inps
            -- uninterpreteds
            [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> ((String, (Bool, Maybe [String], SBVType)) -> [Text])
-> [(String, (Bool, Maybe [String], SBVType))] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ProgInfo -> (String, (Bool, Maybe [String], SBVType)) -> [Text]
declUI ProgInfo
curProgInfo) [(String, (Bool, Maybe [String], SBVType))]
uis
            -- table declarations
            [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [Text]
tableDecls
            -- expressions
            [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> ((SV, SBVExpr) -> [Text]) -> Seq (SV, SBVExpr) -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ProgInfo -> SMTConfig -> TableMap -> (SV, SBVExpr) -> [Text]
declDef ProgInfo
curProgInfo SMTConfig
cfg TableMap
tableMap) Seq (SV, SBVExpr)
asgnsSeq
            -- table setups
            [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [[Text]] -> [Text]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Text]]
tableAssigns
            -- extra constraints
            [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> ((Bool, [(String, String)], SV) -> Text)
-> [(Bool, [(String, String)], SV)] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (\(Bool
isSoft, [(String, String)]
attr, SV
v) -> Text
"(assert" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (if Bool
isSoft then Text
"-soft " else Text
" ") Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [(String, String)] -> Text -> Text
addAnnotations [(String, String)]
attr (SV -> Text
cvtSV SV
v) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")") (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 -> [Text]
declInp (NamedSymVar -> SV
getSV -> SV
s) = SV -> SBVType -> Maybe Text -> [Text]
declareFun SV
s ([Kind] -> SBVType
SBVType [SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
s]) Maybe Text
forall a. Maybe a
Nothing

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

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

        -- If we need flattening in models, do emit the required lines if preset
        settings :: [Text]
settings
          | (Kind -> Bool) -> [Kind] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
needsFlattening [Kind]
newKinds
          = [[Text]] -> [Text]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([Maybe [Text]] -> [[Text]]
forall a. [Maybe a] -> [a]
catMaybes [(String -> Text) -> [String] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map String -> Text
T.pack ([String] -> [Text]) -> Maybe [String] -> Maybe [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) -> [Text]
declDef :: ProgInfo -> SMTConfig -> TableMap -> (SV, SBVExpr) -> [Text]
declDef ProgInfo
curProgInfo SMTConfig
cfg TableMap
tableMap (SV
s, SBVExpr
expr) =
        case SBVExpr
expr of
          SBVApp  (Label String
m) [SV
e] -> SMTConfig -> (SV, Text) -> Maybe Text -> [Text]
defineFun SMTConfig
cfg (SV
s, SV -> Text
cvtSV                                   SV
e) (Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack String
m)
          SBVExpr
e                     -> SMTConfig -> (SV, Text) -> Maybe Text -> [Text]
defineFun SMTConfig
cfg (SV
s, SMTConfig
-> ProgInfo
-> SolverCapabilities
-> RoundingMode
-> TableMap
-> SBVExpr
-> Text
cvtExp SMTConfig
cfg ProgInfo
curProgInfo SolverCapabilities
caps RoundingMode
rm TableMap
tableMap SBVExpr
e) Maybe Text
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, Text) -> Maybe Text -> [Text]
defineFun :: SMTConfig -> (SV, Text) -> Maybe Text -> [Text]
defineFun SMTConfig
cfg (SV
s, Text
def) Maybe Text
mbComment
   | Bool
hasDefFun = [Text
"(define-fun "  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
varT Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
def Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
cmnt]
   | Bool
True      = [ Text
"(declare-fun " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
varT Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
cmnt
                 , Text
"(assert (= " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
var Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
def Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"))"
                 ]
  where var :: Text
var  = String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ SV -> String
forall a. Show a => a -> String
show SV
s
        varT :: Text
varT = Text
var Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [SV] -> SV -> Text
svFunType [] SV
s
        cmnt :: Text
cmnt = Text -> (Text -> Text) -> Maybe Text -> Text
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Text
"" (Text
" ; " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>) Maybe Text
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) -> [Text]
declConst :: SMTConfig -> (SV, CV) -> [Text]
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, Text) -> Maybe Text -> [Text]
defineFun SMTConfig
cfg (SV
s, RoundingMode -> CV -> Text
cvtCV (SMTConfig -> RoundingMode
roundingMode SMTConfig
cfg) CV
c) Maybe Text
forall a. Maybe a
Nothing

-- Make a function equality of nm against the internal function fun
mkRelEq :: Text -> (Text, Text) -> Kind -> Text
mkRelEq :: Text -> (Text, Text) -> Kind -> Text
mkRelEq Text
nm (Text
fun, Text
order) Kind
ak = Text
res
   where lhs :: Text
lhs = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
nm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" x y)"
         rhs :: Text
rhs = Text
"((_ " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
fun Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
order Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") x y)"
         tk :: Text
tk  = String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Kind -> String
smtType Kind
ak
         res :: Text
res = Text
"(forall ((x " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
tk Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") (y " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
tk Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")) (= " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
lhs Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
rhs Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"))"

declUI :: ProgInfo -> (String, (Bool, Maybe [String], SBVType)) -> [Text]
declUI :: ProgInfo -> (String, (Bool, Maybe [String], SBVType)) -> [Text]
declUI ProgInfo{[(String, String)]
progTransClosures :: [(String, String)]
progTransClosures :: ProgInfo -> [(String, String)]
progTransClosures} (String
i, (Bool
_, Maybe [String]
_, SBVType
t)) = Text -> SBVType -> Maybe Text -> [Text]
declareName (String -> Text
T.pack String
i) SBVType
t Maybe Text
forall a. Maybe a
Nothing [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [Text]
declClosure
  where declClosure :: [Text]
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
                    =  Text -> SBVType -> Maybe Text -> [Text]
declareName (String -> Text
T.pack String
external) SBVType
t Maybe Text
forall a. Maybe a
Nothing
                    [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [Text
"(assert " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> (Text, Text) -> Kind -> Text
mkRelEq (String -> Text
T.pack String
external) (Text
"transitive-closure", String -> Text
T.pack String
i) (SBVType -> Kind
argKind SBVType
t) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"]
                    | 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. Semigroup 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 :: [(String, (SMTDef, SBVType))] -> [Text]
declUserFuns :: [(String, (SMTDef, SBVType))] -> [Text]
declUserFuns [(String, (SMTDef, SBVType))]
ds = (SCC (String, (SMTDef, SBVType)) -> Text)
-> [SCC (String, (SMTDef, SBVType))] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SCC (String, (SMTDef, SBVType)) -> Text
forall {a}. Show a => SCC (String, (SMTDef, a)) -> Text
declGroup [SCC (String, (SMTDef, SBVType))]
sorted
  where mkNode :: (a, (SMTDef, b)) -> ((a, (SMTDef, b)), a, [String])
mkNode (a, (SMTDef, b))
d = ((a, (SMTDef, b))
d, (a, (SMTDef, b)) -> a
forall a b. (a, b) -> a
fst (a, (SMTDef, b))
d, (a, (SMTDef, b)) -> [String]
forall {a} {b}. (a, (SMTDef, b)) -> [String]
getDeps (a, (SMTDef, b))
d)

        getDeps :: (a, (SMTDef, b)) -> [String]
getDeps (a
_, (SMTDef Kind
_ [String]
d Maybe String
_ Int -> String
_, b
_)) = [String]
d

        mkDecl :: Maybe String -> Text -> Text
mkDecl Maybe String
Nothing  Text
rt = Text
"() " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
rt
        mkDecl (Just String
p) Text
rt = String -> Text
T.pack String
p Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
rt

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

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

        declUserDef :: Bool -> (String, (SMTDef, a)) -> Text
declUserDef Bool
isRec (String
nm, (SMTDef Kind
fk [String]
deps Maybe String
param Int -> String
body, a
ty)) =
          Text
"; " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack String
nm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" :: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (a -> String
forall a. Show a => a -> String
show a
ty) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
recursive Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
frees Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
s
           where (Text
recursive, Text
definer) | Bool
isRec = (Text
" [Recursive]", Text
"define-fun-rec")
                                      | Bool
True  = (Text
"",             Text
"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 :: Text
frees | [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
otherDeps = Text
""
                       | Bool
True           = Text
" [Refers to: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
T.intercalate Text
", " ((String -> Text) -> [String] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map String -> Text
T.pack [String]
otherDeps) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"]"

                 decl :: Text
decl = Maybe String -> Text -> Text
mkDecl Maybe String
param (String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Kind -> String
smtType Kind
fk)

                 s :: Text
s = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
definer Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack String
nm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
decl Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Int -> String
body Int
2) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

        -- declare a bunch of mutually-recursive functions
        declUserDefMulti :: [(String, (SMTDef, a))] -> Text
declUserDefMulti [(String, (SMTDef, a))]
bs = [([String], String, a, Text, String)] -> Text
forall {a}. Show a => [([String], String, a, Text, String)] -> Text
render ([([String], String, a, Text, String)] -> Text)
-> [([String], String, a, Text, String)] -> Text
forall a b. (a -> b) -> a -> b
$ ((String, (SMTDef, a)) -> ([String], String, a, Text, String))
-> [(String, (SMTDef, a))] -> [([String], String, a, Text, String)]
forall a b. (a -> b) -> [a] -> [b]
map (String, (SMTDef, a)) -> ([String], String, a, Text, String)
forall {c}.
(String, (SMTDef, c)) -> ([String], String, c, Text, String)
collect [(String, (SMTDef, a))]
bs
          where collect :: (String, (SMTDef, c)) -> ([String], String, c, Text, String)
collect (String
nm, (SMTDef Kind
fk [String]
deps Maybe String
param Int -> String
body, c
ty)) = ([String]
deps, String
nm, c
ty, Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack String
nm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
decl Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")", Int -> String
body Int
3)
                  where decl :: Text
decl = Maybe String -> Text -> Text
mkDecl Maybe String
param (String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Kind -> String
smtType Kind
fk)

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

                           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) -> Text
dump ([String]
deps, String
nm, a
ty, d
_, String
body) = Text
"; Definition of: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack String
nm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" :: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (a -> String
forall a. Show a => a -> String
show a
ty) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
". [Refers to: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
T.intercalate Text
", " ((String -> Text) -> [String] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map String -> Text
T.pack [String]
deps) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"]"
                                                        Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack String
body

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

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

mkTable :: (((Int, Kind, Kind), [SV]), [Text]) -> (Text, [Text])
mkTable :: (((Int, Kind, Kind), [SV]), [Text]) -> (Text, [Text])
mkTable (((Int
i, Kind
ak, Kind
rk), [SV]
_elts), [Text]
is) = (Text
decl, (Int -> Text -> Text) -> [Int] -> [Text] -> [Text]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Text -> Text
wrap [(Int
0::Int)..] [Text]
is [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [Text]
setup)
  where t :: Text
t       = Text
"table" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Int -> String
forall a. Show a => a -> String
show Int
i)
        decl :: Text
decl    = Text
"(declare-fun " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Kind -> String
smtType Kind
ak) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Kind -> String
smtType Kind
rk) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

        -- Arrange for initializers
        mkInit :: Int -> Text
mkInit Int
idx   = Text
"table" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Int -> String
forall a. Show a => a -> String
show Int
i) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_initializer_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Int -> String
forall a. Show a => a -> String
show (Int
idx :: Int))
        initializer :: Text
initializer  = Text
"table" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Int -> String
forall a. Show a => a -> String
show Int
i) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_initializer"

        wrap :: Int -> Text -> Text
wrap Int
index Text
s = Text
"(define-fun " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
mkInit Int
index Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" () Bool " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
s Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

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

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

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

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

        mkElt :: SV -> p -> (Bool, (Text, Text))
mkElt SV
x p
k   = (Bool
isReady, (Text
idx, SV -> Text
cvtSV SV
x))
          where idx :: Text
idx = RoundingMode -> CV -> Text
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 :: (Text, Text) -> Text
mkEntry (Text
idx, Text
v) = Text
"(= (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
idx Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
v Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

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

svType :: SV -> Text
svType :: SV -> Text
svType SV
s = String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Kind -> String
smtType (SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
s)

svFunType :: [SV] -> SV -> Text
svFunType :: [SV] -> SV -> Text
svFunType [SV]
ss SV
s = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords ((SV -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
svType [SV]
ss) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
svType SV
s

cvtType :: SBVType -> Text
cvtType :: SBVType -> Text
cvtType (SBVType []) = String -> Text
forall a. HasCallStack => String -> a
error String
"SBV.SMT.SMTLib2.cvtType: internal: received an empty type!"
cvtType (SBVType [Kind]
xs) = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords ((Kind -> Text) -> [Kind] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (String -> Text
T.pack (String -> Text) -> (Kind -> String) -> Kind -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> String
smtType) [Kind]
body) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (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 Text

-- Present an SV, simply show
cvtSV :: SV -> Text
cvtSV :: SV -> Text
cvtSV = String -> Text
T.pack (String -> Text) -> (SV -> String) -> SV -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SV -> String
forall a. Show a => a -> String
show

cvtCV :: RoundingMode -> CV -> Text
cvtCV :: RoundingMode -> CV -> Text
cvtCV = String -> Text
T.pack (String -> Text)
-> (RoundingMode -> CV -> String) -> RoundingMode -> CV -> Text
forall {b} {c} {a} {a}. (b -> c) -> (a -> a -> b) -> a -> a -> c
.* RoundingMode -> CV -> String
cvToSMTLib
  where .* :: (b -> c) -> (a -> a -> b) -> a -> a -> c
(.*) = ((a -> b) -> a -> c) -> (a -> a -> b) -> a -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) (((a -> b) -> a -> c) -> (a -> a -> b) -> a -> a -> c)
-> ((b -> c) -> (a -> b) -> a -> c)
-> (b -> c)
-> (a -> a -> b)
-> a
-> a
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)

getTable :: TableMap -> Int -> Text
getTable :: TableMap -> Int -> Text
getTable TableMap
m Int
i
  | Just Text
tn <- Int
i Int -> TableMap -> Maybe Text
forall a. Int -> IntMap a -> Maybe a
`IM.lookup` TableMap
m = Text
tn
  | Bool
True                       = Text
"table" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Int -> String
forall a. Show a => a -> String
show Int
i)

cvtExp :: SMTConfig -> ProgInfo -> SolverCapabilities -> RoundingMode -> TableMap -> SBVExpr -> Text
cvtExp :: SMTConfig
-> ProgInfo
-> SolverCapabilities
-> RoundingMode
-> TableMap
-> SBVExpr
-> Text
cvtExp SMTConfig
cfg ProgInfo
curProgInfo SolverCapabilities
caps RoundingMode
rm TableMap
tableMap expr :: SBVExpr
expr@(SBVApp Op
_ [SV]
arguments) = SBVExpr -> Text
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 :: a
bad | Bool
intOp = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
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 -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
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 {a}. a
bad
        ensureBV :: Bool
ensureBV       = Bool
bvOp Bool -> Bool -> Bool
|| Bool
forall {a}. a
bad

        addRM :: Text -> Text
addRM Text
s = Text
s Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (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 :: a -> p -> [a] -> a
lift2  a
o p
_ [a
x, a
y] = a
"(" a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
o a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
" " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
" " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
y a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
")"
        lift2  a
o p
_ [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.lift2: Unexpected arguments: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (a, [a]) -> String
forall a. Show a => a -> String
show (a
o, [a]
sbvs)

        -- lift an arbitrary arity operator
        liftN :: Text -> p -> [Text] -> Text
liftN Text
o p
_ [Text]
xs = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
o Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords [Text]
xs Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

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

        lift1FP :: a -> a -> p -> [a] -> a
lift1FP a
o a
fo | Bool
fpOp = a -> p -> [a] -> a
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> p -> [a] -> a
lift1 a
fo
                     | Bool
True = a -> p -> [a] -> a
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> p -> [a] -> a
lift1 a
o

        liftAbs :: Bool -> [Text] -> Text
liftAbs Bool
sgned [Text]
args | Bool
fpOp        = Text -> Bool -> [Text] -> Text
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> p -> [a] -> a
lift1 Text
"fp.abs" Bool
sgned [Text]
args
                           | Bool
intOp       = Text -> Bool -> [Text] -> Text
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> p -> [a] -> a
lift1 Text
"abs"    Bool
sgned [Text]
args
                           | Bool
bvOp, Bool
sgned = Text -> Text -> Text -> Text
mkAbs Text
fArg Text
"bvslt" Text
"bvneg"
                           | Bool
bvOp        = Text
fArg
                           | Bool
True        = Text -> Text -> Text -> Text
mkAbs Text
fArg Text
"<"     Text
"-"
          where fArg :: Text
fArg = String -> [Text] -> Text
forall {a}. String -> [a] -> a
hd String
"liftAbs" [Text]
args
                mkAbs :: Text -> Text -> Text -> Text
mkAbs Text
x Text
cmp Text
neg = Text
"(ite " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ltz Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
nx Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
                  where ltz :: Text
ltz = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
cmp Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
z Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
                        nx :: Text
nx  = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
neg Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
                        z :: Text
z   = RoundingMode -> CV -> Text
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 :: a -> a -> p -> [a] -> a
lift2B a
bOp a
vOp
          | Bool
boolOp = a -> p -> [a] -> a
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> p -> [a] -> a
lift2 a
bOp
          | Bool
True   = a -> p -> [a] -> a
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> p -> [a] -> a
lift2 a
vOp

        lift1B :: a -> a -> p -> [a] -> a
lift1B a
bOp a
vOp
          | Bool
boolOp = a -> p -> [a] -> a
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> p -> [a] -> a
lift1 a
bOp
          | Bool
True   = a -> p -> [a] -> a
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> p -> [a] -> a
lift1 a
vOp

        eqBV :: p -> [Text] -> Text
eqBV  = Text -> p -> [Text] -> Text
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> p -> [a] -> a
lift2 Text
"="
        neqBV :: p -> [Text] -> Text
neqBV = Text -> p -> [Text] -> Text
forall {p}. Text -> p -> [Text] -> Text
liftN Text
"distinct"

        equal :: p -> [a] -> a
equal p
sgn [a]
sbvs
          | Bool
fpOp = a -> p -> [a] -> a
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> p -> [a] -> a
lift2 a
"fp.eq" p
sgn [a]
sbvs
          | Bool
True = a -> p -> [a] -> a
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> p -> [a] -> a
lift2 a
"="     p
sgn [a]
sbvs

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

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

        lift2S :: a -> a -> Bool -> [a] -> a
lift2S a
oU a
oS Bool
sgn = a -> Bool -> [a] -> a
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> p -> [a] -> a
lift2 (if Bool
sgn then a
oS else a
oU) Bool
sgn
        liftNS :: Text -> Text -> Bool -> [Text] -> Text
liftNS Text
oU Text
oS Bool
sgn = Text -> Bool -> [Text] -> Text
forall {p}. Text -> p -> [Text] -> Text
liftN (if Bool
sgn then Text
oS else Text
oU) Bool
sgn

        lift2Cmp :: a -> a -> p -> [a] -> a
lift2Cmp a
o a
fo | Bool
fpOp = a -> p -> [a] -> a
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> p -> [a] -> a
lift2 a
fo
                      | Bool
True = a -> p -> [a] -> a
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> p -> [a] -> a
lift2 a
o

        stringOrChar :: Kind -> Bool
stringOrChar Kind
KString = Bool
True
        stringOrChar Kind
KChar   = Bool
True
        stringOrChar Kind
_       = Bool
False
        stringCmp :: Bool -> a -> [a] -> a
stringCmp Bool
swap a
o [a
a, a
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 (a
a1, a
a2) | Bool
swap = (a
b, a
a)
                         | Bool
True = (a
a, a
b)
            in a
"(" a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
o a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
" " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
a1 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
" " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
a2 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
")"
        stringCmp Bool
_ a
o [a]
sbvs = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.sh.stringCmp: Unexpected arguments: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (a, [a]) -> String
forall a. Show a => a -> String
show (a
o, [a]
sbvs)

        -- NB. Likewise for sequences
        seqCmp :: Bool -> a -> [a] -> a
seqCmp Bool
swap a
o [a
a, a
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 (a
a1, a
a2) | Bool
swap = (a
b, a
a)
                         | Bool
True = (a
a, a
b)
            in a
"(" a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
o a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
" " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
a1 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
" " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
a2 a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
")"
        seqCmp Bool
_ a
o [a]
sbvs = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.sh.seqCmp: Unexpected arguments: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (a, [a]) -> String
forall a. Show a => a -> String
show (a
o, [a]
sbvs)

        lift1 :: a -> p -> [a] -> a
lift1  a
o p
_ [a
x]    = a
"(" a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
o a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
" " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
")"
        lift1  a
o p
_ [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.lift1: Unexpected arguments: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (a, [a]) -> String
forall a. Show a => a -> String
show (a
o, [a]
sbvs)

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

        sh (SBVApp (LkUp (Int
t, Kind
aKnd, Kind
_, Int
l) SV
i SV
e) [])
          | Bool
needsCheck = Text
"(ite " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
cond Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
e Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
lkUp Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
          | Bool
True       = Text
lkUp
          where unexpected :: a
unexpected = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: Unexpected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
forall a. Show a => a -> String
show Kind
aKnd
                needsCheck :: Bool
needsCheck = case Kind
aKnd of
                              KVar{}        -> Bool
forall {a}. a
unexpected
                              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
                              KApp String
_ [Kind]
_      -> Bool
forall {a}. a
unexpected
                              KADT String
_ [(String, Kind)]
_ [(String, [Kind])]
_    -> Bool
forall {a}. a
unexpected
                              Kind
KReal         -> Bool
forall {a}. a
unexpected
                              Kind
KFloat        -> Bool
forall {a}. a
unexpected
                              Kind
KDouble       -> Bool
forall {a}. a
unexpected
                              KFP Int
_ Int
_       -> Bool
forall {a}. a
unexpected
                              Kind
KRational     -> Bool
forall {a}. a
unexpected
                              Kind
KChar         -> Bool
forall {a}. a
unexpected
                              Kind
KString       -> Bool
forall {a}. a
unexpected
                              KList Kind
_       -> Bool
forall {a}. a
unexpected
                              KSet  Kind
_       -> Bool
forall {a}. a
unexpected
                              KTuple [Kind]
_      -> Bool
forall {a}. a
unexpected
                              KArray  Kind
_ Kind
_   -> Bool
forall {a}. a
unexpected

                lkUp :: Text
lkUp = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> TableMap -> Int -> Text
getTable TableMap
tableMap Int
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
i Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

                cond :: Text
cond
                 | SV -> Bool
forall a. HasKind a => a -> Bool
hasSign SV
i = Text
"(or " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
le0 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
gtl Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") "
                 | Bool
True      = Text
gtl Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" "

                (Text
less, Text
leq) = case Kind
aKnd of
                                KVar{}        -> String -> (Text, Text)
forall a. HasCallStack => String -> a
error String
"SBV.SMT.SMTLib2.cvtExp: unexpected variable index"
                                Kind
KBool         -> String -> (Text, Text)
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 (Text
"bvslt", Text
"bvsle") else (Text
"bvult", Text
"bvule")
                                Kind
KUnbounded    -> (Text
"<", Text
"<=")
                                Kind
KReal         -> (Text
"<", Text
"<=")
                                Kind
KFloat        -> (Text
"fp.lt", Text
"fp.leq")
                                Kind
KDouble       -> (Text
"fp.lt", Text
"fp.leq")
                                Kind
KRational     -> (Text
"sbv.rat.lt", Text
"sbv.rat.leq")
                                KFP{}         -> (Text
"fp.lt", Text
"fp.leq")
                                Kind
KChar         -> String -> (Text, Text)
forall a. HasCallStack => String -> a
error String
"SBV.SMT.SMTLib2.cvtExp: unexpected string valued index"
                                Kind
KString       -> String -> (Text, Text)
forall a. HasCallStack => String -> a
error String
"SBV.SMT.SMTLib2.cvtExp: unexpected string valued index"
                                KApp  String
s [Kind]
_     -> String -> (Text, Text)
forall a. HasCallStack => String -> a
error (String -> (Text, Text)) -> String -> (Text, Text)
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: unexpected ADT applied index: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
                                KADT  String
s [(String, Kind)]
_ [(String, [Kind])]
_   -> String -> (Text, Text)
forall a. HasCallStack => String -> a
error (String -> (Text, Text)) -> String -> (Text, Text)
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp: unexpected ADT valued index: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s
                                KList Kind
k       -> String -> (Text, Text)
forall a. HasCallStack => String -> a
error (String -> (Text, Text)) -> String -> (Text, Text)
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 -> (Text, Text)
forall a. HasCallStack => String -> a
error (String -> (Text, Text)) -> String -> (Text, Text)
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 -> (Text, Text)
forall a. HasCallStack => String -> a
error (String -> (Text, Text)) -> String -> (Text, Text)
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
                                KArray  Kind
k1 Kind
k2 -> String -> (Text, Text)
forall a. HasCallStack => String -> a
error (String -> (Text, Text)) -> String -> (Text, Text)
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 -> Text
mkCnst = RoundingMode -> CV -> Text
cvtCV RoundingMode
rm (CV -> Text) -> (Int -> CV) -> Int -> Text
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 :: Text
le0  = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
less Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
i Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
mkCnst Int
0 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
                gtl :: Text
gtl  = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
leq  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
mkCnst Int
l Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
i Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

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

        sh (SBVApp (ArrayInit (Left (Kind
f, Kind
t))) [SV
a])   = Text
"((as const (Array " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Kind -> String
smtType Kind
f) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Kind -> String
smtType Kind
t) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")) " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
        sh (SBVApp (ArrayInit (Right SMTLambda
s)) [])        = String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ SMTLambda -> String
forall a. Show a => a -> String
show SMTLambda
s
        sh (SBVApp Op
ReadArray             [SV
a, SV
i])    = Text
"(select " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
i Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
        sh (SBVApp Op
WriteArray            [SV
a, SV
i, SV
e]) = Text
"(store "  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
i Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
e Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

        sh (SBVApp (Uninterpreted String
nm) [])   = String -> Text
T.pack String
nm
        sh (SBVApp (Uninterpreted String
nm) [SV]
args) = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack String
nm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords ((SV -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
cvtSV [SV]
args) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

        sh (SBVApp (ADTOp ADTOp
aop) [SV]
args) = SolverCapabilities -> ADTOp -> [SV] -> Text
handleADT SolverCapabilities
caps ADTOp
aop [SV]
args

        sh (SBVApp (QuantifiedBool String
i) [])   = String -> Text
T.pack String
i
        sh (SBVApp (QuantifiedBool String
i) [SV]
args) = String -> Text
forall a. HasCallStack => String -> a
error (String -> Text) -> String -> Text
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 -> Text
forall a. HasCallStack => String -> a
error (String -> Text) -> String -> Text
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 -> Text
asrt String
nm String
fun = Text -> (Text, Text) -> Kind -> Text
mkRelEq (String -> Text
T.pack String
nm) (String -> Text
T.pack String
fun, String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
order) Kind
k
            in case SpecialRelOp
o of
                 IsPartialOrder         String
nm -> String -> String -> Text
asrt String
nm String
"partial-order"
                 IsLinearOrder          String
nm -> String -> String -> Text
asrt String
nm String
"linear-order"
                 IsTreeOrder            String
nm -> String -> String -> Text
asrt String
nm String
"tree-order"
                 IsPiecewiseLinearOrder String
nm -> String -> String -> Text
asrt String
nm String
"piecewise-linear-order"

        sh (SBVApp (Divides Integer
n) [SV
a]) = Text
"((_ divisible " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Integer -> String
forall a. Show a => a -> String
show Integer
n) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

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

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

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

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

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

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

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

        sh (SBVApp Op
op [SV]
args)
          | Just Bool -> [Text] -> Text
f <- Op
-> [(Op, Bool -> [Text] -> Text)] -> Maybe (Bool -> [Text] -> Text)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, Bool -> [Text] -> Text)]
forall {p}. [(Op, p -> [Text] -> Text)]
smtBVOpTable, Bool
ensureBVOrBool
          = Bool -> [Text] -> Text
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 -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
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 -> [Text] -> Text)]
smtBVOpTable = [ (Op
And,  Text -> Text -> p -> [Text] -> Text
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> a -> p -> [a] -> a
lift2B Text
"and" Text
"bvand")
                               , (Op
Or,   Text -> Text -> p -> [Text] -> Text
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> a -> p -> [a] -> a
lift2B Text
"or"  Text
"bvor")
                               , (Op
XOr,  Text -> Text -> p -> [Text] -> Text
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> a -> p -> [a] -> a
lift2B Text
"xor" Text
"bvxor")
                               , (Op
Not,  Text -> Text -> p -> [Text] -> Text
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> a -> p -> [a] -> a
lift1B Text
"not" Text
"bvnot")
                               , (Op
Join, Text -> p -> [Text] -> Text
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> p -> [a] -> a
lift2 Text
"concat")
                               ]

        sh (SBVApp (Label String
_) [SV
a]) = SV -> Text
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 -> Text -> Text -> Text
handleFPCast Kind
kFrom Kind
kTo (SV -> Text
cvtSV SV
m) ([Text] -> Text
T.unwords ((SV -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
cvtSV [SV]
args))
        sh (SBVApp (IEEEFP FPOp
w                    ) [SV]
args) = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (FPOp -> String
forall a. Show a => a -> String
show FPOp
w) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords ((SV -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
cvtSV [SV]
args) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

        -- 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   = Text
"(^ "    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" 0.5)"
                                               | Bool
isCVC5 = Text
"(sqrt " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>     Text
")"

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

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

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

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

        -- Note the unfortunate reversal in StrInRe..
        sh (SBVApp (StrOp (StrInRe RegExp
r)) [SV]
args) = Text
"(str.in_re " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords ((SV -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
cvtSV [SV]
args) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (RegExp -> String
regExpToSMTString RegExp
r) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
        sh (SBVApp (StrOp StrOp
op)          [SV]
args) = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (StrOp -> String
forall a. Show a => a -> String
show StrOp
op) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords ((SV -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
cvtSV [SV]
args) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

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

        -- Sequences. The only interesting thing here is that unit over KChar is a no-op since SMTLib doesn't distinguish
        -- Strings and Characters, but SBV does.
        sh (SBVApp (SeqOp (SeqUnit Kind
KChar)) [SV
a]) = SV -> Text
cvtSV SV
a
        sh (SBVApp (SeqOp SeqOp
op)             [SV]
args) = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (SeqOp -> String
forall a. Show a => a -> String
show SeqOp
op) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords ((SV -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
cvtSV [SV]
args) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

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

        sh (SBVApp (TupleConstructor Int
0)   [])    = Text
"mkSBVTuple0"
        sh (SBVApp (TupleConstructor Int
n)   [SV]
args)  = Text
"((as mkSBVTuple" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Int -> String
forall a. Show a => a -> String
show Int
n) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (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))) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords ((SV -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
cvtSV [SV]
args) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
        sh (SBVApp (TupleAccess      Int
i Int
n) [SV
tup]) = Text
"(proj_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Int -> String
forall a. Show a => a -> String
show Int
i) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_SBVTuple" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Int -> String
forall a. Show a => a -> String
show Int
n) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
tup Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

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

        sh (SBVApp Op
Implies [SV
a, SV
b]) = Text
"(=> " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
b Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

        sh inp :: SBVExpr
inp@(SBVApp Op
op [SV]
args)
          | Bool
intOp, Just Bool -> [Text] -> Text
f <- Op
-> [(Op, Bool -> [Text] -> Text)] -> Maybe (Bool -> [Text] -> Text)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, Bool -> [Text] -> Text)]
smtOpIntTable
          = Bool -> [Text] -> Text
f Bool
True ((SV -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
cvtSV [SV]
args)
          | Bool
boolOp, Just [Text] -> Text
f <- Op -> [(Op, [Text] -> Text)] -> Maybe ([Text] -> Text)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, [Text] -> Text)]
boolComps
          = [Text] -> Text
f ((SV -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
cvtSV [SV]
args)
          | Bool
bvOp, Just Bool -> [Text] -> Text
f <- Op
-> [(Op, Bool -> [Text] -> Text)] -> Maybe (Bool -> [Text] -> Text)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, Bool -> [Text] -> Text)]
smtOpBVTable
          = Bool -> [Text] -> Text
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 -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
cvtSV [SV]
args)
          | Bool
realOp, Just Bool -> [Text] -> Text
f <- Op
-> [(Op, Bool -> [Text] -> Text)] -> Maybe (Bool -> [Text] -> Text)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, Bool -> [Text] -> Text)]
smtOpRealTable
          = Bool -> [Text] -> Text
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 -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
cvtSV [SV]
args)
          | Bool
ratOp, Just [Text] -> Text
f <- Op -> [(Op, [Text] -> Text)] -> Maybe ([Text] -> Text)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, [Text] -> Text)]
ratOpTable
          = [Text] -> Text
f ((SV -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
cvtSV [SV]
args)
          | Bool
fpOp, Just Bool -> [Text] -> Text
f <- Op
-> [(Op, Bool -> [Text] -> Text)] -> Maybe (Bool -> [Text] -> Text)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, Bool -> [Text] -> Text)]
smtOpFloatDoubleTable
          = Bool -> [Text] -> Text
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 -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
cvtSV [SV]
args)
          | Bool
charOp Bool -> Bool -> Bool
|| Bool
stringOp, Just [Text] -> Text
f <- Op -> [(Op, [Text] -> Text)] -> Maybe ([Text] -> Text)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, [Text] -> Text)]
smtStringTable
          = [Text] -> Text
f ((SV -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
cvtSV [SV]
args)
          | Bool
listOp, Just [Text] -> Text
f <- Op -> [(Op, [Text] -> Text)] -> Maybe ([Text] -> Text)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, [Text] -> Text)]
smtListTable
          = [Text] -> Text
f ((SV -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
cvtSV [SV]
args)
          | Just [Text] -> Text
f <- Op -> [(Op, [Text] -> Text)] -> Maybe ([Text] -> Text)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, [Text] -> Text)]
uninterpretedTable
          = [Text] -> Text
f ((SV -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
cvtSV [SV]
args)
          | Bool
True
          = String -> Text
forall a. HasCallStack => String -> a
error (String -> Text) -> String -> Text
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 -> [Text] -> Text)]
smtOpBVTable  = [ (Op
Plus,          Text -> Bool -> [Text] -> Text
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> p -> [a] -> a
lift2   Text
"bvadd")
                                , (Op
Minus,         Text -> Bool -> [Text] -> Text
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> p -> [a] -> a
lift2   Text
"bvsub")
                                , (Op
Times,         Text -> Bool -> [Text] -> Text
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> p -> [a] -> a
lift2   Text
"bvmul")
                                , (Op
UNeg,          Text -> Text -> Bool -> [Text] -> Text
forall {a} {p}.
(Semigroup a, IsString a, Show a) =>
a -> a -> p -> [a] -> a
lift1B  Text
"not"    Text
"bvneg")
                                , (Op
Abs,           Bool -> [Text] -> Text
liftAbs)
                                , (Op
Quot,          Text -> Text -> Bool -> [Text] -> Text
forall {a}.
(Semigroup a, IsString a, Show a) =>
a -> a -> Bool -> [a] -> a
lift2S  Text
"bvudiv" Text
"bvsdiv")
                                , (Op
Rem,           Text -> Text -> Bool -> [Text] -> Text
forall {a}.
(Semigroup a, IsString a, Show a) =>
a -> a -> Bool -> [a] -> a
lift2S  Text
"bvurem" Text
"bvsrem")
                                , (Bool -> Op
Equal Bool
True,    Bool -> [Text] -> Text
forall {p}. p -> [Text] -> Text
eqBV)
                                , (Bool -> Op
Equal Bool
False,   Bool -> [Text] -> Text
forall {p}. p -> [Text] -> Text
eqBV)
                                , (Op
NotEqual,      Bool -> [Text] -> Text
forall {p}. p -> [Text] -> Text
neqBV)
                                , (Op
LessThan,      Text -> Text -> Bool -> [Text] -> Text
forall {a}.
(Semigroup a, IsString a, Show a) =>
a -> a -> Bool -> [a] -> a
lift2S  Text
"bvult" Text
"bvslt")
                                , (Op
GreaterThan,   Text -> Text -> Bool -> [Text] -> Text
forall {a}.
(Semigroup a, IsString a, Show a) =>
a -> a -> Bool -> [a] -> a
lift2S  Text
"bvugt" Text
"bvsgt")
                                , (Op
LessEq,        Text -> Text -> Bool -> [Text] -> Text
forall {a}.
(Semigroup a, IsString a, Show a) =>
a -> a -> Bool -> [a] -> a
lift2S  Text
"bvule" Text
"bvsle")
                                , (Op
GreaterEq,     Text -> Text -> Bool -> [Text] -> Text
forall {a}.
(Semigroup a, IsString a, Show a) =>
a -> a -> Bool -> [a] -> a
lift2S  Text
"bvuge" Text
"bvsge")
                                ]

                -- Boolean comparisons.. SMTLib's bool type doesn't do comparisons, but Haskell does.. Sigh
                boolComps :: [(Op, [Text] -> Text)]
boolComps      = [ (Op
LessThan,      [Text] -> Text
forall {a}. (Semigroup a, IsString a, Show a) => [a] -> a
blt)
                                 , (Op
GreaterThan,   [Text] -> Text
forall {a}. (Semigroup a, IsString a, Show a) => [a] -> a
blt ([Text] -> Text) -> ([Text] -> [Text]) -> [Text] -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> [Text]
forall {a}. Show a => [a] -> [a]
swp)
                                 , (Op
LessEq,        [Text] -> Text
forall {a}. (Semigroup a, IsString a, Show a) => [a] -> a
blq)
                                 , (Op
GreaterEq,     [Text] -> Text
forall {a}. (Semigroup a, IsString a, Show a) => [a] -> a
blq ([Text] -> Text) -> ([Text] -> [Text]) -> [Text] -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Text] -> [Text]
forall {a}. Show a => [a] -> [a]
swp)
                                 ]
                               where blt :: [a] -> a
blt [a
x, a
y] = a
"(and (not " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
") " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
y a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
")"
                                     blt [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.blt: 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
                                     blq :: [a] -> a
blq [a
x, a
y] = a
"(or (not " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
") " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
y a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
")"
                                     blq [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.blq: 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
                                     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 -> [Text] -> Text)]
smtOpRealTable =  [(Op, Bool -> [Text] -> Text)]
smtIntRealShared
                               [(Op, Bool -> [Text] -> Text)]
-> [(Op, Bool -> [Text] -> Text)] -> [(Op, Bool -> [Text] -> Text)]
forall a. [a] -> [a] -> [a]
++ [ (Op
Quot,        Text -> Text -> Bool -> [Text] -> Text
forall {p}. Text -> Text -> p -> [Text] -> Text
lift2WM Text
"/" Text
"fp.div")
                                  ]

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

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

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

                ratOpTable :: [(Op, [Text] -> Text)]
ratOpTable = [ (Bool -> Op
Equal Bool
True,  Text -> [Text] -> Text
forall {a}. (Semigroup a, IsString a, Show a) => a -> [a] -> a
lift2Rat Text
"sbv.rat.eq")
                             , (Bool -> Op
Equal Bool
False, Text -> [Text] -> Text
forall {a}. (Semigroup a, IsString a, Show a) => a -> [a] -> a
lift2Rat Text
"sbv.rat.eq")
                             , (Op
NotEqual,    Text -> [Text] -> Text
forall {a}. (Semigroup a, IsString a, Show a) => a -> [a] -> a
lift2Rat Text
"sbv.rat.notEq")
                             ]
                        where lift2Rat :: a -> [a] -> a
lift2Rat a
o [a
x, a
y] = a
"(" a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
o a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
" " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
x a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
" " a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
y a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
")"
                              lift2Rat a
o [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.lift2Rat: Unexpected arguments: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (a, [a]) -> String
forall a. Show a => a -> String
show (a
o, [a]
sbvs)

                -- equality and comparisons are the only thing that works on uninterpreted sorts and pretty much everything else
                uninterpretedTable :: [(Op, [Text] -> Text)]
uninterpretedTable = [ (Bool -> Op
Equal Bool
True,  Text -> Text -> Bool -> [Text] -> Text
forall {a}.
(Semigroup a, IsString a, Show a) =>
a -> a -> Bool -> [a] -> a
lift2S Text
"="        Text
"="        Bool
True)
                                     , (Bool -> Op
Equal Bool
False, Text -> Text -> Bool -> [Text] -> Text
forall {a}.
(Semigroup a, IsString a, Show a) =>
a -> a -> Bool -> [a] -> a
lift2S Text
"="        Text
"="        Bool
True)
                                     , (Op
NotEqual,    Text -> Text -> Bool -> [Text] -> Text
liftNS Text
"distinct" Text
"distinct" Bool
True)
                                     ]

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

                -- For lists, equality is really the only operator. Also, not strong-equality due to lists of floats.
                -- Likewise here, things might change for comparisons
                smtListTable :: [(Op, [Text] -> Text)]
smtListTable = [ (Bool -> Op
Equal Bool
False, Text -> Text -> Bool -> [Text] -> Text
forall {a}.
(Semigroup a, IsString a, Show a) =>
a -> a -> Bool -> [a] -> a
lift2S Text
"="        Text
"="        Bool
True)
                               , (Op
NotEqual,    Text -> Text -> Bool -> [Text] -> Text
liftNS Text
"distinct" Text
"distinct" Bool
True)
                               , (Op
LessThan,    Bool -> Text -> [Text] -> Text
forall {a}.
(Semigroup a, IsString a, Show a) =>
Bool -> a -> [a] -> a
seqCmp Bool
False Text
"seq.<")
                               , (Op
GreaterThan, Bool -> Text -> [Text] -> Text
forall {a}.
(Semigroup a, IsString a, Show a) =>
Bool -> a -> [a] -> a
seqCmp Bool
True  Text
"seq.<")
                               , (Op
LessEq,      Bool -> Text -> [Text] -> Text
forall {a}.
(Semigroup a, IsString a, Show a) =>
Bool -> a -> [a] -> a
seqCmp Bool
False Text
"seq.<=")
                               , (Op
GreaterEq,   Bool -> Text -> [Text] -> Text
forall {a}.
(Semigroup a, IsString a, Show a) =>
Bool -> a -> [a] -> a
seqCmp Bool
True  Text
"seq.<=")
                               ]

declareFun :: SV -> SBVType -> Maybe Text -> [Text]
declareFun :: SV -> SBVType -> Maybe Text -> [Text]
declareFun SV
sv = Text -> SBVType -> Maybe Text -> [Text]
declareName (String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ SV -> String
forall a. Show a => a -> String
show SV
sv)

-- 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 :: Text -> SBVType -> Maybe Text -> [Text]
declareName :: Text -> SBVType -> Maybe Text -> [Text]
declareName Text
s t :: SBVType
t@(SBVType [Kind]
inputKS) Maybe Text
mbCmnt = Text
decl Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: [Text]
restrict
  where decl :: Text
decl = Text
"(declare-fun " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
s Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SBVType -> Text
cvtType SBVType
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> (Text -> Text) -> Maybe Text -> Text
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Text
"" (Text
" ; " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>) Maybe Text
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]
++ Text -> String
T.unpack Text
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 :: Text
resultVar | Bool
needsQuant = Text
"result"
                  | Bool
True       = Text
s

        argList :: [Text]
argList   = [Text
"a" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (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 :: [Text]
argTList  = [Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Kind -> String
smtType Kind
k) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")" | (Text
a, Kind
k) <- [Text] -> [Kind] -> [(Text, Kind)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Text]
argList [Kind]
args]
        resultExp :: Text
resultExp = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
s Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords [Text]
argList Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

        restrict :: [Text]
restrict | Bool
noCharOrRat = []
                 | Bool
needsQuant  =    [               Text
"(assert (forall (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords [Text]
argTList Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
                                    ,               Text
"                (let ((" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
resultVar Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
resultExp Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"))"
                                    ]
                                 [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> (case [Text]
constraints of
                                       []     ->  [ Text
"                     true"]
                                       [Text
x]    ->  [ Text
"                     " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x]
                                       (Text
x:[Text]
xs) ->  ( Text
"                     (and " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x)
                                               Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
:  [ Text
"                          " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
c | Text
c <- [Text]
xs]
                                               [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [ Text
"                     )"])
                                 [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [        Text
"                )))"]
                 | Bool
True        = case [Text]
constraints of
                                  []     -> []
                                  [Text
x]    -> [Text
"(assert " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"]
                                  (Text
x:[Text]
xs) -> ( Text
"(assert (and " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x)
                                         Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
:  [ Text
"             " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
c | Text
c <- [Text]
xs]
                                         [Text] -> [Text] -> [Text]
forall a. Semigroup a => a -> a -> a
<> [ Text
"        ))"]

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

        mkAnd :: [Text] -> (Text -> [a]) -> [a]
mkAnd [] Text -> [a]
_context = []
        mkAnd [Text
c] Text -> [a]
context = Text -> [a]
context Text
c
        mkAnd [Text]
cs  Text -> [a]
context = Text -> [a]
context (Text -> [a]) -> Text -> [a]
forall a b. (a -> b) -> a -> b
$ Text
"(and " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords [Text]
cs Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

        walk :: Int -> Text -> (Kind -> Text -> [Text]) -> Kind -> [Text]
        walk :: Int -> Text -> (Kind -> Text -> [Text]) -> Kind -> [Text]
walk Int
_d Text
nm Kind -> Text -> [Text]
f k :: Kind
k@KVar      {}         = Kind -> Text -> [Text]
f Kind
k Text
nm
        walk Int
_d Text
nm Kind -> Text -> [Text]
f k :: Kind
k@KBool     {}         = Kind -> Text -> [Text]
f Kind
k Text
nm
        walk Int
_d Text
nm Kind -> Text -> [Text]
f k :: Kind
k@KBounded  {}         = Kind -> Text -> [Text]
f Kind
k Text
nm
        walk Int
_d Text
nm Kind -> Text -> [Text]
f k :: Kind
k@KUnbounded{}         = Kind -> Text -> [Text]
f Kind
k Text
nm
        walk Int
_d Text
nm Kind -> Text -> [Text]
f k :: Kind
k@KReal     {}         = Kind -> Text -> [Text]
f Kind
k Text
nm
        walk Int
_d Text
nm Kind -> Text -> [Text]
f k :: Kind
k@KApp      {}         = Kind -> Text -> [Text]
f Kind
k Text
nm
        walk Int
_d Text
nm Kind -> Text -> [Text]
f k :: Kind
k@KFloat    {}         = Kind -> Text -> [Text]
f Kind
k Text
nm
        walk Int
_d Text
nm Kind -> Text -> [Text]
f k :: Kind
k@KDouble   {}         = Kind -> Text -> [Text]
f Kind
k Text
nm
        walk Int
_d Text
nm Kind -> Text -> [Text]
f k :: Kind
k@KRational {}         = Kind -> Text -> [Text]
f Kind
k Text
nm
        walk Int
_d Text
nm Kind -> Text -> [Text]
f k :: Kind
k@KFP       {}         = Kind -> Text -> [Text]
f Kind
k Text
nm
        walk Int
_d Text
nm Kind -> Text -> [Text]
f k :: Kind
k@KChar     {}         = Kind -> Text -> [Text]
f Kind
k Text
nm
        walk Int
_d Text
nm Kind -> Text -> [Text]
f k :: Kind
k@KString   {}         = Kind -> Text -> [Text]
f Kind
k Text
nm
        walk  Int
d Text
nm Kind -> Text -> [Text]
f  (KList Kind
k)
          | Kind -> Bool
charRatFree Kind
k                 = []
          | Bool
True                          = let fnm :: Text
fnm   = Text
"seq" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Int -> String
forall a. Show a => a -> String
show Int
d)
                                                cstrs :: [Text]
cstrs = Int -> Text -> (Kind -> Text -> [Text]) -> Kind -> [Text]
walk (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Text
"(seq.nth " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
nm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
fnm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")") Kind -> Text -> [Text]
f Kind
k
                                            in [Text] -> (Text -> [Text]) -> [Text]
forall {a}. [Text] -> (Text -> [a]) -> [a]
mkAnd [Text]
cstrs ((Text -> [Text]) -> [Text]) -> (Text -> [Text]) -> [Text]
forall a b. (a -> b) -> a -> b
$ \Text
hole -> [Text
"(forall ((" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
fnm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Kind -> String
smtType Kind
KUnbounded) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")) (=> (and (>= " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
fnm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" 0) (< " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
fnm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" (seq.len " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
nm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"))) " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
hole Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"))"]
        walk  Int
d  Text
nm Kind -> Text -> [Text]
f (KSet Kind
k)
          | Kind -> Bool
charRatFree Kind
k                 = []
          | Bool
True                          = let fnm :: Text
fnm    = Text
"set" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Int -> String
forall a. Show a => a -> String
show Int
d)
                                                cstrs :: [Text]
cstrs  = Int -> Text -> (Kind -> Text -> [Text]) -> Kind -> [Text]
walk (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Text
nm (\Kind
sk Text
snm -> [Text
"(=> (select " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
snm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
fnm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
c Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")" | Text
c <- Kind -> Text -> [Text]
f Kind
sk Text
fnm]) Kind
k
                                            in [Text] -> (Text -> [Text]) -> [Text]
forall {a}. [Text] -> (Text -> [a]) -> [a]
mkAnd [Text]
cstrs ((Text -> [Text]) -> [Text]) -> (Text -> [Text]) -> [Text]
forall a b. (a -> b) -> a -> b
$ \Text
hole -> [Text
"(forall ((" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
fnm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Kind -> String
smtType Kind
k) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")) " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
hole Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"]
        walk  Int
d  Text
nm  Kind -> Text -> [Text]
f (KTuple [Kind]
ks)        = let tt :: Text
tt        = Text
"SBVTuple" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (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 -> Text
project a
i = Text
"(proj_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (a -> String
forall a. Show a => a -> String
show a
i) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
tt Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
nm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
                                                nmks :: [(Text, Kind)]
nmks      = [(Int -> Text
forall {a}. Show a => a -> Text
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 ((Text, Kind) -> [Text]) -> [(Text, Kind)] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(Text
n, Kind
k) -> Int -> Text -> (Kind -> Text -> [Text]) -> Kind -> [Text]
walk (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Text
n Kind -> Text -> [Text]
f Kind
k) [(Text, Kind)]
nmks
        walk Int
d  Text
nm Kind -> Text -> [Text]
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 :: Text
fnm   = Text
"array" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Int -> String
forall a. Show a => a -> String
show Int
d)
                                                cstrs :: [Text]
cstrs = Int -> Text -> (Kind -> Text -> [Text]) -> Kind -> [Text]
walk (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Text
"(select " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
nm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
fnm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")") Kind -> Text -> [Text]
f Kind
k2
                                            in [Text] -> (Text -> [Text]) -> [Text]
forall {a}. [Text] -> (Text -> [a]) -> [a]
mkAnd [Text]
cstrs ((Text -> [Text]) -> [Text]) -> (Text -> [Text]) -> [Text]
forall a b. (a -> b) -> a -> b
$ \Text
hole -> [Text
"(forall ((" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
fnm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Kind -> String
smtType Kind
k1) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")) " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
hole Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"]
        walk Int
d Text
nm Kind -> Text -> [Text]
f (KADT String
ty [(String, Kind)]
dict [(String, [Kind])]
pureFS) = let fs :: [(String, [Kind])]
fs = [(String
c, (Kind -> Kind) -> [Kind] -> [Kind]
forall a b. (a -> b) -> [a] -> [b]
map (String -> [(String, Kind)] -> Kind -> Kind
substituteADTVars String
ty [(String, Kind)]
dict) [Kind]
ks) | (String
c, [Kind]
ks) <- [(String, [Kind])]
pureFS]
                                                nmks :: [(Text, Kind)]
nmks  = [(Text
"(get" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack String
c Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Int -> String
forall a. Show a => a -> String
show Int
i) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
nm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")", Kind
k) | (String
c, [Kind]
ks) <- [(String, [Kind])]
fs, (Int
i, Kind
k) <- [Int] -> [Kind] -> [(Int, Kind)]
forall a b. [a] -> [b] -> [(a, b)]
zip [(Int
1::Int)..] [Kind]
ks]
                                            in ((Text, Kind) -> [Text]) -> [(Text, Kind)] -> [Text]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\(Text
n, Kind
k) -> Int -> Text -> (Kind -> Text -> [Text]) -> Kind -> [Text]
walk (Int
dInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) Text
n Kind -> Text -> [Text]
f Kind
k) [(Text, Kind)]
nmks

-----------------------------------------------------------------------------------------------
-- 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 -> Text -> Text -> Text
handleFPCast :: Kind -> Kind -> Text -> Text -> Text
handleFPCast Kind
kFromIn Kind
kToIn Text
rm Text
input
  | Kind
kFrom Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
kTo
  = Text
input
  | Bool
True
  = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Kind -> Kind -> Text -> Text
cast Kind
kFrom Kind
kTo Text
input Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
  where addRM :: Text -> Text -> Text
addRM Text
a Text
s = Text
s Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
rm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
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) -> Text
size (a
eb, a
sb) = String -> Text
T.pack (a -> String
forall a. Show a => a -> String
show a
eb) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (a -> String
forall a. Show a => a -> String
show a
sb)

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

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

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

        -- To real
        cast KFP{} Kind
KReal Text
a = Text
"fp.to_real" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
a

        -- Nothing else should come up:
        cast Kind
f  Kind
d  Text
_ = String -> Text
forall a. HasCallStack => String -> a
error (String -> Text) -> String -> Text
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 :: Text -> Int -> SV -> Text
rot :: Text -> Int -> SV -> Text
rot Text
o Int
c SV
x = Text
"((_ " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
o Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Int -> String
forall a. Show a => a -> String
show Int
c) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

shft :: Text -> Text -> SV -> SV -> Text
shft :: Text -> Text -> SV -> SV -> Text
shft Text
oW Text
oS SV
x SV
c = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
o Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> SV -> Text
cvtSV SV
c Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
   where o :: Text
o = if SV -> Bool
forall a. HasKind a => a -> Bool
hasSign SV
x then Text
oS else Text
oW

-- ADT operations
handleADT :: SolverCapabilities -> ADTOp -> [SV] -> Text
handleADT :: SolverCapabilities -> ADTOp -> [SV] -> Text
handleADT SolverCapabilities
caps ADTOp
op [SV]
args = case [SV]
args of
                          [] -> Text
f
                          [SV]
_  -> Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
f Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords ((SV -> Text) -> [SV] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map SV -> Text
cvtSV [SV]
args) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
  where f :: Text
f = case ADTOp
op of
              ADTConstructor String
nm Kind
k -> Text -> Kind -> Text
ascribe (String -> Text
T.pack String
nm) Kind
k
              ADTTester      String
nm Kind
k -> if SolverCapabilities -> Bool
supportsDirectTesters SolverCapabilities
caps
                                     then String -> Text
T.pack String
nm
                                     else Text -> Kind -> Text
ascribe (String -> Text
T.pack String
nm) Kind
k
              ADTAccessor    String
nm Kind
_ -> String -> Text
T.pack String
nm

        ascribe :: Text -> Kind -> Text
ascribe Text
nm Kind
k = Text
"(as " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
nm Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Kind -> String
smtType Kind
k) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

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

      Kind
KUnbounded   -> case Kind
kTo of
                        Kind
KReal        -> Text
"(to_real " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
                        KBounded Bool
_ Int
n -> Text
"((_ int_to_bv " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Int -> String
forall a. Show a => a -> String
show Int
n) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
                        Kind
_            -> Text
tryFPCast

      Kind
KReal        -> case Kind
kTo of
                        Kind
KUnbounded   -> Text
"(to_int " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
                        Kind
_            -> Text
tryFPCast

      Kind
_            -> Text
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 :: Text
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 -> Text -> Text -> Text
handleFPCast Kind
kFrom Kind
kTo (String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ RoundingMode -> String
smtRoundingMode RoundingMode
RoundNearestTiesToEven) Text
a
          | Bool
True
          = String -> Text
forall a. HasCallStack => String -> a
error (String -> Text) -> String -> Text
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 -> Text) -> a -> a -> Text
fromBV a -> Text
upConv a
m a
n
         | a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
m  = a -> Text
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 = Text
a
         | Bool
True   = a -> Text
forall {a}. Show a => a -> Text
extract (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1)

        signExtend :: a -> Text
signExtend a
i = Text
"((_ sign_extend " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (a -> String
forall a. Show a => a -> String
show a
i) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>  Text
") "  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
        zeroExtend :: a -> Text
zeroExtend a
i = Text
"((_ zero_extend " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (a -> String
forall a. Show a => a -> String
show a
i) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>  Text
") "  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
        extract :: a -> Text
extract    a
i = Text
"((_ extract "     Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (a -> String
forall a. Show a => a -> String
show a
i) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" 0) " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

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

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

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

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

        opt :: [Text] -> Text
opt   [Text]
xs = Text
"(set-option " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords [Text]
xs Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
        info :: [Text] -> Text
info  [Text]
xs = Text
"(set-info "   Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.unwords [Text]
xs Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

        logic :: Logic -> Text
logic Logic
Logic_NONE = Text
"; NB. not setting the logic per user request of Logic_NONE"
        logic Logic
l          = Text
"(set-logic " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> String -> Text
T.pack (Logic -> String
forall a. Show a => a -> String
show Logic
l) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

        -- 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 -> [Text]
timeOut a
i = case SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
cfg) of
                     Solver
CVC4 -> [Text
":tlimit-per", String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
i]
                     Solver
CVC5 -> [Text
":tlimit-per", String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
i]
                     Solver
_    -> [Text
":timeout",    String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
i]

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

{- HLint ignore module "Use record patterns" -}