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

module Language.Hasmtlib.Internal.Parser where

import Prelude hiding (not, (&&), (||), and , or)
import Language.Hasmtlib.Internal.Bitvec
import Language.Hasmtlib.Internal.Render
import Language.Hasmtlib.Internal.Expr
import Language.Hasmtlib.Equatable
import Language.Hasmtlib.Orderable
import Language.Hasmtlib.Boolean
import Language.Hasmtlib.Iteable
import Language.Hasmtlib.Codec
import Language.Hasmtlib.Type.Solution
import Language.Hasmtlib.Type.ArrayMap
import Data.Bit
import Data.Coerce
import Data.Proxy
import Data.Ratio ((%))
import Data.ByteString
import Data.ByteString.Builder
import Data.Attoparsec.ByteString hiding (Result, skipWhile)
import Data.Attoparsec.ByteString.Char8 hiding (Result)
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
  (SomeSMTSort SSMTSort t
someSort) <- Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
parseSomeSort
  ()
_     <- Parser ()
skipSpace
  Expr t
expr  <- SSMTSort t -> Parser (Expr t)
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> Parser (Expr t)
parseExpr' SSMTSort t
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 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 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 t)
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 t -> SomeKnownOrdSMTSort SMTVarSol
forall (cs :: [SMTSort -> Constraint]) (f :: SMTSort -> *)
       (t :: SMTSort).
AllC cs t =>
f t -> SomeSMTSort cs f
SomeSMTSort (SMTVarSol t -> SomeKnownOrdSMTSort SMTVarSol)
-> SMTVarSol t -> SomeKnownOrdSMTSort SMTVarSol
forall a b. (a -> b) -> a -> b
$ SMTVar t -> Value t -> SMTVarSol t
forall (t :: SMTSort). SMTVar t -> Value t -> SMTVarSol t
SMTVarSol (Int -> SMTVar t
forall a b. Coercible a b => a -> b
coerce Int
vId) (HaskellType t -> Value t
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue HaskellType t
Decoded (Expr t)
value)
{-# INLINEABLE parseSomeSol #-}

parseSomeSort :: Parser (SomeKnownOrdSMTSort SSMTSort)
parseSomeSort :: Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
parseSomeSort = (ByteString -> Parser ByteString
string ByteString
"Bool" Parser ByteString
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
forall a. a -> Parser ByteString a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SSMTSort 'BoolSort
-> SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort
forall (cs :: [SMTSort -> Constraint]) (f :: SMTSort -> *)
       (t :: SMTSort).
AllC cs t =>
f t -> SomeSMTSort cs f
SomeSMTSort SSMTSort 'BoolSort
SBoolSort))
        Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
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 (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
forall a. a -> Parser ByteString a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SSMTSort 'IntSort
-> SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort
forall (cs :: [SMTSort -> Constraint]) (f :: SMTSort -> *)
       (t :: SMTSort).
AllC cs t =>
f t -> SomeSMTSort cs f
SomeSMTSort SSMTSort 'IntSort
SIntSort))
        Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
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 (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
forall a b.
Parser ByteString a -> Parser ByteString b -> Parser ByteString b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
forall a. a -> Parser ByteString a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SSMTSort 'RealSort
-> SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort
forall (cs :: [SMTSort -> Constraint]) (f :: SMTSort -> *)
       (t :: SMTSort).
AllC cs t =>
f t -> SomeSMTSort cs f
SomeSMTSort SSMTSort 'RealSort
SRealSort))
        Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
parseSomeBitVecSort
        Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
parseSomeArraySort
{-# INLINEABLE parseSomeSort #-}

parseSomeBitVecSort :: Parser (SomeKnownOrdSMTSort SSMTSort)
parseSomeBitVecSort :: Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
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
    SomeNat Proxy n
pn -> SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort
 -> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort))
-> SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
forall a b. (a -> b) -> a -> b
$ SSMTSort ('BvSort n)
-> SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort
forall (cs :: [SMTSort -> Constraint]) (f :: SMTSort -> *)
       (t :: SMTSort).
AllC cs t =>
f t -> SomeSMTSort cs f
SomeSMTSort (SSMTSort ('BvSort n)
 -> SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
-> SSMTSort ('BvSort n)
-> SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort
forall a b. (a -> b) -> a -> b
$ Proxy n -> SSMTSort ('BvSort n)
forall (n :: Natural).
KnownNat n =>
Proxy n -> SSMTSort ('BvSort n)
SBvSort Proxy n
pn
{-# INLINEABLE parseSomeBitVecSort #-}

parseSomeArraySort :: Parser (SomeKnownOrdSMTSort SSMTSort)
parseSomeArraySort :: Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
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
  (SomeSMTSort SSMTSort t
keySort)   <- Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
parseSomeSort
  ()
_ <- Parser ()
skipSpace
  (SomeSMTSort SSMTSort t
valueSort) <- Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
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
')'
  SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort
 -> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort))
-> SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort
-> Parser (SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
forall a b. (a -> b) -> a -> b
$ SSMTSort ('ArraySort t t)
-> SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort
forall (cs :: [SMTSort -> Constraint]) (f :: SMTSort -> *)
       (t :: SMTSort).
AllC cs t =>
f t -> SomeSMTSort cs f
SomeSMTSort (SSMTSort ('ArraySort t t)
 -> SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort)
-> SSMTSort ('ArraySort t t)
-> SomeSMTSort '[KnownSMTSort, OrdHaskellType] SSMTSort
forall a b. (a -> b) -> a -> b
$ Proxy t -> Proxy t -> SSMTSort ('ArraySort t t)
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
Proxy k -> Proxy v -> SSMTSort ('ArraySort k v)
SArraySort (SSMTSort t -> Proxy t
forall (t :: SMTSort). SSMTSort t -> Proxy t
goProxy SSMTSort t
keySort) (SSMTSort t -> Proxy t
forall (t :: SMTSort). SSMTSort t -> Proxy t
goProxy SSMTSort t
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). 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
<|> Parser (Expr t)
forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
smtIte
        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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> 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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"mod" Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
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
<|> Parser (Expr 'IntSort)
toIntFun
              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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> 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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> 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
<|> Parser (Expr 'RealSort)
toRealFun
                      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 -> Parser (Expr 'BoolSort)
isIntFun
                      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)
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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> 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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> 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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> 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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> 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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> 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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> 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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> 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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> 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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> 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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> 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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> 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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> 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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> 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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> 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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> 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) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary @RealSort ByteString
">" Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(>?)
                      -- TODO: Add compare ops for all (?) bv-sorts
              SBvSort Proxy n
_ -> ByteString
-> (Expr ('BvSort n) -> Expr ('BvSort n))
-> Parser (Expr ('BvSort n))
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"bvnot" Expr ('BvSort n) -> Expr ('BvSort n)
forall b. Boolean b => b -> b
not
                      Parser (Expr ('BvSort n))
-> Parser (Expr ('BvSort n)) -> Parser (Expr ('BvSort 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 n) -> Expr ('BvSort n) -> Expr ('BvSort n))
-> Parser (Expr ('BvSort n))
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"bvand" Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall b. Boolean b => b -> b -> b
(&&)  Parser (Expr ('BvSort n))
-> Parser (Expr ('BvSort n)) -> Parser (Expr ('BvSort 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 n) -> Expr ('BvSort n) -> Expr ('BvSort n))
-> Parser (Expr ('BvSort n))
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"bvor" Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall b. Boolean b => b -> b -> b
(||) Parser (Expr ('BvSort n))
-> Parser (Expr ('BvSort n)) -> Parser (Expr ('BvSort 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 n) -> Expr ('BvSort n) -> Expr ('BvSort n))
-> Parser (Expr ('BvSort n))
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"bvxor" Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall b. Boolean b => b -> b -> b
xor Parser (Expr ('BvSort n))
-> Parser (Expr ('BvSort n)) -> Parser (Expr ('BvSort 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 n) -> Expr ('BvSort n) -> Expr ('BvSort n))
-> Parser (Expr ('BvSort n))
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"bvnand" Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Natural).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvNand Parser (Expr ('BvSort n))
-> Parser (Expr ('BvSort n)) -> Parser (Expr ('BvSort 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 n) -> Expr ('BvSort n) -> Expr ('BvSort n))
-> Parser (Expr ('BvSort n))
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"bvnor" Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Natural).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvNor
                      Parser (Expr ('BvSort n))
-> Parser (Expr ('BvSort n)) -> Parser (Expr ('BvSort 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 n) -> Expr ('BvSort n))
-> Parser (Expr ('BvSort n))
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary  ByteString
"bvneg" Expr ('BvSort n) -> Expr ('BvSort n)
forall a. Num a => a -> a
negate
                      Parser (Expr ('BvSort n))
-> Parser (Expr ('BvSort n)) -> Parser (Expr ('BvSort 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 n) -> Expr ('BvSort n) -> Expr ('BvSort n))
-> Parser (Expr ('BvSort n))
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"bvadd" Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall a. Num a => a -> a -> a
(+)  Parser (Expr ('BvSort n))
-> Parser (Expr ('BvSort n)) -> Parser (Expr ('BvSort 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 n) -> Expr ('BvSort n) -> Expr ('BvSort n))
-> Parser (Expr ('BvSort n))
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"bvsub" (-) Parser (Expr ('BvSort n))
-> Parser (Expr ('BvSort n)) -> Parser (Expr ('BvSort 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 n) -> Expr ('BvSort n) -> Expr ('BvSort n))
-> Parser (Expr ('BvSort n))
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"bvmul" Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall a. Num a => a -> a -> a
(*)
                      Parser (Expr ('BvSort n))
-> Parser (Expr ('BvSort n)) -> Parser (Expr ('BvSort 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 n) -> Expr ('BvSort n) -> Expr ('BvSort n))
-> Parser (Expr ('BvSort n))
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"bvudiv" Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Natural).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvuDiv Parser (Expr ('BvSort n))
-> Parser (Expr ('BvSort n)) -> Parser (Expr ('BvSort 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 n) -> Expr ('BvSort n) -> Expr ('BvSort n))
-> Parser (Expr ('BvSort n))
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"bvurem" Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Natural).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvuRem
                      Parser (Expr ('BvSort n))
-> Parser (Expr ('BvSort n)) -> Parser (Expr ('BvSort 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 n) -> Expr ('BvSort n) -> Expr ('BvSort n))
-> Parser (Expr ('BvSort n))
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"bvshl" Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Natural).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvShL Parser (Expr ('BvSort n))
-> Parser (Expr ('BvSort n)) -> Parser (Expr ('BvSort 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 n) -> Expr ('BvSort n) -> Expr ('BvSort n))
-> Parser (Expr ('BvSort n))
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"bvlshr" Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Natural).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvLShR
              SArraySort Proxy k
_ Proxy v
_ -> Parser (Expr t)
Parser (Expr ('ArraySort k v))
forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
Parser (Expr ('ArraySort k v))
parseStore
                      -- TODO: Add compare ops for all (?) array-sorts

var :: Parser (Expr t)
var :: forall (t :: SMTSort). 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). 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 Double -> Parser Double
forall a. Num a => Parser a -> Parser a
anyValue Parser Double
parseRatioDouble Parser Double -> Parser Double -> Parser Double
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Double
parseToRealDouble Parser Double -> Parser Double -> Parser Double
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser Double -> Parser Double
forall a. Num a => Parser a -> Parser a
anyValue Parser Double
forall a. Fractional a => Parser a
rational
  SSMTSort t
SBoolSort -> Parser Bool
Parser (HaskellType t)
parseBool
  SBvSort Proxy n
p -> Proxy n -> Parser (Bitvec n)
forall (n :: Natural). KnownNat n => Proxy n -> Parser (Bitvec 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
{-# INLINE 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 :: KnownNat n => Proxy n -> Parser (Bitvec n)
anyBitvector :: forall (n :: Natural). KnownNat n => Proxy n -> Parser (Bitvec n)
anyBitvector Proxy n
p = Proxy n -> Parser (Bitvec n)
forall (n :: Natural). KnownNat n => Proxy n -> Parser (Bitvec n)
binBitvector Proxy n
p Parser (Bitvec n) -> Parser (Bitvec n) -> Parser (Bitvec 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 n)
forall (n :: Natural). KnownNat n => Proxy n -> Parser (Bitvec n)
hexBitvector Proxy n
p Parser (Bitvec n) -> Parser (Bitvec n) -> Parser (Bitvec 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 n)
forall (n :: Natural). KnownNat n => Proxy n -> Parser (Bitvec n)
literalBitvector Proxy n
p
{-# INLINE anyBitvector #-}

binBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)
binBitvector :: forall (n :: Natural). KnownNat n => Proxy n -> Parser (Bitvec 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 n)
forall (n :: Natural).
KnownNat n =>
Proxy n -> [Bit] -> Maybe (Bitvec n)
bvFromListN' Proxy n
p [Bit]
bs' of
    Maybe (Bitvec n)
Nothing -> [Char] -> Parser (Bitvec n)
forall a. [Char] -> Parser ByteString a
forall (m :: * -> *) a. MonadFail m => [Char] -> m a
fail ([Char] -> Parser (Bitvec n)) -> [Char] -> Parser (Bitvec 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 n
v  -> Bitvec n -> Parser (Bitvec n)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return Bitvec n
v
{-# INLINEABLE binBitvector #-}

hexBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)
hexBitvector :: forall (n :: Natural). KnownNat n => Proxy n -> Parser (Bitvec 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 n
forall a. Num a => Integer -> a
fromInteger (Integer -> Bitvec n) -> Parser Integer -> Parser (Bitvec 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 :: KnownNat n => Proxy n -> Parser (Bitvec n)
literalBitvector :: forall (n :: Natural). KnownNat n => Proxy n -> Parser (Bitvec 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 n -> Parser (Bitvec n)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Bitvec n -> Parser (Bitvec n)) -> Bitvec n -> Parser (Bitvec n)
forall a b. (a -> b) -> a -> b
$ Integer -> Bitvec 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 #-}

parseSelect :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Parser (Expr v)
parseSelect :: forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
Proxy k -> Parser (Expr v)
parseSelect Proxy k
_ = 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
"select" 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 ('ArraySort k v)
arr <- forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr @(ArraySort k v)
  ()
_ <- Parser ()
skipSpace
  Expr k
i <- forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr @k
  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 v -> Parser (Expr v)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr v -> Parser (Expr v)) -> Expr v -> Parser (Expr v)
forall a b. (a -> b) -> a -> b
$ Expr ('ArraySort k v) -> Expr k -> Expr v
forall (k :: SMTSort) (t :: SMTSort).
(KnownSMTSort k, KnownSMTSort t, Ord (HaskellType k)) =>
Expr ('ArraySort k t) -> Expr k -> Expr t
ArrSelect Expr ('ArraySort k v)
arr Expr k
i

parseStore :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Parser (Expr (ArraySort k v))
parseStore :: forall (k :: SMTSort) (v :: SMTSort).
(KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) =>
Parser (Expr ('ArraySort k v))
parseStore = 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
"store" 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 ('ArraySort k v)
arr <- forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr @(ArraySort k v)
  ()
_ <- Parser ()
skipSpace
  Expr k
i <- forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr @k
  ()
_ <- Parser ()
skipSpace
  Expr v
x <- forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr @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
')'

  Expr ('ArraySort k v) -> Parser (Expr ('ArraySort k v))
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr ('ArraySort k v) -> Parser (Expr ('ArraySort k v)))
-> Expr ('ArraySort k v) -> Parser (Expr ('ArraySort k v))
forall a b. (a -> b) -> a -> b
$ 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 Expr ('ArraySort k v)
arr Expr k
i Expr v
x

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 r. KnownSMTSort t => ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary :: forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
opStr Expr t -> 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
l <- Parser (Expr t)
forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr
  ()
_ <- Parser ()
skipSpace
  Expr t
r <- 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
l Expr t -> Expr t -> Expr r
`op` Expr t
r
{-# INLINE binary #-}

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

toRealFun :: Parser (Expr RealSort)
toRealFun :: Parser (Expr 'RealSort)
toRealFun = 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
"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
  Expr 'IntSort
val <- Parser (Expr 'IntSort)
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 'RealSort -> Parser (Expr 'RealSort)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr 'RealSort -> Parser (Expr 'RealSort))
-> Expr 'RealSort -> Parser (Expr 'RealSort)
forall a b. (a -> b) -> a -> b
$ Expr 'IntSort -> Expr 'RealSort
ToReal Expr 'IntSort
val
{-# INLINEABLE toRealFun #-}

toIntFun :: Parser (Expr IntSort)
toIntFun :: Parser (Expr 'IntSort)
toIntFun = 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
"to_int" 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 'RealSort
val <- Parser (Expr 'RealSort)
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 'IntSort -> Parser (Expr 'IntSort)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr 'IntSort -> Parser (Expr 'IntSort))
-> Expr 'IntSort -> Parser (Expr 'IntSort)
forall a b. (a -> b) -> a -> b
$ Expr 'RealSort -> Expr 'IntSort
ToInt Expr 'RealSort
val
{-# INLINEABLE toIntFun #-}

isIntFun :: Parser (Expr BoolSort)
isIntFun :: Parser (Expr 'BoolSort)
isIntFun = 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
"is_int" 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 'RealSort
val <- Parser (Expr 'RealSort)
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 'BoolSort -> Parser (Expr 'BoolSort)
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr 'BoolSort -> Parser (Expr 'BoolSort))
-> Expr 'BoolSort -> Parser (Expr 'BoolSort)
forall a b. (a -> b) -> a -> b
$ Expr 'RealSort -> Expr 'BoolSort
IsInt Expr 'RealSort
val
{-# INLINEABLE isIntFun #-}

smtIte :: forall t. KnownSMTSort t => Parser (Expr t)
smtIte :: forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
smtIte = 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
"ite" 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 'BoolSort
p <- forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr @BoolSort
  ()
_ <- Parser ()
skipSpace
  Expr t
t <- Parser (Expr t)
forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr
  ()
_ <- Parser ()
skipSpace
  Expr t
f <- 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 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
$ Expr 'BoolSort -> Expr t -> Expr t -> Expr t
forall b a. Iteable b a => b -> a -> a -> a
ite Expr 'BoolSort
p Expr t
t Expr t
f
{-# INLINEABLE smtIte #-}

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

parseRatioDouble :: Parser Double
parseRatioDouble :: Parser Double
parseRatioDouble = 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
')'

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

parseToRealDouble :: Parser Double
parseToRealDouble :: Parser Double
parseToRealDouble = 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
')'
  
  Double -> Parser Double
forall a. a -> Parser ByteString a
forall (m :: * -> *) a. Monad m => a -> m a
return (Double -> Parser Double) -> Double -> Parser Double
forall a b. (a -> b) -> a -> b
$ Integer -> Double
forall a. Num a => Integer -> a
fromInteger Integer
dec
{-# INLINEABLE parseToRealDouble #-}

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)