Module splr::processor

Module 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, Eliminator, EliminateIF}, solver::Solver, types::{Instantiate, PropertyDereference}};
  use std::path::Path;

  let mut s = Solver::try_from(Path::new("cnfs/sample.cnf")).expect("failed to load");
  let Solver {
      ref mut asg,
      ref mut cdb,
      ref mut state,
      ..
  } = s;
  let mut elim = Eliminator::instantiate(&state.config, &state.cnf);
  elim.simplify(asg, cdb, state, false).expect("panic");
  assert!(!state.config.enable_eliminator || 0 < asg.num_eliminated_vars);

Structs

• Eliminator
  Literal eliminator

Traits

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