Struct Solver 

pub struct Solver<S, St = UNKNOWN>
where
    S: Search,
    St: SolverState,
{
    pub(crate) pre_processor: Vec<Box<dyn Pass>>,
    pub(crate) in_processor: Vec<Box<dyn Pass>>,
    pub(crate) search: S,
    pub(crate) kernel: Kernel,
    pub(crate) _state: PhantomData<St>,
}

主求解器对象。

组件说明：

• pre_processor：搜索前执行；
• in_processor：搜索循环中周期执行；
• search：CDCL 核心；
• kernel：统一状态与数据。

Fields

pre_processor: Vec<Box<dyn Pass>>

in_processor: Vec<Box<dyn Pass>>

search: S

kernel: Kernel

_state: PhantomData<St>

Implementations

impl<S, St> Solver<S, St>

where S: Search, St: SolverState,

pub const fn status(&self) -> SolverStatus

返回编译期状态对应的运行时枚举。

pub fn kernel(&self) -> &Kernel

只读访问内核。

pub(crate) fn into_state<Next>(self) -> Solver<S, Next>

where Next: SolverState,

impl<S> Solver<S, UNKNOWN>

where S: Search,

pub fn new(search: S, kernel: Kernel) -> Self

创建处于 UNKNOWN 状态的求解器。

pub fn add_preprocess_pass(&mut self, pass: impl Pass + 'static)

注册一个预处理 Pass。

pub fn arrange_preprocess_passes(&mut self, ordered: &str)

按逗号分隔短名重排预处理 Pass。

pub fn add_inprocess_pass(&mut self, pass: impl Pass + 'static)

注册一个搜索中 Pass。

pub fn arrange_inprocess_passes(&mut self, ordered: &str)

按逗号分隔短名重排搜索中 Pass。

pub fn solve(self) -> SolveResult<S>

执行完整求解流程并返回分型结果。

主要顺序：

1. 先跑预处理，若可直接判定则提前返回；
2. 进入 SOLVING 状态，执行 CDCL 搜索；
3. 按最终结果转移到 SAT/UNSAT/UNKNOWN 状态。

pub(crate) fn arrange_passes(passes: &mut Vec<Box<dyn Pass>>, ordered: &str)

根据短名称重排 Pass，未出现在 ordered 中的 Pass 会被丢弃。

impl<S> Solver<S, SAT>

where S: Search,

pub fn model(&self) -> Vec<bool>

导出模型（索引 0 保留，不对应实际变量）。

pub fn check_sat(&self) -> Result<(), String>

用当前模型逐子句校验 SAT 结果。

pub fn print_model(&self)

按 DIMACS 竞赛风格打印模型。