ai.krr.propositions
Class IntEncodedClause

java.lang.Object
  ai.krr.propositions.IntEncodedClause

All Implemented Interfaces:

java.lang.Cloneable, java.lang.Comparable<IntEncodedClause>

Direct Known Subclasses:

RTPSolverIE.DerivedClause

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

An IntEncodedClause consists of a list of Literals that are interpreted as a disjunction. Internally Literals are stored in an array of ints, using an encoding provided at construction time. Note that the list representation means that the order of Literals within a Clause may be relevant, e.g. for equality testing. However, IntEncodedClauses that contain more than a fixed number of Literals will be sorted.

Author:

Gerhard Wickler

Nested Class Summary

protected static class	IntEncodedClause.CnfIntEncodedClauseListAdaptor
protected static class	IntEncodedClause.IntEncodedClauseList
protected static class	IntEncodedClause.LiteralSet

Field Summary

protected int	hValue a cached hash value for this Clause
protected int[]	literals the encoded Literals in this Clause

Constructor Summary

protected	IntEncodedClause(java.util.Collection<java.lang.Integer> lits) This constructor creates a Clause from the given Literals.
protected	IntEncodedClause(int[] lits) This constructor creates a Clause from the given Literals and hash value.
	IntEncodedClause(IntEncoding enc, java.util.Collection<Literal> lits) This constructor for a Clause takes a Collection of Literals.
	IntEncodedClause(IntEncoding enc, Literal... lits) This constructor for a Clause takes an Array of Literals.

Method Summary

protected IntEncodedClause	clone() This function generates a shallow copy of this Clause.
int	compareTo(IntEncodedClause other) This function compares this Clause to the given Clause.
boolean	contains(int literal) This function tests whether the given Literal is contained in this Clause.
boolean	equals(IntEncodedClause 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.
int[]	getLiterals() This function returns the the Literals that are joined in this Clause.
java.util.Set<NamedSymbol>	getPropositions(IntEncoding encoding) This function returns the set of propositional symbols that occur in this Clause.
int	hashCode() This function returns the hash code of this Clause.
int	isTautology() This function tests whether this clause is a tautology.
protected IntEncodedClause	remove(int lit) This function returns a shallow copy of this Clause in which the given Literal has 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 int[] literals

the encoded Literals in this Clause

hValue

protected final int hValue

a cached hash value for this Clause

Constructor Detail

IntEncodedClause

public IntEncodedClause(IntEncoding enc,
                        java.util.Collection<Literal> lits)

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

Parameters:

enc - the Class used for consistently encoding Literals as ints

lits - the Literals to be connected here

IntEncodedClause

public IntEncodedClause(IntEncoding enc,
                        Literal... lits)

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

Parameters:

enc - the Class used for consistently encoding Literals as ints

lits - the Literals to be connected here

IntEncodedClause

protected IntEncodedClause(java.util.Collection<java.lang.Integer> lits)

This constructor creates a Clause from the given Literals.

IntEncodedClause

protected IntEncodedClause(int[] lits)

This constructor creates a Clause from the given Literals and hash value.

Method Detail

clone

protected IntEncodedClause 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(IntEncodedClause 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 in which they are stored internally, which may be sorted.

Specified by:

compareTo in interface java.lang.Comparable<IntEncodedClause>

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 int[] 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(int 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(IntEncoding encoding)

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 int 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 0 if there is no such proposition

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(IntEncodedClause 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 IntEncodedClause remove(int lit)

This function returns a shallow copy of this Clause in which the given Literal has been removed. If the given Literal is not contained in this Clause this function returns null.

Parameters:

lit - the Literal to be omitted in the copy

Returns:

a new Clause not containing the given Literal or null