Hsmtlib.Solvers.Cmd.Parser.CmdResult

Documentation

genResponse :: String -> GenResult

checkSatResponse :: String -> SatResult

getValueResponse :: String -> GValResult

getVR' :: [GValResult] -> GValResult

getValResponse :: [ValuationPair] -> [GValResult]

valErrors' :: [ValuationPair] -> [Maybe GValResult] -> [GValResult]

joinArrays :: [Maybe GValResult] -> [GValResult]

joinArrays' :: GValResult -> [Maybe GValResult] -> [GValResult]

checkGVal :: GValResult -> Maybe GValResult -> GValResult

getValResponses :: [ValuationPair] -> [Maybe GValResult]

getGValResult :: ValuationPair -> Maybe GValResult

getBitVec :: ValuationPair -> Maybe GValResult

Retrives the value of a BitVector. Works with: - Z3.

getBitVec' :: Maybe String -> Maybe String -> Maybe GValResult

getFun :: ValuationPair -> Maybe GValResult

Retrives the value of a function. Works with: - Z3.

getFun' :: Maybe String -> Maybe Value -> Maybe GValResult

getVar :: ValuationPair -> Maybe GValResult

Retrives the value of a variable. Works with: - Z3.

getVar' :: Maybe String -> Maybe Integer -> Maybe GValResult

getArray :: ValuationPair -> Maybe GValResult

Retrives the value of an array. Works with: - Z3.

getArray' :: Maybe String -> Maybe Integer -> Maybe String -> Maybe Integer -> Maybe Arrays

isArray :: ValuationPair -> Maybe Bool

isArray' :: String -> Maybe Bool

Verifies if the string correspond to a certain notation that indicates that is an Array. For example Z3 would have the keyword select therefor it's an array. If it isn't an array then returns nothing

arrayName :: ValuationPair -> Maybe String

Retrives the name of the array. Works with: - Z3.

arrayIntPos :: ValuationPair -> Maybe Integer

Retrives the position of the array if it is an Integer. Works with: - Z3.

arrayVarPos :: ValuationPair -> Maybe String

Retrives the position of the array if it is a String. Works with: - Z3.

arrayVal :: ValuationPair -> Maybe Integer

Retrives the value of an array. Works with: - Z3.

getVarName :: ValuationPair -> Maybe String

Retrive the name of a variable. Works with: - Z3.

getVarValue :: ValuationPair -> Maybe Integer

Retrive the variable of a variable. Works with: - Z3.

getFunName :: ValuationPair -> Maybe String

Retrives the name of a function. Works with: - Z3

getFunResult :: ValuationPair -> Maybe Value

Retrives the result of a function if it is a Integer. Works with: - Z3.

getFunResultBool :: ValuationPair -> Maybe Value

getFunResultInt :: ValuationPair -> Maybe Value

(<#>) :: Functor m => (b -> c) -> (a -> m b) -> a -> m c

toBool :: String -> Maybe Bool

getFunResultInt' :: ValuationPair -> Maybe Integer

getFunResultBool' :: ValuationPair -> Maybe String

getHexVal :: ValuationPair -> Maybe String

Retrives the result of a bitvector. Works with: - Z3

fstTerm :: ValuationPair -> Maybe Term

Returns the first term of a valuation pair.

sndTerm :: ValuationPair -> Maybe Term

Returns the second term of a valuation pair.

sndTermQualIdentierT :: Term -> Maybe [Term]

Returns the list of terms from TermQualIdeintifierT

fstTermQualIdentierT :: Term -> Maybe QualIdentifier

termQualIdentifier :: Term -> Maybe QualIdentifier

getTermSpecConstant :: Term -> Maybe SpecConstant

qIdentifier :: QualIdentifier -> Maybe Identifier

symbol :: Identifier -> Maybe String

numeral :: SpecConstant -> Maybe Integer

hex :: SpecConstant -> Maybe String