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, AbstractPBDataStructureFactory, ClausalDataStructureCB, ClausalDataStructureCBWL, ClausalDataStructureWL, 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

Method Summary

void	conflictDetectedInWatchesFor(int p, int i)
Constr	createCardinalityConstraint(IVecInt literals, int degree)
Constr	createPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
Constr	createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
L	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

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

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

createClause, createUnregisteredClause

Method Detail

conflictDetectedInWatchesFor

public void conflictDetectedInWatchesFor(int p,
                                         int i)

Specified by:

conflictDetectedInWatchesFor in interface DataStructureFactory<L extends ILits>

i - the index of the conflicting constraint

getWatchesFor

public IVec<Propagatable> getWatchesFor(int p)

Specified by:

getWatchesFor in interface DataStructureFactory<L extends ILits>

Returns:

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

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

createPseudoBooleanConstraint

public Constr createPseudoBooleanConstraint(IVecInt literals,
                                            IVec<java.math.BigInteger> coefs,
                                            boolean moreThan,
                                            java.math.BigInteger degree)
                                     throws ContradictionException

Specified by:

createPseudoBooleanConstraint in interface DataStructureFactory<L extends ILits>

Throws:

ContradictionException

createUnregisteredPseudoBooleanConstraint

public Constr createUnregisteredPseudoBooleanConstraint(IVecInt literals,
                                                        IVec<java.math.BigInteger> coefs,
                                                        java.math.BigInteger degree)

Specified by:

createUnregisteredPseudoBooleanConstraint in interface DataStructureFactory<L extends ILits>