public interface ILits
Modifier and Type | Field and Description |
---|---|
static int |
UNDEFINED |
Modifier and Type | Method and Description |
---|---|
boolean |
belongsToPool(int x)
Returns true iff the variable is used in the set of constraints.
|
void |
ensurePool(int howmany)
Make sure that all data structures are ready to manage howmany boolean
variables.
|
void |
forgets(int var)
Removes a variable from the formula.
|
int |
getFromPool(int x)
Translates a Dimacs literal into an internal representation literal.
|
int |
getLevel(int lit)
Returns the level at which that literal has been assigned a value, else
-1.
|
Constr |
getReason(int lit)
Returns the reason of the assignment of a literal.
|
void |
init(int nvar) |
boolean |
isFalsified(int lit)
Check if a literal is falsified.
|
boolean |
isImplied(int lit) |
boolean |
isSatisfied(int lit)
Check if a literal is satisfied.
|
boolean |
isUnassigned(int lit)
Check if a literal is assigned a truth value.
|
int |
nextFreeVarId(boolean reserve)
Ask the solver for a free variable identifier, in Dimacs format (i.e. a
positive number).
|
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)
Reset a literal in the vocabulary.
|
void |
resetPool()
reset the vocabulary.
|
void |
satisfies(int lit)
Satisfies a boolean variable (truth value is TRUE).
|
void |
setLevel(int lit,
int l)
Sets the decision level of a literal.
|
void |
setReason(int lit,
Constr r)
Sets the reason of the assignment of a literal.
|
void |
unassign(int lit)
Unassigns a boolean variable (truth value if UNDEF).
|
IVec<Undoable> |
undos(int lit)
Retrieve the methods to call when the solver backtracks.
|
String |
valueToString(int lit)
Returns a textual representation of the truth value of that literal.
|
void |
watch(int lit,
Propagatable c)
Record a new constraint to watch when a literal is satisfied.
|
IVec<Propagatable> |
watches(int lit) |
static final int UNDEFINED
void init(int nvar)
int getFromPool(int x)
x
- the Dimacs literal (a non null integer).boolean belongsToPool(int x)
x
- void resetPool()
void ensurePool(int howmany)
howmany
- the new capacity (in boolean variables) of the vocabulary.void unassign(int lit)
lit
- a literal in internal format.void satisfies(int lit)
lit
- a literal in internal format.void forgets(int var)
var
- a variable in Dimacs format.boolean isSatisfied(int lit)
lit
- a literal in internal format.boolean isFalsified(int lit)
lit
- a literal in internal format.boolean isUnassigned(int lit)
lit
- a literal in internal format.boolean isImplied(int lit)
lit
- int nVars()
int realnVars()
int nextFreeVarId(boolean reserve)
void reset(int lit)
lit
- a literal in internal representation.int getLevel(int lit)
lit
- a literal in internal representation.void setLevel(int lit, int l)
lit
- a literal in internal representation.l
- a decision level, or -1Constr getReason(int lit)
lit
- a literal in internal representation.void setReason(int lit, Constr r)
lit
- a literal in internal representation.r
- the constraint that forces the assignment of that literal,
null if there are none.IVec<Undoable> undos(int lit)
lit
- a literal in internal representation.void watch(int lit, Propagatable c)
lit
- a literal in internal representation.c
- a constraint that contains the negation of that literal.IVec<Propagatable> watches(int lit)
lit
- a literal in internal representation.String valueToString(int lit)
lit
- a literal in internal representation.Copyright © 2013 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.