Package org.tweetyproject.logics.commons.syntax

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.