Skip to content

Commit a61801a

Browse files
jsfpdnjsfpdn
committed
refac: improve documentation
1 parent 81f63e2 commit a61801a

File tree

12 files changed

+146
-23
lines changed

12 files changed

+146
-23
lines changed

‎sddrs/lib.rs

+116-2
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,121 @@
1+
//! # Bottom-up compiler for Sentential Decision Diagrams.
2+
//!
3+
//! Incrementally build, manipualate, and optimize
4+
//! [Sentential Decision Diagrams (SDD)](https://en.wikipedia.org/wiki/Sentential_decision_diagram):
5+
//! a succinct representation of Boolean functions.
6+
//!
7+
//! The compiler currently supports:
8+
//! * incremental compilation of Boolean functions (knowledge bases) to *compressed* and *trimmed* SDDs,
9+
//! * efficient querying of model count, model enumeration, and equivalence of SDDs,
10+
//! * dynamic minimization of SDDs via *vtree fragments*,
11+
//! * garbage collection of dead nodes,
12+
//! * SDD compilation from CNF in
13+
//! [DIMACS](https://www21.in.tum.de/~lammich/2015_SS_Seminar_SAT/resources/dimacs-cnf.pdf) format.
14+
//!
15+
//!
16+
//!
17+
//!
18+
//!
19+
//!
20+
//! The following snippet compiles the function `(A ∧ B) ∨ C` to SDD,
21+
//! computes number of its models, enumerates and prints them to the stdout,
22+
//! and renders the compiled SDD and its vtree to the DOT format.
23+
//!
24+
//! ```rust
25+
//! use sddrs::manager::{options, GCStatistics, SddManager};
26+
//! use sddrs::literal::literal::Polarity;
27+
//! use bon::arr;
28+
//!
29+
//! fn main() {
30+
//! let options = options::SddOptions::builder()
31+
//! // Create right-linear vtree.
32+
//! .vtree_strategy(options::VTreeStragey::RightLinear)
33+
//! // Initialize the manager with variables A, B, and C.
34+
//! .variables(["A".to_string(), "B".to_string(), "C".to_string()])
35+
//! .build();
36+
//! let manager = SddManager::new(options);
37+
//!
38+
//! // Retrieve SDDs for literals A, B, and C.
39+
//! let a = manager.literal("A", Polarity::Positive).unwrap();
40+
//! let b = manager.literal("B", Polarity::Positive).unwrap();
41+
//! let c = manager.literal("C", Polarity::Positive).unwrap();
42+
//!
43+
//! // Compute "A ∧ B"
44+
//! let a_and_b = manager.conjoin(&a, &b);
45+
//! // Compute "(A ∧ B) ∨ C"
46+
//! let a_and_b_or_c = manager.disjoin(&a_and_b, &c);
47+
//!
48+
//! let model_count = manager.model_count(&a_and_b_or_c);
49+
//! let models = manager.model_enumeration(&a_and_b_or_c);
50+
//!
51+
//! println!("'(A ∧ B) ∨ C' has {model_count} models.");
52+
//! println!("They are:\n{models}");
53+
//!
54+
//! let sdd_path = "my_formula.dot"
55+
//! let f = File::create(sdd_path).unwrap();
56+
//! let mut b = BufWriter::new(f);
57+
//! manager
58+
//! .draw_sdd(&mut b as &mut dyn std::io::Write, &sdd)
59+
//! .unwrap();
60+
//!
61+
//! let vtree_path = "my_vtree.dot"
62+
//! let f = File::create(vtree_path).unwrap();
63+
//! let mut b = BufWriter::new(f);
64+
//! manager
65+
//! .draw_vtree(&mut b as &mut dyn std::io::Write)
66+
//! .unwrap();
67+
//!
68+
//! println!("Rendered SDD to '{sdd_path}' and vtree to '{vtree_path}'");
69+
//! }
70+
//! ```
71+
//!
72+
//! ---
73+
//!
74+
//! Main methods to compile SDDs are:
75+
//!
76+
//! * [`crate::manager::SddManager::conjoin`] -- compute AND of two SDDs
77+
//! * [`crate::manager::SddManager::disjoin`] -- compute OR of two SDDs
78+
//! * [`crate::manager::SddManager::imply`] -- compute implication of two SDDs
79+
//! * [`crate::manager::SddManager::equiv`] -- compute equivalence of two SDDs
80+
//! * [`crate::manager::SddManager::negate`] -- compute negation of SDD
81+
//!
82+
//! Main methods to query SDDs are:
83+
//!
84+
//! * [`crate::manager::SddManager::model_count`] -- count the number of models of an SDD
85+
//! * [`crate::manager::SddManager::model_enumeration`] -- enumerate models of an SDD
86+
//! * [`crate::sdd::SddRef::size`] -- get size of the SDD
87+
//!
88+
//! SDDs can be also minimized after compilation by appropriately manipulating the vtree:
89+
//!
90+
//! * [`crate::manager::SddManager::swap`] -- swap children of a vtree and adjust SDDs
91+
//! * [`crate::manager::SddManager::rotate_right`] -- rotate vtree node to the right and adjust SDDs
92+
//! * [`crate::manager::SddManager::rotate_left`] -- rotate vtree node to the left and adjust SDDs
93+
//!
94+
//! These transformations do not guarantee that the SDD will decrease in size. In fact, it may grow.
95+
//! For this purpose, dynamic minimization via [`crate::vtree::fragment::Fragment`] tries to find
96+
//! the vtree that actually minimizes the SDD the most [`crate::manager::SddManager::minimize`].
97+
//!
98+
//! There are also additional helper functions:
99+
//!
100+
//! * [`crate::manager::SddManager::from_dimacs`] -- compile SDD based on a DIMACS CNF file
101+
//! * [`crate::manager::SddManager::draw_sdd`] -- draw a particular SDD to a DOT Graphviz format
102+
//! * [`crate::manager::SddManager::draw_all_sdds`] -- draw every SDDs to a DOT Graphviz format
103+
//! * [`crate::manager::SddManager::draw_vtree`] -- draw vtree a DOT Graphviz format
104+
//!
105+
//!
106+
//! Additional resources:
107+
//!
108+
//! * [SDD: A New Canonical Representation of Propositional Knowledge Bases - Adnad Darwiche](http://reasoning.cs.ucla.edu/fetch.php?id=121&type=pdf):
109+
//! paper introducing SDDs
110+
//! * [Dynamic Minimization of Sentential Decision Diagrams - Arthur Choi and Adnan Darwiche](http://reasoning.cs.ucla.edu/fetch.php?id=128&type=pdf):
111+
//! paper describing dynamic minimization of SDDs
112+
//! * [SDD: A New Canonical Representation of Propositional Knowledge Bases – Adnan Darwiche](https://www.youtube.com/watch?v=_5Estmve91o): YouTube tutorial
113+
114+
/// Variables, polarities, and literals.
1115
pub mod literal;
2116
pub mod manager;
3117
pub mod sdd;
4118
#[macro_use]
5-
pub mod util;
6-
pub mod dot_writer;
119+
pub(crate) mod util;
120+
pub(crate) mod dot_writer;
7121
pub mod vtree;

