-----------------------------------------------------------------------------
-- |
-- 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 #-}

{-# 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(..))
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

tbd :: String -> a
tbd :: String -> a
tbd String
e = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMTLib2: Not-yet-supported: " String -> String -> String
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 [(SV, CV)]
consts [((Int, Kind, Kind), [SV])]
tbls [(Int, ArrayInfo)]
arrs [(String, SBVType)]
uis [(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 Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
        hasReal :: Bool
hasReal        = Kind
KReal      Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
        hasFloat :: Bool
hasFloat       = Kind
KFloat     Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
        hasString :: Bool
hasString      = Kind
KString    Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
        hasChar :: Bool
hasChar        = Kind
KChar      Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
        hasDouble :: Bool
hasDouble      = Kind
KDouble    Kind -> Set Kind -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set Kind
kindInfo
        hasRounding :: Bool
hasRounding    = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String
s | (String
s, Maybe [String]
_) <- [(String, Maybe [String])]
usorts, String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
"RoundingMode"]
        hasBVs :: Bool
hasBVs         = Bool
hasChar Bool -> Bool -> Bool
|| Bool -> Bool
not ([()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [() | KBounded{} <- Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList Set Kind
kindInfo])   -- Remember, characters map to Word8
        usorts :: [(String, Maybe [String])]
usorts         = [(String
s, Maybe [String]
dt) | KUserSort String
s Maybe [String]
dt <- Set Kind -> [Kind]
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 String -> String -> Bool
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 (Bool -> Bool) -> ([()] -> Bool) -> [()] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [() | (Int
_, (String
_, (Kind
k1, Kind
k2), ArrayContext
_)) <- [(Int, ArrayInfo)]
arrs, Bool -> Bool
not (Kind -> Bool
forall a. HasKind a => a -> Bool
isBounded Kind
k1 Bool -> Bool -> Bool
&& Kind -> Bool
forall a. HasKind a => a -> Bool
isBounded Kind
k2)]
        hasArrayInits :: Bool
hasArrayInits  = (Bool -> Bool
not (Bool -> Bool) -> ([()] -> Bool) -> [()] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [()] -> Bool
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 (Bool -> Bool) -> ([()] -> Bool) -> [()] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [()] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) [() | (OvOp
_ :: OvOp) <- Seq (SV, SBVExpr) -> [OvOp]
forall from to. Biplate from to => from -> [to]
G.universeBi Seq (SV, SBVExpr)
asgnsSeq]
        hasList :: Bool
hasList        = (Kind -> Bool) -> Set Kind -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
forall a. HasKind a => a -> Bool
isList Set Kind
kindInfo
        hasSets :: Bool
hasSets        = (Kind -> Bool) -> Set Kind -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
forall a. HasKind a => a -> Bool
isSet Set Kind
kindInfo
        hasTuples :: Bool
hasTuples      = Bool -> Bool
not (Bool -> Bool) -> ([Int] -> Bool) -> [Int] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Int] -> Bool) -> [Int] -> Bool
forall a b. (a -> b) -> a -> b
$ [Int]
tupleArities
        hasEither :: Bool
hasEither      = (Kind -> Bool) -> Set Kind -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
forall a. HasKind a => a -> Bool
isEither Set Kind
kindInfo
        hasMaybe :: Bool
hasMaybe       = (Kind -> Bool) -> Set Kind -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
forall a. HasKind a => a -> Bool
isMaybe  Set Kind
kindInfo
        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 = [[String]] -> Maybe [String]
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 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
w
                          , String
"***     But the chosen solver (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Solver -> String
forall a. Show a => a -> String
show (SMTSolver -> Solver
name (SMTConfig -> SMTSolver
solver SMTConfig
cfg)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") doesn't support this feature."
                          ]

        setAll :: String -> [String]
setAll String
reason = [String
"(set-logic ALL) ; "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
reason String -> String -> String
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
                         []  -> Maybe Logic
forall a. Maybe a
Nothing
                         [Logic
l] -> Logic -> Maybe Logic
forall a. a -> Maybe a
Just Logic
l
                         [Logic]
ls  -> String -> Maybe Logic
forall a. HasCallStack => String -> a
error (String -> Maybe Logic) -> String -> Maybe Logic
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
""
                                                , String
"*** Only one setOption call to 'setLogic' is allowed, found: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([Logic] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Logic]
ls)
                                                , String
"***  " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Logic -> String) -> [Logic] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Logic -> String
forall a. Show a => a -> String
show [Logic]
ls)
                                                ]
           = case Logic
l of
               Logic
Logic_NONE -> [String
"; NB. Not setting the logic per user request of Logic_NONE"]
               Logic
_          -> [String
"(set-logic " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Logic -> String
forall a. Show a => a -> String
show Logic
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") ; NB. User specified."]

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

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

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

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

           | Bool
hasDouble Bool -> Bool -> Bool
|| Bool
hasFloat Bool -> Bool -> Bool
|| Bool
hasRounding
           = if Bool -> Bool
not ([SV] -> Bool
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 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
qs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
as String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ufs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"BV)"]
                                else [String
"(set-logic ALL)"] -- fall-thru
          where qs :: String
qs  | [SV] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls Bool -> Bool -> Bool
&& [(String, [String])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, [String])]
axs = String
"QF_"  -- axioms are likely to contain quantifiers
                    | Bool
True                     = String
""
                as :: String
as  | [(Int, ArrayInfo)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, ArrayInfo)]
arrs                = String
""
                    | Bool
True                     = String
"A"
                ufs :: String
