Uses of Class
org.jacop.jasat.core.clauses.MapClause

Packages that use MapClause

Package	Description
org.jacop.jasat.core
org.jacop.jasat.core.clauses
org.jacop.jasat.modules
org.jacop.jasat.modules.interfaces
org.jacop.jasat.utils
org.jacop.satwrapper
org.jacop.satwrapper.translation

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 explanationClause
int	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 clause
void	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 occurs
void	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 backtrack
void	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.