|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
public interface Constr
Method Summary | |
---|---|
void |
assertConstraint(UnitPropagationListener s)
Method called when the constraint is to be asserted. |
void |
calcReason(int p,
IVecInt outReason)
Calcule la cause de l'affection d'un litt? |
double |
getActivity()
|
void |
incActivity(double claInc)
|
boolean |
locked()
Indicate wether a constraint is responsible from an assignment. |
void |
register()
Register the constraint to the solver. |
void |
remove()
Enl? |
void |
rescaleBy(double d)
Rescale the clause activity by a value. |
void |
setLearnt()
Mark a constraint as learnt. |
boolean |
simplify()
Simplifie une contrainte, par exemple en enlevant les litt? |
Methods inherited from interface org.sat4j.minisat.core.Propagatable |
---|
propagate |
Methods inherited from interface org.sat4j.specs.IConstr |
---|
get, learnt, size |
Method Detail |
---|
void remove()
boolean simplify()
void calcReason(int p, IVecInt outReason)
p
- un litt?ral falsifi? (ou Lit.UNDEFINED)outReason
- la liste des litt?raux falsifi?s dont la n?gation correspond ?
la raison de l'affectation.void incActivity(double claInc)
claInc
- the value to increase the activity withdouble getActivity()
boolean locked()
void setLearnt()
void register()
void rescaleBy(double d)
d
- the value to rescale the clause activity with.void assertConstraint(UnitPropagationListener s)
s
- a UnitPropagationListener to use for unit propagation.
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |