-----------------------------------------------------------------------------
-- |
-- 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, nubBy)
import Data.Maybe  (fromMaybe, listToMaybe)
import Data.Word   (Word32, Word64)

import Control.Monad (foldM)

import Numeric    (readInt, readSigned, 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
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 = forall a. [a] -> [a]
reverse [String]
sofar

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

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

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

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

       go (Char
'"':String
r) [String]
sofar = String -> [String] -> [String]
go String
rest (String
finalStr forall a. a -> [a] -> [a]
: [String]
sofar)
           where grabString :: String -> String -> (String, String)
grabString []             String
acc = (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
'"' forall a. a -> [a] -> [a]
:String
acc)
                 grabString (Char
'"':String
cs)       String
acc = (forall a. [a] -> [a]
reverse String
acc, String
cs)
                 grabString (Char
c:String
cs)         String
acc = String -> String -> (String, String)
grabString String
cs (Char
cforall a. a -> [a] -> [a]
:String
acc)

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

       go String
cs [String]
sofar = case forall a. (a -> Bool) -> [a] -> ([a], [a])
span (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 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 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
balanceforall a. Num a => a -> a -> a
+Int
1) [String]
rest
        go !Int
balance (String
")" : [String]
rest) = Int -> [String] -> Int
go (Int
balanceforall 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 forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
extras
                       then case SExpr
sexp of
                              EApp [ECon String
"error", ECon String
er] -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ String
"Solver returned an error: " forall a. [a] -> [a] -> [a]
++ String
er
                              SExpr
_                            -> forall (m :: * -> *) a. Monad m => a -> m a
return SExpr
sexp

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

        parse :: [String] -> Either String (SExpr, [String])
parse []         = 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)
                              forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr
f', [String]
r)
        parse (String
")":[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
                              forall (m :: * -> *) a. Monad m => a -> m a
return (SExpr
t, [])
        parse [String]
_          = forall {b}. String -> Either String b
die String
"ill-formed s-expr"

        parseApp :: [String] -> [SExpr] -> Either String ([SExpr], [String])
parseApp []         [SExpr]
_     = forall {b}. String -> Either String b
die String
"failed to grab s-expr application"
        parseApp (String
")":[String]
toks) [SExpr]
sofar = forall (m :: * -> *) a. Monad m => a -> m a
return (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
"("forall a. a -> [a] -> [a]
:[String]
toks)
                                       [String] -> [SExpr] -> Either String ([SExpr], [String])
parseApp [String]
r (SExpr
f 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 forall a. a -> [a] -> [a]
: [SExpr]
sofar)

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

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

        pTok String
n | String -> Bool
possiblyNum String
n = if 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 forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ forall a. Real a => ReadS a -> ReadS a
readSigned forall a. (Eq a, Num a) => ReadS a
readDec String
n else forall {m :: * -> *}. Monad m => String -> m SExpr
getReal String
n
        pTok String
n                 = forall (m :: * -> *) a. Monad m => a -> m a
return 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 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
"")] = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Integer, Maybe Int) -> SExpr
ENum (Integer
n, Maybe Int
l)
        mkNum Maybe Int
_ [(Integer, String)]
_         = forall {b}. String -> Either String b
die String
"cannot read number"

        getReal :: String -> m SExpr
getReal String
n = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal forall a b. (a -> b) -> a -> b
$ Either (Bool, String) (Integer, [(Integer, Integer)]) -> AlgReal
mkPolyReal (forall a b. a -> Either a b
Left (Bool
exact, String
n'))
          where exact :: Bool
exact = Bool -> Bool
not (String
"?" forall a. Eq a => [a] -> [a] -> Bool
`isPrefixOf` forall a. [a] -> [a]
reverse String
n)
                n' :: String
n' | Bool
exact = String
n
                   | Bool
True  = 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])                       = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal AlgReal
a   -- ignore the "casting"
        cvt (EApp [ECon String
"to_real", EReal AlgReal
a])                       = forall (m :: * -> *) a. Monad m => a -> m a
return 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])                    = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal (AlgReal
a forall a. Fractional a => a -> a -> a
/ AlgReal
b)
        cvt (EApp [ECon String
"/", EReal AlgReal
a, ENum  (Integer, Maybe Int)
b])                    = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal (AlgReal
a                   forall a. Fractional a => a -> a -> a
/ forall a. Num a => Integer -> a
fromInteger (forall a b. (a, b) -> a
fst (Integer, Maybe Int)
b))
        cvt (EApp [ECon String
"/", ENum  (Integer, Maybe Int)
a, EReal AlgReal
b])                    = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal (forall a. Num a => Integer -> a
fromInteger (forall a b. (a, b) -> a
fst (Integer, Maybe Int)
a) forall a. Fractional a => a -> a -> a
/             AlgReal
b      )
        cvt (EApp [ECon String
"/", ENum  (Integer, Maybe Int)
a, ENum  (Integer, Maybe Int)
b])                    = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal (forall a. Num a => Integer -> a
fromInteger (forall a b. (a, b) -> a
fst (Integer, Maybe Int)
a) forall a. Fractional a => a -> a -> a
/ forall a. Num a => Integer -> a
fromInteger (forall a b. (a, b) -> a
fst (Integer, Maybe Int)
b))
        cvt (EApp [ECon String
"-", EReal AlgReal
a])                             = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal (-AlgReal
a)
        cvt (EApp [ECon String
"-", ENum (Integer, Maybe Int)
a])                              = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Integer, Maybe Int) -> SExpr
ENum  (-(forall a b. (a, b) -> a
fst (Integer, Maybe Int)
a), 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])                     = forall (m :: * -> *) a. Monad m => a -> m a
return 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 <- 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
                                                                        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal forall a b. (a -> b) -> a -> b
