org.sat4j.pb.constraints
Class AbstractPBClauseCardConstrDataStructure

java.lang.Object
  extended by org.sat4j.minisat.constraints.AbstractDataStructureFactory
      extended by org.sat4j.pb.constraints.AbstractPBDataStructureFactory
          extended by org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure
All Implemented Interfaces:
java.io.Serializable, DataStructureFactory, PBDataStructureFactory
Direct Known Subclasses:
PuebloPBMinClauseCardConstrDataStructure

public abstract class AbstractPBClauseCardConstrDataStructure
extends AbstractPBDataStructureFactory

See Also:
Serialized Form

Field Summary
 
Fields inherited from class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
FOR_COMPETITION, NO_COMPETITION
 
Fields inherited from class org.sat4j.minisat.constraints.AbstractDataStructureFactory
learner, lits, solver
 
Constructor Summary
AbstractPBClauseCardConstrDataStructure()
           
 
Method Summary
protected  Constr constraintFactory(int[] literals, java.math.BigInteger[] coefs, java.math.BigInteger degree)
           
protected abstract  Constr constructCard(IVecInt theLits, int degree)
           
protected abstract  Constr constructClause(IVecInt v)
           
protected abstract  Constr constructLearntCard(IDataStructurePB dspb)
           
protected abstract  Constr constructLearntClause(IVecInt literals)
           
protected abstract  Constr constructLearntPB(IDataStructurePB dspb)
           
protected abstract  Constr constructPB(int[] theLits, java.math.BigInteger[] coefs, java.math.BigInteger degree)
           
protected  Constr learntConstraintFactory(IDataStructurePB dspb)
           
 
Methods inherited from class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
createCardinalityConstraint, createClause, createLits, createPseudoBooleanConstraint, createUnregisteredClause, createUnregisteredPseudoBooleanConstraint, getNormalizer, setNormalizer, setNormalizer
 
Methods inherited from class org.sat4j.minisat.constraints.AbstractDataStructureFactory
conflictDetectedInWatchesFor, getVocabulary, getWatchesFor, learnConstraint, reset, setLearner, setUnitPropagationListener
 
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
conflictDetectedInWatchesFor, getVocabulary, getWatchesFor, learnConstraint, reset, setLearner, setUnitPropagationListener
 

Constructor Detail

AbstractPBClauseCardConstrDataStructure

public AbstractPBClauseCardConstrDataStructure()
Method Detail

constraintFactory

protected Constr constraintFactory(int[] literals,
                                   java.math.BigInteger[] coefs,
                                   java.math.BigInteger degree)
                            throws ContradictionException
Specified by:
constraintFactory in class AbstractPBDataStructureFactory
Throws:
ContradictionException

learntConstraintFactory

protected Constr learntConstraintFactory(IDataStructurePB dspb)
Specified by:
learntConstraintFactory in class AbstractPBDataStructureFactory

constructClause

protected abstract Constr constructClause(IVecInt v)

constructCard

protected abstract Constr constructCard(IVecInt theLits,
                                        int degree)
                                 throws ContradictionException
Throws:
ContradictionException

constructPB

protected abstract Constr constructPB(int[] theLits,
                                      java.math.BigInteger[] coefs,
                                      java.math.BigInteger degree)
                               throws ContradictionException
Throws:
ContradictionException

constructLearntClause

protected abstract Constr constructLearntClause(IVecInt literals)

constructLearntCard

protected abstract Constr constructLearntCard(IDataStructurePB dspb)

constructLearntPB

protected abstract Constr constructLearntPB(IDataStructurePB dspb)


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