Package org.jacop.jasat.core
Class Trail
java.lang.Object
org.jacop.jasat.core.Trail
- All Implemented Interfaces:
SolverComponent
It stores the current variables status (affected or not, with which value and explanation).
It values of variables are packed in an int, together with the level at which
they were asserted.
- Version:
- 4.10
-
Field Summary
FieldsModifier and TypeFieldDescriptionprivate int
int[]
private int
private int[]
int[]
-
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescriptionvoid
addVariable
(int var) It adds a variable to the trail.private void
assertLit
(int var, int literal, int level, boolean asserted) real assignment of literal at levelvoid
assertLiteral
(int literal, int level) Sets a literal, that is, a variable signed with its value (> 0 for true, < 0 for false).void
assertLiteral
(int literal, int level, int causeId) Sets a literal, with an explanation clause.void
backjump
(int level) It tells the trail to return to given level.void
ensureCapacity
(int numVar) It ensures the trail can contain @param numVar variablesint
getExplanation
(int var) It returns the index of the clause that caused this variable to be setint
getLevel
(int var) It returns the level at which @param var has been set.void
initialize
(Core core) to be called before any use of the trailboolean
isAsserted
(int var) It returns information if a variable was asserted or only propagated.boolean
isSet
(int var) predicate which meaning is : is this variable set or unknown ?int
size()
returns the number of currently set variablestoString()
void
unset
(int var) It unsets the given variable.
-
Field Details
-
pool
-
values
public int[] values -
explanations
public int[] explanations -
assertionStack
-
levels
private int[] levels -
ASSERTED_MASK
private int ASSERTED_MASK -
LEVEL_MASK
private int LEVEL_MASK
-
-
Constructor Details
-
Trail
public Trail()
-
-
Method Details
-
addVariable
public void addVariable(int var) It adds a variable to the trail.- Parameters:
var
- the variable
-
ensureCapacity
public void ensureCapacity(int numVar) It ensures the trail can contain @param numVar variables- Parameters:
numVar
- the number of variables the trail must be able to contain
-
assertLiteral
public void assertLiteral(int literal, int level) Sets a literal, that is, a variable signed with its value (> 0 for true, < 0 for false). This must be used only for asserted values, not the ones propagated from unit clauses.- Parameters:
literal
- the literallevel
- the current level
-
assertLiteral
public void assertLiteral(int literal, int level, int causeId) Sets a literal, with an explanation clause. For unit propagation only.- Parameters:
literal
- the literal (non nul relative number)level
- the level at which this assertion occurscauseId
- the ID of the clause that triggered this assertion
-
assertLit
private void assertLit(int var, int literal, int level, boolean asserted) real assignment of literal at level -
unset
public void unset(int var) It unsets the given variable. Does not take car of assertionLevels !- Parameters:
var
- the variable to unset. Must be positive.
-
backjump
public void backjump(int level) It tells the trail to return to given level. It will therefore erase all assertion strictly above this level. Literals asserted at @param level will be kept.- Parameters:
level
- the level to jump to.
-
getLevel
public int getLevel(int var) It returns the level at which @param var has been set. @param var *must* be set, otherwise this will fail.- Parameters:
var
- the literal which level we wish to know- Returns:
- the level
-
getExplanation
public int getExplanation(int var) It returns the index of the clause that caused this variable to be set- Parameters:
var
- the literal. Must be set.- Returns:
- an index if there was an explanation, 0 otherwise
-
isAsserted
public boolean isAsserted(int var) It returns information if a variable was asserted or only propagated.- Parameters:
var
- the variable- Returns:
- true if the variable was asserted
-
isSet
public boolean isSet(int var) predicate which meaning is : is this variable set or unknown ?- Parameters:
var
- the variable, must be positive- Returns:
- true if the variable is set.
-
size
public int size()returns the number of currently set variables- Returns:
- the number of currently set variables
-
toString
-
initialize
to be called before any use of the trail- Specified by:
initialize
in interfaceSolverComponent
- Parameters:
core
- the Solver instance
-