| Safe Haskell | Safe-Inferred |
|---|
Hsmtlib.HighLevel
Description
This Module provide auxiliar functions that simplify writing expressions to send to the solver.
- functionArg :: Name -> [Expr] -> Expr
- constant :: String -> Expr
- assertDistinct :: Solver -> [Expr] -> IO GenResult
- literal :: Int -> Expr
- mapAssert :: Solver -> [Expr] -> IO ()
- maping :: Solver -> (a -> Expr) -> [a] -> IO ()
- declFun :: Solver -> String -> [Type] -> Type -> IO GenResult
- defFun :: Solver -> String -> [Binder] -> Type -> Expr -> IO GenResult
- bind :: String -> Type -> Binder
- declConst :: Solver -> String -> Type -> IO GenResult
- mapDeclConst :: Solver -> [String] -> Type -> IO ()
- getPos :: Show a => Solver -> String -> a -> IO GValResult
- declType :: Solver -> String -> Integer -> IO GenResult
- produceModels :: Solver -> IO GenResult
- interactiveMode :: Solver -> IO GenResult
Documentation
functionArg :: Name -> [Expr] -> ExprSource
This function hides the application of a function on the SMT syntax receives the name of the function and the args and gives the corresponding SMT2Lib syntax.
constant :: String -> ExprSource
This function hides the application of a constant function on the SMT syntax receives the name of the function and gives the corresponding SMT2Lib syntax, the function must be already declared using declareFun.
assertDistinct :: Solver -> [Expr] -> IO GenResultSource
This function hides the application of distinct on the SMT syntax receives the solver and a list of the expressions which must be distinct and gives the corresponding SMT2Lib syntax.
This function hides Integers on the SMT syntax receives a integer and gives the corresponding SMT2Lib syntax.
mapAssert :: Solver -> [Expr] -> IO ()Source
This function allows the user to given a list of expressions make a assert of them giving the SMTLib2 syntax corespondant (auxiliary function for maping).
maping :: Solver -> (a -> Expr) -> [a] -> IO ()Source
This function when giving a solver and a function that gives an Expr and a list of the input type of that function, asserts the map of expressions its particulary useful to say that some set variables are all for example greater than zero.
declFun :: Solver -> String -> [Type] -> Type -> IO GenResultSource
This function hides the name creation on the SMT syntax receives a string and gives the corresponding SMT2Lib syntax for declaring a function.
declConst :: Solver -> String -> Type -> IO GenResultSource
This function hides Constants implemnted as functions without arguments on the SMT syntax receives a String and a type and gives the corresponding SMT2Lib syntax for declaring a constant function.
mapDeclConst :: Solver -> [String] -> Type -> IO ()Source
This function hides Constants implemnted as functions without arguments on the SMT syntax receives a String and a type and gives the corresponding SMT2Lib syntax for declaring a constant function.
getPos :: Show a => Solver -> String -> a -> IO GValResultSource
This function hides the way to access an array (Hammered version) on the SMT syntax receives a integer and gives the corresponding SMT2Lib syntax.
declType :: Solver -> String -> Integer -> IO GenResultSource
This function hides the Name Type in the declare type comand
produceModels :: Solver -> IO GenResultSource
This function simplifies the command to set the option to Produce Models.
interactiveMode :: Solver -> IO GenResultSource
This function simplifies the command to set the option to Interactive Mode.