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

{-# OPTIONS_GHC -Wall -Werror #-}

module Data.SBV.SMT.SMTLib2(cvt, cvtInc) where

import Data.Bits  (bit)
import Data.List  (intercalate, partition, nub, sort)
import Data.Maybe (listToMaybe, fromMaybe, catMaybes)

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

import Data.SBV.Core.Data
import Data.SBV.Core.Symbolic (QueryContext(..), SetOp(..), OvOp(..), CnstMap, getUserName', getSV, regExpToSMTString)
import Data.SBV.Core.Kind (smtType, needsFlattening)
import Data.SBV.SMT.Utils
import Data.SBV.Control.Types

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

import qualified Data.Generics.Uniplate.Data as G

import Data.Either(lefts)

tbd :: String -> a
tbd :: forall a. String -> a
tbd String
e = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.SMTLib2: Not-yet-supported: " forall a. [a] -> [a] -> [a]
++ String
e

-- | Translate a problem into an SMTLib2 script
cvt :: SMTLibConverter [String]
cvt :: SMTLibConverter [String]
cvt QueryContext
ctx Set Kind
kindInfo Bool
isSat [String]
comments ([(Quantifier, NamedSymVar)]
inputs, [NamedSymVar]
trackerVars) [Either SV (SV, [SV])]
skolemInps (CnstMap
allConsts, [(SV, CV)]
consts) [((Int, Kind, Kind), [SV])]
tbls [(Int, ArrayInfo)]
arrs [(String, SBVType)]
uis [(Bool, String, [String])]
axs (SBVPgm Seq (SV, SBVExpr)
asgnsSeq) Seq (Bool, [(String, String)], SV)
cstrs SV
out SMTConfig
cfg = [String]
pgm
  where hasInteger :: Bool
hasInteger     = Kind
KUnbounded forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
        hasReal :: Bool
hasReal        = Kind
KReal      forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
        hasFP :: Bool
hasFP          =  Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [() | KFP{} <- forall a. Set a -> [a]
Set.toList Set Kind
kindInfo])
                       Bool -> Bool -> Bool
|| Kind
KFloat     forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
                       Bool -> Bool -> Bool
|| Kind
KDouble    forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
        hasString :: Bool
hasString      = Kind
KString     forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
        hasRegExp :: Bool
hasRegExp      = (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [() | (RegExOp
_ :: RegExOp) <- forall from to. Biplate from to => from -> [to]
G.universeBi Seq (SV, SBVExpr)
asgnsSeq]
        hasChar :: Bool
hasChar        = Kind
KChar      forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
        hasRounding :: Bool
hasRounding    = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String
s | (String
s, Maybe [String]
_) <- [(String, Maybe [String])]
usorts, String
s forall a. Eq a => a -> a -> Bool
== String
"RoundingMode"]
        hasBVs :: Bool
hasBVs         = Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [() | KBounded{} <- forall a. Set a -> [a]
Set.toList Set Kind
kindInfo])
        usorts :: [(String, Maybe [String])]
usorts         = [(String
s, Maybe [String]
dt) | KUserSort String
s Maybe [String]
dt <- forall a. Set a -> [a]
Set.toList Set Kind
kindInfo]
        trueUSorts :: [String]
trueUSorts     = [String
s | (String
s, Maybe [String]
_) <- [(String, Maybe [String])]
usorts, String
s forall a. Eq a => a -> a -> Bool
/= String
"RoundingMode"]
        tupleArities :: [Int]
tupleArities   = Set Kind -> [Int]
findTupleArities Set Kind
kindInfo
        hasNonBVArrays :: Bool
hasNonBVArrays = (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [() | (Int
_, (String
_, (Kind
k1, Kind
k2), ArrayContext
_)) <- [(Int, ArrayInfo)]
arrs, Bool -> Bool
not (forall a. HasKind a => a -> Bool
isBounded Kind
k1 Bool -> Bool -> Bool
&& forall a. HasKind a => a -> Bool
isBounded Kind
k2)]
        hasArrayInits :: Bool
hasArrayInits  = (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [() | (Int
_, (String
_, (Kind, Kind)
_, ArrayFree (Just SV
_))) <- [(Int, ArrayInfo)]
arrs]
        hasOverflows :: Bool
hasOverflows   = (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [() | (OvOp
_ :: OvOp) <- forall from to. Biplate from to => from -> [to]
G.universeBi Seq (SV, SBVExpr)
asgnsSeq]
        hasList :: Bool
hasList        = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. HasKind a => a -> Bool
isList Set Kind
kindInfo
        hasSets :: Bool
hasSets        = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. HasKind a => a -> Bool
isSet Set Kind
kindInfo
        hasTuples :: Bool
hasTuples      = Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall a b. (a -> b) -> a -> b
$ [Int]
tupleArities
        hasEither :: Bool
hasEither      = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. HasKind a => a -> Bool
isEither Set Kind
kindInfo
        hasMaybe :: Bool
hasMaybe       = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. HasKind a => a -> Bool
isMaybe  Set Kind
kindInfo
        hasRational :: Bool
hasRational    = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. HasKind a => a -> Bool
isRational Set Kind
kindInfo
        rm :: RoundingMode
rm             = SMTConfig -> RoundingMode
roundingMode SMTConfig
cfg
        solverCaps :: SolverCapabilities
solverCaps     = SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)

        -- Is there a reason why we can't handle this problem?
        -- NB. There's probably a lot more checking we can do here, but this is a start:
        doesntHandle :: Maybe [String]
doesntHandle = forall a. [a] -> Maybe a
listToMaybe [String -> [String]
nope String
w | (String
w, Bool
have, Bool
need) <- [(String, Bool, Bool)]
checks, Bool
need Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
have]
           where checks :: [(String, Bool, Bool)]
checks = [ (String
"data types",     SolverCapabilities -> Bool
supportsDataTypes  SolverCapabilities
solverCaps, Bool
hasTuples Bool -> Bool -> Bool
|| Bool
hasEither Bool -> Bool -> Bool
|| Bool
hasMaybe)
                          , (String
"set operations", SolverCapabilities -> Bool
supportsSets       SolverCapabilities
solverCaps, Bool
hasSets)
                          , (String
"bit vectors",    SolverCapabilities -> Bool
supportsBitVectors SolverCapabilities
solverCaps, Bool
hasBVs)
                          ]

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

        setAll :: String -> [String]
setAll String
reason = [String
"(set-logic ALL) ; "  forall a. [a] -> [a] -> [a]
++ String
reason forall a. [a] -> [a] -> [a]
++ String
", using catch-all."]

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

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

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

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

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

           | Bool
hasFP Bool -> Bool -> Bool
|| Bool
hasRounding
           = if Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls)
             then [String
"(set-logic ALL)"]
             else if Bool
hasBVs
                  then [String
"(set-logic QF_FPBV)"]
                  else [String
"(set-logic QF_FP)"]

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

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

        -- process all other settings we're given. If an option cannot be repeated, we only take the last one.
        userSettings :: [String]
userSettings = forall a b. (a -> b) -> [a] -> [b]
map SMTOption -> String
setSMTOption forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. SMTOption -> Bool
isLogic) forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SMTOption -> [SMTOption] -> [SMTOption]
comb [] 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
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SMTOption -> Bool
isDiagOutput [SMTOption]
rest =     [SMTOption]
rest
                   | Bool
