blog
Class EqualityFormula

java.lang.Object
  extended by blog.ArgSpec
      extended by blog.Formula
          extended by blog.EqualityFormula

public class EqualityFormula
extends Formula

Represents an equality test on 2 expressions, each of which is a non-boolean-valued Term.

See Also:
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

EqualityFormula

public EqualityFormula(Term eq1,
                       Term eq2)
Method Detail

getTerm1

public Term getTerm1()

getTerm2

public Term getTerm2()

evaluate

public java.lang.Object evaluate(EvalContext context)
Description copied from class: ArgSpec
Returns the value of this argument specification in the given context. Returns null if the partial world in this context is not complete enough to evaluate this ArgSpec, or if this ArgSpec contains a free variable that is not assigned a value in the given context.

Specified by:
evaluate in class ArgSpec

getSubExprs

public java.util.Collection getSubExprs()
Description copied from class: Formula
Returns the proper sub-expressions of this formula. This default implementation returns the set of sub-formulas of this formula. This implementation is overridden by AtomicFormula and EqualityFormula, whose sub-expressions are terms.

Overrides:
getSubExprs in class Formula
Returns:
unmodifiable Collection of ArgSpec

isLiteral

public boolean isLiteral()
Returns true.

Overrides:
isLiteral in class Formula

getTopLevelTerms

public java.util.List getTopLevelTerms()
Description copied from class: Formula
Returns the terms that are part of this formula, but not part of any other term or formula within this formula. The default implementation returns an empty list.

Overrides:
getTopLevelTerms in class Formula
Returns:
unmodifiable List of Term objects

getEqualTerm

public Term getEqualTerm(Term subject)
Returns the term that, according to this equality formula, has the same denotation as subject. Returns null if subject is not one of the terms in this equality.


assertsNull

public boolean assertsNull(Term subject)
Returns true if this equality formula asserts that subject has the same denotation as the constant "null".


getSatisfiersIfExplicit

public java.util.Set getSatisfiersIfExplicit(EvalContext context,
                                             LogicalVar subject,
                                             GenericObject genericObj)
Description copied from class: Formula
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. 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.

Specified by:
getSatisfiersIfExplicit in class Formula
Parameters:
context - an evaluation context that does not assign a value to the logical variable subject
subject - a logical variable
genericObj - a GenericObject instance, which can stand for any object of a given type or include values for certain generating functions

getNonSatisfiersIfExplicit

public java.util.Set getNonSatisfiersIfExplicit(EvalContext context,
                                                LogicalVar subject,
                                                GenericObject genericObj)
Description copied from class: Formula
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. 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.

Overrides:
getNonSatisfiersIfExplicit in class Formula
Parameters:
context - an evaluation context that does not assign a value to the logical variable subject
subject - a logical variable
genericObj - a GenericObject instance, which can stand for any object of a given type or include values for certain generating functions

equals

public boolean equals(java.lang.Object o)
Two EqualityFormulas are equal if they have the same pair of terms.

Overrides:
equals in class java.lang.Object

hashCode

public int hashCode()
Overrides:
hashCode in class java.lang.Object

toString

public java.lang.String toString()
Returns a string of the form (t1 = t2) where t1 and t2 are the terms being compared in this EqualityFormula.

Overrides:
toString in class java.lang.Object

checkTypesAndScope

public 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.

Specified by:
checkTypesAndScope in class ArgSpec
scope - a Map from variable names (Strings) to LogicalVar objects

getSubstResult

public ArgSpec getSubstResult(Substitution subst,
                              java.util.Set<LogicalVar> boundVars)
Description copied from class: ArgSpec
Returns the result of applying the substitution 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.

Specified by:
getSubstResult in class ArgSpec