Class ActivityModule

    • Field Detail

      • BUMP_INCREASE_FACTOR

        private int BUMP_INCREASE_FACTOR
      • posActivities

        private int[] posActivities
      • negActivities

        private int[] negActivities
      • activitiesIndex

        private int activitiesIndex
      • currentBumpRate

        private int currentBumpRate
      • rebaseThreshold

        private int rebaseThreshold
      • learntCount

        private int learntCount
      • priorities

        private java.lang.Integer[] priorities
      • prioritiesIndex

        private int prioritiesIndex
      • prioritizedVars

        private java.util.BitSet prioritizedVars
      • conflictCount

        private int conflictCount
      • core

        public Core core
      • comparator

        private final java.util.Comparator<java.lang.Integer> comparator
        compares literals according to their activity. This stands for i > j and not i < j, because we want activities to be sorted in decreasing order
    • Constructor Detail

      • ActivityModule

        public ActivityModule()
    • Method Detail

      • onBackjump

        public void onBackjump​(int oldLevel,
                               int newLevel)
        Description copied from interface: BackjumpListener
        Called when the solver backtracks. It will also be called when the solver restarts.

        components that want to be warned about backjumps should put themselves in Core.backjumpModules.

        Specified by:
        onBackjump in interface BackjumpListener
        Parameters:
        oldLevel - the level at which the solver was before backtracking
        newLevel - the level to which the solver backtracks
      • onRestart

        public void onRestart​(int oldLevel)
        Description copied from interface: BackjumpListener
        called when the solver restarts.

        components that want to be warned about restarts should put themselves in Core.restartModules.

        Specified by:
        onRestart in interface BackjumpListener
        Parameters:
        oldLevel - the level at which the solver was before restarting
      • onConflict

        public void onConflict​(MapClause conflictClause,
                               int level)
        Description copied from interface: ConflictListener
        called when a conflict occurs
        Specified by:
        onConflict in interface ConflictListener
        Parameters:
        conflictClause - the conflict (unsatisfiable) clause
        level - the level at which the conflict occurred
      • sortArray

        public void sortArray()
        sort the priorities array (useful after adding a lot of clauses)
      • onClauseAdd

        public final void onClauseAdd​(int[] clause,
                                      int clauseId,
                                      boolean isModelClause)
        Description copied from interface: ClauseListener
        called when the given clause is added.
        Specified by:
        onClauseAdd in interface ClauseListener
        Parameters:
        clause - the clause
        clauseId - the clause's unique Id
        isModelClause - is this clause a model clause ?
      • onClauseRemoval

        public final void onClauseRemoval​(int clauseId)
        Description copied from interface: ClauseListener
        called when the clause with unique Id @param clauseId is removed
        Specified by:
        onClauseRemoval in interface ClauseListener
        Parameters:
        clauseId - the id
      • getLiteralToAssert

        public final int getLiteralToAssert()
        returns the non-set literal with highest activity, if any
        Returns:
        a non set literal, or 0 if all known literals are set
      • getLiteralActivity

        private final int getLiteralActivity​(int var,
                                             boolean polarity)
        gives activity of a (signed) literal
        Parameters:
        literal - the literal
        Returns:
        the activity of this (variable, polarity)
      • bumpVar

        private final int bumpVar​(int literal)
        code that really performs variable and polarity activity bumping.
        Parameters:
        var - the variable
        Returns:
        the new activity of the variable
      • ensureVarSize

        private final void ensureVarSize​(int var)
      • increaseBumpRate

        private final void increaseBumpRate()
        increases the bump rate, so that recent activity is more important than old activity
      • rebase

        private final void rebase​(int value)
        rebases all values
        Parameters:
        value - the value that just overflowed
      • 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