ufs | [(String, SBVType)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, SBVType)]
uis Bool -> Bool -> Bool
&& [((Int, Kind, Kind), [SV])] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [((Int, Kind, Kind), [SV])]
tbls    = String
""     -- we represent tables as UFs
                    | Bool
True                     = String
"UF"

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

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

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

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

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

        pgm :: [String]
pgm  =  (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String
"; " String -> String -> String
forall a. [a] -> [a] -> [a]
++) [String]
comments
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
settings
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- uninterpreted sorts ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((String, Maybe [String]) -> [String])
-> [(String, Maybe [String])] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String, Maybe [String]) -> [String]
declSort [(String, Maybe [String])]
usorts
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- tuples ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Int -> [String]) -> [Int] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Int -> [String]
declTuple [Int]
tupleArities
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- sums ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (if Set Kind -> Bool
containsSum   Set Kind
kindInfo then [String]
declSum   else [])
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (if Set Kind -> Bool
containsMaybe Set Kind
kindInfo then [String]
declMaybe else [])
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- literal constants ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((SV, CV) -> [String]) -> [(SV, CV)] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SMTConfig -> (SV, CV) -> [String]
declConst SMTConfig
cfg) [(SV, CV)]
consts
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- skolem constants ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"(declare-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SV] -> SV -> String
svFunType [SV]
ss SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
userName SV
s | Right (SV
s, [SV]
ss) <- [Either SV (SV, [SV])]
skolemInps]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- optimization tracker variables ---" | Bool -> Bool
not ([NamedSymVar] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedSymVar]
trackerVars) ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"(declare-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [SV] -> SV -> String
svFunType [] SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") ; tracks " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm | (SV
s, String
nm) <- [NamedSymVar]
trackerVars]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- constant tables ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((((Int, Kind, Kind), [SV]), [String]) -> [String])
-> [(((Int, Kind, Kind), [SV]), [String])] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((String -> [String] -> [String]) -> (String, [String]) -> [String]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (:) ((String, [String]) -> [String])
-> ((((Int, Kind, Kind), [SV]), [String]) -> (String, [String]))
-> (((Int, Kind, Kind), [SV]), [String])
-> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((Int, Kind, Kind), [SV]), [String]) -> (String, [String])
constTable) [(((Int, Kind, Kind), [SV]), [String])]
constTables
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- skolemized tables ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((((Int, Kind, Kind), [SV]), [String]) -> String)
-> [(((Int, Kind, Kind), [SV]), [String])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> (((Int, Kind, Kind), [SV]), [String]) -> String
skolemTable ([String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
svType [SV]
foralls))) [(((Int, Kind, Kind), [SV]), [String])]
skolemTables
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- arrays ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
arrayConstants
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- uninterpreted constants ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((String, SBVType) -> [String]) -> [(String, SBVType)] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String, SBVType) -> [String]
declUI [(String, SBVType)]
uis
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- user given axioms ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((String, [String]) -> String) -> [(String, [String])] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, [String]) -> String
declAx [(String, [String])]
axs
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ String
"; --- formula ---" ]

             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((SV, SBVExpr) -> [String]) -> [(SV, SBVExpr)] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SMTConfig -> SkolemMap -> TableMap -> (SV, SBVExpr) -> [String]
declDef SMTConfig
cfg SkolemMap
skolemMap TableMap
tableMap) [(SV, SBVExpr)]
preQuantifierAssigns
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"(assert (forall (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n                 "
                                        [String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
svType SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")" | SV
s <- [SV]
foralls] String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                | Bool -> Bool
not ([SV] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls)
                ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((SV, SBVExpr) -> [String]) -> [(SV, SBVExpr)] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SV, SBVExpr) -> [String]
mkAssign [(SV, SBVExpr)]
postQuantifierAssigns

             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
arrayDelayeds

             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
arraySetups

             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String] -> [String]
delayedAsserts [String]
delayedEqualities

             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
finalAssert

        -- identify the assignments that can come before the first quantifier
        ([(SV, SBVExpr)]
preQuantifierAssigns, [(SV, SBVExpr)]
postQuantifierAssigns)
           | [SV] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls
           = ([], [(SV, SBVExpr)]
asgns)  -- the apparent "switch" here is OK; rest of the code works correctly if there are no foralls.
           | Bool
True
           = ((SV, SBVExpr) -> Bool)
-> [(SV, SBVExpr)] -> ([(SV, SBVExpr)], [(SV, SBVExpr)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (SV, SBVExpr) -> Bool
forall b. (SV, b) -> Bool
pre [(SV, SBVExpr)]
asgns
           where first :: NodeId
first      = SV -> NodeId
nodeId ([SV] -> SV
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 NodeId -> NodeId -> Bool
forall a. Ord a => a -> a -> Bool
< NodeId
first

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

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

        foralls :: [SV]
foralls    = [SV
s | Left SV
s <- [Either SV (SV, [SV])]
skolemInps]
        forallArgs :: String
forallArgs = (SV -> String) -> [SV] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (SV -> String) -> SV -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SV -> String
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 ([SV] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls), String
forallArgs) (((SV, CV) -> SV) -> [(SV, CV)] -> [SV]
forall a b. (a -> b) -> [a] -> [b]
map (SV, CV) -> SV
forall a b. (a, b) -> a
fst [(SV, CV)]
consts) ((Int, Kind, Kind), [SV])
t) | ((Int, Kind, Kind), [SV])
t <- [((Int, Kind, Kind), [SV])]
tbls]
        ([[String]]
arrayConstants, [[String]]
arrayDelayeds, [[String]]
arraySetups) = [([String], [String], [String])]
-> ([[String]], [[String]], [[String]])
forall a b c. [(a, b, c)] -> ([a], [b], [c])
unzip3 ([([String], [String], [String])]
 -> ([[String]], [[String]], [[String]]))
