Hsmtlib.HighLevel

This Module provide auxiliar functions that simplify writing expressions to send to the solver.

Documentation

functionArg :: Name -> [Expr] -> Expr

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 -> Expr

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 GenResult

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.

literal :: Int -> Expr

This function hides Integers on the SMT syntax receives a integer and gives the corresponding SMT2Lib syntax.

mapAssert :: Solver -> [Expr] -> IO ()

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 ()

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 GenResult

This function hides the name creation on the SMT syntax receives a string and gives the corresponding SMT2Lib syntax for declaring a function.

defFun :: Solver -> String -> [Binder] -> Type -> Expr -> IO GenResult

bind :: String -> Type -> Binder

This function binds a name to a type, and returns a Binder.

declConst :: Solver -> String -> Type -> IO GenResult

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 ()

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 GValResult

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 GenResult

This function hides the Name Type in the declare type comand

produceModels :: Solver -> IO GenResult

This function simplifies the command to set the option to Produce Models.

interactiveMode :: Solver -> IO GenResult

This function simplifies the command to set the option to Interactive Mode.