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

{-# 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(..))
import Data.SBV.Core.Kind (smtType, needsFlattening)
import Data.SBV.SMT.Utils
import Data.SBV.Control.Types

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

tbd :: String -> a
tbd :: String -> a
tbd e :: String
e = String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ "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 ctx :: QueryContext
ctx kindInfo :: Set Kind
kindInfo isSat :: Bool
isSat comments :: [String]
comments (inputs :: [(Quantifier, NamedSymVar)]
inputs, trackerVars :: [NamedSymVar]
trackerVars) skolemInps :: [Either SV (SV, [SV])]
skolemInps consts :: [(SV, CV)]
consts tbls :: [((Int, Kind, Kind), [SV])]
tbls arrs :: [(Int, ArrayInfo)]
arrs uis :: [(String, SBVType)]
uis axs :: [(String, [String])]
axs (SBVPgm asgnsSeq :: Seq (SV, SBVExpr)
asgnsSeq) cstrs :: Seq (Bool, [(String, String)], SV)
cstrs out :: SV
out cfg :: 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 | (s :: String
s, _) <- [(String, Either String [String])]
usorts, String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "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, Either String [String])]
usorts         = [(String
s, Either String [String]
dt) | KUninterpreted s :: String
s dt :: Either String [String]
dt <- Set Kind -> [Kind]
forall a. Set a -> [a]
Set.toList Set Kind
kindInfo]
        trueUSorts :: [String]
trueUSorts     = [String
s | (s :: String
s, _) <- [(String, Either String [String])]
usorts, String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= "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) [() | (_, (_, (k1 :: Kind
k1, k2 :: Kind
k2), _)) <- [(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) [() | (_, (_, _, ArrayFree (Just _))) <- [(Int, ArrayInfo)]
arrs]
        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 | (w :: String
w, have :: Bool
have, need :: Bool
need) <- [(String, Bool, Bool)]
checks, Bool
need Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
have]
           where checks :: [(String, Bool, Bool)]
checks = [ ("data types",     SolverCapabilities -> Bool
supportsDataTypes SolverCapabilities
solverCaps, Bool
hasTuples Bool -> Bool -> Bool
|| Bool
hasEither Bool -> Bool -> Bool
|| Bool
hasMaybe)
                          , ("set operations", SolverCapabilities -> Bool
supportsSets      SolverCapabilities
solverCaps, Bool
hasSets)
                          ]

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

        -- Determining the logic is surprisingly tricky!
        logic :: [String]
logic
           -- user told us what to do: so just take it:
           | Just l :: Logic
l <- case [Logic
l | SetLogic l :: Logic
l <- SMTConfig -> [SMTOption]
solverSetOptions SMTConfig
cfg] of
                         []  -> Maybe Logic
forall a. Maybe a
Nothing
                         [l :: Logic
l] -> Logic -> Maybe Logic
forall a. a -> Maybe a
Just Logic
l
                         ls :: [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 [ ""
                                                , "*** 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
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_NONE -> ["; NB. Not setting the logic per user request of Logic_NONE"]
               _          -> ["(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]
++ ") ; NB. User specified."]

           -- There's a reason why we can't handle this problem:
           | Just cantDo :: [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
$   [ ""
                                 , "*** SBV is unable to choose a proper solver configuration:"
                                 , "***"
                                 ]
                             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
cantDo
                             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ "***"
                                , "*** Please report this as a feature request, either for SBV or the backend solver."
                                ]

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

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

           | Bool
hasInteger Bool -> Bool -> Bool
|| Bool
hasReal Bool -> Bool -> Bool
|| Bool -> Bool
not ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
trueUSorts) Bool -> Bool -> Bool
|| Bool
hasNonBVArrays Bool -> Bool -> Bool
|| Bool
hasTuples Bool -> Bool -> Bool
|| Bool
hasEither Bool -> Bool -> Bool
|| Bool
hasMaybe Bool -> Bool -> Bool
|| Bool
hasSets Bool -> Bool -> Bool
|| Bool
hasList Bool -> Bool -> Bool
|| Bool
hasString Bool -> Bool -> Bool
|| Bool
hasArrayInits
           = let why :: String
why | Bool
hasInteger            = "has unbounded values"
                     | Bool
hasReal               = "has algebraic reals"
                     | Bool -> Bool
not ([String] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
trueUSorts) = "has user-defined sorts"
                     | Bool
hasNonBVArrays        = "has non-bitvector arrays"
                     | Bool
hasTuples             = "has tuples"
                     | Bool
hasEither             = "has either type"
                     | Bool
hasMaybe              = "has maybe type"
                     | Bool
hasSets               = "has sets"
                     | Bool
hasList               = "has lists"
                     | Bool
hasString             = "has strings"
                     | Bool
hasArrayInits         = "has array initializers"
                     | Bool
True                  = "cannot determine the SMTLib-logic to use"
             in ["(set-logic ALL) ; "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
why String -> String -> String
forall a. [a] -> [a] -> [a]
++ ", using catch-all."]

           | 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 ["(set-logic ALL)"]
             else if Bool
hasBVs
                  then ["(set-logic QF_FPBV)"]
                  else ["(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
               QueryExternal -> ["(set-logic ALL) ; external query, using all logics."]
               QueryInternal -> ["(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]
++ "BV)"]
          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 = "QF_"  -- axioms are likely to contain quantifiers
                    | Bool
True                     = ""
                as :: String
as  | [(Int, ArrayInfo)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, ArrayInfo)]
arrs                = ""
                    | Bool
True                     = "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    = ""     -- we represent tables as UFs
                    | Bool
True                     = "UF"

        -- SBV always requires the production of models!
        getModels :: [String]
getModels   = "(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 flattenConfig :: [String]
flattenConfig <- [SolverCapabilities -> Maybe [String]
supportsFlattenedModels SolverCapabilities
solverCaps]]

        -- process all other settings we're given
        userSettings :: [String]
