Module Curry2SMT

funcs2SMT :: Options -> IORef VState -> [(String,String)] -> IO (Command,[AFuncDecl TypeExpr],[((String,String),Bool)])   

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. Non-deterministic operations are axiomatized by the "planned choice" translation (see module FlatCurry.Typed.NonDet2Det). In order to call them correctly, a list of qualified operation names together with their non-determinism status (True means non-deterministic) is also returned.

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

exp2SMT :: AExpr TypeExpr -> Term   

patternTest :: APattern TypeExpr -> Term -> Term   

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

Translates a constructor name and a term into an SMT formula implementing a test on the term for this constructor. If the first argument is true, parametric sorts are used (i.e., we translate a polymorphic function), otherwise type variables are translated into the sort TVar.

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

preludeSort2SMT :: String -> [Command]   

Translates a prelude sort (with SMT name) into an SMT datatype declaration, if necessary.

pairType :: [Command]   

Further infos:

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

maybeType :: [Command]   

Further infos:

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

eitherType :: [Command]   

Further infos:

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

orderingType :: [Command]   

Further infos:

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

unitType :: [Command]   

Further infos:

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

dictType :: [Command]   

Further infos:

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

cons2SMT :: Bool -> Bool -> (String,String) -> TypeExpr -> QIdent   

Translates a qualifed name with given result type into an SMT identifier. If the first argument is true and the result type is not a base type, the type is attached via (as ...) to resolve overloading problems in SMT. If the second argument is true, parametric sorts are used (i.e., we translate a polymorphic function), otherwise type variables are translated into the sort TVar.

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.