Module splr::types

Module types provides various building blocks, including some common traits.

Re-exports

• pub use crate::assign::AssignReason;
• pub use crate::cdb::Clause;
• pub use crate::cdb::ClauseDB;
• pub use crate::cdb::ClauseIF;
• pub use crate::cdb::ClauseId;
• pub use crate::cdb::ClauseIdIF;
• pub use crate::config::Config;
• pub use crate::solver::SolverEvent;
• pub use crate::primitive::ema::*;
• pub use crate::primitive::luby::*;

Structs

• CNFDescription
  Data storage about a problem.
• CNFReader
  A wrapper structure to make a CNFDescription from a file. To make CNFDescription clone-able, a BufReader should be separated from it. If you want to make a CNFDescription which isn’t connected to a file, just call CNFDescription::default() directly.
• FlagClause
  Misc flags used by Clause.
• FlagVar
  Misc flags used by Var.
• Lit
  Literal encoded on u32 as:
• Logger
• OrderedProxy

Enums

• CNFIndicator
  CNF locator
• RefClause
• SolverError
  Internal errors. Note: returning Result<(), a-singleton> is identical to returning bool.

Traits

• ActivityIF
  API for reward based activity management.
• Delete
  API for O(n) deletion from a list, providing delete_unstable.
• FlagIF
  API for object properties.
• Instantiate
  API for object instantiation based on Configuration and CNFDescription. This is implemented by all the Splr modules except Configuration and CNFDescription.
• LitIF
  API for Literal like vi, as_bool, is_none and so on.
• PropertyDereference
• PropertyReference
  API for accessing internal data in a module. For example, State::progress needs to access misc parameters and statistics, which, however, should be used locally in the defining modules. To avoid to make them public, we define a generic accessor or exporter here.

Functions

• i32s
  convert literals to [i32] (for debug).

Type Aliases

• ConflictContext
  Capture a conflict
• DecisionLevel
  Decision Level Representation.
• MaybeInconsistent
  A Return type used by solver functions.
• PropagationResult
  Return type of unit propagation
• VarId
  ‘Variable’ identifier or ‘variable’ index, starting with one. Implementation note: NonZeroUsize can be used but requires a lot of changes. The current abstraction is incomplete.