Orbital library

orbital.moon.logic.resolution
Class IndexedClausalSetImpl

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
                      extended by 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

Orbital library
1.3.0: 11 Apr 2009

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