public class ExistsQuantifiedFormula extends FolFormula
Modifier and Type | Field and Description |
---|---|
protected QuantifiedFormulaSupport<FolFormula> |
support
This helper class implements common functionalities of quantified
formulas, meaning the implementation can delegate the method calls to the support
class.
|
Constructor and Description |
---|
ExistsQuantifiedFormula(ExistsQuantifiedFormula other) |
ExistsQuantifiedFormula(RelationalFormula folFormula,
java.util.Set<Variable> variables)
Creates a new quantified folFormula with the given folFormula and variables.
|
ExistsQuantifiedFormula(RelationalFormula folFormula,
Variable variable)
Creates a new quantified folFormula with the given folFormula and variable.
|
Modifier and Type | Method and Description |
---|---|
ExistsQuantifiedFormula |
clone()
Creates a deep copy of this formula
|
FolFormula |
collapseAssociativeFormulas()
This method collapses all associative operations appearing
in this term, e.g.
|
boolean |
containsQuantifier()
Checks whether this formula contains any quantification.
|
boolean |
equals(java.lang.Object obj) |
java.util.Set<FOLAtom> |
getAtoms()
Processes the set of all atoms which appear in this formula
|
FolFormula |
getFormula() |
java.util.Set<Functor> |
getFunctors() |
java.util.Set<? extends Predicate> |
getPredicates()
Processes the set of all predicates which appear in this
formula
|
java.util.Set<FolFormula> |
getQuantifiedFormulas() |
java.util.Set<Variable> |
getQuantifierVariables() |
java.util.Set<Term<?>> |
getTerms() |
<C extends Term<?>> |
getTerms(java.lang.Class<C> cls)
Processes the set containing all terms of type C.
|
java.util.Set<Variable> |
getUnboundVariables() |
boolean |
isClosed()
Checks whether this formula is closed, i.e.
|
boolean |
isClosed(java.util.Set<Variable> boundVariables)
Checks whether this formula is closed, i.e.
|
boolean |
isDnf()
Checks whether this formula is in disjunctive normal form.
|
boolean |
isLiteral() |
boolean |
isWellBound()
Checks whether this formula is well-bound, i.e.
|
boolean |
isWellBound(java.util.Set<Variable> boundVariables)
Checks whether this formula is well-bound, i.e.
|
void |
setFormula(FolFormula formula) |
void |
setQuantifierVariables(java.util.Set<Variable> variables) |
ExistsQuantifiedFormula |
substitute(Term<?> v,
Term<?> t)
Substitutes all occurrences of term "v" in this formula
by term "t" and returns the new formula.
|
FolFormula |
toNnf()
Makes the negation normal form of this formula.
|
java.lang.String |
toString() |
combineWithAnd, combineWithOr, complement, getSignature, getUniformProbability, toDnf
allGroundInstances, allSubstitutions, containsTermsOfType, exchange, getPredicateCls, getSatisfactionRatio, isGround, isWellFormed, substitute
finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
hashCode
protected QuantifiedFormulaSupport<FolFormula> support
public ExistsQuantifiedFormula(RelationalFormula folFormula, java.util.Set<Variable> variables)
folFormula
- the folFormula this quantified folFormula ranges over.variables
- the variables of this quantified folFormula.public ExistsQuantifiedFormula(RelationalFormula folFormula, Variable variable)
folFormula
- the folFormula this quantified folFormula ranges over.variable
- the variable of this quantified folFormula.public ExistsQuantifiedFormula(ExistsQuantifiedFormula other)
public java.util.Set<FolFormula> getQuantifiedFormulas()
public boolean equals(java.lang.Object obj)
equals
in interface SimpleLogicalFormula
equals
in class java.lang.Object
public FolFormula toNnf()
FolFormula
toNnf
in class FolFormula
public FolFormula collapseAssociativeFormulas()
FolFormula
collapseAssociativeFormulas
in class FolFormula
public ExistsQuantifiedFormula substitute(Term<?> v, Term<?> t) throws java.lang.IllegalArgumentException
RelationalFormula
substitute
in interface ComplexLogicalFormula
substitute
in class FolFormula
v
- the term to be substituted.t
- the term to substitute.java.lang.IllegalArgumentException
- if "v" and "t" are of different sorts
(NOTE: this exception is only thrown when "v" actually appears in this
formula).public java.lang.String toString()
toString
in class RelationalFormula
public ExistsQuantifiedFormula clone()
SimpleLogicalFormula
clone
in interface ComplexLogicalFormula
clone
in interface SimpleLogicalFormula
clone
in class FolFormula
public FolFormula getFormula()
getFormula
in interface QuantifiedFormula
getFormula
in class RelationalFormula
public java.util.Set<Variable> getQuantifierVariables()
getQuantifierVariables
in interface QuantifiedFormula
getQuantifierVariables
in class FolFormula
public void setFormula(FolFormula formula)
public void setQuantifierVariables(java.util.Set<Variable> variables)
public java.util.Set<FOLAtom> getAtoms()
SimpleLogicalFormula
getAtoms
in interface SimpleLogicalFormula
getAtoms
in class RelationalFormula
public java.util.Set<Functor> getFunctors()
getFunctors
in class RelationalFormula
public boolean isDnf()
FolFormula
isDnf
in class FolFormula
public java.util.Set<? extends Predicate> getPredicates()
SimpleLogicalFormula
public boolean isLiteral()
public java.util.Set<Variable> getUnboundVariables()
public boolean containsQuantifier()
QuantifiedFormula
public boolean isWellBound()
QuantifiedFormula
public boolean isWellBound(java.util.Set<Variable> boundVariables)
QuantifiedFormula
boundVariables
- the variables assumed to be bound.public boolean isClosed()
QuantifiedFormula
public boolean isClosed(java.util.Set<Variable> boundVariables)
QuantifiedFormula
boundVariables
- the variables assumed to be bound.public java.util.Set<Term<?>> getTerms()
public <C extends Term<?>> java.util.Set<C> getTerms(java.lang.Class<C> cls)
LogicStructure
cls
- The Class structure containing type information about the
searched term