{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE LiberalTypeSynonyms #-}

module Language.Hasmtlib.Internal.Parser where

import Prelude hiding (not, (&&), (||), and , or)
import Language.Hasmtlib.Internal.Render
import Language.Hasmtlib.Boolean
import Language.Hasmtlib.Codec
import Language.Hasmtlib.Type.Value
import Language.Hasmtlib.Type.Bitvec
import Language.Hasmtlib.Type.SMTSort
import Language.Hasmtlib.Type.Solution
import Language.Hasmtlib.Type.ArrayMap
import Language.Hasmtlib.Type.Expr
import Data.Some.Constraint
import Data.Bit
import Data.Coerce
import Data.Proxy
import Data.Ratio ((%))
import Data.ByteString hiding (filter, foldl)
import Data.ByteString.Builder
import Data.Attoparsec.ByteString hiding (Result, skipWhile, takeTill)
import Data.Attoparsec.ByteString.Char8 hiding (Result)
import Data.Text.Encoding (decodeUtf8)
import qualified Data.Text as Text
import Control.Applicative
import Control.Lens hiding (op)
import GHC.TypeNats

answerParser :: Parser (Result, Solution)
answerParser :: Parser (Result, Solution)
answerParser = do
  Result
result  <- Parser Result
resultParser
  Solution
model   <- Parser Solution
anyModelParser

  (Result, Solution) -> Parser (Result, Solution)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Result
result, Solution
model)

resultParser :: Parser Result
resultParser :: Parser Result
resultParser = (ByteString -> Parser ByteString
string ByteString
"sat" Parser ByteString -> Parser Result -> Parser Result
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Result -> Parser Result
forall a. a -> Parser ByteString a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Result
Sat)
           Parser Result -> Parser Result -> Parser Result
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (ByteString -> Parser ByteString
string ByteString
"unsat" Parser ByteString -> Parser Result -> Parser Result
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Result -> Parser Result
forall a. a -> Parser ByteString a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Result
Unsat)
           Parser Result -> Parser Result -> Parser Result
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (ByteString -> Parser ByteString
string ByteString
"unknown" Parser ByteString -> Parser Result -> Parser Result
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Result -> Parser Result
forall a. a -> Parser ByteString a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Result
Unknown)

anyModelParser :: Parser Solution
anyModelParser :: Parser Solution
anyModelParser = Parser Solution
smt2ModelParser Parser Solution -> Parser Solution -> Parser Solution
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Solution
defaultModelParser Parser Solution -> Parser Solution -> Parser Solution
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Solution -> Parser Solution
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return Solution
forall a. Monoid a => a
mempty

-- For the format CVC5 and Z3 use - what is it called?
defaultModelParser :: Parser Solution
defaultModelParser :: Parser Solution
defaultModelParser = do
  ()
_       <- Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
'(' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  [SomeKnownOrdSMTSort SMTVarSol]
varSols <- Parser ByteString (SomeKnownOrdSMTSort SMTVarSol)
-> Parser ByteString [SomeKnownOrdSMTSort SMTVarSol]
forall a. Parser ByteString a -> Parser ByteString [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (Parser ByteString (SomeKnownOrdSMTSort SMTVarSol)
 -> Parser ByteString [SomeKnownOrdSMTSort SMTVarSol])
-> Parser ByteString (SomeKnownOrdSMTSort SMTVarSol)
-> Parser ByteString [SomeKnownOrdSMTSort SMTVarSol]
forall a b. (a -> b) -> a -> b
$ Parser ByteString (SomeKnownOrdSMTSort SMTVarSol)
parseSomeSol Parser ByteString (SomeKnownOrdSMTSort SMTVarSol)
-> Parser () -> Parser ByteString (SomeKnownOrdSMTSort SMTVarSol)
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
skipSpace
  ()
_       <- (Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
')' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace) Parser () -> Parser () -> Parser ()
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ()
skipSpace

  Solution -> Parser Solution
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Solution -> Parser Solution) -> Solution -> Parser Solution
forall a b. (a -> b) -> a -> b
$ [SomeKnownOrdSMTSort SMTVarSol] -> Solution
fromSomeVarSols [SomeKnownOrdSMTSort SMTVarSol]
varSols

smt2ModelParser :: Parser Solution
smt2ModelParser :: Parser Solution
smt2ModelParser = do
  ()
_       <- Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
'(' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace Parser () -> Parser ByteString -> Parser ByteString
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ByteString -> Parser ByteString
string ByteString
"model" Parser ByteString -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  [SomeKnownOrdSMTSort SMTVarSol]
varSols <- Parser ByteString (SomeKnownOrdSMTSort SMTVarSol)
-> Parser ByteString [SomeKnownOrdSMTSort SMTVarSol]
forall a. Parser ByteString a -> Parser ByteString [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (Parser ByteString (SomeKnownOrdSMTSort SMTVarSol)
 -> Parser ByteString [SomeKnownOrdSMTSort SMTVarSol])
-> Parser ByteString (SomeKnownOrdSMTSort SMTVarSol)
-> Parser ByteString [SomeKnownOrdSMTSort SMTVarSol]
forall a b. (a -> b) -> a -> b
$ Parser ByteString (SomeKnownOrdSMTSort SMTVarSol)
parseSomeSol Parser ByteString (SomeKnownOrdSMTSort SMTVarSol)
-> Parser () -> Parser ByteString (SomeKnownOrdSMTSort SMTVarSol)
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
skipSpace
  ()
_       <- (Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
')' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace) Parser () -> Parser () -> Parser ()
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ()
skipSpace

  Solution -> Parser Solution
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Solution -> Parser Solution) -> Solution -> Parser Solution
forall a b. (a -> b) -> a -> b
$ [SomeKnownOrdSMTSort SMTVarSol] -> Solution
fromSomeVarSols [SomeKnownOrdSMTSort SMTVarSol]
varSols

parseSomeSol :: Parser (SomeKnownOrdSMTSort SMTVarSol)
parseSomeSol :: Parser ByteString (SomeKnownOrdSMTSort SMTVarSol)
parseSomeSol = do
  ()
_     <- Char -> Parser ByteString Char
char Char
'(' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  ()
_     <- ByteString -> Parser ByteString
string ByteString
"define-fun" Parser ByteString -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  ByteString
_     <- ByteString -> Parser ByteString
string ByteString
"var_"
  Int
vId   <- forall a. Integral a => Parser a
decimal @Int
  ()
_     <- Parser ()
skipSpace Parser () -> Parser ByteString -> Parser ByteString
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ByteString -> Parser ByteString
string ByteString
"()" Parser ByteString -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  (Some1 f a
someSort) <- Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
parseSomeSort
  ()
_     <- Parser ()
skipSpace
  Expr a
expr  <- f a -> Parser (Expr a)
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> Parser (Expr t)
parseExpr' f a
someSort
  Char
_     <- Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
')'
  case Solution -> Expr a -> Maybe (Decoded (Expr a))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
forall a. Monoid a => a
mempty Expr a
expr of
    Maybe (Decoded (Expr a))
