NanoByte SAT Solver
Public Member Functions | Static Public Member Functions | Public Attributes | List of all members
NanoByte.SatSolver.Clause< T > Class Template Reference

A Boolean Clause. Consists of a set of Literal<T>s of which at least one must be true. More...

Inheritance diagram for NanoByte.SatSolver.Clause< T >:

Public Member Functions

 Clause ()
 Creates an empty Clause. More...
 
 Clause (IEnumerable< Literal< T >> literals)
 Creates a Clause consisting the specified literals . More...
 
Clause< T > Without (Literal< T > literal)
 Returns a negated copy of this Clause without the specified literal . More...
 
override string ToString ()
 
bool Equals (Clause< T > other)
 
override bool Equals (object obj)
 
override int GetHashCode ()
 

Static Public Member Functions

static Clause< T > operator| (Clause< T > clause, Literal< T > literal)
 Creates a Clause<T> consisting of all Literals from an existing Clause plus an additional Literal<T>. More...
 
static Clause< T > operator| (Literal< T > literal, Clause< T > clause)
 Creates a Clause<T> consisting of all Literals from an existing Clause plus an additional Literal<T>. More...
 
static Formula< T > operator & (Clause< T > clause1, Clause< T > clause2)
 Creates a Formula<T> consisting of two Clause<T>s. More...
 

Public Attributes

bool IsEmpty => Count == 0
 Indicates whether this Clause is empty and therefore unsatisfiable. More...
 
bool IsUnit => Count == 1
 Indicates whether this is a Unit Clause, i.e. contains exactly one Literal. More...
 

Detailed Description

A Boolean Clause. Consists of a set of Literal<T>s of which at least one must be true.

Template Parameters
TThe underlying type used to identify/compare Literals.
Type Constraints
T :IEquatable<T> 

Constructor & Destructor Documentation

◆ Clause() [1/2]

Creates an empty Clause.

◆ Clause() [2/2]

NanoByte.SatSolver.Clause< T >.Clause ( IEnumerable< Literal< T >>  literals)
inline

Creates a Clause consisting the specified literals .

Member Function Documentation

◆ operator &()

static Formula<T> NanoByte.SatSolver.Clause< T >.operator & ( Clause< T >  clause1,
Clause< T >  clause2 
)
static

Creates a Formula<T> consisting of two Clause<T>s.

Parameters
clause1The first Clause.
clause2The second Clause.

◆ operator|() [1/2]

static Clause<T> NanoByte.SatSolver.Clause< T >.operator| ( Clause< T >  clause,
Literal< T >  literal 
)
static

Creates a Clause<T> consisting of all Literals from an existing Clause plus an additional Literal<T>.

Parameters
clauseThe existing Clause.
literalThe additional Literal.

◆ operator|() [2/2]

static Clause<T> NanoByte.SatSolver.Clause< T >.operator| ( Literal< T >  literal,
Clause< T >  clause 
)
static

Creates a Clause<T> consisting of all Literals from an existing Clause plus an additional Literal<T>.

Parameters
literalThe additional Literal.
clauseThe existing Clause.

◆ Without()

Clause<T> NanoByte.SatSolver.Clause< T >.Without ( Literal< T >  literal)

Returns a negated copy of this Clause without the specified literal .

Member Data Documentation

◆ IsEmpty

bool NanoByte.SatSolver.Clause< T >.IsEmpty => Count == 0

Indicates whether this Clause is empty and therefore unsatisfiable.

◆ IsUnit

bool NanoByte.SatSolver.Clause< T >.IsUnit => Count == 1

Indicates whether this is a Unit Clause, i.e. contains exactly one Literal.


The documentation for this class was generated from the following file: