CNFGEN

生成CNF（合取范式）公式的库。

此库提供简单的CNF写入器，用于从布尔表达式和整数表达式创建布尔公式和整数表达式的结构。模块 writer 提供基本类型、处理子句和文字的特性和简单的CNF写入器，用于写入相同的CNF公式。模块 boolexpr 提供构建布尔表达式的结构。模块 intexpr 和 dynintexpr 提供构建整数表达式和多位表达式结构和特性。

可以使用运算符或方法以自然的方式构建表达式。名为 ExprCreator 的对象持有所有表达式。允许构建表达式的主体结构是表达式节点：BoolExprNode、IntExprNode 和 DynIntExprNode。BoolExprNode 允许构建布尔表达式。 IntExprNode 和 DynIntExprNode 允许构建整数表达式或多位表达式。

版本 0.4.0（当前）提供了操作表达式的新接口。此接口在 boolvar、intvar 和 dynintvar 模块中。新接口提供了一些简化，便于编写复杂的表达式。

此库的典型用法是：构建布尔表达式，并使用表达式对象的方法 write 编写它。可以使用 writer 模块编写“原始”CNF公式，这些公式可以由其他软件生成。

示例用法

use cnfgen::boolexpr::*;
use cnfgen::intexpr::*;
use cnfgen::writer::{CNFError, CNFWriter};
use std::io;

fn write_diophantine_equation() -> Result<(), CNFError> {
    // define ExprCreator.
    let creator = ExprCreator32::new();
    // define variables - signed 32-bit wide.
    let x = I32ExprNode::variable(creator.clone());
    let y = I32ExprNode::variable(creator.clone());
    let z = I32ExprNode::variable(creator.clone());
    // define equation: x^2 + y^2 - 77*z^2 = 0
    let powx = x.clone().fullmul(x);  // x^2
    let powy = y.clone().fullmul(y);  // y^2
    let powz = z.clone().fullmul(z);  // z^2
    // We use cond_mul to get product and required condition to avoid overflow.
    let (prod, cond0) = powz.cond_mul(77i64);
    // Similary, we use conditional addition and conditional subtraction.
    let (sum1, cond1) = powx.cond_add(powy);
    let (diff2, cond2) = sum1.cond_sub(prod);
    // define final formula with required conditions.
    let formula: BoolExprNode<_> = diff2.equal(0) & cond0 & cond1 & cond2;
    // write CNF to stdout.
    formula.write(&mut CNFWriter::new(io::stdout()))
}