eu.bandm.tools.util

Class SAT.Form<P>

java.lang.Object

java.util.AbstractCollection<SAT.Clause<P>>

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

All Implemented Interfaces:

Iterable<SAT.Clause<P>>, Collection<SAT.Clause<P>>

Enclosing class:

SAT<P>

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

Conjunction of clauses.

Clauses are accessible via the unmodifiable collection interface.

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	Form()

Method Summary

Modifier and Type	Method and Description
abstract boolean	isFalse() Check whether this formula is unsatisfiable.
abstract boolean	isTrue() Check whether this formula is tautological.
abstract Iterable<SAT.Literal<? extends P>>	literals() View literals occurring in this formula.

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

Form

protected Form()

Method Detail

isTrue

public abstract boolean isTrue()

Check whether this formula is tautological.

Returns:

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

isFalse

public abstract boolean isFalse()

Check whether this formula is unsatisfiable.

Returns:

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

literals

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

View literals occurring in this formula.

Returns:

an unmodifiable enumeration of literals in all clauses of this formula, in textual order and with duplicates.