org.sat4j.minisat.constraints.cnf
Class MarkableLits

java.lang.Object
  extended by org.sat4j.minisat.constraints.cnf.Lits
      extended by 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.


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