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 :: Parser (Expr t)

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

constantExpr :: 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)

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

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

parseStore :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Parser (Expr (ArraySort k v))

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)