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)