| Safe Haskell | Safe-Inferred |
|---|
Hsmtlib.Solvers.Cmd.Parser.CmdResult
- 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
- getBitVec' :: Maybe String -> Maybe String -> Maybe GValResult
- getFun :: ValuationPair -> Maybe GValResult
- getFun' :: Maybe String -> Maybe Value -> Maybe GValResult
- getVar :: ValuationPair -> Maybe GValResult
- getVar' :: Maybe String -> Maybe Integer -> Maybe GValResult
- getArray :: ValuationPair -> Maybe GValResult
- getArray' :: Maybe String -> Maybe Integer -> Maybe String -> Maybe Integer -> Maybe Arrays
- isArray :: ValuationPair -> Maybe Bool
- isArray' :: String -> Maybe Bool
- arrayName :: ValuationPair -> Maybe String
- arrayIntPos :: ValuationPair -> Maybe Integer
- arrayVarPos :: ValuationPair -> Maybe String
- arrayVal :: ValuationPair -> Maybe Integer
- getVarName :: ValuationPair -> Maybe String
- getVarValue :: ValuationPair -> Maybe Integer
- getFunName :: ValuationPair -> Maybe String
- getFunResult :: ValuationPair -> Maybe Value
- 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
- fstTerm :: ValuationPair -> Maybe Term
- sndTerm :: ValuationPair -> Maybe Term
- sndTermQualIdentierT :: Term -> Maybe [Term]
- 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
Documentation
genResponse :: String -> GenResultSource
checkSatResponse :: String -> SatResultSource
getValueResponse :: String -> GValResultSource
getVR' :: [GValResult] -> GValResultSource
getValResponse :: [ValuationPair] -> [GValResult]Source
valErrors' :: [ValuationPair] -> [Maybe GValResult] -> [GValResult]Source
joinArrays :: [Maybe GValResult] -> [GValResult]Source
joinArrays' :: GValResult -> [Maybe GValResult] -> [GValResult]Source
checkGVal :: GValResult -> Maybe GValResult -> GValResultSource
getValResponses :: [ValuationPair] -> [Maybe GValResult]Source
getGValResult :: ValuationPair -> Maybe GValResultSource
getBitVec :: ValuationPair -> Maybe GValResultSource
Retrives the value of a BitVector. Works with: - Z3.
getBitVec' :: Maybe String -> Maybe String -> Maybe GValResultSource
getFun :: ValuationPair -> Maybe GValResultSource
Retrives the value of a function. Works with: - Z3.
getFun' :: Maybe String -> Maybe Value -> Maybe GValResultSource
getVar :: ValuationPair -> Maybe GValResultSource
Retrives the value of a variable. Works with: - Z3.
getVar' :: Maybe String -> Maybe Integer -> Maybe GValResultSource
getArray :: ValuationPair -> Maybe GValResultSource
Retrives the value of an array. Works with: - Z3.
isArray :: ValuationPair -> Maybe BoolSource
isArray' :: String -> Maybe BoolSource
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 StringSource
Retrives the name of the array. Works with: - Z3.
arrayIntPos :: ValuationPair -> Maybe IntegerSource
Retrives the position of the array if it is an Integer. Works with: - Z3.
arrayVarPos :: ValuationPair -> Maybe StringSource
Retrives the position of the array if it is a String. Works with: - Z3.
arrayVal :: ValuationPair -> Maybe IntegerSource
Retrives the value of an array. Works with: - Z3.
getVarName :: ValuationPair -> Maybe StringSource
Retrive the name of a variable. Works with: - Z3.
getVarValue :: ValuationPair -> Maybe IntegerSource
Retrive the variable of a variable. Works with: - Z3.
getFunName :: ValuationPair -> Maybe StringSource
Retrives the name of a function. Works with: - Z3
getFunResult :: ValuationPair -> Maybe ValueSource
Retrives the result of a function if it is a Integer. Works with: - Z3.
getFunResultBool :: ValuationPair -> Maybe ValueSource
getFunResultInt :: ValuationPair -> Maybe ValueSource
getFunResultInt' :: ValuationPair -> Maybe IntegerSource
getFunResultBool' :: ValuationPair -> Maybe StringSource
getHexVal :: ValuationPair -> Maybe StringSource
Retrives the result of a bitvector. Works with: - Z3
fstTerm :: ValuationPair -> Maybe TermSource
Returns the first term of a valuation pair.
sndTerm :: ValuationPair -> Maybe TermSource
Returns the second term of a valuation pair.
sndTermQualIdentierT :: Term -> Maybe [Term]Source
Returns the list of terms from TermQualIdeintifierT
fstTermQualIdentierT :: Term -> Maybe QualIdentifierSource
termQualIdentifier :: Term -> Maybe QualIdentifierSource
getTermSpecConstant :: Term -> Maybe SpecConstantSource
qIdentifier :: QualIdentifier -> Maybe IdentifierSource
symbol :: Identifier -> Maybe StringSource
numeral :: SpecConstant -> Maybe IntegerSource
hex :: SpecConstant -> Maybe StringSource