Struct MultiSolver 

pub struct MultiSolver<T> { /* private fields */ }

treats multiple SatSolvers as one SatSolver

Implementations

impl<T> MultiSolver<T>

pub fn next(&mut self)

rotate to the next solver

pub fn as_mut_slice(&mut self) -> &mut [T]

return a mutable slice of SatSolvers

impl<T> MultiSolver<T>

where T: SatSolver,

pub fn new_by_size(n: usize) -> Self

n > 0

Trait Implementations

impl<T, C> AddConstraints<C> for MultiSolver<T>

where T: AddConstraints<C>,

fn insert(&mut self, constraints: &C)

impl<T> SatSolver for MultiSolver<T>

where T: SatSolver,

type Status = <T as SatSolver>::Status

fn new() -> Self

Create a new SAT solver

fn solve(&mut self) -> Self::Status

Decide whether current constraints are satisfiable or not

fn val(&mut self, lit: i32) -> bool

After Self::solve returns sat, query the solver for the boolean value of the SAT variable lit.

fn load_model(&mut self) -> Model

After Self::solve returns sat, obtain the full model.

fn block_model(&mut self)

After Self::solve returns sat, block the current model. It is useful for model enumeration.