com.ibm.wala.logic
Interface IFormula

All Known Subinterfaces:

ICNFFormula, IMaxTerm

All Known Implementing Classes:

AbstractBinaryFormula, BinaryFormula, BooleanConstantFormula, CNFFormula, Disjunction, NotFormula, NotFormulaMaxTerm, QuantifiedFormula, RelationFormula

public interface IFormula

Formula := P(Term, ....) | NOT(Formula) | Formula CONNECTIVE Formula | QUANTIFIER Formula | TRUE | FALSE

Nested Class Summary

static class

IFormula.Kind

Method Summary

java.util.Collection<? extends ITerm>	getAllTerms()
java.util.Collection<? extends IConstant>	getConstants()
java.util.Collection<AbstractVariable>	getFreeVariables()
IFormula.Kind	getKind()
java.lang.String	prettyPrint(ILogicDecorator d)

Method Detail

getKind

IFormula.Kind getKind()

getFreeVariables

java.util.Collection<AbstractVariable> getFreeVariables()

Returns:

the free variables in this formula

getConstants

java.util.Collection<? extends IConstant> getConstants()

Returns:

the constants that appear in this formula

getAllTerms

java.util.Collection<? extends ITerm> getAllTerms()

Returns:

all terms that appear in this formula, including recursive descent on on-atomic terms

prettyPrint

java.lang.String prettyPrint(ILogicDecorator d)