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.


Copyright © 2009 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.