-> [([String], [String], [String])]
-> ([[String]], [[String]], [[String]])
forall a b. (a -> b) -> a -> b
$ ((Int, ArrayInfo) -> ([String], [String], [String]))
-> [(Int, ArrayInfo)] -> [([String], [String], [String])]
forall a b. (a -> b) -> [a] -> [b]
map (SMTConfig
-> Bool
-> [(SV, CV)]
-> SkolemMap
-> (Int, ArrayInfo)
-> ([String], [String], [String])
declArray SMTConfig
cfg (Bool -> Bool
not ([SV] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls)) [(SV, CV)]
consts SkolemMap
skolemMap) [(Int, ArrayInfo)]
arrs
        delayedEqualities :: [String]
delayedEqualities = ((((Int, Kind, Kind), [SV]), [String]) -> [String])
-> [(((Int, Kind, Kind), [SV]), [String])] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (((Int, Kind, Kind), [SV]), [String]) -> [String]
forall a b. (a, b) -> b
snd [(((Int, Kind, Kind), [SV]), [String])]
skolemTables

        delayedAsserts :: [String] -> [String]
delayedAsserts []              = []
        delayedAsserts ds :: [String]
ds@(String
deH : [String]
deTs)
          | [SV] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls = (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\String
s -> String
"(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")") [String]
ds
          | Bool
True         = (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
letShift ((String
"(and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
deH) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (String -> String) -> [String] -> [String]
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
          | [SV] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls Bool -> Bool -> Bool
&& Bool
noConstraints
          = []
          | [SV] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls
          =    (([(String, String)], Either SV SV) -> String)
-> [([(String, String)], Either SV SV)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\([(String, String)]
attr, Either SV SV
v) -> String
"(assert "      String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(String, String)] -> String -> String
addAnnotations [(String, String)]
attr (Either SV SV -> String
mkLiteral Either SV SV
v) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")") [([(String, String)], Either SV SV)]
hardAsserts
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (([(String, String)], Either SV SV) -> String)
-> [([(String, String)], Either SV SV)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\([(String, String)]
attr, Either SV SV
v) -> String
"(assert-soft " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(String, String)] -> String -> String
addAnnotations [(String, String)]
attr (Either SV SV -> String
mkLiteral Either SV SV
v) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")") [([(String, String)], Either SV SV)]
softAsserts
          | Bool -> Bool
not ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
namedAsserts)
          = String -> [String]
forall a. HasCallStack => String -> a
error (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [ String
"SBV: Constraints with attributes and quantifiers cannot be mixed!"
                                     , String
"   Quantified variables: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
forall a. Show a => a -> String
show [SV]
foralls)
                                     , String
"   Named constraints   : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
forall a. Show a => a -> String
show [String]
namedAsserts)
                                     ]
          | Bool -> Bool
not ([([(String, String)], Either SV SV)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [([(String, String)], Either SV SV)]
softAsserts)
          = String -> [String]
forall a. HasCallStack => String -> a
error (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"\n" [ String
"SBV: Soft constraints and quantifiers cannot be mixed!"
                                     , String
"   Quantified variables: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
forall a. Show a => a -> String
show [SV]
foralls)
                                     , String
"   Soft constraints    : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " ((([(String, String)], Either SV SV) -> String)
-> [([(String, String)], Either SV SV)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ([(String, String)], Either SV SV) -> String
forall a. Show a => a -> String
show [([(String, String)], Either SV SV)]
softAsserts)
                                     ]
          | Bool
True
          = [String -> String
impAlign (String -> String
letShift String
combined) String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
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 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SkolemMap -> SV -> String
cvtSV SkolemMap
skolemMap SV
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

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

                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 ([(String, String)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(String, String)]
attrs)]
                 where findName :: [(String, String)] -> String
findName [(String, String)]
attrs = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
"<anonymous>" ([String] -> Maybe String
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  | (Either SV SV -> Bool) -> [Either SV SV] -> Bool
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 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Either SV SV -> String) -> [Either SV SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Either SV SV -> String
mkLiteral [Either SV SV]
xs) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                  where lits :: [Either SV SV]
lits = (Either SV SV -> Bool) -> [Either SV SV] -> [Either SV SV]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (Either SV SV -> Bool) -> Either SV SV -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either SV SV -> Bool
redundant) ([Either SV SV] -> [Either SV SV])
-> [Either SV SV] -> [Either SV SV]
forall a b. (a -> b) -> a -> b
$ [Either SV SV] -> [Either SV SV]
forall a. Eq a => [a] -> [a]
nub ([Either SV SV] -> [Either SV SV]
forall a. Ord a => [a] -> [a]
sort ((([(String, String)], Either SV SV) -> Either SV SV)
-> [([(String, String)], Either SV SV)] -> [Either SV SV]
forall a b. (a -> b) -> [a] -> [b]
map ([(String, String)], Either SV SV) -> Either SV SV
forall a b. (a, b) -> b
snd [([(String, String)], Either SV SV)]
hardAsserts))
                        redundant :: Either SV SV -> Bool
redundant (Left SV
v)  = SV
v SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV
                        redundant (Right SV
v) = SV
v SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV
                        bad :: Either SV SV -> Bool
bad (Left  SV
v) = SV
v SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV
                        bad (Right SV
v) = SV
v SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV

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

        align :: Int -> String -> String
align Int
n String
s = Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
n Char
' ' String -> String -> String
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
           | [(Bool, [(String, String)], Either SV SV)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Bool, [(String, String)], Either SV SV)]
