public class TruthValuePOExtension extends java.lang.Object implements POExtension
POExtension
to support truth value evaluation.Constructor and Description |
---|
TruthValuePOExtension() |
Modifier and Type | Method and Description |
---|---|
boolean |
isPOSupported(ProofOblInput po)
Checks if the given
ProofOblInput is supported. |
protected Term |
labelPostTerm(Services services,
Term term)
Labels all predicates in the given
Term and its children with
a FormulaTermLabel . |
Term |
modifyPostTerm(InitConfig proofConfig,
Services services,
Term postTerm)
Modifies the post condition.
|
public boolean isPOSupported(ProofOblInput po)
ProofOblInput
is supported.isPOSupported
in interface POExtension
po
- The ProofOblInput
to check.true
is supported, false
is not supported.public Term modifyPostTerm(InitConfig proofConfig, Services services, Term postTerm)
modifyPostTerm
in interface POExtension
proofConfig
- The InitConfig
to use.services
- The Services
to use.postTerm
- The post condition to modify.