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::{self, EliminateIF}, solver::Solver, types::PropertyDereference};
  use std::convert::TryFrom;
  let mut s = Solver::try_from("cnfs/sample.cnf").expect("failed to load");
  let Solver {
      ref mut asg,
      ref mut cdb,
      ref mut elim,
      ref mut rst,
      ref mut state,
      ..
  } = s;
  elim.activate();
  elim.simplify(asg, cdb, rst, state).expect("panic");
  assert_eq!(elim.derefer(processor::property::Tusize::NumFullElimination), 1);
  assert!(0 < asg.num_eliminated_vars);

Modules

property

Structs

Eliminator

Literal eliminator

Traits

EliminateIF

API for Eliminator like activate, stop, eliminate and so on.