Package eu.bandm.tools.dpll
Class SAT.Form<P>
- All Implemented Interfaces:
Iterable<SAT.Clause<P>>
,Collection<SAT.Clause<P>>
Conjunction of clauses.
Clauses are accessible via the unmodifiable collection interface.
-
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescription(package private) static <P> SAT.Form<P>
and
(SAT.Clause<P>... cs) (package private) static <P> SAT.Form<P>
and
(SAT.Clause<P> first, SAT.Form<P> rest) (package private) static <P> SAT.Form<P>
and
(SAT.Literal<? extends P> first, SAT.Form<P> rest) (package private) static <P> SAT.Form<P>
and
(Collection<? extends SAT.Clause<P>> cs) 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.nextUnit()
propagate
(SAT.Literal<? extends P> lit) (package private) abstract Set<SAT.Literal<? extends P>>
pure()
int
score()
(package private) abstract Iterable<SAT.Clause<P>>
units()
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, toArray
-
Constructor Details
-
Form
protected Form()
-
-
Method Details
-
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
View literals occurring in this formula.- Returns:
- an unmodifiable enumeration of literals in all clauses of this formula, in textual order and with duplicates.
-
score
public int score() -
units
-
pure
-
propagate
-
nextUnit
-
and
-
and
-
and
-
and
-