blog
Class Formula

java.lang.Object
  blog.ArgSpec
      blog.Formula

Direct Known Subclasses:

AtomicFormula, ConjFormula, DisjFormula, EqualityFormula, ExistentialFormula, ImplicFormula, NegFormula, TrueFormula, UniversalFormula

public abstract class Formula
extends ArgSpec

Formula is an abstract class from which all classes denoting particular kinds of formulas inherit. A formula can be "wrapped" in the class Wrapper that facilitates error-checking.

Field Summary

static java.util.Set	ALL_OBJECTS Special value returned by getSatisfiersIfExplicit and getNonSatisfiersIfExplicit to indicate that the set of satisfiers or non-satisfiers consists of all objects of the appropriate type.
static java.util.Set	NOT_EXPLICIT Special value returned by getSatisfiersIfExplicit and GetNonSatisfiersIfExplicit to indicate that the desired set cannot be determined without iterating over possible values of the subject variable.

Fields inherited from class blog.ArgSpec

location

Constructor Summary

Formula()

Method Summary

int	compile(java.util.LinkedHashSet callStack) Compiles all sub-formulas and top-level terms of this formula.
boolean	containsAnyTerm(java.util.Collection terms) Returns true if this formula contains any term in the given collection.
boolean	containsRandomSymbol() Returns true if any of the subformulas or top-level terms of this term contain a random symbol.
boolean	containsTerm(Term target) Returns true if this formula contains the given term.
Formula	getEquivToNegation() Returns a formula that is equivalent to the negation of this formula, but is not simply a NegFormula constructed with this formula as its argument.
protected Formula	getEquivToNegationInternal() Returns a formula that is equivalent to the negation of this formula, but is not simply a NegFormula constructed with this formula as its argument.
java.util.Set	getGenFuncsApplied(Term subject) Returns the set of generating functions that are applied to the term subject anywhere in this formula.
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() Returns an equivalent formula that consists of a conjunction where each conjunct is an elementary disjunction.
DisjFormula	getPropDNF() Returns an equivalent formula that consists of a disjunction where each disjunct is an elementary conjunction.
abstract 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() Returns a new formula in which: occurrences of the formula "true" have been converted to empty conjunctions; implications have been converted to disjunctions; only literals (atomic and equality formulas) are negated.
java.util.Collection	getSubExprs() Returns the proper sub-expressions of this formula.
java.util.List	getSubformulas() Returns the proper subformulas of this formula.
java.util.List	getTopLevelTerms() Returns the terms that are part of this formula, but not part of any other term or formula within this formula.
boolean	isElementary() Returns true if this formula is elementary, that is, all its subformulas are literals or unnegated quantified formulas.
boolean	isLiteral() Returns true if this formula is a literal, that is, an atomic/equality formula or the negation thereof.
boolean	isQuantified() Returns true if this is a quantified formula.
boolean	isTrue(PartialWorld w) Returns the logical value of this formula in the given partial world.

Methods inherited from class blog.ArgSpec

checkTypesAndScope, evaluate, evaluate, evaluate, getFreeVars, getLocation, getSubstResult, getSubstResult, getValueIfNonRandom, getVariable, isDetermined, isNumeric, setLocation

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

NOT_EXPLICIT

public static final java.util.Set NOT_EXPLICIT

Special value returned by getSatisfiersIfExplicit and GetNonSatisfiersIfExplicit to indicate that the desired set cannot be determined without iterating over possible values of the subject variable.

ALL_OBJECTS

public static final java.util.Set ALL_OBJECTS

Special value returned by getSatisfiersIfExplicit and getNonSatisfiersIfExplicit to indicate that the set of satisfiers or non-satisfiers consists of all objects of the appropriate type. This means that the truth value of the formula does not depend on the value of the subject variable.

Constructor Detail

Formula

public Formula()

Method Detail

isTrue

public boolean isTrue(PartialWorld w)

Returns the logical value of this formula in the given partial world. If the given world is not complete enough to determine the value of this formula, this method yields a fatal error.

