    -----------------------------------------------------------------------------
    -- |
    -- Module    : Data.SBV.Utils.SExpr
    -- Copyright : (c) Levent Erkok
    -- License   : BSD3
    -- Maintainer: erkokl@gmail.com
    -- Stability : experimental
    --
    -- Parsing of S-expressions (mainly used for parsing SMT-Lib get-value output)
    -----------------------------------------------------------------------------

    {-# LANGUAGE BangPatterns #-}

    {-# OPTIONS_GHC -Wall -Werror #-}

    module Data.SBV.Utils.SExpr (SExpr(..), parenDeficit, parseSExpr, parseSExprFunction) where

    import Data.Bits   (setBit, testBit)
    import Data.Char   (isDigit, ord, isSpace)
    import Data.Either (partitionEithers)
    import Data.List   (isPrefixOf)
    import Data.Maybe  (fromMaybe, listToMaybe)
    import Data.Word   (Word32, Word64)

    import Numeric    (readInt, readDec, readHex, fromRat)

    import Data.SBV.Core.AlgReals
    import Data.SBV.Core.Data (nan, infinity, RoundingMode(..))

    import Data.SBV.Utils.Numeric (fpIsEqualObjectH)

    import Data.Numbers.CrackNum (wordToFloat, wordToDouble)

    -- | ADT S-Expression format, suitable for representing get-model output of SMT-Lib
    data SExpr = ECon    String
               | ENum    (Integer, Maybe Int)  -- Second argument is how wide the field was in bits, if known. Useful in FP parsing.
               | EReal   AlgReal
               | EFloat  Float
               | EDouble Double
               | EApp    [SExpr]
               deriving Int -> SExpr -> ShowS
    [SExpr] -> ShowS
    SExpr -> String
    (Int -> SExpr -> ShowS)
    -> (SExpr -> String) -> ([SExpr] -> ShowS) -> Show SExpr
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [SExpr] -> ShowS
    $cshowList :: [SExpr] -> ShowS
    show :: SExpr -> String
    $cshow :: SExpr -> String
    showsPrec :: Int -> SExpr -> ShowS
    $cshowsPrec :: Int -> SExpr -> ShowS
    Show

    -- | Extremely simple minded tokenizer, good for our use model.
    tokenize :: String -> [String]
    tokenize :: String -> [String]
    tokenize inp :: String
    inp = String -> [String] -> [String]
    go String
    inp []
     where go :: String -> [String] -> [String]
    go "" sofar :: [String]
    sofar = [String] -> [String]
    forall a. [a] -> [a]
    reverse [String]
    sofar

           go (c :: Char
    c:cs :: String
    cs) sofar :: [String]
    sofar
              | Char -> Bool
    isSpace Char
    c = String -> [String] -> [String]
    go ((Char -> Bool) -> ShowS
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile Char -> Bool
    isSpace String
    cs) [String]
    sofar

           go ('(':cs :: String
    cs) sofar :: [String]
    sofar = String -> [String] -> [String]
    go String
    cs ("(" String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    sofar)
           go (')':cs :: String
    cs) sofar :: [String]
    sofar = String -> [String] -> [String]
    go String
    cs (")" String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    sofar)

           go (':':':':cs :: String
    cs) sofar :: [String]
    sofar = String -> [String] -> [String]
    go String
    cs ("::" String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    sofar)

           go (':':cs :: String
    cs) sofar :: [String]
    sofar = case (Char -> Bool) -> String -> (String, String)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    break (Char -> String -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` String
    stopper) String
    cs of
                                (pre :: String
    pre, rest :: String
    rest) -> String -> [String] -> [String]
    go String
    rest ((':'Char -> ShowS
    forall a. a -> [a] -> [a]
    :String
    pre) String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    sofar)

           go ('|':r :: String
    r) sofar :: [String]
    sofar = case (Char -> Bool) -> String -> (String, String)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= '|') String
    r of
                                (pre :: String
    pre, '|':rest :: String
    rest) -> String -> [String] -> [String]
    go String
    rest (String
    pre String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    sofar)
                                (pre :: String
    pre, rest :: String
    rest)     -> String -> [String] -> [String]
    go String
    rest (String
    pre String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    sofar)

           go ('"':r :: String
    r) sofar :: [String]
    sofar = String -> [String] -> [String]
    go String
    rest (String
    finalStr String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    sofar)
               where grabString :: String -> String -> (String, String)
    grabString []             acc :: String
    acc = (ShowS
    forall a. [a] -> [a]
    reverse String
    acc, [])         -- Strictly speaking, this is the unterminated string case; but let's ignore
                     grabString ('"' :'"':cs :: String
    cs)  acc :: String
    acc = String -> String -> (String, String)
    grabString String
    cs ('"' Char -> ShowS
    forall a. a -> [a] -> [a]
    :String
    acc)
                     grabString ('"':cs :: String
    cs)       acc :: String
    acc = (ShowS
    forall a. [a] -> [a]
    reverse String
    acc, String
    cs)
                     grabString (c :: Char
    c:cs :: String
    cs)         acc :: String
    acc = String -> String -> (String, String)
    grabString String
    cs (Char
    cChar -> ShowS
    forall a. a -> [a] -> [a]
    :String
    acc)

                     (str :: String
    str, rest :: String
    rest) = String -> String -> (String, String)
    grabString String
    r []
                     finalStr :: String
    finalStr    = '"' Char -> ShowS
    forall a. a -> [a] -> [a]
    : String
    str String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "\""

           go cs :: String
    cs sofar :: [String]
    sofar = case (Char -> Bool) -> String -> (String, String)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    span (Char -> String -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` String
    stopper) String
    cs of
                           (pre :: String
    pre, post :: String
    post) -> String -> [String] -> [String]
    go String
    post (String
    pre String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : [String]
    sofar)

           -- characters that can stop the current token
           -- it is *crucial* that this list contains every character
           -- we can match in one of the previous cases!
           stopper :: String
    stopper = " \t\n():|\""

    -- | The balance of parens in this string. If 0, this means it's a legit line!
    parenDeficit :: String -> Int
    parenDeficit :: String -> Int
    parenDeficit = Int -> [String] -> Int
    go 0 ([String] -> Int) -> (String -> [String]) -> String -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> [String]
    tokenize
      where go :: Int -> [String] -> Int
            go :: Int -> [String] -> Int
    go !Int
    balance []           = Int
    balance
            go !Int
    balance ("(" : rest :: [String]
    rest) = Int -> [String] -> Int
    go (Int
    balanceInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +1) [String]
    rest
            go !Int
    balance (")" : rest :: [String]
    rest) = Int -> [String] -> Int
    go (Int
    balanceInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -1) [String]
    rest
            go !Int
    balance (_   : rest :: [String]
    rest) = Int -> [String] -> Int
    go Int
    balance     [String]
    rest

    -- | Parse a string into an SExpr, potentially failing with an error message
    parseSExpr :: String -> Either String SExpr
    parseSExpr :: String -> Either String SExpr
    parseSExpr inp :: String
    inp = do (sexp :: SExpr
    sexp, extras :: [String]
    extras) <- [String] -> Either String (SExpr, [String])
    parse [String]
    inpToks
                        if [String] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [String]
    extras
                           then case SExpr
    sexp of
                                  EApp [ECon "error", ECon er :: String
    er] -> String -> Either String SExpr
    forall a b. a -> Either a b
    Left (String -> Either String SExpr) -> String -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ "Solver returned an error: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    er
                                  _                            -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return SExpr
    sexp

                           else String -> Either String SExpr
    forall b. String -> Either String b
    die "Extra tokens after valid input"
      where inpToks :: [String]
    inpToks = String -> [String]
    tokenize String
    inp

            die :: String -> Either String b
    die w :: String
    w = String -> Either String b
    forall a b. a -> Either a b
    Left (String -> Either String b) -> String -> Either String b
    forall a b. (a -> b) -> a -> b
    $  "SBV.Provers.SExpr: Failed to parse S-Expr: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    w
                         String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ "\n*** Input : <" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    inp String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ">"

            parse :: [String] -> Either String (SExpr, [String])
    parse []         = String -> Either String (SExpr, [String])
    forall b. String -> Either String b
    die "ran out of tokens"
            parse ("(":toks :: [String]
    toks) = do (f :: [SExpr]
    f, r :: [String]
    r) <- [String] -> [SExpr] -> Either String ([SExpr], [String])
    parseApp [String]
    toks []
                                  SExpr
    f' <- SExpr -> Either String SExpr
    cvt ([SExpr] -> SExpr
    EApp [SExpr]
    f)
                                  (SExpr, [String]) -> Either String (SExpr, [String])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr
    f', [String]
    r)
            parse (")":_)    = String -> Either String (SExpr, [String])
    forall b. String -> Either String b
    die "extra tokens after close paren"
            parse [tok :: String
    tok]      = do SExpr
    t <- String -> Either String SExpr
    pTok String
    tok
                                  (SExpr, [String]) -> Either String (SExpr, [String])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr
    t, [])
            parse _          = String -> Either String (SExpr, [String])
    forall b. String -> Either String b
    die "ill-formed s-expr"

            parseApp :: [String] -> [SExpr] -> Either String ([SExpr], [String])
    parseApp []         _     = String -> Either String ([SExpr], [String])
    forall b. String -> Either String b
    die "failed to grab s-expr application"
            parseApp (")":toks :: [String]
    toks) sofar :: [SExpr]
    sofar = ([SExpr], [String]) -> Either String ([SExpr], [String])
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([SExpr] -> [SExpr]
    forall a. [a] -> [a]
    reverse [SExpr]
    sofar, [String]
    toks)
            parseApp ("(":toks :: [String]
    toks) sofar :: [SExpr]
    sofar = do (f :: SExpr
    f, r :: [String]
    r) <- [String] -> Either String (SExpr, [String])
    parse ("("String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    :[String]
    toks)
                                           [String] -> [SExpr] -> Either String ([SExpr], [String])
    parseApp [String]
    r (SExpr
    f SExpr -> [SExpr] -> [SExpr]
    forall a. a -> [a] -> [a]
    : [SExpr]
    sofar)
            parseApp (tok :: String
    tok:toks :: [String]
    toks) sofar :: [SExpr]
    sofar = do SExpr
    t <- String -> Either String SExpr
    pTok String
    tok
                                           [String] -> [SExpr] -> Either String ([SExpr], [String])
    parseApp [String]
    toks (SExpr
    t SExpr -> [SExpr] -> [SExpr]
    forall a. a -> [a] -> [a]
    : [SExpr]
    sofar)

            pTok :: String -> Either String SExpr
    pTok "false" = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ (Integer, Maybe Int) -> SExpr
    ENum (0, Maybe Int
    forall a. Maybe a
    Nothing)
            pTok "true"  = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ (Integer, Maybe Int) -> SExpr
    ENum (1, Maybe Int
    forall a. Maybe a
    Nothing)

            pTok ('0':'b':r :: String
    r)                                 = Maybe Int -> [(Integer, String)] -> Either String SExpr
    mkNum (Int -> Maybe Int
    forall a. a -> Maybe a
    Just (String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    r))     ([(Integer, String)] -> Either String SExpr)
    -> [(Integer, String)] -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Integer -> (Char -> Bool) -> (Char -> Int) -> ReadS Integer
    forall a. Num a => a -> (Char -> Bool) -> (Char -> Int) -> ReadS a
    readInt 2 (Char -> String -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` "01") (\c :: Char
    c -> Char -> Int
    ord Char
    c Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Char -> Int
    ord '0') String
    r
            pTok ('b':'v':r :: String
    r) | Bool -> Bool
    not (String -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    r) Bool -> Bool -> Bool
    && (Char -> Bool) -> String -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Char -> Bool
    isDigit String
    r = Maybe Int -> [(Integer, String)] -> Either String SExpr
    mkNum Maybe Int
    forall a. Maybe a
    Nothing               ([(Integer, String)] -> Either String SExpr)
    -> [(Integer, String)] -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ ReadS Integer
    forall a. (Eq a, Num a) => ReadS a
    readDec ((Char -> Bool) -> ShowS
    forall a. (a -> Bool) -> [a] -> [a]
    takeWhile (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    /= '[') String
    r)
            pTok ('#':'b':r :: String
    r)                                 = Maybe Int -> [(Integer, String)] -> Either String SExpr
    mkNum (Int -> Maybe Int
    forall a. a -> Maybe a
    Just (String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    r))     ([(Integer, String)] -> Either String SExpr)
    -> [(Integer, String)] -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Integer -> (Char -> Bool) -> (Char -> Int) -> ReadS Integer
    forall a. Num a => a -> (Char -> Bool) -> (Char -> Int) -> ReadS a
    readInt 2 (Char -> String -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` "01") (\c :: Char
    c -> Char -> Int
    ord Char
    c Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Char -> Int
    ord '0') String
    r
            pTok ('#':'x':r :: String
    r)                                 = Maybe Int -> [(Integer, String)] -> Either String SExpr
    mkNum (Int -> Maybe Int
    forall a. a -> Maybe a
    Just (4 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    * String -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length String
    r)) ([(Integer, String)] -> Either String SExpr)
    -> [(Integer, String)] -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ ReadS Integer
    forall a. (Eq a, Num a) => ReadS a
    readHex String
    r

            pTok n :: String
    n
              | Bool -> Bool
    not (String -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null String
    n) Bool -> Bool -> Bool
    && Char -> Bool
    isDigit (String -> Char
    forall a. [a] -> a
    head String
    n)
              = if '.' Char -> String -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` String
    n then String -> Either String SExpr
    forall (m :: * -> *). Monad m => String -> m SExpr
    getReal String
    n
                else Maybe Int -> [(Integer, String)] -> Either String SExpr
    mkNum Maybe Int
    forall a. Maybe a
    Nothing ([(Integer, String)] -> Either String SExpr)
    -> [(Integer, String)] -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ ReadS Integer
    forall a. (Eq a, Num a) => ReadS a
    readDec String
    n
            pTok n :: String
    n                 = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ String -> SExpr
    ECon (ShowS
    constantMap String
    n)

            mkNum :: Maybe Int -> [(Integer, String)] -> Either String SExpr
    mkNum l :: Maybe Int
    l [(n :: Integer
    n, "")] = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ (Integer, Maybe Int) -> SExpr
    ENum (Integer
    n, Maybe Int
    l)
            mkNum _ _         = String -> Either String SExpr
    forall b. String -> Either String b
    die "cannot read number"

            getReal :: String -> m SExpr
    getReal n :: String
    n = SExpr -> m SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> m SExpr) -> SExpr -> m SExpr
    forall a b. (a -> b) -> a -> b
    $ AlgReal -> SExpr
    EReal (AlgReal -> SExpr) -> AlgReal -> SExpr
    forall a b. (a -> b) -> a -> b
    $ Either (Bool, String) (Integer, [(Integer, Integer)]) -> AlgReal
    mkPolyReal ((Bool, String)
    -> Either (Bool, String) (Integer, [(Integer, Integer)])
    forall a b. a -> Either a b
    Left (Bool
    exact, String
    n'))
              where exact :: Bool
    exact = Bool -> Bool
    not ("?" String -> String -> Bool
    forall a. Eq a => [a] -> [a] -> Bool
    `isPrefixOf` ShowS
    forall a. [a] -> [a]
    reverse String
    n)
                    n' :: String
    n' | Bool
    exact = String
    n
                       | Bool
    True  = ShowS
    forall a. [a] -> [a]
    init String
    n

            -- simplify numbers and root-obj values
            cvt :: SExpr -> Either String SExpr
    cvt (EApp [ECon "to_int",  EReal a :: AlgReal
    a])                       = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ AlgReal -> SExpr
    EReal AlgReal
    a   -- ignore the "casting"
            cvt (EApp [ECon "to_real", EReal a :: AlgReal
    a])                       = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ AlgReal -> SExpr
    EReal AlgReal
    a   -- ignore the "casting"
            cvt (EApp [ECon "/", EReal a :: AlgReal
    a, EReal b :: AlgReal
    b])                    = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ AlgReal -> SExpr
    EReal (AlgReal
    a AlgReal -> AlgReal -> AlgReal
    forall a. Fractional a => a -> a -> a
    / AlgReal
    b)
            cvt (EApp [ECon "/", EReal a :: AlgReal
    a, ENum  b :: (Integer, Maybe Int)
    b])                    = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ AlgReal -> SExpr
    EReal (AlgReal
    a                   AlgReal -> AlgReal -> AlgReal
    forall a. Fractional a => a -> a -> a
    / Integer -> AlgReal
    forall a. Num a => Integer -> a
    fromInteger ((Integer, Maybe Int) -> Integer
    forall a b. (a, b) -> a
    fst (Integer, Maybe Int)
    b))
            cvt (EApp [ECon "/", ENum  a :: (Integer, Maybe Int)
    a, EReal b :: AlgReal
    b])                    = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ AlgReal -> SExpr
    EReal (Integer -> AlgReal
    forall a. Num a => Integer -> a
    fromInteger ((Integer, Maybe Int) -> Integer
    forall a b. (a, b) -> a
    fst (Integer, Maybe Int)
    a) AlgReal -> AlgReal -> AlgReal
    forall a. Fractional a => a -> a -> a
    /             AlgReal
    b      )
            cvt (EApp [ECon "/", ENum  a :: (Integer, Maybe Int)
    a, ENum  b :: (Integer, Maybe Int)
    b])                    = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ AlgReal -> SExpr
    EReal (Integer -> AlgReal
    forall a. Num a => Integer -> a
    fromInteger ((Integer, Maybe Int) -> Integer
    forall a b. (a, b) -> a
    fst (Integer, Maybe Int)
    a) AlgReal -> AlgReal -> AlgReal
    forall a. Fractional a => a -> a -> a
    / Integer -> AlgReal
    forall a. Num a => Integer -> a
    fromInteger ((Integer, Maybe Int) -> Integer
    forall a b. (a, b) -> a
    fst (Integer, Maybe Int)
    b))
            cvt (EApp [ECon "-", EReal a :: AlgReal
    a])                             = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ AlgReal -> SExpr
    EReal (-AlgReal
    a)
            cvt (EApp [ECon "-", ENum a :: (Integer, Maybe Int)
    a])                              = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ (Integer, Maybe Int) -> SExpr
    ENum  (-((Integer, Maybe Int) -> Integer
    forall a b. (a, b) -> a
    fst (Integer, Maybe Int)
    a), (Integer, Maybe Int) -> Maybe Int
    forall a b. (a, b) -> b
    snd (Integer, Maybe Int)
    a)

            -- bit-vector value as CVC4 prints: (_ bv0 16) for instance
            cvt (EApp [ECon "_", ENum a :: (Integer, Maybe Int)
    a, ENum _b :: (Integer, Maybe Int)
    _b])                     = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ (Integer, Maybe Int) -> SExpr
    ENum (Integer, Maybe Int)
    a
            cvt (EApp [ECon "root-obj", EApp (ECon "+":trms :: [SExpr]
    trms), ENum k :: (Integer, Maybe Int)
    k]) = do [(Integer, Integer)]
    ts <- (SExpr -> Either String (Integer, Integer))
    -> [SExpr] -> Either String [(Integer, Integer)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM SExpr -> Either String (Integer, Integer)
    getCoeff [SExpr]
    trms
                                                                            SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ AlgReal -> SExpr
    EReal (AlgReal -> SExpr) -> AlgReal -> SExpr
    forall a b. (a -> b) -> a -> b
    $ Either (Bool, String) (Integer, [(Integer, Integer)]) -> AlgReal
    mkPolyReal ((Integer, [(Integer, Integer)])
    -> Either (Bool, String) (Integer, [(Integer, Integer)])
    forall a b. b -> Either a b
    Right ((Integer, Maybe Int) -> Integer
    forall a b. (a, b) -> a
    fst (Integer, Maybe Int)
    k, [(Integer, Integer)]
    ts))
            cvt (EApp [ECon "as", n :: SExpr
    n, EApp [ECon "_", ECon "FloatingPoint", ENum (11, _), ENum (53, _)]]) = SExpr -> Either String SExpr
    getDouble SExpr
    n
            cvt (EApp [ECon "as", n :: SExpr
    n, EApp [ECon "_", ECon "FloatingPoint", ENum ( 8, _), ENum (24, _)]]) = SExpr -> Either String SExpr
    getFloat  SExpr
    n
            cvt (EApp [ECon "as", n :: SExpr
    n, ECon "Float64"])                                                    = SExpr -> Either String SExpr
    getDouble SExpr
    n
            cvt (EApp [ECon "as", n :: SExpr
    n, ECon "Float32"])                                                    = SExpr -> Either String SExpr
    getFloat  SExpr
    n

            -- Deal with CVC4's approximate reals
            cvt x :: SExpr
    x@(EApp [ECon "witness", EApp [EApp [ECon v :: String
    v, ECon "Real"]]
                                       , EApp [ECon "or", EApp [ECon "=", ECon v' :: String
    v', val :: SExpr
    val], _]]) | String
    v String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    v'   = do
                                                    SExpr
    approx <- SExpr -> Either String SExpr
    cvt SExpr
    val
                                                    case SExpr
    approx of
                                                      ENum (s :: Integer
    s, _) -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ AlgReal -> SExpr
    EReal (AlgReal -> SExpr) -> AlgReal -> SExpr
    forall a b. (a -> b) -> a -> b
    $ Either (Bool, String) (Integer, [(Integer, Integer)]) -> AlgReal
    mkPolyReal ((Bool, String)
    -> Either (Bool, String) (Integer, [(Integer, Integer)])
    forall a b. a -> Either a b
    Left (Bool
    False, Integer -> String
    forall a. Show a => a -> String
    show Integer
    s))
                                                      EReal aval :: AlgReal
    aval  -> case AlgReal
    aval of
                                                                       AlgRational _ r :: Rational
    r -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ AlgReal -> SExpr
    EReal (AlgReal -> SExpr) -> AlgReal -> SExpr
    forall a b. (a -> b) -> a -> b
    $ Bool -> Rational -> AlgReal
    AlgRational Bool
    False Rational
    r
                                                                       _               -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ AlgReal -> SExpr
    EReal AlgReal
    aval
                                                      _           -> String -> Either String SExpr
    forall b. String -> Either String b
    die (String -> Either String SExpr) -> String -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ "Cannot parse a CVC4 approximate value from: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    x

            -- NB. Note the lengths on the mantissa for the following two are 23/52; not 24/53!
            cvt (EApp [ECon "fp",    ENum (s :: Integer
    s, Just 1), ENum ( e :: Integer
    e, Just 8),  ENum (m :: Integer
    m, Just 23)])           = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Float -> SExpr
    EFloat  (Float -> SExpr) -> Float -> SExpr
    forall a b. (a -> b) -> a -> b
    $ Integer -> Integer -> Integer -> Float
    getTripleFloat  Integer
    s Integer
    e Integer
    m
            cvt (EApp [ECon "fp",    ENum (s :: Integer
    s, Just 1), ENum ( e :: Integer
    e, Just 11), ENum (m :: Integer
    m, Just 52)])           = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Double -> SExpr
    EDouble (Double -> SExpr) -> Double -> SExpr
    forall a b. (a -> b) -> a -> b
    $ Integer -> Integer -> Integer -> Double
    getTripleDouble Integer
    s Integer
    e Integer
    m
            cvt (EApp [ECon "_",     ECon "NaN",       ENum ( 8, _),       ENum (24,      _)])           = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Float -> SExpr
    EFloat  Float
    forall a. Floating a => a
    nan
            cvt (EApp [ECon "_",     ECon "NaN",       ENum (11, _),       ENum (53,      _)])           = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Double -> SExpr
    EDouble Double
    forall a. Floating a => a
    nan
            cvt (EApp [ECon "_",     ECon "+oo",       ENum ( 8, _),       ENum (24,      _)])           = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Float -> SExpr
    EFloat  Float
    forall a. Floating a => a
    infinity
            cvt (EApp [ECon "_",     ECon "+oo",       ENum (11, _),       ENum (53,      _)])           = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Double -> SExpr
    EDouble Double
    forall a. Floating a => a
    infinity
            cvt (EApp [ECon "_",     ECon "-oo",       ENum ( 8, _),       ENum (24,      _)])           = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Float -> SExpr
    EFloat  (-Float
    forall a. Floating a => a
    infinity)
            cvt (EApp [ECon "_",     ECon "-oo",       ENum (11, _),       ENum (53,      _)])           = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Double -> SExpr
    EDouble (-Double
    forall a. Floating a => a
    infinity)
            cvt (EApp [ECon "_",     ECon "+zero",     ENum ( 8, _),       ENum (24,      _)])           = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Float -> SExpr
    EFloat  0
            cvt (EApp [ECon "_",     ECon "+zero",     ENum (11, _),       ENum (53,      _)])           = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Double -> SExpr
    EDouble 0
            cvt (EApp [ECon "_",     ECon "-zero",     ENum ( 8, _),       ENum (24,      _)])           = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Float -> SExpr
    EFloat  (-0)
            cvt (EApp [ECon "_",     ECon "-zero",     ENum (11, _),       ENum (53,      _)])           = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Double -> SExpr
    EDouble (-0)
            cvt x :: SExpr
    x                                                                                        = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return SExpr
    x

            getCoeff :: SExpr -> Either String (Integer, Integer)
    getCoeff (EApp [ECon "*", ENum k :: (Integer, Maybe Int)
    k, EApp [ECon "^", ECon "x", ENum p :: (Integer, Maybe Int)
    p]]) = (Integer, Integer) -> Either String (Integer, Integer)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Integer, Maybe Int) -> Integer
    forall a b. (a, b) -> a
    fst (Integer, Maybe Int)
    k, (Integer, Maybe Int) -> Integer
    forall a b. (a, b) -> a
    fst (Integer, Maybe Int)
    p)  -- kx^p
            getCoeff (EApp [ECon "*", ENum k :: (Integer, Maybe Int)
    k,                 ECon "x"        ] ) = (Integer, Integer) -> Either String (Integer, Integer)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Integer, Maybe Int) -> Integer
    forall a b. (a, b) -> a
    fst (Integer, Maybe Int)
    k,     1)  -- kx
            getCoeff (                        EApp [ECon "^", ECon "x", ENum p :: (Integer, Maybe Int)
    p] ) = (Integer, Integer) -> Either String (Integer, Integer)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (    1, (Integer, Maybe Int) -> Integer
    forall a b. (a, b) -> a
    fst (Integer, Maybe Int)
    p)  --  x^p
            getCoeff (                                        ECon "x"          ) = (Integer, Integer) -> Either String (Integer, Integer)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (    1,     1)  --  x
            getCoeff (                ENum k :: (Integer, Maybe Int)
    k                                    ) = (Integer, Integer) -> Either String (Integer, Integer)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Integer, Maybe Int) -> Integer
    forall a b. (a, b) -> a
    fst (Integer, Maybe Int)
    k,     0)  -- k
            getCoeff x :: SExpr
    x = String -> Either String (Integer, Integer)
    forall b. String -> Either String b
    die (String -> Either String (Integer, Integer))
    -> String -> Either String (Integer, Integer)
    forall a b. (a -> b) -> a -> b
    $ "Cannot parse a root-obj,\nProcessing term: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    x
            getDouble :: SExpr -> Either String SExpr
    getDouble (ECon s :: String
    s)  = case (String
    s, String -> Maybe Double
    forall a. (Read a, RealFloat a) => String -> Maybe a
    rdFP ((Char -> Bool) -> ShowS
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == '+') String
    s)) of
                                    ("plusInfinity",  _     ) -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Double -> SExpr
    EDouble Double
    forall a. Floating a => a
    infinity
                                    ("minusInfinity", _     ) -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Double -> SExpr
    EDouble (-Double
    forall a. Floating a => a
    infinity)
                                    ("oo",            _     ) -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Double -> SExpr
    EDouble Double
    forall a. Floating a => a
    infinity
                                    ("-oo",           _     ) -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Double -> SExpr
    EDouble (-Double
    forall a. Floating a => a
    infinity)
                                    ("zero",          _     ) -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Double -> SExpr
    EDouble 0
                                    ("-zero",         _     ) -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Double -> SExpr
    EDouble (-0)
                                    ("NaN",           _     ) -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Double -> SExpr
    EDouble Double
    forall a. Floating a => a
    nan
                                    (_,               Just v :: Double
    v) -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Double -> SExpr
    EDouble Double
    v
                                    _               -> String -> Either String SExpr
    forall b. String -> Either String b
    die (String -> Either String SExpr) -> String -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ "Cannot parse a double value from: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    s
            getDouble (EApp [_, s :: SExpr
    s, _, _]) = SExpr -> Either String SExpr
    getDouble SExpr
    s
            getDouble (EReal r :: AlgReal
    r) = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Double -> SExpr
    EDouble (Double -> SExpr) -> Double -> SExpr
    forall a b. (a -> b) -> a -> b
    $ Rational -> Double
    forall a. RealFloat a => Rational -> a
    fromRat (Rational -> Double) -> Rational -> Double
    forall a b. (a -> b) -> a -> b
    $ AlgReal -> Rational
    forall a. Real a => a -> Rational
    toRational AlgReal
    r
            getDouble x :: SExpr
    x         = String -> Either String SExpr
    forall b. String -> Either String b
    die (String -> Either String SExpr) -> String -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ "Cannot parse a double value from: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    x
            getFloat :: SExpr -> Either String SExpr
    getFloat (ECon s :: String
    s)   = case (String
    s, String -> Maybe Float
    forall a. (Read a, RealFloat a) => String -> Maybe a
    rdFP ((Char -> Bool) -> ShowS
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == '+') String
    s)) of
                                    ("plusInfinity",  _     ) -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Float -> SExpr
    EFloat Float
    forall a. Floating a => a
    infinity
                                    ("minusInfinity", _     ) -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Float -> SExpr
    EFloat (-Float
    forall a. Floating a => a
    infinity)
                                    ("oo",            _     ) -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Float -> SExpr
    EFloat Float
    forall a. Floating a => a
    infinity
                                    ("-oo",           _     ) -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Float -> SExpr
    EFloat (-Float
    forall a. Floating a => a
    infinity)
                                    ("zero",          _     ) -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Float -> SExpr
    EFloat 0
                                    ("-zero",         _     ) -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Float -> SExpr
    EFloat (-0)
                                    ("NaN",           _     ) -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Float -> SExpr
    EFloat Float
    forall a. Floating a => a
    nan
                                    (_,               Just v :: Float
    v) -> SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Float -> SExpr
    EFloat Float
    v
                                    _               -> String -> Either String SExpr
    forall b. String -> Either String b
    die (String -> Either String SExpr) -> String -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ "Cannot parse a float value from: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    s
            getFloat (EReal r :: AlgReal
    r)  = SExpr -> Either String SExpr
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SExpr -> Either String SExpr) -> SExpr -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ Float -> SExpr
    EFloat (Float -> SExpr) -> Float -> SExpr
    forall a b. (a -> b) -> a -> b
    $ Rational -> Float
    forall a. RealFloat a => Rational -> a
    fromRat (Rational -> Float) -> Rational -> Float
    forall a b. (a -> b) -> a -> b
    $ AlgReal -> Rational
    forall a. Real a => a -> Rational
    toRational AlgReal
    r
            getFloat (EApp [_, s :: SExpr
    s, _, _]) = SExpr -> Either String SExpr
    getFloat SExpr
    s
            getFloat x :: SExpr
    x          = String -> Either String SExpr
    forall b. String -> Either String b
    die (String -> Either String SExpr) -> String -> Either String SExpr
    forall a b. (a -> b) -> a -> b
    $ "Cannot parse a float value from: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SExpr -> String
    forall a. Show a => a -> String
    show SExpr
    x

    -- | Parses the Z3 floating point formatted numbers like so: 1.321p5/1.2123e9 etc.
    rdFP :: (Read a, RealFloat a) => String -> Maybe a
    rdFP :: String -> Maybe a
    rdFP s :: String
    s = case (Char -> Bool) -> String -> (String, String)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    break (Char -> String -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` "pe") String
    s of
               (m :: String
    m, 'p':e :: String
    e) -> String -> Maybe a
    forall a. Read a => String -> Maybe a
    rd String
    m Maybe a -> (a -> Maybe a) -> Maybe a
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \m' :: a
    m' -> String -> Maybe a
    forall a. Read a => String -> Maybe a
    rd String
    e Maybe a -> (a -> Maybe a) -> Maybe a
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \e' :: a
    e' -> a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> Maybe a) -> a -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ a
    m' a -> a -> a
    forall a. Num a => a -> a -> a
    * ( 2 a -> a -> a
    forall a. Floating a => a -> a -> a
    ** a
    e')
               (m :: String
    m, 'e':e :: String
    e) -> String -> Maybe a
    forall a. Read a => String -> Maybe a
    rd String
    m Maybe a -> (a -> Maybe a) -> Maybe a
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \m' :: a
    m' -> String -> Maybe a
    forall a. Read a => String -> Maybe a
    rd String
    e Maybe a -> (a -> Maybe a) -> Maybe a
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \e' :: a
    e' -> a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (a -> Maybe a) -> a -> Maybe a
    forall a b. (a -> b) -> a -> b
    $ a
    m' a -> a -> a
    forall a. Num a => a -> a -> a
    * (10 a -> a -> a
    forall a. Floating a => a -> a -> a
    ** a
    e')
               (m :: String
    m, "")    -> String -> Maybe a
    forall a. Read a => String -> Maybe a
    rd String
    m
               _          -> Maybe a
    forall a. Maybe a
    Nothing
     where rd :: String -> Maybe a
    rd v :: String
    v = case ReadS a
    forall a. Read a => ReadS a
    reads String
    v of
                    [(n :: a
    n, "")] -> a -> Maybe a
    forall a. a -> Maybe a
    Just a
    n
                    _         -> Maybe a
    forall a. Maybe a
    Nothing

    -- | Convert an (s, e, m) triple to a float value
    getTripleFloat :: Integer -> Integer -> Integer -> Float
    getTripleFloat :: Integer -> Integer -> Integer -> Float
    getTripleFloat s :: Integer
    s e :: Integer
    e m :: Integer
    m = Word32 -> Float
    wordToFloat Word32
    w32
      where sign :: [Bool]
    sign      = [Integer
    s Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == 1]
            expt :: [Bool]
    expt      = [Integer
    e Integer -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    `testBit` Int
    i | Int
    i <- [ 7,  6 .. 0]]
            mantissa :: [Bool]
    mantissa  = [Integer
    m Integer -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    `testBit` Int
    i | Int
    i <- [22, 21 .. 0]]
            positions :: [Int]
    positions = [Int
    i | (i :: Int
    i, b :: Bool
    b) <- [Int] -> [Bool] -> [(Int, Bool)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [31, 30 .. 0] ([Bool]
    sign [Bool] -> [Bool] -> [Bool]
    forall a. [a] -> [a] -> [a]
    ++ [Bool]
    expt [Bool] -> [Bool] -> [Bool]
    forall a. [a] -> [a] -> [a]
    ++ [Bool]
    mantissa), Bool
    b]
            w32 :: Word32
    w32       = (Int -> Word32 -> Word32) -> Word32 -> [Int] -> Word32
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ((Word32 -> Int -> Word32) -> Int -> Word32 -> Word32
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Word32 -> Int -> Word32
    forall a. Bits a => a -> Int -> a
    setBit) (0::Word32) [Int]
    positions

    -- | Convert an (s, e, m) triple to a float value
    getTripleDouble :: Integer -> Integer -> Integer -> Double
    getTripleDouble :: Integer -> Integer -> Integer -> Double
    getTripleDouble s :: Integer
    s e :: Integer
    e m :: Integer
    m = Word64 -> Double
    wordToDouble Word64
    w64
      where sign :: [Bool]
    sign      = [Integer
    s Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == 1]
            expt :: [Bool]
    expt      = [Integer
    e Integer -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    `testBit` Int
    i | Int
    i <- [10,  9 .. 0]]
            mantissa :: [Bool]
    mantissa  = [Integer
    m Integer -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    `testBit` Int
    i | Int
    i <- [51, 50 .. 0]]
            positions :: [Int]
    positions = [Int
    i | (i :: Int
    i, b :: Bool
    b) <- [Int] -> [Bool] -> [(Int, Bool)]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [63, 62 .. 0] ([Bool]
    sign [Bool] -> [Bool] -> [Bool]
    forall a. [a] -> [a] -> [a]
    ++ [Bool]
    expt [Bool] -> [Bool] -> [Bool]
    forall a. [a] -> [a] -> [a]
    ++ [Bool]
    mantissa), Bool
    b]
            w64 :: Word64
    w64       = (Int -> Word64 -> Word64) -> Word64 -> [Int] -> Word64
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr ((Word64 -> Int -> Word64) -> Int -> Word64 -> Word64
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Word64 -> Int -> Word64
    forall a. Bits a => a -> Int -> a
    setBit) (0::Word64) [Int]
    positions

    -- | Special constants of SMTLib2 and their internal translation. Mainly
    -- rounding modes for now.
    constantMap :: String -> String
    constantMap :: ShowS
    constantMap n :: String
    n = String -> Maybe String -> String
    forall a. a -> Maybe a -> a
    fromMaybe String
    n ([String] -> Maybe String
    forall a. [a] -> Maybe a
    listToMaybe [String
    to | (from :: [String]
    from, to :: String
    to) <- [([String], String)]
    special, String
    n String -> [String] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String]
    from])
     where special :: [([String], String)]
    special = [ (["RNE", "roundNearestTiesToEven"], RoundingMode -> String
    forall a. Show a => a -> String
    show RoundingMode
    RoundNearestTiesToEven)
                     , (["RNA", "roundNearestTiesToAway"], RoundingMode -> String
    forall a. Show a => a -> String
    show RoundingMode
    RoundNearestTiesToAway)
                     , (["RTP", "roundTowardPositive"],    RoundingMode -> String
    forall a. Show a => a -> String
    show RoundingMode
    RoundTowardPositive)
                     , (["RTN", "roundTowardNegative"],    RoundingMode -> String
    forall a. Show a => a -> String
    show RoundingMode
    RoundTowardNegative)
                     , (["RTZ", "roundTowardZero"],        RoundingMode -> String
    forall a. Show a => a -> String
    show RoundingMode
    RoundTowardZero)
                     ]

    -- | Parse a function like value. These come in two flavors: Either in the form of
    -- a store-expression or a lambda-expression. So we handle both here.
    parseSExprFunction :: SExpr -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
    parseSExprFunction :: SExpr -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
    parseSExprFunction e :: SExpr
    e
      | Just r :: ([([SExpr], SExpr)], SExpr)
    r <- SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
    parseLambdaExpression  SExpr
    e = Either String ([([SExpr], SExpr)], SExpr)
    -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
    forall a. a -> Maybe a
    Just (([([SExpr], SExpr)], SExpr)
    -> Either String ([([SExpr], SExpr)], SExpr)
    forall a b. b -> Either a b
    Right ([([SExpr], SExpr)], SExpr)
    r)
      | Just r :: Either String ([([SExpr], SExpr)], SExpr)
    r <- SExpr -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
    parseStoreAssociations SExpr
    e = Either String ([([SExpr], SExpr)], SExpr)
    -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
    forall a. a -> Maybe a
    Just Either String ([([SExpr], SExpr)], SExpr)
    r
      | Bool
    True                               = Maybe (Either String ([([SExpr], SExpr)], SExpr))
    forall a. Maybe a
    Nothing         -- out-of luck. NB. This is where we would add support for other solvers!

    -- | Parse a lambda expression, most likely z3 specific. There's some guess work
    -- involved here regarding how z3 produces lambda-expressions; while we try to
    -- be flexible, this is certainly not a full fledged parser. But hopefully it'll
    -- cover everything z3 will throw at it.
    parseLambdaExpression :: SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
    parseLambdaExpression :: SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
    parseLambdaExpression funExpr :: SExpr
    funExpr = case SExpr
    funExpr of
                                      EApp [ECon "lambda", EApp params :: [SExpr]
    params, body :: SExpr
    body] -> (SExpr -> Maybe String) -> [SExpr] -> Maybe [String]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM SExpr -> Maybe String
    getParam [SExpr]
    params Maybe [String]
    -> ([String] -> Maybe [Either ([SExpr], SExpr) SExpr])
    -> Maybe [Either ([SExpr], SExpr) SExpr]
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= ([String] -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr])
    -> SExpr -> [String] -> Maybe [Either ([SExpr], SExpr) SExpr]
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip [String] -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
    lambda SExpr
    body Maybe [Either ([SExpr], SExpr) SExpr]
    -> ([Either ([SExpr], SExpr) SExpr]
        -> Maybe ([([SExpr], SExpr)], SExpr))
    -> Maybe ([([SExpr], SExpr)], SExpr)
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= [Either ([SExpr], SExpr) SExpr]
    -> Maybe ([([SExpr], SExpr)], SExpr)
    chainAssigns
                                      _                                       -> Maybe ([([SExpr], SExpr)], SExpr)
    forall a. Maybe a
    Nothing
      where getParam :: SExpr -> Maybe String
    getParam (EApp [ECon v :: String
    v, _]) = String -> Maybe String
    forall a. a -> Maybe a
    Just String
    v
            getParam _                  = Maybe String
    forall a. Maybe a
    Nothing

            lambda :: [String] -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
            lambda :: [String] -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
    lambda params :: [String]
    params body :: SExpr
    body = [Either ([SExpr], SExpr) SExpr] -> [Either ([SExpr], SExpr) SExpr]
    forall a. [a] -> [a]
    reverse ([Either ([SExpr], SExpr) SExpr]
     -> [Either ([SExpr], SExpr) SExpr])
    -> Maybe [Either ([SExpr], SExpr) SExpr]
    -> Maybe [Either ([SExpr], SExpr) SExpr]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Either ([SExpr], SExpr) SExpr]
    -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
    go [] SExpr
    body
              where true :: SExpr
    true  = (Integer, Maybe Int) -> SExpr
    ENum (1, Maybe Int
    forall a. Maybe a
    Nothing)
                    false :: SExpr
    false = (Integer, Maybe Int) -> SExpr
    ENum (0, Maybe Int
    forall a. Maybe a
    Nothing)

                    go :: [Either ([SExpr], SExpr) SExpr] -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
                    go :: [Either ([SExpr], SExpr) SExpr]
    -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
    go sofar :: [Either ([SExpr], SExpr) SExpr]
    sofar (EApp [ECon "ite", selector :: SExpr
    selector, thenBranch :: SExpr
    thenBranch, elseBranch :: SExpr
    elseBranch])
                      = do [SExpr]
    s  <- SExpr -> Maybe [SExpr]
    select SExpr
    selector
                           [Either ([SExpr], SExpr) SExpr]
    tB <- [Either ([SExpr], SExpr) SExpr]
    -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
    go [] SExpr
    thenBranch
                           case [SExpr]
    -> [Either ([SExpr], SExpr) SExpr] -> Maybe ([SExpr], SExpr)
    cond [SExpr]
    s [Either ([SExpr], SExpr) SExpr]
    tB of
                              Just sv :: ([SExpr], SExpr)
    sv -> [Either ([SExpr], SExpr) SExpr]
    -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
    go (([SExpr], SExpr) -> Either ([SExpr], SExpr) SExpr
    forall a b. a -> Either a b
    Left ([SExpr], SExpr)
    sv Either ([SExpr], SExpr) SExpr
    -> [Either ([SExpr], SExpr) SExpr]
    -> [Either ([SExpr], SExpr) SExpr]
    forall a. a -> [a] -> [a]
    : [Either ([SExpr], SExpr) SExpr]
    sofar) SExpr
    elseBranch
                              _       -> Maybe [Either ([SExpr], SExpr) SExpr]
    forall a. Maybe a
    Nothing

                    -- Catch cases like: x = a)
                    go sofar :: [Either ([SExpr], SExpr) SExpr]
    sofar inner :: SExpr
    inner@(EApp [ECon "=", _, _])
                      = [Either ([SExpr], SExpr) SExpr]
    -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
    go [Either ([SExpr], SExpr) SExpr]
    sofar ([SExpr] -> SExpr
    EApp [String -> SExpr
    ECon "ite", SExpr
    inner, SExpr
    true, SExpr
    false])

                    -- Catch cases like: not x
                    go sofar :: [Either ([SExpr], SExpr) SExpr]
    sofar (EApp [ECon "not", inner :: SExpr
    inner])
                      = [Either ([SExpr], SExpr) SExpr]
    -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
    go [Either ([SExpr], SExpr) SExpr]
    sofar ([SExpr] -> SExpr
    EApp [String -> SExpr
    ECon "ite", SExpr
    inner, SExpr
    false, SExpr
    true])

                    -- Catch (or x y z..)
                    go sofar :: [Either ([SExpr], SExpr) SExpr]
    sofar (EApp (ECon "or" : elts :: [SExpr]
    elts))
                      = let xform :: [SExpr] -> SExpr
    xform []     = SExpr
    false
                            xform [x :: SExpr
    x]    = SExpr
    x
                            xform (x :: SExpr
    x:xs :: [SExpr]
    xs) = [SExpr] -> SExpr
    EApp [String -> SExpr
    ECon "ite", SExpr
    x, SExpr
    true, [SExpr] -> SExpr
    xform [SExpr]
    xs]
                        in [Either ([SExpr], SExpr) SExpr]
    -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
    go [Either ([SExpr], SExpr) SExpr]
    sofar (SExpr -> Maybe [Either ([SExpr], SExpr) SExpr])
    -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
    forall a b. (a -> b) -> a -> b
    $ [SExpr] -> SExpr
    xform [SExpr]
    elts

                    -- Catch (and x y z..)
                    go sofar :: [Either ([SExpr], SExpr) SExpr]
    sofar (EApp (ECon "and" : elts :: [SExpr]
    elts))
                      = let xform :: [SExpr] -> SExpr
    xform []     = SExpr
    true
                            xform [x :: SExpr
    x]    = SExpr
    x
                            xform (x :: SExpr
    x:xs :: [SExpr]
    xs) = [SExpr] -> SExpr
    EApp [String -> SExpr
    ECon "ite", SExpr
    x, [SExpr] -> SExpr
    xform [SExpr]
    xs, SExpr
    false]
                        in [Either ([SExpr], SExpr) SExpr]
    -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
    go [Either ([SExpr], SExpr) SExpr]
    sofar (SExpr -> Maybe [Either ([SExpr], SExpr) SExpr])
    -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
    forall a b. (a -> b) -> a -> b
    $ [SExpr] -> SExpr
    xform [SExpr]
    elts

                    -- z3 sometimes puts together a bunch of booleans as final expression,
                    -- see if we can catch that.
                    go sofar :: [Either ([SExpr], SExpr) SExpr]
    sofar e :: SExpr
    e
                     | Just s :: [SExpr]
    s <- SExpr -> Maybe [SExpr]
    select SExpr
    e
                     = [Either ([SExpr], SExpr) SExpr]
    -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
    go (([SExpr], SExpr) -> Either ([SExpr], SExpr) SExpr
    forall a b. a -> Either a b
    Left ([SExpr]
    s, SExpr
    true) Either ([SExpr], SExpr) SExpr
    -> [Either ([SExpr], SExpr) SExpr]
    -> [Either ([SExpr], SExpr) SExpr]
    forall a. a -> [a] -> [a]
    : [Either ([SExpr], SExpr) SExpr]
    sofar) SExpr
    false

                    -- Otherwise, just treat it as an "unknown" arbitrary expression
                    -- as the default. It could be something arbitrary of course, but it's
                    -- too complicated to parse; and hopefully this is good enough.
                    go sofar :: [Either ([SExpr], SExpr) SExpr]
    sofar e :: SExpr
    e = [Either ([SExpr], SExpr) SExpr]
    -> Maybe [Either ([SExpr], SExpr) SExpr]
    forall a. a -> Maybe a
    Just ([Either ([SExpr], SExpr) SExpr]
     -> Maybe [Either ([SExpr], SExpr) SExpr])
    -> [Either ([SExpr], SExpr) SExpr]
    -> Maybe [Either ([SExpr], SExpr) SExpr]
    forall a b. (a -> b) -> a -> b
    $ SExpr -> Either ([SExpr], SExpr) SExpr
    forall a b. b -> Either a b
    Right SExpr
    e Either ([SExpr], SExpr) SExpr
    -> [Either ([SExpr], SExpr) SExpr]
    -> [Either ([SExpr], SExpr) SExpr]
    forall a. a -> [a] -> [a]
    : [Either ([SExpr], SExpr) SExpr]
    sofar

                    cond :: [SExpr] -> [Either ([SExpr], SExpr) SExpr] -> Maybe ([SExpr], SExpr)
                    cond :: [SExpr]
    -> [Either ([SExpr], SExpr) SExpr] -> Maybe ([SExpr], SExpr)
    cond s :: [SExpr]
    s [Right v :: SExpr
    v] = ([SExpr], SExpr) -> Maybe ([SExpr], SExpr)
    forall a. a -> Maybe a
    Just ([SExpr]
    s, SExpr
    v)
                    cond _ _         = Maybe ([SExpr], SExpr)
    forall a. Maybe a
    Nothing

                    -- select takes the condition of an ite, and returns precisely what match is done to the parameters
                    select :: SExpr -> Maybe [SExpr]
                    select :: SExpr -> Maybe [SExpr]
    select e :: SExpr
    e
                       | Just dict :: [(String, SExpr)]
    dict <- SExpr -> [(String, SExpr)] -> Maybe [(String, SExpr)]
    build SExpr
    e [] = (String -> Maybe SExpr) -> [String] -> Maybe [SExpr]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM (String -> [(String, SExpr)] -> Maybe SExpr
    forall a b. Eq a => a -> [(a, b)] -> Maybe b
    `lookup` [(String, SExpr)]
    dict) [String]
    params
                       | Bool
    True                    = Maybe [SExpr]
    forall a. Maybe a
    Nothing
                      where -- build a dictionary of assignments from the scrutinee
                            build :: SExpr -> [(String, SExpr)] -> Maybe [(String, SExpr)]
                            build :: SExpr -> [(String, SExpr)] -> Maybe [(String, SExpr)]
    build (EApp (ECon "and" : rest :: [SExpr]
    rest)) sofar :: [(String, SExpr)]
    sofar = let next :: SExpr -> Maybe [(String, SExpr)] -> Maybe [(String, SExpr)]
    next _ Nothing  = Maybe [(String, SExpr)]
    forall a. Maybe a
    Nothing
                                                                         next c :: SExpr
    c (Just x :: [(String, SExpr)]
    x) = SExpr -> [(String, SExpr)] -> Maybe [(String, SExpr)]
    build SExpr
    c [(String, SExpr)]
    x
                                                                     in (SExpr -> Maybe [(String, SExpr)] -> Maybe [(String, SExpr)])
    -> Maybe [(String, SExpr)] -> [SExpr] -> Maybe [(String, SExpr)]
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr SExpr -> Maybe [(String, SExpr)] -> Maybe [(String, SExpr)]
    next ([(String, SExpr)] -> Maybe [(String, SExpr)]
    forall a. a -> Maybe a
    Just [(String, SExpr)]
    sofar) [SExpr]
    rest

                            build expr :: SExpr
    expr sofar :: [(String, SExpr)]
    sofar | Just (v :: String
    v, r :: SExpr
    r) <- SExpr -> Maybe (String, SExpr)
    grok SExpr
    expr, String
    v String -> [String] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [String]
    params = [(String, SExpr)] -> Maybe [(String, SExpr)]
    forall a. a -> Maybe a
    Just ([(String, SExpr)] -> Maybe [(String, SExpr)])
    -> [(String, SExpr)] -> Maybe [(String, SExpr)]
    forall a b. (a -> b) -> a -> b
    $ (String
    v, SExpr
    r) (String, SExpr) -> [(String, SExpr)] -> [(String, SExpr)]
    forall a. a -> [a] -> [a]
    : [(String, SExpr)]
    sofar
                                             | Bool
    True                                      = Maybe [(String, SExpr)]
    forall a. Maybe a
    Nothing

                            -- See if we can figure out what z3 is telling us; hopefully this
                            -- mapping covers everything we can see:
                            grok :: SExpr -> Maybe (String, SExpr)
    grok (EApp [ECon "=", ECon v :: String
    v, r :: SExpr
    r]) = (String, SExpr) -> Maybe (String, SExpr)
    forall a. a -> Maybe a
    Just (String
    v, SExpr
    r)
                            grok (EApp [ECon "=", r :: SExpr
    r, ECon v :: String
    v]) = (String, SExpr) -> Maybe (String, SExpr)
    forall a. a -> Maybe a
    Just (String
    v, SExpr
    r)
                            grok (EApp [ECon "not", ECon v :: String
    v])  = (String, SExpr) -> Maybe (String, SExpr)
    forall a. a -> Maybe a
    Just (String
    v, SExpr
    false) -- boolean negation, require it to be false
                            grok (ECon v :: String
    v)                     = (String, SExpr) -> Maybe (String, SExpr)
    forall a. a -> Maybe a
    Just (String
    v, SExpr
    true)  -- boolean identity, require it to be true

                            -- Tough luck, we couldn't understand:
                            grok _ = Maybe (String, SExpr)
    forall a. Maybe a
    Nothing

    -- | Parse a series of associations in the array notation, things that look like:
    --
    --     (store (store ((as const Array) 12) 3 5 9) 5 6 75)
    --
    -- This is (most likely) entirely Z3 specific. So, we might have to tweak it for other
    -- solvers; though it isn't entirely clear how to do that as we do not know what solver
    -- we're using here. The trick is to handle all of possible SExpr's we see.
    -- We'll cross that bridge when we get to it.
    --
    -- NB. In case there's no "constraint" on the UI, Z3 produces the self-referential model:
    --
    --    (x (_ as-array x))
    --
    -- So, we specifically handle that here, by returning a Left of that name.
    parseStoreAssociations :: SExpr -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
    parseStoreAssociations :: SExpr -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
    parseStoreAssociations (EApp [ECon "_", ECon "as-array", ECon nm :: String
    nm]) = Either String ([([SExpr], SExpr)], SExpr)
    -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
    forall a. a -> Maybe a
    Just (Either String ([([SExpr], SExpr)], SExpr)
     -> Maybe (Either String ([([SExpr], SExpr)], SExpr)))
    -> Either String ([([SExpr], SExpr)], SExpr)
    -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
    forall a b. (a -> b) -> a -> b
    $ String -> Either String ([([SExpr], SExpr)], SExpr)
    forall a b. a -> Either a b
    Left String
    nm
    parseStoreAssociations e :: SExpr
    e                                           = ([([SExpr], SExpr)], SExpr)
    -> Either String ([([SExpr], SExpr)], SExpr)
    forall a b. b -> Either a b
    Right (([([SExpr], SExpr)], SExpr)
     -> Either String ([([SExpr], SExpr)], SExpr))
    -> Maybe ([([SExpr], SExpr)], SExpr)
    -> Maybe (Either String ([([SExpr], SExpr)], SExpr))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ([Either ([SExpr], SExpr) SExpr]
    -> Maybe ([([SExpr], SExpr)], SExpr)
    chainAssigns ([Either ([SExpr], SExpr) SExpr]
     -> Maybe ([([SExpr], SExpr)], SExpr))
    -> Maybe [Either ([SExpr], SExpr) SExpr]
    -> Maybe ([([SExpr], SExpr)], SExpr)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
    vals SExpr
    e)
        where vals :: SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
              vals :: SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
    vals (EApp [EApp [ECon "as", ECon "const", ECon "Array"],            defVal :: SExpr
    defVal]) = [Either ([SExpr], SExpr) SExpr]
    -> Maybe [Either ([SExpr], SExpr) SExpr]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SExpr -> Either ([SExpr], SExpr) SExpr
    forall a b. b -> Either a b
    Right SExpr
    defVal]
              vals (EApp [EApp [ECon "as", ECon "const", EApp (ECon "Array" : _)], defVal :: SExpr
    defVal]) = [Either ([SExpr], SExpr) SExpr]
    -> Maybe [Either ([SExpr], SExpr) SExpr]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SExpr -> Either ([SExpr], SExpr) SExpr
    forall a b. b -> Either a b
    Right SExpr
    defVal]
              vals (EApp (ECon "store" : prev :: SExpr
    prev : argsVal :: [SExpr]
    argsVal)) | [SExpr] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SExpr]
    argsVal Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= 2             = do [Either ([SExpr], SExpr) SExpr]
    rest <- SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
    vals SExpr
    prev
                                                                                                 [Either ([SExpr], SExpr) SExpr]
    -> Maybe [Either ([SExpr], SExpr) SExpr]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Either ([SExpr], SExpr) SExpr]
     -> Maybe [Either ([SExpr], SExpr) SExpr])
    -> [Either ([SExpr], SExpr) SExpr]
    -> Maybe [Either ([SExpr], SExpr) SExpr]
    forall a b. (a -> b) -> a -> b
    $ ([SExpr], SExpr) -> Either ([SExpr], SExpr) SExpr
    forall a b. a -> Either a b
    Left ([SExpr] -> [SExpr]
    forall a. [a] -> [a]
    init [SExpr]
    argsVal, [SExpr] -> SExpr
    forall a. [a] -> a
    last [SExpr]
    argsVal) Either ([SExpr], SExpr) SExpr
    -> [Either ([SExpr], SExpr) SExpr]
    -> [Either ([SExpr], SExpr) SExpr]
    forall a. a -> [a] -> [a]
    : [Either ([SExpr], SExpr) SExpr]
    rest
              vals _                                                                        = Maybe [Either ([SExpr], SExpr) SExpr]
    forall a. Maybe a
    Nothing

    -- | Turn a sequence of left-right chain assignments (condition + free) into a single chain
    chainAssigns :: [Either ([SExpr], SExpr) SExpr] -> Maybe ([([SExpr], SExpr)], SExpr)
    chainAssigns :: [Either ([SExpr], SExpr) SExpr]
    -> Maybe ([([SExpr], SExpr)], SExpr)
    chainAssigns chain :: [Either ([SExpr], SExpr) SExpr]
    chain = ([([SExpr], SExpr)], [SExpr]) -> Maybe ([([SExpr], SExpr)], SExpr)
    forall b.
    ([([SExpr], SExpr)], [b]) -> Maybe ([([SExpr], SExpr)], b)
    regroup (([([SExpr], SExpr)], [SExpr])
     -> Maybe ([([SExpr], SExpr)], SExpr))
    -> ([([SExpr], SExpr)], [SExpr])
    -> Maybe ([([SExpr], SExpr)], SExpr)
    forall a b. (a -> b) -> a -> b
    $ [Either ([SExpr], SExpr) SExpr] -> ([([SExpr], SExpr)], [SExpr])
    forall a b. [Either a b] -> ([a], [b])
    partitionEithers [Either ([SExpr], SExpr) SExpr]
    chain
      where regroup :: ([([SExpr], SExpr)], [b]) -> Maybe ([([SExpr], SExpr)], b)
    regroup (vs :: [([SExpr], SExpr)]
    vs, [d :: b
    d]) = ([([SExpr], SExpr)], b) -> Maybe ([([SExpr], SExpr)], b)
    forall a. a -> Maybe a
    Just ([([SExpr], SExpr)] -> [([SExpr], SExpr)]
    checkDup [([SExpr], SExpr)]
    vs, b
    d)
            regroup _         = Maybe ([([SExpr], SExpr)], b)
    forall a. Maybe a
    Nothing

            -- If we get into a case like this:
            --
            --     (store (store a 1 2) 1 3)
            --
            -- then we need to drop the 1->2 assignment!
            --
            -- The way we parse these, the first assignment wins.
            checkDup :: [([SExpr], SExpr)] -> [([SExpr], SExpr)]
            checkDup :: [([SExpr], SExpr)] -> [([SExpr], SExpr)]
    checkDup []              = []
            checkDup (a :: ([SExpr], SExpr)
    a@(key :: [SExpr]
    key, _):as :: [([SExpr], SExpr)]
    as) = ([SExpr], SExpr)
    a ([SExpr], SExpr) -> [([SExpr], SExpr)] -> [([SExpr], SExpr)]
    forall a. a -> [a] -> [a]
    : [([SExpr], SExpr)] -> [([SExpr], SExpr)]
    checkDup [([SExpr], SExpr)
    r | r :: ([SExpr], SExpr)
    r@(key' :: [SExpr]
    key', _) <- [([SExpr], SExpr)]
    as, Bool -> Bool
    not ([SExpr]
    key [SExpr] -> [SExpr] -> Bool
    `sameKey` [SExpr]
    key')]

            sameKey :: [SExpr] -> [SExpr] -> Bool
            sameKey :: [SExpr] -> [SExpr] -> Bool
    sameKey as :: [SExpr]
    as bs :: [SExpr]
    bs
              | [SExpr] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SExpr]
    as Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [SExpr] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SExpr]
    bs = [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and ([Bool] -> Bool) -> [Bool] -> Bool
    forall a b. (a -> b) -> a -> b
    $ (SExpr -> SExpr -> Bool) -> [SExpr] -> [SExpr] -> [Bool]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith SExpr -> SExpr -> Bool
    same [SExpr]
    as [SExpr]
    bs
              | Bool
    True                   = String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV: Differing length of key received in chainAssigns: " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ([SExpr], [SExpr]) -> String
    forall a. Show a => a -> String
    show ([SExpr]
    as, [SExpr]
    bs)

            -- We don't want to derive Eq; as this is more careful on floats and such
            same :: SExpr -> SExpr -> Bool
            same :: SExpr -> SExpr -> Bool
    same x :: SExpr
    x y :: SExpr
    y = case (SExpr
    x, SExpr
    y) of
                         (ECon a :: String
    a,      ECon b :: String
    b)       -> String
    a String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    b
                         (ENum (i :: Integer
    i, _), ENum (j :: Integer
    j, _))  -> Integer
    i Integer -> Integer -> Bool
    forall a. Eq a => a -> a -> Bool
    == Integer
    j
                         (EReal a :: AlgReal
    a,     EReal b :: AlgReal
    b)      -> AlgReal -> AlgReal -> Bool
    algRealStructuralEqual AlgReal
    a AlgReal
    b
                         (EFloat  f1 :: Float
    f1,  EFloat  f2 :: Float
    f2)   -> Float -> Float -> Bool
    forall a. RealFloat a => a -> a -> Bool
    fpIsEqualObjectH Float
    f1 Float
    f2
                         (EDouble d1 :: Double
    d1,  EDouble d2 :: Double
    d2)   -> Double -> Double -> Bool
    forall a. RealFloat a => a -> a -> Bool
    fpIsEqualObjectH Double
    d1 Double
    d2
                         (EApp as :: [SExpr]
    as,     EApp bs :: [SExpr]
    bs)      -> [SExpr] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SExpr]
    as Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [SExpr] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [SExpr]
    bs Bool -> Bool -> Bool
    && [Bool] -> Bool
    forall (t :: * -> *). Foldable t => t Bool -> Bool
    and ((SExpr -> SExpr -> Bool) -> [SExpr] -> [SExpr] -> [Bool]
    forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
    zipWith SExpr -> SExpr -> Bool
    same [SExpr]
    as [SExpr]
    bs)
                         (e1 :: SExpr
    e1,          e2 :: SExpr
    e2)           -> if SExpr -> Int
    eRank SExpr
    e1 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == SExpr -> Int
    eRank SExpr
    e2
                                                        then String -> Bool
    forall a. HasCallStack => String -> a
    error (String -> Bool) -> String -> Bool
    forall a b. (a -> b) -> a -> b
    $ "Data.SBV: You've found a bug in SBV! Please report: SExpr(same): " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ (SExpr, SExpr) -> String
    forall a. Show a => a -> String
    show (SExpr
    e1, SExpr
    e2)
                                                        else Bool
    False
            -- Defensive programming: It's too long to list all pair up, so we use this function and
            -- GHC's pattern-match completion warning to catch cases we might've forgotten. If
            -- you ever get the error line above fire, because you must've disabled the pattern-match
            -- completion check warning! Shame on you.
            eRank :: SExpr -> Int
            eRank :: SExpr -> Int
    eRank ECon{}    = 0
            eRank ENum{}    = 1
            eRank EReal{}   = 2
            eRank EFloat{}  = 3
            eRank EDouble{} = 4
            eRank EApp{}    = 5

    {-# ANN chainAssigns ("HLint: ignore Redundant if" :: String) #-}