Package org.jacop.jasat.core.clauses
Class MapClause
java.lang.Object
org.jacop.jasat.core.clauses.MapClause
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.10
-
Nested Class Summary
Nested Classes -
Field Summary
FieldsModifier and TypeFieldDescriptionint
the literal that will be asserted due to unit propagation of the conflict clause.int
the level at which backjumping should go due to the explanation clause.the literals of the clause -
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescriptionfinal boolean
addAll
(int[] clause) same as previousfinal boolean
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
Deprecated.boolean
boolean
boolean
isUnsatisfiableIn
(Trail trail) 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[]
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.toString()
returns a nice representation of the clauseMethods 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 Details
-
literals
the literals of the clause -
assertedLiteral
public int assertedLiteralthe literal that will be asserted due to unit propagation of the conflict clause. -
backjumpLevel
public int backjumpLevelthe 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
-
-
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
- Parameters:
trail
- the trail to check- Returns:
- true if all literals of the clause are false in the trail
-
isUnitIn
- 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
-
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
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.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
returns a nice representation of the clause -
clear
public void clear()clear the clause, ie. removes all literals -
addAll
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
(slow) iterate over literals of the clause
-