compile

public int compile(java.util.LinkedHashSet callStack)

Compiles all sub-formulas and top-level terms of this formula.

Overrides:

compile in class ArgSpec

Parameters:

callStack - Set of objects whose compile methods are parents of this method invocation. Ordered by invocation order. Used to detect cycles.

getSubExprs

public java.util.Collection getSubExprs()

Returns the proper sub-expressions of this formula. This default implementation returns the set of sub-formulas of this formula. This implementation is overridden by AtomicFormula and EqualityFormula, whose sub-expressions are terms.

Overrides:

getSubExprs in class ArgSpec

Returns:

unmodifiable Collection of ArgSpec

getStandardForm

public Formula getStandardForm()

Returns a new formula in which:

• occurrences of the formula "true" have been converted to empty conjunctions;
• implications have been converted to disjunctions;
• only literals (atomic and equality formulas) are negated.

The default implementation just returns this formula.

getEquivToNegation

public Formula getEquivToNegation()

Returns a formula that is equivalent to the negation of this formula, but is not simply a NegFormula constructed with this formula as its argument. If no such formula can be constructed easily, this method returns null.

This method calls getEquivToNegationInternal and caches the formula that is returned (if it is non-null).

getEquivToNegationInternal

protected Formula getEquivToNegationInternal()

Returns a formula that is equivalent to the negation of this formula, but is not simply a NegFormula constructed with this formula as its argument. If no such formula can be constructed easily, this method returns null.

The default implementation returns null.

getSubformulas

public java.util.List getSubformulas()

Returns the proper subformulas of this formula. The default implementation returns an empty list.

Returns:

unmodifiable List of Formula objects

getTopLevelTerms

public java.util.List getTopLevelTerms()

Returns the terms that are part of this formula, but not part of any other term or formula within this formula. The default implementation returns an empty list.

Returns:

unmodifiable List of Term objects

containsRandomSymbol

public boolean containsRandomSymbol()

Returns true if any of the subformulas or top-level terms of this term contain a random symbol. Note that this is overridden by UniversalFormula and ExistentialFormula.

Specified by:

containsRandomSymbol in class ArgSpec

containsTerm

public boolean containsTerm(Term target)

Returns true if this formula contains the given term.

containsAnyTerm

public boolean containsAnyTerm(java.util.Collection terms)

Returns true if this formula contains any term in the given collection.

getGenFuncsApplied

public java.util.Set getGenFuncsApplied(Term subject)

Returns the set of generating functions that are applied to the term subject anywhere in this formula.

Returns:

unmodifiable Set of GeneratingFunction

getPropCNF

public ConjFormula getPropCNF()

Returns an equivalent formula that consists of a conjunction where each conjunct is an elementary disjunction. An elementary formula is one in which all the subformulas are atomic or equality formulas, or negations of those formulas, or unnegated quantified formulas. This is "propositional" CNF in that quantified formulas are treated as atomic.

The default implementation just returns a conjunction consisting of one disjunction, whose sole disjunct is this formula. This is the correct behavior for literals and quantified formulas.

getPropDNF

public DisjFormula getPropDNF()

Returns an equivalent formula that consists of a disjunction where each disjunct is an elementary conjunction. An elementary formula is one in which all the subformulas are atomic or equality formulas, or negations of those formulas, or unnegated quantified formulas. This is "propositional" DNF in that quantified formulas are treated as atomic.

The default implementation just returns a disjunction consisting of one conjunction, whose sole conjunct is this formula. This is the correct behavior for literals and quantified formulas.

isLiteral

public boolean isLiteral()

Returns true if this formula is a literal, that is, an atomic/equality formula or the negation thereof.

The default implementation returns false.

isQuantified

public boolean isQuantified()

Returns true if this is a quantified formula. The default implementation returns false.

isElementary

public boolean isElementary()

Returns true if this formula is elementary, that is, all its subformulas are literals or unnegated quantified formulas.

getSatisfiersIfExplicit

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

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

getNonSatisfiersIfExplicit

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

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