org.sat4j.minisat.constraints
Class AbstractPBClauseCardConstrDataStructure

java.lang.Object
  extended by org.sat4j.minisat.constraints.AbstractDataStructureFactory<ILits>
      extended by org.sat4j.minisat.constraints.AbstractPBDataStructureFactory
          extended by 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)


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