org.sat4j.minisat.constraints.cnf
Class MarkableLits

java.lang.Object
  org.sat4j.minisat.constraints.cnf.Lits
      org.sat4j.minisat.constraints.cnf.MarkableLits

All Implemented Interfaces:

java.io.Serializable, ILits, IMarkableLits

public class MarkableLits
extends Lits
implements IMarkableLits

See Also:

Serialized Form

Field Summary

Fields inherited from class org.sat4j.minisat.constraints.cnf.Lits

watches

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

MARKLESS

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

UNDEFINED

Constructor Summary

MarkableLits()

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()
void	init(int nvar)
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 class org.sat4j.minisat.constraints.cnf.Lits

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

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

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

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

Constructor Detail

MarkableLits

public MarkableLits()

Method Detail

init

public void init(int nvar)

Specified by:

init in interface ILits

Overrides:

init in class Lits

setMark

public void setMark(int p,
                    int mark)

Description copied from interface: IMarkableLits

Mark a given literal with a given mark.

Specified by:

setMark in interface IMarkableLits

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

public void setMark(int p)

Description copied from interface: IMarkableLits

Mark a given literal.

Specified by:

setMark in interface IMarkableLits

Parameters:

p - a literal

getMark

public int getMark(int p)

Description copied from interface: IMarkableLits

To get the mark for a given literal.

Specified by:

getMark in interface IMarkableLits

Parameters:

p - a literal

Returns:

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

isMarked

public boolean isMarked(int p)

Description copied from interface: IMarkableLits

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

Specified by:

isMarked in interface IMarkableLits

Parameters:

p - a literal

Returns:

true iif the literal is marked.

resetMark

public void resetMark(int p)

Description copied from interface: IMarkableLits

Set the mark of a given literal to MARKLESS.

Specified by:

resetMark in interface IMarkableLits

Parameters:

p - a literal

resetAllMarks

public void resetAllMarks()

Description copied from interface: IMarkableLits

Set all the literal marks to MARKLESS

Specified by:

resetAllMarks in interface IMarkableLits

getMarkedLiterals

public IVecInt getMarkedLiterals()

Description copied from interface: IMarkableLits

Returns the set of all marked literals.

Specified by:

getMarkedLiterals in interface IMarkableLits

Returns:

a set of literals whose mark is different from MARKLESS.

getMarkedLiterals

public IVecInt getMarkedLiterals(int mark)

Description copied from interface: IMarkableLits

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

Specified by:

getMarkedLiterals in interface IMarkableLits

Parameters:

mark - a mark

Returns:

a set of literals whose mark is mark

getMarkedVariables

public IVecInt getMarkedVariables()

Description copied from interface: IMarkableLits

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

Specified by:

getMarkedVariables in interface IMarkableLits

Returns:

a set of variables whose mark is different from MARKLESS.

getMarkedVariables

public IVecInt getMarkedVariables(int mark)

Description copied from interface: IMarkableLits

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

Specified by:

getMarkedVariables in interface IMarkableLits

Parameters:

mark - a mark.

Returns:

a set of variables whose mark is mark.

getMarks

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

Specified by:

getMarks in interface IMarkableLits

Returns:

a list of marks used to mark the literals.