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:
Serializable, DataStructureFactory, PBDataStructureFactory
Direct Known Subclasses:
CompetMinHTmixedClauseCardConstrDataStructureFactory, CompetResolutionMinPBLongMixedWLClauseCardConstrDataStructure, CompetResolutionPBLongMixedHTClauseCardConstrDataStructure, CompetResolutionPBLongMixedWLClauseCardConstrDataStructure, CompetResolutionPBMixedHTClauseCardConstrDataStructure, CompetResolutionPBMixedWLClauseCardConstrDataStructure, PBLongMaxClauseCardConstrDataStructure, PBLongMinClauseCardConstrDataStructure, PBMaxClauseAtLeastConstrDataStructure, PBMaxClauseCardConstrDataStructure, PBMinClauseCardConstrDataStructure, PuebloPBMinClauseAtLeastConstrDataStructure, 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
 
Method Summary
protected  Constr constraintFactory(int[] literals, BigInteger[] coefs, BigInteger degree)
           
protected  Constr constructCard(IVecInt theLits, int degree)
           
protected  Constr constructClause(IVecInt v)
           
protected  Constr constructLearntCard(IDataStructurePB dspb)
           
protected  Constr constructLearntClause(IVecInt literals)
           
protected  Constr constructLearntPB(IDataStructurePB dspb)
           
protected  Constr constructPB(int[] theLits, BigInteger[] coefs, BigInteger degree)
           
 Constr createClause(IVecInt literals)
           
 Constr createUnregisteredClause(IVecInt literals)
           
protected  Constr learntConstraintFactory(IDataStructurePB dspb)
           
static BigInteger sumOfCoefficients(BigInteger[] coefs)
           
 
Methods inherited from class org.sat4j.pb.constraints.AbstractPBDataStructureFactory
createAtLeastPBConstraint, createAtMostPBConstraint, createCardinalityConstraint, createLits, createPseudoBooleanConstraint, 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
 

Method Detail

createClause

public Constr createClause(IVecInt literals)
                    throws ContradictionException
Specified by:
createClause in interface DataStructureFactory
Overrides:
createClause in class AbstractPBDataStructureFactory
Throws:
ContradictionException

createUnregisteredClause

public Constr createUnregisteredClause(IVecInt literals)
Specified by:
createUnregisteredClause in interface DataStructureFactory
Overrides:
createUnregisteredClause in class AbstractPBDataStructureFactory

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 Constr constructClause(IVecInt v)

constructCard

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

constructPB

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

constructLearntClause

protected Constr constructLearntClause(IVecInt literals)

constructLearntCard

protected Constr constructLearntCard(IDataStructurePB dspb)

constructLearntPB

protected Constr constructLearntPB(IDataStructurePB dspb)

sumOfCoefficients

public static final BigInteger sumOfCoefficients(BigInteger[] coefs)


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