Module splr::types

Crate 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::ClauseIF;

pub use crate::cdb::ClauseId;

pub use crate::config::Config;

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.

Ema

Exponential Moving Average, with a calibrator if feature EMA_calibration is on.

Ema2

Exponential Moving Average pair, with a calibrator if feature EMA_calibration is on.

EmaSU

Ema of Sequence of usize

Flag

Misc flags used by Clause and 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.

Constants

NULL_LIT

a dummy literal.

Traits

ActivityIF

API for reward based activity management.

ClauseIdIF

API for Clause Id.

Delete

API for O(n) deletion from a list, providing delete_unstable.

EmaIF

API for Exponential Moving Average, EMA, like get, reset, update and so on.

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 Definitions

DecisionLevel

Decision Level Representation.

MaybeInconsistent

A Return type used by solver functions.

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.