Interface Clause

All Superinterfaces:

Iterable<Literal>

public interface Clause
extends Iterable<Literal>

The Clause interface represents a logical clause, which is a disjunction (OR) of literals in propositional logic. Clauses are fundamental components in SAT solvers and are used to encode constraints and logical formulas.

Author:

Mathias Hofer

Method Summary

Modifier and Type	Method	Description
static Clause	of()	Creates a clause with no literals.
static Clause	of(Collection<? extends Literal> literals)	Creates a clause from a collection of literals.
static Clause	of(Collection<? extends Literal> literals, Literal l)	Creates a clause from a collection of literals and an additional literal.
static Clause	of(Collection<? extends Literal> literals, Literal l1, Literal l2)	Creates a clause from a collection of literals and two additional literals.
static Clause	of(Collection<? extends Literal> literals, Literal l1, Literal l2, Literal l3)	Creates a clause from a collection of literals and three additional literals.
static Clause	of(Clause c, Literal l)	Creates a clause by extending an existing clause with an additional literal.
static Clause	of(Literal l)	Creates a clause with a single literal.
static Clause	of(Literal l1, Literal l2)	Creates a clause with two literals.
static Clause	of(Literal l1, Literal l2, Literal l3)	Creates a clause with three literals.
int	size()	Returns the number of literals in this clause.
Stream<Literal>	stream()	Returns a stream of literals contained in this clause.

Methods inherited from interface java.lang.Iterable

forEach, iterator, spliterator

Method Details

stream

Stream<Literal> stream()

Returns a stream of literals contained in this clause.

Returns:

a Stream of literals in the clause

size

int size()

Returns the number of literals in this clause.

Returns:

the size of the clause

of

static Clause of()

Creates a clause with no literals. This represents an empty clause.

Returns:

a clause with no literals

of

static Clause of(Literal l)

Creates a clause with a single literal.

Parameters:

l - the single literal

Returns:

a clause containing the given literal

of

static Clause of(Literal l1,
 Literal l2)

Creates a clause with two literals.

Parameters:

l1 - the first literal

l2 - the second literal

Returns:

a clause containing the given literals

of

static Clause of(Literal l1,
 Literal l2,
 Literal l3)

Creates a clause with three literals.

Parameters:

l1 - the first literal

l2 - the second literal

l3 - the third literal

Returns:

a clause containing the given literals

of

static Clause of(Clause c,
 Literal l)

Creates a clause by extending an existing clause with an additional literal.

Parameters:

c - the existing clause

l - the additional literal

Returns:

a new clause that is the extension of the given clause with the additional literal

of

static Clause of(Collection<? extends Literal> literals)

Creates a clause from a collection of literals.

Parameters:

literals - a collection of literals

Returns:

a clause containing the literals from the collection

of

static Clause of(Collection<? extends Literal> literals,
 Literal l)

Creates a clause from a collection of literals and an additional literal.

Parameters:

literals - a collection of literals

l - the additional literal

Returns:

a new clause containing the literals from the collection plus the additional literal

of

static Clause of(Collection<? extends Literal> literals,
 Literal l1,
 Literal l2)

Creates a clause from a collection of literals and two additional literals.

Parameters:

literals - a collection of literals

l1 - the first additional literal

l2 - the second additional literal

Returns:

a new clause containing the literals from the collection plus the additional literals

of

static Clause of(Collection<? extends Literal> literals,
 Literal l1,
 Literal l2,
 Literal l3)

Creates a clause from a collection of literals and three additional literals.

Parameters:

literals - a collection of literals

l1 - the first additional literal

l2 - the second additional literal

l3 - the third additional literal

Returns:

a new clause containing the literals from the collection plus the additional literals