refac: prepare for publishing

Cargo.toml

@@ -1,5 +1,5 @@
 [workspace]
-members = ["bin", "benchmarks", "sdd-rs-lib"]
+members = ["bin", "benchmarks", "sddrs"]
 resolver = "2"
 
 [workspace.lints.rust]

bin/Cargo.toml

@@ -1,6 +1,21 @@
 [package]
 name = "sddrsc"
 edition = "2021"
+license = "BSD-3-Clause"
+authors = ["Josef Podany"]
+repository = "https://github.com/jsfpdn/sdd-rs"
+description = "Bottom-up Sentential Decision Diagram compiler."
+keywords = [
+    "knowledge-compilation",
+    "boolean-functions",
+    "sentential-decision-diagrams",
+]
+categories = [
+    "compilers",
+    "data-structures",
+    "mathematics",
+    "command-line-utilities",
+]
 
 [[bin]]
 name = "sddrsc"
@@ -10,7 +25,7 @@ path = "main.rs"
 tracing-subscriber = "0.3"
 tracing = "0.1"
 clap = { version = "4.5.4", features = ["derive"] }
-sddrs = { path = "../sdd-rs-lib" }
+sddrs = { path = "../sddrs" }
 anyhow = "1.0"
 
 [lints]

sdd-rs-lib/Cargo.toml → sddrs/Cargo.toml

@@ -2,9 +2,18 @@
 name = "sddrs"
 version = "0.1.0"
 edition = "2021"
-authors = ["josef podany"]
+authors = ["Josef Podany"]
 repository = "https://github.com/jsfpdn/sdd-rs"
-description = "Bottom-up sentential decision diagram compiler library."
+description = "Bottom-up Sentential Decision Diagram compiler library."
+keywords = [
+    "knowledge-compilation",
+    "boolean-functions",
+    "sentential-decision-diagrams",
+    "model-counting",
+    "satisfiability",
+]
+categories = ["compilers", "data-structures", "mathematics"]
+license = "BSD-3-Clause"
 
 [lib]
 name = "sddrs"

sddrs/README.md

@@ -0,0 +1,81 @@
+# :books: sddrs: Bottom-Up Sentential Decision Diagram Compiler
+
+**Incrementally build, manipualate, and optimize
+[Sentential Decision Diagrams (SDD)](https://en.wikipedia.org/wiki/Sentential_decision_diagram):
+a succinct representation of Boolean functions.**
+
+## :tada: Features
+
+The compiler currently supports:
+
+* incremental compilation of Boolean functions (knowledge bases) to *compressed* and *trimmed* SDDs,
+* efficient querying of model count, model enumeration, and equivalence of SDDs,
+* dynamic minimization of SDDs via *vtree fragments*,
+* garbage collection of dead nodes,
+* SDD compilation from CNF in
+  [DIMACS](https://www21.in.tum.de/~lammich/2015_SS_Seminar_SAT/resources/dimacs-cnf.pdf) format.
+
+## :package: Usage
+
+The following snippet compiles the function $(A \land B) \lor C$ to an SDD,
+computes number of its models, enumerates and prints them to the stdout,
+and renders the compiled SDD and its vtree to the DOT format.
+
+```rust
+use sddrs::manager::{options, GCStatistics, SddManager};
+use sddrs::literal::literal::Polarity;
+use bon::arr;
+
+fn main() {
+    let options = options::SddOptions::builder()
+        // Create right-linear vtree.
+        .vtree_strategy(options::VTreeStragey::RightLinear)
+        // Initialize the manager with variables A, B, and C.
+        .variables(["A".to_string(), "B".to_string(), "C"])
+        .build();
+    let manager = SddManager::new(options);
+
+    // Retrieve SDDs for literals A, B, and C.
+    let a = manager.literal("A", Polarity::Positive).unwrap();
+    let b = manager.literal("B", Polarity::Positive).unwrap();
+    let c = manager.literal("C", Polarity::Positive).unwrap();
+
+    // Compute "A ∧ B"
+    let a_and_b = manager.conjoin(&a, &b);
+    // Compute "(A ∧ B) ∨ C"
+    let a_and_b_or_c = manager.disjoin(&a_and_b, &c);
+
+    let model_count = manager.model_count(&a_and_b_or_c);
+    let models = manager.model_enumeration(&a_and_b_or_c);
+
+    println!("'(A ∧ B) ∨ C' has {model_count} models.");
+    println!("They are:\n{models}");
+
+    let sdd_path = "my_formula.dot"
+    let f = File::create(sdd_path).unwrap();
+    let mut b = BufWriter::new(f);
+    manager
+        .draw_sdd(&mut b as &mut dyn std::io::Write, &sdd)
+        .unwrap();
+
+    let vtree_path = "my_vtree.dot"
+    let f = File::create(vtree_path).unwrap();
+    let mut b = BufWriter::new(f);
+    manager
+        .draw_vtree(&mut b as &mut dyn std::io::Write)
+        .unwrap();
+
+    println!("Rendered SDD to '{sdd_path}' and vtree to '{vtree_path}'");
+}
+```
+
+## :page_with_curl: Related Links
+
+* [SDD: A New Canonical Representation of Propositional Knowledge Bases - Adnad Darwiche](http://reasoning.cs.ucla.edu/fetch.php?id=121&type=pdf):
+  paper introducing SDDs
+* [Dynamic Minimization of Sentential Decision Diagrams - Arthur Choi and Adnan Darwiche](http://reasoning.cs.ucla.edu/fetch.php?id=128&type=pdf):
+  paper describing dynamic minimization of SDDs
+* [SDD: A New Canonical Representation of Propositional Knowledge Bases – Adnan Darwiche (YouTube tutorial)](https://www.youtube.com/watch?v=_5Estmve91o)
+* [Bottom-Up Knowledge Compilers – Adnan Darwiche (YouTube tutorial)](https://www.youtube.com/watch?v=8yZapazT9Ls)
+* [The SDD Package homepage](http://reasoning.cs.ucla.edu/sdd/): homepage of the original C SDD compiler
+* [RSDD](https://github.com/neuppl/rsdd): alternative implementation of SDD in Rust

sdd-rs-lib/manager/model.rs → sddrs/manager/model.rs

@@ -32,7 +32,7 @@ impl Models {
 impl Display for Models {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
         let mut builder = Builder::default();
-        builder.push_record(self.variables.iter().map(|v| v.label()));
+        builder.push_record(self.variables.iter().map(Variable::label));
 
         for model in &self.models {
             builder.push_record(