Documentation

Clause type

The makeClause function constructs a clause from a list of literals. Clauses are sorted and duplicate literals are removed. Furthermore occurrences of 0 are removed ( 0 is not a valid literal).

The isEmpty function return True is the clause contains no literal.

The size function returns the number of literals in the clause.

The isUnit function return True if the clause contains exactly one literal.