blog
Class ExistentialFormula

java.lang.Object
  extended by blog.ArgSpec
      extended by blog.Formula
          extended by 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.