org.sat4j.minisat.core
Interface ILits

All Known Subinterfaces:

ILits2, ILits23, IMarkableLits

All Known Implementing Classes:

Lits, Lits2, Lits23, MarkableLits

public interface ILits

Author:

leberre To change the template for this generated type comment go to Window - Preferences - Java - Code Generation - Code and Comments

Field Summary

static int

UNDEFINED

Method Summary

boolean	belongsToPool(int x) Returns true iff the variable is used in the set of constraints.
void	ensurePool(int howmany)
int	getFromPool(int x) Translates a Dimacs literal into an internal representation literal.
int	getLevel(int lit)
Constr	getReason(int lit)
void	init(int nvar)
boolean	isFalsified(int lit)
boolean	isImplied(int lit)
boolean	isSatisfied(int lit)
boolean	isUnassigned(int lit)
int	not(int lit)
int	nVars() to obtain the max id of the variable
int	realnVars() to obtain the real number of variables appearing in the formula
void	reset(int lit)
void	resetPool()
void	satisfies(int lit)
void	setLevel(int lit, int l)
void	setReason(int lit, Constr r)
void	unassign(int lit)
IVec<Undoable>	undos(int lit)
java.lang.String	valueToString(int lit)
void	watch(int lit, Propagatable c)
IVec<Propagatable>	watches(int lit)

Field Detail

UNDEFINED

static final int UNDEFINED

See Also:

Constant Field Values

Method Detail

init

void init(int nvar)

getFromPool

int getFromPool(int x)

Translates a Dimacs literal into an internal representation literal.

Parameters:

x - the Dimacs literal (a non null integer).

Returns:

the literal in the internal representation.

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)