Skip to content

Commit

Permalink
fix: Cargo.toml: keywords
Browse files Browse the repository at this point in the history
  • Loading branch information
jsfpdn committed Dec 15, 2024
1 parent a61801a commit 875419c
Show file tree
Hide file tree
Showing 3 changed files with 44 additions and 51 deletions.
1 change: 1 addition & 0 deletions Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -8,3 +8,4 @@ unsafe_code = "forbid"
[workspace.lints.clippy]
mutable_key_type = "allow"
module_inception = "allow"
doc_markdown = "allow"
6 changes: 3 additions & 3 deletions sddrs/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,11 @@ authors = ["Josef Podany"]
repository = "https://github.com/jsfpdn/sdd-rs"
description = "Bottom-up Sentential Decision Diagram compiler library."
keywords = [
"knowledge-compilation",
"knowledge-base",
"boolean-functions",
"sentential-decision-diagrams",
"decision-diagrams",
"model-counting",
"satisfiability",
"sdd",
]
categories = ["compilers", "data-structures", "mathematics"]
license = "BSD-3-Clause"
Expand Down
88 changes: 40 additions & 48 deletions sddrs/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -9,13 +9,7 @@
//! * 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.
//!
//!
//!
//!
//!
//! * SDD compilation from CNF in [DIMACS](https://www21.in.tum.de/~lammich/2015_SS_Seminar_SAT/resources/dimacs-cnf.pdf) format.
//!
//! The following snippet compiles the function `(A ∧ B) ∨ C` to SDD,
//! computes number of its models, enumerates and prints them to the stdout,
Expand All @@ -26,47 +20,45 @@
//! 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".to_string()])
//! .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}'");
//! }
//! 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".to_string()])
//! .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}'");
//! ```
//!
//! ---
Expand Down

0 comments on commit 875419c

Please sign in to comment.