{-# LANGUAGE LambdaCase #-}

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 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 qualified Data.IntMap as IM
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
  [SomeKnownSMTSort SMTVarSol]
varSols <- Parser ByteString (SomeKnownSMTSort SMTVarSol)
-> Parser ByteString [SomeKnownSMTSort SMTVarSol]
forall a. Parser ByteString a -> Parser ByteString [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (Parser ByteString (SomeKnownSMTSort SMTVarSol)
 -> Parser ByteString [SomeKnownSMTSort SMTVarSol])
-> Parser ByteString (SomeKnownSMTSort SMTVarSol)
-> Parser ByteString [SomeKnownSMTSort SMTVarSol]
forall a b. (a -> b) -> a -> b
$ Parser ByteString (SomeKnownSMTSort SMTVarSol)
parseSomeSol Parser ByteString (SomeKnownSMTSort SMTVarSol)
-> Parser () -> Parser ByteString (SomeKnownSMTSort 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
$ [SomeKnownSMTSort SMTVarSol] -> Solution
fromSomeList [SomeKnownSMTSort 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
  [SomeKnownSMTSort SMTVarSol]
varSols <- Parser ByteString (SomeKnownSMTSort SMTVarSol)
-> Parser ByteString [SomeKnownSMTSort SMTVarSol]
forall a. Parser ByteString a -> Parser ByteString [a]
forall (f :: * -> *) a. Alternative f => f a -> f [a]
many (Parser ByteString (SomeKnownSMTSort SMTVarSol)
 -> Parser ByteString [SomeKnownSMTSort SMTVarSol])
-> Parser ByteString (SomeKnownSMTSort SMTVarSol)
-> Parser ByteString [SomeKnownSMTSort SMTVarSol]
forall a b. (a -> b) -> a -> b
$ Parser ByteString (SomeKnownSMTSort SMTVarSol)
parseSomeSol Parser ByteString (SomeKnownSMTSort SMTVarSol)
-> Parser () -> Parser ByteString (SomeKnownSMTSort 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
$ [SomeKnownSMTSort SMTVarSol] -> Solution
fromSomeList [SomeKnownSMTSort SMTVarSol]
varSols

fromSomeList :: [SomeKnownSMTSort SMTVarSol] -> Solution
fromSomeList :: [SomeKnownSMTSort SMTVarSol] -> Solution
fromSomeList = [(Key, SomeKnownSMTSort SMTVarSol)] -> Solution
forall a. [(Key, a)] -> IntMap a
IM.fromList ([(Key, SomeKnownSMTSort SMTVarSol)] -> Solution)
-> ([SomeKnownSMTSort SMTVarSol]
    -> [(Key, SomeKnownSMTSort SMTVarSol)])
-> [SomeKnownSMTSort SMTVarSol]
-> Solution
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SomeKnownSMTSort SMTVarSol -> (Key, SomeKnownSMTSort SMTVarSol))
-> [SomeKnownSMTSort SMTVarSol]
-> [(Key, SomeKnownSMTSort SMTVarSol)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\case someVarSol :: SomeKnownSMTSort SMTVarSol
someVarSol@(SomeKnownSMTSort SMTVarSol t
varSol) -> (SMTVar t -> Key
forall a b. Coercible a b => a -> b
coerce (SMTVarSol t
varSolSMTVarSol t
-> Getting (SMTVar t) (SMTVarSol t) (SMTVar t) -> SMTVar t
forall s a. s -> Getting a s a -> a
^.Getting (SMTVar t) (SMTVarSol t) (SMTVar t)
forall (t :: SMTSort) (f :: * -> *).
Functor f =>
(SMTVar t -> f (SMTVar t)) -> SMTVarSol t -> f (SMTVarSol t)
solVar), SomeKnownSMTSort SMTVarSol
someVarSol))

parseSomeSol :: Parser (SomeKnownSMTSort SMTVarSol)
parseSomeSol :: Parser ByteString (SomeKnownSMTSort SMTVarSol)
parseSomeSol = SMTVarSol 'IntSort -> SomeKnownSMTSort SMTVarSol
forall (t :: SMTSort) (f :: SMTSort -> *).
KnownSMTSort t =>
f t -> SomeKnownSMTSort f
SomeKnownSMTSort (SMTVarSol 'IntSort -> SomeKnownSMTSort SMTVarSol)
-> Parser ByteString (SMTVarSol 'IntSort)
-> Parser ByteString (SomeKnownSMTSort SMTVarSol)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: SMTSort). KnownSMTSort t => Parser (SMTVarSol t)
parseSol @IntSort)
           Parser ByteString (SomeKnownSMTSort SMTVarSol)
-> Parser ByteString (SomeKnownSMTSort SMTVarSol)
-> Parser ByteString (SomeKnownSMTSort SMTVarSol)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SMTVarSol 'RealSort -> SomeKnownSMTSort SMTVarSol
forall (t :: SMTSort) (f :: SMTSort -> *).
KnownSMTSort t =>
f t -> SomeKnownSMTSort f
SomeKnownSMTSort (SMTVarSol 'RealSort -> SomeKnownSMTSort SMTVarSol)
-> Parser ByteString (SMTVarSol 'RealSort)
-> Parser ByteString (SomeKnownSMTSort SMTVarSol)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: SMTSort). KnownSMTSort t => Parser (SMTVarSol t)
parseSol @RealSort)
           Parser ByteString (SomeKnownSMTSort SMTVarSol)
-> Parser ByteString (SomeKnownSMTSort SMTVarSol)
-> Parser ByteString (SomeKnownSMTSort SMTVarSol)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> SMTVarSol 'BoolSort -> SomeKnownSMTSort SMTVarSol
forall (t :: SMTSort) (f :: SMTSort -> *).
KnownSMTSort t =>
f t -> SomeKnownSMTSort f
SomeKnownSMTSort (SMTVarSol 'BoolSort -> SomeKnownSMTSort SMTVarSol)
-> Parser ByteString (SMTVarSol 'BoolSort)
-> Parser ByteString (SomeKnownSMTSort SMTVarSol)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (t :: SMTSort). KnownSMTSort t => Parser (SMTVarSol t)
parseSol @BoolSort)
           Parser ByteString (SomeKnownSMTSort SMTVarSol)
-> Parser ByteString (SomeKnownSMTSort SMTVarSol)
-> Parser ByteString (SomeKnownSMTSort SMTVarSol)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Natural -> Parser ByteString (SomeKnownSMTSort SMTVarSol)
parseAnyBvUpToLength Natural
128

parseAnyBvUpToLength :: Natural -> Parser (SomeKnownSMTSort SMTVarSol)
parseAnyBvUpToLength :: Natural -> Parser ByteString (SomeKnownSMTSort SMTVarSol)
parseAnyBvUpToLength Natural
hi = [Parser ByteString (SomeKnownSMTSort SMTVarSol)]
-> Parser ByteString (SomeKnownSMTSort SMTVarSol)
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum ([Parser ByteString (SomeKnownSMTSort SMTVarSol)]
 -> Parser ByteString (SomeKnownSMTSort SMTVarSol))
-> [Parser ByteString (SomeKnownSMTSort SMTVarSol)]
-> Parser ByteString (SomeKnownSMTSort SMTVarSol)
forall a b. (a -> b) -> a -> b
$ (Natural -> Parser ByteString (SomeKnownSMTSort SMTVarSol))
-> [Natural] -> [Parser ByteString (SomeKnownSMTSort SMTVarSol)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((\case SomeNat Proxy n
p -> Proxy n -> Parser ByteString (SomeKnownSMTSort SMTVarSol)
forall (n :: Natural).
KnownNat n =>
Proxy n -> Parser ByteString (SomeKnownSMTSort SMTVarSol)
goProxy Proxy n
p) (SomeNat -> Parser ByteString (SomeKnownSMTSort SMTVarSol))
-> (Natural -> SomeNat)
-> Natural
-> Parser ByteString (SomeKnownSMTSort SMTVarSol)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> SomeNat
someNatVal) [Natural
0..Natural
hi]
  where
    goProxy :: forall n. KnownNat n => Proxy n -> Parser (SomeKnownSMTSort SMTVarSol)
    goProxy :: forall (n :: Natural).
KnownNat n =>
Proxy n -> Parser ByteString (SomeKnownSMTSort SMTVarSol)
goProxy Proxy n
_ = SMTVarSol ('BvSort n) -> SomeKnownSMTSort SMTVarSol
forall (t :: SMTSort) (f :: SMTSort -> *).
KnownSMTSort t =>
f t -> SomeKnownSMTSort f
SomeKnownSMTSort (SMTVarSol ('BvSort n) -> SomeKnownSMTSort SMTVarSol)
-> Parser ByteString (SMTVarSol ('BvSort n))
-> Parser ByteString (SomeKnownSMTSort SMTVarSol)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: SMTSort). KnownSMTSort t => Parser (SMTVarSol t)
parseSol @(BvSort n)

parseSol :: forall t. KnownSMTSort t => Parser (SMTVarSol t)
parseSol :: forall (t :: SMTSort). KnownSMTSort t => Parser (SMTVarSol t)
parseSol = 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_"
  Key
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
  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
$ SSMTSort t -> Builder
forall a. Render a => a -> Builder
render (forall (t :: SMTSort). KnownSMTSort t => SSMTSort t
sortSing @t)
  ()
_     <- Parser ()
skipSpace
  Expr t
expr  <- forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
parseExpr @t
  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
')'

  -- Try to evaluate expression given by solver as solution
  -- Better: Take into scope already successfully parsed solutions for other vars.
  -- Is this even required though? Do the solvers ever answer like-wise?
  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]
++ Key -> [Char]
forall a. Show a => a -> [Char]
show Key
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 -> 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 (Key -> SMTVar t
forall a b. Coercible a b => a -> b
coerce Key
vId) (HaskellType t -> Value t
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue HaskellType t
Decoded (Expr t)
value)
{-# INLINEABLE parseSol #-}

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)
constant 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 t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"abs" Expr t -> Expr t
forall a. Num a => a -> a
abs Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary  ByteString
"-" Expr t -> Expr t
forall a. Num a => a -> a
negate
                      Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> ([Expr t] -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
nary ByteString
"+" [Expr t] -> Expr t
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum  Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"-" (-) Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> ([Expr t] -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
nary ByteString
"*" [Expr t] -> Expr t
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr 'IntSort -> Expr 'IntSort -> Expr t) -> Parser (Expr t)
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 t
Expr 'IntSort -> Expr 'IntSort -> Expr 'IntSort
Mod
                      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)
Parser (Expr 'IntSort)
toIntFun
              SSMTSort t
SRealSort -> ByteString -> (Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"abs" Expr t -> Expr t
forall a. Num a => a -> a
abs Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary  ByteString
"-" Expr t -> Expr t
forall a. Num a => a -> a
negate
                      Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> ([Expr t] -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
nary ByteString
"+" [Expr t] -> Expr t
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum  Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"-" (-) Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> ([Expr t] -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
nary ByteString
"*" [Expr t] -> Expr t
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"/" Expr t -> Expr t -> Expr t
forall a. Fractional a => a -> a -> a
(/)
                      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)
Parser (Expr 'RealSort)
toRealFun
                      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)
Parser (Expr 'RealSort)
smtPi Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"sqrt" Expr t -> Expr t
forall a. Floating a => a -> a
sqrt Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"exp" Expr t -> Expr t
forall a. Floating a => a -> a
exp
                      Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"sin" Expr t -> Expr t
forall a. Floating a => a -> a
sin Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"cos" Expr t -> Expr t
forall a. Floating a => a -> a
cos Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"tan" Expr t -> Expr t
forall a. Floating a => a -> a
tan
                      Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"arcsin" Expr t -> Expr t
forall a. Floating a => a -> a
asin Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"arccos" Expr t -> Expr t
forall a. Floating a => a -> a
acos Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"arctan" Expr t -> Expr t
forall a. Floating a => a -> a
atan
              SSMTSort t
SBoolSort -> Parser (Expr t)
Parser (Expr 'BoolSort)
isIntFun
                      Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"not" Expr t -> Expr t
forall b. Boolean b => b -> b
not
                      Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> ([Expr t] -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
nary ByteString
"and" [Expr t] -> Expr t
forall (t :: * -> *) b. (Foldable t, Boolean b) => t b -> b
and  Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> ([Expr t] -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)
nary ByteString
"or" [Expr t] -> Expr t
forall (t :: * -> *) b. (Foldable t, Boolean b) => t b -> b
or Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"=>" Expr t -> Expr t -> Expr t
forall b. Boolean b => b -> b -> b
(==>) Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"xor" Expr t -> Expr t -> Expr t
forall b. Boolean b => b -> b -> b
xor
                      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
<|> 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 t
Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
(===) Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 t
Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
(/==)
                      Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 t
Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
(===) Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 t
Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
(/==)
                      Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 t
Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
(===) Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 t
Expr 'BoolSort -> Expr 'BoolSort -> Expr 'BoolSort
forall a. Equatable a => a -> a -> Expr 'BoolSort
(/==)
                      Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 t
Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(<?) Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 t
Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(<=?)
                      Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 t
Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(>=?) Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 t
Expr 'IntSort -> Expr 'IntSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(>?)
                      Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 t
Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(<?) Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 t
Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(<=?)
                      Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 t
Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(>=?) Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> 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 t
Expr 'RealSort -> Expr 'RealSort -> Expr 'BoolSort
forall a. Orderable a => a -> a -> Expr 'BoolSort
(>?)
                      -- TODO: All (?) bv lengths - also for '=' and 'distinct'
--                      <|> binary @(BvSort 10) "bvult" (<?) <|> binary @(BvSort 10) "bvule" (<=?)
--                      <|> binary @(BvSort 10) "bvuge" (>=?) <|> binary @(BvSort 10) "bvugt" (>?)
              SBvSort Proxy n
_ -> ByteString -> (Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary ByteString
"bvnot" Expr t -> Expr t
forall b. Boolean b => b -> b
not
                      Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"bvand" Expr t -> Expr t -> Expr t
forall b. Boolean b => b -> b -> b
(&&)  Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"bvor" Expr t -> Expr t -> Expr t
forall b. Boolean b => b -> b -> b
(||) Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"bvxor" Expr t -> Expr t -> Expr t
forall b. Boolean b => b -> b -> b
xor Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> Parser (Expr t)
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 t
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 t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> Parser (Expr t)
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 t
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 t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr r) -> Parser (Expr r)
unary  ByteString
"bvneg" Expr t -> Expr t
forall a. Num a => a -> a
negate
                      Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"bvadd" Expr t -> Expr t -> Expr t
forall a. Num a => a -> a -> a
(+)  Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"bvsub" (-) Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString -> (Expr t -> Expr t -> Expr t) -> Parser (Expr t)
forall (t :: SMTSort) (r :: SMTSort).
KnownSMTSort t =>
ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)
binary ByteString
"bvmul" Expr t -> Expr t -> Expr t
forall a. Num a => a -> a -> a
(*)
                      Parser (Expr t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> Parser (Expr t)
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 t
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 t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> Parser (Expr t)
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 t
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 t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> Parser (Expr t)
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 t
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 t) -> Parser (Expr t) -> Parser (Expr t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> ByteString
-> (Expr ('BvSort n) -> Expr ('BvSort n) -> Expr t)
-> Parser (Expr t)
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 t
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
forall (n :: Natural).
KnownNat n =>
Expr ('BvSort n) -> Expr ('BvSort n) -> Expr ('BvSort n)
BvLShR

var :: Parser (Expr t)
var :: forall (t :: SMTSort). Parser (Expr t)
var = do
  ByteString
_     <- ByteString -> Parser ByteString
string ByteString
"var_"
  Key
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
$ Key -> SMTVar t
forall a b. Coercible a b => a -> b
coerce Key
vId
{-# INLINEABLE var #-}

constant :: forall t. KnownSMTSort t => Parser (Expr t)
constant :: forall (t :: SMTSort). KnownSMTSort t => Parser (Expr t)
constant = do
  HaskellType t
cval <- case forall (t :: SMTSort). KnownSMTSort t => SSMTSort t
sortSing @t of
    SSMTSort t
SIntSort  -> Parser ByteString (HaskellType t)
-> Parser ByteString (HaskellType t)
forall a. Num a => Parser a -> Parser a
anyValue Parser ByteString (HaskellType t)
forall a. Integral a => Parser a
decimal
    SSMTSort t
SRealSort -> Parser ByteString (HaskellType t)
-> Parser ByteString (HaskellType t)
forall a. Num a => Parser a -> Parser a
anyValue Parser Double
Parser ByteString (HaskellType t)
parseRatioDouble Parser ByteString (HaskellType t)
-> Parser ByteString (HaskellType t)
-> Parser ByteString (HaskellType t)
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 ByteString (HaskellType t)
parseToRealDouble Parser ByteString (HaskellType t)
-> Parser ByteString (HaskellType t)
-> Parser ByteString (HaskellType t)
forall a.
Parser ByteString a -> Parser ByteString a -> Parser ByteString a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Parser ByteString (HaskellType t)
-> Parser ByteString (HaskellType t)
forall a. Num a => Parser a -> Parser a
anyValue Parser ByteString (HaskellType t)
forall a. Fractional a => Parser a
rational
    SSMTSort t
SBoolSort -> Parser Bool
Parser ByteString (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

  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
$ Value t -> Expr t
forall (t :: SMTSort). Value t -> Expr t
Constant (Value t -> Expr t) -> Value t -> Expr t
forall a b. (a -> b) -> a -> b
$ HaskellType t -> Value t
forall (t :: SMTSort). KnownSMTSort t => HaskellType t -> Value t
wrapValue HaskellType t
cval
{-# INLINEABLE constant #-}

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

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 ByteString Integer -> Parser (Bitvec n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Parser ByteString Integer
forall a. (Integral a, Bits a) => Parser a
hexadecimal
{-# INLINEABLE 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 ByteString 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
{-# INLINEABLE literalBitvector #-}

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
{-# INLINEABLE 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
{-# INLINEABLE 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
{-# INLINEABLE 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
{-# INLINEABLE 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
{-# INLINEABLE 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 ByteString Integer
forall a. Integral a => Parser a
decimal
  ()
_           <- Parser ()
skipSpace
  Integer
denominator <- Parser ByteString 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 ByteString Integer -> Parser ByteString Integer
forall a. Num a => Parser a -> Parser a
anyValue Parser ByteString 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]
++ Key -> [Char]
forall a. Show a => a -> [Char]
show (SMTVar t
vSMTVar t -> Getting Key (SMTVar t) Key -> Key
forall s a. s -> Getting a s a -> a
^.Getting Key (SMTVar t) Key
forall (t1 :: SMTSort) (t2 :: SMTSort) (p :: * -> * -> *)
       (f :: * -> *).
(Profunctor p, Functor f) =>
p Key (f Key) -> 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)