blog
Class DisjFormula

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

public class DisjFormula
extends Formula

Represents a disjunction of expressions, each of which is a Formula.

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

DisjFormula

public DisjFormula(Formula disj)
Creates a new disjunction with just one disjunct, namely the given formula.


DisjFormula

public DisjFormula(Formula disj1,
                   Formula disj2)

DisjFormula

public DisjFormula(java.util.List disjuncts)
Creates a new disjunction formula with the given disjuncts.

Parameters:
disjuncts - a List of Formula objects
Method Detail

getDisjuncts

public java.util.List getDisjuncts()
Returns a List of Formula objects representing the disjuncts in this disjunction formula.


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

getStandardForm

public Formula getStandardForm()
The standard form of a disjunction formula is just the disjunction of the standard forms of its disjuncts.

Overrides:
getStandardForm in class Formula

getEquivToNegationInternal

protected Formula getEquivToNegationInternal()
The formula equivalent to the negation of psi_1 | ... | psi_N is !psi_1 & ... & !psi_N (this is one of De Morgan's laws).

Overrides:
getEquivToNegationInternal in class Formula

getSubformulas

public java.util.List getSubformulas()
Description copied from class: Formula
Returns the proper subformulas of this formula. The default implementation returns an empty list.

Overrides:
getSubformulas in class Formula
Returns:
unmodifiable List of Formula objects

getPropCNF

public 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. In its basic form, this says ((a & b) | c) is equivalent to ((a | c) & (b | c)). More generally, if we choose one conjunct from each disjunct, then at least one of these conjuncts must be satisfied. We get an AND over ways of choosing one conjunct from each disjunct.

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.

Overrides:
getPropCNF in class Formula

getPropDNF

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

Overrides:
getPropDNF in class Formula

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

equals

public boolean equals(java.lang.Object o)
Two DisjFormulas are equal if they have the same list of subformulas.

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 (psi_1 | ... | psi_N) where psi_1, ..., psi_N are the subformulas of this DisjFormula.

Overrides:
toString in class java.lang.Object

checkTypesAndScope

public boolean checkTypesAndScope(Model model,
                                  java.util.Map scope)
Description copied from class: ArgSpec
Returns true if, within the given scope, all the variables used in this ArgSpec are in scope and all type constraints are satisfied. If there is a type or scope error, prints an appropriate message to standard error and returns false.

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