$ Either (Bool, String) (Integer, [(Integer, Integer)]) -> AlgReal
mkPolyReal (forall a b. b -> Either a b
Right (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 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
_) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal forall a b. (a -> b) -> a -> b
$ Either (Bool, String) (Integer, [(Integer, Integer)]) -> AlgReal
mkPolyReal (forall a b. a -> Either a b
Left (Bool
False, forall a. Show a => a -> String
show Integer
s))
                                                  EReal AlgReal
aval  -> case AlgReal
aval of
                                                                   AlgRational Bool
_ Rational
r -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal forall a b. (a -> b) -> a -> b
$ Bool -> Rational -> AlgReal
AlgRational Bool
False Rational
r
                                                                   AlgReal
_               -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal AlgReal
aval
                                                  SExpr
_           -> forall {b}. String -> Either String b
die forall a b. (a -> b) -> a -> b
$ String
"Cannot parse a CVC4 approximate value from: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExpr
x

        -- Deal with CVC5's algebraic reals. This is very crude!
        cvt x :: SExpr
x@(EApp (ECon String
"_" : ECon String
"real_algebraic_number" : [SExpr]
rest)) =
            let isComma :: SExpr -> Bool
isComma (ECon String
",") = Bool
True
                isComma SExpr
_          = Bool
False

                get :: SExpr -> Either String Rational
get (ENum    (Integer
n, Maybe Int
_))               = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n
                get (EReal   (AlgRational Bool
True Rational
r)) = forall (m :: * -> *) a. Monad m => a -> m a
return Rational
r
                get (EFloat  Float
f)                    = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Real a => a -> Rational
toRational Float
f
                get (EDouble Double
d)                    = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Real a => a -> Rational
toRational Double
d
                get SExpr
t                              = forall {b}. String -> Either String b
die forall a b. (a -> b) -> a -> b
$ String
"Cannot get a CVC5 real-algebraic bound from: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExpr
t

            in case forall a. Int -> [a] -> [a]
drop Int
1 (forall a. (a -> Bool) -> [a] -> [a]
dropWhile (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. SExpr -> Bool
isComma) [SExpr]
rest) of
                [EApp [SExpr
n1, SExpr
n2], SExpr
_] -> do Rational
low  <- SExpr -> Either String Rational
get SExpr
n1
                                         Rational
high <- SExpr -> Either String Rational
get SExpr
n2
                                         forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AlgReal -> SExpr
EReal forall a b. (a -> b) -> a -> b
$ RealPoint Rational -> RealPoint Rational -> AlgReal
AlgInterval (forall a. a -> RealPoint a
OpenPoint Rational
low) (forall a. a -> RealPoint a
OpenPoint Rational
high)
                [SExpr]
_                  -> forall {b}. String -> Either String b
die forall a b. (a -> b) -> a -> b
$ String
"Cannot parse a CVC5 real-algebraic number from: " forall a. [a] -> [a] -> [a]
++ 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)])           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat         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)])           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble        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)])           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FP -> SExpr
EFloatingPoint forall a b. (a -> b) -> a -> b
$ Bool -> (Integer, Int) -> (Integer, Int) -> FP
fpFromRawRep (Integer
s forall a. Eq a => a -> a -> Bool
== Integer
1) (Integer
e, Int
eb) (Integer
m, Int
sbforall 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
_)])           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat           forall a. Floating a => a
nan
        cvt (EApp [ECon String
"_",     ECon String
"NaN",       ENum (Integer
11, Maybe Int
_),       ENum (Integer
53,      Maybe Int
_)])           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble          forall a. Floating a => a
nan
        cvt (EApp [ECon String
"_",     ECon String
"NaN",       ENum (Integer
eb, Maybe Int
_),       ENum (Integer
sb,      Maybe Int
_)])           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FP -> SExpr
EFloatingPoint forall a b. (a -> b) -> a -> b
$ Int -> Int -> FP
fpNaN (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
eb) (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
_)])           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat           forall a. Floating a => a
infinity
        cvt (EApp [ECon String
"_",     ECon String
"+oo",       ENum (Integer
11, Maybe Int
_),       ENum (Integer
53,      Maybe Int
_)])           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble          forall a. Floating a => a
infinity
        cvt (EApp [ECon String
"_",     ECon String
"+oo",       ENum (Integer
eb, Maybe Int
_),       ENum (Integer
sb,      Maybe Int
_)])           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FP -> SExpr
EFloatingPoint forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Int -> FP
fpInf Bool
False (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
eb) (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
_)])           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat         forall a b. (a -> b) -> a -> b
$ -forall a. Floating a => a
infinity
        cvt (EApp [ECon String
"_",     ECon String
"-oo",       ENum (Integer
11, Maybe Int
_),       ENum (Integer
53,      Maybe Int
_)])           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble        forall a b. (a -> b) -> a -> b
$ -forall a. Floating a => a
infinity
        cvt (EApp [ECon String
"_",     ECon String
"-oo",       ENum (Integer
eb, Maybe Int
_),       ENum (Integer
sb,      Maybe Int
_)])           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FP -> SExpr
EFloatingPoint forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Int -> FP
fpInf Bool
True (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
eb) (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
_)])           = forall (m :: * -> *) a. Monad m => a -> m a
return 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
_)])           = forall (m :: * -> *) a. Monad m => a -> m a
return 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
_)])           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FP -> SExpr
EFloatingPoint forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Int -> FP
fpZero Bool
False (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
eb) (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
_)])           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat         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
_)])           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble        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
_)])           = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ FP -> SExpr
EFloatingPoint forall a b. (a -> b) -> a -> b
$ Bool -> Int -> Int -> FP
fpZero Bool
True (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
eb) (forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
sb)

        cvt SExpr
