Module splr::cdb

Module cdb provides Clause object and its manager ClauseDB.

Re-exports

• pub use self::property::*;

Modules

• property

Structs

• BinaryLinkDB
  storage with mapper to ClauseId of binary links
• CertificationStore
  Struct for saving UNSAT certification
• Clause
  A representation of ‘clause’
• ClauseDB
  Clause database
• ClauseId
  Clause identifier, or clause index, starting with one. Note: ids are re-used after ‘garbage collection’.

Enums

• ReductionType

Traits

• ClauseDBIF
  API for clause management like reduce, new_clause, remove_clause, and so on.
• ClauseIF
  API for Clause, providing literal accessors.
• ClauseIdIF
  API for Clause Id.
• StochasticLocalSearchIF
• VivifyIF

Type Aliases

• BinaryLinkList
  storage of binary links