‎sddrs/literal/mod.rs

+2-1
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
1+
/// Variables, polarities, and literals.
12
pub mod literal;
2-
pub mod manager;
3+
pub(crate) mod manager;
34

45
pub(crate) use crate::literal::literal::*;
56
pub(crate) use crate::literal::manager::*;

‎sddrs/manager/dimacs.rs

+1
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
//! DIMACS module responsible for parsing DIMACS CNF problem files.
12
use crate::literal::{Polarity, VariableIdx};
23
use crate::manager::SddManager;
34
use crate::sdd::SddRef;

‎sddrs/manager/manager.rs

+12-14
Original file line numberDiff line numberDiff line change
@@ -75,13 +75,11 @@ impl GCStatistics {
7575
}
7676
}
7777

78-
/// [`SddManager`] is a structure responsible for maintaing the state of the compilation.
78+
/// Structure responsible for maintaing the state of the compilation.
7979
/// It is the central piece when compiling Boolean functions --- it is responsible
8080
/// combining SDDs, querying the knowledge, caching operations, collecting garbage
8181
/// (if configured), dynamically minimizing compiled knowledge (if configured),
82-
/// and much more.
83-
///
84-
/// See [`SddOptions`] on how [`SddManager`] can be configured.
82+
/// and much more. See [`SddOptions`] on how [`SddManager`] can be configured.
8583
///
8684
/// ```
8785
/// use sddrs::literal::literal::Polarity;
@@ -345,7 +343,7 @@ impl SddManager {
345343
}
346344
}
347345

