|
|||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object blog.ArgSpec blog.Formula blog.DisjFormula
public class DisjFormula
Represents a disjunction of expressions, each of which is a Formula.
Formula
Field Summary |
---|
Fields inherited from class blog.Formula |
---|
ALL_OBJECTS, NOT_EXPLICIT |
Fields inherited from class blog.ArgSpec |
---|
location |
Constructor Summary | |
---|---|
DisjFormula(Formula disj)
Creates a new disjunction with just one disjunct, namely the given formula. |
|
DisjFormula(Formula disj1,
Formula disj2)
|
|
DisjFormula(java.util.List disjuncts)
Creates a new disjunction formula with the given disjuncts. |
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 DisjFormulas are equal if they have the same list of subformulas. |
java.lang.Object |
evaluate(EvalContext context)
Returns the value of this argument specification in the given context. |
java.util.List |
getDisjuncts()
Returns a List of Formula objects representing the disjuncts in this disjunction formula. |
protected Formula |
getEquivToNegationInternal()
The formula equivalent to the negation of psi_1 | ... |
ConjFormula |
getPropCNF()
To get the CNF form of a disjunction formula, we convert each disjunct to CNF, then use the distributive property of OR over AND. |
DisjFormula |
getPropDNF()
To get the DNF form of a disjunction formula, we get the DNF forms of all its disjunts, then agglomerate all the disjuncts of the resulting DNF forms in one big disjunction. |
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 disjunction formula is just the disjunction of the standard forms of its disjuncts. |
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()
|
java.lang.String |
toString()
Returns a string of the form (psi_1 | ... |
Methods inherited from class blog.Formula |
---|
compile, containsAnyTerm, containsRandomSymbol, containsTerm, getEquivToNegation, getGenFuncsApplied, getNonSatisfiersIfExplicit, getSubExprs, 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 |
Constructor Detail |
---|
public DisjFormula(Formula disj)
public DisjFormula(Formula disj1, Formula disj2)
public DisjFormula(java.util.List disjuncts)
disjuncts
- a List of Formula objectsMethod Detail |
---|
public java.util.List getDisjuncts()
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()
We begin by converting each disjunct to CNF, yielding something like: ((psi_{1,1} & ... & psi_{1,k1}) | ... | (psi_{n,1} & ... & psi_{n,kn})) where each psi is a disjunction of literals. Then we form a disjunction for each tuple (chi_1, ..., chi_n) in the cross product {psi_{1,1}, ..., psi_{1,k1}} x ... x {psi_{n,1}, ..., psi_{n,kn}}, then put all these disjunctions together in a big conjunction.
Special cases: if this is an empty disjunction, then the output is a conjunction consisting of one empty disjunction, which is always false. If this formula contains a disjunct whose CNF form is an empty conjunction, then the output is an empty conjunction, which is always true.
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 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 |