public abstract class WatchPbLongCP extends Object implements IWatchPb, Propagatable, Undoable, Serializable
Modifier and Type | Field and Description |
---|---|
protected double |
activity
constraint activity
|
protected BigInteger[] |
bigCoefs
coefficients of the literals of the constraint
|
protected BigInteger |
bigDegree
degree of the pseudo-boolean constraint
|
protected long[] |
coefs
coefficients of the literals of the constraint
|
protected long |
degree
degree of the pseudo-boolean constraint
|
protected boolean |
learnt
true if the constraint is a learned constraint
|
protected int[] |
lits
literals of the constraint
|
protected long |
sumcoefs |
protected ILits |
voc
constraint's vocabulary
|
Modifier and Type | Method and Description |
---|---|
void |
assertConstraint(UnitPropagationListener s)
Method called when the constraint is to be asserted.
|
void |
assertConstraintIfNeeded(UnitPropagationListener s)
Method called when the constraint is added to the solver "on the fly".
|
void |
calcReason(int p,
IVecInt outReason)
compute the reason for the assignment of a literal
|
void |
calcReasonOnTheFly(int p,
IVecInt trail,
IVecInt outReason)
Compute the reason for a given assignment in a the constraint created on
the fly in the solver.
|
boolean |
canBePropagatedMultipleTimes()
Partition constraints into the ones that can only be found once on the
trail (e.g. clauses) and the ones that can be found several times (e.g.
|
boolean |
coefficientsEqualToOne() |
IVecInt |
computeAnImpliedClause()
compute an implied clause on the literals with the greater coefficients.
|
long |
computeLeftSide()
compute the sum of the coefficients of the satisfied or non-assigned
literals of the current constraint (usually called poss)
|
BigInteger |
computeLeftSide(BigInteger[] theCoefs)
compute the sum of the coefficients of the satisfied or non-assigned
literals of a described constraint (usually called poss)
|
long |
computeLeftSide(long[] theCoefs)
compute the sum of the coefficients of the satisfied or non-assigned
literals of a described constraint (usually called poss)
|
protected abstract void |
computePropagation(UnitPropagationListener s) |
protected abstract void |
computeWatches() |
boolean |
equals(Object pb) |
void |
forwardActivity(double claInc) |
int |
get(int i)
to obtain the i-th literal of the constraint
|
double |
getActivity()
to obtain the activity value of the constraint
|
BigInteger |
getCoef(int i)
to obtain the coefficient of the i-th literal of the constraint
|
BigInteger[] |
getCoefs()
to obtain the coefficients of the constraint.
|
BigInteger |
getDegree() |
int[] |
getLits()
to obtain the literals of the constraint.
|
long[] |
getLongCoefs() |
ILits |
getVocabulary() |
int |
hashCode() |
void |
incActivity(double claInc)
increase activity value of the constraint
|
boolean |
isAssertive(int dl)
This predicate tests wether the constraint is assertive at decision level
dl
|
protected boolean |
isSatisfiable()
tests if the constraint is still satisfiable.
|
boolean |
learnt()
is the constraint a learnt constraint ?
|
boolean |
locked()
The constraint is the reason of a unit propagation.
|
protected static BigInteger |
ppcm(BigInteger a,
BigInteger b)
ppcm : least common multiple for two integers (plus petit commun
multiple)
|
void |
register()
Register the constraint to the solver.
|
void |
rescaleBy(double d)
to re-scale the activity of the constraint
|
void |
setActivity(double d)
Set the activity at a specific value
|
void |
setLearnt()
the constraint is learnt
|
boolean |
simplify()
simplify the constraint (if it is satisfied)
|
int |
size() |
long |
slackConstraint()
compute the slack of the current constraint slack = poss - degree of the
constraint
|
BigInteger |
slackConstraint(BigInteger[] theCoefs,
BigInteger theDegree) |
long |
slackConstraint(long[] theCoefs,
long theDegree)
compute the slack of a described constraint slack = poss - degree of the
constraint
|
protected void |
sort()
sort coefficient and literal arrays
|
protected void |
sort(int from,
int to)
sort partially coefficient and literal arrays
|
Constr |
toConstraint()
Allow to access a constraint view of the propagatable to avoid casting.
|
static long[] |
toLong(BigInteger[] bigValues) |
String |
toString() |
clone, finalize, getClass, notify, notifyAll, wait, wait, wait
propagate
protected double activity
protected BigInteger[] bigCoefs
protected BigInteger bigDegree
protected long[] coefs
protected long sumcoefs
protected long degree
protected int[] lits
protected boolean learnt
protected ILits voc
public static long[] toLong(BigInteger[] bigValues)
public boolean isAssertive(int dl)
dl
- public void calcReason(int p, IVecInt outReason)
calcReason
in interface Constr
p
- a falsified literal (or Lit.UNDEFINED)outReason
- list of falsified literals for which the negation is the
reason of the assignmentConstr.calcReason(int, IVecInt)
protected abstract void computeWatches() throws ContradictionException
ContradictionException
protected abstract void computePropagation(UnitPropagationListener s) throws ContradictionException
ContradictionException
public int get(int i)
public double getActivity()
getActivity
in interface IConstr
IConstr.getActivity()
public void incActivity(double claInc)
incActivity
in interface Constr
claInc
- the value to increase the activity withConstr.incActivity(double)
public void setActivity(double d)
Constr
setActivity
in interface Constr
d
- the new activitypublic long slackConstraint()
public long slackConstraint(long[] theCoefs, long theDegree)
theCoefs
- coefficients of the constrainttheDegree
- degree of the constraintpublic long computeLeftSide(long[] theCoefs)
coefs
- coefficients of the constraintpublic BigInteger computeLeftSide(BigInteger[] theCoefs)
coefs
- coefficients of the constraintpublic long computeLeftSide()
protected boolean isSatisfiable()
public boolean learnt()
learnt
in interface IConstr
IConstr.learnt()
public boolean locked()
protected static BigInteger ppcm(BigInteger a, BigInteger b)
a
- one integerb
- the other integerpublic void rescaleBy(double d)
public void setLearnt()
public boolean simplify()
public final int size()
protected final void sort()
protected final void sort(int from, int to)
from
- index for the beginning of the sortto
- index for the end of the sortpublic void assertConstraint(UnitPropagationListener s)
Constr
assertConstraint
in interface Constr
s
- a UnitPropagationListener to use for unit propagation.public void assertConstraintIfNeeded(UnitPropagationListener s)
Constr
Constr.assertConstraint(UnitPropagationListener)
method.assertConstraintIfNeeded
in interface Constr
s
- a UnitPropagationListener to use for unit propagation.public void register()
Constr
public int[] getLits()
public ILits getVocabulary()
getVocabulary
in interface PBConstr
public IVecInt computeAnImpliedClause()
computeAnImpliedClause
in interface PBConstr
public boolean coefficientsEqualToOne()
public void forwardActivity(double claInc)
forwardActivity
in interface Constr
public long[] getLongCoefs()
public BigInteger slackConstraint(BigInteger[] theCoefs, BigInteger theDegree)
slackConstraint
in interface IWatchPb
public BigInteger getCoef(int i)
public BigInteger[] getCoefs()
public BigInteger getDegree()
public boolean canBePropagatedMultipleTimes()
IConstr
canBePropagatedMultipleTimes
in interface IConstr
public Constr toConstraint()
Propagatable
toConstraint
in interface Propagatable
public void calcReasonOnTheFly(int p, IVecInt trail, IVecInt outReason)
Constr
Constr.calcReason(int, IVecInt)
, the falsification may not have been
detected as soon as possible. As such, it is necessary to take into
account the order of the literals in the trail.calcReasonOnTheFly
in interface Constr
p
- a satisfied literal (or Lit.UNDEFINED)trail
- all the literals satisfied in the solvers, should not be
modified.outReason
- a list of falsified literals whose negation is the reason of
the assignment of p to true.Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.