ai.krr.propositions
Class Clause

java.lang.Object
  extended by ai.krr.propositions.Clause
All Implemented Interfaces:
java.lang.Cloneable, java.lang.Comparable<Clause>

public class Clause
extends java.lang.Object
implements java.lang.Cloneable, java.lang.Comparable<Clause>

A Clause consists of a list of Literals that are interpreted as a disjunction. Internally Literals are stored in an array. Note that the list representation means that the order of Literals within a Clause is relevant, e.g. for equality testing.

Author:
Gerhard Wickler

Field Summary
protected  Literal[] literals
          the Literals of this Clause
 
Constructor Summary
Clause(java.util.Collection<Literal> lits)
           This constructor for a Clause takes a Collection of Literals.
Clause(Literal... lits)
           This constructor for a Clause takes an Array of Literals.
 
Method Summary
protected  Clause clone()
           This function generates a shallow copy of this Clause.
 int compareTo(Clause other)
           This function compares this Clause to the given Clause.
 boolean contains(Literal literal)
           This function tests whether the given Literal is contained in this Clause.
 boolean equals(Clause other)
           This function tests whether this and the given Clause are equal.
 boolean equals(java.lang.Object obj)
           This function tests whether this and the given Object are equal.
 BooleanSymbol evaluate(Interpretation ipt)
           This function evaluates this Clause under the given Interpretation.
 Literal[] getLiterals()
           This function returns the the Literals that are joined in this Clause.
 java.util.Set<NamedSymbol> getPropositions()
           This function returns the set of propositional symbols that occur in this Clause.
 int hashCode()
           This function returns the hash code of this Clause.
 NamedSymbol isTautology()
           This function tests whether this clause is a tautology.
protected  Clause remove(Literal lit)
           This function returns a Clause in which the given Literal has been removed.
protected  Clause removeAll(java.util.Set<Literal> lits)
           This function returns a Clause in which the given Literals have been removed.
 int size()
           This function returns the number of Literals in this Clause.
 java.lang.String toString()
           A Clause is printed as:
 
Methods inherited from class java.lang.Object
finalize, getClass, notify, notifyAll, wait, wait, wait
 

Field Detail

literals

protected final Literal[] literals
the Literals of this Clause

Constructor Detail

Clause

public Clause(java.util.Collection<Literal> lits)

This constructor for a Clause takes a Collection of Literals. The given Collection should not contain duplicate Literals.

Parameters:
lits - the Literals to be connected here

Clause

public Clause(Literal... lits)

This constructor for a Clause takes an Array of Literals. The given Collection should not contain duplicate Literals.

Parameters:
lits - the Literals to be connected here
Method Detail

clone

protected Clause clone()

This function generates a shallow copy of this Clause. The copy will contain the same Literals as the original.

Overrides:
clone in class java.lang.Object
Returns:
an equal copy of this Clause

compareTo

public int compareTo(Clause other)

This function compares this Clause to the given Clause. The order between Clauses is primarily determined by their length: shorter Clauses come first. The order between Clauses of equal length is a lexical ordering, i.e. first the first Literals are compared. If they are different this determines the overall result, otherwise the second Literals are compared, etc. Note that Literals are not considered in the order given to the constructor, but in their natural order.

Specified by:
compareTo in interface java.lang.Comparable<Clause>
Parameters:
other - the Clause to which this Clause is to be compared
Returns:
0 if the two Clauses are identical; -1 if the given Clause should come after this Clause; and +1 if the given Clause should come before this Clause

getLiterals

public final Literal[] getLiterals()

This function returns the the Literals that are joined in this Clause.

Returns:
the Literals of this Clause

size

public int size()

This function returns the number of Literals in this Clause.

Returns:
the number of Literals in this Clause

contains

public boolean contains(Literal literal)

This function tests whether the given Literal is contained in this Clause.

Parameters:
literal - the Literal to be tested for
Returns:
whether lit is in this Clause

getPropositions

public java.util.Set<NamedSymbol> getPropositions()

This function returns the set of propositional symbols that occur in this Clause. The boolean propositions TRUE and FALSE will not be contained in the result.

Returns:
the Set of all the propositional symbols contained in this Clause

isTautology

public NamedSymbol isTautology()

This function tests whether this clause is a tautology. This is the case if it contains a complementary pair of Literals.

Returns:
the proposition that is both, negative and positive in this clause, or null if there is no such proposition

evaluate

public BooleanSymbol evaluate(Interpretation ipt)

This function evaluates this Clause under the given Interpretation. If all propositions occurring in the Clause have a truth value assigned by the Interpretation the result will be either BooleanSymbol.TRUE or BooleanSymbol.FALSE. Otherwise the result may be null, indicating the truth value of this Clause is undefined under the given Interpretation.

Parameters:
ipt - the Interpretation giving truth values for propositions
Returns:
the truth value of this Clause under the given Interpretation

toString

public java.lang.String toString()

A Clause is printed as:

 ( <literal>+ )
 

Overrides:
toString in class java.lang.Object
Returns:
the String that represents this Clause

equals

public boolean equals(java.lang.Object obj)

This function tests whether this and the given Object are equal. In general, two Clauses are equal if all the Literals are in the same order and equal.

Overrides:
equals in class java.lang.Object
Parameters:
obj - the Object this one is to be compared to
Returns:
whether the given Object is equal to this one

equals

public boolean equals(Clause other)

This function tests whether this and the given Clause are equal. In general, two Clauses are equal if they contain equal Literals, where the order of the Literals is only relevant if they are not sorted.

Parameters:
other - the Clause this one is to be compared to
Returns:
whether the given Object is equal to this one

hashCode

public final int hashCode()

This function returns the hash code of this Clause.

Overrides:
hashCode in class java.lang.Object
Returns:
a positive integer that may be used for hashing

remove

protected Clause remove(Literal lit)

This function returns a Clause in which the given Literal has been removed. If the given Literal is not contained in this Clause this Clause is returned.

Parameters:
lit - the Literal to be omitted in the copy
Returns:
a Clause not containing the given Literal

removeAll

protected Clause removeAll(java.util.Set<Literal> lits)

This function returns a Clause in which the given Literals have been removed. If none of the given Literals is contained in this Clause this Clause is returned.

Parameters:
lits - the Literals to be omitted in the copy
Returns:
a Clause not containing the given Literal