org.sat4j.minisat.core
Interface IMarkableLits

All Superinterfaces:

ILits

All Known Implementing Classes:

MarkableLits

public interface IMarkableLits
extends ILits

Vocabulary in which literals can be marked.

Author:

daniel

Field Summary

static int

MARKLESS

Fields inherited from interface org.sat4j.minisat.core.ILits

UNDEFINED

Method Summary

int	getMark(int p) To get the mark for a given literal.
IVecInt	getMarkedLiterals() Returns the set of all marked literals.
IVecInt	getMarkedLiterals(int mark) Returns that set of all the literals having a specific mark.
IVecInt	getMarkedVariables() Returns the set of all marked variables.
IVecInt	getMarkedVariables(int mark) Returns the set of all variables having a specific mark.
java.util.Set<java.lang.Integer>	getMarks()
boolean	isMarked(int p) To know if a given literal is marked, i.e. has a mark different from MARKLESS.
void	resetAllMarks() Set all the literal marks to MARKLESS
void	resetMark(int p) Set the mark of a given literal to MARKLESS.
void	setMark(int p) Mark a given literal.
void	setMark(int p, int mark) Mark a given literal with a given mark.

Methods inherited from interface org.sat4j.minisat.core.ILits

attach, attaches, belongsToPool, ensurePool, getFromPool, getLevel, getReason, init, isFalsified, isImplied, isSatisfied, isUnassigned, not, nVars, realnVars, reset, resetPool, satisfies, setLevel, setReason, unassign, undos, valueToString

Field Detail

MARKLESS

static final int MARKLESS

See Also:

Constant Field Values

Method Detail

setMark

void setMark(int p,
             int mark)

Mark a given literal with a given mark.

Parameters:

p - the literal

mark - an integer used to mark the literal. The specific mark MARKLESS is used to denote that the literal is not marked. The marks are supposed to be positive in the most common cases.

setMark

void setMark(int p)

Mark a given literal.

Parameters:

p - a literal

getMark

int getMark(int p)

To get the mark for a given literal.

Parameters:

p - a literal

Returns:

the mark associated with that literal, or MARKLESS if the literal is not marked.

isMarked

boolean isMarked(int p)

To know if a given literal is marked, i.e. has a mark different from MARKLESS.

Parameters:

p - a literal

Returns:

true iif the literal is marked.

resetMark

void resetMark(int p)

Set the mark of a given literal to MARKLESS.

Parameters:

p - a literal

resetAllMarks

void resetAllMarks()

Set all the literal marks to MARKLESS

getMarkedLiterals

IVecInt getMarkedLiterals()

Returns the set of all marked literals.

Returns:

a set of literals whose mark is different from MARKLESS.

getMarkedLiterals

IVecInt getMarkedLiterals(int mark)

Returns that set of all the literals having a specific mark.

Parameters:

mark - a mark

Returns:

a set of literals whose mark is mark

getMarkedVariables

IVecInt getMarkedVariables()

Returns the set of all marked variables. A variable is marked iff at least one of its literal is marked.

Returns:

a set of variables whose mark is different from MARKLESS.

getMarkedVariables

IVecInt getMarkedVariables(int mark)

Returns the set of all variables having a specific mark. A variable is marked iff at least one of its literal is marked.

Parameters:

mark - a mark.

Returns:

a set of variables whose mark is mark.

getMarks

java.util.Set<java.lang.Integer> getMarks()

Returns:

a list of marks used to mark the literals.