2 个版本

0.1.1	2020 年 7 月 26 日
0.1.0	2020 年 7 月 19 日

#1370 in 解析器实现

MIT/Apache

29KB
679 行

CNF 解析器

持续集成	文档	Crates.io

一个高效的、可定制的解析器，用于处理 .cnf (合取范式) 文件格式，该格式由 SAT 求解器使用。

没有 unsafe Rust!
无依赖！
解析时无堆分配！
no_std 兼容！

用法

要解析，请使用 parse_cnf 函数。它需要一个预期为 .cnf 编码的输入源，以及一个可定制的输出 &mut。此输出需要实现 Output 特性，并很可能是您的求解器或从给定的 .cnf 输入初始化求解器的某种东西。

示例

为了使用 parse_cnf，您首先需要定义自己的 Output 类型

#[derive(Default)]
pub struct MyOutput {
    head_clause: Vec<Literal>,
    clauses: Vec<Vec<Literal>>,
}

impl Output for MyOutput {
    type Error = &'static str;

    fn problem(
        &mut self, num_variables: u32, num_clauses: u32
    ) -> Result<(), Self::Error> {
        Ok(())
    }

    fn literal(&mut self, literal: Literal) -> Result<(), Self::Error> {
        self.head_clause.push(literal); Ok(())
    }

    fn finalize_clause(&mut self) -> Result<(), Self::Error> {
        if self.head_clause.is_empty() {
            return Err("encountered empty clause")
        }
        self.clauses.push(
            core::mem::replace(&mut self.head_clause, Vec::new())
        );
        Ok(())
    }

    fn finish(&mut self) -> Result<(), Self::Error> {
        if !self.head_clause.is_empty() {
            self.finalize_clause()?
        }
        Ok(())
    }
}

然后按照以下方式使用 parse_cnf

let my_input: &[u8] = br"
    c This is my input .cnf file with 3 variables and 2 clauses.
    p cnf 3 2
    1 -2 3 0
    1 -3 0
";
let mut my_output = MyOutput::default();
cnf_parser::parse_cnf(&mut my_input.as_ref(), &mut my_output)
    .expect("encountered invalid .cnf input");