True                                    = SMTOption
o forall a. a -> [a] -> [a]
: [SMTOption]
rest

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

        pgm :: [String]
pgm  =  forall a b. (a -> b) -> [a] -> [b]
map (String
"; " forall a. [a] -> [a] -> [a]
++) [String]
comments
             forall a. [a] -> [a] -> [a]
++ [String]
settings
             forall a. [a] -> [a] -> [a]
++ [ String
"; --- uninterpreted sorts ---" ]
             forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String, Maybe [String]) -> [String]
declSort [(String, Maybe [String])]
usorts
             forall a. [a] -> [a] -> [a]
++ [ String
"; --- tuples ---" ]
             forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Int -> [String]
declTuple [Int]
tupleArities
             forall a. [a] -> [a] -> [a]
++ [ String
"; --- sums ---" ]
             forall a. [a] -> [a] -> [a]
++ (if Set Kind -> Bool
containsSum       Set Kind
kindInfo then [String]
declSum       else [])
             forall a. [a] -> [a] -> [a]
++ (if Set Kind -> Bool
containsMaybe     Set Kind
kindInfo then [String]
declMaybe     else [])
             forall a. [a] -> [a] -> [a]
++ (if Set Kind -> Bool
containsRationals Set Kind
kindInfo then [String]
declRationals else [])
             forall a. [a] -> [a] -> [a]
++ [ String
"; --- literal constants ---" ]
             forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SMTConfig -> (SV, CV) -> [String]
declConst SMTConfig
cfg) [(SV, CV)]
consts
             forall a. [a] -> [a] -> [a]
++ [ String
"; --- skolem constants ---" ]
             forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [SV -> SBVType -> Maybe String -> [String]
declareFun SV
s ([Kind] -> SBVType
SBVType (forall a b. (a -> b) -> [a] -> [b]
map forall a. HasKind a => a -> Kind
kindOf ([SV]
ss forall a. [a] -> [a] -> [a]
++ [SV
s]))) (SV -> Maybe String
userName SV
s) | Right (SV
s, [SV]
ss) <- [Either SV (SV, [SV])]
skolemInps]
             forall a. [a] -> [a] -> [a]
++ [ String
"; --- optimization tracker variables ---" | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedSymVar]
trackerVars) ]
             forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [SV -> SBVType -> Maybe String -> [String]
declareFun SV
s ([Kind] -> SBVType
SBVType [forall a. HasKind a => a -> Kind
kindOf SV
s]) (forall a. a -> Maybe a
Just (String
"tracks " forall a. Semigroup a => a -> a -> a
<> String
nm)) | NamedSymVar
var <- [NamedSymVar]
trackerVars, let s :: SV
s = NamedSymVar -> SV
getSV NamedSymVar
var, let nm :: String
nm = NamedSymVar -> String
getUserName' NamedSymVar
var]
             forall a. [a] -> [a] -> [a]
++ [ String
"; --- constant tables ---" ]
             forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (:) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Int, Kind, Kind), [SV]), [String]) -> (String, [String])
constTable) [(((Int, Kind, Kind), [SV]), [String])]
constTables
             forall a. [a] -> [a] -> [a]
++ [ String
"; --- skolemized tables ---" ]
             forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (String -> (((Int, Kind, Kind), [SV]), [String]) -> String
skolemTable ([String] -> String
unwords (forall a b. (a -> b) -> [a] -> [b]
map SV -> String
svType [SV]
foralls))) [(((Int, Kind, Kind), [SV]), [String])]
skolemTables
             forall a. [a] -> [a] -> [a]
++ [ String
"; --- arrays ---" ]
             forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
arrayConstants
             forall a. [a] -> [a] -> [a]
++ [ String
"; --- uninterpreted constants ---" ]
             forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String, SBVType) -> [String]
declUI [(String, SBVType)]
uis
             forall a. [a] -> [a] -> [a]
++ [ String
"; --- SBV Function definitions" | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null Map Op String
funcMap) ]
             forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ Op -> String -> [String]
declSBVFunc Op
op String
nm | (Op
op, String
nm) <- forall k a. Map k a -> [(k, a)]
M.toAscList Map Op String
funcMap ]
             forall a. [a] -> [a] -> [a]
++ [ String
"; --- user given axioms ---" ]
             forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (Bool, String, [String]) -> String
declAx [(Bool, String, [String])]
axs
             forall a. [a] -> [a] -> [a]
++ [ String
"; --- preQuantifier assignments ---" ]
             forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SMTConfig
-> SkolemMap
-> TableMap
-> Map Op String
-> (SV, SBVExpr)
-> [String]
declDef SMTConfig
cfg SkolemMap
skolemMap TableMap
tableMap Map Op String
funcMap) [(SV, SBVExpr)]
preQuantifierAssigns
             forall a. [a] -> [a] -> [a]
++ [ String
"; --- arrayDelayeds ---" ]
             forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
arrayDelayeds
             forall a. [a] -> [a] -> [a]
++ [ String
"; --- arraySetups ---" ]
             forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
arraySetups
             forall a. [a] -> [a] -> [a]
++ [ String
"; --- formula ---" ]
             forall a. [a] -> [a] -> [a]
