Class Clause<T>
A Boolean Clause. Consists of a set of Literal<T>s of which at least one must be true.
Assembly: NanoByte.SatSolver.dll
Syntax
public class Clause<T> : HashSet<Literal<T>> where T : IEquatable<T>
Type Parameters
| Name |
Description |
| T |
The underlying type used to identify/compare Literals.
|
Constructors
Clause()
Declaration
Clause(IEnumerable<Literal<T>>)
Creates a Clause consisting the specified literals.
Declaration
public Clause(IEnumerable<Literal<T>> literals)
Parameters
Properties
IsEmpty
Indicates whether this Clause is empty and therefore unsatisfiable.
Declaration
public bool IsEmpty { get; }
Property Value
IsUnit
Indicates whether this is a Unit Clause, i.e. contains exactly one Literal.
Declaration
public bool IsUnit { get; }
Property Value
Methods
Equals(Clause<T>)
Declaration
public bool Equals(Clause<T> other)
Parameters
| Type |
Name |
Description |
| Clause<T> |
other |
|
Returns
Equals(Object)
Declaration
public override bool Equals(object obj)
Parameters
| Type |
Name |
Description |
| Object |
obj |
|
Returns
GetHashCode()
Declaration
public override int GetHashCode()
Returns
ToString()
Declaration
public override string ToString()
Returns
Without(Literal<T>)
Returns a negated copy of this Clause without the specified literal.
Declaration
public Clause<T> Without(Literal<T> literal)
Parameters
| Type |
Name |
Description |
| Literal<T> |
literal |
|
Returns
Operators
BitwiseAnd(Clause<T>, Clause<T>)
Declaration
public static Formula<T> operator &(Clause<T> clause1, Clause<T> clause2)
Parameters
| Type |
Name |
Description |
| Clause<T> |
clause1 |
The first Clause.
|
| Clause<T> |
clause2 |
The second Clause.
|
Returns
BitwiseOr(Clause<T>, Literal<T>)
Creates a Clause<T> consisting of all Literals from an existing Clause plus an additional Literal<T>.
Declaration
public static Clause<T> operator |(Clause<T> clause, Literal<T> literal)
Parameters
| Type |
Name |
Description |
| Clause<T> |
clause |
The existing Clause.
|
| Literal<T> |
literal |
The additional Literal.
|
Returns
BitwiseOr(Literal<T>, Clause<T>)
Creates a Clause<T> consisting of all Literals from an existing Clause plus an additional Literal<T>.
Declaration
public static Clause<T> operator |(Literal<T> literal, Clause<T> clause)
Parameters
| Type |
Name |
Description |
| Literal<T> |
literal |
The additional Literal.
|
| Clause<T> |
clause |
The existing Clause.
|
Returns
Implements