| java.lang.Object de.uka.ilkd.key.proof.decproc.translation.CreateTypePred
CreateTypePred | public class CreateTypePred (Code) | | This class is responsible for creating and managing type (guard) predicates
Type predicates are needed to support the SMT logic AUFLIA (quanitifier support).
author: akuwertz version: 1.1, 12/17/2006 |
areVarsGuarded | boolean areVarsGuarded(Code) | | A boolean indicating if any quantified variables have been type guarded
|
CreateTypePred | public CreateTypePred(Services services)(Code) | | Just a mere constructor
Parameters: services - the Services used during current translation |
createObjHierarchyPreds | protected Vector createObjHierarchyPreds()(Code) | | Returns a Vector containing all hierarchy predicates needed for the current
translation
The hierarchy predicates are calculated by searching for the most direct occuring
supersort of each occuring sort.
All supersorts occuring in the current sequent must be present in the limitingObjectSorts
Set
the Vector of created hierarchy predicates |
createTypePredUif | protected void createTypePredUif(Sort type, String funcName, int args)(Code) | | Creates and internally stores a unique type predicate for the given Sort with the
given uninterpreted function as argument
The given Sort must be a fully qualified and therefore unique Sort
The given function name must be a legal identifier in AUFLIA (see UninterpretedFuncTerm)
Parameters: type - the Sort to be represented by a type predicate Parameters: funcName - a String denoting the name of the UninterpretedFuncTermto be represented by the created type predicate Parameters: args - the arity of the specified uninterpreted function throws: IllegalArgumentException - if args is negative See Also: UninterpretedFuncTerm |
getCreatedTypePreds | protected Vector getCreatedTypePreds()(Code) | | Returns a Vector containing all type predicates created during the translation
of the current term
the Vector of created type predicates |
getTypePredLv | protected Formula getTypePredLv(Sort type, TermVariable termVar)(Code) | | Creates a type predicate for the given Sort with the given TermVariable
as argument.
The given Sort must be a fully qualified and therefore unique Sort
Parameters: type - the Sort to be represented by a type predicate Parameters: termVar - the Term variable of Sort type to be represented an UninterpretedPredFormula representing the specified type predicate |
|
|