++ [String
"(assert (forall (" forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
"\n                 "
                                        [String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SV
s forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ SV -> String
svType SV
s forall a. [a] -> [a] -> [a]
++ String
")" | SV
s <- [SV]
foralls] forall a. [a] -> [a] -> [a]
++ String
")"
                | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls)
                ]
             forall a. [a] -> [a] -> [a]
++ [ String
"; --- postQuantifier assignments ---" ]
             forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SV, SBVExpr) -> [String]
mkAssign [(SV, SBVExpr)]
postQuantifierAssigns
             forall a. [a] -> [a] -> [a]
++ [ String
"; --- delayedEqualities ---" ]
             forall a. [a] -> [a] -> [a]
++ [String] -> [String]
delayedAsserts [String]
delayedEqualities
             forall a. [a] -> [a] -> [a]
++ [ String
"; -- finalAssert ---" ]
             forall a. [a] -> [a] -> [a]
++ [String]
finalAssert

        -- identify the assignments that can come before the first quantifier
        ([(SV, SBVExpr)]
preQuantifierAssigns, [(SV, SBVExpr)]
postQuantifierAssigns)
           | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls
           = ([(SV, SBVExpr)]
asgns, [])
           | Bool
True
           = forall a. (a -> Bool) -> [a] -> ([a], [a])
span forall {b}. (SV, b) -> Bool
pre [(SV, SBVExpr)]
asgns
           where first :: NodeId
first      = SV -> NodeId
nodeId (forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
minimum [SV]
foralls)
                 pre :: (SV, b) -> Bool
pre (SV
s, b
_) = SV -> NodeId
nodeId SV
s forall a. Ord a => a -> a -> Bool
< NodeId
first

                 nodeId :: SV -> NodeId
nodeId (SV Kind
_ NodeId
n) = NodeId
n

        noOfCloseParens :: Int
noOfCloseParens
          | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls = Int
0
          | Bool
True         = forall (t :: * -> *) a. Foldable t => t a -> Int
length [(SV, SBVExpr)]
postQuantifierAssigns forall a. Num a => a -> a -> a
+ Int
2 forall a. Num a => a -> a -> a
+ (if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
delayedEqualities then Int
0 else Int
1)

        foralls :: [SV]
foralls    = forall a b. [Either a b] -> [a]
lefts [Either SV (SV, [SV])]
skolemInps
        forallArgs :: String
forallArgs = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((String
" " forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) [SV]
foralls

        ([(((Int, Kind, Kind), [SV]), [String])]
constTables, [(((Int, Kind, Kind), [SV]), [String])]
skolemTables) = ([(((Int, Kind, Kind), [SV])
t, [String]
d) | (((Int, Kind, Kind), [SV])
t, Left [String]
d) <- [(((Int, Kind, Kind), [SV]), Either [String] [String])]
allTables], [(((Int, Kind, Kind), [SV])
t, [String]
d) | (((Int, Kind, Kind), [SV])
t, Right [String]
d) <- [(((Int, Kind, Kind), [SV]), Either [String] [String])]
allTables])
        allTables :: [(((Int, Kind, Kind), [SV]), Either [String] [String])]
allTables = [(((Int, Kind, Kind), [SV])
t, RoundingMode
-> SkolemMap
-> (Bool, String)
-> [SV]
-> ((Int, Kind, Kind), [SV])
-> Either [String] [String]
genTableData RoundingMode
rm SkolemMap
skolemMap (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls), String
forallArgs) (forall a b. (a -> b) -> [a] -> [b]
map 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]
        ([[String]]
arrayConstants, [[String]]
arrayDelayeds, [[String]]
arraySetups) = forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (SMTConfig
-> Bool
-> CnstMap
-> SkolemMap
-> (Int, ArrayInfo)
-> ([String], [String], [String])
declArray SMTConfig
cfg (Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls)) CnstMap
allConsts SkolemMap
skolemMap) [(Int, ArrayInfo)]
arrs
        delayedEqualities :: [String]
delayedEqualities = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall a b. (a, b) -> b
snd [(((Int, Kind, Kind), [SV]), [String])]
skolemTables

        delayedAsserts :: [String] -> [String]
delayedAsserts []              = []
        delayedAsserts ds :: [String]
ds@(String
deH : [String]
deTs)
          | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls = forall a b. (a -> b) -> [a] -> [b]
map (\String
s -> String
"(assert " forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
")") [String]
ds
          | Bool
True         = forall a b. (a -> b) -> [a] -> [b]
map String -> String
letShift ((String
"(and " forall a. [a] -> [a] -> [a]
++ String
deH) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map (Int -> String -> String
align Int
5) [String]
deTs)

        letShift :: String -> String
letShift = Int -> String -> String
align Int
12

        finalAssert :: [String]
finalAssert
          | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls Bool -> Bool -> Bool
&& Bool
noConstraints
          = []
          | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls
          =    forall a b. (a -> b) -> [a] -> [b]
map (\([(String, String)]
attr, Either SV SV
v) -> String
"(assert "      forall a. [a] -> [a] -> [a]
++ [(String, String)] -> String -> String
addAnnotations [(String, String)]
attr (Either SV SV -> String
mkLiteral Either SV SV
v) forall a. [a] -> [a] -> [a]
++ String
")") [([(String, String)], Either SV SV)]
hardAsserts
            forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (\([(String, String)]
attr, Either SV SV
v) -> String
"(assert-soft " forall a. [a] -> [a] -> [a]
++ [(String, String)] -> String -> String
addAnnotations [(String, String)]
attr (Either SV SV -> String
mkLiteral Either SV SV
v) forall a. [a] -> [a] -> [a]
++ String
")") [([(String, String)], Either SV SV)]
softAsserts
          | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
namedAsserts)
          = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [ String
"SBV: Constraints with attributes and quantifiers cannot be mixed!"
                                     , String
"   Quantified variables: " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [SV]
foralls)
                                     , String
"   Named constraints   : " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [String]
namedAsserts)
                                     ]
          | Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([(String, String)], Either SV SV)]
softAsserts)
          = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [ String
"SBV: Soft constraints and quantifiers cannot be mixed!"
                                     , String
"   Quantified variables: " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [SV]
foralls)
                                     , String
