blog
Class ExistentialFormula

java.lang.Object
  blog.ArgSpec
      blog.Formula
          blog.ExistentialFormula

public class ExistentialFormula
extends Formula

Represents an existential instantiation for one variable satisfying an expression of type Formula.

Field Summary

Fields inherited from class blog.Formula

ALL_OBJECTS, NOT_EXPLICIT

Fields inherited from class blog.ArgSpec

location

Constructor Summary

ExistentialFormula(LogicalVar var, Formula cond)

ExistentialFormula(java.lang.String varName, Type varType, Formula cond)

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.
int	compile(java.util.LinkedHashSet callStack) Compiles a specification for the set of witnesses for this existential formula.
boolean	containsRandomSymbol() Returns true if any of the subformulas or top-level terms of this term contain a random symbol.
boolean	equals(java.lang.Object o)
java.lang.Object	evaluate(EvalContext context) Returns the value of this argument specification in the given context.
Formula	getCond() Returns the formula inside the existential quantifier.
protected Formula	getEquivToNegationInternal() A formula equivalent to the negation of an exisential formula (exists x psi) is (forall x !psi).
java.util.Set	getFreeVars() Returns the logical variables that occur free in this expression.
LogicalVar	getLogicalVariable() Returns the logical variable governed by the existential quantifier in 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 an existential formula (exists x psi) is (exists x psi'), where psi' is the standard form of psi.
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.
Type	getType() Returns the type that the existential quantifier in this formula ranges over.
protected CompiledSetSpec	getWitnessSpec() Returns a CompiledSetSpec for the set of objects that are witnesses to this existential formula: that is, the objects that make the condition true.
int	hashCode()
boolean	isQuantified() Returns true if this is a quantified formula.
java.lang.String	toString()

Methods inherited from class blog.Formula

containsAnyTerm, containsTerm, getEquivToNegation, getGenFuncsApplied, getNonSatisfiersIfExplicit, getPropCNF, getPropDNF, getSubExprs, getTopLevelTerms, isElementary, isLiteral, isTrue

Methods inherited from class blog.ArgSpec

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

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

ExistentialFormula

public ExistentialFormula(java.lang.String varName,
                          Type varType,
                          Formula cond)

Parameters:

varName - name of existentially quantified variable

varType - type being quantified over. May be null, but then the main program should exit before the compilation phase.

cond - formula in the scope of the quantifier

ExistentialFormula

public ExistentialFormula(LogicalVar var,
                          Formula cond)

Method Detail

getLogicalVariable

public LogicalVar getLogicalVariable()

Returns the logical variable governed by the existential quantifier in this formula.

getType

public Type getType()

Returns the type that the existential quantifier in this formula ranges over.

getCond

public Formula getCond()

Returns the formula inside the existential quantifier.

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

containsRandomSymbol

public boolean containsRandomSymbol()

Description copied from class: Formula

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.

Overrides:

containsRandomSymbol in class Formula

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

compile

public int compile(java.util.LinkedHashSet callStack)

Compiles a specification for the set of witnesses for this existential formula.

Overrides:

compile in class Formula

Parameters:

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

getStandardForm

public Formula getStandardForm()

The standard form of an existential formula (exists x psi) is (exists x psi'), where psi' is the standard form of psi.

Overrides:

getStandardForm in class Formula

getEquivToNegationInternal

protected Formula getEquivToNegationInternal()

A formula equivalent to the negation of an exisential formula (exists x psi) is (forall x !psi).

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

getFreeVars

public java.util.Set getFreeVars()

Description copied from class: ArgSpec

Returns the logical variables that occur free in this expression. If this expression was loaded from a file, then this method should be called only after checkTypesAndScope, which converts SymbolTerms to LogicalVars.

The default implementation returns the union of the sets of free variables in this expression's sub-expressions.

Overrides:

getFreeVars in class ArgSpec

Returns:

unmodifiable Set of LogicalVar

isQuantified

public boolean isQuantified()

Description copied from class: Formula

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

Overrides:

isQuantified 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

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

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

equals

public boolean equals(java.lang.Object o)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

getWitnessSpec

protected CompiledSetSpec getWitnessSpec()

Returns a CompiledSetSpec for the set of objects that are witnesses to this existential formula: that is, the objects that make the condition true.