Struct splr::solver::Solver [−][src]
pub struct Solver { pub asg: AssignStack, pub cdb: ClauseDB, pub elim: Eliminator, pub rst: Restarter, pub state: State, }
Expand description
The SAT solver object consisting of 6 sub modules.
use std::convert::TryFrom; use crate::splr::*; use crate::splr::{assign::{AssignIF, VarManipulateIF}, state::{State, StateIF}, types::*}; let mut s = Solver::try_from("cnfs/sample.cnf").expect("can't load"); assert_eq!(s.asg.derefer(assign::property::Tusize::NumVar), 250); assert_eq!(s.asg.derefer(assign::property::Tusize::NumUnassertedVar), 250); if let Ok(Certificate::SAT(v)) = s.solve() { assert_eq!(v.len(), 250); // But don't expect `s.asg.var_stats().3 == 0` at this point. // It returns the number of vars which were assigned at decision level 0. } else { panic!("It should be satisfied!"); } assert_eq!(Solver::try_from("cnfs/unsat.cnf").expect("can't load").solve(), Ok(Certificate::UNSAT));
Fields
asg: AssignStack
assignment management
cdb: ClauseDB
clause container
elim: Eliminator
clause and variable elimination
rst: Restarter
restart management
state: State
misc data holder
Trait Implementations
use crate::{splr::config::Config, splr::types::*}; use splr::solver::Solver; let s = Solver::instantiate(&Config::default(), &CNFDescription::default());
update by a solver event.
Examples
use splr::config::Config; use splr::solver::{SatSolverIF, Solver}; let config = Config::from("cnfs/sample.cnf"); assert!(Solver::build(&config).is_ok());
dump an UNSAT certification file
add an assignment to Solver. Read more
add a literal to Solver. Read more
reinitialize a solver for incremental solving. Requires ‘incremental_solver’ feature
Examples
use splr::*; let config = Config::from("cnfs/sample.cnf"); if let Ok(mut s) = Solver::build(&config) { let res = s.solve(); assert!(res.is_ok()); assert_ne!(res.unwrap(), Certificate::UNSAT); }
return a new solver build for a CNF file.
Example
use std::convert::TryFrom; use crate::splr::solver::{SatSolverIF, Solver}; let mut s = Solver::try_from("cnfs/sample.cnf").expect("fail to load");
type Error = SolverError
type Error = SolverError
The type returned in the event of a conversion error.
inject an assignment set into solver.
An assignment set is represented by a list of i32
.
#Example
use crate::{splr::config::Config, splr::types::*}; use splr::solver::{Solver, ValidateIF}; let cnf = CNFDescription { num_of_variables: 4, ..CNFDescription::default() }; let mut s = Solver::instantiate(&Config::default(), &cnf); assert_eq!(s.inject_assignment(&[1i32, -2, 3]), Ok(()));
returns None if the given assignment is a model of a problem. Otherwise returns a clause which is not satisfiable under a given assignment.
#Example
use crate::{splr::config::Config, splr::types::*}; use splr::solver::{Solver, ValidateIF}; let cnf = CNFDescription { num_of_variables: 4, ..CNFDescription::default() }; let mut s = Solver::instantiate(&Config::default(), &cnf); s.inject_assignment(&[1i32, -2, 3]); assert_eq!(s.validate(), None);
Auto Trait Implementations
impl RefUnwindSafe for Solver
impl UnwindSafe for Solver
Blanket Implementations
Mutably borrows from an owned value. Read more