public abstract class AbstractPBDataStructureFactory extends AbstractDataStructureFactory implements PBDataStructureFactory
Modifier and Type | Field and Description |
---|---|
static org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer |
FOR_COMPETITION |
static org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer |
NO_COMPETITION |
learner, lits, solver
Constructor and Description |
---|
AbstractPBDataStructureFactory() |
conflictDetectedInWatchesFor, getVocabulary, getWatchesFor, learnConstraint, reset, setLearner, setUnitPropagationListener
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
conflictDetectedInWatchesFor, getVocabulary, getWatchesFor, learnConstraint, reset, setLearner, setUnitPropagationListener
public static final org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer FOR_COMPETITION
public static final org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer NO_COMPETITION
protected org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer getNormalizer()
public void setNormalizer(String simp)
public void setNormalizer(org.sat4j.pb.constraints.AbstractPBDataStructureFactory.INormalizer normalizer)
public Constr createClause(IVecInt literals) throws ContradictionException
createClause
in interface DataStructureFactory
literals
- a set of literals using Dimacs format (signed non null
integers).ContradictionException
- the constraint is trivially unsatisfiable.public Constr createUnregisteredClause(IVecInt literals)
createUnregisteredClause
in interface DataStructureFactory
public Constr createCardinalityConstraint(IVecInt literals, int degree) throws ContradictionException
DataStructureFactory
createCardinalityConstraint
in interface DataStructureFactory
createCardinalityConstraint
in class AbstractDataStructureFactory
literals
- a set of literals.degree
- the degree of the cardinality constraint.ContradictionException
public Constr createPseudoBooleanConstraint(IVecInt literals, IVec<BigInteger> coefs, boolean moreThan, BigInteger degree) throws ContradictionException
createPseudoBooleanConstraint
in interface PBDataStructureFactory
ContradictionException
public Constr createAtMostPBConstraint(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree) throws ContradictionException
createAtMostPBConstraint
in interface PBDataStructureFactory
ContradictionException
public Constr createAtLeastPBConstraint(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree) throws ContradictionException
createAtLeastPBConstraint
in interface PBDataStructureFactory
ContradictionException
public Constr createUnregisteredPseudoBooleanConstraint(IDataStructurePB dspb)
createUnregisteredPseudoBooleanConstraint
in interface PBDataStructureFactory
public Constr createUnregisteredAtLeastConstraint(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
createUnregisteredAtLeastConstraint
in interface PBDataStructureFactory
public Constr createUnregisteredAtMostConstraint(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
createUnregisteredAtMostConstraint
in interface PBDataStructureFactory
protected abstract Constr constraintFactory(int[] literals, BigInteger[] coefs, BigInteger degree) throws ContradictionException
ContradictionException
protected abstract Constr learntConstraintFactory(IDataStructurePB dspb)
protected abstract Constr learntAtLeastConstraintFactory(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
protected abstract Constr learntAtMostConstraintFactory(IVecInt literals, IVec<BigInteger> coefs, BigInteger degree)
protected ILits createLits()
createLits
in class AbstractDataStructureFactory
public Constr createUnregisteredCardinalityConstraint(IVecInt literals, int degree)
createUnregisteredCardinalityConstraint
in interface DataStructureFactory
createUnregisteredCardinalityConstraint
in class AbstractDataStructureFactory
Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.