org.sat4j.minisat.constraints
Class AbstractDataStructureFactory

java.lang.Object
  org.sat4j.minisat.constraints.AbstractDataStructureFactory

All Implemented Interfaces:

Serializable, DataStructureFactory

Direct Known Subclasses:

AbstractCardinalityDataStructure, AbstractPBDataStructureFactory, ClausalDataStructureWL, MixedDataStructureDanielHT, MixedDataStructureDanielWL, MixedDataStructureSingleWL

public abstract class AbstractDataStructureFactory
extends Object
implements DataStructureFactory, 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 ILits	lits
protected UnitPropagationListener	solver

Constructor Summary

protected

AbstractDataStructureFactory()

Method Summary

void	conflictDetectedInWatchesFor(int p, int i)
Constr	createCardinalityConstraint(IVecInt literals, int degree) Create a cardinality constraint of the form sum li >= degree.
protected abstract ILits	createLits()
ILits	getVocabulary()
IVec<Propagatable>	getWatchesFor(int p)
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 ILits lits

solver

protected UnitPropagationListener solver

learner

protected Learner learner

Constructor Detail

AbstractDataStructureFactory

protected AbstractDataStructureFactory()

Method Detail

conflictDetectedInWatchesFor

public void conflictDetectedInWatchesFor(int p,
                                         int i)

Specified by:

conflictDetectedInWatchesFor in interface DataStructureFactory

i - the index of the conflicting constraint

getWatchesFor

public IVec<Propagatable> getWatchesFor(int p)

Specified by:

getWatchesFor in interface DataStructureFactory

Returns:

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

createLits

protected abstract ILits createLits()

getVocabulary

public ILits getVocabulary()

Specified by:

getVocabulary in interface DataStructureFactory

setUnitPropagationListener

public void setUnitPropagationListener(UnitPropagationListener s)

Specified by:

setUnitPropagationListener in interface DataStructureFactory

setLearner

public void setLearner(Learner learner)

Specified by:

setLearner in interface DataStructureFactory

reset

public void reset()

Specified by:

reset in interface DataStructureFactory

learnConstraint

public void learnConstraint(Constr constr)

Specified by:

learnConstraint in interface DataStructureFactory

createCardinalityConstraint

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

Description copied from interface: DataStructureFactory

Create a cardinality constraint of the form sum li >= degree.

Specified by:

createCardinalityConstraint in interface DataStructureFactory

Parameters:

literals - a set of literals.

degree - the degree of the cardinality constraint.

Returns:

a constraint stating that at least degree literals are satisfied.

Throws:

ContradictionException