edu.kit.iti.lfm.spotlight

Class Formula

java.lang.Object

edu.kit.iti.lfm.spotlight.Formula

Direct Known Subclasses:

Formula.And, Formula.Equiv, Formula.Impl, Formula.Literal, Formula.Not, Formula.Or

public abstract class Formula
extends Object

This class is the abstract base class to model propositional formulas of arbitrary structure. The propositional atoms are denoted as DIMACS integer values: Positive integers denote positive literals, and negative denote negative literals. 0 is not permitted as input.

The class has several subclasses implementing various propositional operators:

• Formula.And implementing conjunctions (2 subformulas)
• Formula.Or implementing disjunctions (2 subformulas)
• Formula.Impl implementing implications (2 subformulas)
• Formula.Equiv implementing equivalences (2 subformulas)
• Formula.Not implementing negation (1 subformula)
• Formula.Literal implementing a propositional literal (no subformulas)

Subformulas

Every formula has none, one or two direct subformulas. You can query the number of subformulas using method countSubFormulas(). The subformulas can be retrieved using getSubFormula(int). The first subformula has index 0.

FormulaVisitor

The interface FormulaVisitor can be used traverse a formula and can be helpful, e.g., to transform the formula into a different logical representation.

Example

The formula ¬(P₁ ∧ P₁₂) ∨ ¬ P₁ for the two propositional variables P1 and P12 can be constructed as follows

 new Or(new Not(new And(new Literal(1), new Literal(12))), new Literal(-1))
 

or alternatively as the equivalent (but not equal!) formula

 new Or(new Not(new And(new Literal(1), new Literal(12))), new Not(new Literal(1)))
 

assuming that for the above code, import static edu.kit.iti.lfm.spotlight.Formula.*; has been added to the beginning of the compilation unit.

Author:

Mattias Ulbrich, David Farago

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
static class	Formula.And Propositional conjunction The conjunction takes two subformulas.
static class	Formula.Equiv Propositional equivalence The equivalence takes two subformulas.
static class	Formula.Impl Propositional implication The implication takes two subformulas.
static class	Formula.Literal Prositional literal Literals are the basic blocks of formulas.
static class	Formula.Not Propositional negation The negation takes one subformula.
static class	Formula.Or Propositional disjunction The disjunction takes two subformulas.

Field Summary

Fields

Modifier and Type	Field and Description
static int	depth
static Formula	FALSE
static Formula	TRUE

Method Summary

Methods

Modifier and Type	Method and Description
abstract int	accept(FormulaVisitor visitor) Entry point for a FormulaVisitor.
int	countSubFormulas() Get the number of direct subformulas for this formula.
boolean	equals(Object o) Indicate whether some other object is "equal to" this one.
Formula	getSubFormula(int idx) Get a sub formula of this formula.
int	hashCode() Return a hash code value for the object.
abstract String	toString() Return a string representation of the object.

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

TRUE

public static final Formula TRUE

FALSE

public static final Formula FALSE

depth

public static int depth

Method Detail

accept

public abstract int accept(FormulaVisitor visitor)

Entry point for a FormulaVisitor.

This methods realises the accept-part of the visitor pattern.

Parameters:

visitor - a non-null visitor reference

Returns:

an integer value, its meanings depends on the visitor.

equals

public boolean equals(Object o)

Indicate whether some other object is "equal to" this one.

This formula is considered equal to another object if they are of the same class and their subFormulas are pairwise equal.

Overrides:

equals in class Object

Parameters:

o - an arbitrary reference

hashCode

public int hashCode()

Return a hash code value for the object.

The hashcode of a formula is the hashcode of its string representation.

Overrides:

hashCode in class Object

Returns:

a hash code value for this object.

getSubFormula

public Formula getSubFormula(int idx)
                      throws IndexOutOfBoundsException

Get a sub formula of this formula.

The first subformula has index 0, the last has index countSubFormulas()-1.

Parameters:

idx - the index of the subformula to get

Returns:

a non-null reference to a formula.

Throws:

IndexOutOfBoundsException - if idx < 0 or idx >= countSubFormulas()

countSubFormulas

public int countSubFormulas()

Get the number of direct subformulas for this formula.

Returns:

the non-negative count of subformulas

toString

public abstract String toString()

Return a string representation of the object.

Formulas are represented using unicode infix and prefix operators.

Overrides:

toString in class Object

Returns:

a string representation of this formula.