|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object blog.ArgSpec blog.Formula blog.TrueFormula
public class TrueFormula
A Formula consisting of just the zero-ary logical operator "true", which is true in every world under every assignment.
Field Summary | |
---|---|
static TrueFormula |
TRUE
A canonical instance of TrueFormula. |
Fields inherited from class blog.Formula |
---|
ALL_OBJECTS, NOT_EXPLICIT |
Fields inherited from class blog.ArgSpec |
---|
location |
Constructor Summary | |
---|---|
TrueFormula()
Creates a new TrueFormula. |
Method Summary | |
---|---|
boolean |
checkTypesAndScope(Model model,
java.util.Map scope)
Returns true if, within the given scope, all the variables used in this ArgSpec are in scope and all type constraints are satisfied. |
boolean |
equals(java.lang.Object o)
Any two instances of TrueFormula are equal. |
java.lang.Object |
evaluate(EvalContext context)
Returns the value of this argument specification in the given context. |
protected Formula |
getEquivToNegationInternal()
A formula equivalent to the negation of "true" is the empty disjunction, which is always false. |
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 . |
ConjFormula |
getPropCNF()
The CNF form of TrueFormula has no conjuncts. |
DisjFormula |
getPropDNF()
The DNF form of TrueFormula has just one disjunct, which is an empty conjunction. |
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 . |
Formula |
getStandardForm()
The standard form of the formula "true" is an empty conjunction, which is always true. |
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 . |
int |
hashCode()
|
java.lang.String |
toString()
Returns the string "true". |
Methods inherited from class blog.Formula |
---|
compile, containsAnyTerm, containsRandomSymbol, containsTerm, getEquivToNegation, getGenFuncsApplied, getSubExprs, getSubformulas, getTopLevelTerms, isElementary, isLiteral, 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 |
Field Detail |
---|
public static final TrueFormula TRUE
Constructor Detail |
---|
public TrueFormula()
Method Detail |
---|
public java.lang.Object evaluate(EvalContext context)
ArgSpec
evaluate
in class ArgSpec
public Formula getStandardForm()
getStandardForm
in class Formula
protected Formula getEquivToNegationInternal()
getEquivToNegationInternal
in class Formula
public ConjFormula getPropCNF()
getPropCNF
in class Formula
public DisjFormula getPropDNF()
getPropDNF
in class Formula
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)
ArgSpec
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 |