Class QuantifiedFormulaSupport<T extends RelationalFormula>

java.lang.Object
org.tweetyproject.logics.commons.syntax.QuantifiedFormulaSupport<T>
Type Parameters:
T - The type of the formulas which are quantified.
public class QuantifiedFormulaSupport<T extends RelationalFormula> extends Object
This class provides common functionalities for quantified formulas, i.e. forall and exists quantified formulas.
Author:
Matthias Thimm, Anna Gessler

  • Constructor Summary

    Constructors
    Constructor
    Description
    QuantifiedFormulaSupport(T formula, Set<Variable> variables)
    Constructs a new QuantifiedFormulaSupport instance with the specified formula and quantifier variables.

  • Method Summary

    Modifier and Type
    Method
    Description
    boolean
    containsQuantifier()
    Checks whether the formula contains a quantifier.
    Set<? extends Atom>
    getAtoms()
    Returns the set of atoms contained in the inner formula.
    T
    getFormula()
    Returns the formula that this quantified formula ranges over.
    Set<Functor>
    getFunctors()
    Returns the set of functors contained in the inner formula.
    Set<? extends Predicate>
    getPredicates()
    Returns the set of predicates contained in the inner formula.
    Set<Variable>
    getQuantifierVariables()
    Returns the set of variables that are quantified within this formula.
    Set<Term<?>>
    getTerms()
    Returns the set of terms used in the inner formula.
    <C extends Term<?>>
    Set<C>
    getTerms(Class<C> cls)
    Returns the set of terms of a specified type used in the inner formula.
    Set<Variable>
    getUnboundVariables()
    Returns the set of unbound variables in the inner formula, excluding the quantified variables.
    int
    hashCode()
    Computes the hash code for this QuantifiedFormulaSupport object.
    boolean
    isClosed()
    Checks whether the formula is closed, meaning all variables are bound by a quantifier.
    boolean
    isClosed(Set<Variable> boundVariables)
    Checks whether the formula is closed when considering an additional set of bound variables.
    boolean
    isDnf()
    Checks whether the formula is in Disjunctive Normal Form (DNF).
    boolean
    isLiteral()
    Checks whether the formula is a literal.
    boolean
    isWellBound()
    Checks whether the formula is well-bound, meaning no variable is bound more than once.
    boolean
    isWellBound(Set<Variable> boundVariables)
    Checks whether the formula is well-bound when considering an additional set of bound variables.
    void
    setFormula(T formula)
    Sets the formula that this quantified formula ranges over.
    void
    setQuantifierVariables(Set<Variable> variables)
    Sets the set of variables that are quantified within this formula.

    Methods inherited from class java.lang.Object

    equals, getClass, notify, notifyAll, toString, wait, wait, wait

  • Constructor Details

    • QuantifiedFormulaSupport

      public QuantifiedFormulaSupport(T formula, Set<Variable> variables)
      Constructs a new QuantifiedFormulaSupport instance with the specified formula and quantifier variables.
      Parameters:
      formula - The relational formula that this quantified formula ranges over.
      variables - The set of variables that are quantified within the formula.

  • Method Details

    • getFormula

      public T getFormula()
      Returns the formula that this quantified formula ranges over.
      Returns:
      The relational formula that this quantified formula ranges over.

    • getQuantifierVariables

      public Set<Variable> getQuantifierVariables()
      Returns the set of variables that are quantified within this formula.
      Returns:
      The set of quantified variables.

    • setFormula

      public void setFormula(T formula)
      Sets the formula that this quantified formula ranges over.
      Parameters:
      formula - The relational formula to set.

    • setQuantifierVariables

      public void setQuantifierVariables(Set<Variable> variables)
      Sets the set of variables that are quantified within this formula.
      Parameters:
      variables - The set of variables to be quantified.

    • isClosed

      public boolean isClosed()
      Checks whether the formula is closed, meaning all variables are bound by a quantifier.
      Returns:
      true if the formula is closed, false otherwise.

    • isClosed

      public boolean isClosed(Set<Variable> boundVariables)
      Checks whether the formula is closed when considering an additional set of bound variables.
      Parameters:
      boundVariables - The set of additional variables considered to be bound.
      Returns:
      true if the formula is closed with the additional variables, false otherwise.

    • containsQuantifier

      public boolean containsQuantifier()
      Checks whether the formula contains a quantifier.
      Returns:
      true since this support class is specifically for quantified formulas.

    • isWellBound

      public boolean isWellBound()
      Checks whether the formula is well-bound, meaning no variable is bound more than once.
      Returns:
      true if the formula is well-bound, false otherwise.

    • isWellBound

      public boolean isWellBound(Set<Variable> boundVariables)
      Checks whether the formula is well-bound when considering an additional set of bound variables.
      Parameters:
      boundVariables - The set of additional variables considered to be bound.
      Returns:
      true if the formula is well-bound with the additional variables, false otherwise.

    • getPredicates

      public Set<? extends Predicate> getPredicates()
      Returns the set of predicates contained in the inner formula.
      Returns:
      A set of predicates used in the inner formula.

    • getFunctors

      public Set<Functor> getFunctors()
      Returns the set of functors contained in the inner formula.
      Returns:
      A set of functors used in the inner formula.

    • getAtoms

      public Set<? extends Atom> getAtoms()
      Returns the set of atoms contained in the inner formula.
      Returns:
      A set of atoms used in the inner formula.

    • getUnboundVariables

      public Set<Variable> getUnboundVariables()
      Returns the set of unbound variables in the inner formula, excluding the quantified variables.
      Returns:
      A set of unbound variables in the inner formula.

    • isDnf

      public boolean isDnf()
      Checks whether the formula is in Disjunctive Normal Form (DNF).
      Returns:
      false, as this class does not specifically check for DNF.

    • isLiteral

      public boolean isLiteral()
      Checks whether the formula is a literal.
      Returns:
      false, as this class is intended for quantified formulas, not literals.

    • getTerms

      public Set<Term<?>> getTerms()
      Returns the set of terms used in the inner formula.
      Returns:
      A set of terms used in the inner formula.

    • getTerms

      public <C extends Term<?>> Set<C> getTerms(Class<C> cls)
      Returns the set of terms of a specified type used in the inner formula.
      Type Parameters:
      C - The type of terms to return.
      Parameters:
      cls - The class object representing the type of terms to return.
      Returns:
      A set of terms of the specified type used in the inner formula.

    • hashCode

      public int hashCode()
      Computes the hash code for this QuantifiedFormulaSupport object.
      Overrides:
      hashCode in class Object
      Returns:
      The hash code value for this object.