Hsmtlib-0.2.0.6: Haskell library for easy interaction with SMT-LIB 2 compliant solvers.

Safe HaskellSafe-Inferred
LanguageHaskell2010

Hsmtlib.Solvers.Cmd.Parser.CmdResult

Synopsis

Documentation

getBitVec :: ValuationPair -> Maybe GValResult Source

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

getFun :: ValuationPair -> Maybe GValResult Source

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

getVar :: ValuationPair -> Maybe GValResult Source

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

getArray :: ValuationPair -> Maybe GValResult Source

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

isArray' :: String -> Maybe Bool Source

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 Source

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

arrayIntPos :: ValuationPair -> Maybe Integer Source

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

arrayVarPos :: ValuationPair -> Maybe String Source

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

arrayVal :: ValuationPair -> Maybe Integer Source

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

getVarName :: ValuationPair -> Maybe String Source

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

getVarValue :: ValuationPair -> Maybe Integer Source

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

getFunName :: ValuationPair -> Maybe String Source

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

getFunResult :: ValuationPair -> Maybe Value Source

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

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

getHexVal :: ValuationPair -> Maybe String Source

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

fstTerm :: ValuationPair -> Maybe Term Source

Returns the first term of a valuation pair.

sndTerm :: ValuationPair -> Maybe Term Source

Returns the second term of a valuation pair.

sndTermQualIdentierT :: Term -> Maybe [Term] Source

Returns the list of terms from TermQualIdeintifierT