From 8b121d1a534ac21a2238e7f927f3672d6ceb1587 Mon Sep 17 00:00:00 2001 From: Nils Husung Date: Sat, 20 Apr 2024 14:52:44 +0200 Subject: [PATCH 1/3] Fix: Unique pairs for commutative operators (apply cache) The bug did not lead to incorrect results but has probably affected performance in a negative way. Thanks @TarVK! --- crates/oxidd-rules-bdd/src/simple/mod.rs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/crates/oxidd-rules-bdd/src/simple/mod.rs b/crates/oxidd-rules-bdd/src/simple/mod.rs index dc8356a..27274ac 100644 --- a/crates/oxidd-rules-bdd/src/simple/mod.rs +++ b/crates/oxidd-rules-bdd/src/simple/mod.rs @@ -234,7 +234,7 @@ fn terminal_bin<'a, M: Manager, const OP: u8>( match (m.get_node(f), m.get_node(g)) { // Unique representation of {f, g} for commutative functions (Inner(_), Inner(_)) if f > g => Binary(BDDOp::And, g.borrowed(), f.borrowed()), - (Inner(_), Inner(_)) => Binary(BDDOp::And, g.borrowed(), f.borrowed()), + (Inner(_), Inner(_)) => Binary(BDDOp::And, f.borrowed(), g.borrowed()), (Terminal(t), _) | (_, Terminal(t)) if *t.borrow() == False => { Done(m.get_terminal(False).unwrap()) } @@ -247,7 +247,7 @@ fn terminal_bin<'a, M: Manager, const OP: u8>( } match (m.get_node(f), m.get_node(g)) { (Inner(_), Inner(_)) if f > g => Binary(BDDOp::Or, g.borrowed(), f.borrowed()), - (Inner(_), Inner(_)) => Binary(BDDOp::Or, g.borrowed(), f.borrowed()), + (Inner(_), Inner(_)) => Binary(BDDOp::Or, f.borrowed(), g.borrowed()), (Terminal(t), _) | (_, Terminal(t)) if *t.borrow() == True => { Done(m.get_terminal(True).unwrap()) } @@ -260,7 +260,7 @@ fn terminal_bin<'a, M: Manager, const OP: u8>( } match (m.get_node(f), m.get_node(g)) { (Inner(_), Inner(_)) if f > g => Binary(BDDOp::Nand, g.borrowed(), f.borrowed()), - (Inner(_), Inner(_)) => Binary(BDDOp::Nand, g.borrowed(), f.borrowed()), + (Inner(_), Inner(_)) => Binary(BDDOp::Nand, f.borrowed(), g.borrowed()), (Terminal(t), _) | (_, Terminal(t)) if *t.borrow() == False => { Done(m.get_terminal(True).unwrap()) } @@ -273,7 +273,7 @@ fn terminal_bin<'a, M: Manager, const OP: u8>( } match (m.get_node(f), m.get_node(g)) { (Inner(_), Inner(_)) if f > g => Binary(BDDOp::Nor, g.borrowed(), f.borrowed()), - (Inner(_), Inner(_)) => Binary(BDDOp::Nor, g.borrowed(), f.borrowed()), + (Inner(_), Inner(_)) => Binary(BDDOp::Nor, f.borrowed(), g.borrowed()), (Terminal(t), _) | (_, Terminal(t)) if *t.borrow() == True => { Done(m.get_terminal(False).unwrap()) } From 82e45315a54ebfb59505c94e2f64d2ef32f4a19a Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 15 Apr 2024 17:33:55 +0200 Subject: [PATCH 2/3] Use consistent type size_t for node_count() in C++ bindings --- bindings/cpp/include/oxidd/bcdd.hpp | 2 +- bindings/cpp/include/oxidd/bdd.hpp | 2 +- bindings/cpp/include/oxidd/concepts.hpp | 1 + bindings/cpp/include/oxidd/zbdd.hpp | 2 +- 4 files changed, 4 insertions(+), 3 deletions(-) diff --git a/bindings/cpp/include/oxidd/bcdd.hpp b/bindings/cpp/include/oxidd/bcdd.hpp index 20b8a62..024114b 100644 --- a/bindings/cpp/include/oxidd/bcdd.hpp +++ b/bindings/cpp/include/oxidd/bcdd.hpp @@ -509,7 +509,7 @@ class bcdd_function { /// Locking behavior: acquires a shared manager lock. /// /// @returns Node count including the terminal node - [[nodiscard]] size_t node_count() const noexcept { + [[nodiscard]] std::size_t node_count() const noexcept { assert(_func._p); return capi::oxidd_bcdd_node_count(_func); } diff --git a/bindings/cpp/include/oxidd/bdd.hpp b/bindings/cpp/include/oxidd/bdd.hpp index e720c57..582f32b 100644 --- a/bindings/cpp/include/oxidd/bdd.hpp +++ b/bindings/cpp/include/oxidd/bdd.hpp @@ -507,7 +507,7 @@ class bdd_function { /// Locking behavior: acquires a shared manager lock. /// /// @returns Node count including the two terminal nodes - [[nodiscard]] uint64_t node_count() const noexcept { + [[nodiscard]] std::size_t node_count() const noexcept { assert(_func._p); return capi::oxidd_bdd_node_count(_func); } diff --git a/bindings/cpp/include/oxidd/concepts.hpp b/bindings/cpp/include/oxidd/concepts.hpp index 4f6a6cf..71f628a 100644 --- a/bindings/cpp/include/oxidd/concepts.hpp +++ b/bindings/cpp/include/oxidd/concepts.hpp @@ -5,6 +5,7 @@ #if __cplusplus >= 202002L #include +#include #include #include #include diff --git a/bindings/cpp/include/oxidd/zbdd.hpp b/bindings/cpp/include/oxidd/zbdd.hpp index 112cbcf..71943a6 100644 --- a/bindings/cpp/include/oxidd/zbdd.hpp +++ b/bindings/cpp/include/oxidd/zbdd.hpp @@ -545,7 +545,7 @@ class zbdd_function { /// Locking behavior: acquires a shared manager lock. /// /// @returns Node count including the two terminal nodes - [[nodiscard]] uint64_t node_count() const noexcept { + [[nodiscard]] std::size_t node_count() const noexcept { assert(_func._p); return capi::oxidd_zbdd_node_count(_func); } From 4a5a7b884a5d721a9bbfaef068486ac7827bb541 Mon Sep 17 00:00:00 2001 From: Nils Husung Date: Sat, 20 Apr 2024 15:11:58 +0200 Subject: [PATCH 3/3] cSpell config: also ignore .git file (for worktrees) --- .cspell.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.cspell.json b/.cspell.json index ecb9d2e..1368cf9 100644 --- a/.cspell.json +++ b/.cspell.json @@ -5,7 +5,7 @@ "ignorePaths": [ "/.cache/", "/.cspellcache", - "/.git/", + "/.git", "/.project-words.txt", "/build/", "/doc/book/book/",