348-
/// Retrieve the SDD representing [`Literal`] with given label and [`Polarity`].
346+
/// Retrieve the SDD representing a literal with given label and [`Polarity`].
349347
/// Returns [`None`] if such variable does not exist.
350348
pub fn literal(&self, label: &str, polarity: Polarity) -> Option<SddRef> {
351349
let (_, variants) = self.literal_manager.borrow().find_by_label(label)?;
@@ -1378,8 +1376,8 @@ impl SddManager {
13781376
self.vtree_manager.borrow().root()
13791377
}
13801378

1381-
/// Rotate the vtree [`x`] to the left and adjust SDDs accordingly.
1382-
/// The user must make sure that [`x`] is 'rotatable', i.e., [`x`]
1379+
/// Rotate the vtree `x` to the left and adjust SDDs accordingly.
1380+
/// The user must make sure that `x` is 'rotatable', i.e., `x`
13831381
/// is an internal node and has a parent.
13841382
///
13851383
/// ```text
@@ -1391,7 +1389,7 @@ impl SddManager {
13911389
/// ```
13921390
///
13931391
/// This is a low-level operation working directly on a vtree. See
1394-
/// [`SddManager::minimization`] for a more sophisticated way of finding better vtrees.
1392+
/// [`SddManager::minimize`] for a more sophisticated way of finding better vtrees.
13951393
///
13961394
/// Children hanged at `w` must be split accordingly, depending on the vtrees
13971395
/// they are normalized for:
@@ -1444,8 +1442,8 @@ impl SddManager {
14441442
}
14451443
}
14461444

1447-
/// Rotate the vtree [`x`] to the right and adjust SDDs accordingly.
1448-
/// The user must make sure that [`x`] is 'rotatable', i.e., [`x`]
1445+
/// Rotate the vtree `x` to the right and adjust SDDs accordingly.
1446+
/// The user must make sure that `x` is 'rotatable', i.e., `x`
14491447
/// is an internal node an its left child `w` is an internal node as well.
14501448
///
14511449
/// ```text
@@ -1457,7 +1455,7 @@ impl SddManager {
14571455
/// ```
14581456
///
14591457
/// This is a low-level operation working directly on a vtree. See
1460-
/// [`SddManager::minimization`] for a more sophisticated way of finding better vtrees.
1458+
/// [`SddManager::minimize`] for a more sophisticated way of finding better vtrees.
14611459
///
14621460
/// Children hanged at `w` must be split accordingly, depending on the vtrees
14631461
/// they are normalized for:
@@ -1494,8 +1492,8 @@ impl SddManager {
14941492
Ok(())
14951493
}
14961494

1497-
/// Swap children of the given vtree [`x`] and adjust SDDs accordingly.
1498-
/// The user must make sure that [`x`] is 'swappable', i.e., it is
1495+
/// Swap children of the given vtree `x` and adjust SDDs accordingly.
1496+
/// The user must make sure that `x` is 'swappable', i.e., it is
14991497
/// an internal node.
15001498
///
15011499
/// ```text
@@ -1505,7 +1503,7 @@ impl SddManager {
15051503
/// ```
15061504
///
15071505
/// This is a low-level operation working directly on a vtree. See
1508-
/// [`SddManager::minimization`] for a more sophisticated way of finding better vtrees.
1506+
/// [`SddManager::minimize`] for a more sophisticated way of finding better vtrees.
15091507
///
15101508
/// # Errors
15111509
///

‎sddrs/manager/mod.rs

+2
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
//! Manager responsible for manipulating and querying SDDs as well as maintaining
2+
//! the state of the compilation.
13
mod manager;
24

35
pub mod dimacs;

‎sddrs/manager/model.rs

+1
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
//! Models of the compiled knowledge base.
12
use crate::literal::{Literal, Polarity, Variable};
23
use bitvec::prelude::*;
34
use std::fmt::Display;

‎sddrs/manager/options.rs

+2-1
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
//! Configure [`crate::manager::SddManager`].
12
use bon::Builder;
23
use clap::ValueEnum;
34

@@ -58,7 +59,7 @@ pub enum MinimizationCutoff {
5859
BreakAfterFirstImprovement,
5960
}
6061

61-
/// [`sddrs::manager::SddManager`] configuration options. See individual
62+
/// [`crate::manager::SddManager`] configuration options. See individual
6263
/// fields for more information.
6364
#[allow(clippy::module_name_repetitions)]
6465
#[derive(Debug, Clone, Builder)]

‎sddrs/sdd/mod.rs

+1
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
//! Sentential Decision Diagrams.
12
mod decision;
23
mod element;
34
mod sdd;

‎sddrs/sdd/sdd_ref.rs

+2-3
Original file line numberDiff line numberDiff line change
@@ -137,7 +137,6 @@ impl SddRef {
137137
return negation == other.id();
138138
}
139139

140-
// TODO: This may cause panic w.r.t. borrowing here and later when negating.
141140
let fst_sdd_type = self.0.borrow().sdd_type.clone();
142141
let snd_sdd_type = other.0.borrow().sdd_type.clone();
143142

@@ -189,7 +188,7 @@ impl SddRef {
189188
self.0.borrow().canonicalize(manager)
190189
}
191190

192-
/// Recursively check whether [`self`] and all its descendants are trimmed.
191+
/// Recursively check whether [`SddRef`] and all its descendants are trimmed.
193192
/// SDD is trimmed if it does not contain decompositions in the form of
194193
/// `{(true, alpha)}` and `{(alpha, true), (!alpha, false)}`.
195194
pub fn is_trimmed(&self, manager: &SddManager) -> bool {
@@ -198,7 +197,7 @@ impl SddRef {
198197

199198
/// Recursivelly checks whether the SDD is compressed.
200199
/// Decision node is compressed if all subs are distinct, i.e.,
201-
/// for all indexes i,j such that i != j, it holds that `s_i != s_j`.
200+
/// for all indexes i,j such that i != j, it holds that s_i != s_j.
202201
///
203202
/// See definition 8 in [SDD: A New Canonical Representation of Propositional Knowledge Bases](https://ai.dmi.unibas.ch/research/reading_group/darwiche-ijcai2011.pdf).
204203
///

‎sddrs/vtree/fragment.rs

+4
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
1+
//! Fragment of a [`crate::vtree::VTreeRef`] used for dynamic minimization
2+
//! [`crate::manager::SddManager::minimize`] to decrease the size of [`crate::sdd::SddRef`].
13
#![allow(clippy::many_single_char_names, clippy::similar_names)]
24

35
use anyhow::{Context, Result};
@@ -61,6 +63,8 @@ const MOVES_RIGHT_LINEAR: [Move; 12] = [
6163
Move::SwapChild,
6264
];
6365

66+
/// Fragment represents a part of a vtree. It is defined by a root
67+
/// and a child. It can be either left-linear or right-linear.
6468
#[derive(Debug, Clone)]
6569
pub struct Fragment {
6670
current_root: VTreeRef,

‎sddrs/vtree/mod.rs

+2-1
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,5 @@
1-
mod fragment;
1+
//! Vtrees and fragments.
2+
pub mod fragment;
23
mod vtree;
34

45
pub(crate) use crate::vtree::fragment::*;

‎sddrs/vtree/vtree.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -154,7 +154,7 @@ pub(crate) enum VTreeOrder {
154154
RightSubOfLeft,
155155
}
156156

157-
/// Vtree is a node of a full binary tree.
157+
/// Vtree is a node of a full binary tree for which an [`crate::sdd::SddRef`] is normalized.
158158
#[derive(Debug, Clone)]
159159
pub struct VTreeRef(pub(crate) Rc<RefCell<VTree>>);
160160

0 commit comments

Comments
 (0)