public final class MaxWatchPbLong extends WatchPbLong
Modifier and Type | Method and Description |
---|---|
protected void |
computePropagation(UnitPropagationListener s) |
protected void |
computeWatches()
All the literals are watched.
|
static MaxWatchPbLong |
normalizedMaxWatchPbNew(UnitPropagationListener s,
ILits voc,
int[] lits,
BigInteger[] coefs,
BigInteger degree,
BigInteger sumCoefs)
build a pseudo boolean constraint.
|
static WatchPbLong |
normalizedWatchPbNew(ILits voc,
IDataStructurePB mpb)
build a pseudo boolean constraint from a specific data structure.
|
boolean |
propagate(UnitPropagationListener s,
int p)
Propagation of a falsified literal
|
void |
remove(UnitPropagationListener upl)
Remove a constraint from the solver
|
void |
undo(int p)
this method is called during backtrack
|
assertConstraint, assertConstraintIfNeeded, calcReason, calcReasonOnTheFly, canBePropagatedMultipleTimes, coefficientsEqualToOne, computeAnImpliedClause, computeLeftSide, computeLeftSide, equals, forwardActivity, get, getActivity, getLits, getVocabulary, hashCode, incActivity, isAssertive, isSatisfiable, learnt, locked, ppcm, register, rescaleBy, setActivity, setLearnt, simplify, size, slackConstraint, slackConstraint, sort, sort, toConstraint, toLong, toString
protected void computeWatches() throws ContradictionException
computeWatches
in class WatchPbLong
ContradictionException
WatchPbLong.computeWatches()
protected void computePropagation(UnitPropagationListener s) throws ContradictionException
computePropagation
in class WatchPbLong
ContradictionException
public boolean propagate(UnitPropagationListener s, int p)
propagate
in interface Propagatable
propagate
in class WatchPbLong
s
- the solverp
- the propagated literal (it must be falsified)public void remove(UnitPropagationListener upl)
remove
in interface Constr
remove
in class WatchPbLong
public void undo(int p)
undo
in interface Undoable
undo
in class WatchPbLong
p
- an unassigned literalpublic static MaxWatchPbLong normalizedMaxWatchPbNew(UnitPropagationListener s, ILits voc, int[] lits, BigInteger[] coefs, BigInteger degree, BigInteger sumCoefs) throws ContradictionException
s
- a unit propagation listener (usually the solver)voc
- the vocabularylits
- the literals of the constraintcoefs
- the coefficients of the constraintdegree
- the degree of the constraintContradictionException
public static WatchPbLong normalizedWatchPbNew(ILits voc, IDataStructurePB mpb)
s
- a unit propagation listener (usually the solver)mpb
- data structure which contains literals of the constraint,
coefficients (a0, a1, ... an), and the degree of the
constraint (k). The constraint is a "more than" constraint.Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.