Struct splr::solver::Solver [−][src]
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("tests/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("tests/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
impl Clone for Solver
[src]
impl Debug for Solver
[src]
impl Default for Solver
[src]
impl Instantiate for Solver
[src]
fn instantiate(config: &Config, cnf: &CNFDescription) -> Solver
[src]
use crate::{splr::config::Config, splr::types::*}; use splr::solver::Solver; let s = Solver::instantiate(&Config::default(), &CNFDescription::default());
fn handle(&mut self, _e: SolverEvent)
[src]
impl SatSolverIF for Solver
[src]
fn add_assignment(&mut self, val: i32) -> Result<&mut Solver, SolverError>
[src]
fn add_clause<V>(&mut self, vec: V) -> Result<&mut Solver, SolverError> where
V: AsRef<[i32]>,
[src]
V: AsRef<[i32]>,
fn add_var(&mut self) -> usize
[src]
fn build(config: &Config) -> Result<Solver, SolverError>
[src]
Examples
use splr::config::Config; use splr::solver::{SatSolverIF, Solver}; let config = Config::from("tests/sample.cnf"); assert!(Solver::build(&config).is_ok());
fn reset(&mut self)
[src]
impl SolveIF for Solver
[src]
fn solve(&mut self) -> SolverResult
[src]
Examples
use splr::*; let config = Config::from("tests/sample.cnf"); if let Ok(mut s) = Solver::build(&config) { let res = s.solve(); assert!(res.is_ok()); assert_ne!(res.unwrap(), Certificate::UNSAT); }
impl TryFrom<&'_ str> for Solver
[src]
type Error = SolverError
The type returned in the event of a conversion error.
fn try_from(s: &str) -> Result<Self, Self::Error>
[src]
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("tests/sample.cnf").expect("fail to load");
impl<V> TryFrom<(Config, &'_ [V])> for Solver where
V: AsRef<[i32]>,
[src]
V: AsRef<[i32]>,
type Error = SolverResult
The type returned in the event of a conversion error.
fn try_from((config, vec): (Config, &[V])) -> Result<Self, Self::Error>
[src]
impl ValidateIF for Solver
[src]
fn inject_assignment(&mut self, vec: &[i32]) -> MaybeInconsistent
[src]
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(()));
fn validate(&self) -> Option<Vec<i32>>
[src]
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 Send for Solver
impl Sync for Solver
impl Unpin for Solver
impl UnwindSafe for Solver
Blanket Implementations
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
pub fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> From<T> for T
[src]
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
pub fn to_owned(&self) -> T
[src]
pub fn clone_into(&self, target: &mut T)
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
pub fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,