"   Soft constraints    : " forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
", " (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [([(String, String)], Either SV SV)]
softAsserts)
                                     ]
          | Bool
True
          = [String -> String
impAlign (String -> String
letShift String
combined) forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate Int
noOfCloseParens Char
')']
          where mkLiteral :: Either SV SV -> String
mkLiteral (Left  SV
v) =            SkolemMap -> SV -> String
cvtSV SkolemMap
skolemMap SV
v
                mkLiteral (Right SV
v) = String
"(not " forall a. [a] -> [a] -> [a]
++ SkolemMap -> SV -> String
cvtSV SkolemMap
skolemMap SV
v forall a. [a] -> [a] -> [a]
++ String
")"

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

                namedAsserts :: [String]
namedAsserts = [[(String, String)] -> String
findName [(String, String)]
attrs | (Bool
_, [(String, String)]
attrs, Either SV SV
_) <- [(Bool, [(String, String)], Either SV SV)]
assertions, Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, String)]
attrs)]
                 where findName :: [(String, String)] -> String
findName [(String, String)]
attrs = forall a. a -> Maybe a -> a
fromMaybe String
"<anonymous>" (forall a. [a] -> Maybe a
listToMaybe [String
nm | (String
":named", String
nm) <- [(String, String)]
attrs])

                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]

                combined :: String
combined = case [Either SV SV]
lits of
                             []               -> String
"true"
                             [Either SV SV
x]              -> Either SV SV -> String
mkLiteral Either SV SV
x
                             [Either SV SV]
xs  | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Either SV SV -> Bool
bad [Either SV SV]
xs -> String
"false"
                                 | Bool
True       -> String
"(and " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (forall a b. (a -> b) -> [a] -> [b]
map Either SV SV -> String
mkLiteral [Either SV SV]
xs) forall a. [a] -> [a] -> [a]
++ String
")"
                  where lits :: [Either SV SV]
lits = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either SV SV -> Bool
redundant) forall a b. (a -> b) -> a -> b
$ forall a. Eq a => [a] -> [a]
nub (forall a. Ord a => [a] -> [a]
sort (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [([(String, String)], Either SV SV)]
hardAsserts))
                        redundant :: Either SV SV -> Bool
redundant (Left SV
v)  = SV
v forall a. Eq a => a -> a -> Bool
== SV
trueSV
                        redundant (Right SV
v) = SV
v forall a. Eq a => a -> a -> Bool
== SV
falseSV
                        bad :: Either SV SV -> Bool
bad (Left  SV
v) = SV
v forall a. Eq a => a -> a -> Bool
== SV
falseSV
                        bad (Right SV
v) = SV
v forall a. Eq a => a -> a -> Bool
== SV
trueSV

        impAlign :: String -> String
impAlign String
s
          | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
delayedEqualities = String
s
          | Bool
True                   = String
"     " forall a. [a] -> [a] -> [a]
++ String
s

        align :: Int -> String -> String
align Int
n String
s = forall a. Int -> a -> [a]
replicate Int
n Char
' ' forall a. [a] -> [a] -> [a]
++ String
s

        finalAssertions :: (Bool, [(Bool, [(String, String)], Either SV SV)])  -- If Left: positive, Right: negative
        finalAssertions :: (Bool, [(Bool, [(String, String)], Either SV SV)])
finalAssertions
           | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Bool, [(String, String)], Either SV SV)]
finals = (Bool
True,  [(Bool
False, [], 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  = forall {b}. [(Bool, [(String, String)], Either SV b)]
cstrs' forall a. [a] -> [a] -> [a]
++ 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) <- forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (Bool, [(String, String)], SV)
cstrs, Just Either SV b
c' <- [forall {b}. SV -> Maybe (Either SV b)
pos SV
c]]

                 mbO :: Maybe (Either SV SV)
mbO | Bool
isSat = 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 forall a. Eq a => a -> a -> Bool
== SV
falseSV = forall a. Maybe a
Nothing
                  | SV
s forall a. Eq a => a -> a -> Bool
== SV
trueSV  = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left SV
falseSV
                  | Bool
True         = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right SV
s

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

        skolemMap :: SkolemMap
skolemMap = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(SV
s, [SV]
ss) | Right (SV
s, [SV]
ss) <- [Either SV (SV, [SV])]
skolemInps, Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
ss)]
        tableMap :: TableMap
tableMap  = forall a. [(Int, a)] -> IntMap a
IM.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c} {b} {b}.
Show a =>
(((a, b, c), b), b) -> (a, String)
mkConstTable [(((Int, Kind, Kind), [SV]), [String])]
constTables forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c} {b} {b}.
Show a =>
(((a, b, c), b), b) -> (a, String)
mkSkTable [(((Int, Kind, Kind), [SV]), [String])]
skolemTables
          where mkConstTable :: (((a, b, c), b), b) -> (a, String)
mkConstTable (((a
t, b
_, c
_), b
_), b
_) = (a
t, String
"table" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
t)
                mkSkTable :: (((a, b, c), b), b) -> (a, String)
mkSkTable    (((a
t, b
_, c
_), b
_), b
_) = (a
t, String
"table" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
t forall a. [a] -> [a] -> [a]
++ String
forallArgs)

        -- SBV only functions.
        funcMap :: Map Op String
funcMap = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(Op, String)]
reverses
          where reverses :: [(Op, String)]
reverses = forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Eq a => [a] -> [a]
nub [Op
op | op :: Op
op@(SeqOp SBVReverse{}) <- forall from to. Biplate from to => from -> [to]
G.universeBi Seq (SV, SBVExpr)
asgnsSeq])
                               [String
"sbv.reverse_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i | Int
i <- [(Int
0::Int)..]]

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

        mkAssign :: (SV, SBVExpr) -> [String]
mkAssign (SV, SBVExpr)
a
          | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls = SMTConfig
-> SkolemMap
-> TableMap
-> Map Op String
-> (SV, SBVExpr)
-> [String]
declDef SMTConfig
cfg SkolemMap
skolemMap TableMap
tableMap Map Op String
funcMap (SV, SBVExpr)
a
          | Bool
True         = [String -> String
letShift (forall {a}. Show a => (a, SBVExpr) -> String
mkLet (SV, SBVExpr)
a)]

        mkLet :: (a, SBVExpr) -> String
