public class ForallQuantifiedFormula extends QuantifiedFormula
Constructor and Description |
---|
ForallQuantifiedFormula(FolFormula folFormula,
Variable variable)
Creates a new for-all-quantified formula with the given formula and variable.
|
ForallQuantifiedFormula(ForallQuantifiedFormula other) |
ForallQuantifiedFormula(RelationalFormula folFormula,
java.util.Set<Variable> variables)
Creates a new for-all-quantified formula with the given formula and variables.
|
Modifier and Type | Method and Description |
---|---|
ForallQuantifiedFormula |
clone()
Creates a deep copy of this formula
|
FolFormula |
collapseAssociativeFormulas()
This method collapses all associative operations appearing
in this term, e.g.
|
ForallQuantifiedFormula |
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 ForallQuantifiedFormula(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 ForallQuantifiedFormula(FolFormula folFormula, Variable variable)
folFormula
- the formula this for-all-quantified formula ranges over.variable
- the variable of this for-all-quantified formula.public ForallQuantifiedFormula(ForallQuantifiedFormula other)
public ForallQuantifiedFormula 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 collapseAssociativeFormulas()
FolFormula
collapseAssociativeFormulas
in class FolFormula
public FolFormula toNnf()
FolFormula
toNnf
in class FolFormula
public java.lang.String toString()
toString
in class RelationalFormula
public ForallQuantifiedFormula clone()
SimpleLogicalFormula
clone
in interface ComplexLogicalFormula
clone
in interface SimpleLogicalFormula
clone
in class FolFormula