Module Verify.WithSMT

Some operations to translate FlatCurry operations into SMT assertions.

Author: Michael Hanus

Version: March 2024

Summary of exported operations:

checkUnsatisfiabilityWithSMT :: Options -> (String,String) -> String -> IORef ProgInfo -> [((String,String),(Int,ConsType,[((String,String),Int)]))] -> [(Int,TypeExpr)] -> Expr -> IO (Maybe Bool)  Non-deterministic 
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)  Non-deterministic 
readIncludeFile :: String -> IO String  Deterministic 
Try to read a file in the include directory of the package
typedVar2SMT :: (Int,TypeExpr) -> Command  Deterministic 
tconsOfTypeExpr :: TypeExpr -> [(String,String)]  Deterministic 
allQNamesInExp :: Expr -> [Either (String,String) (String,String)]  Deterministic 
showWithLineNums :: String -> String  Deterministic 
Shows a text with line numbers prefixed:
ilog :: Int -> Int  Deterministic 
The value of ilog n is the floor of the logarithm in the base 10 of n.
tdecl2SMT :: TypeDecl -> Command  Deterministic 
Translates a type declaration into an SMT datatype declaration.
genSelName :: (String,String) -> Int -> String  Deterministic 
Generates the name of the i-th selector for a given constructor.
preludeType2SMT :: String -> [Command]  Deterministic 
Translates a prelude type into an SMT datatype declaration, if necessary.
fun2SMT :: FuncDecl -> Maybe ([String],FunSig,Term)  Deterministic 
ndExpr :: Expr -> Bool  Deterministic 
Returns True if the expression is non-deterministic, i.e., if Or or Free occurs in the expression.
replaceHigherOrderInExp :: Expr -> Expr  Deterministic 
exp2SMTWithVars :: Int -> Maybe Term -> Expr -> Maybe (Term,[(Int,Sort)])  Deterministic 
exp2SMT :: Maybe Term -> Expr -> Maybe Term  Deterministic 
isTyped :: Expr -> Bool  Deterministic 
Is a expression typed? (should go into FlatCurry.Goodies)
exprType :: Expr -> TypeExpr  Deterministic 
Gets the type of a typed expression.
lit2SMT :: Literal -> Term  Deterministic 
Translates a literal into an SMT expression.
elimFailed :: Int -> Term -> (Term,[(Int,Sort)])  Deterministic 
elimFailedInTerm :: Term -> StateT TransApplyState Identity Term  Deterministic 
allVarsInTerm :: Term -> [Int]  Deterministic 
varOfSV :: SortedVar -> Int  Deterministic 
type2sort :: TypeExpr -> Sort  Deterministic 
Translates a FlatCurry type expression into a corresponding SMT sort.
type2sortD :: Bool -> TypeExpr -> Sort  Deterministic 
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  Deterministic 
Translates a FlatCurry type constructor name into SMT.
transPrimTCons :: [(String,String)]  Deterministic 
Primitive type constructors from the prelude and their SMT names.
encodeSpecialChars :: String -> String  Deterministic 
Encode special characters in strings
decodeSpecialChars :: String -> String  Deterministic 
Translates urlencoded string into equivalent ASCII string.
transOpName :: (String,String) -> String  Deterministic 
Translates a qualified FlatCurry name into an SMT string.
untransOpName :: String -> Maybe (String,String)  Deterministic 
Translates a (translated) SMT string back into qualified FlatCurry name.
primNames :: [(String,String)]  Deterministic 
Some primitive names of the prelude and their SMT names.
getAllFunctions :: Options -> IORef ProgInfo -> [(String,String)] -> IO [FuncDecl]  Non-deterministic 
Extract all user-defined FlatCurry functions that might be called by a given list of function names provided as the last argument.
usedFunctions :: [(String,String)] -> [FuncDecl] -> [FuncDecl]  Deterministic 
Removes from a list of function declarations the functions not used by an initial list of function names.
loadModulesForQNames :: Options -> IORef ProgInfo -> [(String,String)] -> IO ()  Non-deterministic 
Extract all user-defined FlatCurry functions that might be called by a given list of function names provided as the last argument.
preloadedFuncDecls :: [FuncDecl]  Deterministic 
excludedCurryOperations :: [(String,String)]  Deterministic 
Exclude character-related operations since characters are treated as integers so that these operations are not required.
funcsOfFuncDecl :: FuncDecl -> [(String,String)]  Deterministic 
Returns the names of all functions occurring in the body of a function declaration.

Exported datatypes:


TransApplyState

Constructors:

  • TransApplyState :: Int -> [(Int,Sort)] -> TransApplyState

    Fields:

    • tsFreshVarIndex :: Int
    • tsNewVars :: [(Int,Sort)]

TAState

Type synonym: TAState a = State TransApplyState a


Exported operations:

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

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)  Non-deterministic 

readIncludeFile :: String -> IO String  Deterministic 

Try to read a file in the include directory of the package

typedVar2SMT :: (Int,TypeExpr) -> Command  Deterministic 

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

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

showWithLineNums :: String -> String  Deterministic 

Shows a text with line numbers prefixed:

ilog :: Int -> Int  Deterministic 

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.
Further infos:
  • partially defined

tdecl2SMT :: TypeDecl -> Command  Deterministic 

Translates a type declaration into an SMT datatype declaration.

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

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

Further infos:
  • partially defined

preludeType2SMT :: String -> [Command]  Deterministic 

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

Further infos:
  • partially defined

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

ndExpr :: Expr -> Bool  Deterministic 

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

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

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

isTyped :: Expr -> Bool  Deterministic 

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

exprType :: Expr -> TypeExpr  Deterministic 

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

lit2SMT :: Literal -> Term  Deterministic 

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

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

elimFailedInTerm :: Term -> StateT TransApplyState Identity Term  Deterministic 

Further infos:
  • partially defined

allVarsInTerm :: Term -> [Int]  Deterministic 

varOfSV :: SortedVar -> Int  Deterministic 

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

type2sort :: TypeExpr -> Sort  Deterministic 

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  Deterministic 

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  Deterministic 

Translates a FlatCurry type constructor name into SMT.

Further infos:
  • partially defined

transPrimTCons :: [(String,String)]  Deterministic 

Primitive type constructors from the prelude and their SMT names.

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

encodeSpecialChars :: String -> String  Deterministic 

Encode special characters in strings

decodeSpecialChars :: String -> String  Deterministic 

Translates urlencoded string into equivalent ASCII string.

Further infos:
  • partially defined

transOpName :: (String,String) -> String  Deterministic 

Translates a qualified FlatCurry name into an SMT string.

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

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

primNames :: [(String,String)]  Deterministic 

Some primitive names of the prelude and their SMT names.

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

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]  Deterministic 

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

Further infos:
  • partially defined

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

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]  Deterministic 

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

excludedCurryOperations :: [(String,String)]  Deterministic 

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

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

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