mkLet (a
s, SBVApp (Label String
m) [SV
e]) = String
"(let ((" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
s forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ SkolemMap -> SV -> String
cvtSV                SkolemMap
skolemMap                  SV
e forall a. [a] -> [a] -> [a]
++ String
")) ; " forall a. [a] -> [a] -> [a]
++ String
m
        mkLet (a
s, SBVExpr
e)                    = String
"(let ((" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
s forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ SolverCapabilities
-> RoundingMode
-> SkolemMap
-> TableMap
-> Map Op String
-> SBVExpr
-> String
cvtExp SolverCapabilities
solverCaps RoundingMode
rm SkolemMap
skolemMap TableMap
tableMap Map Op String
funcMap SBVExpr
e forall a. [a] -> [a] -> [a]
++ String
"))"

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

-- Declare "known" SBV functions here
declSBVFunc :: Op -> String -> [String]
declSBVFunc :: Op -> String -> [String]
declSBVFunc Op
op String
nm = case Op
op of
                      SeqOp (SBVReverse Kind
KString)   -> [String]
mkStringRev
                      SeqOp (SBVReverse (KList Kind
k)) -> Kind -> [String]
mkSeqRev (Kind -> Kind
KList Kind
k)
                      Op
_                            -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV.declSBVFunc: Unexpected internal function: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Op
op, String
nm)
  where mkStringRev :: [String]
mkStringRev = [ String
"(define-fun-rec " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
" ((str String)) String"
                      , String
"                (ite (= str \"\")"
                      , String
"                     \"\""
                      , String
"                     (str.++ (" forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
" (str.substr str 1 (- (str.len str) 1)))"
                      , String
"                             (str.substr str 0 1))))"
                      ]


        mkSeqRev :: Kind -> [String]
mkSeqRev Kind
k = [ String
"(define-fun-rec " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
" ((lst " forall a. [a] -> [a] -> [a]
++ String
t forall a. [a] -> [a] -> [a]
++ String
")) " forall a. [a] -> [a] -> [a]
++ String
t
                     , String
"                (ite (= lst (as seq.empty " forall a. [a] -> [a] -> [a]
++ String
t forall a. [a] -> [a] -> [a]
++ String
"))"
                     , String
"                     (as seq.empty " forall a. [a] -> [a] -> [a]
++ String
t forall a. [a] -> [a] -> [a]
++ String
")"
                     , String
"                     (seq.++ (" forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
" (seq.extract lst 1 (- (seq.len lst) 1))) (seq.unit (seq.nth lst 0)))))"
                     ]
          where t :: String
t = Kind -> String
smtType Kind
k

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

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

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

        proj :: a -> String
proj a
i = String
"(proj_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
i forall a. [a] -> [a] -> [a]
++ String
"_SBVTuple" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
arity forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
param a
i forall a. [a] -> [a] -> [a]
++ String
")"

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

        param :: a -> String
param a
i = String
"T" forall a. [a] -> [a] -> [a]
++ 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 = forall a. Set a -> [a]
Set.toAscList
                    forall a b. (a -> b) -> a -> b
$ forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map forall (t :: * -> *) a. Foldable t => t a -> Int
length
                    forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList [ [Kind]
tupKs | KTuple [Kind]
tupKs <- forall a. Set a -> [a]
Set.toList Set Kind
ks ]

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

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

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

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

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

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

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

        -- The following is not really kosher; if it happens that a "new" variant of a function is used only incrementally.
        -- But we'll punt on this for now, as it should be rare and can be "worked-around" if necessary.
        funcMap :: Map k a
funcMap = forall {k} {a}. Map k a
M.empty

        rm :: RoundingMode
rm = SMTConfig -> RoundingMode
roundingMode SMTConfig
cfg

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

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

        ([[String]]
arrayConstants, [[String]]
arrayDelayeds, [[String]]
arraySetups) = forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (SMTConfig
-> Bool
-> CnstMap
-> SkolemMap
-> (Int, ArrayInfo)
-> ([String], [String], [String])
declArray SMTConfig
cfg Bool
False CnstMap
allConsts forall {k} {a}. Map k a
skolemMap) [(Int, ArrayInfo)]
arrs

        allTables :: [(((Int, Kind, Kind), [SV]), [String])]
