Module Curry2SMT

m1 :: IO ()   

m2 :: IO ()   

funcs2SMT :: [(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   

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

type2SMTExp :: TypeExpr -> BoolExp   

Translates a FlatCurry type expression into a corresponding SMT expression.

pat2bool :: APattern TypeExpr -> BoolExp   

Translates a pattern into an SMT expression.

lit2bool :: Literal -> BoolExp   

Translates a literal into an SMT expression.

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.