com.ibm.wala.logic
Interface ISemiDecisionProcedure

All Known Implementing Classes:

AbstractSemiDecisionProcedure, AdHocSemiDecisionProcedure

public interface ISemiDecisionProcedure

Method Summary

boolean	isContradiction(IFormula f)
boolean	isContradiction(IFormula f, java.util.Collection<IMaxTerm> facts)
boolean	isTautology(IFormula f)
boolean	isTautology(IFormula f, java.util.Collection<IMaxTerm> facts)

Method Detail

isContradiction

boolean isContradiction(IFormula f)

Returns:

true if we can prove f is a contradiction

isTautology

boolean isTautology(IFormula f)

Returns:

true if we can prove f is a tautology

isTautology

boolean isTautology(IFormula f,
                    java.util.Collection<IMaxTerm> facts)
                    throws java.lang.IllegalArgumentException

Parameters:

facts - formulae that can be treated as axioms

Returns:

true if we can prove f is a tautology

Throws:

java.lang.IllegalArgumentException - if facts == null

isContradiction

boolean isContradiction(IFormula f,
                        java.util.Collection<IMaxTerm> facts)
                        throws java.lang.IllegalArgumentException

Parameters:

facts - formulae that can be treated as axioms

Returns:

true if we can prove f is a contradiction

Throws:

java.lang.IllegalArgumentException - if facts == null