Module Verify.WithSMT

checkUnsatisfiabilityWithSMT :: Options -> (String,String) -> String -> IORef ProgInfo -> [((String,String),(Int,ConsType,[((String,String),Int)]))] -> [(Int,TypeExpr)] -> Expr -> IO (Maybe Bool)   

checkUnsatWithSMT :: Options -> (String,String) -> String -> IORef ProgInfo -> [((String,String),(Int,ConsType,[((String,String),Int)]))] -> [(Int,TypeExpr)] -> [(Int,Sort)] -> Term -> [(String,String)] -> [(String,String)] -> IO (Maybe Bool)   

typedVar2SMT :: (Int,TypeExpr) -> Command   

tconsOfTypeExpr :: TypeExpr -> [(String,String)]   

allQNamesInExp :: Expr -> [Either (String,String) (String,String)]   

showWithLineNums :: String -> String   

Shows a text with line numbers prefixed:

ilog :: Int -> Int   

The value of ilog n is the floor of the logarithm in the base 10 of n. Fails if n <= 0. For positive integers, the returned value is 1 less the number of digits in the decimal representation of n.

Example call:

(ilog n)

Parameters:

• n : The argument.

Returns:

the floor of the logarithm in the base 10 of n.

tdecl2SMT :: TypeDecl -> Command   

Translates a type declaration into an SMT datatype declaration.

genSelName :: (String,String) -> Int -> String   

Generates the name of the i-th selector for a given constructor.

preludeType2SMT :: String -> [Command]   

Translates a prelude type into an SMT datatype declaration, if necessary.

fun2SMT :: FuncDecl -> Maybe ([String],FunSig,Term)   

ndExpr :: Expr -> Bool   

Returns True if the expression is non-deterministic, i.e., if Or or Free occurs in the expression.

replaceHigherOrderInExp :: Expr -> Expr   

exp2SMTWithVars :: Int -> Maybe Term -> Expr -> Maybe (Term,[(Int,Sort)])   

exp2SMT :: Maybe Term -> Expr -> Maybe Term   

isTyped :: Expr -> Bool   

Is a expression typed? (should go into FlatCurry.Goodies)

exprType :: Expr -> TypeExpr   

Gets the type of a typed expression. (should go into FlatCurry.Goodies)

lit2SMT :: Literal -> Term   

Translates a literal into an SMT expression. We represent character as ints.

elimFailed :: Int -> Term -> (Term,[(Int,Sort)])   

elimFailedInTerm :: Term -> StateT TransApplyState Identity Term   

Further infos:

• partially defined

allVarsInTerm :: Term -> [Int]   

varOfSV :: SortedVar -> Int   

Further infos:

• solution complete, i.e., able to compute all solutions

type2sort :: TypeExpr -> Sort   

Translates a FlatCurry type expression into a corresponding SMT sort. Type variables are translated into the sort TVar where a type variable index is appended (TVari) in order to generate a polymorphic sort (which will later be translated by the SMT translator). The types TVar and Func are defined in the SMT prelude which is always loaded.

type2sortD :: Bool -> TypeExpr -> Sort   

Similarly as type2sort but type variables are shown as Ti if the first argument is true, which is used when generating algebraic data tyep declarations.

tcons2SMT :: (String,String) -> String   

Translates a FlatCurry type constructor name into SMT.

transPrimTCons :: [(String,String)]   

Primitive type constructors from the prelude and their SMT names.

Further infos:

• solution complete, i.e., able to compute all solutions

encodeSpecialChars :: String -> String   

Encode special characters in strings

decodeSpecialChars :: String -> String   

Translates urlencoded string into equivalent ASCII string.

transOpName :: (String,String) -> String   

Translates a qualified FlatCurry name into an SMT string.

untransOpName :: String -> Maybe (String,String)   

Translates a (translated) SMT string back into qualified FlatCurry name. Returns Nothing if it was not a qualified name.

primNames :: [(String,String)]   

Some primitive names of the prelude and their SMT names.

getAllFunctions :: Options -> IORef ProgInfo -> [(String,String)] -> IO [FuncDecl]   

Extract all user-defined FlatCurry functions that might be called by a given list of function names provided as the last argument. The second argument is an IORef to the currently loaded modules. Its contents will be extended when necessary.

usedFunctions :: [(String,String)] -> [FuncDecl] -> [FuncDecl]   

Removes from a list of function declarations the functions not used by an initial list of function names. It is assumed that the list of functions is already sorted by dependencies (ealier functions might call later ones).

loadModulesForQNames :: Options -> IORef ProgInfo -> [(String,String)] -> IO ()   

Extract all user-defined FlatCurry functions that might be called by a given list of function names provided as the last argument. The second argument is an IORef to the currently loaded modules. Its contents will be extended when necessary.

preloadedFuncDecls :: [FuncDecl]   

Further infos:

• solution complete, i.e., able to compute all solutions

excludedCurryOperations :: [(String,String)]   

Exclude character-related operations since characters are treated as integers so that these operations are not required.

funcsOfFuncDecl :: FuncDecl -> [(String,String)]   

Returns the names of all functions occurring in the body of a function declaration.