Module FCY2SMTLib

updTypeEnv :: [Int] -> TypeExpr -> [Int] -> SMTTrans ()   

Update the type environment possibly specializing type information for existing entries

hasTypeInfo :: Int -> SMTInfo -> Bool   

Check, if there is type information for the given variable

specTypes :: SMTInfo -> FM Int TypeExpr -> Int -> TypeInfo -> TypeInfo   

Specialize type information applying the given type substitution

typeInfo :: SMTInfo -> TypeExpr -> [Int] -> TypeInfo   

Generate a new TypeInfo object

rnmTVars :: TypeExpr -> SMTTrans TypeExpr   

Rename all type variables in the given type expression

freshTVars :: Int -> SMTTrans [Int]   

Get n fresh type variable indices

declConst :: Int -> TypeInfo -> Command   

Generate a single SMT-LIB constant declaration

declConsts :: SMTInfo -> [Int] -> [Command]   

Generate SMT-LIB constant declarations for the given indices

assertConstr :: SMTInfo -> [(Int,SymObj,[Int])] -> CoveredCs -> Int -> Int -> Command   

Generate SMT-LIB assertions for the given path constraints

pc2SMT :: SMTInfo -> (Int,SymObj,[Int]) -> Term   

Transform path constraints to SMT-LIB constraints

initSMTInfo :: SMTInfo   

get :: SMTTrans SMTInfo   

put :: SMTInfo -> SMTTrans ()   

modify :: (SMTInfo -> SMTInfo) -> SMTTrans ()   

execSMTTrans :: SMTTrans a -> SMTInfo -> SMTInfo   

Execute an SMT transformation

addSMTDecl :: Command -> SMTTrans ()   

Add an SMT datatype declaration

lookupSMTCons :: SymObj -> SMTInfo -> Maybe String   

Lookup the SMT constructor for the given FlatCurry constructor

lookupFCYCons :: String -> SMTInfo -> Maybe SymObj   

Lookup the FlatCurry constructor for the given SMT constructor

lookupType :: (String,String) -> SMTInfo -> Maybe String   

Lookup the SMT type for the given FlatCurry type

getFCYType :: Int -> SMTInfo -> TypeExpr   

Get FlatCurry type information for the given SMT-LIB variable

getSMTSort :: SMTInfo -> Int -> Sort   

Get SMT-LIB sort information for the given SMT-LIB variable

getArgs :: Int -> SMTInfo -> [Int]   

Get the arguments for the given SMT-LIB variable

newSMTSort :: (String,String) -> SMTTrans String   

Lookup or generate SMTLib sort representation for the given FlatCurry type

newSMTCons :: SymObj -> SMTTrans ()   

Create an SMTLib constructor for the given typed FlatCurry constructor

fcy2SMT :: [TypeDecl] -> SMTInfo   

tdecl2SMT :: TypeDecl -> SMTTrans ()   

newDT :: [Int] -> [ConsDecl] -> DTDecl   

cdecl2SMT :: TypeExpr -> ConsDecl -> SMTTrans ConsDecl   

ty2SMT :: TypeExpr -> SMTTrans Sort   

cons2SMT :: SMTInfo -> SymObj -> Int -> QIdent   

Transform a FlatCurry constructor to an SMT-LIB identifier

lc2SMT :: LConstr -> Term -> Term -> Term   

Transform a literal constraint to SMT-LIB

Further infos:

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

lit2SMT :: Literal -> Term   

Transform a FlatCurry literal to SMT-LIB

fromTerm :: SMTInfo -> Int -> Term -> AExpr (TypeExpr,Maybe Int,Bool)   

Transform an SMT-LIB term into a FlatCurry expression

fromSpecConst :: SpecConstant -> AExpr TypeExpr   

Transform an SMT-LIB spec constant into a FlatCurry expression

toSort :: SMTInfo -> TypeExpr -> Sort   

Transform a FlatCurry type expression into an SMTLib sort

typeVars :: [String]   

infinite list of type variables

predefTypes :: BM (String,String) String   

predefined SMTLib representations predefined basic types and type constructors

predefCons :: BM SymObj String   

predefined constructors

ignoredTypes :: [String]   

data types which are ignored regarding the generation of SMT data type declarations

Further infos:

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

genTpl :: Int -> (SymObj,String)   

mkTplType :: String -> Int -> SymObj