public class AssumptionFormula extends java.lang.Object implements TacletFormula
Constructor and Description |
---|
AssumptionFormula(Taclet taclet,
java.util.Collection<Term> formula,
java.lang.String status) |
AssumptionFormula(Taclet taclet,
java.util.Collection<Term> formula,
java.lang.String status,
de.uka.ilkd.key.taclettranslation.assumptions.TacletConditions conditions) |
Modifier and Type | Method and Description |
---|---|
de.uka.ilkd.key.taclettranslation.assumptions.TacletConditions |
getConditions() |
Term |
getFormula(TermServices services) |
java.util.Collection<Term> |
getInstantiations()
It can be that a taclet is translated into several formulas, i.e.
|
java.lang.String |
getStatus() |
Taclet |
getTaclet() |
public AssumptionFormula(Taclet taclet, java.util.Collection<Term> formula, java.lang.String status)
public AssumptionFormula(Taclet taclet, java.util.Collection<Term> formula, java.lang.String status, de.uka.ilkd.key.taclettranslation.assumptions.TacletConditions conditions) throws IllegalTacletException
IllegalTacletException
public de.uka.ilkd.key.taclettranslation.assumptions.TacletConditions getConditions()
public Term getFormula(TermServices services)
getFormula
in interface TacletFormula
services
- TODOnull
. If the translation of the taclet
consists of several instantiations (e.g. the taclet has some
generic sorts) the returned term is a conjunction of these
instantiations.public Taclet getTaclet()
getTaclet
in interface TacletFormula
public java.lang.String getStatus()
getStatus
in interface TacletFormula
public java.util.Collection<Term> getInstantiations()
TacletFormula
getInstantiations
in interface TacletFormula
Copyright © 2003-2019 The KeY-Project.