allTables = [(((Int, Kind, Kind), [SV])
t, forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. a -> a
id forall a. a -> a
id (RoundingMode
-> SkolemMap
-> (Bool, String)
-> [SV]
-> ((Int, Kind, Kind), [SV])
-> Either [String] [String]
genTableData RoundingMode
rm forall {k} {a}. Map k a
skolemMap (Bool
False, []) (forall a b. (a -> b) -> [a] -> [b]
map 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]
        ([String]
tableDecls, [[String]]
tableAssigns) = forall a b. [(a, b)] -> ([a], [b])
unzip forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (((Int, Kind, Kind), [SV]), [String]) -> (String, [String])
constTable [(((Int, Kind, Kind), [SV]), [String])]
allTables

        tableMap :: TableMap
tableMap  = forall a. [(Int, a)] -> IntMap a
IM.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall {a} {b} {c} {b} {b}.
Show a =>
(((a, b, c), b), b) -> (a, String)
mkTable [(((Int, Kind, Kind), [SV]), [String])]
allTables
          where mkTable :: (((a, b, c), b), b) -> (a, String)
mkTable (((a
t, b
_, c
_), b
_), b
_) = (a
t, String
"table" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
t)

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

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

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

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

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

declUI :: (String, SBVType) -> [String]
declUI :: (String, SBVType) -> [String]
declUI (String
i, SBVType
t) = String -> SBVType -> Maybe String -> [String]
declareName String
i SBVType
t forall a. Maybe a
Nothing

-- NB. We perform no check to as to whether the axiom is meaningful in any way.
declAx :: (Bool, String, [String]) -> String
declAx :: (Bool, String, [String]) -> String
declAx (Bool
hasDefinition, String
nm, [String]
ls) = (String
";; -- user given " forall a. [a] -> [a] -> [a]
++ String
what forall a. [a] -> [a] -> [a]
++ String
": " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
"\n") forall a. [a] -> [a] -> [a]
++ forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [String]
ls
  where what :: String
what | Bool
hasDefinition = String
"definition"
             | Bool
True          = String
"axiom"

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

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

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

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

        setup :: [String]
setup
          | Int
lis forall a. Eq a => a -> a -> Bool
== Int
0       = [ String
"(define-fun " forall a. [a] -> [a] -> [a]
++ String
initializer forall a. [a] -> [a] -> [a]
++ String
" () Bool true) ; no initialization needed"
                             ]
          | Int
lis forall a. Eq a => a -> a -> Bool
== Int
1       = [ String
"(define-fun " forall a. [a] -> [a] -> [a]
++ String
initializer forall a. [a] -> [a] -> [a]
++ String
" () Bool " forall a. [a] -> [a] -> [a]
++ Int -> String
mkInit Int
0 forall a. [a] -> [a] -> [a]
++ String
")"
                             , String
"(assert " forall a. [a] -> [a] -> [a]
++ String
initializer forall a. [a] -> [a] -> [a]
++ String
")"
                             ]
          | Bool
True           = [ String
"(define-fun " forall a. [a] -> [a] -> [a]
++ String
initializer forall a. [a] -> [a] -> [a]
++ String
" () Bool (and " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (forall a b. (a -> b) -> [a] -> [b]
map Int -> String
mkInit [Int
0..Int
lis forall a. Num a => a -> a -> a
- Int
1]) forall a. [a] -> [a] -> [a]
++ String
"))"
                             , String
"(assert " forall a. [a] -> [a] -> [a]
++ String
initializer forall a. [a] -> [a] -> [a]
++ String
")"
                             ]

skolemTable :: String -> (((Int, Kind, Kind), [SV]), [String]) -> String
skolemTable :: String -> (((Int, Kind, Kind), [SV]), [String]) -> String
skolemTable String
qsIn (((Int
i, Kind
ak, Kind
rk), [SV]
_elts), [String]
_) = String
decl
  where qs :: String
qs   = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
qsIn then String
"" else String
qsIn forall a. [a] -> [a] -> [a]
++ String
" "
        t :: String
t    = String
"table" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
        decl :: String
decl = String
"(declare-fun " forall a. [a] -> [a] -> [a]
++ String
t forall a. [a] -> [a] -> [a]
++ String
" (" forall a. [a] -> [a] -> [a]
++ String
qs forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
ak forall a. [a] -> [a] -> [a]
++ String
") " forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
rk forall a. [a] -> [a] -> [a]
++ String
")"

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

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

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

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

-- TODO: We currently do not support non-constant arrays when quantifiers are present, as
-- we might have to skolemize those. Implement this properly.
-- The difficulty is with the Mutate/Merge: We have to postpone an init if
-- the components are themselves postponed, so this cannot be implemented as a simple map.
declArray :: SMTConfig -> Bool -> CnstMap -> SkolemMap -> (Int, ArrayInfo) -> ([String], [String], [String])
declArray :: SMTConfig
-> Bool
-> CnstMap
-> SkolemMap
-> (Int, ArrayInfo)
-> ([String], [String], [String])
declArray SMTConfig
cfg Bool
quantified CnstMap
consts SkolemMap
skolemMap (Int
i, (String
_, (Kind
aKnd, Kind
bKnd), ArrayContext
ctx)) = (String
adecl forall a. a -> [a] -> [a]
: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> String -> String
wrap [(Int
0::Int)..] (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Bool, String)]
pre), forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> String -> String
wrap [Int
lpre..] (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Bool, String)]
post), [String]
setup)
  where constMapping :: Map SV CV
constMapping = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(SV
s, CV
c) | (CV
c, SV
s) <- forall k a. Map k a -> [(k, a)]
M.assocs CnstMap
consts]
        constNames :: [SV]
constNames   = forall k a. Map k a -> [k]
M.keys Map SV CV
constMapping

        topLevel :: Bool
topLevel = Bool -> Bool
not Bool
quantified Bool -> Bool -> Bool
|| case ArrayContext
ctx of
                                       ArrayFree Maybe SV
mbi      -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SV]
constNames) Maybe SV
mbi
                                       ArrayMutate ArrayIndex
_ SV
a SV
b  -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SV]
constNames) [SV
a, SV
b]
                                       ArrayMerge SV
c ArrayIndex
_ ArrayIndex
_   -> SV
c forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SV]
constNames
        ([(Bool, String)]
pre, [(Bool, String)]
post) = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition forall a b. (a, b) -> a
fst [(Bool, String)]
ctxInfo
        nm :: String
nm = String
"array_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i

        ssv :: SV -> String
ssv SV
sv
         | Bool
topLevel Bool -> Bool -> Bool
|| SV
sv forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SV]
constNames
         = SkolemMap -> SV -> String
cvtSV SkolemMap
skolemMap SV
sv
         | Bool
True
         = forall a. String -> a
tbd String
"Non-constant array initializer in a quantified context"

        atyp :: String
atyp  = String
"(Array " forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
aKnd forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
bKnd forall a. [a] -> [a] -> [a]
++ String
")"

        adecl :: String
adecl = case ArrayContext
ctx of
                  ArrayFree (Just SV
v) -> String
"(define-fun "  forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
" () " forall a. [a] -> [a] -> [a]
++ String
atyp forall a. [a] -> [a] -> [a]
++ String
" ((as const " forall a. [a] -> [a] -> [a]
++ String
atyp forall a. [a] -> [a] -> [a]
++ String
") " forall a. [a] -> [a] -> [a]
++ SV -> String
constInit SV
v forall a. [a] -> [a] -> [a]
++ String
"))"
                  ArrayFree Maybe SV
Nothing
                    | Kind
bKnd forall a. Eq a => a -> a -> Bool
== Kind
KChar  ->  -- Can't support yet, because we need to make sure all the elements are length-1 strings. So, punt for now.
                                         forall a. String -> a
tbd String
"Free array declarations containing SChars"
                  ArrayContext
_                  -> String
"(declare-fun " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
" () " forall a. [a] -> [a] -> [a]
++ String
atyp forall a. [a] -> [a] -> [a]
++                                                  String
")"

        -- CVC4 chokes if the initializer is not a constant. (Z3 is ok with it.) So, print it as
        -- a constant if we have it in the constants; otherwise, we merely print it and hope for the best.
        constInit :: SV -> String
constInit SV
v = case SV
v forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map SV CV
constMapping of
                        Maybe CV
