Uses of Class
org.jacop.jasat.core.clauses.MapClause
-
-
Uses of MapClause in org.jacop.jasat.core
Fields in org.jacop.jasat.core declared as MapClause Modifier and Type Field Description MapClause
Core. explanationClause
Methods in org.jacop.jasat.core with parameters of type MapClause Modifier and Type Method Description private void
ConflictLearning. applyExplain(MapClause explanationClause, int literal)
performs one step of resolution for conflict explanation on given explanation clause.void
ConflictLearning. applyExplainUIP(MapClause explanationClause)
It builds the explanation clause made of all literals that were involved in a conflict (ie which are in the clause and were asserted, or were asserted and triggered, in another clause, the propagation of a literal present in the current clause)private int
ConflictLearning. findPositionTopLiteral(MapClause explanationClause, int level, int startingPosition)
It gets the position of last set literal of the clause.int
ConflictLearning. getLevelToBackjump(MapClause explanationClause)
It computes to which level we should backjump to solve the conflict explained by @param explanationClauseint
Core. getLevelToBackjump(MapClause explanationClause)
void
Core. triggerConflictEvent(MapClause clause)
triggers a conflict.void
Core. triggerLearnEvent(MapClause clauseToLearn)
triggers an event of learning -
Uses of MapClause in org.jacop.jasat.core.clauses
Methods in org.jacop.jasat.core.clauses that return MapClause Modifier and Type Method Description MapClause
BinaryClausesDatabase. resolutionWith(int clauseId, MapClause clause)
MapClause
ClauseDatabaseInterface. resolutionWith(int clauseIndex, MapClause clause)
It returns the clause obtained by resolution between clauseIndex and clause.MapClause
DatabasesStore. resolutionWith(int clauseId, MapClause clause)
MapClause
DefaultClausesDatabase. resolutionWith(int clauseId, MapClause explanation)
MapClause
LongClausesDatabase. resolutionWith(int clauseIndex, MapClause clause)
MapClause
TernaryClausesDatabase. resolutionWith(int clauseId, MapClause clause)
MapClause
UnaryClausesDatabase. resolutionWith(int clauseId, MapClause clause)
Methods in org.jacop.jasat.core.clauses with parameters of type MapClause Modifier and Type Method Description MapClause
BinaryClausesDatabase. resolutionWith(int clauseId, MapClause clause)
MapClause
ClauseDatabaseInterface. resolutionWith(int clauseIndex, MapClause clause)
It returns the clause obtained by resolution between clauseIndex and clause.MapClause
DatabasesStore. resolutionWith(int clauseId, MapClause clause)
MapClause
DefaultClausesDatabase. resolutionWith(int clauseId, MapClause explanation)
MapClause
LongClausesDatabase. resolutionWith(int clauseIndex, MapClause clause)
MapClause
TernaryClausesDatabase. resolutionWith(int clauseId, MapClause clause)
MapClause
UnaryClausesDatabase. resolutionWith(int clauseId, MapClause clause)
-
Uses of MapClause in org.jacop.jasat.modules
Fields in org.jacop.jasat.modules declared as MapClause Modifier and Type Field Description private MapClause
SearchModule. clauseToLearn
private MapClause
DebugModule. mapClause
Methods in org.jacop.jasat.modules with parameters of type MapClause Modifier and Type Method Description private int
HeuristicForgetModule. computeLBD(MapClause clause)
compute the LBD (Literal Block Distance) of a clausevoid
ActivityModule. onConflict(MapClause conflictClause, int level)
void
DebugModule. onConflict(MapClause conflictClause, int level)
void
HeuristicRestartModule. onConflict(MapClause clause, int level)
void
StatModule. onConflict(MapClause clause, int level)
void
DebugModule. onExplain(MapClause explanation)
void
HeuristicForgetModule. onExplain(MapClause explanation)
void
SearchModule. onExplain(MapClause explanation)
private void
DebugModule. printClause(java.lang.String prefix, MapClause mapClause)
private void
DebugModule. printTrail(java.lang.String prefix, MapClause clause)
-
Uses of MapClause in org.jacop.jasat.modules.interfaces
Methods in org.jacop.jasat.modules.interfaces with parameters of type MapClause Modifier and Type Method Description void
ConflictListener. onConflict(MapClause conflictclause, int level)
called when a conflict occursvoid
ExplanationListener. onExplain(MapClause explanation)
called when the conflict clause is explained -
Uses of MapClause in org.jacop.jasat.utils
Fields in org.jacop.jasat.utils declared as MapClause Modifier and Type Field Description private MapClause
BasicPreprocessor. localClause
-
Uses of MapClause in org.jacop.satwrapper
Fields in org.jacop.satwrapper declared as MapClause Modifier and Type Field Description private MapClause
SatWrapper. clauseToLearn
private MapClause
WrapperDebugModule. mapClause
Methods in org.jacop.satwrapper with parameters of type MapClause Modifier and Type Method Description void
SatWrapper. onConflict(MapClause clause, int level)
wrapper listens for conflicts.void
WrapperDebugModule. onConflict(MapClause conflictClause, int level)
void
SatWrapper. onExplain(MapClause explanation)
wrapper listens for explanations, to know how deep to backtrackvoid
WrapperDebugModule. onExplain(MapClause explanation)
private void
WrapperDebugModule. printTrail(java.lang.String prefix, MapClause clause)
-
Uses of MapClause in org.jacop.satwrapper.translation
Methods in org.jacop.satwrapper.translation that return MapClause Modifier and Type Method Description MapClause
DomainClausesDatabase. resolutionWith(int clauseIndex, MapClause clause)
to get a real clause to resolve with, we seek for the clause at the origin of the propagation.Methods in org.jacop.satwrapper.translation with parameters of type MapClause Modifier and Type Method Description MapClause
DomainClausesDatabase. resolutionWith(int clauseIndex, MapClause clause)
to get a real clause to resolve with, we seek for the clause at the origin of the propagation.
-