blog
Class ConjFormula

java.lang.Object
  blog.ArgSpec
      blog.Formula
          blog.ConjFormula

public class ConjFormula
extends Formula

Represents a conjuction 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

ConjFormula(Formula conj)
Creates a new conjunction with just one conjunct, namely the given formula.

ConjFormula(Formula conj1, Formula conj2)

ConjFormula(java.util.List conjuncts)
Creates a new conjunction formula with the given conjuncts.

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 ConjFormulas 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	getConjuncts() Returns a List of Formula objects representing the conjuncts in this conjunction formula.
protected Formula	getEquivToNegationInternal() The formula equivalent to the negation of psi_1 & ...
ConjFormula	getPropCNF() To get the CNF form of a conjunction, we first convert its conjuncts into CNF, then agglomerate all the conjuncts of the resulting CNF forms together in a big conjunction.
DisjFormula	getPropDNF() To get the DNF form of a conjunction formula, we convert each conjunct to DNF, then use the distributive property of AND over OR.
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 conjunction formula is just the conjunction of the standard forms of its conjuncts.
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

ConjFormula

public ConjFormula(Formula conj)

Creates a new conjunction with just one conjunct, namely the given formula.

ConjFormula

public ConjFormula(Formula conj1,
                   Formula conj2)

ConjFormula

public ConjFormula(java.util.List conjuncts)

Creates a new conjunction formula with the given conjuncts.

Parameters:

conjuncts - a List of Formula objects

Method Detail

getConjuncts

public java.util.List getConjuncts()

Returns a List of Formula objects representing the conjuncts in this conjunction 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 conjunction formula is just the conjunction of the standard forms of its conjuncts.

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 conjunction, we first convert its conjuncts into CNF, then agglomerate all the conjuncts of the resulting CNF forms together in a big conjunction.

Overrides:

getPropCNF in class Formula

getPropDNF

public DisjFormula getPropDNF()

To get the DNF form of a conjunction formula, we convert each conjunct to DNF, then use the distributive property of AND over OR. In its basic form, this says ((a | b) & c) is equivalent to ((a & c) | (b & c)). More generally, in order to satisfy the conjunction, we need to satisfy one disjunct from every conjunct. We get an OR over ways to choose one disjunct from each conjuct.

We begin by converting each conjunct to DNF, yielding something like: ((psi_{1,1} | ... | psi_{1,k1}) & ... & (psi_{n,1} | ... | psi_{n,kn})) where each psi is a conjunction of literals. Then we form a conjunction 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 conjunctions together in a big disjunction.

Special cases: if this is an empty conjunction, the output is a disjunction consisting of one empty conjunction, which is always true. If this formula contains a conjunct whose DNF form is an empty disjunction, then the output is an empty disjunction, which is always false.

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 ConjFormulas 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 ConjFormula.

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