Nothing    -> [Char] -> Parser ByteString (SomeKnownOrdSMTSort SMTVarSol)
forall a. [Char] -> Parser ByteString a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char] -> Parser ByteString (SomeKnownOrdSMTSort SMTVarSol))
-> [Char] -> Parser ByteString (SomeKnownOrdSMTSort SMTVarSol)
forall a b. (a -> b) -> a -> b
$ [Char]
"Solver reponded with solution for var_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show Int
vId [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" but it contains "
                      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"another var. This cannot be parsed and evaluated currently."
    Just Decoded (Expr a)
value -> SomeKnownOrdSMTSort SMTVarSol
-> Parser ByteString (SomeKnownOrdSMTSort SMTVarSol)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeKnownOrdSMTSort SMTVarSol
 -> Parser ByteString (SomeKnownOrdSMTSort SMTVarSol))
-> SomeKnownOrdSMTSort SMTVarSol
-> Parser ByteString (SomeKnownOrdSMTSort SMTVarSol)
forall a b. (a -> b) -> a -> b
$ SMTVarSol a -> SomeKnownOrdSMTSort SMTVarSol
forall k (csf :: [(k -> *) -> Constraint])
       (csa :: [k -> Constraint]) (f :: k -> *) (a :: k).
(AllC csf f, AllC csa a) =>
f a -> Somes1 csf csa
Some1 (SMTVarSol a -> SomeKnownOrdSMTSort SMTVarSol)
-> SMTVarSol a -> SomeKnownOrdSMTSort SMTVarSol
forall a b. (a -> b) -> a -> b
$ SMTVar a -> Value a -> SMTVarSol a
forall (t :: SMTSort). SMTVar t -> Value t -> SMTVarSol t
SMTVarSol (Int -> SMTVar a
forall a b. Coercible a b => a -> b
coerce Int
vId) (HaskellType a -> Value a
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue HaskellType a
Decoded (Expr a)
value)
{-# INLINEABLE parseSomeSol #-}

parseSomeSort :: Parser (SomeKnownOrdSMTSort SSMTSort)
parseSomeSort :: Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
parseSomeSort = (ByteString -> Parser ByteString
string ByteString
"Bool" Parser ByteString
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
forall a. a -> Parser ByteString a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SSMTSort 'BoolSort
-> Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]
forall k (csf :: [(k -> *) -> Constraint])
       (csa :: [k -> Constraint]) (f :: k -> *) (a :: k).
(AllC csf f, AllC csa a) =>
f a -> Somes1 csf csa
Some1 SSMTSort 'BoolSort
SBoolSort))
        Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (ByteString -> Parser ByteString
string ByteString
"Int"  Parser ByteString
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
forall a. a -> Parser ByteString a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SSMTSort 'IntSort
-> Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]
forall k (csf :: [(k -> *) -> Constraint])
       (csa :: [k -> Constraint]) (f :: k -> *) (a :: k).
(AllC csf f, AllC csa a) =>
f a -> Somes1 csf csa
Some1 SSMTSort 'IntSort
SIntSort))
        Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (ByteString -> Parser ByteString
string ByteString
"Real" Parser ByteString
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
forall a. a -> Parser ByteString a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SSMTSort 'RealSort
-> Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]
forall k (csf :: [(k -> *) -> Constraint])
       (csa :: [k -> Constraint]) (f :: k -> *) (a :: k).
(AllC csf f, AllC csa a) =>
f a -> Somes1 csf csa
Some1 SSMTSort 'RealSort
SRealSort))
        Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
parseSomeBitVecSort
        Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
parseSomeArraySort
        Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (ByteString -> Parser ByteString
string ByteString
"String" Parser ByteString
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
forall a. a -> Parser ByteString a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SSMTSort 'StringSort
-> Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]
forall k (csf :: [(k -> *) -> Constraint])
       (csa :: [k -> Constraint]) (f :: k -> *) (a :: k).
(AllC csf f, AllC csa a) =>
f a -> Somes1 csf csa
Some1 SSMTSort 'StringSort
SStringSort))
{-# INLINEABLE parseSomeSort #-}

parseSomeBitVecSort :: Parser (SomeKnownOrdSMTSort SSMTSort)
parseSomeBitVecSort :: Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
parseSomeBitVecSort = do
  ()
_ <- Char -> Parser ByteString Char
char Char
'(' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
'_' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  ()
_ <- ByteString -> Parser ByteString
string ByteString
"BitVec" Parser ByteString -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  Integer
n <- Parser Integer
forall a. Integral a => Parser a
decimal
  Char
_ <- Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
')'
  case Natural -> SomeNat
someNatVal (Natural -> SomeNat) -> Natural -> SomeNat
forall a b. (a -> b) -> a -> b
$ Integer -> Natural
forall a. Num a => Integer -> a
fromInteger Integer
n of
    -- SMTLib does not differentiate between signed and unsigned BitVec on the type-level
    -- We do. So we always just put Unsigned here and in Codec (Expr t)
    -- if (t ~ BvSort Signed _) we retrieve unsigned solution and flip type-level encoding
    SomeNat Proxy n
pn -> Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]
 -> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]))
-> Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
forall a b. (a -> b) -> a -> b
$ SSMTSort ('BvSort 'Unsigned n)
-> Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]
forall k (csf :: [(k -> *) -> Constraint])
       (csa :: [k -> Constraint]) (f :: k -> *) (a :: k).
(AllC csf f, AllC csa a) =>
f a -> Somes1 csf csa
Some1 (SSMTSort ('BvSort 'Unsigned n)
 -> Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
-> SSMTSort ('BvSort 'Unsigned n)
-> Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]
forall a b. (a -> b) -> a -> b
$ Proxy 'Unsigned -> Proxy n -> SSMTSort ('BvSort 'Unsigned n)
forall (enc :: BvEnc) (n :: Natural).
(KnownBvEnc enc, KnownNat n) =>
Proxy enc -> Proxy n -> SSMTSort ('BvSort enc n)
SBvSort (forall {k} (t :: k). Proxy t
forall (t :: BvEnc). Proxy t
Proxy @Unsigned) Proxy n
pn
{-# INLINEABLE parseSomeBitVecSort #-}

parseSomeArraySort :: Parser (SomeKnownOrdSMTSort SSMTSort)
parseSomeArraySort :: Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
parseSomeArraySort = do
  ()
_ <- Char -> Parser ByteString Char
char Char
'(' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  ()
_ <- ByteString -> Parser ByteString
string ByteString
"Array" Parser ByteString -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  (Some1 f a
keySort)   <- Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
parseSomeSort
  ()
_ <- Parser ()
skipSpace
  (Some1 f a
valueSort) <- Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
parseSomeSort
  Char
_ <- Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
')'
  Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]
 -> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]))
-> Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]
-> Parser (Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
forall a b. (a -> b) -> a -> b
$ SSMTSort ('ArraySort a a)
-> Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]
forall k (csf :: [(k -> *) -> Constraint])
       (csa :: [k -> Constraint]) (f :: k -> *) (a :: k).
(AllC csf f, AllC csa a) =>
f a -> Somes1 csf csa
Some1 (SSMTSort ('ArraySort a a)
 -> Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType])
-> SSMTSort ('ArraySort a a)
-> Somes1 '[(~) SSMTSort] '[KnownSMTSort, OrdHaskellType]
forall a b. (a -> b) -> a -> b
$ Proxy a -> Proxy a -> SSMTSort ('ArraySort a a)
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k),
 Ord (HaskellType v)) =>
Proxy k -> Proxy v -> SSMTSort ('ArraySort k v)
SArraySort (SSMTSort a -> Proxy a
forall (t :: SMTSort). SSMTSort t -> Proxy t
goProxy f a
SSMTSort a
keySort) (SSMTSort a -> Proxy a
forall (t :: SMTSort). SSMTSort t -> Proxy t
goProxy f a
SSMTSort a
valueSort)
    where
      goProxy :: forall t. SSMTSort t -> Proxy t
      goProxy :: forall (t :: SMTSort). SSMTSort t -> Proxy t
goProxy SSMTSort t
_ = forall {k} (t :: k). Proxy t
forall (t :: SMTSort). Proxy t
Proxy @t
{-# INLINEABLE parseSomeArraySort #-}

parseExpr' :: forall prxy t. KnownSMTSort t => prxy t -> Parser (Expr t)
parseExpr' :: forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> Parser (Expr t)
parseExpr' prxy t
_ = forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr @t
{-# INLINE parseExpr' #-}

-- TODO: Add parseSelect
parseExpr :: forall t. KnownSMTSort t => Parser (Expr t)
parseExpr :: forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr = Parser (Expr t)
forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
var Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser (Expr t)
forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
constantExpr Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'BoolSort -> Expr t -> Expr t -> Expr t)
-> Parser (Expr t)
forall (t :: SMTSort) (u :: SMTSort) (v :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u, KnownSMTSort v) =>
ByteString
-> (Expr t -> Expr u -> Expr v -> Expr r) -> Parser (Expr r)
ternary ByteString
"ite" (forall b a. Iteable b a => b -> a -> a -> a
ite @(Expr BoolSort))
        Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> case forall (t :: SMTSort). KnownSMTSort t => SSMTSort t
sortSing @t of
              SSMTSort t
SIntSort  -> ByteString
-> (Expr 'IntSort -> Expr 'IntSort) -> Parser (Expr 'IntSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"abs" Expr 'IntSort -> Expr 'IntSort
forall a. Num a => a -> a
abs Parser (Expr 'IntSort)
-> Parser (Expr 'IntSort) -> Parser (Expr 'IntSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'IntSort -> Expr 'IntSort) -> Parser (Expr 'IntSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary  ByteString
"-" Expr 'IntSort -> Expr 'IntSort
forall a. Num a => a -> a
negate
                      Parser (Expr 'IntSort)
-> Parser (Expr 'IntSort) -> Parser (Expr 'IntSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> ([Expr 'IntSort] -> Expr 'IntSort) -> Parser (Expr 'IntSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
nary ByteString
"+" [Expr 'IntSort] -> Expr 'IntSort
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum  Parser (Expr 'IntSort)
-> Parser (Expr 'IntSort) -> Parser (Expr 'IntSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort)
-> Parser (Expr 'IntSort)
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"-" (-) Parser (Expr 'IntSort)
-> Parser (Expr 'IntSort) -> Parser (Expr 'IntSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> ([Expr 'IntSort] -> Expr 'IntSort) -> Parser (Expr 'IntSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
nary ByteString
"*" [Expr 'IntSort] -> Expr 'IntSort
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product Parser (Expr 'IntSort)
-> Parser (Expr 'IntSort) -> Parser (Expr 'IntSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort)
-> Parser (Expr 'IntSort)
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"mod" Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
forall (t :: SMTSort).
Integral (HaskellType t) =>
Expr t -> Expr t -> Expr t
Mod
                      Parser (Expr 'IntSort)
-> Parser (Expr 'IntSort) -> Parser (Expr 'IntSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'RealSort -> Expr 'IntSort) -> Parser (Expr 'IntSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"to_int" Expr 'RealSort -> Expr 'IntSort
toIntSort Parser (Expr 'IntSort)
-> Parser (Expr 'IntSort) -> Parser (Expr 'IntSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'StringSort -> Expr 'IntSort) -> Parser (Expr 'IntSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"str.len" Expr 'StringSort -> Expr 'IntSort
strLength
                      Parser (Expr 'IntSort)
-> Parser (Expr 'IntSort) -> Parser (Expr 'IntSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'StringSort
    -> Expr 'StringSort -> Expr 'IntSort -> Expr 'IntSort)
-> Parser (Expr 'IntSort)
forall (t :: SMTSort) (u :: SMTSort) (v :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u, KnownSMTSort v) =>
ByteString
-> (Expr t -> Expr u -> Expr v -> Expr r) -> Parser (Expr r)
ternary ByteString
"str.indexof" Expr 'StringSort
-> Expr 'StringSort -> Expr 'IntSort -> Expr 'IntSort
strIndexOf
              SSMTSort t
SRealSort -> ByteString
-> (Expr 'RealSort -> Expr 'RealSort) -> Parser (Expr 'RealSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"abs" Expr 'RealSort -> Expr 'RealSort
forall a. Num a => a -> a
abs Parser (Expr 'RealSort)
-> Parser (Expr 'RealSort) -> Parser (Expr 'RealSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'RealSort -> Expr 'RealSort) -> Parser (Expr 'RealSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary  ByteString
"-" Expr 'RealSort -> Expr 'RealSort
forall a. Num a => a -> a
negate
                      Parser (Expr 'RealSort)
-> Parser (Expr 'RealSort) -> Parser (Expr 'RealSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> ([Expr 'RealSort] -> Expr 'RealSort) -> Parser (Expr 'RealSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
nary ByteString
"+" [Expr 'RealSort] -> Expr 'RealSort
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum  Parser (Expr 'RealSort)
-> Parser (Expr 'RealSort) -> Parser (Expr 'RealSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort)
-> Parser (Expr 'RealSort)
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"-" (-) Parser (Expr 'RealSort)
-> Parser (Expr 'RealSort) -> Parser (Expr 'RealSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> ([Expr 'RealSort] -> Expr 'RealSort) -> Parser (Expr 'RealSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
nary ByteString
"*" [Expr 'RealSort] -> Expr 'RealSort
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product Parser (Expr 'RealSort)
-> Parser (Expr 'RealSort) -> Parser (Expr 'RealSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort)
-> Parser (Expr 'RealSort)
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"/" Expr 'RealSort -> Expr 'RealSort -> Expr 'RealSort
forall a. Fractional a => a -> a -> a
(/)
                      Parser (Expr 'RealSort)
-> Parser (Expr 'RealSort) -> Parser (Expr 'RealSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'IntSort -> Expr 'RealSort) -> Parser (Expr 'RealSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"to_real" Expr 'IntSort -> Expr 'RealSort
toRealSort
                      Parser (Expr 'RealSort)
-> Parser (Expr 'RealSort) -> Parser (Expr 'RealSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser (Expr 'RealSort)
smtPi Parser (Expr 'RealSort)
-> Parser (Expr 'RealSort) -> Parser (Expr 'RealSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'RealSort -> Expr 'RealSort) -> Parser (Expr 'RealSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"sqrt" Expr 'RealSort -> Expr 'RealSort
forall a. Floating a => a -> a
sqrt Parser (Expr 'RealSort)
-> Parser (Expr 'RealSort) -> Parser (Expr 'RealSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'RealSort -> Expr 'RealSort) -> Parser (Expr 'RealSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"exp" Expr 'RealSort -> Expr 'RealSort
forall a. Floating a => a -> a
exp
                      Parser (Expr 'RealSort)
-> Parser (Expr 'RealSort) -> Parser (Expr 'RealSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'RealSort -> Expr 'RealSort) -> Parser (Expr 'RealSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"sin" Expr 'RealSort -> Expr 'RealSort
forall a. Floating a => a -> a
sin Parser (Expr 'RealSort)
-> Parser (Expr 'RealSort) -> Parser (Expr 'RealSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'RealSort -> Expr 'RealSort) -> Parser (Expr 'RealSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"cos" Expr 'RealSort -> Expr 'RealSort
forall a. Floating a => a -> a
cos Parser (Expr 'RealSort)
-> Parser (Expr 'RealSort) -> Parser (Expr 'RealSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'RealSort -> Expr 'RealSort) -> Parser (Expr 'RealSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"tan" Expr 'RealSort -> Expr 'RealSort
forall a. Floating a => a -> a
tan
                      Parser (Expr 'RealSort)
-> Parser (Expr 'RealSort) -> Parser (Expr 'RealSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'RealSort -> Expr 'RealSort) -> Parser (Expr 'RealSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"arcsin" Expr 'RealSort -> Expr 'RealSort
forall a. Floating a => a -> a
asin Parser (Expr 'RealSort)
-> Parser (Expr 'RealSort) -> Parser (Expr 'RealSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'RealSort -> Expr 'RealSort) -> Parser (Expr 'RealSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"arccos" Expr 'RealSort -> Expr 'RealSort
forall a. Floating a => a -> a
acos Parser (Expr 'RealSort)
-> Parser (Expr 'RealSort) -> Parser (Expr 'RealSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'RealSort -> Expr 'RealSort) -> Parser (Expr 'RealSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"arctan" Expr 'RealSort -> Expr 'RealSort
forall a. Floating a => a -> a
atan
              SSMTSort t
SBoolSort -> ByteString
-> (Expr 'BoolSort -> Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"not" Expr 'BoolSort -> Expr 'BoolSort
forall b. Boolean b => b -> b
not
                      Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> ([Expr 'BoolSort] -> Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
nary ByteString
"and" [Expr 'BoolSort] -> Expr 'BoolSort
forall (t :: * -> *) b. (Foldable t, Boolean b) => t b -> b
and  Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> ([Expr 'BoolSort] -> Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
nary ByteString
"or" [Expr 'BoolSort] -> Expr 'BoolSort
forall (t :: * -> *) b. (Foldable t, Boolean b) => t b -> b
or Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort)
-> Parser (Expr 'BoolSort)
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"=>" Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
forall b. Boolean b => b -> b -> b
(==>) Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort)
-> Parser (Expr 'BoolSort)
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"xor" Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
forall b. Boolean b => b -> b -> b
xor
                      Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary @IntSort  ByteString
"=" Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
(===) Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary @IntSort  ByteString
"distinct" Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
(/==)
                      Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary @RealSort ByteString
"=" Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
(===) Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary @RealSort ByteString
"distinct" Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
(/==)
                      Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary @BoolSort ByteString
"=" Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
(===) Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary @BoolSort ByteString
"distinct" Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
(/==)
                      Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary @IntSort ByteString
"<" Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(<?) Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary @IntSort ByteString
"<=" Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(<=?)
                      Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary @IntSort ByteString
">=" Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(>=?) Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary @IntSort ByteString
">" Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(>?)
                      Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary @RealSort ByteString
"<" Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(<?) Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary @RealSort ByteString
"<=" Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(<=?)
                      Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary @RealSort ByteString
">=" Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(>=?) Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary @RealSort ByteString
">" Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(>?)
                      Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary @StringSort ByteString
"str.<" Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(<?) Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary @StringSort ByteString
"str.<=" Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(<=?)
                      Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'RealSort -> Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"is_int" Expr 'RealSort -> Expr 'BoolSort
isIntSort
                      Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort)
-> Parser (Expr 'BoolSort)
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"str.prefixof" Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
strPrefixOf Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort)
-> Parser (Expr 'BoolSort)
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"str.suffixof" Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
strSuffixOf
                      Parser (Expr 'BoolSort)
-> Parser (Expr 'BoolSort) -> Parser (Expr 'BoolSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort)
-> Parser (Expr 'BoolSort)
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"str.contains" Expr 'StringSort -> Expr 'StringSort -> Expr 'BoolSort
strContains
                      -- TODO: Add compare ops for all (?) bv-sorts
              SBvSort Proxy enc
enc Proxy n
_ -> ByteString
-> (Expr ('BvSort enc n) -> Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n))
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"bvnot" Expr ('BvSort enc n) -> Expr ('BvSort enc n)
forall b. Boolean b => b -> b
not
                      Parser (Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n)) -> Parser (Expr ('BvSort enc n))
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr ('BvSort enc n)
    -> Expr ('BvSort enc n) -> Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n))
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"bvand" Expr ('BvSort enc n)
-> Expr ('BvSort enc n) -> Expr ('BvSort enc n)
forall b. Boolean b => b -> b -> b
(&&)  Parser (Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n)) -> Parser (Expr ('BvSort enc n))
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr ('BvSort enc n)
    -> Expr ('BvSort enc n) -> Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n))
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"bvor" Expr ('BvSort enc n)
-> Expr ('BvSort enc n) -> Expr ('BvSort enc n)
forall b. Boolean b => b -> b -> b
(||) Parser (Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n)) -> Parser (Expr ('BvSort enc n))
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr ('BvSort enc n)
    -> Expr ('BvSort enc n) -> Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n))
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"bvxor" Expr ('BvSort enc n)
-> Expr ('BvSort enc n) -> Expr ('BvSort enc n)
forall b. Boolean b => b -> b -> b
xor Parser (Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n)) -> Parser (Expr ('BvSort enc n))
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr ('BvSort enc n)
    -> Expr ('BvSort enc n) -> Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n))
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"bvnand" Expr ('BvSort enc n)
-> Expr ('BvSort enc n) -> Expr ('BvSort enc n)
forall (enc :: BvEnc) (n :: Natural).
(KnownBvEnc enc, KnownNat n) =>
Expr ('BvSort enc n)
-> Expr ('BvSort enc n) -> Expr ('BvSort enc n)
BvNand Parser (Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n)) -> Parser (Expr ('BvSort enc n))
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr ('BvSort enc n)
    -> Expr ('BvSort enc n) -> Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n))
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"bvnor" Expr ('BvSort enc n)
-> Expr ('BvSort enc n) -> Expr ('BvSort enc n)
forall (enc :: BvEnc) (n :: Natural).
(KnownBvEnc enc, KnownNat n) =>
Expr ('BvSort enc n)
-> Expr ('BvSort enc n) -> Expr ('BvSort enc n)
BvNor
                      Parser (Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n)) -> Parser (Expr ('BvSort enc n))
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr ('BvSort enc n) -> Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n))
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary  ByteString
"bvneg" Expr ('BvSort enc n) -> Expr ('BvSort enc n)
forall a. Num a => a -> a
negate
                      Parser (Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n)) -> Parser (Expr ('BvSort enc n))
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr ('BvSort enc n)
    -> Expr ('BvSort enc n) -> Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n))
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"bvadd" Expr ('BvSort enc n)
-> Expr ('BvSort enc n) -> Expr ('BvSort enc n)
forall a. Num a => a -> a -> a
(+)  Parser (Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n)) -> Parser (Expr ('BvSort enc n))
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr ('BvSort enc n)
    -> Expr ('BvSort enc n) -> Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n))
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"bvsub" (-) Parser (Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n)) -> Parser (Expr ('BvSort enc n))
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr ('BvSort enc n)
    -> Expr ('BvSort enc n) -> Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n))
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"bvmul" Expr ('BvSort enc n)
-> Expr ('BvSort enc n) -> Expr ('BvSort enc n)
forall a. Num a => a -> a -> a
(*)
                      Parser (Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n)) -> Parser (Expr ('BvSort enc n))
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr ('BvSort enc n)
    -> Expr ('BvSort enc n) -> Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n))
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"bvudiv" Expr ('BvSort enc n)
-> Expr ('BvSort enc n) -> Expr ('BvSort enc n)
forall a. Integral a => a -> a -> a
div Parser (Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n)) -> Parser (Expr ('BvSort enc n))
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr ('BvSort enc n)
    -> Expr ('BvSort enc n) -> Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n))
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"bvurem" Expr ('BvSort enc n)
-> Expr ('BvSort enc n) -> Expr ('BvSort enc n)
forall a. Integral a => a -> a -> a
rem
                      Parser (Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n)) -> Parser (Expr ('BvSort enc n))
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr ('BvSort enc n)
    -> Expr ('BvSort enc n) -> Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n))
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"bvshl" Expr ('BvSort enc n)
-> Expr ('BvSort enc n) -> Expr ('BvSort enc n)
forall (enc :: BvEnc) (n :: Natural).
(KnownBvEnc enc, KnownNat n) =>
Expr ('BvSort enc n)
-> Expr ('BvSort enc n) -> Expr ('BvSort enc n)
BvShL
                      Parser (Expr ('BvSort enc n))
-> Parser (Expr ('BvSort enc n)) -> Parser (Expr ('BvSort enc n))
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> case Proxy enc -> SBvEnc enc
forall (enc :: BvEnc) (prxy :: BvEnc -> *).
KnownBvEnc enc =>
prxy enc -> SBvEnc enc
bvEncSing' Proxy enc
enc of SBvEnc enc
SUnsigned -> ByteString
-> (Expr ('BvSort 'Unsigned n)
    -> Expr ('BvSort 'Unsigned n) -> Expr ('BvSort 'Unsigned n))
-> Parser (Expr ('BvSort 'Unsigned n))
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"bvlshr" Expr ('BvSort 'Unsigned n)
-> Expr ('BvSort 'Unsigned n) -> Expr ('BvSort 'Unsigned n)
forall (n :: Natural).
KnownNat n =>
Expr ('BvSort 'Unsigned n)
-> Expr ('BvSort 'Unsigned n) -> Expr ('BvSort 'Unsigned n)
BvLShR ; SBvEnc enc
SSigned -> ByteString
-> (Expr ('BvSort 'Signed n)
    -> Expr ('BvSort 'Signed n) -> Expr ('BvSort 'Signed n))
-> Parser (Expr ('BvSort 'Signed n))
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"bvashr" Expr ('BvSort 'Signed n)
-> Expr ('BvSort 'Signed n) -> Expr ('BvSort 'Signed n)
forall (n :: Natural).
KnownNat n =>
Expr ('BvSort 'Signed n)
-> Expr ('BvSort 'Signed n) -> Expr ('BvSort 'Signed n)
BvAShR
              SArraySort Proxy k
_ Proxy v
_ -> ByteString
-> (Expr ('ArraySort k v)
    -> Expr k -> Expr v -> Expr ('ArraySort k v))
-> Parser (Expr ('ArraySort k v))
forall (t :: SMTSort) (u :: SMTSort) (v :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u, KnownSMTSort v) =>
ByteString
-> (Expr t -> Expr u -> Expr v -> Expr r) -> Parser (Expr r)
ternary ByteString
"store" Expr ('ArraySort k v) -> Expr k -> Expr v -> Expr ('ArraySort k v)
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
Expr ('ArraySort k v) -> Expr k -> Expr v -> Expr ('ArraySort k v)
ArrStore
                      -- TODO: Add compare ops for all (?) array-sorts
              SSMTSort t
SStringSort -> ByteString
-> (Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort)
-> Parser (Expr 'StringSort)
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"str.++" Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
forall a. Semigroup a => a -> a -> a
(<>) Parser (Expr 'StringSort)
-> Parser (Expr 'StringSort) -> Parser (Expr 'StringSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'StringSort -> Expr 'IntSort -> Expr 'StringSort)
-> Parser (Expr 'StringSort)
forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
"str.at" Expr 'StringSort -> Expr 'IntSort -> Expr 'StringSort
strAt Parser (Expr 'StringSort)
-> Parser (Expr 'StringSort) -> Parser (Expr 'StringSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'StringSort
    -> Expr 'IntSort -> Expr 'IntSort -> Expr 'StringSort)
-> Parser (Expr 'StringSort)
forall (t :: SMTSort) (u :: SMTSort) (v :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u, KnownSMTSort v) =>
ByteString
-> (Expr t -> Expr u -> Expr v -> Expr r) -> Parser (Expr r)
ternary ByteString
"str.substr" Expr 'StringSort
-> Expr 'IntSort -> Expr 'IntSort -> Expr 'StringSort
StrSubstring
                      Parser (Expr 'StringSort)
-> Parser (Expr 'StringSort) -> Parser (Expr 'StringSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'StringSort
    -> Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort)
-> Parser (Expr 'StringSort)
forall (t :: SMTSort) (u :: SMTSort) (v :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u, KnownSMTSort v) =>
ByteString
-> (Expr t -> Expr u -> Expr v -> Expr r) -> Parser (Expr r)
ternary ByteString
"str.replace" Expr 'StringSort
-> Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
strReplace Parser (Expr 'StringSort)
-> Parser (Expr 'StringSort) -> Parser (Expr 'StringSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'StringSort
    -> Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort)
-> Parser (Expr 'StringSort)
forall (t :: SMTSort) (u :: SMTSort) (v :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u, KnownSMTSort v) =>
ByteString
-> (Expr t -> Expr u -> Expr v -> Expr r) -> Parser (Expr r)
ternary ByteString
"str.replace_all" Expr 'StringSort
-> Expr 'StringSort -> Expr 'StringSort -> Expr 'StringSort
strReplaceAll

var :: KnownSMTSort t => Parser (Expr t)
var :: forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
var = do
  ByteString
_     <- ByteString -> Parser ByteString
string ByteString
"var_"
  Int
vId <- forall a. Integral a => Parser a
decimal @Int
  Expr t -> Parser (Expr t)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr t -> Parser (Expr t)) -> Expr t -> Parser (Expr t)
forall a b. (a -> b) -> a -> b
$ SMTVar t -> Expr t
forall (t :: SMTSort). KnownSMTSort t => SMTVar t -> Expr t
Var (SMTVar t -> Expr t) -> SMTVar t -> Expr t
forall a b. (a -> b) -> a -> b
$ Int -> SMTVar t
forall a b. Coercible a b => a -> b
coerce Int
vId
{-# INLINE var #-}

constant :: forall t. KnownSMTSort t => Parser (HaskellType t)
constant :: forall (t :: SMTSort). KnownSMTSort t => Parser (HaskellType t)
constant = case forall (t :: SMTSort). KnownSMTSort t => SSMTSort t
sortSing @t of
  SSMTSort t
SIntSort       -> Parser (HaskellType t) -> Parser (HaskellType t)
forall a. Num a => Parser a -> Parser a
anyValue Parser (HaskellType t)
forall a. Integral a => Parser a
decimal
  SSMTSort t
SRealSort      -> Parser Rational -> Parser Rational
forall a. Num a => Parser a -> Parser a
anyValue Parser Rational
parseRational Parser Rational -> Parser Rational -> Parser Rational
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Rational
parseToRealRational Parser Rational -> Parser Rational -> Parser Rational
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Rational -> Parser Rational
forall a. Num a => Parser a -> Parser a
anyValue Parser Rational
forall a. Fractional a => Parser a
rational
  SSMTSort t
SBoolSort      -> Parser Bool
Parser (HaskellType t)
parseBool
  SBvSort Proxy enc
_ Proxy n
p    -> Proxy n -> Parser (Bitvec enc n)
forall (enc :: BvEnc) (n :: Natural).
(KnownBvEnc enc, KnownNat n) =>
Proxy n -> Parser (Bitvec enc n)
anyBitvector Proxy n
p
  SArraySort Proxy k
k Proxy v
v -> Proxy k
-> Proxy v -> Parser (ConstArray (HaskellType k) (HaskellType v))
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort v, Ord (HaskellType k)) =>
Proxy k
-> Proxy v -> Parser (ConstArray (HaskellType k) (HaskellType v))
constArray Proxy k
k Proxy v
v
  SSMTSort t
SStringSort    -> Parser Text
Parser (HaskellType t)
parseSmtString
{-# INLINEABLE constant #-}

constantExpr :: forall t. KnownSMTSort t => Parser (Expr t)
constantExpr :: forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
constantExpr = Value t -> Expr t
forall (t :: SMTSort). Value t -> Expr t
Constant (Value t -> Expr t)
-> (HaskellType t -> Value t) -> HaskellType t -> Expr t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. HaskellType t -> Value t
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue (HaskellType t -> Expr t)
-> Parser ByteString (HaskellType t) -> Parser ByteString (Expr t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: SMTSort). KnownSMTSort t => Parser (HaskellType t)
constant @t
{-# INLINE constantExpr #-}

anyBitvector :: (KnownBvEnc enc, KnownNat n) => Proxy n -> Parser (Bitvec enc n)
anyBitvector :: forall (enc :: BvEnc) (n :: Natural).
(KnownBvEnc enc, KnownNat n) =>
Proxy n -> Parser (Bitvec enc n)
anyBitvector Proxy n
p = Proxy n -> Parser (Bitvec enc n)
forall (n :: Natural) (enc :: BvEnc).
KnownNat n =>
Proxy n -> Parser (Bitvec enc n)
binBitvector Proxy n
p Parser (Bitvec enc n)
-> Parser (Bitvec enc n) -> Parser (Bitvec enc n)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Proxy n -> Parser (Bitvec enc n)
forall (enc :: BvEnc) (n :: Natural).
(KnownBvEnc enc, KnownNat n) =>
Proxy n -> Parser (Bitvec enc n)
hexBitvector Proxy n
p Parser (Bitvec enc n)
-> Parser (Bitvec enc n) -> Parser (Bitvec enc n)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Proxy n -> Parser (Bitvec enc n)
forall (enc :: BvEnc) (n :: Natural).
(KnownBvEnc enc, KnownNat n) =>
Proxy n -> Parser (Bitvec enc n)
literalBitvector Proxy n
p
{-# INLINE anyBitvector #-}

binBitvector :: KnownNat n => Proxy n -> Parser (Bitvec enc n)
binBitvector :: forall (n :: Natural) (enc :: BvEnc).
KnownNat n =>
Proxy n -> Parser (Bitvec enc n)
binBitvector Proxy n
p = do
  ()
_  <- ByteString -> Parser ByteString
string ByteString
"#b" Parser ByteString -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  [Char]
bs <- Parser ByteString Char -> Parser ByteString [Char]
forall a. Parser ByteString a -> Parser ByteString [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (Parser ByteString Char -> Parser ByteString [Char])
-> Parser ByteString Char -> Parser ByteString [Char]
forall a b. (a -> b) -> a -> b
$ Char -> Parser ByteString Char
char Char
'0' Parser ByteString Char
-> Parser ByteString Char -> Parser ByteString Char
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Char -> Parser ByteString Char
char Char
'1'
  let [Bit]
bs' :: [Bit] = (Char -> Bit) -> [Char] -> [Bit]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\Char
b -> Bool -> Bit -> Bit -> Bit
forall b a. Iteable b a => b -> a -> a -> a
ite (Char
b Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'1') Bit
forall b. Boolean b => b
true Bit
forall b. Boolean b => b
false) [Char]
bs
  case Proxy n -> [Bit] -> Maybe (Bitvec enc n)
forall (n :: Natural) (enc :: BvEnc).
KnownNat n =>
Proxy n -> [Bit] -> Maybe (Bitvec enc n)
bitvecFromListN' Proxy n
p [Bit]
bs' of
    Maybe (Bitvec enc n)
Nothing -> [Char] -> Parser (Bitvec enc n)
forall a. [Char] -> Parser ByteString a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char] -> Parser (Bitvec enc n))
-> [Char] -> Parser (Bitvec enc n)
forall a b. (a -> b) -> a -> b
$ [Char]
"Expected BitVector of length" [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> Natural -> [Char]
forall a. Show a => a -> [Char]
show (Proxy n -> Natural
forall (n :: Natural) (proxy :: Natural -> *).
KnownNat n =>
proxy n -> Natural
natVal Proxy n
p) [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
", but got a different one"
    Just Bitvec enc n
v  -> Bitvec enc n -> Parser (Bitvec enc n)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return Bitvec enc n
v
{-# INLINEABLE binBitvector #-}

hexBitvector :: (KnownBvEnc enc, KnownNat n) => Proxy n -> Parser (Bitvec enc n)
hexBitvector :: forall (enc :: BvEnc) (n :: Natural).
(KnownBvEnc enc, KnownNat n) =>
Proxy n -> Parser (Bitvec enc n)
hexBitvector Proxy n
_ = do
  ()
_ <- ByteString -> Parser ByteString
string ByteString
"#x" Parser ByteString -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  Integer -> Bitvec enc n
forall a. Num a => Integer -> a
fromInteger (Integer -> Bitvec enc n)
-> Parser Integer -> Parser (Bitvec enc n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser Integer
forall a. (Integral a, Bits a) => Parser a
hexadecimal
{-# INLINE hexBitvector #-}

literalBitvector :: (KnownBvEnc enc, KnownNat n) => Proxy n -> Parser (Bitvec enc n)
literalBitvector :: forall (enc :: BvEnc) (n :: Natural).
(KnownBvEnc enc, KnownNat n) =>
Proxy n -> Parser (Bitvec enc n)
literalBitvector Proxy n
_ = do
  ()
_ <- Char -> Parser ByteString Char
char Char
'(' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  ()
_ <- Char -> Parser ByteString Char
char Char
'_' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  ByteString
_ <- ByteString -> Parser ByteString
string ByteString
"bv"
  Integer
x <- Parser Integer
forall a. Integral a => Parser a
decimal
  Char
_ <- (Char -> Bool) -> Parser ()
skipWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
')') Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
')'

  Bitvec enc n -> Parser (Bitvec enc n)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bitvec enc n -> Parser (Bitvec enc n))
-> Bitvec enc n -> Parser (Bitvec enc n)
forall a b. (a -> b) -> a -> b
$ Integer -> Bitvec enc n
forall a. Num a => Integer -> a
fromInteger Integer
x
{-# INLINE literalBitvector #-}

constArray :: forall k v. (KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Proxy v -> Parser (ConstArray (HaskellType k) (HaskellType v))
constArray :: forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort v, Ord (HaskellType k)) =>
Proxy k
-> Proxy v -> Parser (ConstArray (HaskellType k) (HaskellType v))
constArray Proxy k
_ Proxy v
_ = do
  ()
_ <- Char -> Parser ByteString Char
char Char
'(' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
'(' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  ()
_ <- ByteString -> Parser ByteString
string ByteString
"as" Parser ByteString -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace Parser () -> Parser ByteString -> Parser ByteString
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ByteString -> Parser ByteString
string ByteString
"const" Parser ByteString -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  ()
_ <- Char -> Parser ByteString Char
char Char
'(' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (Char -> Bool) -> Parser ()
skipWhile (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
')') Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
')' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  ()
_ <- Char -> Parser ByteString Char
char Char
')' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  HaskellType v
constVal <- forall (t :: SMTSort). KnownSMTSort t => Parser (HaskellType t)
constant @v
  Char
_ <- Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
')'

  ConstArray (HaskellType k) (HaskellType v)
-> Parser (ConstArray (HaskellType k) (HaskellType v))
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstArray (HaskellType k) (HaskellType v)
 -> Parser (ConstArray (HaskellType k) (HaskellType v)))
-> ConstArray (HaskellType k) (HaskellType v)
-> Parser (ConstArray (HaskellType k) (HaskellType v))
forall a b. (a -> b) -> a -> b
$ HaskellType v -> ConstArray (HaskellType k) (HaskellType v)
forall (f :: * -> * -> *) k v. ArrayMap f k v => v -> f k v
asConst HaskellType v
constVal
{-# INLINEABLE constArray #-}

parseSmtString :: Parser Text.Text
parseSmtString :: Parser Text
parseSmtString = do
  Char
_ <- Char -> Parser ByteString Char
char Char
'"'
  Text
s <- ByteString -> Text
decodeUtf8 (ByteString -> Text) -> Parser ByteString -> Parser Text
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Char -> Bool) -> Parser ByteString
takeTill (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'"')
  Char
_ <- Char -> Parser ByteString Char
char Char
'"'
  Text -> Parser Text
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return Text
s

unary :: forall t r. KnownSMTSort t => ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary :: forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
opStr Expr t -> Expr r
op = do
  ()
_ <- Char -> Parser ByteString Char
char Char
'(' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  ()
_ <- ByteString -> Parser ByteString
string ByteString
opStr Parser ByteString -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  Expr t
val <- Parser (Expr t)
forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr
  Char
_ <- Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
')'

  Expr r -> Parser (Expr r)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr r -> Parser (Expr r)) -> Expr r -> Parser (Expr r)
forall a b. (a -> b) -> a -> b
$ Expr t -> Expr r
op Expr t
val
{-# INLINE unary #-}

binary :: forall t u r. (KnownSMTSort t, KnownSMTSort u) => ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary :: forall (t :: SMTSort) (u :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u) =>
ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r)
binary ByteString
opStr Expr t -> Expr u -> Expr r
op = do
  ()
_ <- Char -> Parser ByteString Char
char Char
'(' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  ()
_ <- ByteString -> Parser ByteString
string ByteString
opStr Parser ByteString -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  Expr t
l <- Parser (Expr t)
forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr
  ()
_ <- Parser ()
skipSpace
  Expr u
r <- Parser (Expr u)
forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr
  Char
_ <- Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
')'
  Expr r -> Parser (Expr r)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr r -> Parser (Expr r)) -> Expr r -> Parser (Expr r)
forall a b. (a -> b) -> a -> b
$ Expr t
l Expr t -> Expr u -> Expr r
`op` Expr u
r
{-# INLINE binary #-}

ternary :: forall t u v r. (KnownSMTSort t, KnownSMTSort u, KnownSMTSort v) => ByteString -> (Expr t -> Expr u -> Expr v -> Expr r) -> Parser (Expr r)
ternary :: forall (t :: SMTSort) (u :: SMTSort) (v :: SMTSort) (r :: SMTSort).
(KnownSMTSort t, KnownSMTSort u, KnownSMTSort v) =>
ByteString
-> (Expr t -> Expr u -> Expr v -> Expr r) -> Parser (Expr r)
ternary ByteString
opStr Expr t -> Expr u -> Expr v -> Expr r
op = do
  ()
_ <- Char -> Parser ByteString Char
char Char
'(' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  ()
_ <- ByteString -> Parser ByteString
string ByteString
opStr Parser ByteString -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  Expr t
l <- Parser (Expr t)
forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr
  ()
_ <- Parser ()
skipSpace
  Expr u
m <- Parser (Expr u)
forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr
  ()
_ <- Parser ()
skipSpace
  Expr v
r <- Parser (Expr v)
forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr
  Char
_ <- Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
')'
  Expr r -> Parser (Expr r)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr r -> Parser (Expr r)) -> Expr r -> Parser (Expr r)
forall a b. (a -> b) -> a -> b
$ Expr t -> Expr u -> Expr v -> Expr r
op Expr t
l Expr u
m Expr v
r
{-# INLINE ternary #-}

nary :: forall t r. KnownSMTSort t => ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
nary :: forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
nary ByteString
opStr [Expr t] -> Expr r
op = do
  ()
_    <- Char -> Parser ByteString Char
char Char
'(' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  ()
_    <- ByteString -> Parser ByteString
string ByteString
opStr Parser ByteString -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  [Expr t]
args <- Parser (Expr t)
forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr Parser (Expr t) -> Parser () -> Parser ByteString [Expr t]
forall (f :: * -> *) a s. Alternative f => f a -> f s -> f [a]
`sepBy1` Parser ()
skipSpace
  Char
_    <- Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
')'
  Expr r -> Parser (Expr r)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr r -> Parser (Expr r)) -> Expr r -> Parser (Expr r)
forall a b. (a -> b) -> a -> b
$ [Expr t] -> Expr r
op [Expr t]
args
{-# INLINE nary #-}

smtPi :: Parser (Expr RealSort)
smtPi :: Parser (Expr 'RealSort)
smtPi = ByteString -> Parser ByteString
string ByteString
"real.pi" Parser ByteString
-> Parser (Expr 'RealSort) -> Parser (Expr 'RealSort)
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Expr 'RealSort -> Parser (Expr 'RealSort)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return Expr 'RealSort
forall a. Floating a => a
pi
{-# INLINE smtPi #-}

anyValue :: Num a => Parser a -> Parser a
anyValue :: forall a. Num a => Parser a -> Parser a
anyValue Parser a
p = Parser a -> Parser a
forall a. Num a => Parser a -> Parser a
negativeValue Parser a
p Parser a -> Parser a -> Parser a
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser a
p
{-# INLINEABLE anyValue #-}

negativeValue :: Num a => Parser a -> Parser a
negativeValue :: forall a. Num a => Parser a -> Parser a
negativeValue Parser a
p = do
  ()
_ <- Char -> Parser ByteString Char
char Char
'(' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
'-' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  a
val <- Parser a -> Parser a
forall a. Num a => Parser a -> Parser a
signed Parser a
p
  Char
_ <- Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
')'

  a -> Parser a
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Parser a) -> a -> Parser a
forall a b. (a -> b) -> a -> b
$ a -> a
forall a. Num a => a -> a
negate a
val
{-# INLINE negativeValue #-}

parseRational :: Parser Rational
parseRational :: Parser Rational
parseRational = do
  ()
_           <- Char -> Parser ByteString Char
char Char
'(' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
'/' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  Integer
numerator   <- Parser Integer
forall a. Integral a => Parser a
decimal
  ()
_           <- Parser ()
skipSpace
  Integer
denominator <- Parser Integer
forall a. Integral a => Parser a
decimal
  Char
_           <- Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
')'

  Rational -> Parser Rational
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Rational -> Parser Rational) -> Rational -> Parser Rational
forall a b. (a -> b) -> a -> b
$ Integer
numerator Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
denominator
{-# INLINEABLE parseRational #-}

parseToRealRational :: Parser Rational
parseToRealRational :: Parser Rational
parseToRealRational = do
  ()
_   <- Char -> Parser ByteString Char
char Char
'(' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace Parser () -> Parser ByteString -> Parser ByteString
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ByteString -> Parser ByteString
string ByteString
"to_real" Parser ByteString -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  Integer
dec <- Parser Integer -> Parser Integer
forall a. Num a => Parser a -> Parser a
anyValue Parser Integer
forall a. Integral a => Parser a
decimal
  Char
_   <- Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
')'

  Rational -> Parser Rational
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Rational -> Parser Rational) -> Rational -> Parser Rational
forall a b. (a -> b) -> a -> b
$ Integer -> Rational
forall a. Real a => a -> Rational
toRational Integer
dec
{-# INLINEABLE parseToRealRational #-}

parseBool :: Parser Bool
parseBool :: Parser Bool
parseBool = (ByteString -> Parser ByteString
string ByteString
"true" Parser ByteString -> Parser Bool -> Parser Bool
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Bool -> Parser Bool
forall a. a -> Parser ByteString a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True) Parser Bool -> Parser Bool -> Parser Bool
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (ByteString -> Parser ByteString
string ByteString
"false" Parser ByteString -> Parser Bool -> Parser Bool
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Bool -> Parser Bool
forall a. a -> Parser ByteString a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False)
{-# INLINEABLE parseBool #-}

getValueParser :: KnownSMTSort t => SMTVar t -> Parser (SMTVarSol t)
getValueParser :: forall (t :: SMTSort).
KnownSMTSort t =>
SMTVar t -> Parser (SMTVarSol t)
getValueParser SMTVar t
v = do
  ()
_ <- Char -> Parser ByteString Char
char Char
'(' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
'(' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace
  ByteString
_ <- ByteString -> Parser ByteString
string (ByteString -> Parser ByteString)
-> ByteString -> Parser ByteString
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString
toStrict (ByteString -> ByteString) -> ByteString -> ByteString
forall a b. (a -> b) -> a -> b
$ Builder -> ByteString
toLazyByteString (Builder -> ByteString) -> Builder -> ByteString
forall a b. (a -> b) -> a -> b
$ SMTVar t -> Builder
forall a. Render a => a -> Builder
render SMTVar t
v
  ()
_ <- Parser ()
skipSpace
  Expr t
expr <- Parser (Expr t)
forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr
  Char
_ <- Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
')' Parser ByteString Char -> Parser () -> Parser ()
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
skipSpace Parser () -> Parser ByteString Char -> Parser ByteString Char
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> Parser ByteString Char
char Char
')'
  case Solution -> Expr t -> Maybe (Decoded (Expr t))
forall a. Codec a => Solution -> a -> Maybe (Decoded a)
decode Solution
forall a. Monoid a => a
mempty Expr t
expr of
    Maybe (Decoded (Expr t))
Nothing    -> [Char] -> Parser (SMTVarSol t)
forall a. [Char] -> Parser ByteString a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char] -> Parser (SMTVarSol t)) -> [Char] -> Parser (SMTVarSol t)
forall a b. (a -> b) -> a -> b
$ [Char]
"Solver reponded with solution for var_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (SMTVar t
vSMTVar t -> Getting Int (SMTVar t) Int -> Int
forall s a. s -> Getting a s a -> a
^.Getting Int (SMTVar t) Int
forall (t1 :: SMTSort) (t2 :: SMTSort) (p :: * -> * -> *)
       (f :: * -> *).
(Profunctor p, Functor f) =>
p Int (f Int) -> p (SMTVar t1) (f (SMTVar t2))
varId) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
" but it contains "
                      [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"another var. This cannot be parsed and evaluated currently."
    Just Decoded (Expr t)
value -> SMTVarSol t -> Parser (SMTVarSol t)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (SMTVarSol t -> Parser (SMTVarSol t))
-> SMTVarSol t -> Parser (SMTVarSol t)
forall a b. (a -> b) -> a -> b
$ SMTVar t -> Value t -> SMTVarSol t
forall (t :: SMTSort). SMTVar t -> Value t -> SMTVarSol t
SMTVarSol SMTVar t
v (HaskellType t -> Value t
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue HaskellType t
Decoded (Expr t)
value)