{-# 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.Num ()
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.SMTSort
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)