Language.Hasmtlib.Internal.Parser

Documentation

answerParser :: Parser (Result, Solution)

resultParser :: Parser Result

anyModelParser :: Parser Solution

defaultModelParser :: Parser Solution

smt2ModelParser :: Parser Solution

fromSomeList :: [SomeKnownSMTSort SMTVarSol] -> Solution

parseSomeSol :: Parser (SomeKnownSMTSort SMTVarSol)

parseAnyBvUpToLength :: Natural -> Parser (SomeKnownSMTSort SMTVarSol)

parseSol :: forall t. KnownSMTSort t => Parser (SMTVarSol t)

parseExpr :: forall t. KnownSMTSort t => Parser (Expr t)

var :: Parser (Expr t)

constant :: forall t. KnownSMTSort t => Parser (Expr t)

anyBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)

binBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)

hexBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)

literalBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)

unary :: forall t r. KnownSMTSort t => ByteString -> (Expr t -> Expr r) -> Parser (Expr r)

binary :: forall t r. KnownSMTSort t => ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)

nary :: forall t r. KnownSMTSort t => ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r)

smtPi :: Parser (Expr RealSort)

toRealFun :: Parser (Expr RealSort)

toIntFun :: Parser (Expr IntSort)

isIntFun :: Parser (Expr BoolSort)

smtIte :: forall t. KnownSMTSort t => Parser (Expr t)

anyValue :: Num a => Parser a -> Parser a

negativeValue :: Num a => Parser a -> Parser a

parseRatioDouble :: Parser Double

parseToRealDouble :: Parser Double

parseBool :: Parser Bool

getValueParser :: KnownSMTSort t => SMTVar t -> Parser (SMTVarSol t)