org.sat4j.minisat.constraints
Class AbstractPBDataStructureFactory

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

All Implemented Interfaces:

java.io.Serializable, IInternalPBConstraintCreator, DataStructureFactory

Direct Known Subclasses:

PBMaxDataStructure, PBMinDataStructure

public abstract class AbstractPBDataStructureFactory
extends AbstractDataStructureFactory
implements IInternalPBConstraintCreator

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

Constructor Summary

AbstractPBDataStructureFactory()

Method Summary

Constr	createCardinalityConstraint(IVecInt literals, int degree)
Constr	createClause(IVecInt literals)
Constr	createPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
Constr	createUnregisteredClause(IVecInt literals)
Constr	createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, java.math.BigInteger degree)
IConstr	createUnregisteredPseudoBooleanConstraint(IVecInt literals, IVec<java.math.BigInteger> coefs, boolean moreThan, java.math.BigInteger degree)
void	reset()

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

conflictDetectedInWatchesFor, getVocabulary, getWatchesFor, learnConstraint, setLearner, setUnitPropagationListener

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

AbstractPBDataStructureFactory

public AbstractPBDataStructureFactory()

Method Detail

createClause

public Constr createClause(IVecInt literals)
                    throws ContradictionException

Specified by:

createClause in interface DataStructureFactory

Parameters:

literals - a set of literals using Dimacs format (signed non null integers).

Returns:

null if the constraint is a tautology.

Throws:

ContradictionException - the constraint is trivially unsatisfiable.

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<java.math.BigInteger> coefs,
                                            boolean moreThan,
                                            java.math.BigInteger degree)
                                     throws ContradictionException

Specified by:

createPseudoBooleanConstraint in interface DataStructureFactory

Overrides:

createPseudoBooleanConstraint in class AbstractDataStructureFactory

Throws:

ContradictionException

reset

public void reset()

Specified by:

reset in interface DataStructureFactory

Overrides:

reset in class AbstractDataStructureFactory

createUnregisteredPseudoBooleanConstraint

public Constr createUnregisteredPseudoBooleanConstraint(IVecInt literals,
                                                        IVec<java.math.BigInteger> coefs,
                                                        java.math.BigInteger degree)

Specified by:

createUnregisteredPseudoBooleanConstraint in interface IInternalPBConstraintCreator

Specified by:

createUnregisteredPseudoBooleanConstraint in interface DataStructureFactory

Overrides:

createUnregisteredPseudoBooleanConstraint in class AbstractDataStructureFactory

createUnregisteredPseudoBooleanConstraint

public IConstr createUnregisteredPseudoBooleanConstraint(IVecInt literals,
                                                         IVec<java.math.BigInteger> coefs,
                                                         boolean moreThan,
                                                         java.math.BigInteger degree)
                                                  throws ContradictionException

Throws:

ContradictionException