orbital.moon.logic.resolution
Class IndexedClausalSetImpl

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

All Implemented Interfaces:

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

public class IndexedClausalSetImpl
extends ClausalSetImpl

Implementation of a representation of a set of clauses with clause indexing.

Author:

André Platzer

See Also:

ClausalIndex, Serialized Form

Field Summary

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

CONTRADICTION_SINGLETON_SET, TAUTOLOGY_SINGLETON_SET

Constructor Summary

IndexedClausalSetImpl()

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

Method Summary

boolean	add(java.lang.Object o)
void	clear()
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.
java.util.Iterator	getProbableUnifiables(Formula L) Get an iterator of all clauses that contain literals which could possibly unify with L.
java.util.Iterator	iterator()
boolean	remove(java.lang.Object o)

Methods inherited from class orbital.moon.logic.resolution.ClausalSetImpl

removeAllSubsumedBy, toFormula

Methods inherited from class java.util.HashSet

clone, contains, isEmpty, 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

addAll, contains, containsAll, equals, hashCode, isEmpty, removeAll, retainAll, size, toArray, toArray

Constructor Detail

IndexedClausalSetImpl

public IndexedClausalSetImpl(java.util.Set clauses)

Copy constructor.

IndexedClausalSetImpl

public IndexedClausalSetImpl()

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

Overrides:

getProbableComplementsOf in class ClausalSetImpl

getProbableUnifiables

public java.util.Iterator getProbableUnifiables(Formula L)

Get an iterator of all clauses that contain literals which could possibly unify with L.

add

public boolean add(java.lang.Object o)

Specified by:

add in interface java.util.Collection

Specified by:

add in interface java.util.Set

Overrides:

add in class java.util.HashSet

clear

public void clear()

Specified by:

clear in interface java.util.Collection

Specified by:

clear in interface java.util.Set

Overrides:

clear in class java.util.HashSet

remove

public boolean remove(java.lang.Object o)

Specified by:

remove in interface java.util.Collection

Specified by:

remove in interface java.util.Set

Overrides:

remove in class java.util.HashSet

iterator

public java.util.Iterator iterator()

Specified by:

iterator in interface java.lang.Iterable

Specified by:

iterator in interface java.util.Collection

Specified by:

iterator in interface java.util.Set

Overrides:

iterator in class java.util.HashSet