Expand description
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§
- Data storage about a problem.
- 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.
- Misc flags used by
Clause
. - Misc flags used by
Var
. - Literal encoded on
u32
as:
Enums§
- CNF locator
- Internal errors. Note: returning
Result<(), a-singleton>
is identical to returningbool
.
Traits§
- API for reward based activity management.
- API for O(n) deletion from a list, providing
delete_unstable
. - API for object properties.
- API for object instantiation based on
Configuration
andCNFDescription
. This is implemented by all the Splr modules exceptConfiguration
andCNFDescription
. - API for Literal like
vi
,as_bool
,is_none
and so on. - 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§
- convert literals to
[i32]
(for debug).
Type Aliases§
- Capture a conflict
- Decision Level Representation.
- A Return type used by solver functions.
- Return type of unit propagation
- ‘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.