Class Trail

java.lang.Object
org.jacop.jasat.core.Trail
All Implemented Interfaces:
SolverComponent

public final class Trail extends 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.9
  • Field Summary

    Fields
    Modifier and Type
    Field
    Description
    private int
     
     
    int[]
     
    private int
     
    private int[]
     
     
    int[]
     
  • Constructor Summary

    Constructors
    Constructor
    Description
     
  • Method Summary

    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
    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
    returns the number of currently set variables
     
    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 Details

    • pool

      public MemoryPool pool
    • 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 Details

    • Trail

      public Trail()
  • Method Details

    • 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 String toString()
      Overrides:
      toString in class 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