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.9

Author:

Simon Cruanes and Radoslaw Szymanek

Field Summary

Fields

Modifier and Type	Field and 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 and Description
AbstractClausesDatabase()

Method Summary

Modifier and Type	Method and Description
protected void	addWatch(int literal, int clauseIndex) adds a watch (var => clause), ie make var watch clause
protected 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 database
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 void	removeWatch(int literal, int clauseIndex) removes the clause from the list of clauses that literal watches
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 database
protected void	swap(int[] clause, int i, int j) swaps the two literals at position i and j in the clause
abstract void	toCNF(BufferedWriter output) It creates a CNF description of the clauses stored in this database.
String	toString() print the content of the Database in a nice way
String	toString(String prefix) prints the content of the database in a nice way, each line being prefixed with
int	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.

Constructor Detail

AbstractClausesDatabase

public AbstractClausesDatabase()

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 check

clauseIndex - 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 literal

clauseIndex - 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 literal

clauseIndex - the clause to remove

size

public abstract int size()

number of clauses in the database

Specified by:

size in interface ClauseDatabaseInterface

Returns:

the number of clauses in the database

toString

public String toString(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 String toString()

print the content of the Database in a nice way

Overrides:

toString in class 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 interface SolverComponent

Parameters:

core - core component to initialize

toCNF

public abstract void toCNF(BufferedWriter output)
                    throws IOException

It creates a CNF description of the clauses stored in this database.

Specified by:

toCNF in interface ClauseDatabaseInterface

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 clause

i - the position (index) of the first literal

j - the position of the second literal