Class MapClause

java.lang.Object
org.jacop.jasat.core.clauses.MapClause
All Implemented Interfaces:
Iterable<Integer>

public final class MapClause extends Object implements Iterable<Integer>
A clause used for resolution, easily modifiable several times, and that can then be converted to an int[].

This represents a *single* clause.

Version:
4.8
  • Field Details

    • literals

      public Map<Integer,Boolean> literals
      the literals of the clause
    • assertedLiteral

      public int assertedLiteral
      the literal that will be asserted due to unit propagation of the conflict clause.
    • backjumpLevel

      public int backjumpLevel
      the level at which backjumping should go due to the explanation clause.
  • Constructor Details

    • MapClause

      public MapClause()
      creates an empty clause
    • MapClause

      public MapClause(int[] clause)
      initializes the SetClause with given int[] clause
      Parameters:
      clause - the clause
    • MapClause

      public MapClause(Iterable<Integer> clause)
  • Method Details

    • addLiteral

      public boolean addLiteral(int literal)
      Add a literal to the clause, with resolution. If the opposite literal (same variable, opposite sign) is in the clause, it returns true.
      Parameters:
      literal - the literal to be added from another clause
      Returns:
      true if the opposite literal is in the clause, false otherwise
    • removeLiteral

      public boolean removeLiteral(int literal)
      It removes the literal, if it is in the clause. It uses a HashMap to obtain constant time remove time.
      Parameters:
      literal - the literal to remove (sign sensitive)
      Returns:
      true if the literal was present (and removed), false otherwise
    • partialResolveWith

      public void partialResolveWith(int literal)
      If variable specified by the literal does not exists in this clause then literal is added. If variable exists as the opposite literal then the opposite literal is removed and nothing is added.
      Parameters:
      literal - the literal to be added
    • containsLiteral

      public boolean containsLiteral(int literal)
      Predicate which is true iff the literal is present.
      Parameters:
      literal - a literal
      Returns:
      true if the literal (and not its opposite) is in the clause
    • containsVariable

      public boolean containsVariable(int var)
      Predicate which is true iff the variable or its opposite is present
      Parameters:
      var - a variable (> 0)
      Returns:
      true if the literal or its opposite is in the clause
    • isUnsatisfiableIn

      public boolean isUnsatisfiableIn(Trail trail)
      Parameters:
      trail - the trail to check
      Returns:
      true if all literals of the clause are false in the trail
    • isUnitIn

      public boolean isUnitIn(int literal, Trail trail)
      Parameters:
      literal - the only satisfiable literal in the clause
      trail - the trail for the literal
      Returns:
      true if the clause is unit with only @param literal not set
    • isUnitIn

      public boolean isUnitIn(Trail trail)
    • isEmpty

      public boolean isEmpty()
      Returns:
      true if the clause is empty
    • size

      public int size()
      returns the number of literals in the clause
      Returns:
      the number of literals in the clause
    • toIntArray

      public int[] toIntArray(MemoryPool pool)
      converts the clause to an int[] suitable for the efficient clauses pool implementations. The clause must not be empty.
      Parameters:
      pool - the pool for clause implementation
      Returns:
      an equivalent clause
    • toIntArray

      private int[] toIntArray(int[] array)
    • toIntArray

      public int[] toIntArray()
      allocates an int[] and dumps the clause in
      Returns:
      a new int[] representing this clause
    • isTrivial

      @Deprecated public boolean isTrivial()
      Deprecated.
      true iff the clause is trivial (contains a literal and its opposite). Now, by construction, a MapClause cannot be trivial
      Returns:
      true iff the clause is trivial
    • toString

      public String toString()
      returns a nice representation of the clause
      Overrides:
      toString in class Object
    • clear

      public void clear()
      clear the clause, ie. removes all literals
    • addAll

      public final boolean addAll(Iterable<Integer> clause)
      adds all elements of clause to the SetClause, performing resolution.
      Parameters:
      clause - the literals to add
      Returns:
      true if the resulting SetClause is trivial (tautology), false otherwise
    • addAll

      public final boolean addAll(int[] clause)
      same as previous
      Parameters:
      clause - clause the literals to add
      Returns:
      true if the resulting SetClause is trivial (tautology), false otherwise
    • iterator

      public Iterator<Integer> iterator()
      (slow) iterate over literals of the clause
      Specified by:
      iterator in interface Iterable<Integer>