org.sat4j.pb.constraints
Class AbstractPBDataStructureFactory

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

All Implemented Interfaces:

Serializable, DataStructureFactory, PBDataStructureFactory

Direct Known Subclasses:

AbstractPBClauseCardConstrDataStructure, PBMaxDataStructure, PBMinDataStructure, PuebloPBMinDataStructure

public abstract class AbstractPBDataStructureFactory
extends AbstractDataStructureFactory
implements PBDataStructureFactory

Author:

leberre To change the template for this generated type comment go to Window>Preferences>Java>Code Generation>Code and Comments

See Also:

Serialized Form

Field Summary

static org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer	FOR_COMPETITION
static org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer	NO_COMPETITION

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

learner, lits, solver

Constructor Summary

AbstractPBDataStructureFactory()

Method Summary

protected abstract Constr	constraintFactory(int[] literals, BigInteger[] coefs, BigInteger degree)
Constr	createAtLeastPBConstraint(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
Constr	createAtMostPBConstraint(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
Constr	createCardinalityConstraint(IVecInt literals, int degree)
Constr	createClause(IVecInt literals)
protected ILits	createLits()
Constr	createPseudoBooleanConstraint(IVecInt literals, IVec<BigInteger> coefs, boolean moreThan, BigInteger degree)
Constr	createUnregisteredClause(IVecInt literals)
Constr	createUnregisteredPseudoBooleanConstraint(IDataStructurePB dspb)
protected org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer	getNormalizer()
protected abstract Constr	learntConstraintFactory(IDataStructurePB dspb)
void	setNormalizer(org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer normalizer)
void	setNormalizer(String simp)

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

Field Detail

FOR_COMPETITION

public static final org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer FOR_COMPETITION

NO_COMPETITION

public static final org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer NO_COMPETITION

Constructor Detail

AbstractPBDataStructureFactory

public AbstractPBDataStructureFactory()

Method Detail

getNormalizer

protected org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer getNormalizer()

setNormalizer

public void setNormalizer(String simp)

setNormalizer

public void setNormalizer(org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer normalizer)

createClause

public Constr createClause(IVecInt literals)
                    throws ContradictionException

Specified by:

createClause in interface DataStructureFactory

Throws:

ContradictionException

createUnregisteredClause

public Constr createUnregisteredClause(IVecInt literals)

Specified by:

createUnregisteredClause in interface DataStructureFactory

createCardinalityConstraint

public Constr createCardinalityConstraint(IVecInt literals,
                                          int degree)
                                   throws ContradictionException

Specified by:

createCardinalityConstraint in interface DataStructureFactory

Overrides:

createCardinalityConstraint in class AbstractDataStructureFactory

Throws:

ContradictionException

createPseudoBooleanConstraint

public Constr createPseudoBooleanConstraint(IVecInt literals,
                                            IVec<BigInteger> coefs,
                                            boolean moreThan,
                                            BigInteger degree)
                                     throws ContradictionException

Specified by:

createPseudoBooleanConstraint in interface PBDataStructureFactory

Throws:

ContradictionException

createAtMostPBConstraint

public Constr createAtMostPBConstraint(IVecInt literals,
                                       IVec<BigInteger> coefs,
                                       BigInteger degree)
                                throws ContradictionException

Specified by:

createAtMostPBConstraint in interface PBDataStructureFactory

Throws:

ContradictionException

createAtLeastPBConstraint

public Constr createAtLeastPBConstraint(IVecInt literals,
                                        IVec<BigInteger> coefs,
                                        BigInteger degree)
                                 throws ContradictionException

Specified by:

createAtLeastPBConstraint in interface PBDataStructureFactory

Throws:

ContradictionException

createUnregisteredPseudoBooleanConstraint

public Constr createUnregisteredPseudoBooleanConstraint(IDataStructurePB dspb)

Specified by:

createUnregisteredPseudoBooleanConstraint in interface PBDataStructureFactory

constraintFactory

protected abstract Constr constraintFactory(int[] literals,
                                            BigInteger[] coefs,
                                            BigInteger degree)
                                     throws ContradictionException

Throws:

ContradictionException

learntConstraintFactory

protected abstract Constr learntConstraintFactory(IDataStructurePB dspb)

createLits

protected ILits createLits()

Specified by:

createLits in class AbstractDataStructureFactory