finals = (Bool
True,  [(Bool
False, [], SV -> Either SV SV
forall a b. a -> Either a b
Left SV
trueSV)])
           | Bool
True        = (Bool
False, [(Bool, [(String, String)], Either SV SV)]
finals)

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

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

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

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

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

        skolemMap :: SkolemMap
skolemMap = [(SV, [SV])] -> 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 ([SV] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
ss)]
        tableMap :: TableMap
tableMap  = [(Int, String)] -> TableMap
forall a. [(Int, a)] -> IntMap a
IM.fromList ([(Int, String)] -> TableMap) -> [(Int, String)] -> TableMap
forall a b. (a -> b) -> a -> b
$ ((((Int, Kind, Kind), [SV]), [String]) -> (Int, String))
-> [(((Int, Kind, Kind), [SV]), [String])] -> [(Int, String)]
forall a b. (a -> b) -> [a] -> [b]
map (((Int, Kind, Kind), [SV]), [String]) -> (Int, String)
forall a b c b b. Show a => (((a, b, c), b), b) -> (a, String)
mkConstTable [(((Int, Kind, Kind), [SV]), [String])]
constTables [(Int, String)] -> [(Int, String)] -> [(Int, String)]
forall a. [a] -> [a] -> [a]
++ ((((Int, Kind, Kind), [SV]), [String]) -> (Int, String))
-> [(((Int, Kind, Kind), [SV]), [String])] -> [(Int, String)]
forall a b. (a -> b) -> [a] -> [b]
map (((Int, Kind, Kind), [SV]), [String]) -> (Int, String)
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" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
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" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
forallArgs)
        asgns :: [(SV, SBVExpr)]
asgns = Seq (SV, SBVExpr) -> [(SV, SBVExpr)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (SV, SBVExpr)
asgnsSeq

        mkAssign :: (SV, SBVExpr) -> [String]
mkAssign (SV, SBVExpr)
a
          | [SV] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls = SMTConfig -> SkolemMap -> TableMap -> (SV, SBVExpr) -> [String]
declDef SMTConfig
cfg SkolemMap
skolemMap TableMap
tableMap (SV, SBVExpr)
a
          | Bool
True         = [String -> String
letShift ((SV, SBVExpr) -> String
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 ((" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SkolemMap -> SV -> String
cvtSV                SkolemMap
skolemMap          SV
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")) ; " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
m
        mkLet (a
s, SBVExpr
e)                    = String
"(let ((" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SolverCapabilities
-> RoundingMode -> SkolemMap -> TableMap -> SBVExpr -> String
cvtExp SolverCapabilities
solverCaps RoundingMode
rm SkolemMap
skolemMap TableMap
tableMap SBVExpr
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"

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

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

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

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

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

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

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

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

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

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

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))))))"
            ]

-- | 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 [(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
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((String, Maybe [String]) -> [String])
-> [(String, Maybe [String])] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String, Maybe [String]) -> [String]
declSort [(String
s, Maybe [String]
dt) | KUserSort String
s Maybe [String]
dt <- [Kind]
newKinds]
            -- tuples. NB. Only declare the new sizes, old sizes persist.
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Int -> [String]) -> [Int] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Int -> [String]
declTuple (Set Kind -> [Int]
findTupleArities Set Kind
newKs)
            -- sums
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (if Set Kind -> Bool
containsSum   Set Kind
newKs then [String]
declSum   else [])
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (if Set Kind -> Bool
containsMaybe Set Kind
newKs then [String]
declMaybe else [])
            -- constants
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((SV, CV) -> [String]) -> [(SV, CV)] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SMTConfig -> (SV, CV) -> [String]
declConst SMTConfig
cfg) [(SV, CV)]
consts
            -- inputs
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (NamedSymVar -> String) -> [NamedSymVar] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map NamedSymVar -> String
forall b. (SV, b) -> String
declInp [NamedSymVar]
inps
            -- arrays
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
arrayConstants
            -- uninterpreteds
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((String, SBVType) -> [String]) -> [(String, SBVType)] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String, SBVType) -> [String]
declUI [(String, SBVType)]
uis
            -- table declarations
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
tableDecls
            -- expressions
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((SV, SBVExpr) -> [String]) -> [(SV, SBVExpr)] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (SMTConfig -> SkolemMap -> TableMap -> (SV, SBVExpr) -> [String]
declDef SMTConfig
cfg SkolemMap
forall k a. Map k a
skolemMap TableMap
tableMap) (Seq (SV, SBVExpr) -> [(SV, SBVExpr)]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (SV, SBVExpr)
asgnsSeq)
            -- delayed equalities
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
arrayDelayeds
            -- table setups
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
tableAssigns
            -- array setups
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[String]]
arraySetups
            -- extra constraints
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((Bool, [(String, String)], SV) -> String)
-> [(Bool, [(String, String)], SV)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\(Bool
isSoft, [(String, String)]
attr, SV
v) -> String
"(assert" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
isSoft then String
"-soft " else String
" ") String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(String, String)] -> String -> String
addAnnotations [(String, String)]
attr (SkolemMap -> SV -> String
cvtSV SkolemMap
forall k a. Map k a
skolemMap SV
v) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")") (Seq (Bool, [(String, String)], SV)
-> [(Bool, [(String, String)], SV)]
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 = Map k a
forall k a. Map k a
M.empty

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

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

        declInp :: (SV, b) -> String
declInp (SV
s, b
_) = String
"(declare-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" () " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
svType SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

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

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

        tableMap :: TableMap
tableMap  = [(Int, String)] -> TableMap
forall a. [(Int, a)] -> IntMap a
IM.fromList ([(Int, String)] -> TableMap) -> [(Int, String)] -> TableMap
forall a b. (a -> b) -> a -> b
$ ((((Int, Kind, Kind), [SV]), [String]) -> (Int, String))
-> [(((Int, Kind, Kind), [SV]), [String])] -> [(Int, String)]
forall a b. (a -> b) -> [a] -> [b]
map (((Int, Kind, Kind), [SV]), [String]) -> (Int, String)
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" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
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
          | (Kind -> Bool) -> [Kind] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Kind -> Bool
needsFlattening [Kind]
newKinds
          = [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([Maybe [String]] -> [[String]]
forall a. [Maybe a] -> [a]
catMaybes [SolverCapabilities -> Maybe [String]
supportsFlattenedModels SolverCapabilities
solverCaps])
          | Bool
True
          = []
          where solverCaps :: SolverCapabilities
solverCaps = SMTSolver -> SolverCapabilities
capabilities (SMTConfig -> SMTSolver
solver SMTConfig
cfg)

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

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

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

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

declUI :: (String, SBVType) -> [String]
declUI :: (String, SBVType) -> [String]
declUI (String
i, SBVType
t) = [String
"(declare-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVType -> String
cvtType SBVType
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"]

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

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

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

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

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

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

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 String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
qsIn then String
"" else String
qsIn String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
        t :: String
t    = String
"table" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i
        decl :: String
decl = String
"(declare-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
qs String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
ak String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
rk String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

-- 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)
  | [(Bool, (String, String))] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Bool, (String, String))]
