Expand description
The library to generate CNF (Conjunctive Normal Form) formulas.
This library provides simple CNF writer, structures to create boolean formula 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 formulas. 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.
Samples of usage of these modules can be found in documentation of these modules.
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 formulas that can be generated by other software.
Re-exports§
pub use writer::Literal;
pub use writer::VarLit;
pub use generic_array;
Modules§
- The module to generate CNF clauses from boolean expressions.
- The module to generate CNF clauses from boolean expressions.
- The module to generate CNF clauses from dynamic integer expressions.
- The module to generate CNF clauses from integer expressions.
- The module to write CNF from clauses.