Package org.jacop.jasat.core.clauses

Class MapClause

  • All Implemented Interfaces:
    java.lang.Iterable<java.lang.Integer>
    public final class MapClause
extends java.lang.Object
implements java.lang.Iterable<java.lang.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 Summary

      Fields 
      Modifier and Type Field Description
      int assertedLiteral
      the literal that will be asserted due to unit propagation of the conflict clause.
      int backjumpLevel
      the level at which backjumping should go due to the explanation clause.
      java.util.Map<java.lang.Integer,​java.lang.Boolean> literals
      the literals of the clause

    • Constructor Summary

      Constructors 
      Constructor Description
      MapClause()
      creates an empty clause
      MapClause​(int[] clause)
      initializes the SetClause with given int[] clause
      MapClause​(java.lang.Iterable<java.lang.Integer> clause)  

    • Method Summary

      All Methods Instance Methods Concrete Methods Deprecated Methods 
      Modifier and Type Method Description
      boolean addAll​(int[] clause)
      same as previous
      boolean addAll​(java.lang.Iterable<java.lang.Integer> clause)
      adds all elements of clause to the SetClause, performing resolution.
      boolean addLiteral​(int literal)
      Add a literal to the clause, with resolution.
      void clear()
      clear the clause, ie.
      boolean containsLiteral​(int literal)
      Predicate which is true iff the literal is present.
      boolean containsVariable​(int var)
      Predicate which is true iff the variable or its opposite is present
      boolean isEmpty()  
      boolean isTrivial()
      Deprecated.
      boolean isUnitIn​(int literal, Trail trail)  
      boolean isUnitIn​(Trail trail)  
      boolean isUnsatisfiableIn​(Trail trail)  
      java.util.Iterator<java.lang.Integer> iterator()
      (slow) iterate over literals of the clause
      void partialResolveWith​(int literal)
      If variable specified by the literal does not exists in this clause then literal is added.
      boolean removeLiteral​(int literal)
      It removes the literal, if it is in the clause.
      int size()
      returns the number of literals in the clause
      int[] toIntArray()
      allocates an int[] and dumps the clause in
      private int[] toIntArray​(int[] array)  
      int[] toIntArray​(MemoryPool pool)
      converts the clause to an int[] suitable for the efficient clauses pool implementations.
      java.lang.String toString()
      returns a nice representation of the clause

      • Methods inherited from class java.lang.Object

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

      • Methods inherited from interface java.lang.Iterable

        forEach, spliterator

    • Field Detail

      • literals

        public java.util.Map<java.lang.Integer,​java.lang.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 Detail

      • 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​(java.lang.Iterable<java.lang.Integer> clause)

    • Method Detail

      • 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 java.lang.String toString()
        returns a nice representation of the clause
        Overrides:
        toString in class java.lang.Object

      • clear

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

      • addAll

        public final boolean addAll​(java.lang.Iterable<java.lang.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 java.util.Iterator<java.lang.Integer> iterator()
        (slow) iterate over literals of the clause
        Specified by:
        iterator in interface java.lang.Iterable<java.lang.Integer>