Module splr::processor

Crate processor implements a simplifier: clause subsumption and var elimination.

• private module eliminate provides var elimination
• private module subsume provides clause subsumption

Example

  use splr::{processor::EliminateIF, solver::Solver, types::Export};
  use std::convert::TryFrom;
  let mut s = Solver::try_from("tests/sample.cnf").expect("failed to load");
  let Solver {
      ref mut asg,
      ref mut cdb,
      ref mut elim,
      ref mut state,
      ..
  } = s;
  elim.activate();
  elim.simplify(asg, cdb, state).expect("panic");
  assert_eq!(elim.exports().0, 1);
  assert!(0 < asg.num_eliminated_vars);

Structs

Eliminator	Literal eliminator
LitOccurs	Mapping from Literal to Clauses.
VarOccHeap	Var heap structure based on the number of occurrences

Traits

EliminateIF	API for Eliminator like activate, stop, eliminate and so on.
EliminatorStatIF	API for getting stats about Eliminator's internal data.