org.sat4j.minisat.constraints
Class AbstractDataStructureFactory

java.lang.Object
  extended by org.sat4j.minisat.constraints.AbstractDataStructureFactory
All Implemented Interfaces:
Serializable, DataStructureFactory
Direct Known Subclasses:
AbstractCardinalityDataStructure, 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


Copyright © 2012 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.