|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object blog.ArgSpec blog.Formula blog.EqualityFormula
public class EqualityFormula
Represents an equality test on 2 expressions, each of which is a non-boolean-valued Term.
Formula
Field Summary |
---|
Fields inherited from class blog.Formula |
---|
ALL_OBJECTS, NOT_EXPLICIT |
Fields inherited from class blog.ArgSpec |
---|
location |
Constructor Summary | |
---|---|
EqualityFormula(Term eq1,
Term eq2)
|
Method Summary | |
---|---|
boolean |
assertsNull(Term subject)
Returns true if this equality formula asserts that subject
has the same denotation as the constant "null". |
boolean |
checkTypesAndScope(Model model,
java.util.Map scope)
An equality formula is properly typed if the type of one term is a subtype of the type of the other term. |
boolean |
equals(java.lang.Object o)
Two EqualityFormulas are equal if they have the same pair of terms. |
java.lang.Object |
evaluate(EvalContext context)
Returns the value of this argument specification in the given context. |
Term |
getEqualTerm(Term subject)
Returns the term that, according to this equality formula, has the same denotation as subject . |
java.util.Set |
getNonSatisfiersIfExplicit(EvalContext context,
LogicalVar subject,
GenericObject genericObj)
Returns the set of values for the logical variable subject that are consistent with the generating
function values of genericObj and that make this
formula false in the given context, if this set can be
determined without enumerating possible values for
subject . |
java.util.Set |
getSatisfiersIfExplicit(EvalContext context,
LogicalVar subject,
GenericObject genericObj)
Returns the set of values for the logical variable subject that are consistent with the generating
function values of genericObj and that make this
formula true in the given context, if this set can be
determined without enumerating possible values for
subject . |
java.util.Collection |
getSubExprs()
Returns the proper sub-expressions of this formula. |
ArgSpec |
getSubstResult(Substitution subst,
java.util.Set<LogicalVar> boundVars)
Returns the result of applying the substitution subst to this expression, excluding the logical
variables in boundVars . |
Term |
getTerm1()
|
Term |
getTerm2()
|
java.util.List |
getTopLevelTerms()
Returns the terms that are part of this formula, but not part of any other term or formula within this formula. |
int |
hashCode()
|
boolean |
isLiteral()
Returns true. |
java.lang.String |
toString()
Returns a string of the form (t1 = t2) where t1 and t2 are the terms being compared in this EqualityFormula. |
Methods inherited from class blog.Formula |
---|
compile, containsAnyTerm, containsRandomSymbol, containsTerm, getEquivToNegation, getEquivToNegationInternal, getGenFuncsApplied, getPropCNF, getPropDNF, getStandardForm, getSubformulas, isElementary, isQuantified, isTrue |
Methods inherited from class blog.ArgSpec |
---|
evaluate, evaluate, getFreeVars, getLocation, getSubstResult, getValueIfNonRandom, getVariable, isDetermined, isNumeric, setLocation |
Methods inherited from class java.lang.Object |
---|
clone, finalize, getClass, notify, notifyAll, wait, wait, wait |
Constructor Detail |
---|
public EqualityFormula(Term eq1, Term eq2)
Method Detail |
---|
public Term getTerm1()
public Term getTerm2()
public java.lang.Object evaluate(EvalContext context)
ArgSpec
evaluate
in class ArgSpec
public java.util.Collection getSubExprs()
Formula
getSubExprs
in class Formula
public boolean isLiteral()
isLiteral
in class Formula
public java.util.List getTopLevelTerms()
Formula
getTopLevelTerms
in class Formula
public Term getEqualTerm(Term subject)
subject
. Returns null if
subject
is not one of the terms in this equality.
public boolean assertsNull(Term subject)
subject
has the same denotation as the constant "null".
public java.util.Set getSatisfiersIfExplicit(EvalContext context, LogicalVar subject, GenericObject genericObj)
Formula
subject
that are consistent with the generating
function values of genericObj
and that make this
formula true in the given context, if this set can be
determined without enumerating possible values for
subject
. Returns the special value
Formula.NOT_EXPLICIT if determining the desired set would
requiring enumerating possible values for subject
.
Also, returns the special value Formula.ALL_OBJECTS if this
formula is true in the given context for all objects consistent
with genericObj
. Finally, returns null if it
tries to access an uninstantiated random variable.
getSatisfiersIfExplicit
in class Formula
context
- an evaluation context that does not assign a
value to the logical variable subject
subject
- a logical variablegenericObj
- a GenericObject instance, which can stand for
any object of a given type or include values
for certain generating functionspublic java.util.Set getNonSatisfiersIfExplicit(EvalContext context, LogicalVar subject, GenericObject genericObj)
Formula
subject
that are consistent with the generating
function values of genericObj
and that make this
formula false in the given context, if this set can be
determined without enumerating possible values for
subject
. Returns the special value
Formula.NOT_EXPLICIT if determining the desired set would
requiring enumerating possible values for subject
.
Also, returns the special value Formula.ALL_OBJECTS if this
formula is false in the given context for all objects
consistent with genericObj
. Finally, returns null
if it tries to access an uninstantiated random variable.
This default implementation calls
getEquivToNegation
, then calls
getSatisfiersIfExplicit
on the resulting formula.
Warning: subclasses must override either this method or
getEquivToNegationInternal
to avoid an
UnsupportedOperationException.
getNonSatisfiersIfExplicit
in class Formula
context
- an evaluation context that does not assign a
value to the logical variable subject
subject
- a logical variablegenericObj
- a GenericObject instance, which can stand for
any object of a given type or include values
for certain generating functionspublic boolean equals(java.lang.Object o)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
public java.lang.String toString()
toString
in class java.lang.Object
public boolean checkTypesAndScope(Model model, java.util.Map scope)
checkTypesAndScope
in class ArgSpec
scope
- a Map from variable names (Strings) to LogicalVar objectspublic ArgSpec getSubstResult(Substitution subst, java.util.Set<LogicalVar> boundVars)
ArgSpec
subst
to this expression, excluding the logical
variables in boundVars
. This method is used for
recursive calls. The set boundVars
should contain
those variables that are bound in the syntax tree between this
sub-expression and the top-level expression to which the
substitution is being applied.
getSubstResult
in class ArgSpec
|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |