Package org.jacop.jasat.core.clauses
Class DatabasesStore
java.lang.Object
org.jacop.jasat.core.clauses.DatabasesStore
- All Implemented Interfaces:
ClauseDatabaseInterface
,SolverComponent
public final class DatabasesStore
extends Object
implements SolverComponent, ClauseDatabaseInterface
This provides a unique interface to several databases. It also translates
clauses ids to get them unique across the whole system. Databases have
access to it, so that they can translate unique clauses ids in both way.
- Version:
- 4.8
-
Field Summary
FieldsModifier and TypeFieldDescriptionint
private int
private int
private int
private int
private int
-
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescriptionint
addClause
(int[] clause, boolean isModelClause) It adds a clause to the database.void
addDatabase
(AbstractClausesDatabase database) Adds a ClausesDatabase to the Storefinal void
assertLiteral
(int literal) tells all databases that the literal is set, for unit propagation.void
backjump
(int level) tells all databases to backjump at this levelboolean
canRemove
(int clauseId) It tells if the implementation of ClausesDatabase can remove clauses or notfinal int
indexesToUniqueId
(int clauseIndex, int databaseIndex) It gets a unique id from a clause index, relative to a database, and a database index.void
initialize
(Core core) initializes the component with the given solver.private void
void
removeClause
(int clauseId) removes this clause from the database it belongs to.resolutionWith
(int clauseId, MapClause clause) It returns the clause obtained by resolution between clauseIndex and clause.int
size()
the number of clauses in all databasesvoid
toCNF
(BufferedWriter output) It writes the clauses of the databases in cnf format to the specified writer.toString()
final int
uniqueIdToDb
(int clauseId) returns the ClausesDatabase associated with this clauseIdfinal int
uniqueIdToIndex
(int clauseId) Removes the database index of the clause, to get a real clause index.
-
Field Details
-
MAX_NUMBER_OF_DATABASES
private int MAX_NUMBER_OF_DATABASES -
DATABASES_MASK
private int DATABASES_MASK -
INDEX_MASK
private int INDEX_MASK -
INDEX_MASK_NUM_BITS
private int INDEX_MASK_NUM_BITS -
LOG_OF_NUM_DATABASES
private int LOG_OF_NUM_DATABASES -
databases
-
currentIndex
public int currentIndex -
core
-
-
Constructor Details
-
DatabasesStore
public DatabasesStore()
-
-
Method Details
-
initializeMasks
private void initializeMasks() -
addClause
public int addClause(int[] clause, boolean isModelClause) Description copied from interface:ClauseDatabaseInterface
It adds a clause to the database. This can change the state of the solver, for example if the clause is unsatisfiable in the current trail affectation, the solver will get in the conflict state.- Specified by:
addClause
in interfaceClauseDatabaseInterface
- Parameters:
clause
- the clause to addisModelClause
- defined if the clause is model clause- Returns:
- the unique ID referring to the clause
-
canRemove
public boolean canRemove(int clauseId) Description copied from interface:ClauseDatabaseInterface
It tells if the implementation of ClausesDatabase can remove clauses or not- Specified by:
canRemove
in interfaceClauseDatabaseInterface
- Parameters:
clauseId
- the unique Id of the clause- Returns:
- true iff removal of clauses is possible
-
removeClause
public void removeClause(int clauseId) removes this clause from the database it belongs to.- Specified by:
removeClause
in interfaceClauseDatabaseInterface
- Parameters:
clauseId
- the id of the clause to be deleted
-
resolutionWith
Description copied from interface:ClauseDatabaseInterface
It returns the clause obtained by resolution between clauseIndex and clause. It will also modify in place the given SetClause (avoid allocating).- Specified by:
resolutionWith
in interfaceClauseDatabaseInterface
- Parameters:
clauseId
- the unique id of the clauseclause
- an explanation clause that is modified by resolution- Returns:
- the clause obtained by resolution
-
addDatabase
Adds a ClausesDatabase to the Store- Parameters:
database
- the database to add
-
size
public int size()the number of clauses in all databases- Specified by:
size
in interfaceClauseDatabaseInterface
- Returns:
- the number of clauses in the database
-
backjump
public void backjump(int level) tells all databases to backjump at this level- Specified by:
backjump
in interfaceClauseDatabaseInterface
- Parameters:
level
- the level to backjump to
-
assertLiteral
public final void assertLiteral(int literal) tells all databases that the literal is set, for unit propagation. Stops when all databases are informed, or the solver has reached a stop-state- Specified by:
assertLiteral
in interfaceClauseDatabaseInterface
- Parameters:
literal
- the literal
-
uniqueIdToDb
public final int uniqueIdToDb(int clauseId) returns the ClausesDatabase associated with this clauseId- Parameters:
clauseId
- a unique clause Id- Returns:
- the index of the ClausesDatabase that contains the clause
-
uniqueIdToIndex
public final int uniqueIdToIndex(int clauseId) Removes the database index of the clause, to get a real clause index. The normal way to use it is together with getClausesDatabase(), so that we have both the good database and the real id of the clause- Parameters:
clauseId
- the unique clauseId- Returns:
- the clause index in the database
-
indexesToUniqueId
public final int indexesToUniqueId(int clauseIndex, int databaseIndex) It gets a unique id from a clause index, relative to a database, and a database index.- Parameters:
clauseIndex
- clause indexdatabaseIndex
- database index- Returns:
- unique id from a clause index
-
toString
-
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
Description copied from interface:ClauseDatabaseInterface
It writes the clauses of the databases in cnf format to the specified writer.- Specified by:
toCNF
in interfaceClauseDatabaseInterface
- Parameters:
output
- the output writer to which all the clauses will be written to.- Throws:
IOException
- execption from java.io package
-