userSettings = (SMTOption -> [String]) -> [SMTOption] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap SMTOption -> [String]
opts ([SMTOption] -> [String]) -> [SMTOption] -> [String]
forall a b. (a -> b) -> a -> b
$ SMTConfig -> [SMTOption]
solverSetOptions SMTConfig
cfg
           where opts :: SMTOption -> [String]
opts SetLogic{} = []     -- processed already
                 opts o :: SMTOption
o          = [SMTOption -> String
setSMTOption SMTOption
o]

        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
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]
++ [ "; --- uninterpreted sorts ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((String, Either String [String]) -> [String])
-> [(String, Either String [String])] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String, Either String [String]) -> [String]
declSort [(String, Either String [String])]
usorts
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ "; --- 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]
++ [ "; --- 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]
++ [ "; --- 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]
++ [ "; --- skolem constants ---" ]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ "(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
forall a. [a] -> [a] -> [a]
++ [SV] -> SV -> String
svFunType [SV]
ss SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")" String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
userName SV
s | Right (s :: SV
s, ss :: [SV]
ss) <- [Either SV (SV, [SV])]
skolemInps]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ "; --- 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]
++ [ "(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
forall a. [a] -> [a] -> [a]
++ [SV] -> SV -> String
svFunType [] SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") ; tracks " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm | (s :: SV
s, nm :: String
nm) <- [NamedSymVar]
trackerVars]
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ "; --- 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 (Bool -> (((Int, Kind, Kind), [SV]), [String]) -> [String]
constTable Bool
False) [(((Int, Kind, Kind), [SV]), [String])]
constTables
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [ "; --- 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]
++ [ "; --- 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]
++ [ "; --- 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]
++ [ "; --- 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]
++ [ "; --- formula ---" ]

             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((SV, SBVExpr) -> String) -> [(SV, SBVExpr)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (SMTConfig -> SkolemMap -> TableMap -> (SV, SBVExpr) -> String
declDef SMTConfig
cfg SkolemMap
skolemMap TableMap
tableMap) [(SV, SBVExpr)]
preQuantifierAssigns
             [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ["(assert (forall (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n                 "
                                        ["(" 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
forall a. [a] -> [a] -> [a]
++ SV -> String
svType SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")" | SV
s <- [SV]
foralls] String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                | 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 a b. (a -> b) -> [a] -> [b]
map (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
        (preQuantifierAssigns :: [(SV, SBVExpr)]
preQuantifierAssigns, postQuantifierAssigns :: [(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 (s :: SV
s, _) = SV -> NodeId
nodeId SV
s NodeId -> NodeId -> Bool
forall a. Ord a => a -> a -> Bool
< NodeId
first

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

        noOfCloseParens :: Int
noOfCloseParens
          | [SV] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SV]
foralls = 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
+ 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 0 else 1)

        foralls :: [SV]
foralls    = [SV
s | Left s :: 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
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

        (constTables :: [(((Int, Kind, Kind), [SV]), [String])]
constTables, skolemTables :: [(((Int, Kind, Kind), [SV]), [String])]
skolemTables) = ([(((Int, Kind, Kind), [SV])
t, [String]
d) | (t :: ((Int, Kind, Kind), [SV])
t, Left d :: [String]
d) <- [(((Int, Kind, Kind), [SV]), Either [String] [String])]
allTables], [(((Int, Kind, Kind), [SV])
t, [String]
d) | (t :: ((Int, Kind, Kind), [SV])
t, Right d :: [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]
        (arrayConstants :: [[String]]
arrayConstants, arrayDelayeds :: [[String]]
arrayDelayeds, arraySetups :: [[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
-> Bool
-> [(SV, CV)]
-> SkolemMap
-> (Int, ArrayInfo)
-> ([String], [String], [String])
declArray SMTConfig
cfg Bool
False (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@(deH :: String
deH : deTs :: [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 (\s :: String
s -> "(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")") [String]
ds
          | Bool
True         = (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String
letShift (("(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 5) [String]
deTs)

        letShift :: String -> String
letShift = Int -> String -> String
align 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 (\(attr :: [(String, String)]
attr, v :: Either SV SV
v) -> "(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)], 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 (\(attr :: [(String, String)]
attr, v :: Either SV SV
v) -> "(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)], 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 "\n" [ "SBV: Constraints with attributes and quantifiers cannot be mixed!"
                                     , "   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)
                                     , "   Named constraints   : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " ((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 "\n" [ "SBV: Soft constraints and quantifiers cannot be mixed!"
                                     , "   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)
                                     , "   Soft constraints    : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate ", " ((([(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 ')']
          where mkLiteral :: Either SV SV -> String
mkLiteral (Left  v :: SV
v) =            SkolemMap -> SV -> String
cvtSV SkolemMap
skolemMap SV
v
                mkLiteral (Right v :: SV
v) = "(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]
++ ")"

                (noConstraints :: Bool
noConstraints, assertions :: [(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 | (_, attrs :: [(String, String)]
attrs, _) <- [(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 attrs :: [(String, String)]
attrs = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "<anonymous>" ([String] -> Maybe String
forall a. [a] -> Maybe a
listToMaybe [String
nm | (":named", nm :: 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) | (False, attr :: [(String, String)]
attr, v :: 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) | (True,  attr :: [(String, String)]
attr, v :: Either SV SV
v) <- [(Bool, [(String, String)], Either SV SV)]
assertions]

                combined :: String
combined = case [Either SV SV]
lits of
                             []               -> "true"
                             [x :: Either SV SV
x]              -> Either SV SV -> String
mkLiteral Either SV SV
x
                             xs :: [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 -> "false"
                                 | Bool
True       -> "(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]
++ ")"
                  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 v :: SV
v)  = SV
v SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV
                        redundant (Right v :: SV
v) = SV
v SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV
                        bad :: Either SV SV -> Bool
bad (Left  v :: SV
v) = SV
v SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV
                        bad (Right v :: SV
v) = SV
v SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV

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

        align :: Int -> String -> String
align n :: Int
n s :: String
s = Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
n ' ' 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 [] (\r :: 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') | (isSoft :: Bool
isSoft, attrs :: [(String, String)]
attrs, c :: 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 c' :: 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 s :: 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 s :: 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 (s :: SV
s, ss :: [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 (((t :: a
t, _, _), _), _) = (a
t, "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    (((t :: a
t, _, _), _), _) = (a
t, "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 a :: (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 (s :: a
s, SBVApp (Label m :: String
m) [e :: SV
e]) = "(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
forall a. [a] -> [a] -> [a]
++ SkolemMap -> SV -> String
cvtSV                SkolemMap
skolemMap          SV
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")) ; " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
m
        mkLet (s :: a
s, e :: SBVExpr
e)                    = "(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
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]
++ "))"

        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 s :: 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 u :: 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 -> " ; tracks user variable " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
u
                        _ -> ""

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

-- | 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 arity :: Int
arity
  | Int
arity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 = ["(declare-datatypes ((SBVTuple0 0)) (((mkSBVTuple0))))"]
  | Int
arity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1 = String -> [String]
forall a. HasCallStack => String -> a
error "Data.SBV.declTuple: Unexpected one-tuple"
  | Bool
True       =    (String
l1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "(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 <- [1..Int
arity]] String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")")
                 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 <- [1..Int
arity]]
  where l1 :: String
l1     = "(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
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
arity String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")) ("
        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) ' ' String -> String -> String
forall a. [a] -> [a] -> [a]
++ "((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]
++ " "
        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) ' '

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

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

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

        param :: a -> String
param i :: a
i = "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 ks :: 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 tupKs :: [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 = [ "(declare-datatypes ((SBVEither 2)) ((par (T1 T2)"
          , "                                    ((left_SBVEither  (get_left_SBVEither  T1))"
          , "                                     (right_SBVEither (get_right_SBVEither T2))))))"
          ]

declMaybe :: [String]
declMaybe :: [String]
declMaybe = [ "(declare-datatypes ((SBVMaybe 1)) ((par (T)"
            , "                                    ((nothing_SBVMaybe)"
            , "                                     (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 :: Bool -> SMTLibIncConverter [String]
cvtInc :: Bool -> SMTLibIncConverter [String]
cvtInc afterAPush :: Bool
afterAPush inps :: [NamedSymVar]
inps newKs :: Set Kind
newKs consts :: [(SV, CV)]
consts arrs :: [(Int, ArrayInfo)]
arrs tbls :: [((Int, Kind, Kind), [SV])]
tbls uis :: [(String, SBVType)]
uis (SBVPgm asgnsSeq :: Seq (SV, SBVExpr)
asgnsSeq) cstrs :: Seq (Bool, [(String, String)], SV)
cstrs cfg :: SMTConfig
cfg =
            -- any new settings?
               [String]
settings
            -- sorts
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((String, Either String [String]) -> [String])
-> [(String, Either String [String])] -> [String]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (String, Either String [String]) -> [String]
declSort [(String
s, Either String [String]
dt) | KUninterpreted s :: String
s dt :: Either String [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
            -- 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 (Bool -> (((Int, Kind, Kind), [SV]), [String]) -> [String]
constTable Bool
afterAPush) [(((Int, Kind, Kind), [SV]), [String])]
allTables
            -- expressions
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ ((SV, SBVExpr) -> String) -> [(SV, SBVExpr)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map  (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
            -- 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 (\(isSoft :: Bool
isSoft, attr :: [(String, String)]
attr, v :: SV
v) -> "(assert" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
isSoft then "-soft " else " ") 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]
++ ")") (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 (s :: SV
s, _) = "(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
forall a. [a] -> [a] -> [a]
++ SV -> String
svType SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

        (arrayConstants :: [[String]]
arrayConstants, arrayDelayeds :: [[String]]
arrayDelayeds, arraySetups :: [[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
-> Bool
-> [(SV, CV)]
-> SkolemMap
-> (Int, ArrayInfo)
-> ([String], [String], [String])
declArray SMTConfig
cfg Bool
afterAPush 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]
        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 (((t :: a
t, _, _), _), _) = (a
t, "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 cfg :: SMTConfig
cfg skolemMap :: SkolemMap
skolemMap tableMap :: TableMap
tableMap (s :: SV
s, expr :: SBVExpr
expr) =
        case SBVExpr
expr of
          SBVApp  (Label m :: String
m) [e :: SV
e] -> NamedSymVar -> Maybe String -> String
defineFun (SV
s, SkolemMap -> SV -> String
cvtSV          SkolemMap
skolemMap          SV
e) (String -> Maybe String
forall a. a -> Maybe a
Just String
m)
          e :: SBVExpr
e                     -> NamedSymVar -> Maybe String -> String
defineFun (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 :: (SV, String) -> Maybe String -> String
defineFun :: NamedSymVar -> Maybe String -> String
defineFun (s :: SV
s, def :: String
def) mbComment :: Maybe String
mbComment = "(define-fun "   String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
varT String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
def String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cmnt
  where varT :: String
varT      = SV -> String
forall a. Show a => a -> String
show SV
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " 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
forall a. [a] -> [a] -> [a]
++) Maybe String
mbComment

-- 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 cfg :: SMTConfig
cfg (s :: SV
s, c :: 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
  = [NamedSymVar -> Maybe String -> String
defineFun (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 (i :: String
i, t :: SBVType
t) = ["(declare-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SBVType -> String
cvtType SBVType
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"]

-- 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 (nm :: String
nm, ls :: [String]
ls) = (";; -- user given axiom: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n") String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate "\n" [String]
ls

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

        -- Arrange for initializers
        mkInit :: Int -> String
mkInit idx :: Int
idx   = "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]
++ "_initializer_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
idx :: Int)
        initializer :: String
initializer  = "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]
++ "_initializer"
        wrap :: Int -> String -> String
wrap index :: Int
index s :: String
s
          | Bool
afterAPush = "(define-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
mkInit Int
index String -> String -> String
forall a. [a] -> [a] -> [a]
++ " () Bool " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
          | Bool
True       = "(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
        lis :: Int
lis          = [String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
is
        setup :: [String]
setup
          | Bool -> Bool
not Bool
afterAPush = []
          | Int
lis Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0       = [ "(define-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
initializer String -> String -> String
forall a. [a] -> [a] -> [a]
++ " () Bool true) ; no initializiation needed"
                             ]
          | Int
lis Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1       = [ "(define-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
initializer String -> String -> String
forall a. [a] -> [a] -> [a]
++ " () Bool " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
mkInit 0 String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                             , "(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
initializer String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                             ]
          | Bool
True           = [ "(define-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
initializer String -> String -> String
forall a. [a] -> [a] -> [a]
++ " () 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 [0..Int
lis Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1]) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))"
                             , "(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
initializer String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                             ]


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

-- 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 rm :: RoundingMode
rm skolemMap :: SkolemMap
skolemMap (_quantified :: Bool
_quantified, args :: String
args) consts :: [SV]
consts ((i :: Int
i, aknd :: Kind
aknd, _), elts :: [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
        (pre :: [(Bool, (String, String))]
pre, post :: [(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 [(0::Int)..])
        t :: String
t           = "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 x :: SV
x k :: 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 (idx :: String
idx, v :: String
v) = "(= (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
idx String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
        nested :: (String, String) -> String
nested   (idx :: String
idx, v :: String
v) = "(= (" 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
forall a. [a] -> [a] -> [a]
++ String
idx String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

        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 -> Bool -> [(SV, CV)] -> SkolemMap -> (Int, ArrayInfo) -> ([String], [String], [String])
declArray :: SMTConfig
-> Bool
-> Bool
-> [(SV, CV)]
-> SkolemMap
-> (Int, ArrayInfo)
-> ([String], [String], [String])
declArray cfg :: SMTConfig
cfg afterAPush :: Bool
afterAPush quantified :: Bool
quantified consts :: [(SV, CV)]
consts skolemMap :: SkolemMap
skolemMap (i :: Int
i, (_, (aKnd :: Kind
aKnd, bKnd :: Kind
bKnd), ctx :: 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 [(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 mbi :: 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 _ a :: SV
a b :: 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 c :: SV
c _ _   -> SV
c SV -> [SV] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SV]
constNames
        (pre :: [(Bool, String)]
pre, post :: [(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 = "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
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 "Non-constant array initializer in a quantified context"

        atyp :: String
atyp  = "(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
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
bKnd String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

        adecl :: String
adecl = case ArrayContext
ctx of
                  ArrayFree (Just v :: SV
v) -> "(define-fun "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " () " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
atyp String -> String -> String
forall a. [a] -> [a] -> [a]
++ " ((as const " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
atyp String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
constInit SV
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))"
                  _                  -> "(declare-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " () " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
atyp String -> String -> String
forall a. [a] -> [a] -> [a]
++                                                  ")"

        -- 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 v :: 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
                        Nothing -> SV -> String
ssv SV
v                      -- Z3 will work, CVC4 will choke. Others don't even support this.
                        Just c :: 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 _       -> []
                    ArrayMutate j :: ArrayIndex
j a :: SV
a b :: 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
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " (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
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))")]
                    ArrayMerge  t :: SV
t j :: ArrayIndex
j k :: ArrayIndex
k -> [(SV
t SV -> [SV] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SV]
constNames,            "(= " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " (ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
t String -> String -> String
forall a. [a] -> [a] -> [a]
++ " 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]
++ " 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]
++ "))")]

        -- Arrange for initializers
        mkInit :: Int -> String
mkInit idx :: Int
idx    = "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]
++ "_initializer_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
idx :: Int)
        initializer :: String
initializer   = "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]
++ "_initializer"

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

        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
          | Bool -> Bool
not Bool
afterAPush = []
          | Int
lAll Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0      = [ "(define-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
initializer String -> String -> String
forall a. [a] -> [a] -> [a]
++ " () Bool true) ; no initializiation needed"
                             ]
          | Int
lAll Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 1      = [ "(define-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
initializer String -> String -> String
forall a. [a] -> [a] -> [a]
++ " () Bool " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
mkInit 0 String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                             , "(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
initializer String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                             ]
          | Bool
True           = [ "(define-fun " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
initializer String -> String -> String
forall a. [a] -> [a] -> [a]
++ " () 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 [0..Int
lAll Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1]) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))"
                             , "(assert " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
initializer String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                             ]

svType :: SV -> String
svType :: SV -> String
svType s :: 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 ss :: [SV]
ss s :: SV
s = "(" 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
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 "SBV.SMT.SMTLib2.cvtType: internal: received an empty type!"
cvtType (SBVType xs :: [Kind]
xs) = "(" 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
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
ret
  where (body :: [Kind]
body, ret :: 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
skolemMap s :: SV
s@(SV _ (NodeId n :: Int
n))
  | Just ss :: [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
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
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]
++ ")"
  | SV
s SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
trueSV
  = "true"
  | SV
s SV -> SV -> Bool
forall a. Eq a => a -> a -> Bool
== SV
falseSV
  = "false"
  | Bool
True
  = '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 m :: TableMap
m i :: Int
i
  | Just tn :: String
tn <- Int
i Int -> TableMap -> Maybe String
forall a. Int -> IntMap a -> Maybe a
`IM.lookup` TableMap
m = String
tn
  | Bool
True                       = "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 caps :: SolverCapabilities
caps rm :: RoundingMode
rm skolemMap :: SkolemMap
skolemMap tableMap :: TableMap
tableMap expr :: SBVExpr
expr@(SBVApp _ arguments :: [SV]
arguments) = SBVExpr -> String
sh SBVExpr
expr
  where ssv :: SV -> String
ssv = SkolemMap -> SV -> String
cvtSV SkolemMap
skolemMap

        supportsPB :: Bool
supportsPB = SolverCapabilities -> Bool
supportsPseudoBooleans 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
$ "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
$ "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 s :: String
s = String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RoundingMode -> String
smtRoundingMode RoundingMode
rm

        -- lift a binary op
        lift2 :: String -> p -> [String] -> String
lift2  o :: String
o _ [x :: String
x, y :: String
y] = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
        lift2  o :: String
o _ sbvs :: [String]
sbvs   = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "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 o :: String
o _ xs :: [String]
xs = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
xs String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

        -- lift a binary operation with rounding-mode added; used for floating-point arithmetic
        lift2WM :: String -> String -> p -> [String] -> String
lift2WM o :: String
o fo :: 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 o :: String
o fo :: 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 sgned :: Bool
sgned args :: [String]
args | Bool
doubleOp Bool -> Bool -> Bool
|| Bool
floatOp = String -> Bool -> [String] -> String
forall p. String -> p -> [String] -> String
lift1 "fp.abs" Bool
sgned [String]
args
                           | Bool
intOp               = String -> Bool -> [String] -> String
forall p. String -> p -> [String] -> String
lift1 "abs"    Bool
sgned [String]
args
                           | Bool
bvOp, Bool
sgned         = String -> String -> String -> String
mkAbs ([String] -> String
forall a. [a] -> a
head [String]
args) "bvslt" "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) "<"     "-"
          where mkAbs :: String -> String -> String -> String
mkAbs x :: String
x cmp :: String
cmp neg :: String
neg = "(ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
ltz String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
nx String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                  where ltz :: String
ltz = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
cmp String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
z String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                        nx :: String
nx  = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
neg String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                        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)) (0::Integer))

        lift2B :: String -> String -> p -> [String] -> String
lift2B bOp :: String
bOp vOp :: 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 bOp :: String
bOp vOp :: 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 "="
        neqBV :: p -> [String] -> String
neqBV = String -> p -> [String] -> String
forall p. String -> p -> [String] -> String
liftN "distinct"

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

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

                walk :: [String] -> [String]
walk []     = []
                walk (e :: String
e:es :: [String]
es) = (String -> String) -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> String -> String
pair String
e) [String]
es [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String] -> [String]
walk [String]
es

                pair :: String -> String -> String
pair e1 :: String
e1 e2 :: String
e2  = "(not (fp.eq " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
e1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
e2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))"

        lift2S :: String -> String -> Bool -> [String] -> String
lift2S oU :: String
oU oS :: String
oS sgn :: 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 oU :: String
oU oS :: String
oS sgn :: 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 o :: String
o fo :: 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 o :: String
o [a :: String
a, b :: String
b]
          | KUninterpreted s :: String
s (Right _) <- SV -> Kind
forall a. HasKind a => a -> Kind
kindOf ([SV] -> SV
forall a. [a] -> a
head [SV]
arguments)
          = let idx :: String -> String
idx v :: String
v = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_constrIndex " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")" in "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
idx String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
idx String
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
        unintComp o :: String
o sbvs :: [String]
sbvs = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "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 swap :: Bool
swap o :: String
o [a :: String
a, b :: String
b]
          | Kind
KString <- SV -> Kind
forall a. HasKind a => a -> Kind
kindOf ([SV] -> SV
forall a. [a] -> a
head [SV]
arguments)
          = let [a1 :: String
a1, a2 :: String
a2] | Bool
swap = [String
b, String
a]
                         | Bool
True = [String
a, String
b]
            in "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
        stringCmp _ o :: String
o sbvs :: [String]
sbvs = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "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 swap :: Bool
swap o :: String
o [a :: String
a, b :: String
b]
          | KList{} <- SV -> Kind
forall a. HasKind a => a -> Kind
kindOf ([SV] -> SV
forall a. [a] -> a
head [SV]
arguments)
          = let [a1 :: String
a1, a2 :: String
a2] | Bool
swap = [String
b, String
a]
                         | Bool
True = [String
a, String
b]
            in "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
        seqCmp _ o :: String
o sbvs :: [String]
sbvs = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "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  o :: String
o _ [x :: String
x]    = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
        lift1  o :: String
o _ sbvs :: [String]
sbvs   = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "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 fld :: String
fld args :: [SV]
args res :: Kind
res = "((as " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
fld String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Kind -> String
smtType Kind
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") " 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]
++ ")"

        -- Similarly, we fully qualify the accessors with their types to work around type checking issues
        dtAccessor :: String -> [Kind] -> Kind -> String
dtAccessor fld :: String
fld params :: [Kind]
params res :: Kind
res = String
result
          where ps :: String
ps       = " (" 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]
++ ") "
                result :: String
result   = "(_ 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]
++ "))"

        sh :: SBVExpr -> String
sh (SBVApp Ite [a :: SV
a, b :: SV
b, c :: SV
c]) = "(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
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

        sh (SBVApp (LkUp (t :: Int
t, aKnd :: Kind
aKnd, _, l :: Int
l) i :: SV
i e :: SV
e) [])
          | Bool
needsCheck = "(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
forall a. [a] -> [a] -> [a]
++ String
lkUp String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
          | Bool
True       = String
lkUp
          where needsCheck :: Bool
needsCheck = case Kind
aKnd of
                              KBool              -> (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 _ n :: Int
n       -> (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
                              KUnbounded         -> Bool
True
                              KReal              -> String -> Bool
forall a. HasCallStack => String -> a
error "SBV.SMT.SMTLib2.cvtExp: unexpected real valued index"
                              KFloat             -> String -> Bool
forall a. HasCallStack => String -> a
error "SBV.SMT.SMTLib2.cvtExp: unexpected float valued index"
                              KDouble            -> String -> Bool
forall a. HasCallStack => String -> a
error "SBV.SMT.SMTLib2.cvtExp: unexpected double valued index"
                              KChar              -> String -> Bool
forall a. HasCallStack => String -> a
error "SBV.SMT.SMTLib2.cvtExp: unexpected char valued index"
                              KString            -> String -> Bool
forall a. HasCallStack => String -> a
error "SBV.SMT.SMTLib2.cvtExp: unexpected string valued index"
                              KList k :: Kind
k            -> String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ "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  k :: Kind
k            -> String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ "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 k :: [Kind]
k           -> String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ "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 k :: Kind
k           -> String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ "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 k1 :: Kind
k1 k2 :: Kind
k2      -> String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ "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)
                              KUninterpreted s :: String
s _ -> String -> Bool
forall a. HasCallStack => String -> a
error (String -> Bool) -> String -> Bool
forall a b. (a -> b) -> a -> b
$ "SBV.SMT.SMTLib2.cvtExp: unexpected uninterpreted valued index: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s

                lkUp :: String
lkUp = "(" 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
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

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

                (less :: String
less, leq :: String
leq) = case Kind
aKnd of
                                KBool              -> String -> (String, String)
forall a. HasCallStack => String -> a
error "SBV.SMT.SMTLib2.cvtExp: unexpected boolean valued index"
                                KBounded{}         -> if SV -> Bool
forall a. HasKind a => a -> Bool
hasSign SV
i then ("bvslt", "bvsle") else ("bvult", "bvule")
                                KUnbounded         -> ("<", "<=")
                                KReal              -> ("<", "<=")
                                KFloat             -> ("fp.lt", "fp.leq")
                                KDouble            -> ("fp.lt", "fp.geq")
                                KChar              -> String -> (String, String)
forall a. HasCallStack => String -> a
error "SBV.SMT.SMTLib2.cvtExp: unexpected string valued index"
                                KString            -> String -> (String, String)
forall a. HasCallStack => String -> a
error "SBV.SMT.SMTLib2.cvtExp: unexpected string valued index"
                                KList k :: Kind
k            -> String -> (String, String)
forall a. HasCallStack => String -> a
error (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ "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  k :: Kind
k            -> String -> (String, String)
forall a. HasCallStack => String -> a
error (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ "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 k :: [Kind]
k           -> String -> (String, String)
forall a. HasCallStack => String -> a
error (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ "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 k :: Kind
k           -> String -> (String, String)
forall a. HasCallStack => String -> a
error (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ "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 k1 :: Kind
k1 k2 :: Kind
k2      -> String -> (String, String)
forall a. HasCallStack => String -> a
error (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ "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)
                                KUninterpreted s :: String
s _ -> String -> (String, String)
forall a. HasCallStack => String -> a
error (String -> (String, String)) -> String -> (String, String)
forall a b. (a -> b) -> a -> b
$ "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
forall a. [a] -> [a] -> [a]
++ String
less String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
mkCnst 0 String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                gtl :: String
gtl  = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
leq  String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
mkCnst Int
l String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

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

        sh (SBVApp (ArrEq i :: ArrayIndex
i j :: ArrayIndex
j) [])  = "(= 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]
++ " 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]
++")"
        sh (SBVApp (ArrRead i :: ArrayIndex
i) [a :: SV
a]) = "(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
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

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

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

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

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

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

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

        sh (SBVApp op :: Op
op args :: [SV]
args)
          | Just f :: 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 "and" "bvand")
                               , (Op
Or,   String -> String -> p -> [String] -> String
forall p. String -> String -> p -> [String] -> String
lift2B "or"  "bvor")
                               , (Op
XOr,  String -> String -> p -> [String] -> String
forall p. String -> String -> p -> [String] -> String
lift2B "xor" "bvxor")
                               , (Op
Not,  String -> String -> p -> [String] -> String
forall p. String -> String -> p -> [String] -> String
lift1B "not" "bvnot")
                               , (Op
Join, String -> p -> [String] -> String
forall p. String -> p -> [String] -> String
lift2 "concat")
                               ]

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

        sh (SBVApp (IEEEFP (FP_Cast kFrom :: Kind
kFrom kTo :: Kind
kTo m :: SV
m)) args :: [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 w :: FPOp
w                    ) args :: [SV]
args) = "(" 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
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]
++ ")"

        sh (SBVApp (PseudoBoolean pb :: PBOp
pb) args :: [SV]
args)
          | Bool
supportsPB = 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 op :: OvOp
op) args :: [SV]
args) = "(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
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]
++ "))"

        -- Note the unfortunate reversal in StrInRe..
        sh (SBVApp (StrOp (StrInRe r :: RegExp
r)) args :: [SV]
args) = "(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
forall a. [a] -> [a] -> [a]
++ RegExp -> String
forall a. Show a => a -> String
show RegExp
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
        sh (SBVApp (StrOp op :: StrOp
op)          args :: [SV]
args) = "(" 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
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]
++ ")"

        sh (SBVApp (SeqOp op :: SeqOp
op) args :: [SV]
args) = "(" 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
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]
++ ")"

        sh (SBVApp (SetOp SetEqual)      args :: [SV]
args)   = "(= "      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]
++ ")"
        sh (SBVApp (SetOp SetMember)     [e :: SV
e, s :: SV
s]) = "(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
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
        sh (SBVApp (SetOp SetInsert)     [e :: SV
e, s :: SV
s]) = "(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
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ " true)"
        sh (SBVApp (SetOp SetDelete)     [e :: SV
e, s :: SV
s]) = "(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
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ " false)"
        sh (SBVApp (SetOp SetIntersect)  args :: [SV]
args)   = "(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]
++ ")"
        sh (SBVApp (SetOp SetUnion)      args :: [SV]
args)   = "(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]
++ ")"
        sh (SBVApp (SetOp SetSubset)     args :: [SV]
args)   = "(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]
++ ")"
        sh (SBVApp (SetOp SetDifference) args :: [SV]
args)   = "(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]
++ ")"
        sh (SBVApp (SetOp SetComplement) args :: [SV]
args)   = "(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]
++ ")"
        sh (SBVApp (SetOp SetHasSize)    args :: [SV]
args)   = "(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]
++ ")"

        sh (SBVApp (TupleConstructor 0)   [])    = "mkSBVTuple0"
        sh (SBVApp (TupleConstructor n :: Int
n)   args :: [SV]
args)  = "(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
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]
++ ")"
        sh (SBVApp (TupleAccess      i :: Int
i n :: Int
n) [tup :: SV
tup]) = "(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]
++ "_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
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
tup String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

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

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

        sh inp :: SBVExpr
inp@(SBVApp op :: Op
op args :: [SV]
args)
          | Bool
intOp, Just f :: 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 f :: [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 f :: 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 f :: 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 f :: 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 f :: 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 f :: [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 f :: [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 f :: [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
isUninterpreted ([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 [ ""
                                 , "*** Cannot translate operator        : " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Op -> String
forall a. Show a => a -> String
show Op
op
                                 , "*** 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]
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))
                                 , "*** 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
                                 , "***"
                                 , "*** Note that uninterpreted kinds only support equality."
                                 , "*** 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
$ "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   "bvadd")
                                , (Op
Minus,         String -> Bool -> [String] -> String
forall p. String -> p -> [String] -> String
lift2   "bvsub")
                                , (Op
Times,         String -> Bool -> [String] -> String
forall p. String -> p -> [String] -> String
lift2   "bvmul")
                                , (Op
UNeg,          String -> String -> Bool -> [String] -> String
forall p. String -> String -> p -> [String] -> String
lift1B  "not"    "bvneg")
                                , (Op
Abs,           Bool -> [String] -> String
liftAbs)
                                , (Op
Quot,          String -> String -> Bool -> [String] -> String
lift2S  "bvudiv" "bvsdiv")
                                , (Op
Rem,           String -> String -> Bool -> [String] -> String
lift2S  "bvurem" "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  "bvult" "bvslt")
                                , (Op
GreaterThan,   String -> String -> Bool -> [String] -> String
lift2S  "bvugt" "bvsgt")
                                , (Op
LessEq,        String -> String -> Bool -> [String] -> String
lift2S  "bvule" "bvsle")
                                , (Op
GreaterEq,     String -> String -> Bool -> [String] -> String
lift2S  "bvuge" "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 [x :: String
x, y :: String
y] = "(and (not " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                                     blt xs :: [String]
xs     = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "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 [x :: String
x, y :: String
y] = "(or (not " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
                                     blq xs :: [String]
xs     = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "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 [x :: a
x, y :: a
y] = [a
y, a
x]
                                     swp xs :: [a]
xs     = String -> [a]
forall a. HasCallStack => String -> a
error (String -> [a]) -> String -> [a]
forall a b. (a -> b) -> a -> b
$ "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 "/" "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   "div")
                                  , (Op
Rem,         String -> Bool -> [String] -> String
forall p. String -> p -> [String] -> String
lift2   "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 "/" "fp.div")]
                smtIntRealShared :: [(Op, Bool -> [String] -> String)]
smtIntRealShared  = [ (Op
Plus,          String -> String -> Bool -> [String] -> String
forall p. String -> String -> p -> [String] -> String
lift2WM "+" "fp.add")
                                    , (Op
Minus,         String -> String -> Bool -> [String] -> String
forall p. String -> String -> p -> [String] -> String
lift2WM "-" "fp.sub")
                                    , (Op
Times,         String -> String -> Bool -> [String] -> String
forall p. String -> String -> p -> [String] -> String
lift2WM "*" "fp.mul")
                                    , (Op
UNeg,          String -> String -> Bool -> [String] -> String
forall p. String -> String -> p -> [String] -> String
lift1FP "-" "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  "<"  "fp.lt")
                                    , (Op
GreaterThan,   String -> String -> Bool -> [String] -> String
forall p. String -> String -> p -> [String] -> String
lift2Cmp  ">"  "fp.gt")
                                    , (Op
LessEq,        String -> String -> Bool -> [String] -> String
forall p. String -> String -> p -> [String] -> String
lift2Cmp  "<=" "fp.leq")
                                    , (Op
GreaterEq,     String -> String -> Bool -> [String] -> String
forall p. String -> String -> p -> [String] -> String
lift2Cmp  ">=" "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 "="        "="        Bool
True)
                                     , (Op
NotEqual,    String -> String -> Bool -> [String] -> String
liftNS "distinct" "distinct" Bool
True)
                                     , (Op
LessThan,    String -> [String] -> String
unintComp "<")
                                     , (Op
GreaterThan, String -> [String] -> String
unintComp ">")
                                     , (Op
LessEq,      String -> [String] -> String
unintComp "<=")
                                     , (Op
GreaterEq,   String -> [String] -> String
unintComp ">=")
                                     ]
                -- 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  "bvult" (String -> String
forall a. HasCallStack => String -> a
error "smtChar.<: did-not expect signed char here!"))
                               , (Op
GreaterThan,   String -> String -> Bool -> [String] -> String
lift2S  "bvugt" (String -> String
forall a. HasCallStack => String -> a
error "smtChar.>: did-not expect signed char here!"))
                               , (Op
LessEq,        String -> String -> Bool -> [String] -> String
lift2S  "bvule" (String -> String
forall a. HasCallStack => String -> a
error "smtChar.<=: did-not expect signed char here!"))
                               , (Op
GreaterEq,     String -> String -> Bool -> [String] -> String
lift2S  "bvuge" (String -> String
forall a. HasCallStack => String -> a
error "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 "="        "="        Bool
True)
                                 , (Op
NotEqual,    String -> String -> Bool -> [String] -> String
liftNS "distinct" "distinct" Bool
True)
                                 , (Op
LessThan,    Bool -> String -> [String] -> String
stringCmp Bool
False "str.<")
                                 , (Op
GreaterThan, Bool -> String -> [String] -> String
stringCmp Bool
True  "str.<")
                                 , (Op
LessEq,      Bool -> String -> [String] -> String
stringCmp Bool
False "str.<=")
                                 , (Op
GreaterEq,   Bool -> String -> [String] -> String
stringCmp Bool
True  "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 "="        "="        Bool
True)
                               , (Op
NotEqual,    String -> String -> Bool -> [String] -> String
liftNS "distinct" "distinct" Bool
True)
                               , (Op
LessThan,    Bool -> String -> [String] -> String
seqCmp Bool
False "seq.<")
                               , (Op
GreaterThan, Bool -> String -> [String] -> String
seqCmp Bool
True  "seq.<")
                               , (Op
LessEq,      Bool -> String -> [String] -> String
seqCmp Bool
False "seq.<=")
                               , (Op
GreaterEq,   Bool -> String -> [String] -> String
seqCmp Bool
True  "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 kFrom :: Kind
kFrom kTo :: Kind
kTo rm :: String
rm input :: String
input
  | Kind
kFrom Kind -> Kind -> Bool
forall a. Eq a => a -> a -> Bool
== Kind
kTo
  = String
input
  | Bool
True
  = "(" 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]
++ ")"
  where addRM :: String -> String -> String
addRM a :: String
a s :: String
s = String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " 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 KUnbounded         KFloat             a :: String
a = "(_ to_fp 8 24) "  String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " (to_real " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
        cast KUnbounded         KDouble            a :: String
a = "(_ to_fp 11 53) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rm String -> String -> String
forall a. [a] -> [a] -> [a]
++ " (to_real " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
        cast KFloat             KUnbounded         a :: String
a = "to_int (fp.to_real " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
        cast KDouble            KUnbounded         a :: String
a = "to_int (fp.to_real " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

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

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

        -- From float/double
        cast KFloat             (KBounded False m :: Int
m) a :: String
a = String -> String -> String
addRM String
a (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "(_ 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]
++ ")"
        cast KDouble            (KBounded False m :: Int
m) a :: String
a = String -> String -> String
addRM String
a (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "(_ 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]
++ ")"
        cast KFloat             (KBounded True  m :: Int
m) a :: String
a = String -> String -> String
addRM String
a (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "(_ 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]
++ ")"
        cast KDouble            (KBounded True  m :: Int
m) a :: String
a = String -> String -> String
addRM String
a (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "(_ 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]
++ ")"

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

        -- Nothing else should come up:
        cast f :: Kind
f                  d :: Kind
d                  _ = String -> String
forall a. HasCallStack => String -> a
error (String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ "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]
++ " 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 ssv :: SV -> String
ssv o :: String
o c :: Int
c x :: SV
x = "((_ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
o String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " 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
forall a. [a] -> [a] -> [a]
++ SV -> String
ssv SV
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

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

-- Various casts
handleKindCast :: Kind -> Kind -> String -> String
handleKindCast :: Kind -> Kind -> String -> String
handleKindCast kFrom :: Kind
kFrom kTo :: Kind
kTo a :: 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 s :: Bool
s m :: Int
m -> case Kind
kTo of
                        KBounded _ n :: 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
                        KUnbounded   -> Bool -> Int -> String
forall b. (Integral b, Show b) => Bool -> b -> String
b2i Bool
s Int
m
                        _            -> String
tryFPCast

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

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

      _            -> 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 (\k :: 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
$ "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]
++ " 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 upConv :: a -> String
upConv m :: a
m n :: 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
- 1)

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

        signExtend :: a -> String
signExtend i :: a
i = "((_ 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
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
        zeroExtend :: a -> String
zeroExtend i :: a
i = "((_ 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
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
        extract :: a -> String
extract    i :: a
i = "((_ 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]
++ " 0) " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

        -- NB. The following 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.
        --
        -- NB2. (TODO) There is an SMTLib equivalent of this function, called int2bv. However, it
        -- used to be uninterpreted for a long time by Z3; though I think that got fixed. We
        -- might want to simply use that if it's reliably available across the board in solvers.
        i2b :: Int -> String
i2b n :: Int
n = "(let (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
reduced String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") (let (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
defs String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
body String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))"
          where b :: Int -> String
b i :: 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  = "(__a (mod " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
b Int
n String -> String -> String
forall a. [a] -> [a] -> [a]
++ "))"
                mkBit :: Int -> String
mkBit 0  = "(__a0 (ite (= (mod __a 2) 0) #b0 #b1))"
                mkBit i :: Int
i  = "(__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]
++ " (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]
++ ") 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 [0 .. Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- 1])
                body :: String
body     = (String -> String -> String) -> [String] -> String
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\c :: String
c r :: String
r -> "(concat " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
r String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")") ["__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
-1, Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-2 .. 0]]

-- Translation of pseudo-booleans, in case the solver supports them
handlePB :: PBOp -> [String] -> String
handlePB :: PBOp -> [String] -> String
handlePB (PB_AtMost  k :: Int
k) args :: [String]
args = "((_ 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
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
handlePB (PB_AtLeast k :: Int
k) args :: [String]
args = "((_ 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
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
handlePB (PB_Exactly k :: Int
k) args :: [String]
args = "((_ 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) 1)) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ") " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
handlePB (PB_Eq cs :: [Int]
cs   k :: Int
k) args :: [String]
args = "((_ 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
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
handlePB (PB_Le cs :: [Int]
cs   k :: Int
k) args :: [String]
args = "((_ 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
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
handlePB (PB_Ge cs :: [Int]
cs   k :: Int
k) args :: [String]
args = "((_ 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
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"

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

  where addIf :: [Int] -> String
        addIf :: [Int] -> String
addIf cs :: [Int]
cs = "(+ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords ["(ite " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " 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]
++ " 0)" | (a :: String
a, c :: 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]
++ ")"