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

  • Field Details

    • CLAUSE_RATE_UNSUPPORTED

      protected static final int CLAUSE_RATE_UNSUPPORTED
      See Also:

    • CLAUSE_RATE_LOW

      protected static final int CLAUSE_RATE_LOW
      See Also:

    • CLAUSE_RATE_AVERAGE

      protected static final int CLAUSE_RATE_AVERAGE
      See Also:

    • CLAUSE_RATE_WELL_SUPPORTED

      protected static final int CLAUSE_RATE_WELL_SUPPORTED
      See Also:

    • 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:

    • 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 Details

    • AbstractClausesDatabase

      public AbstractClausesDatabase()

  • Method Details

    • 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