-----------------------------------------------------------------------------
-- |
-- 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.SizedFloats
import Data.SBV.Core.Data (nan, infinity, RoundingMode(..))

import Data.SBV.Utils.Numeric (fpIsEqualObjectH, 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
           | EFloatingPoint FP
           | 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 String
inp = String -> [String] -> [String]
go String
inp []
 where go :: String -> [String] -> [String]
go String
"" [String]
sofar = [String] -> [String]
forall a. [a] -> [a]
reverse [String]
sofar

       go (Char
c:String
cs) [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 (Char
'(':String
cs) [String]
sofar = String -> [String] -> [String]
go String
cs (String
"(" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)
       go (Char
')':String
cs) [String]
sofar = String -> [String] -> [String]
go String
cs (String
")" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)

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

       go (Char
':':String
cs) [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
                            (String
pre, String
rest) -> String -> [String] -> [String]
go String
rest ((Char
':'Char -> ShowS
forall a. a -> [a] -> [a]
:String
pre) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)

       go (Char
'|':String
r) [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
/= Char
'|') String
r of
                            (String
pre, Char
'|':String
rest) -> String -> [String] -> [String]
go String
rest (String
pre String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)
                            (String
pre, String
rest)     -> String -> [String] -> [String]
go String
rest (String
pre String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
sofar)

       go (Char
'"':String
r) [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 []             String
acc = (ShowS
forall a. [a] -> [a]
reverse String
acc, [])         -- Strictly speaking, this is the unterminated string case; but let's ignore
                 grabString (Char
'"' :Char
'"':String
cs)  String
acc = String -> String -> (String, String)
grabString String
cs (Char
'"' Char -> ShowS
forall a. a -> [a] -> [a]
:String
acc)
                 grabString (Char
'"':String
cs)       String
acc = (ShowS
forall a. [a] -> [a]
reverse String
acc, String
cs)
                 grabString (Char
c:String
cs)         String
acc = String -> String -> (String, String)
grabString String
cs (Char
cChar -> ShowS
forall a. a -> [a] -> [a]
:String
acc)

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

       go String
cs [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
                       (String
pre, 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 = String
" \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 Int
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 (String
"(" : [String]
rest) = Int -> [String] -> Int
go (Int
balanceInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) [String]
rest
        go !Int
balance (String
")" : [String]
rest) = Int -> [String] -> Int
go (Int
balanceInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) [String]
rest
        go !Int
balance (String
_   : [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 String
inp = do (SExpr
sexp, [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 String
"error", ECon 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
$ String
"Solver returned an error: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
er
                              SExpr
_                            -> 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 String
"Extra tokens after valid input"
  where inpToks :: [String]
inpToks = String -> [String]
tokenize String
inp

        die :: String -> Either String b
die 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
$  String
"SBV.Provers.SExpr: Failed to parse S-Expr: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
w
                     String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"\n*** Input : <" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
inp String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
">"

        parse :: [String] -> Either String (SExpr, [String])
parse []         = String -> Either String (SExpr, [String])
forall b. String -> Either String b
die String
"ran out of tokens"
        parse (String
"(":[String]
toks) = do ([SExpr]
f, [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
")":[String]
_)    = String -> Either String (SExpr, [String])
forall b. String -> Either String b
die String
"extra tokens after close paren"
        parse [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]
_          = String -> Either String (SExpr, [String])
forall b. String -> Either String b
die String
"ill-formed s-expr"

        parseApp :: [String] -> [SExpr] -> Either String ([SExpr], [String])
parseApp []         [SExpr]
_     = String -> Either String ([SExpr], [String])
forall b. String -> Either String b
die String
"failed to grab s-expr application"
        parseApp (String
")":[String]
toks) [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 (String
"(":[String]
toks) [SExpr]
sofar = do (SExpr
f, [String]
r) <- [String] -> Either String (SExpr, [String])
parse (String
"("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 (String
tok:[String]
toks) [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 String
"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 (Integer
0, Maybe Int
forall a. Maybe a
Nothing)
        pTok String
"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 (Integer
1, Maybe Int
forall a. Maybe a
Nothing)

        pTok (Char
'0':Char
'b':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 Integer
2 (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
"01") (\Char
c -> Char -> Int
ord Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0') String
r
        pTok (Char
'b':Char
'v':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
/= Char
'[') String
r)
        pTok (Char
'#':Char
'b':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 Integer
2 (Char -> String -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
"01") (\Char
c -> Char -> Int
ord Char
c Int -> Int -> Int
forall a. Num a => a -> a -> a
- Char -> Int
ord Char
'0') String
r
        pTok (Char
'#':Char
'x':String
r)                                 = Maybe Int -> [(Integer, String)] -> Either String SExpr
mkNum (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int
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 String
n | String -> Bool
possiblyNum String
n = if (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
intChar String
n then 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 else String -> Either String SExpr
forall (m :: * -> *). Monad m => String -> m SExpr
getReal String
n
        pTok 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)

        -- crude, but effective!
        possiblyNum :: String -> Bool
possiblyNum String
s = case String
s of
                          String
""        -> Bool
False
                          (Char
'-':Char
c:String
_) -> Char -> Bool
isDigit Char
c
                          (Char
c:String
_)     -> Char -> Bool
isDigit Char
c

        intChar :: Char -> Bool
intChar Char
c = Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'-' Bool -> Bool -> Bool
|| Char -> Bool
isDigit Char
c

        mkNum :: Maybe Int -> [(Integer, String)] -> Either String SExpr
mkNum Maybe Int
l [(Integer
n, String
"")] = 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 Maybe Int
_ [(Integer, String)]
_         = String -> Either String SExpr
forall b. String -> Either String b
die String
"cannot read number"

        getReal :: String -> m SExpr
getReal 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 -> 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 String
"to_int",  EReal 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 String
"to_real", EReal 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 String
"/", EReal AlgReal
a, EReal 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 String
"/", EReal AlgReal
a, ENum  (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 String
"/", ENum  (Integer, Maybe Int)
a, EReal 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 String
"/", ENum  (Integer, Maybe Int)
a, ENum  (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 String
"-", EReal 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 String
"-", ENum (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 String
"_", ENum (Integer, Maybe Int)
a, ENum (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 String
"root-obj", EApp (ECon String
"+":[SExpr]
trms), ENum (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 String
"as", SExpr
n, EApp [ECon String
"_", ECon String
"FloatingPoint", ENum (Integer
11, Maybe Int
_), ENum (Integer
53, Maybe Int
_)]]) = SExpr -> Either String SExpr
getDouble SExpr
n
        cvt (EApp [ECon String
"as", SExpr
n, EApp [ECon String
"_", ECon String
"FloatingPoint", ENum ( Integer
8, Maybe Int
_), ENum (Integer
24, Maybe Int
_)]]) = SExpr -> Either String SExpr
getFloat  SExpr
n
        cvt (EApp [ECon String
"as", SExpr
n, ECon String
"Float64"])                                                    = SExpr -> Either String SExpr
getDouble SExpr
n
        cvt (EApp [ECon String
"as", SExpr
n, ECon String
"Float32"])                                                    = SExpr -> Either String SExpr
getFloat  SExpr
n

        -- Deal with CVC4's approximate reals
        cvt x :: SExpr
x@(EApp [ECon String
"witness", EApp [EApp [ECon String
v, ECon String
"Real"]]
                                   , EApp [ECon String
"or", EApp [ECon String
"=", ECon String
v', SExpr
val], SExpr
_]]) | 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 (Integer
s, Maybe Int
_) -> 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 AlgReal
aval  -> case AlgReal
aval of
                                                                   AlgRational Bool
_ 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
                                                                   AlgReal
_               -> 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
                                                  SExpr
_           -> 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
$ String
"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 String
"fp",    ENum (Integer
s, Just Int
1), ENum ( Integer
e, Just Int
8),  ENum (Integer
m, Just Int
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 String
"fp",    ENum (Integer
s, Just Int
1), ENum ( Integer
e, Just Int
11), ENum (Integer
m, Just Int
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 String
"fp",    ENum (Integer
s, Just Int
1), ENum ( Integer
e, Just Int
eb), ENum (Integer
m, Just Int
sb)])           = 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
$ FP -> SExpr
EFloatingPoint (FP -> SExpr) -> FP -> SExpr
forall a b. (a -> b) -> a -> b
$ Bool -> (Integer, Int) -> (Integer, Int) -> FP
fpFromRawRep (Integer
s Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1) (Integer
e, Int
eb) (Integer
m, Int
sbInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)

        cvt (EApp [ECon String
"_",     ECon String
"NaN",       ENum ( Integer
8, Maybe Int
_),       ENum (Integer
24,      Maybe Int
_)])           = 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 String
"_",     ECon String
"NaN",       ENum (Integer
11, Maybe Int
_),       ENum (Integer
53,      Maybe Int
_)])           = 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 String
"_",     ECon String
"NaN",       ENum (Integer
eb, Maybe Int
_),       ENum (Integer
sb,      Maybe Int
_)])           = 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
$ FP -> SExpr
EFloatingPoint (FP -> SExpr) -> FP -> SExpr
forall a b. (a -> b) -> a -> b
$ Int -> Int -> FP
fpNaN (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
eb) (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
sb)

        cvt (EApp [ECon String
"_",     ECon String
"+oo",       ENum ( Integer
8, Maybe Int
_),       ENum (Integer
24,      Maybe Int
_)])           = 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 String
"_",     ECon String
"+oo",       ENum (Integer
11, Maybe Int
_),       ENum (Integer
53,      Maybe Int
_)])           = 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 String
"_",     ECon String
"+oo",       ENum (Integer
eb, Maybe Int
_),       ENum (Integer
sb,      Maybe Int
_)])           = 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
$ FP -> SExpr
EFloatingPoint (FP -> SExpr) -> FP -> SExpr
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Int -> FP
fpInf Bool
False (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
eb) (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
sb)

        cvt (EApp [ECon String
"_",     ECon String
"-oo",       ENum ( Integer
8, Maybe Int
_),       ENum (Integer
24,      Maybe Int
_)])           = 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
$ -Float
forall a. Floating a => a
infinity
        cvt (EApp [ECon String
"_",     ECon String
"-oo",       ENum (Integer
11, Maybe Int
_),       ENum (Integer
53,      Maybe Int
_)])           = 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
$ -Double
forall a. Floating a => a
infinity
        cvt (EApp [ECon String
"_",     ECon String
"-oo",       ENum (Integer
eb, Maybe Int
_),       ENum (Integer
sb,      Maybe Int
_)])           = 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
$ FP -> SExpr
EFloatingPoint (FP -> SExpr) -> FP -> SExpr
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Int -> FP
fpInf Bool
True (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
eb) (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
sb)

        cvt (EApp [ECon String
"_",     ECon String
"+zero",     ENum ( Integer
8, Maybe Int
_),       ENum (Integer
24,      Maybe Int
_)])           = 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
0
        cvt (EApp [ECon String
"_",     ECon String
"+zero",     ENum (Integer
11, Maybe Int
_),       ENum (Integer
53,      Maybe Int
_)])           = 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
0
        cvt (EApp [ECon String
"_",     ECon String
"+zero",     ENum (Integer
eb, Maybe Int
_),       ENum (Integer
sb,      Maybe Int
_)])           = 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
$ FP -> SExpr
EFloatingPoint (FP -> SExpr) -> FP -> SExpr
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Int -> FP
fpZero Bool
False (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
eb) (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
sb)

        cvt (EApp [ECon String
"_",     ECon String
"-zero",     ENum ( Integer
8, Maybe Int
_),       ENum (Integer
24,      Maybe Int
_)])           = 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
$ -Float
0
        cvt (EApp [ECon String
"_",     ECon String
"-zero",     ENum (Integer
11, Maybe Int
_),       ENum (Integer
53,      Maybe Int
_)])           = 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
$ -Double
0
        cvt (EApp [ECon String
"_",     ECon String
"-zero",     ENum (Integer
eb, Maybe Int
_),       ENum (Integer
sb,      Maybe Int
_)])           = 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
$ FP -> SExpr
EFloatingPoint (FP -> SExpr) -> FP -> SExpr
forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Int -> FP
fpZero Bool
True (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
eb) (Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
sb)

        cvt 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 String
"*", ENum (Integer, Maybe Int)
k, EApp [ECon String
"^", ECon String
"x", ENum (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 String
"*", ENum (Integer, Maybe Int)
k,                 ECon String
"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,     Integer
1)  -- kx
        getCoeff (                        EApp [ECon String
"^", ECon String
"x", ENum (Integer, Maybe Int)
p] ) = (Integer, Integer) -> Either String (Integer, Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (    Integer
1, (Integer, Maybe Int) -> Integer
forall a b. (a, b) -> a
fst (Integer, Maybe Int)
p)  --  x^p
        getCoeff (                                        ECon String
"x"          ) = (Integer, Integer) -> Either String (Integer, Integer)
forall (m :: * -> *) a. Monad m => a -> m a
return (    Integer
1,     Integer
1)  --  x
        getCoeff (                ENum (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,     Integer
0)  -- k
        getCoeff 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
$ String
"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 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
== Char
'+') String
s)) of
                                (String
"plusInfinity",  Maybe Double
_     ) -> 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
                                (String
"minusInfinity", Maybe Double
_     ) -> 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)
                                (String
"oo",            Maybe Double
_     ) -> 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
                                (String
"-oo",           Maybe Double
_     ) -> 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)
                                (String
"zero",          Maybe Double
_     ) -> 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
0
                                (String
"-zero",         Maybe Double
_     ) -> 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
0)
                                (String
"NaN",           Maybe Double
_     ) -> 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
                                (String
_,               Just 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, Maybe Double)
_               -> 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
$ String
"Cannot parse a double value from: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
        getDouble (EApp [SExpr
_, SExpr
s, SExpr
_, SExpr
_]) = SExpr -> Either String SExpr
getDouble SExpr
s
        getDouble (EReal 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 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
$ String
"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 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
== Char
'+') String
s)) of
                                (String
"plusInfinity",  Maybe Float
_     ) -> 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
                                (String
"minusInfinity", Maybe Float
_     ) -> 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)
                                (String
"oo",            Maybe Float
_     ) -> 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
                                (String
"-oo",           Maybe Float
_     ) -> 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)
                                (String
"zero",          Maybe Float
_     ) -> 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
0
                                (String
"-zero",         Maybe Float
_     ) -> 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
0)
                                (String
"NaN",           Maybe Float
_     ) -> 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
                                (String
_,               Just 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, Maybe Float)
_               -> 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
$ String
"Cannot parse a float value from: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s
        getFloat (EReal 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 [SExpr
_, SExpr
s, SExpr
_, SExpr
_]) = SExpr -> Either String SExpr
getFloat SExpr
s
        getFloat 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
$ String
"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 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` String
"pe") String
s of
           (String
m, Char
'p':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
>>= \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
>>= \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
* ( a
2 a -> a -> a
forall a. Floating a => a -> a -> a
** a
e')
           (String
m, Char
'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
>>= \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
>>= \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
* (a
10 a -> a -> a
forall a. Floating a => a -> a -> a
** a
e')
           (String
m, String
"")    -> String -> Maybe a
forall a. Read a => String -> Maybe a
rd String
m
           (String, String)
_          -> Maybe a
forall a. Maybe a
Nothing
 where rd :: String -> Maybe a
rd String
v = case ReadS a
forall a. Read a => ReadS a
reads String
v of
                [(a
n, String
"")] -> a -> Maybe a
forall a. a -> Maybe a
Just a
n
                [(a, String)]
_         -> 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 Integer
s Integer
e Integer
m = Word32 -> Float
wordToFloat Word32
w32
  where sign :: [Bool]
sign      = [Integer
s Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1]
        expt :: [Bool]
expt      = [Integer
e Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
i | Int
i <- [ Int
7,  Int
6 .. Int
0]]
        mantissa :: [Bool]
mantissa  = [Integer
m Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
i | Int
i <- [Int
22, Int
21 .. Int
0]]
        positions :: [Int]
positions = [Int
i | (Int
i, Bool
b) <- [Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
31, Int
30 .. Int
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) (Word32
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 Integer
s Integer
e Integer
m = Word64 -> Double
wordToDouble Word64
w64
  where sign :: [Bool]
sign      = [Integer
s Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1]
        expt :: [Bool]
expt      = [Integer
e Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
i | Int
i <- [Int
10,  Int
9 .. Int
0]]
        mantissa :: [Bool]
mantissa  = [Integer
m Integer -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
`testBit` Int
i | Int
i <- [Int
51, Int
50 .. Int
0]]
        positions :: [Int]
positions = [Int
i | (Int
i, Bool
b) <- [Int] -> [Bool] -> [(Int, Bool)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
63, Int
62 .. Int
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) (Word64
0::Word64) [Int]
positions

-- | Special constants of SMTLib2 and their internal translation. Mainly
-- rounding modes for now.
constantMap :: String -> String
constantMap :: ShowS
constantMap 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 | ([String]
from, 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 = [ ([String
"RNE", String
"roundNearestTiesToEven"], RoundingMode -> String
forall a. Show a => a -> String
show RoundingMode
RoundNearestTiesToEven)
                 , ([String
"RNA", String
"roundNearestTiesToAway"], RoundingMode -> String
forall a. Show a => a -> String
show RoundingMode
RoundNearestTiesToAway)
                 , ([String
"RTP", String
"roundTowardPositive"],    RoundingMode -> String
forall a. Show a => a -> String
show RoundingMode
RoundTowardPositive)
                 , ([String
"RTN", String
"roundTowardNegative"],    RoundingMode -> String
forall a. Show a => a -> String
show RoundingMode
RoundTowardNegative)
                 , ([String
"RTZ", String
"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 SExpr
e
  | Just ([([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 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 SExpr
funExpr = case SExpr
funExpr of
                                  EApp [ECon String
"lambda", EApp [SExpr]
params, 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
                                  SExpr
_                                       -> Maybe ([([SExpr], SExpr)], SExpr)
forall a. Maybe a
Nothing
  where getParam :: SExpr -> Maybe String
getParam (EApp [ECon String
v, SExpr
_]) = String -> Maybe String
forall a. a -> Maybe a
Just String
v
        getParam SExpr
_                  = Maybe String
forall a. Maybe a
Nothing

        lambda :: [String] -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
        lambda :: [String] -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
lambda [String]
params 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 (Integer
1, Maybe Int
forall a. Maybe a
Nothing)
                false :: SExpr
false = (Integer, Maybe Int) -> SExpr
ENum (Integer
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 [Either ([SExpr], SExpr) SExpr]
sofar (EApp [ECon String
"ite", SExpr
selector, SExpr
thenBranch, 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 ([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 ([SExpr], SExpr)
_       -> Maybe [Either ([SExpr], SExpr) SExpr]
forall a. Maybe a
Nothing

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

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

                -- Catch (or x y z..)
                go [Either ([SExpr], SExpr) SExpr]
sofar (EApp (ECon String
"or" : [SExpr]
elts))
                  = let xform :: [SExpr] -> SExpr
xform []     = SExpr
false
                        xform [SExpr
x]    = SExpr
x
                        xform (SExpr
x:[SExpr]
xs) = [SExpr] -> SExpr
EApp [String -> SExpr
ECon String
"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 [Either ([SExpr], SExpr) SExpr]
sofar (EApp (ECon String
"and" : [SExpr]
elts))
                  = let xform :: [SExpr] -> SExpr
xform []     = SExpr
true
                        xform [SExpr
x]    = SExpr
x
                        xform (SExpr
x:[SExpr]
xs) = [SExpr] -> SExpr
EApp [String -> SExpr
ECon String
"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 [Either ([SExpr], SExpr) SExpr]
sofar SExpr
e
                 | Just [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 [Either ([SExpr], SExpr) SExpr]
sofar 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 [SExpr]
s [Right SExpr
v] = ([SExpr], SExpr) -> Maybe ([SExpr], SExpr)
forall a. a -> Maybe a
Just ([SExpr]
s, SExpr
v)
                cond [SExpr]
_ [Either ([SExpr], SExpr) SExpr]
_         = 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 SExpr
e
                   | Just [(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 String
"and" : [SExpr]
rest)) [(String, SExpr)]
sofar = let next :: SExpr -> Maybe [(String, SExpr)] -> Maybe [(String, SExpr)]
next SExpr
_ Maybe [(String, SExpr)]
Nothing  = Maybe [(String, SExpr)]
forall a. Maybe a
Nothing
                                                                     next SExpr
c (Just [(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 SExpr
expr [(String, SExpr)]
sofar | Just (String
v, 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 String
"=", ECon String
v, SExpr
r]) = (String, SExpr) -> Maybe (String, SExpr)
forall a. a -> Maybe a
Just (String
v, SExpr
r)
                        grok (EApp [ECon String
"=", SExpr
r, ECon String
v]) = (String, SExpr) -> Maybe (String, SExpr)
forall a. a -> Maybe a
Just (String
v, SExpr
r)
                        grok (EApp [ECon String
"not", ECon 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 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 SExpr
_ = 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 String
"_", ECon String
"as-array", ECon 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 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 String
"as", ECon String
"const", ECon String
"Array"],            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 String
"as", ECon String
"const", EApp (ECon String
"Array" : [SExpr]
_)], 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 String
"store" : SExpr
prev : [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
>= Int
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 SExpr
_                                                                        = 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 [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 ([([SExpr], SExpr)]
vs, [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 ([([SExpr], SExpr)], [b])
_         = 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@([SExpr]
key, SExpr
_):[([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@([SExpr]
key', SExpr
_) <- [([SExpr], SExpr)]
as, Bool -> Bool
not ([SExpr]
key [SExpr] -> [SExpr] -> Bool
`sameKey` [SExpr]
key')]

        sameKey :: [SExpr] -> [SExpr] -> Bool
        sameKey :: [SExpr] -> [SExpr] -> Bool
sameKey [SExpr]
as [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
$ String
"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 SExpr
x SExpr
y = case (SExpr
x, SExpr
y) of
                     (ECon String
a,      ECon String
b)       -> String
a String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
b
                     (ENum (Integer
i, Maybe Int
_), ENum (Integer
j, Maybe Int
_))  -> Integer
i Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j
                     (EReal AlgReal
a,     EReal AlgReal
b)      -> AlgReal -> AlgReal -> Bool
algRealStructuralEqual AlgReal
a AlgReal
b
                     (EFloat  Float
f1,  EFloat  Float
f2)   -> Float -> Float -> Bool
forall a. RealFloat a => a -> a -> Bool
fpIsEqualObjectH Float
f1 Float
f2
                     (EDouble Double
d1,  EDouble Double
d2)   -> Double -> Double -> Bool
forall a. RealFloat a => a -> a -> Bool
fpIsEqualObjectH Double
d1 Double
d2
                     (EApp [SExpr]
as,     EApp [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)
                     (SExpr
e1,          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
$ String
"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{}           = Int
0
        eRank ENum{}           = Int
1
        eRank EReal{}          = Int
2
        eRank EFloat{}         = Int
3
        eRank EFloatingPoint{} = Int
4
        eRank EDouble{}        = Int
5
        eRank EApp{}           = Int
6

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