public class ExistsQuantifiedFormula extends QuantifiedFormula
Constructor and Description |
---|
ExistsQuantifiedFormula(ExistsQuantifiedFormula other) |
ExistsQuantifiedFormula(FolFormula folFormula,
Variable variable)
Creates a new exists-quantified formula with the given formula and variable.
|
ExistsQuantifiedFormula(RelationalFormula folFormula,
java.util.Set<Variable> variables)
Creates a new exists-quantified formula with the given formula and variables.
|
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.
|
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() |
containsQuantifier, equals, getAtoms, getFormula, getFunctors, getPredicates, getQuantifiedFormulas, getQuantifierVariables, getTerms, getTerms, getUnboundVariables, hashCode, isClosed, isClosed, isDnf, isLiteral, isWellBound, isWellBound
combineWithAnd, combineWithOr, complement, getUniformProbability, toDnf
allGroundInstances, allSubstitutions, containsTermsOfType, exchange, getPredicateCls, getSatisfactionRatio, getSignature, isGround, isWellFormed, substitute
public ExistsQuantifiedFormula(RelationalFormula folFormula, java.util.Set<Variable> variables)
folFormula
- the formula this for-all-quantified formula ranges over.variables
- the variables of this for-all-quantified formula.public ExistsQuantifiedFormula(FolFormula folFormula, Variable variable)
folFormula
- the formula this for-all-quantified formula ranges over.variable
- the variable of this for-all-quantified formula.public ExistsQuantifiedFormula(ExistsQuantifiedFormula other)
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 FolFormula toNnf()
FolFormula
toNnf
in class FolFormula
public FolFormula collapseAssociativeFormulas()
FolFormula
collapseAssociativeFormulas
in class FolFormula
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