org.sat4j.minisat.constraints.cnf
Class Lits

java.lang.Object
  extended by org.sat4j.minisat.constraints.cnf.Lits
All Implemented Interfaces:
Serializable, ILits

public final class Lits
extends Object
implements Serializable, ILits

Author:
laihem, leberre
See Also:
Serialized Form

Field Summary
 
Fields inherited from interface org.sat4j.minisat.core.ILits
UNDEFINED
 
Constructor Summary
Lits()
           
 
Method Summary
 boolean belongsToPool(int x)
          Returns true iff the variable is used in the set of constraints.
protected  int capacity()
          To get the capacity of the current vocabulary.
 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 nextFreeVarId(boolean reserve)
          Ask the solver for a free variable identifier, in Dimacs format (i.e. a positive number).
 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)
           
static String toString(int lit)
           
 void unassign(int lit)
           
 IVec<Undoable> undos(int lit)
           
 String valueToString(int lit)
           
 void watch(int lit, Propagatable c)
           
 IVec<Propagatable> watches(int lit)
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

Lits

public Lits()
Method Detail

init

public final void init(int nvar)
Specified by:
init in interface ILits

getFromPool

public int getFromPool(int x)
Description copied from interface: ILits
Translates a Dimacs literal into an internal representation literal.

Specified by:
getFromPool in interface ILits
Parameters:
x - the Dimacs literal (a non null integer).
Returns:
the literal in the internal representation.

belongsToPool

public boolean belongsToPool(int x)
Description copied from interface: ILits
Returns true iff the variable is used in the set of constraints.

Specified by:
belongsToPool in interface ILits
Returns:
true iff the variable belongs to the formula.

resetPool

public void resetPool()
Specified by:
resetPool in interface ILits

ensurePool

public void ensurePool(int howmany)
Specified by:
ensurePool in interface ILits

unassign

public void unassign(int lit)
Specified by:
unassign in interface ILits

satisfies

public void satisfies(int lit)
Specified by:
satisfies in interface ILits

isSatisfied

public boolean isSatisfied(int lit)
Specified by:
isSatisfied in interface ILits

isFalsified

public final boolean isFalsified(int lit)
Specified by:
isFalsified in interface ILits

isUnassigned

public boolean isUnassigned(int lit)
Specified by:
isUnassigned in interface ILits

valueToString

public String valueToString(int lit)
Specified by:
valueToString in interface ILits

nVars

public int nVars()
Description copied from interface: ILits
to obtain the max id of the variable

Specified by:
nVars in interface ILits
Returns:
the maximum number of variables in the formula

not

public int not(int lit)
Specified by:
not in interface ILits

toString

public static String toString(int lit)

reset

public void reset(int lit)
Specified by:
reset in interface ILits

getLevel

public int getLevel(int lit)
Specified by:
getLevel in interface ILits

setLevel

public void setLevel(int lit,
                     int l)
Specified by:
setLevel in interface ILits

getReason

public Constr getReason(int lit)
Specified by:
getReason in interface ILits

setReason

public void setReason(int lit,
                      Constr r)
Specified by:
setReason in interface ILits

undos

public IVec<Undoable> undos(int lit)
Specified by:
undos in interface ILits

watch

public void watch(int lit,
                  Propagatable c)
Specified by:
watch in interface ILits

watches

public IVec<Propagatable> watches(int lit)
Specified by:
watches in interface ILits
Parameters:
lit - a literal
Returns:
the list of all the constraints that watch the negation of lit

isImplied

public boolean isImplied(int lit)
Specified by:
isImplied in interface ILits
Returns:
true iff the truth value of that literal is due to a unit propagation or a decision.

realnVars

public int realnVars()
Description copied from interface: ILits
to obtain the real number of variables appearing in the formula

Specified by:
realnVars in interface ILits
Returns:
the number of variables used in the pool

capacity

protected int capacity()
To get the capacity of the current vocabulary.

Returns:
the total number of variables that can be managed by the vocabulary.

nextFreeVarId

public int nextFreeVarId(boolean reserve)
Description copied from interface: ILits
Ask the solver for a free variable identifier, in Dimacs format (i.e. a positive number). Note that a previous call to ensurePool(max) will reserve in the solver the variable identifier from 1 to max, so nextFreeVarId() would return max+1, even if some variable identifiers smaller than max are not used.

Specified by:
nextFreeVarId in interface ILits
Returns:
a variable identifier not in use in the constraints already inside the solver.
Since:
2.1


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