org.sat4j.minisat.constraints
Class ClausalDataStructureCB

java.lang.Object
  org.sat4j.minisat.constraints.AbstractDataStructureFactory<ILits>
      org.sat4j.minisat.constraints.ClausalDataStructureCB

All Implemented Interfaces:

java.io.Serializable, DataStructureFactory<ILits>

public class ClausalDataStructureCB
extends AbstractDataStructureFactory<ILits>

Author:

parrain To change the template for this generated type comment go to Window - Preferences - Java - Code Generation - Code and Comments

See Also:

Serialized Form

Field Summary

Fields inherited from class org.sat4j.minisat.constraints.AbstractDataStructureFactory

learner, lits, solver

Constructor Summary

ClausalDataStructureCB()

Method Summary

void	conflictDetectedInWatchesFor(int p, int i)
Constr	createClause(IVecInt literals)
protected ILits	createLits()
Constr	createUnregisteredClause(IVecInt literals)
IVec<Propagatable>	getWatchesFor(int p)

Methods inherited from class org.sat4j.minisat.constraints.AbstractDataStructureFactory

createCardinalityConstraint, createPseudoBooleanConstraint, createUnregisteredPseudoBooleanConstraint, getVocabulary, learnConstraint, reset, setLearner, setUnitPropagationListener

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

ClausalDataStructureCB

public ClausalDataStructureCB()

Method Detail

conflictDetectedInWatchesFor

public void conflictDetectedInWatchesFor(int p,
                                         int i)

Specified by:

conflictDetectedInWatchesFor in interface DataStructureFactory<ILits>

Overrides:

conflictDetectedInWatchesFor in class AbstractDataStructureFactory<ILits>

i - the index of the conflicting constraint

getWatchesFor

public IVec<Propagatable> getWatchesFor(int p)

Specified by:

getWatchesFor in interface DataStructureFactory<ILits>

Overrides:

getWatchesFor in class AbstractDataStructureFactory<ILits>

Returns:

a vector containing all the objects to be notified of the satisfaction of that literal.

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)

createLits

protected ILits createLits()

Specified by:

createLits in class AbstractDataStructureFactory<ILits>