Package org.jacop.jasat.core.clauses

Class DatabasesStore

  • All Implemented Interfaces:
    ClauseDatabaseInterface, SolverComponent
    public final class DatabasesStore
extends java.lang.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.8

    • Constructor Summary

      Constructors 
      Constructor Description
      DatabasesStore()  

    • Method Summary

      All Methods Instance Methods Concrete Methods 
      Modifier and Type Method 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.
      private void initializeMasks()  
      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​(java.io.BufferedWriter output)
      It writes the clauses of the databases in cnf format to the specified writer.
      java.lang.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

      • 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

      • currentIndex

        public int currentIndex

      • core

        public Core core

    • Constructor Detail

      • DatabasesStore

        public DatabasesStore()

    • Method Detail

      • 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 java.lang.String toString()
        Overrides:
        toString in class java.lang.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​(java.io.BufferedWriter output)
           throws java.io.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:
        java.io.IOException - execption from java.io package