[−][src]Trait splr::solver::ValidateIF

pub trait ValidateIF {
    pub fn inject_assignment(&mut self, vec: &[i32]) -> MaybeInconsistent;

    pub fn validate(&self) -> Option<Vec<i32>>;
}

API for SAT validator like inject_assignment, validate and so on.

Required methods

pub fn inject_assignment(&mut self, vec: &[i32]) -> MaybeInconsistent[src]

load a assignment set into solver.

Errors

if solver becomes inconsistent.

pub fn validate(&self) -> Option<Vec<i32>>[src]

return true is the loaded assignment set is satisfiable (a model of a problem).

Loading content...

Implementors

impl ValidateIF for Solver[src]

pub 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(()));

pub 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);
Loading content...