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 java.lang.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.7
-
-
Field Summary
Fields Modifier and Type Field Description protected static int
CLAUSE_RATE_AVERAGE
protected static int
CLAUSE_RATE_I_WANT_THIS_CLAUSE
protected static int
CLAUSE_RATE_LOW
protected static int
CLAUSE_RATE_UNSUPPORTED
protected static int
CLAUSE_RATE_WELL_SUPPORTED
Core
core
int
databaseIndex
DatabasesStore
dbStore
protected static int
MINIMUM_VAR_WATCH_SIZE
MemoryPool
pool
Trail
trail
protected int[][]
watchLists
The first dimension corresponds to the index of the variable for which the watches are stored.
-
Constructor Summary
Constructors Constructor Description AbstractClausesDatabase()
-
Method Summary
All Methods Instance Methods Abstract Methods Concrete Methods Modifier and Type Method Description protected void
addWatch(int literal, int clauseIndex)
adds a watch (var => clause), ie make var watch clauseprotected boolean
doesWatch(int literal, int clauseIndex)
protected void
ensureWatch(int var)
ensures that varWatches.get(var) will succeed with a correct content.int
getDatabaseIndex()
int
indexToUniqueId(int clauseIndex)
gets an unique ID from a clause index in this clause databasevoid
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 void
removeWatch(int literal, int clauseIndex)
removes the clause from the list of clauses that literal watchesvoid
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 void
swap(int[] clause, int i, int j)
swaps the two literals at position i and j in the clauseabstract void
toCNF(java.io.BufferedWriter output)
It creates a CNF description of the clauses stored in this database.java.lang.String
toString()
print the content of the Database in a nice wayjava.lang.String
toString(java.lang.String prefix)
prints the content of the database in a nice way, each line being prefixed withint
uniqueIdToIndex(int clauseId)
gets a local index from the unique ID-
Methods 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 Detail
-
CLAUSE_RATE_UNSUPPORTED
protected static final int CLAUSE_RATE_UNSUPPORTED
- See Also:
- Constant Field Values
-
CLAUSE_RATE_LOW
protected static final int CLAUSE_RATE_LOW
- See Also:
- Constant Field Values
-
CLAUSE_RATE_AVERAGE
protected static final int CLAUSE_RATE_AVERAGE
- See Also:
- Constant Field Values
-
CLAUSE_RATE_WELL_SUPPORTED
protected static final int CLAUSE_RATE_WELL_SUPPORTED
- See Also:
- Constant Field Values
-
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:
- Constant Field Values
-
pool
public MemoryPool pool
-
trail
public Trail trail
-
core
public Core core
-
dbStore
public DatabasesStore dbStore
-
databaseIndex
public int databaseIndex
-
watchLists
protected int[][] watchLists
The 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.
-
-
Method Detail
-
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
public java.lang.String toString(java.lang.String prefix)
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
public final java.lang.String toString()
print the content of the Database in a nice way- Overrides:
toString
in classjava.lang.Object
-
initialize
public final void initialize(Core core)
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
public abstract void toCNF(java.io.BufferedWriter output) throws java.io.IOException
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:
java.io.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
-
-