### 7 releases

new 0.4.0 | Jun 14, 2024 |
---|---|

0.3.3 | May 4, 2024 |

0.3.2 | Apr 12, 2024 |

0.3.1 | Jan 29, 2024 |

0.2.1 | Oct 15, 2022 |

#**147** in Math

**128** downloads per month

Used in **2** crates

**LGPL-2.1-or-later**

1MB

**22K**
SLoC

# CNFGEN

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

This library provides simple CNF writer, structures to create boolean formula from
boolean expressions and integer expressions. The module

provides
basic types, traits to handle clauses and literals, simple the CNF writer to write
same CNF formulas. The `writer`

module provides structure to construct boolean
expressions. The `boolexpr`

and `intexpr`

modules provides structure and traits to
construct integer expressions.`dynintexpr`

Same construction of expressions can be done in natural way by using operators or
methods. The object called

holds all expressions. The main structures
that allow construct expressions are expression nodes: `ExprCreator`

, `BoolExprNode`

and `IntExprNode`

. BoolExprNode allow to construct boolean expressions.
`DynIntExprNode`

and `IntExprNode`

allow to construct integer expressions or multiple
bit expressions.`DynIntExprNode`

Version 0.4.0 (current) offers new interface to operate on expressions.
This interface in

, `boolvar`

and `intvar`

modules. New interface offers
few simplifications that facility writing complex expressions.`dynintvar`

Typical usage of this library is: construction boolean expression and write it by using
method

from an expression object. The `write`

module can be used to write
'raw' CNF formulas that can be generated by other software.`writer`

Sample usage:

`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``(``77``i64``)``;`
`//` 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`(``)``)``)`
`}`

#### Dependencies

~0.6–1MB

~24K SLoC