PAKCS
Exported names: Imported modules:

Module XFD.SMTLib.RDParser

This module implements a parser for programs and formulas in the SMT-LIB2 syntax. It is based on the system library XFD.Parser which defines deterministic parsing combinators.

Summary of exported operations:

parse :: String -> Either String CmdResponse   
parseCmdResult :: [Token] -> Either String ([Token],CmdResponse)   
parseCmdCheckSatResponse :: [Token] -> Either String ([Token],CmdResponse)   
parseCmdGetValueResponse :: [Token] -> Either String ([Token],CmdResponse)   
parseGetValueResponse :: [Token] -> Either String ([Token],[ValuationPair])   
parseValuePair :: [Token] -> Either String ([Token],ValuationPair)   
parseTerm :: [Token] -> Either String ([Token],Term)   
parseCmdGenResponse :: [Token] -> Either String ([Token],CmdResponse)   
parseErrorResponse :: [Token] -> Either String ([Token],GenResponse)   
parseString :: [Token] -> Either String ([Token],String)   

Exported operations:

parse :: String -> Either String CmdResponse   

parseCmdResult :: [Token] -> Either String ([Token],CmdResponse)   

parseCmdCheckSatResponse :: [Token] -> Either String ([Token],CmdResponse)   

parseCmdGetValueResponse :: [Token] -> Either String ([Token],CmdResponse)   

parseGetValueResponse :: [Token] -> Either String ([Token],[ValuationPair])   

parseValuePair :: [Token] -> Either String ([Token],ValuationPair)   

parseTerm :: [Token] -> Either String ([Token],Term)   

parseCmdGenResponse :: [Token] -> Either String ([Token],CmdResponse)   

parseErrorResponse :: [Token] -> Either String ([Token],GenResponse)   

parseString :: [Token] -> Either String ([Token],String)