org.sat4j.pb.constraints
Class AbstractPBClauseCardConstrDataStructure

java.lang.Object
  org.sat4j.minisat.constraints.AbstractDataStructureFactory
      org.sat4j.pb.constraints.AbstractPBDataStructureFactory
          org.sat4j.pb.constraints.AbstractPBClauseCardConstrDataStructure

All Implemented Interfaces:

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, BigInteger[] coefs, 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, BigInteger[] coefs, 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,
                                   BigInteger[] coefs,
                                   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,
                                      BigInteger[] coefs,
                                      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)