org.sat4j.minisat.constraints.cnf
Class Lits

java.lang.Object
  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