Orbital library

orbital.moon.logic.resolution
Class ClausalSetImpl

java.lang.Object
  extended by java.util.AbstractCollection
      extended by java.util.AbstractSet
          extended by java.util.HashSet
              extended by java.util.LinkedHashSet
                  extended by 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

Orbital library
1.3.0: 11 Apr 2009

Copyright © 1996-2009 André Platzer
All Rights Reserved.