Nothing -> SV -> String
ssv SV
v                      -- Z3 will work, CVC4 will choke. Others don't even support this.
                        Just CV
c  -> RoundingMode -> CV -> String
cvtCV (SMTConfig -> RoundingMode
roundingMode SMTConfig
cfg) CV
c -- Z3 and CVC4 will work. Other's don't support this.

        ctxInfo :: [(Bool, String)]
ctxInfo = case ArrayContext
ctx of
                    ArrayFree Maybe SV
_       -> []
                    ArrayMutate ArrayIndex
j SV
a SV
b -> [(forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SV]
constNames) [SV
a, SV
b], String
"(= " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
" (store array_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ArrayIndex
j forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
a forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
b forall a. [a] -> [a] -> [a]
++ String
"))")]
                    ArrayMerge  SV
t ArrayIndex
j ArrayIndex
k -> [(SV
t forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SV]
constNames,            String
"(= " forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
" (ite " forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
t forall a. [a] -> [a] -> [a]
++ String
" array_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ArrayIndex
j forall a. [a] -> [a] -> [a]
++ String
" array_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ArrayIndex
k forall a. [a] -> [a] -> [a]
++ String
"))")]

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

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

        lpre :: Int
lpre          = forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Bool, String)]
pre
        lAll :: Int
lAll          = Int
lpre forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Bool, String)]
post

        setup :: [String]
setup
          | Int
lAll forall a. Eq a => a -> a -> Bool
== Int
0      = [ String
"(define-fun " forall a. [a] -> [a] -> [a]
++ String
initializer forall a. [a] -> [a] -> [a]
++ String
" () Bool true) ; no initialization needed" | Bool -> Bool
not Bool
quantified]
          | Int
lAll forall a. Eq a => a -> a -> Bool
== Int
1      = [ String
"(define-fun " forall a. [a] -> [a] -> [a]
++ String
initializer forall a. [a] -> [a] -> [a]
++ String
" () Bool " forall a. [a] -> [a] -> [a]
++ Int -> String
mkInit Int
0 forall a. [a] -> [a] -> [a]
++ String
")"
                             , String
"(assert " forall a. [a] -> [a] -> [a]
++ String
initializer forall a. [a] -> [a] -> [a]
++ String
")"
                             ]
          | Bool
True           = [ String
"(define-fun " forall a. [a] -> [a] -> [a]
++ String
initializer forall a. [a] -> [a] -> [a]
++ String
" () Bool (and " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (forall a b. (a -> b) -> [a] -> [b]
map Int -> String
mkInit [Int
0..Int
lAll forall a. Num a => a -> a -> a
- Int
1]) forall a. [a] -> [a] -> [a]
++ String
"))"
                             , String
"(assert " forall a. [a] -> [a] -> [a]
++ String
initializer forall a. [a] -> [a] -> [a]
++ String
")"
                             ]

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

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

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

type SkolemMap   = M.Map SV [SV]
type TableMap    = IM.IntMap String
type FunctionMap = M.Map Op String

-- Present an SV; inline true/false as needed
cvtSV :: SkolemMap -> SV -> String
cvtSV :: SkolemMap -> SV -> String
cvtSV SkolemMap
skolemMap s :: SV
s@(SV Kind
_ (NodeId Int
n))
  | Just [SV]
ss <- SV
s forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` SkolemMap
skolemMap
  = String
"(" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SV
s forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((String
" " forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show) [SV]
ss forall a. [a] -> [a] -> [a]
++ String
")"
  | SV
s forall a. Eq a => a -> a -> Bool
== SV
trueSV
  = String
"true"
  | SV
s forall a. Eq a => a -> a -> Bool
== SV
falseSV
  = String
"false"
  | Bool
True
  = Char
's' forall a. a -> [a] -> [a]
: forall a. Show a => a -> String
show Int
n

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

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

cvtExp :: SolverCapabilities -> RoundingMode -> SkolemMap -> TableMap -> FunctionMap -> SBVExpr -> String
cvtExp :: SolverCapabilities
-> RoundingMode
-> SkolemMap
-> TableMap
-> Map Op String
-> SBVExpr
-> String
cvtExp SolverCapabilities
caps RoundingMode
rm SkolemMap
skolemMap TableMap
tableMap Map Op String
functionMap expr :: SBVExpr
expr@(SBVApp Op
_ [SV]
arguments) = SBVExpr -> String
sh SBVExpr
expr
  where ssv :: SV -> String
ssv = SkolemMap -> SV -> String
cvtSV SkolemMap
skolemMap

        hasPB :: Bool
hasPB       = SolverCapabilities -> Bool
supportsPseudoBooleans SolverCapabilities
caps
        hasInt2bv :: Bool
hasInt2bv   = SolverCapabilities -> Bool
supportsInt2bv SolverCapabilities
caps
        hasDistinct :: Bool
hasDistinct = SolverCapabilities -> Bool
supportsDistinct SolverCapabilities
caps

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        sh (SBVApp (ArrEq ArrayIndex
i ArrayIndex
j) [])  = String
"(= array_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ArrayIndex
i forall a. [a] -> [a] -> [a]
++ String
" array_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ArrayIndex
j forall a. [a] -> [a] -> [a]
++String
")"
        sh (SBVApp (ArrRead ArrayIndex
i) [SV
a]) = String
"(select array_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show ArrayIndex
i forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
a forall a. [a] -> [a] -> [a]
++ String
")"

        sh (SBVApp (Uninterpreted String
nm) [])   = String
nm
        sh (SBVApp (Uninterpreted String
nm) [SV]
args) = String
"(" forall a. [a] -> [a] -> [a]
++ String
nm forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (forall a b. (a -> b) -> [a] -> [b]
map SV -> String
ssv [SV]
args) forall a. [a] -> [a] -> [a]
++ String
")"

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

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

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

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

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

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

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

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

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

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

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

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

        -- NB: Z3 semantics have the predicates reversed: i.e., it returns true if overflow isn't possible. Hence the not.
        sh (SBVApp (OverflowOp OvOp
op) [SV]
args) = String
"(not (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show OvOp
op forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (forall a b. (a -> b) -> [a] -> [b]
map SV -> String
ssv [SV]
args) forall a. [a] -> [a] -> [a]
++ String
"))"

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

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

        -- Reverse is special, since we need to generate call to the internally generated function
        sh inp :: SBVExpr
inp@(SBVApp op :: Op
op@(SeqOp SBVReverse{}) [SV]
args) = String
"(" forall a. [a] -> [a] -> [a]
++ String
ops forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords (forall a b. (a -> b) -> [a] -> [b]
map SV -> String
ssv [SV]
args) forall a. [a] -> [a] -> [a]
++ String
")"
          where ops :: String
ops = case Op
op forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` Map Op String
functionMap of
                        Just String
