Module splr::processor [−][src]
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("tests/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);
Re-exports
pub use self::property::*; |
Modules
property |
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 |