edu.kit.iti.lfm.spotlight

Class Clause

java.lang.Object

edu.kit.iti.lfm.spotlight.Clause

public class Clause
extends Object

The Class Clause represents DIMACS clauses.

A clause is a list of integers different from 0. A clause is to be interpreted as the disjunction of the literals that are represented by the integer values. In DIMACS, literals are represented by integers. Positive numbers 1,2,... represent the first, second, ... propositional variable. Negative numbers -1,-2, ... represent the negation of the first, second, ... variable. For instance, the formula (¬A ∨ B) ∧ (C ∨ ¬B) can be represented as the two clauses {-1, 2} and {3, -2}.

Creation of clauses

Clauses are immutable objects. After creation, the values of their fields cannot be changed. If you want to add literals to an existing clause, you can use the methods concat(int) or concat(Clause) which result in new clauses without changing the receiver of the method call.

Constructor Summary

Constructors

Constructor and Description
Clause(int... literals) Instantiates a new clause from a list of literals.
Clause(int[] array, int start, int len) Instantiates a new clause from a segment of an integer array

Method Summary

Methods

Modifier and Type	Method and Description
Clause	concat(Clause clause) Get a clause that represents this clause augmented by the literals of the argument.
Clause	concat(int literal) Get a clause that represents this clause augmented by an additional literal.
int	getMaxVar() Get the largest index of all literals in the clause.
int	getVariable(int var)
int[]	toArray() Extract the integer values of this clause into an array.
String	toDIMACS() Translate the clause to DIMACS text representation.
String	toString() A clause is textually represented as a list in curly braces.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Constructor Detail

Clause

public Clause(int... literals)
       throws IllegalArgumentException

Instantiates a new clause from a list of literals.

Parameters:

literals - a list of zero or more literal integers (different from 0)

Throws:

IllegalArgumentException - iff the list of literals contains the value 0.

Clause

public Clause(int[] array,
      int start,
      int len)
       throws IndexOutOfBoundsException,
              IllegalArgumentException,
              NullPointerException

Instantiates a new clause from a segment of an integer array

Parameters:

array - the non-null array to take the literals from

start - the first index in array to take literals from

len - the number of literals to take from the array

Throws:

IndexOutOfBoundsException - if start is outside the array index range or if start+len is outside.

IllegalArgumentException - if 0 is contained in the array or if len < 0.

NullPointerException - if array is null

Method Detail

concat

public Clause concat(int literal)
              throws IllegalArgumentException

Get a clause that represents this clause augmented by an additional literal. The parameter must not be 0.

Parameters:

literal - the additional literal

Returns:

the clause corresponding to this clause extended by literal.

Throws:

IllegalArgumentException - if the arguments is 0

concat

public Clause concat(Clause clause)

Get a clause that represents this clause augmented by the literals of the argument.

Parameters:

clause - the additional literals

Returns:

the clause corresponding to this clause extended by clause.

toString

public String toString()

A clause is textually represented as a list in curly braces.

For example: The expression new Clause(-1,2,2).toString() yields {-1,2,2}.

Overrides:

toString in class Object

toDIMACS

public String toDIMACS()

Translate the clause to DIMACS text representation.

In DIMACS text representation literals are separated by space characters and clauses terminated by a single 0.

For example: The expression new Clause(-1,2,2).toDIMACS() yields -1 2 2 0.

Returns:

the DIMACS representation of this clause.

toArray

public int[] toArray()

Extract the integer values of this clause into an array.

For example: The expression Clause.make(-1,2,2).toArray() yields [-1,2,2]. The result is freshly created. You may safely change it.

Returns:

a freshly created array of integers

getMaxVar

public int getMaxVar()

Get the largest index of all literals in the clause.

The index of a literal is the used variable number, i.e. the absolute value.

For example: The expression new Clause(-1,2,2).getMaxVar() yields 2. The expression new Clause(5,-7).getMaxVar() yields 7.

Returns:

the largest index of all literals in the clause. 0 for the empty clause.

getVariable

public int getVariable(int var)
                throws IllegalArgumentException

Throws:

IllegalArgumentException