Package org.jacop.jasat.modules
Class ActivityModule
- java.lang.Object
-
- org.jacop.jasat.modules.ActivityModule
-
- All Implemented Interfaces:
SolverComponent
,BackjumpListener
,ClauseListener
,ConflictListener
public final class ActivityModule extends java.lang.Object implements ClauseListener, BackjumpListener, ConflictListener
counts the activity of literals- Version:
- 4.8
-
-
Field Summary
Fields Modifier and Type Field Description private int
activitiesIndex
private int
BUMP_INCREASE_FACTOR
private java.util.Comparator<java.lang.Integer>
comparator
compares literals according to their activity.private int
CONFLICT_COUNT_TO_SORT
private int
conflictCount
Core
core
private int
currentBumpRate
private int
LEARNT_COUNT_TO_INCREASE
private int
learntCount
private int[]
negActivities
private int[]
posActivities
private java.lang.Integer[]
priorities
private int
prioritiesIndex
private java.util.BitSet
prioritizedVars
private int
rebaseThreshold
-
Constructor Summary
Constructors Constructor Description ActivityModule()
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description private int
bumpVar(int literal)
code that really performs variable and polarity activity bumping.private void
ensureVarSize(int var)
private int
getLiteralActivity(int var, boolean polarity)
gives activity of a (signed) literalint
getLiteralToAssert()
returns the non-set literal with highest activity, if anyprivate void
increaseBumpRate()
increases the bump rate, so that recent activity is more important than old activityvoid
initialize(Core core)
initializes the component with the given solver.void
onBackjump(int oldLevel, int newLevel)
Called when the solver backtracks.void
onClauseAdd(int[] clause, int clauseId, boolean isModelClause)
called when the given clause is added.void
onClauseRemoval(int clauseId)
called when the clause with unique Id @param clauseId is removedvoid
onConflict(MapClause conflictClause, int level)
called when a conflict occursvoid
onRestart(int oldLevel)
called when the solver restarts.private void
rebase(int value)
rebases all valuesvoid
sortArray()
sort the priorities array (useful after adding a lot of clauses)java.lang.String
toString()
-
-
-
Field Detail
-
BUMP_INCREASE_FACTOR
private int BUMP_INCREASE_FACTOR
-
LEARNT_COUNT_TO_INCREASE
private final int LEARNT_COUNT_TO_INCREASE
- See Also:
- Constant Field Values
-
CONFLICT_COUNT_TO_SORT
private final int CONFLICT_COUNT_TO_SORT
- See Also:
- Constant Field Values
-
posActivities
private int[] posActivities
-
negActivities
private int[] negActivities
-
activitiesIndex
private int activitiesIndex
-
currentBumpRate
private int currentBumpRate
-
rebaseThreshold
private int rebaseThreshold
-
learntCount
private int learntCount
-
priorities
private java.lang.Integer[] priorities
-
prioritiesIndex
private int prioritiesIndex
-
prioritizedVars
private java.util.BitSet prioritizedVars
-
conflictCount
private int conflictCount
-
core
public Core core
-
comparator
private final java.util.Comparator<java.lang.Integer> comparator
compares literals according to their activity. This stands for i > j and not i < j, because we want activities to be sorted in decreasing order
-
-
Method Detail
-
onBackjump
public void onBackjump(int oldLevel, int newLevel)
Description copied from interface:BackjumpListener
Called when the solver backtracks. It will also be called when the solver restarts.components that want to be warned about backjumps should put themselves in Core.backjumpModules.
- Specified by:
onBackjump
in interfaceBackjumpListener
- Parameters:
oldLevel
- the level at which the solver was before backtrackingnewLevel
- the level to which the solver backtracks
-
onRestart
public void onRestart(int oldLevel)
Description copied from interface:BackjumpListener
called when the solver restarts.components that want to be warned about restarts should put themselves in Core.restartModules.
- Specified by:
onRestart
in interfaceBackjumpListener
- Parameters:
oldLevel
- the level at which the solver was before restarting
-
onConflict
public void onConflict(MapClause conflictClause, int level)
Description copied from interface:ConflictListener
called when a conflict occurs- Specified by:
onConflict
in interfaceConflictListener
- Parameters:
conflictClause
- the conflict (unsatisfiable) clauselevel
- the level at which the conflict occurred
-
sortArray
public void sortArray()
sort the priorities array (useful after adding a lot of clauses)
-
onClauseAdd
public final void onClauseAdd(int[] clause, int clauseId, boolean isModelClause)
Description copied from interface:ClauseListener
called when the given clause is added.- Specified by:
onClauseAdd
in interfaceClauseListener
- Parameters:
clause
- the clauseclauseId
- the clause's unique IdisModelClause
- is this clause a model clause ?
-
onClauseRemoval
public final void onClauseRemoval(int clauseId)
Description copied from interface:ClauseListener
called when the clause with unique Id @param clauseId is removed- Specified by:
onClauseRemoval
in interfaceClauseListener
- Parameters:
clauseId
- the id
-
getLiteralToAssert
public final int getLiteralToAssert()
returns the non-set literal with highest activity, if any- Returns:
- a non set literal, or 0 if all known literals are set
-
getLiteralActivity
private final int getLiteralActivity(int var, boolean polarity)
gives activity of a (signed) literal- Parameters:
literal
- the literal- Returns:
- the activity of this (variable, polarity)
-
bumpVar
private final int bumpVar(int literal)
code that really performs variable and polarity activity bumping.- Parameters:
var
- the variable- Returns:
- the new activity of the variable
-
ensureVarSize
private final void ensureVarSize(int var)
-
increaseBumpRate
private final void increaseBumpRate()
increases the bump rate, so that recent activity is more important than old activity
-
rebase
private final void rebase(int value)
rebases all values- Parameters:
value
- the value that just overflowed
-
toString
public java.lang.String toString()
- Overrides:
toString
in classjava.lang.Object
-
initialize
public void initialize(Core core)
Description copied from interface:SolverComponent
initializes the component with the given solver. May be called only once. This method must register the component to the solver for the run.- Specified by:
initialize
in interfaceSolverComponent
- Parameters:
core
- core component to initialize
-
-