x                                                                                        = 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]]) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a, b) -> a
fst (Integer, Maybe Int)
k, 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"        ] ) = forall (m :: * -> *) a. Monad m => a -> m a
return (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] ) = forall (m :: * -> *) a. Monad m => a -> m a
return (    Integer
1, forall a b. (a, b) -> a
fst (Integer, Maybe Int)
p)  --  x^p
        getCoeff (                                        ECon String
"x"          ) = forall (m :: * -> *) a. Monad m => a -> m a
return (    Integer
1,     Integer
1)  --  x
        getCoeff (                ENum (Integer, Maybe Int)
k                                    ) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a, b) -> a
fst (Integer, Maybe Int)
k,     Integer
0)  -- k
        getCoeff SExpr
x = forall {b}. String -> Either String b
die forall a b. (a -> b) -> a -> b
$ String
"Cannot parse a root-obj,\nProcessing term: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExpr
x
        getDouble :: SExpr -> Either String SExpr
getDouble (ECon String
s)  = case (String
s, forall a. (Read a, RealFloat a) => String -> Maybe a
rdFP (forall a. (a -> Bool) -> [a] -> [a]
dropWhile (forall a. Eq a => a -> a -> Bool
== Char
'+') String
s)) of
                                (String
"plusInfinity",  Maybe Double
_     ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble forall a. Floating a => a
infinity
                                (String
"minusInfinity", Maybe Double
_     ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble (-forall a. Floating a => a
infinity)
                                (String
"oo",            Maybe Double
_     ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble forall a. Floating a => a
infinity
                                (String
"-oo",           Maybe Double
_     ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble (-forall a. Floating a => a
infinity)
                                (String
"zero",          Maybe Double
_     ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble Double
0
                                (String
"-zero",         Maybe Double
_     ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble (-Double
0)
                                (String
"NaN",           Maybe Double
_     ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble forall a. Floating a => a
nan
                                (String
_,               Just Double
v) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble Double
v
                                (String, Maybe Double)
_               -> forall {b}. String -> Either String b
die forall a b. (a -> b) -> a -> b
$ String
"Cannot parse a double value from: " 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) = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Double -> SExpr
EDouble forall a b. (a -> b) -> a -> b
$ forall a. RealFloat a => Rational -> a
fromRat forall a b. (a -> b) -> a -> b
$ forall a. Real a => a -> Rational
toRational AlgReal
r
        getDouble SExpr
x         = forall {b}. String -> Either String b
die forall a b. (a -> b) -> a -> b
$ String
"Cannot parse a double value from: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SExpr
x
        getFloat :: SExpr -> Either String SExpr
getFloat (ECon String
s)   = case (String
s, forall a. (Read a, RealFloat a) => String -> Maybe a
rdFP (forall a. (a -> Bool) -> [a] -> [a]
dropWhile (forall a. Eq a => a -> a -> Bool
== Char
'+') String
s)) of
                                (String
"plusInfinity",  Maybe Float
_     ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat forall a. Floating a => a
infinity
                                (String
"minusInfinity", Maybe Float
_     ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat (-forall a. Floating a => a
infinity)
                                (String
"oo",            Maybe Float
_     ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat forall a. Floating a => a
infinity
                                (String
"-oo",           Maybe Float
_     ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat (-forall a. Floating a => a
infinity)
                                (String
"zero",          Maybe Float
_     ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat Float
0
                                (String
"-zero",         Maybe Float
_     ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat (-Float
0)
                                (String
"NaN",           Maybe Float
_     ) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat forall a. Floating a => a
nan
                                (String
_,               Just Float
v) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat Float
v
                                (String, Maybe Float)
_               -> forall {b}. String -> Either String b
die forall a b. (a -> b) -> a -> b
$ String
"Cannot parse a float value from: " forall a. [a] -> [a] -> [a]
++ String
s
        getFloat (EReal AlgReal
r)  = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Float -> SExpr
EFloat forall a b. (a -> b) -> a -> b
$ forall a. RealFloat a => Rational -> a
fromRat forall a b. (a -> b) -> a -> b
$ 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          = forall {b}. String -> Either String b
die forall a b. (a -> b) -> a -> b
$ String
"Cannot parse a float value from: " forall a. [a] -> [a] -> [a]
++ 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 :: forall a. (Read a, RealFloat a) => String -> Maybe a
rdFP String
s = case forall a. (a -> Bool) -> [a] -> ([a], [a])
break (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` String
"pe") String
s of
           (String
m, Char
'p':String
e) -> forall {a}. Read a => String -> Maybe a
rd String
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
m' -> forall {a}. Read a => String -> Maybe a
rd String
e forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
e' -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ a
m' forall a. Num a => a -> a -> a
* ( a
2 forall a. Floating a => a -> a -> a
** a
e')
           (String
m, Char
'e':String
e) -> forall {a}. Read a => String -> Maybe a
rd String
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
m' -> forall {a}. Read a => String -> Maybe a
rd String
e forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \a
e' -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ a
m' forall a. Num a => a -> a -> a
* (a
10 forall a. Floating a => a -> a -> a
** a
e')
           (String
m, String
"")    -> forall {a}. Read a => String -> Maybe a
rd String
m
           (String, String)
_          -> forall a. Maybe a
Nothing
 where rd :: String -> Maybe a
rd String
v = case forall a. Read a => ReadS a
reads String
v of
                [(a
n, String
"")] -> forall a. a -> Maybe a
Just a
n
                [(a, String)]
_         -> 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 forall a. Eq a => a -> a -> Bool
== Integer
1]
        expt :: [Bool]
expt      = [Integer
e forall a. Bits a => a -> Int -> Bool
`testBit` Int
i | Int
i <- [ Int
7,  Int
6 .. Int
0]]
        mantissa :: [Bool]
mantissa  = [Integer
m 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) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
31, Int
30 .. Int
0] ([Bool]
sign forall a. [a] -> [a] -> [a]
++ [Bool]
expt forall a. [a] -> [a] -> [a]
++ [Bool]
mantissa), Bool
b]
        w32 :: Word32
w32       = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> b -> a -> c
flip 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 forall a. Eq a => a -> a -> Bool
== Integer
1]
        expt :: [Bool]
expt      = [Integer
e forall a. Bits a => a -> Int -> Bool
`testBit` Int
i | Int
i <- [Int
10,  Int
9 .. Int
0]]
        mantissa :: [Bool]
mantissa  = [Integer
m 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) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
63, Int
62 .. Int
0] ([Bool]
sign forall a. [a] -> [a] -> [a]
++ [Bool]
expt forall a. [a] -> [a] -> [a]
++ [Bool]
mantissa), Bool
b]
        w64 :: Word64
w64       = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall a b c. (a -> b -> c) -> b -> a -> c
flip 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 = forall a. a -> Maybe a -> a
fromMaybe String
n (forall a. [a] -> Maybe a
listToMaybe [String
to | ([String]
from, String
to) <- [([String], String)]
special, String
n forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
from])
 where special :: [([String], String)]
special = [ ([String
"RNE", String
"roundNearestTiesToEven"], forall a. Show a => a -> String
show RoundingMode
RoundNearestTiesToEven)
                 , ([String
"RNA", String
"roundNearestTiesToAway"], forall a. Show a => a -> String
show RoundingMode
RoundNearestTiesToAway)
                 , ([String
"RTP", String
"roundTowardPositive"],    forall a. Show a => a -> String
show RoundingMode
RoundTowardPositive)
                 , ([String
"RTN", String
"roundTowardNegative"],    forall a. Show a => a -> String
show RoundingMode
RoundTowardNegative)
                 , ([String
"RTZ", String
"roundTowardZero"],        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 = forall a. a -> Maybe a
Just (forall a b. b -> Either a b
Right ([([SExpr], SExpr)], SExpr)
r)
  | Just ([([SExpr], SExpr)], SExpr)
r <- SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
parseSetLambda         SExpr
e = forall a. a -> Maybe a
Just (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 = forall a. a -> Maybe a
Just Either String ([([SExpr], SExpr)], SExpr)
r
  | Bool
True                               = forall a. Maybe a
Nothing         -- out-of luck. NB. This is where we would add support for other solvers!

-- | Parse a set-lambda expression, which is literally a lambda function, that might look like this:
--        (lambda ((x!1 String))
--          (or (not (or (= x!1 "o") (= x!1 "l") (= x!1 "e") (= x!1 "h")))
--              (= x!1 "o")
--              (= x!1 "l")
--              (= x!1 "e")
--              (= x!1 "h")))
--   For this, we do a little bit of an interpretative dance to see if we can "construct" the necesary expression.
--
--   In parsed form:
--      EApp [ECon "lambda",EApp [EApp [ECon "x!1",ECon "String"]],EApp [ECon "not",EApp [ECon "or",EApp [ECon "=",ECon "x!1",ECon "\"e\""],EApp [ECon "=",ECon "x!1",ECon "\"l\""]]]]
--
--   This is by no means comprehensive, and is quite crude, but hopefully covers the cases we see in practice.
parseSetLambda :: SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
parseSetLambda :: SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
parseSetLambda SExpr
funExpr = case SExpr
funExpr of
                               EApp [l :: SExpr
l@(ECon String
"lambda"), bv :: SExpr
bv@(EApp [EApp [ECon String
_, SExpr
_]]), SExpr
body] -> (SExpr -> SExpr) -> SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
go (\SExpr
bd -> [SExpr] -> SExpr
EApp [SExpr
l, SExpr
bv, SExpr
bd]) SExpr
body
                               SExpr
_                                                            -> forall a. Maybe a
Nothing
  where go :: (SExpr -> SExpr) -> SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
go SExpr -> SExpr
mkLambda = SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
build
         where build :: SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
build (EApp [ECon String
"not",  SExpr
rest      ]) =         ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
neg forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<      SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
build SExpr
rest
               build (EApp (ECon String
"or"  : rest :: [SExpr]
rest@(SExpr
_:[SExpr]
_))) = forall {m :: * -> *} {a}. Monad m => (a -> a -> m a) -> [a] -> m a
foldM1 ([([SExpr], SExpr)], SExpr)
-> ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
disj forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
build [SExpr]
rest
               build (EApp (ECon String
"and" : rest :: [SExpr]
rest@(SExpr
_:[SExpr]
_))) = forall {m :: * -> *} {a}. Monad m => (a -> a -> m a) -> [a] -> m a
foldM1 ([([SExpr], SExpr)], SExpr)
-> ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
conj forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
build [SExpr]
rest
               build SExpr
other                            = SExpr -> Maybe ([([SExpr], SExpr)], SExpr)
parseLambdaExpression (SExpr -> SExpr
mkLambda SExpr
other)

        -- We're guaranteed by above construction that foldM1 will never take an empty list (due to rest@(_:_) pattern match.)
        foldM1 :: (a -> a -> m a) -> [a] -> m a
foldM1 a -> a -> m a
_ []     = forall a. HasCallStack => String -> a
error String
"Data.SBV.parseSetLambda: Impossible happened; empty arg to foldM1"
        foldM1 a -> a -> m a
f (a
x:[a]
xs) = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM a -> a -> m a
f a
x [a]
xs

        checkBool :: SExpr -> Bool
checkBool (ENum (Integer
1, Maybe Int
Nothing)) = Bool
True
        checkBool (ENum (Integer
0, Maybe Int
Nothing)) = Bool
True
        checkBool SExpr
_                   = Bool
False

        negBool :: SExpr -> SExpr
negBool (ENum (Integer
1, Maybe Int
Nothing)) = (Integer, Maybe Int) -> SExpr
ENum (Integer
0, forall a. Maybe a
Nothing)
        negBool SExpr
_                   = (Integer, Maybe Int) -> SExpr
ENum (Integer
1, forall a. Maybe a
Nothing)

        orBool :: SExpr -> SExpr -> SExpr
orBool t :: SExpr
t@(ENum (Integer
1, Maybe Int
Nothing)) SExpr
_                      = SExpr
t
        orBool SExpr
_                     t :: SExpr
t@(ENum (Integer
1, Maybe Int
Nothing))  = SExpr
t
        orBool SExpr
_ SExpr
_                                          = (Integer, Maybe Int) -> SExpr
ENum (Integer
0, forall a. Maybe a
Nothing)

        andBool :: SExpr -> SExpr -> SExpr
andBool f :: SExpr
f@(ENum (Integer
0, Maybe Int
Nothing)) SExpr
_                     = SExpr
f
        andBool SExpr
_                     f :: SExpr
f@(ENum (Integer
0, Maybe Int
Nothing)) = SExpr
f
        andBool SExpr
_ SExpr
_                                         = (Integer, Maybe Int) -> SExpr
ENum (Integer
1, forall a. Maybe a
Nothing)

        neg :: ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
        neg :: ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
neg ([([SExpr], SExpr)]
rows, SExpr
dflt)
         | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SExpr -> Bool
checkBool (SExpr
dflt forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [([SExpr], SExpr)]
rows) = forall a. a -> Maybe a
Just ([([SExpr]
e, SExpr -> SExpr
negBool SExpr
r) | ([SExpr]
e, SExpr
r) <- [([SExpr], SExpr)]
rows], SExpr -> SExpr
negBool SExpr
dflt)
         | Bool
True                                = forall a. Maybe a
Nothing

        disj, conj :: ([([SExpr], SExpr)], SExpr) -> ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
        disj :: ([([SExpr], SExpr)], SExpr)
-> ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
disj = (SExpr -> SExpr -> SExpr)
-> ([([SExpr], SExpr)], SExpr)
-> ([([SExpr], SExpr)], SExpr)
-> Maybe ([([SExpr], SExpr)], SExpr)
bin SExpr -> SExpr -> SExpr
orBool
        conj :: ([([SExpr], SExpr)], SExpr)
-> ([([SExpr], SExpr)], SExpr) -> Maybe ([([SExpr], SExpr)], SExpr)
conj = (SExpr -> SExpr -> SExpr)
-> ([([SExpr], SExpr)], SExpr)
-> ([([SExpr], SExpr)], SExpr)
-> Maybe ([([SExpr], SExpr)], SExpr)
bin SExpr -> SExpr -> SExpr
andBool

        bin :: (SExpr -> SExpr -> SExpr)
-> ([([SExpr], SExpr)], SExpr)
-> ([([SExpr], SExpr)], SExpr)
-> Maybe ([([SExpr], SExpr)], SExpr)
bin SExpr -> SExpr -> SExpr
f rd1 :: ([([SExpr], SExpr)], SExpr)
rd1@([([SExpr], SExpr)]
rows1, SExpr
dflt1) rd2 :: ([([SExpr], SExpr)], SExpr)
rd2@([([SExpr], SExpr)]
rows2, SExpr
dflt2)
          | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all SExpr -> Bool
checkBool (SExpr
dflt1 forall a. a -> [a] -> [a]
: SExpr
dflt2 forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [([SExpr], SExpr)]
rows1 forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [([SExpr], SExpr)]
rows2) = forall a. a -> Maybe a
Just (forall {t} {t}.
(Show t, Show t) =>
(t -> t -> SExpr)
-> ([([SExpr], t)], t)
-> ([([SExpr], t)], t)
-> ([([SExpr], SExpr)], SExpr)
combine SExpr -> SExpr -> SExpr
f ([([SExpr], SExpr)], SExpr)
rd1 ([([SExpr], SExpr)], SExpr)
rd2)
          | Bool
True                                                           = forall a. Maybe a
Nothing

        -- Since we don't have equality over SExprs (can of worms!), we use "show" equality here. The ice is thin, but it works!
        combine :: (t -> t -> SExpr)
-> ([([SExpr], t)], t)
-> ([([SExpr], t)], t)
-> ([([SExpr], SExpr)], SExpr)
combine t -> t -> SExpr
f ([([SExpr], t)]
rows1, t
dflt1) ([([SExpr], t)]
rows2, t
dflt2) = ([([SExpr], SExpr)]
rows, t -> t -> SExpr
f t
dflt1 t
dflt2)
          where rows :: [([SExpr], SExpr)]
rows = forall a b. (a -> b) -> [a] -> [b]
map [SExpr] -> ([SExpr], SExpr)
calc forall a b. (a -> b) -> a -> b
$ forall a. (a -> a -> Bool) -> [a] -> [a]
nubBy (\[SExpr]
x [SExpr]
y -> forall a. Show a => a -> String
show [SExpr]
x forall a. Eq a => a -> a -> Bool
== forall a. Show a => a -> String
show [SExpr]
y) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [([SExpr], t)]
rows1 forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [([SExpr], t)]
rows2)

                calc :: [SExpr] -> ([SExpr], SExpr)
                calc :: [SExpr] -> ([SExpr], SExpr)
calc [SExpr]
args = ([SExpr]
args, t -> t -> SExpr
f (forall {a} {a} {p}.
(Show a, Show a, Show p) =>
[(a, p)] -> p -> a -> p
find [([SExpr], t)]
rows1 t
dflt1 [SExpr]
args) (forall {a} {a} {p}.
(Show a, Show a, Show p) =>
[(a, p)] -> p -> a -> p
find [([SExpr], t)]
rows2 t
dflt2 [SExpr]
args))

                find :: [(a, p)] -> p -> a -> p
find [(a, p)]
rs p
d a
a = case [p
r | (a
v, p
r) <- [(a, p)]
rs, forall a. Show a => a -> String
show a
v forall a. Eq a => a -> a -> Bool
== forall a. Show a => a -> String
show a
a] of
                               []  -> p
d
                               [p
x] -> p
x
                               [p]
x   -> forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines [ String
"Data.SBV.parseSetLambda: Impossible happened while combining rows."
                                                      , String
"   First row  :"   forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [([SExpr], t)]
rows1
                                                      , String
"   First dflt :"  forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
dflt1
                                                      , String
"   Second row :"  forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [([SExpr], t)]
rows2
                                                      , String
"   Second dflt:" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show t
dflt2
                                                      , String
"   Looking for: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
a
                                                      , String
"Multiple matches found: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show [p]
x
                                                      ]

-- | 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] -> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM SExpr -> Maybe (String, Bool)
getParam [SExpr]
params forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall a b c. (a -> b -> c) -> b -> a -> c
flip [(String, Bool)] -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
lambda SExpr
body forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= [Either ([SExpr], SExpr) SExpr]
-> Maybe ([([SExpr], SExpr)], SExpr)
chainAssigns
                                  SExpr
_                                       -> forall a. Maybe a
Nothing
  where getParam :: SExpr -> Maybe (String, Bool)
getParam (EApp [ECon String
v, ECon String
ty]) = forall a. a -> Maybe a
Just (String
v, String
ty forall a. Eq a => a -> a -> Bool
== String
"Bool")
        getParam (EApp [ECon String
v, SExpr
_      ]) = forall a. a -> Maybe a
Just (String
v, Bool
False)
        getParam SExpr
_                        = forall a. Maybe a
Nothing

        lambda :: [(String, Bool)]  -- Bool is True if this is a boolean variable. Otherwise we don't keep track of the type
               -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
        lambda :: [(String, Bool)] -> SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
lambda [(String, Bool)]
params SExpr
body = forall a. [a] -> [a]
reverse 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, forall a. Maybe a
Nothing)
                false :: SExpr
false = (Integer, Maybe Int) -> SExpr
ENum (Integer
0, 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 (forall a b. a -> Either a b
Left ([SExpr], SExpr)
sv forall a. a -> [a] -> [a]
: [Either ([SExpr], SExpr) SExpr]
sofar) SExpr
elseBranch
                          Maybe ([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 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 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 (forall a b. a -> Either a b
Left ([SExpr]
s, SExpr
true) 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 = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right SExpr
e 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] = forall a. a -> Maybe a
Just ([SExpr]
s, SExpr
v)
                cond [SExpr]
_ [Either ([SExpr], 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 [] = forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(String, SExpr)]
dict) [String]
paramNames
                   | Bool
True                    = forall a. Maybe a
Nothing
                  where paramNames :: [String]
paramNames = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(String, Bool)]
params

                        -- 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  = 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 forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr SExpr -> Maybe [(String, SExpr)] -> Maybe [(String, SExpr)]
next (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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
paramNames = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ (String
v, SExpr
r) forall a. a -> [a] -> [a]
: [(String, SExpr)]
sofar
                                         | Bool
True                                          = 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]) = forall a. a -> Maybe a
Just (String
v, SExpr
r)
                        grok (EApp [ECon String
"=", SExpr
r, ECon String
v]) = forall a. a -> Maybe a
Just (String
v, SExpr
r)
                        grok (EApp [ECon String
"not", ECon String
v])  = forall a. a -> Maybe a
Just (String
v, SExpr
false) -- boolean negation, require it to be false
                        grok (ECon String
v)                     = case String
v forall a b. Eq a => a -> [(a, b)] -> Maybe b
`lookup` [(String, Bool)]
params of
                                                               Just Bool
True -> forall a. a -> Maybe a
Just (String
v, SExpr
true)  -- boolean identity, require it to be true
                                                               Maybe Bool
_         -> forall a. Maybe a
Nothing

                        -- Tough luck, we couldn't understand:
                        grok 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]) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left String
nm
parseStoreAssociations SExpr
e                                           = forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([Either ([SExpr], SExpr) SExpr]
-> Maybe ([([SExpr], SExpr)], SExpr)
chainAssigns 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]) = forall (m :: * -> *) a. Monad m => a -> m a
return [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]) = forall (m :: * -> *) a. Monad m => a -> m a
return [forall a b. b -> Either a b
Right SExpr
defVal]
          vals (EApp (ECon String
"store" : SExpr
prev : [SExpr]
argsVal)) | forall (t :: * -> *) a. Foldable t => t a -> Int
length [SExpr]
argsVal forall a. Ord a => a -> a -> Bool
>= Int
2             = do [Either ([SExpr], SExpr) SExpr]
rest <- SExpr -> Maybe [Either ([SExpr], SExpr) SExpr]
vals SExpr
prev
                                                                                             forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left (forall a. [a] -> [a]
init [SExpr]
argsVal, forall a. [a] -> a
last [SExpr]
argsVal) forall a. a -> [a] -> [a]
: [Either ([SExpr], SExpr) SExpr]
rest
          vals 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 = forall {b}.
([([SExpr], SExpr)], [b]) -> Maybe ([([SExpr], SExpr)], b)
regroup forall a b. (a -> b) -> a -> b
$ 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]) = forall a. a -> Maybe a
Just ([([SExpr], SExpr)] -> [([SExpr], SExpr)]
checkDup [([SExpr], SExpr)]
vs, b
d)
        regroup ([([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 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
          | forall (t :: * -> *) a. Foldable t => t a -> Int
length [SExpr]
as forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [SExpr]
bs = forall (t :: * -> *). Foldable t => t Bool -> Bool
and forall a b. (a -> b) -> a -> b
$ forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith SExpr -> SExpr -> Bool
same [SExpr]
as [SExpr]
bs
          | Bool
True                   = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: Differing length of key received in chainAssigns: " forall a. [a] -> [a] -> [a]
++ 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 forall a. Eq a => a -> a -> Bool
== String
b
                     (ENum (Integer
i, Maybe Int
_), ENum (Integer
j, Maybe Int
_))  -> Integer
i 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)   -> forall a. RealFloat a => a -> a -> Bool
fpIsEqualObjectH Float
f1 Float
f2
                     (EDouble Double
d1,  EDouble Double
d2)   -> forall a. RealFloat a => a -> a -> Bool
fpIsEqualObjectH Double
d1 Double
d2
                     (EApp [SExpr]
as,     EApp [SExpr]
bs)      -> forall (t :: * -> *) a. Foldable t => t a -> Int
length [SExpr]
as forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [SExpr]
bs Bool -> Bool -> Bool
&& forall (t :: * -> *). Foldable t => t Bool -> Bool
and (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 forall a. Eq a => a -> a -> Bool
== SExpr -> Int
eRank SExpr
e2
                                                    then forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Data.SBV: You've found a bug in SBV! Please report: SExpr(same): " forall a. [a] -> [a] -> [a]
++ 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) #-}