orbital.moon.logic.resolution
Class ClausalSetImpl

java.lang.Object
  java.util.AbstractCollection
      java.util.AbstractSet
          java.util.HashSet
              java.util.LinkedHashSet
                  orbital.moon.logic.resolution.ClausalSetImpl

All Implemented Interfaces:

java.io.Serializable, java.lang.Cloneable, java.lang.Iterable, java.util.Collection, java.util.Set, ClausalSet

Direct Known Subclasses:

IndexedClausalSetImpl

public class ClausalSetImpl
extends java.util.LinkedHashSet
implements ClausalSet

Default implementation of a representation of a set of clauses.

Author:

André Platzer

See Also:

Serialized Form

Field Summary

Fields inherited from interface orbital.moon.logic.resolution.ClausalSet

CONTRADICTION_SINGLETON_SET, TAUTOLOGY_SINGLETON_SET

Constructor Summary

ClausalSetImpl()

ClausalSetImpl(java.util.Set clauses)
Copy constructor.

Method Summary

java.util.Iterator	getProbableComplementsOf(Clause C) Get (an iterator over) all clauses contained in this set that may possibly form a complement to C for resolution.
boolean	removeAllSubsumedBy(ClausalSet T) Remove all clauses from this set which are subsumed by any of the clauses of T.
Formula	toFormula() Convert this set of clauses to a formula representation.

Methods inherited from class java.util.HashSet

add, clear, clone, contains, isEmpty, iterator, remove, size

Methods inherited from class java.util.AbstractSet

equals, hashCode, removeAll

Methods inherited from class java.util.AbstractCollection

addAll, containsAll, retainAll, toArray, toArray, toString

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface java.util.Set

add, addAll, clear, contains, containsAll, equals, hashCode, isEmpty, iterator, remove, removeAll, retainAll, size, toArray, toArray

Constructor Detail

ClausalSetImpl

public ClausalSetImpl(java.util.Set clauses)

Copy constructor.

ClausalSetImpl

public ClausalSetImpl()

Method Detail

getProbableComplementsOf

public java.util.Iterator getProbableComplementsOf(Clause C)

Description copied from interface: ClausalSet

Get (an iterator over) all clauses contained in this set that may possibly form a complement to C for resolution. The clauses returned will more likely qualify for resolution with C, but need not do so with absolute confidence.

Implementations may use indexing to estimate the clauses to return very quickly.

Specified by:

getProbableComplementsOf in interface ClausalSet

removeAllSubsumedBy

public boolean removeAllSubsumedBy(ClausalSet T)

Description copied from interface: ClausalSet

Remove all clauses from this set which are subsumed by any of the clauses of T.

In case of T == this, don't let clauses remove by mutual subsumption, or by self-subsumption.

Specified by:

removeAllSubsumedBy in interface ClausalSet

Returns:

whether this set has changed as a result of the deletion by subsumption.

toFormula

public Formula toFormula()

Description copied from interface: ClausalSet

Convert this set of clauses to a formula representation.

Specified by:

toFormula in interface ClausalSet