org.sat4j.minisat.constraints.pb
Class MinWatchPb
java.lang.Object
org.sat4j.minisat.constraints.pb.WatchPb
org.sat4j.minisat.constraints.pb.MinWatchPb
- All Implemented Interfaces:
- java.io.Serializable, Constr, Propagatable, Undoable, IConstr
public class MinWatchPb
- extends WatchPb
- implements java.io.Serializable
- See Also:
- Serialized Form
Method Summary |
static MinWatchPb |
minWatchPbNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
static MinWatchPb |
minWatchPbNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
IVecInt coefs,
boolean moreThan,
int degree)
|
boolean |
propagate(UnitPropagationListener s,
int p)
Propagation de la valeur de v??? |
void |
remove()
Enl??? |
void |
undo(int p)
M??? |
static WatchPb |
watchPbNew(ILits voc,
IVecInt lits,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
|
static WatchPb |
watchPbNew(ILits voc,
IVecInt lits,
IVecInt coefs,
boolean moreThan,
int degree)
|
Methods inherited from class org.sat4j.minisat.constraints.pb.WatchPb |
assertConstraint, calcReason, get, getActivity, getBacktrackLevel, getCoef, getDegree, incActivity, isAssertive, learnt, locked, recalcLeftSide, recalcLeftSide, register, rescaleBy, setLearnt, simplify, size, slackConstraint, slackConstraint, toString |
Methods inherited from class java.lang.Object |
equals, getClass, hashCode, notify, notifyAll, wait, wait, wait |
minWatchPbNew
public static MinWatchPb minWatchPbNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
IVecInt coefs,
boolean moreThan,
int degree)
throws ContradictionException
- Parameters:
s
- outil pour la propagation des litt???rauxps
- liste des litt???raux de la nouvelle contraintecoefs
- liste des coefficients des litt???raux de la contraintemoreThan
- d???termine si c'est une sup???rieure ou ???gal ??? l'originedegree
- fournit le degr??? de la contrainte
- Returns:
- une nouvelle clause si tout va bien, ou null si un conflit est
d???tect???
- Throws:
ContradictionException
minWatchPbNew
public static MinWatchPb minWatchPbNew(UnitPropagationListener s,
ILits voc,
IVecInt ps,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)
throws ContradictionException
- Parameters:
s
- outil pour la propagation des litt???rauxps
- liste des litt???raux de la nouvelle contraintecoefs
- liste des coefficients des litt???raux de la contraintemoreThan
- d???termine si c'est une sup???rieure ou ???gal ??? l'originedegree
- fournit le degr??? de la contrainte
- Returns:
- une nouvelle clause si tout va bien, ou null si un conflit est
d???tect???
- Throws:
ContradictionException
propagate
public boolean propagate(UnitPropagationListener s,
int p)
- Propagation de la valeur de v???rit??? d'un litt???ral falsifi???
- Specified by:
propagate
in interface Propagatable
- Parameters:
s
- un prouveurp
- le litt???ral propag??? (il doit etre falsifie)
- Returns:
- false ssi une inconsistance est d???t???ct???e
remove
public void remove()
- Enl???ve une contrainte du prouveur
- Specified by:
remove
in interface Constr
undo
public void undo(int p)
- M???thode appel???e lors du backtrack
- Specified by:
undo
in interface Undoable
- Parameters:
p
- un litt???ral d???saffect???
watchPbNew
public static WatchPb watchPbNew(ILits voc,
IVecInt lits,
IVecInt coefs,
boolean moreThan,
int degree)
watchPbNew
public static WatchPb watchPbNew(ILits voc,
IVecInt lits,
IVec<java.math.BigInteger> coefs,
boolean moreThan,
java.math.BigInteger degree)