org.sat4j.minisat.constraints
Class AbstractPBClauseCardConstrDataStructure

java.lang.Object
  org.sat4j.minisat.constraints.AbstractDataStructureFactory<ILits>
      org.sat4j.minisat.constraints.AbstractPBDataStructureFactory
          org.sat4j.minisat.constraints.AbstractPBClauseCardConstrDataStructure

All Implemented Interfaces:

java.io.Serializable, IInternalPBConstraintCreator, DataStructureFactory<ILits>

Direct Known Subclasses:

PuebloPBMinClauseCardConstrDataStructure

public abstract class AbstractPBClauseCardConstrDataStructure
extends AbstractPBDataStructureFactory

See Also:

Serialized Form

Field Summary

Fields inherited from class org.sat4j.minisat.constraints.AbstractDataStructureFactory

learner, lits, solver

Constructor Summary

AbstractPBClauseCardConstrDataStructure()

Method Summary

protected PBConstr	constraintFactory(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
protected PBConstr	constraintFactory(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
protected PBConstr	constraintFactory(IVecInt literals, IVecInt coefs, boolean moreThan, int degree)
protected PBConstr	constraintFactory(IVecInt literals, IVecInt coefs, int degree)
protected abstract PBConstr	constructCard(IVecInt lits, int degree)
protected abstract PBConstr	constructClause(IVecInt v)
protected abstract PBConstr	constructLearntCard(IVecInt literals, int degree)
protected abstract PBConstr	constructLearntClause(IVecInt literals)
protected abstract PBConstr	constructLearntPB(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
protected abstract PBConstr	constructPB(IDataStructurePB mpb)
protected abstract PBConstr	constructPB(int[] lits, java.math.BigInteger[] coefs, java.math.BigInteger degree)

Methods inherited from class org.sat4j.minisat.constraints.AbstractPBDataStructureFactory

createCardinalityConstraint, createClause, createLits, createPseudoBooleanConstraint, createUnregisteredClause, createUnregisteredPseudoBooleanConstraint, createUnregisteredPseudoBooleanConstraint

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

Constructor Detail

AbstractPBClauseCardConstrDataStructure

public AbstractPBClauseCardConstrDataStructure()

Method Detail

constraintFactory

protected PBConstr constraintFactory(IVecInt literals,
                                     IVecInt coefs,
                                     boolean moreThan,
                                     int degree)
                              throws ContradictionException

Specified by:

constraintFactory in class AbstractPBDataStructureFactory

Parameters:

literals - the literals

coefs - the coefficients

degree - the degree of the constraint

Returns:

a new PB constraint

Throws:

ContradictionException

constraintFactory

protected PBConstr constraintFactory(IVecInt literals,
                                     IVecInt coefs,
                                     int degree)

Specified by:

constraintFactory in class AbstractPBDataStructureFactory

Returns:

a new PB constraint

constraintFactory

protected PBConstr constraintFactory(IVecInt literals,
                                     IVec<java.math.BigInteger> coefs,
                                     boolean moreThan,
                                     java.math.BigInteger degree)
                              throws ContradictionException

Specified by:

constraintFactory in class AbstractPBDataStructureFactory

Throws:

ContradictionException

constraintFactory

protected PBConstr constraintFactory(IVecInt literals,
                                     IVec<java.math.BigInteger> coefs,
                                     java.math.BigInteger degree)

Specified by:

constraintFactory in class AbstractPBDataStructureFactory

constructClause

protected abstract PBConstr constructClause(IVecInt v)

constructCard

protected abstract PBConstr constructCard(IVecInt lits,
                                          int degree)
                                   throws ContradictionException

Throws:

ContradictionException

constructPB

protected abstract PBConstr constructPB(IDataStructurePB mpb)
                                 throws ContradictionException

Throws:

ContradictionException

constructPB

protected abstract PBConstr constructPB(int[] lits,
                                        java.math.BigInteger[] coefs,
                                        java.math.BigInteger degree)
                                 throws ContradictionException

Throws:

ContradictionException

constructLearntClause

protected abstract PBConstr constructLearntClause(IVecInt literals)

constructLearntCard

protected abstract PBConstr constructLearntCard(IVecInt literals,
                                                int degree)

constructLearntPB

protected abstract PBConstr constructLearntPB(IVecInt literals,
                                              IVec<java.math.BigInteger> coefs,
                                              java.math.BigInteger degree)