Class Clause

java.lang.Object
  |
  +--Clause

Direct Known Subclasses:

Conjecture, SpecialClause

public class Clause

extends Object

This class implements a clause.

Author:

P. URSO

See Also:

EqualList

Field Summary

protected EqualList	conj Both side of the clause.
protected EqualList	disj Both side of the clause.
protected static int	HYPOTHESE_NUM Clause number for an hypothese.
protected static int	LEMMA_NUM Clause number for a lemma.

Constructor Summary

Clause(EqualList conj, EqualList disj)
Constructor of a clause.

Method Summary

EqualList	body() Returns the body of an clause.
EqualList	conditions() Returns the conditions of an clause.
boolean	emptyBody() Indicates if this clause posses an empty body.
boolean	equals(Object o) Tests if some other object is "equal to" this one.
protected static String	num(int n) Returns a representation of a clause number.
Equality	oriented() Returns an orientation of this clause if possible.
protected static String	prefix(int n) Returns a representation of a clause number between brackets.
Equality	semiOriented() Returns a semi-orientation of this close.
String	toString() Returns a string representation of this clause.

Methods inherited from class java.lang.Object

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

Field Detail

conj

protected EqualList conj

Both side of the clause.

disj

protected EqualList disj

Both side of the clause.

HYPOTHESE_NUM

protected static final int HYPOTHESE_NUM

Clause number for an hypothese.

LEMMA_NUM

protected static final int LEMMA_NUM

Clause number for a lemma.

Constructor Detail

Clause

public Clause(EqualList conj,
              EqualList disj)

Constructor of a clause.

Parameters:

conj - conjonction part of the clause.

disj - disjonction part of the clause.

Method Detail

conditions

public EqualList conditions()

Returns the conditions of an clause.

Returns:

the conditions of an clause.

body

public EqualList body()

Returns the body of an clause.

Returns:

the body of an clause.

emptyBody

public boolean emptyBody()

Indicates if this clause posses an empty body.

semiOriented

public Equality semiOriented()

Returns a semi-orientation of this close. A clause is semi-oriented if the body of the clause got an unique equality and if all sides in conditions are lower one of the side of the body.

Returns:

the unique equality of the body if greater than condition, null otherwise.

oriented

public Equality oriented()

Returns an orientation of this clause if possible. A clause is oriented if it got an unique equality in its body, if one side of this equality is greater than the other, and if all sides in conditions are lower than this side.

Returns:

an oriented equality if it exists, null otherwise.

See Also:

Node

equals

public boolean equals(Object o)

Tests if some other object is "equal to" this one.

Overrides:

equals in class Object

Parameters:

o - the object with which to compare.

Returns:

true if o is a clause and both part are equal.

num

protected static String num(int n)

Returns a representation of a clause number.

Returns:

a number, H, or L.

prefix

protected static String prefix(int n)

Returns a representation of a clause number between brackets.

Returns:

clause number with extra space or not.

toString

public String toString()

Returns a string representation of this clause. The string representation consists of two lists of equalities. The one before the imply sign " => " is a conjonction, and the one after is a disjonction.

Overrides:

toString in class Object

Returns:

a string representation of this clause.

See Also:

EqualList