add: docs: examples

README.md

@@ -83,6 +83,8 @@ fn main() {
 }
 ```
 
+**See [examples](https://github.com/jsfpdn/sdd-rs/tree/main/sddrs/examples) for more examples.**
+
 ### Binary
 
 The compiler can be also compiled and invoked as a command-line utility.

sddrs/README.md

@@ -17,21 +17,22 @@ The compiler currently supports:
 
 ## Usage
 
+**See [examples](https://github.com/jsfpdn/sdd-rs/tree/main/sddrs/examples) for more examples.**
+
 The following snippet compiles the function `(A & B) | 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"])
+        .variables(&["A".to_string(), "B".to_string(), "C".to_string()])
         .build();
     let manager = SddManager::new(options);
 
@@ -51,14 +52,14 @@ fn main() {
     println!("'(A ∧ B) ∨ C' has {model_count} models.");
     println!("They are:\n{models}");
 
-    let sdd_path = "my_formula.dot"
+    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 vtree_path = "my_vtree.dot";
     let f = File::create(vtree_path).unwrap();
     let mut b = BufWriter::new(f);
     manager

sddrs/examples/fragment_minimization.rs

@@ -0,0 +1,40 @@
+//! Example minimization of compiled knowledge via vtree fragments.
+
+use sddrs::{
+    literal::literal::Polarity,
+    manager::{
+        options::{self, FragmentHeuristic, GarbageCollection, MinimizationCutoff, VTreeStrategy},
+        SddManager,
+    },
+};
+
+fn main() {
+    let opts = options::SddOptions::builder()
+        .vtree_strategy(VTreeStrategy::LeftLinear)
+        .garbage_collection(GarbageCollection::Automatic)
+        .variables(&["A".to_string(), "B".to_string(), "C".to_string()])
+        .build();
+    let manager = SddManager::new(&opts);
+
+    let a = manager.literal("A", Polarity::Positive).unwrap();
+    let b = manager.literal("B", Polarity::Positive).unwrap();
+    let c = manager.literal("C", Polarity::Positive).unwrap();
+
+    let conjunction = manager.conjoin(&a, &manager.conjoin(&b, &c));
+    let size_before = conjunction.size();
+    println!("size for right-linear: {}", size_before);
+
+    manager
+        .minimize(
+            MinimizationCutoff::BreakAfterFirstImprovement,
+            &FragmentHeuristic::Root,
+            &conjunction,
+        )
+        .unwrap();
+
+    let size_after = conjunction.size();
+    println!("size after minimizing via fragments: {}", size_after);
+
+    // Ideally, this should hold:
+    assert!(size_after <= size_before);
+}

sddrs/examples/input_output.rs

@@ -0,0 +1,33 @@
+use sddrs::manager::{
+    options::{self, GarbageCollection, VTreeStrategy},
+    SddManager,
+};
+
+fn main() {
+    let opts = options::SddOptions::builder()
+        .vtree_strategy(VTreeStrategy::LeftLinear)
+        .garbage_collection(GarbageCollection::Automatic)
+        .variables(&[
+            "A".to_string(),
+            "B".to_string(),
+            "C".to_string(),
+            "D".to_string(),
+        ])
+        .build();
+    let manager = SddManager::new(&opts);
+
+    let dimacs = "c
+p cnf 4 3
+1 3 -4 0
+4 0
+2 -3 0
+";
+    let sdd = manager.from_dimacs(&mut dimacs.as_bytes()).unwrap();
+
+    println!("Compiled SDD in DOT Graphviz format:");
+    manager.draw_sdd(&mut std::io::stdout(), &sdd).unwrap();
+
+    println!("\n---\nVtree in DOT Graphviz format:");
+    manager.draw_vtree(&mut std::io::stdout()).unwrap();
+    println!();
+}

sddrs/examples/manual_minimization.rs

@@ -0,0 +1,56 @@
+//! Example of manual minimization of compiled knowledge.
+use sddrs::{
+    literal::literal::Polarity,
+    manager::{
+        options::{self, GarbageCollection, VTreeStrategy},
+        SddManager,
+    },
+};
+
+fn main() {
+    let opts = options::SddOptions::builder()
+        //    x
+        //   / \
+        //  A   y
+        //     / \
+        //    B   C
+        .vtree_strategy(VTreeStrategy::RightLinear)
+        .garbage_collection(GarbageCollection::Automatic)
+        .variables(&["A".to_string(), "B".to_string(), "C".to_string()])
+        .build();
+    let manager = SddManager::new(&opts);
+
+    let a = manager.literal("A", Polarity::Positive).unwrap();
+    let b = manager.literal("B", Polarity::Positive).unwrap();
+    let c = manager.literal("C", Polarity::Positive).unwrap();
+
+    // A && B && C
+    let conjunction = manager.conjoin(&a, &manager.conjoin(&b, &c));
+    println!("size for right-linear: {}", conjunction.size());
+
+    // Rotate 'x' to obtain this vtree:
+    //     x
+    //    / \
+    //   y   C
+    //  / \
+    // A   B
+    manager
+        .rotate_left(&manager.root().right_child().unwrap())
+        .unwrap();
+    println!(
+        "size after rotating 'x' to the left: {}",
+        conjunction.size()
+    );
+
+    // Swap children of 'y' to obtain this vtree:
+    //     x
+    //    / \
+    //   y   C
+    //  / \
+    // B   A
+    manager.swap(&manager.root().left_child().unwrap()).unwrap();
+    println!(
+        "size after swapping children of 'y': {}",
+        conjunction.size()
+    );
+}

sddrs/examples/simple.rs

@@ -0,0 +1,43 @@
+//! Example of simple knowledge compilation.
+use sddrs::{
+    literal::literal::Polarity,
+    manager::{
+        options::{self, GarbageCollection, VTreeStrategy},
+        SddManager,
+    },
+};
+
+fn main() {
+    let opts = options::SddOptions::builder()
+        .vtree_strategy(VTreeStrategy::RightLinear)
+        .garbage_collection(GarbageCollection::Automatic)
+        .variables(&["A".to_string(), "B".to_string(), "C".to_string()])
+        .build();
+
+    let manager = SddManager::new(&opts);
+
+    let a = manager.literal("A", Polarity::Positive).unwrap();
+    let n_b = manager.literal("B", Polarity::Negative).unwrap();
+    let c = manager.literal("C", Polarity::Positive).unwrap();
+
+    // A && !B
+    let fst = manager.conjoin(&a, &n_b);
+    assert_eq!(manager.model_count(&fst), 2);
+    println!("A && !B:\n{}\n", manager.model_enumeration(&fst));
+
+    // C => (A && !B)
+    let snd = manager.imply(&c, &fst);
+    assert_eq!(manager.model_count(&snd), 5);
+    println!("C => (A && !B):\n{}\n", manager.model_enumeration(&snd));
+
+    // !(C => (A && !B))
+    let n_snd = manager.negate(&snd);
+    assert_eq!(manager.model_count(&n_snd), 3);
+    println!("!(C => A && !B):\n{}\n", manager.model_enumeration(&n_snd));
+
+    // (C => (A && !B)) <=> !(C => (A && !B)) == False
+    let ff = manager.equiv(&snd, &n_snd);
+    assert_eq!(manager.model_count(&ff), 0);
+    assert!(ff.is_false());
+    println!("False:\n{}\n", manager.model_enumeration(&ff));
+}

sddrs/lib.rs

@@ -11,6 +11,8 @@
 //! * 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.
 //!
+//! **See [examples](https://github.com/jsfpdn/sdd-rs/tree/main/sddrs/examples) for more examples.**
+//!
 //! The following snippet compiles the function `(A ∧ B) ∨ C` to 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.