org.sat4j.minisat.constraints
Class AbstractDataStructureFactory<L extends ILits>

java.lang.Object
  org.sat4j.minisat.constraints.AbstractDataStructureFactory<L>

All Implemented Interfaces:

java.io.Serializable, DataStructureFactory<L>

Direct Known Subclasses:

AbstractCardinalityDataStructure, ClausalDataStructureCB, ClausalDataStructureCBHT, ClausalDataStructureHT, MixedDataStructureDaniel, MixedDataStructureWithBinary, MixedDataStructureWithBinaryAndTernary

public abstract class AbstractDataStructureFactory<L extends ILits>
extends java.lang.Object
implements DataStructureFactory<L>, java.io.Serializable

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

Field Summary

protected Learner	learner
protected L	lits
protected UnitPropagationListener	solver

Constructor Summary

protected

AbstractDataStructureFactory()

Method Summary

void	conflictDetectedInAttachesFor(int p, int i)
Constr	createCardinalityConstraint(IVecInt literals, int degree)
protected abstract L	createLits()
IVec<Propagatable>	getAttachesFor(int p)
L	getVocabulary()
void	learnConstraint(Constr constr)
void	reset()
void	setLearner(Learner learner)
void	setUnitPropagationListener(UnitPropagationListener s)

Methods inherited from class java.lang.Object

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

Methods inherited from interface org.sat4j.minisat.core.DataStructureFactory

createClause, createUnregisteredClause

Field Detail

lits

protected L extends ILits lits

solver

protected UnitPropagationListener solver

learner

protected Learner learner

Constructor Detail

AbstractDataStructureFactory

protected AbstractDataStructureFactory()

Method Detail

conflictDetectedInAttachesFor

public void conflictDetectedInAttachesFor(int p,
                                          int i)

Specified by:

conflictDetectedInAttachesFor in interface DataStructureFactory<L extends ILits>

i - the index of the conflicting constraint

getAttachesFor

public IVec<Propagatable> getAttachesFor(int p)

Specified by:

getAttachesFor in interface DataStructureFactory<L extends ILits>

Returns:

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

createLits

protected abstract L createLits()

getVocabulary

public L getVocabulary()

Specified by:

getVocabulary in interface DataStructureFactory<L extends ILits>

setUnitPropagationListener

public void setUnitPropagationListener(UnitPropagationListener s)

Specified by:

setUnitPropagationListener in interface DataStructureFactory<L extends ILits>

setLearner

public void setLearner(Learner learner)

Specified by:

setLearner in interface DataStructureFactory<L extends ILits>

reset

public void reset()

Specified by:

reset in interface DataStructureFactory<L extends ILits>

learnConstraint

public void learnConstraint(Constr constr)

Specified by:

learnConstraint in interface DataStructureFactory<L extends ILits>

createCardinalityConstraint

public Constr createCardinalityConstraint(IVecInt literals,
                                          int degree)
                                   throws ContradictionException

Specified by:

createCardinalityConstraint in interface DataStructureFactory<L extends ILits>

Throws:

ContradictionException