Module varisat_checker::clauses

Clause storage (unit and non-unit clauses).

Structs

Clause	Literals and metadata for non-unit clauses.
ClauseLits	Literals of a clause, either inline or an index into a buffer
Clauses	Checker clause storage.
UnitClause	Known unit clauses and metadata.

Enums

DeleteClauseResult	Return type of delete_clause
StoreClauseResult	Return type of store_clause
UnitId	Identifies the origin of a unit clause.

Constants

INLINE_LITS

Functions

add_clause	Adds a clause to the checker.
collect_garbage	Perform a garbage collection if required
delete_clause	Delete a clause from the current formula.
store_clause	Adds a clause to the checker data structures.
store_unit_clause	Adds a unit clause to the checker data structures.