s  -> String
s
                        Maybe String
Nothing -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.cvtExp.sh: impossible happened; can't translate: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SBVExpr
inp

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

        -- Does the kind KChar and KRational *not* occur in the kind anywhere?
        charRatFree :: Kind -> Bool
charRatFree Kind
k = forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall a b. (a -> b) -> a -> b
$ [() | Kind
KChar <- forall on. Uniplate on => on -> [on]
G.universe Kind
k] forall a. [a] -> [a] -> [a]
++ [() | Kind
KRational <- forall on. Uniplate on => on -> [on]
G.universe Kind
k]
        noCharOrRat :: Bool
noCharOrRat   = Kind -> Bool
charRatFree Kind
result
        needsQuant :: Bool
needsQuant    = Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Kind]
args

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

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

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

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

        mkAnd :: [String] -> String
mkAnd []  = String
"true"
        mkAnd [String
c] = String
c
        mkAnd [String]
cs  = String
"(and " forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
cs forall a. [a] -> [a] -> [a]
++ String
")"

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

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

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

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

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

        size :: (a, a) -> String
size (a
eb, a
sb) = forall a. Show a => a -> String
show a
eb forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
sb

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

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

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

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

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

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

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

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

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

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

      Kind
_            -> String
tryFPCast

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

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

        b2i :: Bool -> b -> String
b2i Bool
False b
_ = String
"(bv2nat " forall a. [a] -> [a] -> [a]
++ String
a forall a. [a] -> [a] -> [a]
++ String
")"
        b2i Bool
True  b
1 = String
"(ite (= " forall a. [a] -> [a] -> [a]
++ String
a forall a. [a] -> [a] -> [a]
++ String
" #b0) 0 (- 1))"
        b2i Bool
True  b
m = String
"(ite (= " forall a. [a] -> [a] -> [a]
++ String
msb forall a. [a] -> [a] -> [a]
++ String
" #b0" forall a. [a] -> [a] -> [a]
++ String
") " forall a. [a] -> [a] -> [a]
++ String
ifPos forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ String
ifNeg forall a. [a] -> [a] -> [a]
++ String
")"
          where offset :: Integer
                offset :: Integer
offset = Integer
2forall a b. (Num a, Integral b) => a -> b -> a
^(b
mforall a. Num a => a -> a -> a
-b
1)
                rest :: String
rest   = forall a. Show a => a -> String
extract (b
m forall a. Num a => a -> a -> a
- b
2)

                msb :: String
msb    = let top :: String
top = forall a. Show a => a -> String
show (b
mforall a. Num a => a -> a -> a
-b
1) in String
"((_ extract " forall a. [a] -> [a] -> [a]
++ String
top forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ String
top forall a. [a] -> [a] -> [a]
++ String
") " forall a. [a] -> [a] -> [a]
++ String
a forall a. [a] -> [a] -> [a]
++ String
")"
                ifPos :: String
ifPos  = String
"(bv2nat " forall a. [a] -> [a] -> [a]
++ String
rest forall a. [a] -> [a] -> [a]
++String
")"
                ifNeg :: String
ifNeg  = String
"(- " forall a. [a] -> [a] -> [a]
++ String
ifPos forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Integer
offset forall a. [a] -> [a] -> [a]
++ String
")"

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

        -- Some solvers support int2bv, but not all. So, we use a capability to determine.
        --
        -- NB. The "manual" implementation works regardless n < 0 or not, because the first thing we
        -- do is to compute "reduced" to bring it down to the correct range. It also works
        -- regardless were mapping to signed or unsigned bit-vector; because the representation
        -- is the same.
        i2b :: Int -> String
i2b Int
n
          | Bool
hasInt2bv
          = String
"((_ int2bv " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
") " forall a. [a] -> [a] -> [a]
++ String
a forall a. [a] -> [a] -> [a]
++ String
")"
          | Bool
True
          = String
"(let (" forall a. [a] -> [a] -> [a]
++ String
reduced forall a. [a] -> [a] -> [a]
++ String
") (let (" forall a. [a] -> [a] -> [a]
++ String
defs forall a. [a] -> [a] -> [a]
++ String
") " forall a. [a] -> [a] -> [a]
++ String
body forall a. [a] -> [a] -> [a]
++ String
"))"
          where b :: Int -> String
b Int
i      = forall a. Show a => a -> String
show (forall a. Bits a => Int -> a
bit Int
i :: Integer)
                reduced :: String
reduced  = String
"(__a (mod " forall a. [a] -> [a] -> [a]
++ String
a forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ Int -> String
b Int
n forall a. [a] -> [a] -> [a]
++ String
"))"
                mkBit :: Int -> String
mkBit Int
0  = String
"(__a0 (ite (= (mod __a 2) 0) #b0 #b1))"
                mkBit Int
i  = String
"(__a" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i forall a. [a] -> [a] -> [a]
++ String
" (ite (= (mod (div __a " forall a. [a] -> [a] -> [a]
++ Int -> String
b Int
i forall a. [a] -> [a] -> [a]
++ String
") 2) 0) #b0 #b1))"
                defs :: String
defs     = [String] -> String
unwords (forall a b. (a -> b) -> [a] -> [b]
map Int -> String
mkBit [Int
0 .. Int
n forall a. Num a => a -> a -> a
- Int
1])
                body :: String
body     = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\String
c String
r -> String
"(concat " forall a. [a] -> [a] -> [a]
++ String
c forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ String
r forall a. [a] -> [a] -> [a]
++ String
")") [String
"__a" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i | Int
i <- [Int
nforall a. Num a => a -> a -> a
-Int
1, Int
nforall a. Num a => a -> a -> a
-Int
2 .. Int
0]]

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

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

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