|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object blog.ArgSpec blog.Formula blog.NegFormula
public class NegFormula
Represents a logical negation of an expression of type Formula.
Formula
Field Summary |
---|
Fields inherited from class blog.Formula |
---|
ALL_OBJECTS, NOT_EXPLICIT |
Fields inherited from class blog.ArgSpec |
---|
location |
Constructor Summary | |
---|---|
NegFormula(Formula neg)
|
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)
Two NegFormulas are equal if they have the same subformula. |
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 !psi is psi itself. |
Formula |
getNeg()
|
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()
If this is a literal, then its CNF form is just a conjunction consisting of one disjunction, whose sole disjunct is this formula. |
DisjFormula |
getPropDNF()
If this is a literal, then its DNF form is just a disjunction consisting of one conjunction, whose sole conjunct is this formula. |
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 a negation formula !psi is determined as follows. |
java.util.List |
getSubformulas()
Returns the proper subformulas 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 . |
int |
hashCode()
|
boolean |
isLiteral()
Returns true if the negated formula is an atomic formula or an equality formula. |
java.lang.String |
toString()
Returns a string of the form !psi where psi is the negated formula. |
Methods inherited from class blog.Formula |
---|
compile, containsAnyTerm, containsRandomSymbol, containsTerm, getEquivToNegation, getGenFuncsApplied, getSubExprs, getTopLevelTerms, 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 NegFormula(Formula neg)
Method Detail |
---|
public Formula getNeg()
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 java.util.List getSubformulas()
Formula
getSubformulas
in class Formula
public ConjFormula getPropCNF()
getPropCNF
in class Formula
public DisjFormula getPropDNF()
getPropDNF
in class Formula
public boolean isLiteral()
isLiteral
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 |