Package org.jacop.jasat.core.clauses
Class AbstractClausesDatabase
java.lang.Object
org.jacop.jasat.core.clauses.AbstractClausesDatabase
- All Implemented Interfaces:
ClauseDatabaseInterface
,SolverComponent
- Direct Known Subclasses:
BinaryClausesDatabase
,DefaultClausesDatabase
,DomainClausesDatabase
,LongClausesDatabase
,TernaryClausesDatabase
,UnaryClausesDatabase
public abstract class AbstractClausesDatabase
extends Object
implements SolverComponent, ClauseDatabaseInterface
This class specifies an abstract class for clauses pools.
Those databases must use a MemoryPool to allocate their structures.
All ClausesDatabases have access to the DatabasesStore they belong to, so that they can convert the clauses unique ID to their local clauses index, and conversely.
- Version:
- 4.10
-
Field Summary
FieldsModifier and TypeFieldDescriptionprotected static final int
protected static int
protected static final int
protected static final int
protected static final int
int
protected static final int
protected int[][]
The first dimension corresponds to the index of the variable for which the watches are stored. -
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescriptionprotected final void
addWatch
(int literal, int clauseIndex) adds a watch (var => clause), ie make var watch clauseprotected final boolean
doesWatch
(int literal, int clauseIndex) protected final void
ensureWatch
(int var) ensures that varWatches.get(var) will succeed with a correct content.final int
final int
indexToUniqueId
(int clauseIndex) gets an unique ID from a clause index in this clause databasefinal void
initialize
(Core core) initializes the component with the given solver.abstract int
rateThisClause
(int[] clause) Indicates how much this database is optimized for this clause.protected final void
removeWatch
(int literal, int clauseIndex) removes the clause from the list of clauses that literal watchesfinal void
setDatabaseIndex
(int index) Called by the databaseStore, to inform the DatabasesStore of which index it has.abstract int
size()
number of clauses in the databaseprotected final void
swap
(int[] clause, int i, int j) swaps the two literals at position i and j in the clauseabstract void
toCNF
(BufferedWriter output) It creates a CNF description of the clauses stored in this database.final String
toString()
print the content of the Database in a nice wayprints the content of the database in a nice way, each line being prefixed withfinal int
uniqueIdToIndex
(int clauseId) gets a local index from the unique IDMethods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait
Methods inherited from interface org.jacop.jasat.core.clauses.ClauseDatabaseInterface
addClause, assertLiteral, backjump, canRemove, removeClause, resolutionWith
-
Field Details
-
CLAUSE_RATE_UNSUPPORTED
protected static final int CLAUSE_RATE_UNSUPPORTED- See Also:
-
CLAUSE_RATE_LOW
protected static final int CLAUSE_RATE_LOW- See Also:
-
CLAUSE_RATE_AVERAGE
protected static final int CLAUSE_RATE_AVERAGE- See Also:
-
CLAUSE_RATE_WELL_SUPPORTED
protected static final int CLAUSE_RATE_WELL_SUPPORTED- See Also:
-
CLAUSE_RATE_I_WANT_THIS_CLAUSE
protected static int CLAUSE_RATE_I_WANT_THIS_CLAUSE -
MINIMUM_VAR_WATCH_SIZE
protected static final int MINIMUM_VAR_WATCH_SIZE- See Also:
-
pool
-
trail
-
core
-
dbStore
-
databaseIndex
public int databaseIndex -
watchLists
protected int[][] watchListsThe first dimension corresponds to the index of the variable for which the watches are stored. The second index at position equal to 0 then it specifies the first free position to put index of next watched clause. The second index at position equal to n then it specifies the clause index of the n-th watched clause.
-
-
Constructor Details
-
AbstractClausesDatabase
public AbstractClausesDatabase()
-
-
Method Details
-
rateThisClause
public abstract int rateThisClause(int[] clause) Indicates how much this database is optimized for this clause. The Database that gives the higher rank will get the clause.- Parameters:
clause
- a clause to rate- Returns:
- a non negative integer indicating how much the database is interested in this clause
-
setDatabaseIndex
public final void setDatabaseIndex(int index) Called by the databaseStore, to inform the DatabasesStore of which index it has.- Parameters:
index
- the index of the database
-
getDatabaseIndex
public final int getDatabaseIndex()- Returns:
- the index of this database in the DatabasesStore
-
indexToUniqueId
public final int indexToUniqueId(int clauseIndex) gets an unique ID from a clause index in this clause database- Parameters:
clauseIndex
- a local clause index- Returns:
- an unique ID
-
uniqueIdToIndex
public final int uniqueIdToIndex(int clauseId) gets a local index from the unique ID- Parameters:
clauseId
- the unique Id- Returns:
- the index of the clause it corresponds to
-
doesWatch
protected final boolean doesWatch(int literal, int clauseIndex) - Parameters:
literal
- the literal to checkclauseIndex
- the clause id for checking- Returns:
- true if the literal watches the clause, false otherwise
-
ensureWatch
protected final void ensureWatch(int var) ensures that varWatches.get(var) will succeed with a correct content.- Parameters:
var
- the var we want to be able to add clauses to watch to
-
addWatch
protected final void addWatch(int literal, int clauseIndex) adds a watch (var => clause), ie make var watch clause- Parameters:
literal
- the watching literalclauseIndex
- the index of clause to watch. Not a unique ID.
-
removeWatch
protected final void removeWatch(int literal, int clauseIndex) removes the clause from the list of clauses that literal watches- Parameters:
literal
- the literalclauseIndex
- the clause to remove
-
size
public abstract int size()number of clauses in the database- Specified by:
size
in interfaceClauseDatabaseInterface
- Returns:
- the number of clauses in the database
-
toString
prints the content of the database in a nice way, each line being prefixed with- Parameters:
prefix
- prefix for printed line- Returns:
- a String representation of the database
-
toString
print the content of the Database in a nice way -
initialize
Description copied from interface:SolverComponent
initializes the component with the given solver. May be called only once. This method must register the component to the solver for the run.- Specified by:
initialize
in interfaceSolverComponent
- Parameters:
core
- core component to initialize
-
toCNF
It creates a CNF description of the clauses stored in this database.- Specified by:
toCNF
in interfaceClauseDatabaseInterface
- Parameters:
output
- it specifies the target to which the description will be written.- Throws:
IOException
- execption from java.io package
-
swap
protected final void swap(int[] clause, int i, int j) swaps the two literals at position i and j in the clause- Parameters:
clause
- the clausei
- the position (index) of the first literalj
- the position of the second literal
-