| java.lang.Object de.uka.ilkd.key.rule.TacletApp de.uka.ilkd.key.rule.NoPosTacletApp de.uka.ilkd.key.rule.UninstantiatedNoPosTacletApp
UninstantiatedNoPosTacletApp | class UninstantiatedNoPosTacletApp extends NoPosTacletApp (Code) | | A subclass of NoPosTacletApp for the special case of a
taclet app without any instantiations. The method
setupMatchConditions is overwritten to avoid object
creations.
|
UninstantiatedNoPosTacletApp | UninstantiatedNoPosTacletApp(Taclet taclet)(Code) | | Parameters: taclet - |
Methods inherited from de.uka.ilkd.key.rule.NoPosTacletApp | public TacletApp addInstantiation(SchemaVariable sv, Term term, boolean interesting)(Code)(Java Doc) public TacletApp addInstantiation(SchemaVariable sv, Object[] list, boolean interesting)(Code)(Java Doc) public TacletApp addInstantiation(SchemaVariable sv, ProgramElement pe, boolean interesting)(Code)(Java Doc) public TacletApp addInstantiation(SVInstantiations svi)(Code)(Java Doc) protected static boolean checkVarCondNotFreeIn(Taclet taclet, SVInstantiations instantiations)(Code)(Java Doc) public boolean complete()(Code)(Java Doc) protected SetOfQuantifiableVariable contextVars(SchemaVariable sv)(Code)(Java Doc) public static NoPosTacletApp createFixedNoPosTacletApp(Taclet taclet, SVInstantiations instantiations, Constraint constraint)(Code)(Java Doc) public static NoPosTacletApp createNoPosTacletApp(Taclet taclet)(Code)(Java Doc) public static NoPosTacletApp createNoPosTacletApp(Taclet taclet, SVInstantiations instantiations)(Code)(Java Doc) public static NoPosTacletApp createNoPosTacletApp(Taclet taclet, SVInstantiations instantiations, Constraint matchConstraint, SetOfMetavariable matchNewMetavariables)(Code)(Java Doc) public static NoPosTacletApp createNoPosTacletApp(Taclet taclet, SVInstantiations instantiations, Constraint matchConstraint, SetOfMetavariable matchNewMetavariables, ListOfIfFormulaInstantiation ifInstantiations)(Code)(Java Doc) public static NoPosTacletApp createNoPosTacletApp(Taclet taclet, MatchConditions matchCond)(Code)(Java Doc) public boolean equalContractable(Contractable c)(Code)(Java Doc) public boolean equals(Object o)(Code)(Java Doc) public int hashCode()(Code)(Java Doc) public NoPosTacletApp matchFind(PosInOccurrence pos, Constraint termConstraint, Services services, Constraint userConstraint)(Code)(Java Doc) public NoPosTacletApp matchFind(PosInOccurrence pos, Constraint termConstraint, Services services, Constraint userConstraint, Term t)(Code)(Java Doc) public PosInOccurrence posInOccurrence()(Code)(Java Doc) protected TacletApp setAllInstantiations(MatchConditions mc, ListOfIfFormulaInstantiation ifInstantiations)(Code)(Java Doc) protected TacletApp setInstantiation(SVInstantiations svi)(Code)(Java Doc) protected TacletApp setMatchConditions(MatchConditions mc)(Code)(Java Doc) protected MatchConditions setupMatchConditions(PosInOccurrence pos, Services services, Constraint userConstraint)(Code)(Java Doc) public boolean sufficientlyComplete()(Code)(Java Doc)
|
Methods inherited from de.uka.ilkd.key.rule.TacletApp | public TacletApp addCheckedInstantiation(SchemaVariable sv, Term term, Services services, boolean interesting)(Code)(Java Doc) public TacletApp addCheckedInstantiation(SchemaVariable sv, ProgramElement pe, Services services, boolean interesting)(Code)(Java Doc) abstract public TacletApp addInstantiation(SchemaVariable sv, Term term, boolean interesting)(Code)(Java Doc) abstract public TacletApp addInstantiation(SchemaVariable sv, Object[] list, boolean interesting)(Code)(Java Doc) abstract public TacletApp addInstantiation(SchemaVariable sv, ProgramElement pe, boolean interesting)(Code)(Java Doc) public TacletApp addInstantiation(SchemaVariable sv, Name name)(Code)(Java Doc) abstract public TacletApp addInstantiation(SVInstantiations svi)(Code)(Java Doc) public boolean admissible(boolean interactive, ListOfRuleSet ruleSets)(Code)(Java Doc) protected static SetOfQuantifiableVariable boundAtOccurrenceSet(TacletPrefix prefix, SVInstantiations instantiations)(Code)(Java Doc) protected static SetOfQuantifiableVariable boundAtOccurrenceSet(TacletPrefix prefix, SVInstantiations instantiations, PosInOccurrence pos)(Code)(Java Doc) protected SetOfSchemaVariable calculateNeededNonInstantiatedSV()(Code)(Java Doc) protected SetOfSchemaVariable calculateNonInstantiatedSV()(Code)(Java Doc) protected boolean canUseMVAPosteriori(SchemaVariable p_var, Term p_term)(Code)(Java Doc) public boolean canUseMVAPriori(SchemaVariable p_var)(Code)(Java Doc) public static boolean checkVarCondNotFreeIn(Taclet taclet, SVInstantiations instantiations, PosInOccurrence pos)(Code)(Java Doc) protected static SetOfQuantifiableVariable collectBoundVarsAbove(PosInOccurrence pos)(Code)(Java Doc) abstract public boolean complete()(Code)(Java Doc) public Constraint constraint()(Code)(Java Doc) abstract protected SetOfQuantifiableVariable contextVars(SchemaVariable sv)(Code)(Java Doc) public TacletApp createSkolemConstant(String instantiation, SchemaVariable sv, boolean interesting, Services services)(Code)(Java Doc) public TacletApp createSkolemConstant(String instantiation, SchemaVariable sv, Sort sort, boolean interesting)(Code)(Java Doc) public TacletApp createSkolemFunctions(Namespace p_func_ns, Services services)(Code)(Java Doc) public boolean equals(Object o)(Code)(Java Doc) public ListOfGoal execute(Goal goal, Services services)(Code)(Java Doc) public Namespace extendVarNamespaceForSV(Namespace var_ns, SchemaVariable sv)(Code)(Java Doc) public ListOfTacletApp findIfFormulaInstantiations(Sequent p_seq, Services p_services, Constraint p_userConstraint)(Code)(Java Doc) public Sort getRealSort(SchemaVariable p_sv, Services services)(Code)(Java Doc) public int hashCode()(Code)(Java Doc) public ListOfIfFormulaInstantiation ifFormulaInstantiations()(Code)(Java Doc) public boolean ifInstsComplete()(Code)(Java Doc) protected static boolean ifInstsCorrectSize(Taclet p_taclet, ListOfIfFormulaInstantiation p_list)(Code)(Java Doc) public TacletApp instantiateWithMV(Goal p_goal)(Code)(Java Doc) public SVInstantiations instantiations()(Code)(Java Doc) public boolean instsSufficientlyComplete()(Code)(Java Doc) public boolean isDependingOnModifiesSV(SchemaVariable sv)(Code)(Java Doc) public MatchConditions matchConditions()(Code)(Java Doc) public SetOfSchemaVariable neededUninstantiatedVars()(Code)(Java Doc) public SetOfMetavariable newMetavariables()(Code)(Java Doc) abstract public PosInOccurrence posInOccurrence()(Code)(Java Doc) public TacletApp prepareUserInstantiation()(Code)(Java Doc) protected static SVInstantiations replaceInstantiation(Taclet taclet, SVInstantiations insts, SchemaVariable varSV)(Code)(Java Doc) protected static SVInstantiations resolveCollisionVarSV(Taclet taclet, SVInstantiations insts)(Code)(Java Doc) public Rule rule()(Code)(Java Doc) abstract protected TacletApp setAllInstantiations(MatchConditions mc, ListOfIfFormulaInstantiation ifInstantiations)(Code)(Java Doc) public TacletApp setIfFormulaInstantiations(ListOfIfFormulaInstantiation p_list, Services p_services, Constraint p_userConstraint)(Code)(Java Doc) abstract protected TacletApp setInstantiation(SVInstantiations svi)(Code)(Java Doc) abstract protected TacletApp setMatchConditions(MatchConditions mc)(Code)(Java Doc) public PosTacletApp setPosInOccurrence(PosInOccurrence pos)(Code)(Java Doc) abstract public boolean sufficientlyComplete()(Code)(Java Doc) public Taclet taclet()(Code)(Java Doc) public String toString()(Code)(Java Doc) public TacletApp tryToInstantiate(Goal goal, Services services)(Code)(Java Doc) public SetOfSchemaVariable uninstantiatedVars()(Code)(Java Doc) public SchemaVariable varSVNameConflict()(Code)(Java Doc)
|
|
|