orbital.moon.logic.resolution
Class IndexedClauseImpl

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

All Implemented Interfaces:

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

Direct Known Subclasses:

OrderedClauseImpl

public class IndexedClauseImpl
extends ClauseImpl

Implementation of a representation of a clauses with clause indexing.

Author:

André Platzer

See Also:

ClausalIndex, Serialized Form

Field Summary

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

CONTRADICTION

Constructor Summary

IndexedClauseImpl()

IndexedClauseImpl(java.util.Set literals)
Copy constructor.

Method Summary

boolean	add(java.lang.Object o)
void	clear()
java.util.Iterator	getProbableUnifiables(Formula L) Get (an iterator over) all literals contained in this clause that may possibly unify with L.
java.util.Iterator	iterator()
boolean	remove(java.lang.Object o)

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

factorize, factorize, factorize2, getClausalFactory, getFreeVariables, getResolvableLiterals, getUnifiables, isElementaryValid, isElementaryValidUnion, resolventWith, resolventWith2, resolveWith, resolveWithFactors, resolveWithVariant, resolveWithVariantFactors, subsumes, toFormula, variant

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

IndexedClauseImpl

public IndexedClauseImpl(java.util.Set literals)

Copy constructor.

IndexedClauseImpl

public IndexedClauseImpl()

Method Detail

getProbableUnifiables

public java.util.Iterator getProbableUnifiables(Formula L)

Description copied from interface: Clause

Get (an iterator over) all literals contained in this clause that may possibly unify with L. The formulas returned will more likely qualify for unification with C, but need not do so with absolute confidence.

Implementations may use indexing or links to estimate the clauses to return very quickly. Furthermore, implementations may apply selection refinements.

Specified by:

getProbableUnifiables in interface Clause

Overrides:

getProbableUnifiables in class ClauseImpl

See Also:

Clause.getUnifiables(Formula)

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