org.sat4j.minisat.constraints
Class AbstractDataStructureFactory

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

All Implemented Interfaces:

java.io.Serializable, DataStructureFactory

Direct Known Subclasses:

AbstractCardinalityDataStructure, AbstractPBDataStructureFactory, ClausalDataStructureCB, ClausalDataStructureCBWL, ClausalDataStructureWL

public abstract class AbstractDataStructureFactory
extends java.lang.Object
implements DataStructureFactory, 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

Constructor Summary

AbstractDataStructureFactory()

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)
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

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

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

createClause, createUnregisteredClause

Constructor Detail

AbstractDataStructureFactory

public 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.

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

Specified by:

createCardinalityConstraint in interface DataStructureFactory

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

Throws:

ContradictionException

createUnregisteredPseudoBooleanConstraint

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

Specified by:

createUnregisteredPseudoBooleanConstraint in interface DataStructureFactory