Language.Hasmtlib.Internal.Parser

Documentation

answerParser :: Parser (Result, Solution)

resultParser :: Parser Result

anyModelParser :: Parser Solution

defaultModelParser :: Parser Solution

smt2ModelParser :: Parser Solution

parseSomeSol :: Parser (SomeKnownOrdSMTSort SMTVarSol)

parseSomeSort :: Parser (SomeKnownOrdSMTSort SSMTSort)

parseSomeBitVecSort :: Parser (SomeKnownOrdSMTSort SSMTSort)

parseSomeArraySort :: Parser (SomeKnownOrdSMTSort SSMTSort)

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

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

var :: KnownSMTSort t => Parser (Expr t)

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

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

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

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

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

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

constArray :: forall k v. (KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Proxy v -> Parser (ConstArray (HaskellType k) (HaskellType v))

parseSmtString :: Parser Text

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

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

ternary :: forall t u v r. (KnownSMTSort t, KnownSMTSort u, KnownSMTSort v) => ByteString -> (Expr t -> Expr u -> Expr v -> Expr r) -> Parser (Expr r)

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

smtPi :: Parser (Expr RealSort)

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

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

parseRational :: Parser Rational

parseToRealRational :: Parser Rational

parseBool :: Parser Bool

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