Lits (SAT4J core 2.3.4 API)

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

Constructors
Constructor and Description

Lits()

Constructors
Constructor and Description
`Lits()`

Method Summary

Methods
Modifier and Type	Method and Description
`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)` 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`	`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)` 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.
`static String`	`toString(int lit)`
`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)`

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 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()
```
    Description copied from interface: ILits
    
    reset the vocabulary.
    
    Specified by:
    
    resetPool in interface ILits
  - ensurePool
```
public void ensurePool(int howmany)
```
    Description copied from interface: ILits
    
    Make sure that all data structures are ready to manage howmany boolean variables.
    
    Specified by:
    
    ensurePool in interface ILits
    
    Parameters:
    howmany - the new capacity (in boolean variables) of the vocabulary.
  - unassign
```
public void unassign(int lit)
```
    Description copied from interface: ILits
    
    Unassigns a boolean variable (truth value if UNDEF).
    
    Specified by:
    
    unassign in interface ILits
    
    Parameters:
    lit - a literal in internal format.
  - satisfies
```
public void satisfies(int lit)
```
    Description copied from interface: ILits
    
    Satisfies a boolean variable (truth value is TRUE).
    
    Specified by:
    
    satisfies in interface ILits
    
    Parameters:
    lit - a literal in internal format.
  - forgets
```
public void forgets(int var)
```
    Description copied from interface: ILits
    
    Removes a variable from the formula. All occurrences of that variables are removed. It is equivalent in our implementation to falsify the two phases of that variable.
    
    Specified by:
    
    forgets in interface ILits
    
    Parameters:
    var - a variable in Dimacs format.
  - isSatisfied
```
public boolean isSatisfied(int lit)
```
    Description copied from interface: ILits
    
    Check if a literal is satisfied.
    
    Specified by:
    
    isSatisfied in interface ILits
    
    Parameters:
    lit - a literal in internal format.
    
    Returns:
    true if that literal is satisfied.
  - isFalsified
```
public boolean isFalsified(int lit)
```
    Description copied from interface: ILits
    
    Check if a literal is falsified.
    
    Specified by:
    
    isFalsified in interface ILits
    
    Parameters:
    lit - a literal in internal format.
    
    Returns:
    true if the literal is falsified. Note that a forgotten variable will also see its literals as falsified.
  - isUnassigned
```
public boolean isUnassigned(int lit)
```
    Description copied from interface: ILits
    
    Check if a literal is assigned a truth value.
    
    Specified by:
    
    isUnassigned in interface ILits
    
    Parameters:
    lit - a literal in internal format.
    
    Returns:
    true if the literal is neither satisfied nor falsified.
  - valueToString
```
public String valueToString(int lit)
```
    Description copied from interface: ILits
    
    Returns a textual representation of the truth value of that literal.
    
    Specified by:
    
    valueToString in interface ILits
    
    Parameters:
    lit - a literal in internal representation.
    
    Returns:
    one of T for true, F for False or ? for unassigned.
  - 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)
```
  - toString
```
public static String toString(int lit)
```
  - reset
```
public void reset(int lit)
```
    Description copied from interface: ILits
    
    Reset a literal in the vocabulary.
    
    Specified by:
    
    reset in interface ILits
    
    Parameters:
    lit - a literal in internal representation.
  - getLevel
```
public int getLevel(int lit)
```
    Description copied from interface: ILits
    
    Returns the level at which that literal has been assigned a value, else -1.
    
    Specified by:
    
    getLevel in interface ILits
    
    Parameters:
    lit - a literal in internal representation.
    
    Returns:
    -1 if the literal is unassigned, or the decision level of the literal.
  - setLevel
```
public void setLevel(int lit,
            int l)
```
    Description copied from interface: ILits
    
    Sets the decision level of a literal.
    
    Specified by:
    
    setLevel in interface ILits
    
    Parameters:
    lit - a literal in internal representation.
    l - a decision level, or -1
  - getReason
```
public Constr getReason(int lit)
```
    Description copied from interface: ILits
    
    Returns the reason of the assignment of a literal.
    
    Specified by:
    
    getReason in interface ILits
    
    Parameters:
    lit - a literal in internal representation.
    
    Returns:
    the constraint that propagated that literal, else null.
  - setReason
```
public void setReason(int lit,
             Constr r)
```
    Description copied from interface: ILits
    
    Sets the reason of the assignment of a literal.
    
    Specified by:
    
    setReason in interface ILits
    
    Parameters:
    lit - a literal in internal representation.
    r - the constraint that forces the assignment of that literal, null if there are none.
  - undos
```
public IVec<Undoable> undos(int lit)
```
    Description copied from interface: ILits
    
    Retrieve the methods to call when the solver backtracks. Useful for counter based data structures.
    
    Specified by:
    
    undos in interface ILits
    
    Parameters:
    lit - a literal in internal representation.
    
    Returns:
    a list of methods to call on bactracking.
  - watch
```
public void watch(int lit,
         Propagatable c)
```
    Description copied from interface: ILits
    
    Record a new constraint to watch when a literal is satisfied.
    
    Specified by:
    
    watch in interface ILits
    
    Parameters:
    lit - a literal in internal representation.
    c - a constraint that contains the negation of that literal.
  - watches
```
public IVec<Propagatable> watches(int lit)
```
    Specified by:
    
    watches in interface ILits
    
    Parameters:
    lit - a literal in internal representation.
    
    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

Class Lits

Field Summary

Fields inherited from interface org.sat4j.minisat.core.ILits

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Constructor Detail

Lits

Method Detail

init

getFromPool

belongsToPool

resetPool

ensurePool

unassign

satisfies

forgets

isSatisfied

isFalsified

isUnassigned

valueToString

nVars

not

toString

reset

getLevel

setLevel

getReason

setReason

undos

watch

watches

isImplied

realnVars

capacity

nextFreeVarId