Package org.jacop.jasat.core

Class Trail

  • All Implemented Interfaces:
    SolverComponent
    public final class Trail
extends java.lang.Object
implements SolverComponent
    It stores the current variables status (affected or not, with which value and explanation). It values of variables are packed in an int, together with the level at which they were asserted.
    Version:
    4.8

    • Constructor Summary

      Constructors 
      Constructor Description
      Trail()  

    • Method Summary

      All Methods Instance Methods Concrete Methods 
      Modifier and Type Method Description
      void addVariable​(int var)
      It adds a variable to the trail.
      private void assertLit​(int var, int literal, int level, boolean asserted)
      real assignment of literal at level
      void assertLiteral​(int literal, int level)
      Sets a literal, that is, a variable signed with its value (> 0 for true, < 0 for false).
      void assertLiteral​(int literal, int level, int causeId)
      Sets a literal, with an explanation clause.
      void backjump​(int level)
      It tells the trail to return to given level.
      void ensureCapacity​(int numVar)
      It ensures the trail can contain @param numVar variables
      int getExplanation​(int var)
      It returns the index of the clause that caused this variable to be set
      int getLevel​(int var)
      It returns the level at which @param var has been set.
      void initialize​(Core core)
      to be called before any use of the trail
      boolean isAsserted​(int var)
      It returns information if a variable was asserted or only propagated.
      boolean isSet​(int var)
      predicate which meaning is : is this variable set or unknown ?
      int size()
      returns the number of currently set variables
      java.lang.String toString()  
      void unset​(int var)
      It unsets the given variable.

      • Methods inherited from class java.lang.Object

        clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

    • Field Detail

      • values

        public int[] values

      • explanations

        public int[] explanations

      • assertionStack

        public IntStack assertionStack

      • levels

        private int[] levels

      • ASSERTED_MASK

        private int ASSERTED_MASK

      • LEVEL_MASK

        private int LEVEL_MASK

    • Constructor Detail

      • Trail

        public Trail()

    • Method Detail

      • addVariable

        public void addVariable​(int var)
        It adds a variable to the trail.
        Parameters:
        var - the variable

      • ensureCapacity

        public void ensureCapacity​(int numVar)
        It ensures the trail can contain @param numVar variables
        Parameters:
        numVar - the number of variables the trail must be able to contain

      • assertLiteral

        public void assertLiteral​(int literal,
                          int level)
        Sets a literal, that is, a variable signed with its value (> 0 for true, < 0 for false). This must be used only for asserted values, not the ones propagated from unit clauses.
        Parameters:
        literal - the literal
        level - the current level

      • assertLiteral

        public void assertLiteral​(int literal,
                          int level,
                          int causeId)
        Sets a literal, with an explanation clause. For unit propagation only.
        Parameters:
        literal - the literal (non nul relative number)
        level - the level at which this assertion occurs
        causeId - the ID of the clause that triggered this assertion

      • assertLit

        private void assertLit​(int var,
                       int literal,
                       int level,
                       boolean asserted)
        real assignment of literal at level

      • unset

        public void unset​(int var)
        It unsets the given variable. Does not take car of assertionLevels !
        Parameters:
        var - the variable to unset. Must be positive.

      • backjump

        public void backjump​(int level)
        It tells the trail to return to given level. It will therefore erase all assertion strictly above this level. Literals asserted at @param level will be kept.
        Parameters:
        level - the level to jump to.

      • getLevel

        public int getLevel​(int var)
        It returns the level at which @param var has been set. @param var *must* be set, otherwise this will fail.
        Parameters:
        var - the literal which level we wish to know
        Returns:
        the level

      • getExplanation

        public int getExplanation​(int var)
        It returns the index of the clause that caused this variable to be set
        Parameters:
        var - the literal. Must be set.
        Returns:
        an index if there was an explanation, 0 otherwise

      • isAsserted

        public boolean isAsserted​(int var)
        It returns information if a variable was asserted or only propagated.
        Parameters:
        var - the variable
        Returns:
        true if the variable was asserted

      • isSet

        public boolean isSet​(int var)
        predicate which meaning is : is this variable set or unknown ?
        Parameters:
        var - the variable, must be positive
        Returns:
        true if the variable is set.

      • size

        public int size()
        returns the number of currently set variables
        Returns:
        the number of currently set variables

      • toString

        public java.lang.String toString()
        Overrides:
        toString in class java.lang.Object

      • initialize

        public void initialize​(Core core)
        to be called before any use of the trail
        Specified by:
        initialize in interface SolverComponent
        Parameters:
        core - the Solver instance