org.sat4j.minisat.constraints
Class ClausalDataStructureWL

java.lang.Object
  extended by org.sat4j.minisat.constraints.AbstractDataStructureFactory
      extended by org.sat4j.minisat.constraints.ClausalDataStructureWL
All Implemented Interfaces:
java.io.Serializable, DataStructureFactory
Direct Known Subclasses:
MixedDataStructureDaniel

public class ClausalDataStructureWL
extends AbstractDataStructureFactory

Author:
leberre To change the template for this generated type comment go to Window - Preferences - Java - Code Generation - Code and Comments
See Also:
Serialized Form

Constructor Summary
ClausalDataStructureWL()
           
 
Method Summary
 Constr createClause(IVecInt literals)
           
 Constr createUnregisteredClause(IVecInt literals)
           
 
Methods inherited from class org.sat4j.minisat.constraints.AbstractDataStructureFactory
conflictDetectedInWatchesFor, createCardinalityConstraint, createPseudoBooleanConstraint, createUnregisteredPseudoBooleanConstraint, getVocabulary, getWatchesFor, learnConstraint, reset, setLearner, setUnitPropagationListener
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

ClausalDataStructureWL

public ClausalDataStructureWL()
Method Detail

createClause

public Constr createClause(IVecInt literals)
                    throws ContradictionException
Parameters:
literals - a set of literals using Dimacs format (signed non null integers).
Returns:
null if the constraint is a tautology.
Throws:
ContradictionException - the constraint is trivially unsatisfiable.

createUnregisteredClause

public Constr createUnregisteredClause(IVecInt literals)