MapClause (JaCoP 4.9.0 API)

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.9

Author:

Simon Cruanes and Radoslaw Szymanek

Field Summary

Fields
Modifier and Type	Field and 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.
`Map<Integer,Boolean>`	`literals` the literals of the clause

Constructor Summary

Constructors
Constructor and Description
`MapClause()` creates an empty clause
`MapClause(int[] clause)` initializes the SetClause with given int[] clause
`MapClause(Iterable<Integer> clause)`

Method Summary

All Methods Instance Methods Concrete Methods Deprecated Methods
Modifier and Type	Method and Description
`boolean`	`addAll(int[] clause)` same as previous
`boolean`	`addAll(Iterable<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)`
`Iterator<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
`int[]`	`toIntArray(MemoryPool pool)` converts the clause to an int[] suitable for the efficient clauses pool implementations.
`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 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 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(Iterable<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
```
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>

Class MapClause

Field Summary

Constructor Summary

Method Summary

Methods inherited from class java.lang.Object

Methods inherited from interface java.lang.Iterable

Field Detail

literals

assertedLiteral

backjumpLevel

Constructor Detail

MapClause

MapClause

MapClause

Method Detail

addLiteral

removeLiteral

partialResolveWith

containsLiteral

containsVariable

isUnsatisfiableIn

isUnitIn

isUnitIn

isEmpty

size

toIntArray

toIntArray

isTrivial

toString

clear

addAll

addAll

iterator