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)
BackjumpListenercomponents that want to be warned about backjumps should put themselves in Core.backjumpModules.
onBackjump in interface BackjumpListeneroldLevel - the level at which the solver was before backtrackingnewLevel - the level to which the solver backtrackspublic void onRestart(int oldLevel)
BackjumpListenercomponents that want to be warned about restarts should put themselves in Core.restartModules.
onRestart in interface BackjumpListeneroldLevel - the level at which the solver was before restartingpublic void onConflict(MapClause conflictClause, int level)
ConflictListeneronConflict in interface ConflictListenerconflictClause - the conflict (unsatisfiable) clauselevel - the level at which the conflict occurredpublic void sortArray()
public final void onClauseAdd(int[] clause,
int clauseId,
boolean isModelClause)
ClauseListeneronClauseAdd in interface ClauseListenerclause - the clauseclauseId - the clause's unique IdisModelClause - is this clause a model clause ?public final void onClauseRemoval(int clauseId)
ClauseListeneronClauseRemoval in interface ClauseListenerclauseId - the idpublic final int getLiteralToAssert()
public void initialize(Core core)
SolverComponentinitialize in interface SolverComponentcore - core component to initializeCopyright © 2022. All rights reserved.