eu.bandm.tools.util

Class SAT.Clause<P>

java.lang.Object

java.util.AbstractCollection<SAT.Literal<? extends P>>

eu.bandm.tools.util.SAT.Clause<P>

All Implemented Interfaces:

Iterable<SAT.Literal<? extends P>>, Collection<SAT.Literal<? extends P>>

Enclosing class:

SAT<P>

protected abstract static class SAT.Clause<P>
extends AbstractCollection<SAT.Literal<? extends P>>

Disjunction of literals.

Literals are accessible via the unmodifiable collection interface.

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	Clause()

Method Summary

Modifier and Type	Method and Description
abstract SAT.Literal<? extends P>	getUnit() Extract unit literal.
abstract boolean	isFalse() Check whether this clause is unsatisfiable.
abstract boolean	isTrue() Check whether this clause is tautological.
abstract boolean	isUnit() Check whether this clause is unitary.

Methods inherited from class java.util.AbstractCollection

add, addAll, clear, contains, containsAll, isEmpty, iterator, remove, removeAll, retainAll, size, toArray, toArray, toString

Methods inherited from class java.lang.Object

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

Methods inherited from interface java.util.Collection

equals, hashCode, parallelStream, removeIf, spliterator, stream

Methods inherited from interface java.lang.Iterable

forEach

Constructor Detail

Clause

protected Clause()

Method Detail

isTrue

public abstract boolean isTrue()

Check whether this clause is tautological.

Returns:

true if this clause is true under all interpretations; false otherwise.

isFalse

public abstract boolean isFalse()

Check whether this clause is unsatisfiable.

Returns:

true if this clause is false under all interpretations; false otherwise.

isUnit

public abstract boolean isUnit()

Check whether this clause is unitary.

Returns:

true if this clause contains exactly one literal; false otherwise.

getUnit

public abstract SAT.Literal<? extends P> getUnit()

Extract unit literal.

Returns:

if this clause contains exactly one literal, it is returned; null otherwise.