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

  • 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

      public AbstractClausesDatabase[] databases

    • currentIndex

      public int currentIndex

    • core

      public Core 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 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