Uses of Class
org.jacop.jasat.core.clauses.MapClause
Packages that use MapClause
Package
Description
-
Uses of MapClause in org.jacop.jasat.core
Fields in org.jacop.jasat.core declared as MapClauseMethods in org.jacop.jasat.core with parameters of type MapClauseModifier and TypeMethodDescriptionprivate final 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 final 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 MapClauseModifier and TypeMethodDescriptionBinaryClausesDatabase.resolutionWith
(int clauseId, MapClause clause) ClauseDatabaseInterface.resolutionWith
(int clauseIndex, MapClause clause) It returns the clause obtained by resolution between clauseIndex and clause.DatabasesStore.resolutionWith
(int clauseId, MapClause clause) DefaultClausesDatabase.resolutionWith
(int clauseId, MapClause explanation) LongClausesDatabase.resolutionWith
(int clauseIndex, MapClause clause) TernaryClausesDatabase.resolutionWith
(int clauseId, MapClause clause) UnaryClausesDatabase.resolutionWith
(int clauseId, MapClause clause) Methods in org.jacop.jasat.core.clauses with parameters of type MapClauseModifier and TypeMethodDescriptionBinaryClausesDatabase.resolutionWith
(int clauseId, MapClause clause) ClauseDatabaseInterface.resolutionWith
(int clauseIndex, MapClause clause) It returns the clause obtained by resolution between clauseIndex and clause.DatabasesStore.resolutionWith
(int clauseId, MapClause clause) DefaultClausesDatabase.resolutionWith
(int clauseId, MapClause explanation) LongClausesDatabase.resolutionWith
(int clauseIndex, MapClause clause) TernaryClausesDatabase.resolutionWith
(int clauseId, MapClause clause) UnaryClausesDatabase.resolutionWith
(int clauseId, MapClause clause) -
Uses of MapClause in org.jacop.jasat.modules
Fields in org.jacop.jasat.modules declared as MapClauseModifier and TypeFieldDescriptionprivate MapClause
SearchModule.clauseToLearn
private MapClause
DebugModule.mapClause
Methods in org.jacop.jasat.modules with parameters of type MapClauseModifier and TypeMethodDescriptionprivate 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
void
void
private void
DebugModule.printClause
(String prefix, MapClause mapClause) private void
DebugModule.printTrail
(String prefix, MapClause clause) -
Uses of MapClause in org.jacop.jasat.modules.interfaces
Methods in org.jacop.jasat.modules.interfaces with parameters of type MapClauseModifier and TypeMethodDescriptionvoid
ConflictListener.onConflict
(MapClause conflictclause, int level) called when a conflict occursvoid
called when the conflict clause is explained -
Uses of MapClause in org.jacop.jasat.utils
Fields in org.jacop.jasat.utils declared as MapClause -
Uses of MapClause in org.jacop.satwrapper
Fields in org.jacop.satwrapper declared as MapClauseModifier and TypeFieldDescriptionprivate MapClause
SatWrapper.clauseToLearn
private MapClause
WrapperDebugModule.mapClause
Methods in org.jacop.satwrapper with parameters of type MapClauseModifier and TypeMethodDescriptionvoid
SatWrapper.onConflict
(MapClause clause, int level) wrapper listens for conflicts.void
WrapperDebugModule.onConflict
(MapClause conflictClause, int level) void
wrapper listens for explanations, to know how deep to backtrackvoid
private void
WrapperDebugModule.printTrail
(String prefix, MapClause clause) -
Uses of MapClause in org.jacop.satwrapper.translation
Methods in org.jacop.satwrapper.translation that return MapClauseModifier and TypeMethodDescriptionDomainClausesDatabase.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 MapClauseModifier and TypeMethodDescriptionDomainClausesDatabase.resolutionWith
(int clauseIndex, MapClause clause) to get a real clause to resolve with, we seek for the clause at the origin of the propagation.