cnfgen2 0.2.0

Generate DIMACS CNF formula from operations (second version)
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63

// lib.rs - main library

#![cfg_attr(docsrs, feature(doc_cfg))]
//! The library to generate CNF (Conjunctive Normal Form) formulas.
//! This is newer version of CNFGEN - it introduces current generic-array-1.x crate.
//!
//! 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 provide 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 allows to construct boolean expressions.
//! `IntExprNode` and `DynIntExprNode` allows to construct integer expressions or multiple
//! bit expressions.
//!
//! The version offers new interface to operate on expressions.
//! This interface in `boolvar`, `intvar` and `dynintvar` modules. New interface offers
//! few simplifications that facility writing complex expressions.
//! New `boolvar` module provides simpler interface to construct boolean expressions.
//! New `intvar` module provides simpler interface to construct integer expressions.
//! New `dynintvar` module provides simpler interface to construct dynamic integer expressions.
//! The routine that creates new expression must be called inside `call16`, `call32` or `callsys`.
//! That routine can returns formula to generate. The `BoolVar` allows to operate on boolean
//! expressions, `IntVar` allows to operate on integer expressions and `DynIntVar` allows to
//! operate on dynamic integer expressions. These types can be used as references and
//! constants be converted into one of that type by using From trait.
//!
//! The version provides `min` and `max` helpers, new an optimized tables and If-Then-Else and
//! and additional `subvalues` method to dynamic integers.
//!
//! IMPORTANT: Older version (<0.2) had bug in division definition in conditional variable.
//! (variable that control whether division is legal). Previous versions uses multiplications
//! to define division that causes including improper condition to conditional variable.
//! It recommeded to use new version (>=0.2).
//!
//! 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.

#![allow(unused_imports)]

pub mod writer;
pub use writer::{Literal, VarLit};

pub mod boolexpr;
pub mod boolexpr_creator;
pub mod boolvar;

pub mod dynintexpr;
pub mod dynintvar;
mod int_utils;
pub mod intexpr;
mod intmacros;
pub mod intvar;

pub use generic_array;