public final class ActivityModule extends Object implements ClauseListener, BackjumpListener, ConflictListener
Constructor and Description |
---|
ActivityModule() |
Modifier and Type | Method and Description |
---|---|
int |
getLiteralToAssert()
returns the non-set literal with highest activity, if any
|
void |
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 removed
|
void |
onConflict(MapClause conflictClause,
int level)
called when a conflict occurs
|
void |
onRestart(int oldLevel)
called when the solver restarts.
|
void |
sortArray()
sort the priorities array (useful after adding a lot of clauses)
|
String |
toString() |
public Core core
public void onBackjump(int oldLevel, int newLevel)
BackjumpListener
components that want to be warned about backjumps should put themselves in Core.backjumpModules.
onBackjump
in interface BackjumpListener
oldLevel
- the level at which the solver was before backtrackingnewLevel
- the level to which the solver backtrackspublic void onRestart(int oldLevel)
BackjumpListener
components that want to be warned about restarts should put themselves in Core.restartModules.
onRestart
in interface BackjumpListener
oldLevel
- the level at which the solver was before restartingpublic void onConflict(MapClause conflictClause, int level)
ConflictListener
onConflict
in interface ConflictListener
conflictClause
- the conflict (unsatisfiable) clauselevel
- the level at which the conflict occurredpublic void sortArray()
public final void onClauseAdd(int[] clause, int clauseId, boolean isModelClause)
ClauseListener
onClauseAdd
in interface ClauseListener
clause
- the clauseclauseId
- the clause's unique IdisModelClause
- is this clause a model clause ?public final void onClauseRemoval(int clauseId)
ClauseListener
onClauseRemoval
in interface ClauseListener
clauseId
- the idpublic final int getLiteralToAssert()
public void initialize(Core core)
SolverComponent
initialize
in interface SolverComponent
core
- core component to initializeCopyright © 2022. All rights reserved.