Skip to main content

SolverState

Trait SolverState 

Source
pub trait SolverState {
    // Required methods
    fn is_sat(&self) -> bool;
    fn is_unsat(&self) -> bool;
    fn is_unknown(&self) -> bool;
}
Expand description

This trait provides an abstraction for a solver state.

Invariant: exactly one of Self::is_sat, Self::is_unsat, and Self::is_unknown should be true.

Required Methods§

Source

fn is_sat(&self) -> bool

Source

fn is_unsat(&self) -> bool

Source

fn is_unknown(&self) -> bool

Implementors§