org.sat4j.minisat.core
Interface ILits
- All Known Subinterfaces:
- ILits2, ILits23
- All Known Implementing Classes:
- Lits, Lits2, Lits23
public interface ILits
- Author:
- leberre To change the template for this generated type comment go to
Window - Preferences - Java - Code Generation - Code and Comments
UNDEFINED
static final int UNDEFINED
- See Also:
- Constant Field Values
init
void init(int nvar)
getFromPool
int getFromPool(int x)
belongsToPool
boolean belongsToPool(int x)
- Returns true iff the variable is used in the set of constraints.
- Parameters:
x
-
- Returns:
- true iff the variable belongs to the formula.
resetPool
void resetPool()
ensurePool
void ensurePool(int howmany)
unassign
void unassign(int lit)
satisfies
void satisfies(int lit)
isSatisfied
boolean isSatisfied(int lit)
isFalsified
boolean isFalsified(int lit)
isUnassigned
boolean isUnassigned(int lit)
isImplied
boolean isImplied(int lit)
- Parameters:
lit
-
- Returns:
- true iff the truth value of that literal is due to a unit
propagation or a decision.
nVars
int nVars()
- to obtain the max id of the variable
- Returns:
- the maximum number of variables in the formula
realnVars
int realnVars()
- to obtain the real number of variables appearing in the formula
- Returns:
- the number of variables used in the pool
not
int not(int lit)
reset
void reset(int lit)
getLevel
int getLevel(int lit)
setLevel
void setLevel(int lit,
int l)
getReason
Constr getReason(int lit)
setReason
void setReason(int lit,
Constr r)
undos
IVec<Undoable> undos(int lit)
watch
void watch(int lit,
Propagatable c)
watches
IVec<Propagatable> watches(int lit)
- Parameters:
lit
- a literal
- Returns:
- the list of all the constraints that watch the negation of lit
valueToString
java.lang.String valueToString(int lit)