Class UnaryClausesDatabase
- All Implemented Interfaces:
ClauseDatabaseInterface
,SolverComponent
- Version:
- 4.8
-
Field Summary
FieldsModifier and TypeFieldDescriptionprivate int[]
private int
private static final int
TODO: Radek, just curiousprivate int
Fields inherited from class org.jacop.jasat.core.clauses.AbstractClausesDatabase
CLAUSE_RATE_AVERAGE, CLAUSE_RATE_I_WANT_THIS_CLAUSE, CLAUSE_RATE_LOW, CLAUSE_RATE_UNSUPPORTED, CLAUSE_RATE_WELL_SUPPORTED, core, databaseIndex, dbStore, MINIMUM_VAR_WATCH_SIZE, pool, trail, watchLists
-
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescriptionint
addClause
(int[] clause, boolean isModel) TODO: Radek,void
assertLiteral
(int literal) It informs the ClausesDatabase that this literal is set, so that it can perform unit propagation.void
backjump
(int level) Do everything needed to return to the given level.boolean
canRemove
(int clauseId) It tells if the implementation of ClausesDatabase can remove clauses or notint
rateThisClause
(int[] clause) Indicates how much this database is optimized for this clause.void
removeClause
(int clauseId) It removes the clause which unique ID is @param clauseId.resolutionWith
(int clauseId, MapClause clause) It returns the clause obtained by resolution between clauseIndex and clause.int
size()
number of clauses in the databasevoid
toCNF
(BufferedWriter output) It creates a CNF description of the clauses stored in this database.prints the content of the database in a nice way, each line being prefixed withMethods inherited from class org.jacop.jasat.core.clauses.AbstractClausesDatabase
addWatch, doesWatch, ensureWatch, getDatabaseIndex, indexToUniqueId, initialize, removeWatch, setDatabaseIndex, swap, toString, uniqueIdToIndex
-
Field Details
-
INITIAL_SIZE
private static final int INITIAL_SIZETODO: Radek, just curioushow is the conflict raised by this database? how is the propagation done? After clauses are added, how is the unit propagation taking place?
=> conflicts are only raised when a clause is added, because either we propagate the only literal of the clause, either it is false (=> conflict) However, a good question is: what if we add such a clause at level > 0 and some backjump goes under this level, maybe we should watch literals after all. ==> FIXME
Is the addClause a right place to do above? Would it cause troubles for consistency of state of different components?
- See Also:
-
clauses
private int[] clauses -
currentIndex
private int currentIndex -
numRemoved
private int numRemoved
-
-
Constructor Details
-
UnaryClausesDatabase
public UnaryClausesDatabase()
-
-
Method Details
-
addClause
public int addClause(int[] clause, boolean isModel) TODO: Radek,why would you bother with having any code for removal when nothing is being actually removed. Why not disallow removal altogether and call it StaticUnaryClausesDatabase?
- Parameters:
clause
- the clause to addisModel
- defined if the clause is model clause- Returns:
- the unique ID referring to the clause
-
removeClause
public void removeClause(int clauseId) Description copied from interface:ClauseDatabaseInterface
It removes the clause which unique ID is @param clauseId.- Parameters:
clauseId
- clause id
-
canRemove
public boolean canRemove(int clauseId) Description copied from interface:ClauseDatabaseInterface
It tells if the implementation of ClausesDatabase can remove clauses or not- Parameters:
clauseId
- the unique Id of the clause- Returns:
- true iff removal of clauses is possible
-
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).- Parameters:
clauseId
- the unique id of the clauseclause
- an explanation clause that is modified by resolution- Returns:
- the clause obtained by resolution
-
backjump
public void backjump(int level) Description copied from interface:ClauseDatabaseInterface
Do everything needed to return to the given level.- Parameters:
level
- the level to return to. Must be < solver.getCurrentLevel().
-
assertLiteral
public void assertLiteral(int literal) Description copied from interface:ClauseDatabaseInterface
It informs the ClausesDatabase that this literal is set, so that it can perform unit propagation.- Parameters:
literal
- the literal that is set
-
rateThisClause
public int rateThisClause(int[] clause) Description copied from class:AbstractClausesDatabase
Indicates how much this database is optimized for this clause. The Database that gives the higher rank will get the clause.- Specified by:
rateThisClause
in classAbstractClausesDatabase
- Parameters:
clause
- a clause to rate- Returns:
- a non negative integer indicating how much the database is interested in this clause
-
toString
Description copied from class:AbstractClausesDatabase
prints the content of the database in a nice way, each line being prefixed with- Overrides:
toString
in classAbstractClausesDatabase
- Parameters:
prefix
- prefix for printed line- Returns:
- a String representation of the database
-
size
public int size()Description copied from class:AbstractClausesDatabase
number of clauses in the database- Specified by:
size
in interfaceClauseDatabaseInterface
- Specified by:
size
in classAbstractClausesDatabase
- Returns:
- the number of clauses in the database
-
toCNF
Description copied from class:AbstractClausesDatabase
It creates a CNF description of the clauses stored in this database.- Specified by:
toCNF
in interfaceClauseDatabaseInterface
- Specified by:
toCNF
in classAbstractClausesDatabase
- Parameters:
output
- it specifies the target to which the description will be written.- Throws:
IOException
- execption from java.io package
-