DatabasesStore (JaCoP 4.9.0 API)

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

Author:

Simon Cruanes and Radoslaw Szymanek

Field Summary

Fields
Modifier and Type Field and Description

Core core

int currentIndex

AbstractClausesDatabase[] databases

Fields
Modifier and Type	Field and Description
`Core`	`core`
`int`	`currentIndex`
`AbstractClausesDatabase[]`	`databases`

Constructor Summary

Constructors
Constructor and Description

DatabasesStore()

Constructors
Constructor and Description
`DatabasesStore()`

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`int`	`addClause(int[] clause, boolean isModelClause)` It adds a clause to the database.
`void`	`addDatabase(AbstractClausesDatabase database)` Adds a ClausesDatabase to the Store
`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 level
`boolean`	`canRemove(int clauseId)` It tells if the implementation of ClausesDatabase can remove clauses or not
`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.
`void`	`removeClause(int clauseId)` removes this clause from the database it belongs to.
`MapClause`	`resolutionWith(int clauseId, MapClause clause)` It returns the clause obtained by resolution between clauseIndex and clause.
`int`	`size()` the number of clauses in all databases
`void`	`toCNF(BufferedWriter output)` It writes the clauses of the databases in cnf format to the specified writer.
`String`	`toString()`
`int`	`uniqueIdToDb(int clauseId)` returns the ClausesDatabase associated with this clauseId
`int`	`uniqueIdToIndex(int clauseId)` Removes the database index of the clause, to get a real clause index.

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

- Field Detail
  - databases
```
public AbstractClausesDatabase[] databases
```
  - currentIndex
```
public int currentIndex
```
  - core
```
public Core core
```
- Constructor Detail
  - DatabasesStore
```
public DatabasesStore()
```
- Method Detail
  - 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 interface ClauseDatabaseInterface
    
    Parameters:
    
    clause - the clause to add
    
    isModelClause - 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 interface ClauseDatabaseInterface
    
    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 interface ClauseDatabaseInterface
    
    Parameters:
    
    clauseId - the id of the clause to be deleted
  - resolutionWith
```
public MapClause resolutionWith(int clauseId,
                                MapClause clause)
```
    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 interface ClauseDatabaseInterface
    
    Parameters:
    
    clauseId - the unique id of the clause
    
    clause - an explanation clause that is modified by resolution
    
    Returns:
    
    the clause obtained by resolution
  - addDatabase
```
public void addDatabase(AbstractClausesDatabase database)
```
    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 interface ClauseDatabaseInterface
    
    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 interface ClauseDatabaseInterface
    
    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 interface ClauseDatabaseInterface
    
    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 index
    
    databaseIndex - database index
    
    Returns:
    
    unique id from a clause index
  - toString
```
public String toString()
```
    Overrides:
    
    toString in class Object
  - initialize
```
public 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 void toCNF(BufferedWriter output)
           throws IOException
```
    Description copied from interface: ClauseDatabaseInterface
    
    It writes the clauses of the databases in cnf format to the specified writer.
    
    Specified by:
    
    toCNF in interface ClauseDatabaseInterface
    
    Parameters:
    
    output - the output writer to which all the clauses will be written to.
    
    Throws:
    
    IOException - execption from java.io package

Class DatabasesStore

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Field Detail

databases

currentIndex

core

Constructor Detail

DatabasesStore

Method Detail

addClause

canRemove

removeClause

resolutionWith

addDatabase

size

backjump

assertLiteral

uniqueIdToDb

uniqueIdToIndex

indexesToUniqueId

toString

initialize

toCNF