Class AbstractClausesDatabase

    • Field Detail

      • CLAUSE_RATE_UNSUPPORTED

        protected static final int CLAUSE_RATE_UNSUPPORTED
        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
      • trail

        public Trail trail
      • core

        public Core core
      • 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 java.lang.String toString​(java.lang.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 java.lang.String toString()
        print the content of the Database in a nice way
        Overrides:
        toString in class java.lang.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​(java.io.BufferedWriter output)
                            throws java.io.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:
        java.io.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