CNFGEN

The library to generate CNF (Conjunctive Normal Form) formulaes.

This library provides simple CNF writer, structures to create boolean formulae from boolean expressions and integer expressions. The module writer provides basic types, traits to handle clauses and literals, simple the CNF writer to write same CNF formulaes. The boolexpr module provides structure to construct boolean expressions. The intexpr and dynintexpr modules provides structure and traits to construct integer expressions.

Same construction of expressions can be done in natural way by using operators or methods. The object called ExprCreator holds all expressions. The main structures that allow construct expressions are expression nodes: BoolExprNode, IntExprNode and DynIntExprNode. BoolExprNode allow to construct boolean expressions. IntExprNode and DynIntExprNode allow to construct integer expressions or multiple bit expressions.

Typical usage of this library is: construction boolean expression and write it by using method write from an expression object. The writer module can be used to write 'raw' CNF formulaes that can be generated by other software.

Sample usage:

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

fn writediophantineequation() -> 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 condmul to get product and required condition to avoid overflow. let (prod, cond0) = powz.condmul(77i64); // Similary, we use conditional addition and conditional subtraction. let (sum1, cond1) = powx.condadd(powy); let (diff2, cond2) = sum1.condsub(prod); // define final formulae with required conditions. let formulae: BoolExprNode<_> = diff2.equal(0) & cond0 & cond1 & cond2; // write CNF to stdout. formulae.write(&mut CNFWriter::new(io::stdout())) } ```