Module Curry2SMT

funcs2SMT :: IORef VState -> [(String,String)] -> IO Command   

Translates a list of operations specified by their qualified name (together with all operations on which these operation depend on) into an SMT string that axiomatizes their semantics.

fun2SMT :: AFuncDecl TypeExpr -> ([String],FunSig,Term)   

simpArith :: AExpr TypeExpr -> AExpr TypeExpr   

exp2SMT :: Maybe Term -> AExpr TypeExpr -> Term   

patternTest :: APattern TypeExpr -> Term -> Term   

constructorTest :: (String,String) -> Term -> TypeExpr -> Term   

Translates a constructor name and a term into a SMT formula implementing a test on the term for this constructor.

selectors :: (String,String) -> [String]   

Computes the SMT selector names for a given constructor.

polytype2sort :: TypeExpr -> Sort   

Translates a FlatCurry type expression into a corresponding SMT sort. Polymorphic type variables are translated into the sort TVar. The types TVar and Func are defined in the SMT prelude which is always loaded.

polytype2psort :: TypeExpr -> Sort   

Translates a FlatCurry type expression into a parameter SMT sort. Thus, a polymorphic type variable i is translated into the sort TVari. These type variables are later processed by the SMT translator.

type2sort :: [(String,String)] -> Bool -> Bool -> TypeExpr -> Sort   

Translates a FlatCurry type expression into a corresponding SMT sort. If the first argument is null, then type variables are translated into the sort TVar. If the second argument is true, the type variable index is appended (TVari) in order to generate a polymorphic sort (which will later be translated by the SMT translator). If the first argument is not null, we are in the translation of the types of selector operations and the first argument contains the currently defined data types. In this case, type variables are translated into Ti, but further nesting of the defined data types are not allowed (since this is not supported by SMT). The types TVar and Func are defined in the SMT prelude which is always loaded.

tcons2SMT :: (String,String) -> String   

Translates a FlatCurry type constructor name into SMT.

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.

pat2smt :: APattern TypeExpr -> Term   

Translates a pattern into an SMT expression.

lit2smt :: Literal -> Term   

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

transOpName :: (String,String) -> String   

Translates a qualified FlatCurry name into an SMT string.

encodeSpecialChars :: String -> String   

Encode special characters in strings

decodeSpecialChars :: String -> String   

Translates urlencoded string into equivalent ASCII 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.