From 6427e68ed7587c8dce87d6416105164fca2209e6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Fri, 12 Apr 2024 21:57:46 +0200 Subject: [PATCH 01/11] Add documentation for C++ BDD constructors --- src/sylvan_obj.hpp | 45 ++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 40 insertions(+), 5 deletions(-) diff --git a/src/sylvan_obj.hpp b/src/sylvan_obj.hpp index 4b1dc44e..20cd4a09 100644 --- a/src/sylvan_obj.hpp +++ b/src/sylvan_obj.hpp @@ -35,11 +35,46 @@ class Bdd { friend class Mtbdd; public: - Bdd() { bdd = sylvan_false; sylvan_protect(&bdd); } - Bdd(const BDD from) : bdd(from) { sylvan_protect(&bdd); } - Bdd(const Bdd &from) : bdd(from.bdd) { sylvan_protect(&bdd); } - Bdd(const uint32_t var) { bdd = sylvan_ithvar(var); sylvan_protect(&bdd); } - ~Bdd() { sylvan_unprotect(&bdd); } + /** + * @brief Default constructor, representing *False*. + */ + Bdd() + { + bdd = sylvan_false; + sylvan_protect(&bdd); + } + + /** + * @brief Wraps a raw BDD from Sylvan's C interface into a Bdd object. + */ + Bdd(const BDD from) + : bdd(from) + { + sylvan_protect(&bdd); + } + + /** + * @brief Copy construction of another Bdd. + */ + Bdd(const Bdd &from) + : bdd(from.bdd) + { + sylvan_protect(&bdd); + } + + /** + * @brief Construction of the Bdd represnting a variable index in its positive form. + */ + Bdd(const uint32_t var) + { + bdd = sylvan_ithvar(var); + sylvan_protect(&bdd); + } + + ~Bdd() + { + sylvan_unprotect(&bdd); + } /** * @brief Creates a Bdd representing just the variable index in its positive form From 71c13688798ef2cf28907bb227c3c714e3873948 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Fri, 12 Apr 2024 21:59:13 +0200 Subject: [PATCH 02/11] Reuse C-to-CPP constructor --- src/sylvan_obj.hpp | 30 +++++++++++++----------------- 1 file changed, 13 insertions(+), 17 deletions(-) diff --git a/src/sylvan_obj.hpp b/src/sylvan_obj.hpp index 20cd4a09..74b46a5a 100644 --- a/src/sylvan_obj.hpp +++ b/src/sylvan_obj.hpp @@ -35,39 +35,35 @@ class Bdd { friend class Mtbdd; public: - /** - * @brief Default constructor, representing *False*. - */ - Bdd() - { - bdd = sylvan_false; - sylvan_protect(&bdd); - } - /** * @brief Wraps a raw BDD from Sylvan's C interface into a Bdd object. */ Bdd(const BDD from) : bdd(from) { - sylvan_protect(&bdd); + sylvan_protect(&bdd); } /** - * @brief Copy construction of another Bdd. + * @brief Default constructor, representing *False*. */ - Bdd(const Bdd &from) - : bdd(from.bdd) - { - sylvan_protect(&bdd); - } + Bdd() + : Bdd(sylvan_false) + {} /** * @brief Construction of the Bdd represnting a variable index in its positive form. */ Bdd(const uint32_t var) + : Bdd(sylvan_ithvar(var)) + {} + + /** + * @brief Copy construction of another Bdd. + */ + Bdd(const Bdd &from) + : bdd(from.bdd) { - bdd = sylvan_ithvar(var); sylvan_protect(&bdd); } From 01fbe281043be2864f45cb3a2bad1f205cc5f6fd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Fri, 12 Apr 2024 22:04:07 +0200 Subject: [PATCH 03/11] Add move-constructor for BDD class Assuming 'sylvan_protect' has no effect on 'sylvan_false' or some 'invalid' value, then we can further improve performance by removing the 'sylvan_protect' --- src/sylvan_obj.hpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/sylvan_obj.hpp b/src/sylvan_obj.hpp index 74b46a5a..60a2099a 100644 --- a/src/sylvan_obj.hpp +++ b/src/sylvan_obj.hpp @@ -67,6 +67,13 @@ class Bdd { sylvan_protect(&bdd); } + /** + * @brief Move construction from Bdd. + */ + Bdd(Bdd &&from) + : Bdd(from.bdd) + {} + ~Bdd() { sylvan_unprotect(&bdd); From 7c9afa069c67e9168be238b361bb5c90f2b1353e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Fri, 12 Apr 2024 23:35:08 +0200 Subject: [PATCH 04/11] Add move-assignment to Bdd class Nothing is really gained by doing so since Sylvan's protect and unprotect are on the variables, not by use of reference counting. --- src/sylvan_obj.cpp | 7 +++++++ src/sylvan_obj.hpp | 1 + 2 files changed, 8 insertions(+) diff --git a/src/sylvan_obj.cpp b/src/sylvan_obj.cpp index 42d847d3..afa05a90 100644 --- a/src/sylvan_obj.cpp +++ b/src/sylvan_obj.cpp @@ -42,6 +42,13 @@ Bdd::operator=(const Bdd& right) return *this; } +Bdd& +Bdd::operator=(Bdd&& right) +{ + bdd = right.bdd; + return *this; +} + bool Bdd::operator<=(const Bdd& other) const { diff --git a/src/sylvan_obj.hpp b/src/sylvan_obj.hpp index 60a2099a..8226746a 100644 --- a/src/sylvan_obj.hpp +++ b/src/sylvan_obj.hpp @@ -120,6 +120,7 @@ class Bdd { bool operator==(const Bdd& other) const; bool operator!=(const Bdd& other) const; Bdd& operator=(const Bdd& right); + Bdd& operator=(Bdd&& right); bool operator<=(const Bdd& other) const; bool operator>=(const Bdd& other) const; bool operator<(const Bdd& other) const; From f1d315b2f716e7d28e8ba7ca9276b1539ff35c74 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Fri, 12 Apr 2024 22:13:29 +0200 Subject: [PATCH 05/11] Clean up formatting of 'BddSet' and 'BddMap' classes --- src/sylvan_obj.hpp | 82 +++++++++++++++++++++++++++++++++------------- 1 file changed, 60 insertions(+), 22 deletions(-) diff --git a/src/sylvan_obj.hpp b/src/sylvan_obj.hpp index 8226746a..96900231 100644 --- a/src/sylvan_obj.hpp +++ b/src/sylvan_obj.hpp @@ -382,57 +382,69 @@ class BddSet /** * @brief Create a new empty set. */ - BddSet() : set(Bdd::bddOne()) {} + BddSet() + : set(Bdd::bddOne()) + {} /** * @brief Wrap the BDD cube in a set. */ - BddSet(const Bdd &other) : set(other) {} + BddSet(const Bdd &other) + : set(other) + {} /** * @brief Create a copy of the set . */ - BddSet(const BddSet &other) : set(other.set) {} + BddSet(const BddSet &other) + : set(other.set) + {} /** * @brief Add the variable to this set. */ - void add(uint32_t variable) { + void add(uint32_t variable) + { set *= Bdd::bddVar(variable); } /** * @brief Add all variables in the set to this set. */ - void add(BddSet &other) { + void add(BddSet &other) + { set *= other.set; } /** * @brief Remove the variable from this set. */ - void remove(uint32_t variable) { + void remove(uint32_t variable) + { set = set.ExistAbstract(Bdd::bddVar(variable)); } /** * @brief Remove all variables in the set from this set. */ - void remove(BddSet &other) { + void remove(BddSet &other) + { set = set.ExistAbstract(other.set); } /** * @brief Retrieve the head of the set. (The first variable.) */ - uint32_t TopVar() const { + uint32_t TopVar() const + { return set.TopVar(); } /** * @brief Retrieve the tail of the set. (The set containing all but the first variables.) */ - BddSet Next() const { + BddSet Next() const + { Bdd then = set.Then(); return BddSet(then); } @@ -440,14 +452,16 @@ class BddSet /** * @brief Return true if this set is empty, or false otherwise. */ - bool isEmpty() const { + bool isEmpty() const + { return set.isOne(); } /** * @brief Return true if this set contains the variable , or false otherwise. */ - bool contains(uint32_t variable) const { + bool contains(uint32_t variable) const + { if (isEmpty()) return false; else if (TopVar() == variable) return true; else return Next().contains(variable); @@ -456,7 +470,8 @@ class BddSet /** * @brief Return the number of variables in this set. */ - size_t size() const { + size_t size() const + { if (isEmpty()) return 0; else return 1 + Next().size(); } @@ -465,7 +480,8 @@ class BddSet * @brief Create a set containing the variables in . * It is advised to have the variables in in ascending order. */ - static BddSet fromArray(BDDVAR *arr, size_t length) { + static BddSet fromArray(BDDVAR *arr, size_t length) + { BddSet set; for (size_t i = 0; i < length; i++) { set.add(arr[length-i-1]); @@ -477,7 +493,8 @@ class BddSet * @brief Create a set containing the variables in . * It is advised to have the variables in in ascending order. */ - static BddSet fromVector(const std::vector variables) { + static BddSet fromVector(const std::vector variables) + { BddSet set; for (int i=variables.size()-1; i>=0; i--) { set.set *= variables[i]; @@ -489,7 +506,8 @@ class BddSet * @brief Create a set containing the variables in . * It is advised to have the variables in in ascending order. */ - static BddSet fromVector(const std::vector variables) { + static BddSet fromVector(const std::vector variables) + { BddSet set; for (int i=variables.size()-1; i>=0; i--) { set.add(variables[i]); @@ -501,7 +519,8 @@ class BddSet * @brief Write all variables in this set to . * @param arr An array of at least size this.size(). */ - void toArray(BDDVAR *arr) const { + void toArray(BDDVAR *arr) const + { if (!isEmpty()) { *arr = TopVar(); Next().toArray(arr+1); @@ -511,7 +530,8 @@ class BddSet /** * @brief Return the vector of all variables in this set. */ - std::vector toVector() const { + std::vector toVector() const + { std::vector result; Bdd x = set; while (!x.isOne()) { @@ -526,12 +546,30 @@ class BddMap { friend class Bdd; BDD bdd; - BddMap(const BDD from) : bdd(from) { sylvan_protect(&bdd); } - BddMap(const Bdd &from) : bdd(from.bdd) { sylvan_protect(&bdd); } + + BddMap(const BDD from) + : bdd(from) + { + sylvan_protect(&bdd); + } + + BddMap(const Bdd &from) + : BddMap(from.bdd) + {} + public: - BddMap(const BddMap& from) : bdd(from.bdd) { sylvan_protect(&bdd); } - BddMap() : bdd(sylvan_map_empty()) { sylvan_protect(&bdd); } - ~BddMap() { sylvan_unprotect(&bdd); } + BddMap() + : BddMap(sylvan_map_empty()) + {} + + BddMap(const BddMap& from) + : BddMap(from.bdd) + {} + + ~BddMap() + { + sylvan_unprotect(&bdd); + } BddMap(uint32_t key_variable, const Bdd value); From ffd0a008f4e7b85dd7e7df31af79d0c2593e46fc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Fri, 12 Apr 2024 22:17:23 +0200 Subject: [PATCH 06/11] Remove more code-duplication --- src/sylvan_obj.hpp | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/sylvan_obj.hpp b/src/sylvan_obj.hpp index 96900231..33f491ec 100644 --- a/src/sylvan_obj.hpp +++ b/src/sylvan_obj.hpp @@ -62,10 +62,8 @@ class Bdd { * @brief Copy construction of another Bdd. */ Bdd(const Bdd &from) - : bdd(from.bdd) - { - sylvan_protect(&bdd); - } + : Bdd(from.bdd) + {} /** * @brief Move construction from Bdd. From f5551c2ee0bbdeab3f77e11bc854609e9fff49f5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Fri, 12 Apr 2024 22:22:19 +0200 Subject: [PATCH 07/11] Clean up formatting and constructors of 'Mtbdd' and 'MtbddSet' --- src/sylvan_obj.hpp | 71 ++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 62 insertions(+), 9 deletions(-) diff --git a/src/sylvan_obj.hpp b/src/sylvan_obj.hpp index 33f491ec..4de6d012 100644 --- a/src/sylvan_obj.hpp +++ b/src/sylvan_obj.hpp @@ -604,11 +604,40 @@ class Mtbdd { friend class MtbddMap; public: - Mtbdd() { mtbdd = sylvan_false; mtbdd_protect(&mtbdd); } - Mtbdd(const MTBDD from) : mtbdd(from) { mtbdd_protect(&mtbdd); } - Mtbdd(const Mtbdd &from) : mtbdd(from.mtbdd) { mtbdd_protect(&mtbdd); } - Mtbdd(const Bdd &from) : mtbdd(from.bdd) { mtbdd_protect(&mtbdd); } - ~Mtbdd() { mtbdd_unprotect(&mtbdd); } + /** + * @brief Wrap a raw MTBDD from Sylvan's C interface into an Mtbdd object. + */ + Mtbdd(const MTBDD from) + : mtbdd(from) + { + mtbdd_protect(&mtbdd); + } + + /** + * @brief Default construction, representing the Boolean *False*. + */ + Mtbdd() + : Mtbdd(sylvan_false) + {} + + /** + * @brief Copy construction + */ + Mtbdd(const Mtbdd &from) + : Mtbdd(from.mtbdd) + {} + + /** + * @brief Conversion construction from Bdd object. + */ + Mtbdd(const Bdd &from) + : Mtbdd(from.bdd) + {} + + ~Mtbdd() + { + mtbdd_unprotect(&mtbdd); + } /** * @brief Creates a Mtbdd leaf representing the int64 value @@ -861,11 +890,35 @@ class MtbddMap { friend class Mtbdd; MTBDD mtbdd; - MtbddMap(MTBDD from) : mtbdd(from) { mtbdd_protect(&mtbdd); } - MtbddMap(Mtbdd &from) : mtbdd(from.mtbdd) { mtbdd_protect(&mtbdd); } + + /** + * @brief Wrap a raw MTBDD from Sylvan's C interface into an MtbddMap object. + */ + MtbddMap(MTBDD from) + : mtbdd(from) + { + mtbdd_protect(&mtbdd); + } + + /** + * @brief Conversion construction + */ + MtbddMap(Mtbdd &from) + : MtbddMap(from.mtbdd) + {} + public: - MtbddMap() : mtbdd(mtbdd_map_empty()) { mtbdd_protect(&mtbdd); } - ~MtbddMap() { mtbdd_unprotect(&mtbdd); } + /** + * @brief Default construction of an empty map. + */ + MtbddMap() + : MtbddMap(mtbdd_map_empty()) + {} + + ~MtbddMap() + { + mtbdd_unprotect(&mtbdd); + } MtbddMap(uint32_t key_variable, Mtbdd value); From dd6b412f72af19d074f42f77230bfc76677cae48 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Fri, 12 Apr 2024 23:24:18 +0200 Subject: [PATCH 08/11] Add move constructor for Mtbdd class Similar to the Bdd class, we have to remember to protect the new 'sylvan_false' to not mess up anything when 'sylvan_unprotect' is called during the destructor. --- src/sylvan_obj.hpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/sylvan_obj.hpp b/src/sylvan_obj.hpp index 4de6d012..94558c28 100644 --- a/src/sylvan_obj.hpp +++ b/src/sylvan_obj.hpp @@ -627,6 +627,13 @@ class Mtbdd { : Mtbdd(from.mtbdd) {} + /** + * @brief Move construction + */ + Mtbdd(Mtbdd &&from) + : Mtbdd(from.mtbdd) + {} + /** * @brief Conversion construction from Bdd object. */ From f67d82bf36de18b4428450a8b34e06c53ad7a1db Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Fri, 12 Apr 2024 23:46:17 +0200 Subject: [PATCH 09/11] Change 'Bdd::_=(...)' operators to reuse binary and assignment operators This way, the code for dealing with protection is only taken care of in a single place. Furthermore, there are no code-duplications for the meaning of each operator. Finally, the assignment should use the new move-assignment --- src/sylvan_obj.cpp | 18 ++++++------------ 1 file changed, 6 insertions(+), 12 deletions(-) diff --git a/src/sylvan_obj.cpp b/src/sylvan_obj.cpp index afa05a90..1503a215 100644 --- a/src/sylvan_obj.cpp +++ b/src/sylvan_obj.cpp @@ -95,8 +95,7 @@ Bdd::operator*(const Bdd& other) const Bdd& Bdd::operator*=(const Bdd& other) { - bdd = sylvan_and(bdd, other.bdd); - return *this; + return (*this = *this * other); } Bdd @@ -108,8 +107,7 @@ Bdd::operator&(const Bdd& other) const Bdd& Bdd::operator&=(const Bdd& other) { - bdd = sylvan_and(bdd, other.bdd); - return *this; + return (*this = *this & other); } Bdd @@ -121,8 +119,7 @@ Bdd::operator+(const Bdd& other) const Bdd& Bdd::operator+=(const Bdd& other) { - bdd = sylvan_or(bdd, other.bdd); - return *this; + return (*this = *this + other); } Bdd @@ -134,8 +131,7 @@ Bdd::operator|(const Bdd& other) const Bdd& Bdd::operator|=(const Bdd& other) { - bdd = sylvan_or(bdd, other.bdd); - return *this; + return (*this = *this | other); } Bdd @@ -147,8 +143,7 @@ Bdd::operator^(const Bdd& other) const Bdd& Bdd::operator^=(const Bdd& other) { - bdd = sylvan_xor(bdd, other.bdd); - return *this; + return (*this = *this ^ other); } Bdd @@ -160,8 +155,7 @@ Bdd::operator-(const Bdd& other) const Bdd& Bdd::operator-=(const Bdd& other) { - bdd = sylvan_and(bdd, sylvan_not(other.bdd)); - return *this; + return (*this = *this - other); } Bdd From f0dc35a6974a992af86679f2e8b3846764e53e7e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Sat, 13 Apr 2024 00:00:01 +0200 Subject: [PATCH 10/11] Add move-assignment to Mtbdd class Again, nothing is really gained from doing so except more code. --- src/sylvan_obj.cpp | 7 +++++++ src/sylvan_obj.hpp | 1 + 2 files changed, 8 insertions(+) diff --git a/src/sylvan_obj.cpp b/src/sylvan_obj.cpp index 1503a215..fc4199f5 100644 --- a/src/sylvan_obj.cpp +++ b/src/sylvan_obj.cpp @@ -754,6 +754,13 @@ Mtbdd::operator=(const Mtbdd& right) return *this; } +Mtbdd& +Mtbdd::operator=(Mtbdd&& right) +{ + mtbdd = right.mtbdd; + return *this; +} + Mtbdd Mtbdd::operator!() const { diff --git a/src/sylvan_obj.hpp b/src/sylvan_obj.hpp index 94558c28..b3c42c8c 100644 --- a/src/sylvan_obj.hpp +++ b/src/sylvan_obj.hpp @@ -711,6 +711,7 @@ class Mtbdd { bool operator==(const Mtbdd& other) const; bool operator!=(const Mtbdd& other) const; Mtbdd& operator=(const Mtbdd& right); + Mtbdd& operator=(Mtbdd&& right); Mtbdd operator!() const; Mtbdd operator~() const; Mtbdd operator*(const Mtbdd& other) const; From 1d5066a0cc489c35d5c9218630cadcc9dcca717f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Steffan=20S=C3=B8lvsten?= Date: Sat, 13 Apr 2024 00:03:08 +0200 Subject: [PATCH 11/11] Change 'Mtbdd::_=(...)' operators to reuse binary and assignment operators This way, the code for dealing with protection is only taken care of in a single place. Furthermore, there are no code-duplications for the meaning of each operator. Finally, the assignment should use the new move-assignment --- src/sylvan_obj.cpp | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/sylvan_obj.cpp b/src/sylvan_obj.cpp index fc4199f5..3d4a69a6 100644 --- a/src/sylvan_obj.cpp +++ b/src/sylvan_obj.cpp @@ -782,8 +782,7 @@ Mtbdd::operator*(const Mtbdd& other) const Mtbdd& Mtbdd::operator*=(const Mtbdd& other) { - mtbdd = mtbdd_times(mtbdd, other.mtbdd); - return *this; + return (*this = *this * other); } Mtbdd @@ -795,8 +794,7 @@ Mtbdd::operator+(const Mtbdd& other) const Mtbdd& Mtbdd::operator+=(const Mtbdd& other) { - mtbdd = mtbdd_plus(mtbdd, other.mtbdd); - return *this; + return (*this = *this + other); } Mtbdd @@ -808,8 +806,7 @@ Mtbdd::operator-(const Mtbdd& other) const Mtbdd& Mtbdd::operator-=(const Mtbdd& other) { - mtbdd = mtbdd_minus(mtbdd, other.mtbdd); - return *this; + return (*this = *this - other); } Mtbdd