ai.krr.propositions
Class Clause

java.lang.Object
  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