Package org.jacop.jasat.core.clauses
Class MapClause
- java.lang.Object
-
- org.jacop.jasat.core.clauses.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.7
-
-
Nested Class Summary
Nested Classes Modifier and Type Class Description private class
MapClause.ClauseIterator
-
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
-
Method Summary
All Methods Instance Methods Concrete Methods Deprecated Methods Modifier and Type Method Description boolean
addAll(int[] clause)
same as previousboolean
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 presentboolean
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 clausevoid
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 clauseint[]
toIntArray()
allocates an int[] and dumps the clause inprivate 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
-
-
-
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.
-
-
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 clausetrail
- 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 classjava.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 interfacejava.lang.Iterable<java.lang.Integer>
-
-