post = [String] -> Either [String] [String]
forall a b. a -> Either a b
Left  (((Bool, (String, String)) -> String)
-> [(Bool, (String, String))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String, String) -> String
topLevel ((String, String) -> String)
-> ((Bool, (String, String)) -> (String, String))
-> (Bool, (String, String))
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool, (String, String)) -> (String, String)
forall a b. (a, b) -> b
snd) [(Bool, (String, String))]
pre)
  | Bool
True      = [String] -> Either [String] [String]
forall a b. b -> Either a b
Right (((Bool, (String, String)) -> String)
-> [(Bool, (String, String))] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String, String) -> String
nested   ((String, String) -> String)
-> ((Bool, (String, String)) -> (String, String))
-> (Bool, (String, String))
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool, (String, String)) -> (String, String)
forall a b. (a, b) -> b
snd) ([(Bool, (String, String))]
pre [(Bool, (String, String))]
-> [(Bool, (String, String))] -> [(Bool, (String, String))]
forall a. [a] -> [a] -> [a]
++ [(Bool, (String, String))]
post))
  where ssv :: SV -> String
ssv = SkolemMap -> SV -> String
cvtSV SkolemMap
skolemMap
        ([(Bool, (String, String))]
pre, [(Bool, (String, String))]
post) = ((Bool, (String, String)) -> Bool)
-> [(Bool, (String, String))]
-> ([(Bool, (String, String))], [(Bool, (String, String))])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Bool, (String, String)) -> Bool
forall a b. (a, b) -> a
fst ((SV -> Int -> (Bool, (String, String)))
-> [SV] -> [Int] -> [(Bool, (String, String))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SV -> Int -> (Bool, (String, String))
forall a. Integral a => SV -> a -> (Bool, (String, String))
mkElt [SV]
elts [(Int
0::Int)..])
        t :: String
t           = String
"table" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i

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

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

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

-- 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 -> [(SV, CV)] -> SkolemMap -> (Int, ArrayInfo) -> ([String], [String], [String])
declArray :: SMTConfig
-> Bool
-> [(SV, CV)]
-> SkolemMap
-> (Int, ArrayInfo)
-> ([String], [String], [String])
declArray SMTConfig
cfg Bool
quantified [(SV, CV)]
consts SkolemMap
skolemMap (Int
i, (String
_, (Kind
aKnd, Kind
bKnd), ArrayContext
ctx)) = (String
adecl String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Int -> String -> String) -> [Int] -> [String] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> String -> String
wrap [(Int
0::Int)..] (((Bool, String) -> String) -> [(Bool, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Bool, String) -> String
forall a b. (a, b) -> b
snd [(Bool, String)]
pre), (Int -> String -> String) -> [Int] -> [String] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> String -> String
wrap [Int
lpre..] (((Bool, String) -> String) -> [(Bool, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Bool, String) -> String
forall a b. (a, b) -> b
snd [(Bool, String)]
post), [String]
setup)
  where constNames :: [SV]
constNames = ((SV, CV) -> SV) -> [(SV, CV)] -> [SV]
forall a b. (a -> b) -> [a] -> [b]
map (SV, CV) -> SV
forall a b. (a, b) -> a
fst [(SV, CV)]
consts
        topLevel :: Bool
topLevel = Bool -> Bool
not Bool
quantified Bool -> Bool -> Bool
|| case ArrayContext
ctx of
                                       ArrayFree Maybe SV
mbi      -> Bool -> (SV -> Bool) -> Maybe SV -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (SV -> [SV] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SV]
constNames) Maybe SV
mbi
                                       ArrayMutate ArrayIndex
_ SV
a SV
b  -> (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SV -> [SV] -> Bool
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 SV -> [SV] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SV]
constNames
        ([(Bool, String)]
pre, [(Bool, String)]
post) = ((Bool, String) -> Bool)
-> [(Bool, String)] -> ([(Bool, String)], [(Bool, String)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Bool, String) -> Bool
forall a b. (a, b) -> a
fst [(Bool, String)]
ctxInfo
        nm :: String
nm = String
"array_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i

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

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

        adecl :: String
adecl = case ArrayContext
ctx of
                  ArrayFree (Just SV
v) -> String
"(define-fun "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" () " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
atyp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ((as const " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
atyp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
constInit SV
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
                  ArrayContext
_                  -> String
"(declare-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" () " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
atyp String -> String -> String
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 SV -> [(SV, CV)] -> Maybe CV
forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(SV, CV)]
consts 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 -> [((SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (SV -> [SV] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SV]
constNames) [SV
a, SV
b], String
"(= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (store array_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ ArrayIndex -> String
forall a. Show a => a -> String
show ArrayIndex
j String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))")]
                    ArrayMerge  SV
t ArrayIndex
j ArrayIndex
k -> [(SV
t SV -> [SV] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SV]
constNames,            String
"(= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" array_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ ArrayIndex -> String
forall a. Show a => a -> String
show ArrayIndex
j String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" array_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ ArrayIndex -> String
forall a. Show a => a -> String
show ArrayIndex
k String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))")]

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

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

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

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

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

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

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

type SkolemMap = M.Map SV [SV]
type TableMap  = IM.IntMap 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 SV -> SkolemMap -> Maybe [SV]
forall k a. Ord k => k -> Map k a -> Maybe a
`M.lookup` SkolemMap
skolemMap
  = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
forall a. Show a => a -> String
show SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ (SV -> String) -> [SV] -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (SV -> String) -> SV -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SV -> String
forall a. Show a => a -> String
show) [SV]
ss String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
  | SV
s SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV
  = String
"true"
  | SV
s SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV
  = String
"false"
  | Bool
True
  = Char
's' Char -> String -> String
forall a. a -> [a] -> [a]
: Int -> String
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 Int -> TableMap -> Maybe String
forall a. Int -> IntMap a -> Maybe a
`IM.lookup` TableMap
m = String
tn
  | Bool
True                       = String
"table" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i  -- constant tables are always named this way

cvtExp :: SolverCapabilities -> RoundingMode -> SkolemMap -> TableMap -> SBVExpr -> String
cvtExp :: SolverCapabilities
-> RoundingMode -> SkolemMap -> TableMap -> SBVExpr -> String
cvtExp SolverCapabilities
caps RoundingMode
rm SkolemMap
skolemMap TableMap
tableMap 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     = (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SV -> Bool
forall a. HasKind a => a -> Bool
isBounded   [SV]
arguments
        intOp :: Bool
intOp    = (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SV -> Bool
forall a. HasKind a => a -> Bool
isUnbounded [SV]
arguments
        realOp :: Bool
realOp   = (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SV -> Bool
forall a. HasKind a => a -> Bool
isReal      [SV]
arguments
        doubleOp :: Bool
doubleOp = (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SV -> Bool
forall a. HasKind a => a -> Bool
isDouble    [SV]
arguments
        floatOp :: Bool
floatOp  = (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SV -> Bool
forall a. HasKind a => a -> Bool
isFloat     [SV]
arguments
        boolOp :: Bool
boolOp   = (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SV -> Bool
forall a. HasKind a => a -> Bool
isBoolean   [SV]
arguments
        charOp :: Bool
charOp   = (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SV -> Bool
forall a. HasKind a => a -> Bool
isChar      [SV]
arguments
        stringOp :: Bool
stringOp = (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SV -> Bool
forall a. HasKind a => a -> Bool
isString    [SV]
arguments
        listOp :: Bool
listOp   = (SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SV -> Bool
forall a. HasKind a => a -> Bool
isList      [SV]
arguments

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

        ensureBVOrBool :: Bool
ensureBVOrBool = Bool
bvOp Bool -> Bool -> Bool
|| Bool
boolOp Bool -> Bool -> Bool
|| Bool
forall p. p
bad
        ensureBV :: Bool
ensureBV       = Bool
bvOp Bool -> Bool -> Bool
|| Bool
forall p. p
bad

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

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

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

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

        lift1FP :: String -> String -> p -> [String] -> String
lift1FP String
o String
fo | Bool
doubleOp Bool -> Bool -> Bool
|| Bool
floatOp = String -> p -> [String] -> String
forall p. String -> p -> [String] -> String
lift1 String
fo
                     | Bool
True                = String -> p -> [String] -> String
forall p. String -> p -> [String] -> String
lift1 String
o

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

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

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

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

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

        notEqual :: p -> [String] -> String
notEqual p
sgn [String]
sbvs
          | Bool
doubleOp Bool -> Bool -> Bool
|| Bool
floatOp Bool -> Bool -> Bool
|| Bool -> Bool
not Bool
hasDistinct = [String] -> String
forall a. [a] -> String
liftP [String]
sbvs
          | Bool
True                                   = String -> p -> [String] -> String
forall p. String -> p -> [String] -> String
liftN String
"distinct" p
sgn [String]
sbvs
          where liftP :: [a] -> String
liftP [a
_, a
_] = String
"(not " String -> String -> String
forall a. [a] -> [a] -> [a]
++ p -> [String] -> String
forall p. p -> [String] -> String
equal p
sgn [String]
sbvs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                liftP [a]
args   = String
"(and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ([a] -> [String]
walk [a]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

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

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

        lift2Cmp :: String -> String -> p -> [String] -> String
lift2Cmp String
o String
fo | Bool
doubleOp Bool -> Bool -> Bool
|| Bool
floatOp = String -> p -> [String] -> String
forall p. String -> p -> [String] -> String
lift2 String
fo
                      | Bool
True                = String -> p -> [String] -> String
forall p. String -> p -> [String] -> String
lift2 String
o

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

        -- NB. String comparisons are currently not supported by Z3; but will be with the new logic.
        stringCmp :: Bool -> String -> [String] -> String
stringCmp Bool
swap String
o [String
a, String
b]
          | Kind
KString <- SV -> Kind
forall a. HasKind a => a -> Kind
kindOf ([SV] -> SV
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
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        stringCmp Bool
_ String
o [String]
sbvs = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"SBV.SMT.SMTLib2.sh.stringCmp: Unexpected arguments: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (String, [String]) -> String
forall a. Show a => a -> String
show (String
o, [String]
sbvs)

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

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

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

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

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

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

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

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

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

                mkCnst :: Int -> String
mkCnst = RoundingMode -> CV -> String
cvtCV RoundingMode
rm (CV -> String) -> (Int -> CV) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Kind -> Int -> CV
forall a. Integral a => Kind -> a -> CV
mkConstCV (SV -> Kind
forall a. HasKind a => a -> Kind
kindOf SV
i)
                le0 :: String
le0  = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
less String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
mkCnst Int
0 String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
                gtl :: String
gtl  = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
leq  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
mkCnst Int
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
i String -> String -> String
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_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ ArrayIndex -> String
forall a. Show a => a -> String
show ArrayIndex
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" array_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ ArrayIndex -> String
forall a. Show a => a -> String
show ArrayIndex
j String -> String -> String
forall a. [a] -> [a] -> [a]
++String
")"
        sh (SBVApp (ArrRead ArrayIndex
i) [SV
a]) = String
"(select array_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ ArrayIndex -> String
forall a. Show a => a -> String
show ArrayIndex
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

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

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

        sh (SBVApp Op
op [SV]
args)
          | Just Bool -> [String] -> String
f <- Op
-> [(Op, Bool -> [String] -> String)]
-> Maybe (Bool -> [String] -> String)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Op
op [(Op, Bool -> [String] -> String)]
forall p. [(Op, p -> [String] -> String)]
smtBVOpTable, Bool
ensureBVOrBool
          = Bool -> [String] -> String
f ((SV -> Bool) -> [SV] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any SV -> Bool
forall a. HasKind a => a -> Bool
hasSign [SV]
args) ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
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,  String -> String -> p -> [String] -> String
forall p. String -> String -> p -> [String] -> String
lift2B String
"and" String
"bvand")
                               , (Op
Or,   String -> String -> p -> [String] -> String
forall p. String -> String -> p -> [String] -> String
lift2B String
"or"  String
"bvor")
                               , (Op
XOr,  String -> String -> p -> [String] -> String
forall p. String -> String -> p -> [String] -> String
lift2B String
"xor" String
"bvxor")
                               , (Op
Not,  String -> String -> p -> [String] -> String
forall p. String -> String -> p -> [String] -> String
lift1B String
"not" String
"bvnot")
                               , (Op
Join, String -> p -> [String] -> String
forall p. String -> p -> [String] -> String
lift2 String
"concat")
                               ]

        sh (SBVApp (Label String
_) [SV
a]) = 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 ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
ssv [SV]
args))
        sh (SBVApp (IEEEFP FPOp
w                    ) [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ FPOp -> String
forall a. Show a => a -> String
show FPOp
w String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
ssv [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

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

        sh (SBVApp (PseudoBoolean PBOp
pb) [SV]
args)
          | Bool
hasPB = PBOp -> [String] -> String
handlePB PBOp
pb [String]
args'
          | Bool
True  = PBOp -> [String] -> String
reducePB PBOp
pb [String]
args'
          where args' :: [String]
args' = (SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
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 (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ OvOp -> String
forall a. Show a => a -> String
show OvOp
op String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
ssv [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"

        -- Note the unfortunate reversal in StrInRe..
        sh (SBVApp (StrOp (StrInRe RegExp
r)) [SV]
args) = String
"(str.in.re " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
ssv [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RegExp -> String
forall a. Show a => a -> String
show RegExp
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        sh (SBVApp (StrOp StrOp
op)          [SV]
args) = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ StrOp -> String
forall a. Show a => a -> String
show StrOp
op String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((SV -> String) -> [SV] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map SV -> String
ssv [SV]
args) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

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

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

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

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

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

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

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

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

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

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

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

                -- 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 chars, the underlying type is currently SWord8, so we go with the regular bit-vector operations
                -- TODO: This will change when we move to unicode!
                smtCharTable :: [(Op, Bool -> [String] -> String)]
smtCharTable = [ (Op
Equal,         Bool -> [String] -> String
forall p. p -> [String] -> String
eqBV)
                               , (Op
NotEqual,      Bool -> [String] -> String
forall p. p -> [String] -> String
neqBV)
                               , (Op
LessThan,      String -> String -> Bool -> [String] -> String
lift2S  String
"bvult" (String -> String
forall a. HasCallStack => String -> a
error String
"smtChar.<: did-not expect signed char here!"))
                               , (Op
GreaterThan,   String -> String -> Bool -> [String] -> String
lift2S  String
"bvugt" (String -> String
forall a. HasCallStack => String -> a
error String
"smtChar.>: did-not expect signed char here!"))
                               , (Op
LessEq,        String -> String -> Bool -> [String] -> String
lift2S  String
"bvule" (String -> String
forall a. HasCallStack => String -> a
error String
"smtChar.<=: did-not expect signed char here!"))
                               , (Op
GreaterEq,     String -> String -> Bool -> [String] -> String
lift2S  String
"bvuge" (String -> String
forall a. HasCallStack => String -> a
error String
"smtChar.>=: did-not expect signed char here!"))
                               ]

                -- For strings, equality and comparisons are the only operators
                -- TODO: The string comparison operators will most likely change with the new theory!
                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.<=")
                               ]

-----------------------------------------------------------------------------------------------
-- 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
kFrom Kind
kTo String
rm String
input
  | Kind
kFrom Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
kTo
  = String
input
  | Bool
True
  = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> Kind -> String -> String
cast Kind
kFrom Kind
kTo String
input String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
  where addRM :: String -> String -> String
addRM String
a String
s = String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a

        -- To go and back from Ints, we detour through reals
        cast :: Kind -> Kind -> String -> String
cast Kind
KUnbounded         Kind
KFloat             String
a = String
"(_ to_fp 8 24) "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (to_real " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        cast Kind
KUnbounded         Kind
KDouble            String
a = String
"(_ to_fp 11 53) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rm String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (to_real " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        cast Kind
KFloat             Kind
KUnbounded         String
a = String
"to_int (fp.to_real " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
        cast Kind
KDouble            Kind
KUnbounded         String
a = String
"to_int (fp.to_real " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

        -- To float/double
        cast (KBounded Bool
False Int
_) Kind
KFloat             String
a = String -> String -> String
addRM String
a String
"(_ to_fp_unsigned 8 24)"
        cast (KBounded Bool
False Int
_) Kind
KDouble            String
a = String -> String -> String
addRM String
a String
"(_ to_fp_unsigned 11 53)"
        cast (KBounded Bool
True  Int
_) Kind
KFloat             String
a = String -> String -> String
addRM String
a String
"(_ to_fp 8 24)"
        cast (KBounded Bool
True  Int
_) Kind
KDouble            String
a = String -> String -> String
addRM String
a String
"(_ to_fp 11 53)"
        cast Kind
KReal              Kind
KFloat             String
a = String -> String -> String
addRM String
a String
"(_ to_fp 8 24)"
        cast Kind
KReal              Kind
KDouble            String
a = String -> String -> String
addRM String
a String
"(_ to_fp 11 53)"

        -- Between floats
        cast Kind
KFloat             Kind
KFloat             String
a = String -> String -> String
addRM String
a String
"(_ to_fp 8 24)"
        cast Kind
KFloat             Kind
KDouble            String
a = String -> String -> String
addRM String
a String
"(_ to_fp 11 53)"
        cast Kind
KDouble            Kind
KFloat             String
a = String -> String -> String
addRM String
a String
"(_ to_fp 8 24)"
        cast Kind
KDouble            Kind
KDouble            String
a = String -> String -> String
addRM String
a String
"(_ to_fp 11 53)"

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

        cast Kind
KFloat             Kind
KReal              String
a = String
"fp.to_real" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a
        cast Kind
KDouble            Kind
KReal              String
a = String
"fp.to_real" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a

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

rot :: (SV -> String) -> String -> Int -> SV -> String
rot :: (SV -> String) -> String -> Int -> SV -> String
rot SV -> String
ssv String
o Int
c SV
x = String
"((_ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
x String -> String -> String
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
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
   where o :: String
o = if SV -> Bool
forall a. HasKind a => a -> Bool
hasSign SV
x then String
oS else String
oW

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

      Kind
_            -> String
tryFPCast

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

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

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

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

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

        -- 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 " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
          | Bool
True
          = String
"(let (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
reduced String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") (let (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
defs String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
body String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"))"
          where b :: Int -> String
b Int
i      = Integer -> String
forall a. Show a => a -> String
show (Int -> Integer
forall a. Bits a => Int -> a
bit Int
i :: Integer)
                reduced :: String
reduced  = String
"(__a (mod " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
b Int
n String -> String -> String
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" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" (ite (= (mod (div __a " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
b Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") 2) 0) #b0 #b1))"
                defs :: String
defs     = [String] -> String
unwords ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
mkBit [Int
0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1])
                body :: String
body     = (String -> String -> String) -> [String] -> String
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\String
c String
r -> String
"(concat " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")") [String
"__a" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i | Int
i <- [Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1, Int
nInt -> Int -> Int
forall 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 "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k                                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
handlePB (PB_AtLeast Int
k) [String]
args = String
"((_ at-least " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k                                             String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
handlePB (PB_Exactly Int
k) [String]
args = String
"((_ pbeq "     String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show (Int
k Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: Int -> Int -> [Int]
forall a. Int -> a -> [a]
replicate ([String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
args) Int
1)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
handlePB (PB_Eq [Int]
cs   Int
k) [String]
args = String
"((_ pbeq "     String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show (Int
k Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
cs))                        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
handlePB (PB_Le [Int]
cs   Int
k) [String]
args = String
"((_ pble "     String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show (Int
k Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
cs))                        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"
handlePB (PB_Ge [Int]
cs   Int
k) [String]
args = String
"((_ pbge "     String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ((Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show (Int
k Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
cs))                        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

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

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