Module Curry2SMT

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

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.

ftype2SMT :: AFuncDecl TypeExpr -> String   

fdecl2SMT :: AFuncDecl TypeExpr -> String   

exp2SMT :: Maybe BoolExp -> AExpr TypeExpr -> BoolExp   

patternTest :: APattern TypeExpr -> BoolExp -> BoolExp   

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

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

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

Computes the SMT selector names for a given constructor.

polytype2SMTExp :: TypeExpr -> BoolExp   

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

type2SMTExp :: [(String,String)] -> Bool -> TypeExpr -> BoolExp   

Translates a FlatCurry type expression into a corresponding SMT expression. If the first argument is null, then type variables are translated into the sort TVar, otherwise 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.

Further infos:

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

tdecl2SMT :: TypeDecl -> String   

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.

pat2bool :: APattern TypeExpr -> BoolExp   

Translates a pattern into an SMT expression.

lit2bool :: Literal -> BoolExp   

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.

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

Translates an SMT string into qualified FlatCurry name. Returns Nothing if it was not a qualified name.