From fb4c103320f69eec1c87bf2d1c5e80a8dad21ff2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 30 Nov 2015 13:27:26 +0100 Subject: [PATCH] merged sylvan updates into the sylvan copy. made more tests work Former-commit-id: 18023e03c25492e585abae491a9096cf8928f385 --- resources/3rdparty/sylvan/src/llmsset.c | 14 +- resources/3rdparty/sylvan/src/refs.h | 2 +- resources/3rdparty/sylvan/src/sylvan_bdd.h | 5 +- resources/3rdparty/sylvan/src/sylvan_common.c | 1 + resources/3rdparty/sylvan/src/sylvan_common.h | 5 - resources/3rdparty/sylvan/src/sylvan_obj.cpp | 173 +-- resources/3rdparty/sylvan/src/sylvan_obj.hpp | 1364 ++++++++--------- src/storage/dd/Add.cpp | 4 +- src/storage/dd/cudd/InternalCuddAdd.cpp | 4 +- src/storage/dd/cudd/InternalCuddAdd.h | 2 +- src/storage/dd/cudd/InternalCuddBdd.cpp | 5 + src/storage/dd/sylvan/InternalSylvanAdd.cpp | 24 +- src/storage/dd/sylvan/InternalSylvanAdd.h | 4 +- test/functional/storage/CuddDdTest.cpp | 2 +- test/functional/storage/SylvanDdTest.cpp | 184 ++- 15 files changed, 834 insertions(+), 959 deletions(-) diff --git a/resources/3rdparty/sylvan/src/llmsset.c b/resources/3rdparty/sylvan/src/llmsset.c index b97d092cf..3e1e54b6a 100644 --- a/resources/3rdparty/sylvan/src/llmsset.c +++ b/resources/3rdparty/sylvan/src/llmsset.c @@ -53,14 +53,6 @@ VOID_TASK_0(llmsset_reset_region) SET_THREAD_LOCAL(my_region, my_region); } -VOID_TASK_0(llmsset_init_worker) -{ - // yes, ugly. for now, we use a global thread-local value. - // that is a problem with multiple tables. - // so, for now, do NOT use multiple tables!! - CALL(llmsset_reset_region); -} - static uint64_t claim_data_bucket(const llmsset_t dbs) { @@ -385,9 +377,13 @@ llmsset_create(size_t initial_size, size_t max_size) dbs->create_cb = NULL; dbs->destroy_cb = NULL; + // yes, ugly. for now, we use a global thread-local value. + // that is a problem with multiple tables. + // so, for now, do NOT use multiple tables!! + LACE_ME; INIT_THREAD_LOCAL(my_region); - TOGETHER(llmsset_init_worker); + TOGETHER(llmsset_reset_region); return dbs; } diff --git a/resources/3rdparty/sylvan/src/refs.h b/resources/3rdparty/sylvan/src/refs.h index aaf20bec0..928948c90 100644 --- a/resources/3rdparty/sylvan/src/refs.h +++ b/resources/3rdparty/sylvan/src/refs.h @@ -14,8 +14,8 @@ * limitations under the License. */ +#include #include // for uint32_t etc -#include "sylvan_config.h" #ifndef REFS_INLINE_H #define REFS_INLINE_H diff --git a/resources/3rdparty/sylvan/src/sylvan_bdd.h b/resources/3rdparty/sylvan/src/sylvan_bdd.h index 8ef6a27f0..78c8f5772 100644 --- a/resources/3rdparty/sylvan/src/sylvan_bdd.h +++ b/resources/3rdparty/sylvan/src/sylvan_bdd.h @@ -16,7 +16,7 @@ /* Do not include this file directly. Instead, include sylvan.h */ -#include "tls.h" +#include #ifndef SYLVAN_BDD_H #define SYLVAN_BDD_H @@ -263,13 +263,10 @@ void sylvan_getsha(BDD bdd, char *target); // target must be at least 65 bytes.. /** * Calculate number of satisfying variable assignments. * The set of variables must be >= the support of the BDD. - * - * The cached version uses the operation cache, but is limited to 64-bit floating point numbers. */ TASK_DECL_3(double, sylvan_satcount, BDD, BDDSET, BDDVAR); #define sylvan_satcount(bdd, variables) CALL(sylvan_satcount, bdd, variables, 0) -#define sylvan_satcount_cached(bdd, variables) CALL(sylvan_satcount, bdd, variables, 0) /** * Create a BDD cube representing the conjunction of variables in their positive or negative diff --git a/resources/3rdparty/sylvan/src/sylvan_common.c b/resources/3rdparty/sylvan/src/sylvan_common.c index ee6af34a4..aa0374a7b 100644 --- a/resources/3rdparty/sylvan/src/sylvan_common.c +++ b/resources/3rdparty/sylvan/src/sylvan_common.c @@ -16,6 +16,7 @@ #include +#include #include #ifndef cas diff --git a/resources/3rdparty/sylvan/src/sylvan_common.h b/resources/3rdparty/sylvan/src/sylvan_common.h index 97bbf50c6..61f34cc5b 100644 --- a/resources/3rdparty/sylvan/src/sylvan_common.h +++ b/resources/3rdparty/sylvan/src/sylvan_common.h @@ -14,11 +14,6 @@ * limitations under the License. */ -#include -#include "sylvan.h" -#include "tls.h" -#include "sylvan_config.h" - #ifndef SYLVAN_COMMON_H #define SYLVAN_COMMON_H diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.cpp b/resources/3rdparty/sylvan/src/sylvan_obj.cpp index 649b6cfd4..7cf5960fb 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.cpp @@ -14,7 +14,7 @@ * limitations under the License. */ -#include "sylvan_obj.hpp" +#include using namespace sylvan; @@ -296,13 +296,13 @@ Bdd Bdd::Permute(const std::vector& from, const std::vector& to) const { LACE_ME; - + /* Create a map */ BddMap map; for (int i=from.size()-1; i>=0; i--) { map.put(from[i].TopVar(), to[i]); } - + return sylvan_compose(bdd, map.bdd); } @@ -340,10 +340,19 @@ Bdd::GetShaHash() const } double -Bdd::SatCount(size_t variableCount) const +Bdd::SatCount(const Bdd &variables) const { LACE_ME; - return mtbdd_satcount(bdd, variableCount); + return sylvan_satcount(bdd, variables.bdd); +} + + +double +Bdd::SatCount(size_t nvars) const +{ + LACE_ME; + // Note: the mtbdd_satcount can be called without initializing the MTBDD module. + return mtbdd_satcount(bdd, nvars); } void @@ -357,12 +366,12 @@ std::vector Bdd::PickOneCube(const Bdd &variables) const { std::vector result = std::vector(); - + BDD bdd = this->bdd; BDD vars = variables.bdd; - + if (bdd == sylvan_false) return result; - + for (; !sylvan_set_isempty(vars); vars = sylvan_set_next(vars)) { uint32_t var = sylvan_set_var(vars); if (bdd == sylvan_true) { @@ -385,7 +394,7 @@ Bdd::PickOneCube(const Bdd &variables) const } } } - + return result; } @@ -443,12 +452,6 @@ Bdd::NodeCount() const return sylvan_nodecount(bdd); } -Mtbdd -Bdd::toDoubleMtbdd() const { - LACE_ME; - return mtbdd_bool_to_double(bdd); -} - Bdd Bdd::bddOne() { @@ -730,14 +733,6 @@ Mtbdd::Plus(const Mtbdd &other) const return mtbdd_plus(mtbdd, other.mtbdd); } -Mtbdd -Mtbdd::Minus(const Mtbdd &other) const -{ - LACE_ME; - return mtbdd_minus(mtbdd, other.mtbdd); -} - - Mtbdd Mtbdd::Times(const Mtbdd &other) const { @@ -745,13 +740,6 @@ Mtbdd::Times(const Mtbdd &other) const return mtbdd_times(mtbdd, other.mtbdd); } -Mtbdd -Mtbdd::Divide(const Mtbdd &other) const -{ - LACE_ME; - return mtbdd_divide(mtbdd, other.mtbdd); -} - Mtbdd Mtbdd::Min(const Mtbdd &other) const { @@ -905,101 +893,29 @@ Mtbdd::BddStrictThreshold(double value) const return mtbdd_strict_threshold_double(mtbdd, value); } -Bdd -Mtbdd::NotZero() const -{ - LACE_ME; - return mtbdd_not_zero(mtbdd); -} - -Bdd -Mtbdd::Equals(const Mtbdd& other) const { - LACE_ME; - return mtbdd_equals(mtbdd, other.mtbdd); -} - -Bdd -Mtbdd::Less(const Mtbdd& other) const { - LACE_ME; - return mtbdd_less_as_bdd(mtbdd, other.mtbdd); -} - -Bdd -Mtbdd::LessOrEqual(const Mtbdd& other) const { - LACE_ME; - return mtbdd_less_or_equal_as_bdd(mtbdd, other.mtbdd); -} - -double -Mtbdd::getDoubleMax() const { - LACE_ME; - MTBDD maxNode = mtbdd_maximum(mtbdd); - return mtbdd_getdouble(maxNode); -} - -double -Mtbdd::getDoubleMin() const { - LACE_ME; - MTBDD minNode = mtbdd_minimum(mtbdd); - return mtbdd_getdouble(minNode); -} - -bool -Mtbdd::EqualNorm(const Mtbdd& other, double epsilon) const { - LACE_ME; - return mtbdd_equal_norm_d(mtbdd, other.mtbdd, epsilon); -} - -bool -Mtbdd::EqualNormRel(const Mtbdd& other, double epsilon) const { - LACE_ME; - return mtbdd_equal_norm_rel_d(mtbdd, other.mtbdd, epsilon); -} - -Mtbdd -Mtbdd::Floor() const { - LACE_ME; - return mtbdd_floor(mtbdd); -} - -Mtbdd -Mtbdd::Ceil() const { - LACE_ME; - return mtbdd_ceil(mtbdd); -} - Mtbdd -Mtbdd::Pow(const Mtbdd& other) const { +Mtbdd::Support() const +{ LACE_ME; - return mtbdd_pow(mtbdd, other.mtbdd); + return mtbdd_support(mtbdd); } -Mtbdd -Mtbdd::Mod(const Mtbdd& other) const { - LACE_ME; - return mtbdd_mod(mtbdd, other.mtbdd); +MTBDD +Mtbdd::GetMTBDD() const +{ + return mtbdd; } Mtbdd -Mtbdd::Logxy(const Mtbdd& other) const { - LACE_ME; - return mtbdd_logxy(mtbdd, other.mtbdd); -} - -size_t -Mtbdd::CountLeaves() const { - LACE_ME; - return mtbdd_leafcount(mtbdd); -} - -double -Mtbdd::NonZeroCount(size_t variableCount) const { +Mtbdd::Compose(MtbddMap &m) const +{ LACE_ME; - return mtbdd_non_zero_count(mtbdd, variableCount); + return mtbdd_compose(mtbdd, m.mtbdd); } Mtbdd -Mtbdd::Permute(const std::vector& from, const std::vector& to) const { +Mtbdd::Permute(const std::vector& from, const std::vector& to) const +{ LACE_ME; /* Create a map */ @@ -1008,34 +924,20 @@ Mtbdd::Permute(const std::vector& from, const std::vector& to) const { map.put(from[i].TopVar(), to[i]); } - return sylvan_compose(mtbdd, map.mtbdd); -} - -Mtbdd -Mtbdd::Support() const -{ - LACE_ME; - return mtbdd_support(mtbdd); -} - -MTBDD -Mtbdd::GetMTBDD() const -{ - return mtbdd; + return mtbdd_compose(mtbdd, map.mtbdd); } -Mtbdd -Mtbdd::Compose(MtbddMap &m) const +double +Mtbdd::SatCount(size_t nvars) const { LACE_ME; - return mtbdd_compose(mtbdd, m.mtbdd); + return mtbdd_satcount(mtbdd, nvars); } double -Mtbdd::SatCount(size_t variableCount) const +Mtbdd::SatCount(const Mtbdd &variables) const { - LACE_ME; - return mtbdd_satcount(mtbdd, variableCount); + return SatCount(sylvan_set_count(variables.mtbdd)); } size_t @@ -1045,6 +947,7 @@ Mtbdd::NodeCount() const return mtbdd_nodecount(mtbdd); } + /*** * Implementation of class MtbddMap */ @@ -1132,3 +1035,5 @@ Sylvan::quitPackage() { sylvan_quit(); } + +#include "sylvan_obj_storm.cpp" diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.hpp b/resources/3rdparty/sylvan/src/sylvan_obj.hpp index 6f926ec4b..46670ae73 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.hpp @@ -20,713 +20,685 @@ #include #include -#include "lace.h" -#include "sylvan.h" +#include +#include namespace sylvan { - -class BddMap; - -class Mtbdd; - -class Bdd { - friend class Sylvan; - friend class BddMap; - 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 Creates a Bdd representing just the variable index in its positive form - * The variable index must be a 0<=index<=2^23 (we use 24 bits internally) - */ - static Bdd bddVar(uint32_t index); - - /** - * @brief Returns the Bdd representing "True" - */ - static Bdd bddOne(); - - /** - * @brief Returns the Bdd representing "False" - */ - static Bdd bddZero(); - - /** - * @brief Returns the Bdd representing a cube of variables, according to the given values. - * @param variables the variables that will be in the cube in their positive or negative form - * @param values a character array describing how the variables will appear in the result - * The length of string must be equal to the number of variables in the cube. - * For every ith char in string, if it is 0, the corresponding variable will appear in its negative form, - * if it is 1, it will appear in its positive form, and if it is 2, it will appear as "any", thus it will - * be skipped. - */ - static Bdd bddCube(const Bdd &variables, unsigned char *values); - - /** - * @brief Returns the Bdd representing a cube of variables, according to the given values. - * @param variables the variables that will be in the cube in their positive or negative form - * @param string a character array describing how the variables will appear in the result - * The length of string must be equal to the number of variables in the cube. - * For every ith char in string, if it is 0, the corresponding variable will appear in its negative form, - * if it is 1, it will appear in its positive form, and if it is 2, it will appear as "any", thus it will - * be skipped. - */ - static Bdd bddCube(const Bdd &variables, std::vector values); - - int operator==(const Bdd& other) const; - int operator!=(const Bdd& other) const; - Bdd operator=(const Bdd& right); - int operator<=(const Bdd& other) const; - int operator>=(const Bdd& other) const; - int operator<(const Bdd& other) const; - int operator>(const Bdd& other) const; - Bdd operator!() const; - Bdd operator~() const; - Bdd operator*(const Bdd& other) const; - Bdd operator*=(const Bdd& other); - Bdd operator&(const Bdd& other) const; - Bdd operator&=(const Bdd& other); - Bdd operator+(const Bdd& other) const; - Bdd operator+=(const Bdd& other); - Bdd operator|(const Bdd& other) const; - Bdd operator|=(const Bdd& other); - Bdd operator^(const Bdd& other) const; - Bdd operator^=(const Bdd& other); - Bdd operator-(const Bdd& other) const; - Bdd operator-=(const Bdd& other); - - /** - * @brief Returns non-zero if this Bdd is bddOne() or bddZero() - */ - int isConstant() const; - - /** - * @brief Returns non-zero if this Bdd is bddOne() or bddZero() - */ - int isTerminal() const; - - /** - * @brief Returns non-zero if this Bdd is bddOne() - */ - int isOne() const; - - /** - * @brief Returns non-zero if this Bdd is bddZero() - */ - int isZero() const; - - /** - * @brief Returns the top variable index of this Bdd (the variable in the root node) - */ - uint32_t TopVar() const; - - /** - * @brief Follows the high edge ("then") of the root node of this Bdd - */ - Bdd Then() const; - - /** - * @brief Follows the low edge ("else") of the root node of this Bdd - */ - Bdd Else() const; - - /** - * @brief Computes \exists cube: f \and g - */ - Bdd AndAbstract(const Bdd& g, const Bdd& cube) const; - - /** - * @brief Computes \exists cube: f - */ - Bdd ExistAbstract(const Bdd& cube) const; - - /** - * @brief Computes \forall cube: f - */ - Bdd UnivAbstract(const Bdd& cube) const; - - /** - * @brief Computes if f then g else h - */ - Bdd Ite(const Bdd& g, const Bdd& h) const; - - /** - * @brief Computes f \and g - */ - Bdd And(const Bdd& g) const; - - /** - * @brief Computes f \or g - */ - Bdd Or(const Bdd& g) const; - - /** - * @brief Computes \not (f \and g) - */ - Bdd Nand(const Bdd& g) const; - - /** - * @brief Computes \not (f \or g) - */ - Bdd Nor(const Bdd& g) const; - - /** - * @brief Computes f \xor g - */ - Bdd Xor(const Bdd& g) const; - - /** - * @brief Computes \not (f \xor g), i.e. f \equiv g - */ - Bdd Xnor(const Bdd& g) const; - - /** - * @brief Returns whether all elements in f are also in g - */ - int Leq(const Bdd& g) const; - - /** - * @brief Computes the reverse application of a transition relation to this set. - * @param relation the transition relation to apply - * @param cube the variables that are in the transition relation - * This function assumes that s,t are interleaved with s odd and t even. - * Other variables in the relation are ignored (by existential quantification) - * Set cube to "false" (illegal cube) to assume all encountered variables are in s,t - * - * Use this function to concatenate two relations --> --> - * or to take the 'previous' of a set --> S - */ - Bdd RelPrev(const Bdd& relation, const Bdd& cube) const; - - /** - * @brief Computes the application of a transition relation to this set. - * @param relation the transition relation to apply - * @param cube the variables that are in the transition relation - * This function assumes that s,t are interleaved with s odd and t even. - * Other variables in the relation are ignored (by existential quantification) - * Set cube to "false" (illegal cube) to assume all encountered variables are in s,t - * - * Use this function to take the 'next' of a set S --> - */ - Bdd RelNext(const Bdd& relation, const Bdd& cube) const; - - /** - * @brief Computes the transitive closure by traversing the BDD recursively. - * See Y. Matsunaga, P. C. McGeer, R. K. Brayton - * On Computing the Transitive Closre of a State Transition Relation - * 30th ACM Design Automation Conference, 1993. - */ - Bdd Closure() const; - - /** - * @brief Computes the constrain f @ c - */ - Bdd Constrain(const Bdd &c) const; - - /** - * @brief Computes the BDD restrict according to Coudert and Madre's algorithm (ICCAD90). - */ - Bdd Restrict(const Bdd &c) const; - - /** - * @brief Functional composition. Whenever a variable v in the map m is found in the BDD, - * it is substituted by the associated function. - * You can also use this function to implement variable reordering. - */ - Bdd Compose(const BddMap &m) const; - - /** - * @brief Substitute all variables in the array from by the corresponding variables in to. - */ - Bdd Permute(const std::vector& from, const std::vector& to) const; - - /** - * @brief Computes the support of a Bdd. - */ - Bdd Support() const; - - /** - * @brief Gets the BDD of this Bdd (for C functions) - */ - BDD GetBDD() const; - - /** - * @brief Writes .dot file of this Bdd. Not thread-safe! - */ - void PrintDot(FILE *out) const; - - /** - * @brief Gets a SHA2 hash that describes the structure of this Bdd. - * @param string a character array of at least 65 characters (includes zero-termination) - * This hash is 64 characters long and is independent of the memory locations of BDD nodes. - */ - void GetShaHash(char *string) const; - - std::string GetShaHash() const; - - /** - * @brief Computes the number of satisfying variable assignments, using variables in cube. - */ - double SatCount(size_t variableCount) const; - - /** - * @brief Gets one satisfying assignment according to the variables. - * @param variables The set of variables to be assigned, must include the support of the Bdd. - */ - void PickOneCube(const Bdd &variables, uint8_t *string) const; - - /** - * @brief Gets one satisfying assignment according to the variables. - * @param variables The set of variables to be assigned, must include the support of the Bdd. - * Returns an empty vector when either this Bdd equals bddZero() or the cube is empty. - */ - std::vector PickOneCube(const Bdd &variables) const; - - /** - * @brief Gets a cube that satisfies this Bdd. - */ - Bdd PickOneCube() const; - - /** - * @brief Faster version of: *this + Sylvan::bddCube(variables, values); - */ - Bdd UnionCube(const Bdd &variables, uint8_t *values) const; - - /** - * @brief Faster version of: *this + Sylvan::bddCube(variables, values); - */ - Bdd UnionCube(const Bdd &variables, std::vector values) const; - - /** - * @brief Generate a cube representing a set of variables - */ - static Bdd VectorCube(const std::vector variables); - - /** - * @brief Generate a cube representing a set of variables - * @param variables An sorted set of variable indices - */ - static Bdd VariablesCube(const std::vector variables); - - /** - * @brief Gets the number of nodes in this Bdd. Not thread-safe! - */ - size_t NodeCount() const; - - Mtbdd toDoubleMtbdd() const; - -private: - BDD bdd; -}; - -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); } -public: - BddMap() : bdd(sylvan_map_empty()) { sylvan_protect(&bdd); } - ~BddMap() { sylvan_unprotect(&bdd); } - - BddMap(uint32_t key_variable, const Bdd value); - - BddMap operator+(const Bdd& other) const; - BddMap operator+=(const Bdd& other); - BddMap operator-(const Bdd& other) const; - BddMap operator-=(const Bdd& other); - - /** - * @brief Adds a key-value pair to the map - */ - void put(uint32_t key, Bdd value); - - /** - * @brief Removes a key-value pair from the map - */ - void removeKey(uint32_t key); - - /** - * @brief Returns the number of key-value pairs in this map - */ - size_t size() const; - - /** - * @brief Returns non-zero when this map is empty - */ - int isEmpty() const; -}; - -class MtbddMap; - -class Mtbdd { - friend class Sylvan; - 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 Creates a Mtbdd leaf representing the uint64 value - */ - static Mtbdd uint64Terminal(uint64_t value); - - /** - * @brief Creates a Mtbdd leaf representing the floating-point value - */ - static Mtbdd doubleTerminal(double value); - - /** - * @brief Creates a Mtbdd leaf representing the fraction value / - * Internally, Sylvan uses 32-bit values and reports overflows to stderr. - */ - static Mtbdd fractionTerminal(uint64_t nominator, uint64_t denominator); - - /** - * @brief Creates a Mtbdd leaf of type holding value - * This is useful for custom Mtbdd types. - */ - static Mtbdd terminal(uint32_t type, uint64_t value); - - /** - * @brief Creates a Boolean Mtbdd representing jsut the variable index in its positive form - * The variable index must be 0<=index<=2^23 (Sylvan uses 24 bits internally) - */ - static Mtbdd mtbddVar(uint32_t variable); - - /** - * @brief Returns the Boolean Mtbdd representing "True" - */ - static Mtbdd mtbddOne(); - - /** - * @brief Returns the Boolean Mtbdd representing "False" - */ - static Mtbdd mtbddZero(); - - /** - * @brief Returns the Mtbdd representing a cube of variables, according to the given values. - * @param variables the variables that will be in the cube in their positive or negative form - * @param values a character array describing how the variables will appear in the result - * @param terminal the leaf of the cube - * The length of string must be equal to the number of variables in the cube. - * For every ith char in string, if it is 0, the corresponding variable will appear in its negative form, - * if it is 1, it will appear in its positive form, and if it is 2, it will appear as "any", thus it will - * be skipped. - */ - static Mtbdd mtbddCube(const Mtbdd &variables, unsigned char *values, const Mtbdd &terminal); - - /** - * @brief Returns the Mtbdd representing a cube of variables, according to the given values. - * @param variables the variables that will be in the cube in their positive or negative form - * @param values a character array describing how the variables will appear in the result - * @param terminal the leaf of the cube - * The length of string must be equal to the number of variables in the cube. - * For every ith char in string, if it is 0, the corresponding variable will appear in its negative form, - * if it is 1, it will appear in its positive form, and if it is 2, it will appear as "any", thus it will - * be skipped. - */ - static Mtbdd mtbddCube(const Mtbdd &variables, std::vector values, const Mtbdd &terminal); - - int operator==(const Mtbdd& other) const; - int operator!=(const Mtbdd& other) const; - Mtbdd operator=(const Mtbdd& right); - Mtbdd operator!() const; - Mtbdd operator~() const; - Mtbdd operator*(const Mtbdd& other) const; - Mtbdd operator*=(const Mtbdd& other); - Mtbdd operator+(const Mtbdd& other) const; - Mtbdd operator+=(const Mtbdd& other); - Mtbdd operator-(const Mtbdd& other) const; - Mtbdd operator-=(const Mtbdd& other); - - // not implemented (compared to Bdd): <=, >=, <, >, &, &=, |, |=, ^, ^= - - /** - * @brief Returns non-zero if this Mtbdd is a leaf - */ - int isTerminal() const; - - /** - * @brief Returns non-zero if this Mtbdd is a leaf - */ - int isLeaf() const; - - /** - * @brief Returns non-zero if this Mtbdd is mtbddOne() - */ - int isOne() const; - - /** - * @brief Returns non-zero if this Mtbdd is mtbddZero() - */ - int isZero() const; - - /** - * @brief Returns the top variable index of this Mtbdd (the variable in the root node) - */ - uint32_t TopVar() const; - - /** - * @brief Follows the high edge ("then") of the root node of this Mtbdd - */ - Mtbdd Then() const; - - /** - * @brief Follows the low edge ("else") of the root node of this Mtbdd - */ - Mtbdd Else() const; - - /** - * @brief Returns the negation of the MTBDD - * For Boolean, this means "not", for floating-point and fractions, this means "negative" - */ - Mtbdd Negate() const; - - /** - * @brief Applies the binary operation - */ - Mtbdd Apply(const Mtbdd &other, mtbdd_apply_op op) const; - - /** - * @brief Applies the unary operation with parameter - */ - Mtbdd UApply(mtbdd_uapply_op op, size_t param) const; - - /** - * @brief Computers the abstraction on variables using operator . - * See also: AbstractPlus, AbstractTimes, AbstractMin, AbstractMax - */ - Mtbdd Abstract(const Mtbdd &variables, mtbdd_abstract_op op) const; - - /** - * @brief Computes if f then g else h - * This Mtbdd must be a Boolean Mtbdd - */ - Mtbdd Ite(const Mtbdd &g, const Mtbdd &h) const; - - /** - * @brief Computes f + g - */ - Mtbdd Plus(const Mtbdd &other) const; - - /** - * @brief Computes f - g - */ - Mtbdd Minus(const Mtbdd &other) const; - - /** - * @brief Computes f * g - */ - Mtbdd Times(const Mtbdd &other) const; - - /** - * @brief Computes f / g - */ - Mtbdd Divide(const Mtbdd &other) const; - - /** - * @brief Computes min(f, g) - */ - Mtbdd Min(const Mtbdd &other) const; - - /** - * @brief Computes max(f, g) - */ - Mtbdd Max(const Mtbdd &other) const; - - /** - * @brief Computes abstraction by summation (existential quantification) - */ - Mtbdd AbstractPlus(const Mtbdd &variables) const; - - /** - * @brief Computes abstraction by multiplication (universal quantification) - */ - Mtbdd AbstractTimes(const Mtbdd &variables) const; - - /** - * @brief Computes abstraction by minimum - */ - Mtbdd AbstractMin(const Mtbdd &variables) const; - - /** - * @brief Computes abstraction by maximum - */ - Mtbdd AbstractMax(const Mtbdd &variables) const; - - /** - * @brief Computes abstraction by summation of f \times g - */ - Mtbdd AndExists(const Mtbdd &other, const Mtbdd &variables) const; - - /** - * @brief Convert floating-point/fraction Mtbdd to a Boolean Mtbdd, leaf >= value ? true : false - */ - Mtbdd MtbddThreshold(double value) const; - - /** - * @brief Convert floating-point/fraction Mtbdd to a Boolean Mtbdd, leaf > value ? true : false - */ - Mtbdd MtbddStrictThreshold(double value) const; - - /** - * @brief Convert floating-point/fraction Mtbdd to a Boolean Mtbdd, leaf >= value ? true : false - * Same as MtbddThreshold (Bdd = Boolean Mtbdd) - */ - Bdd BddThreshold(double value) const; - - /** - * @brief Convert floating-point/fraction Mtbdd to a Boolean Mtbdd, leaf > value ? true : false - * Same as MtbddStrictThreshold (Bdd = Boolean Mtbdd) - */ - Bdd BddStrictThreshold(double value) const; - Bdd NotZero() const; + class BddMap; - Bdd Equals(const Mtbdd& other) const; + class Mtbdd; - Bdd Less(const Mtbdd& other) const; - - Bdd LessOrEqual(const Mtbdd& other) const; + class Bdd { + friend class Sylvan; + friend class BddMap; + 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 Creates a Bdd representing just the variable index in its positive form + * The variable index must be a 0<=index<=2^23 (we use 24 bits internally) + */ + static Bdd bddVar(uint32_t index); + + /** + * @brief Returns the Bdd representing "True" + */ + static Bdd bddOne(); + + /** + * @brief Returns the Bdd representing "False" + */ + static Bdd bddZero(); + + /** + * @brief Returns the Bdd representing a cube of variables, according to the given values. + * @param variables the variables that will be in the cube in their positive or negative form + * @param values a character array describing how the variables will appear in the result + * The length of string must be equal to the number of variables in the cube. + * For every ith char in string, if it is 0, the corresponding variable will appear in its negative form, + * if it is 1, it will appear in its positive form, and if it is 2, it will appear as "any", thus it will + * be skipped. + */ + static Bdd bddCube(const Bdd &variables, unsigned char *values); + + /** + * @brief Returns the Bdd representing a cube of variables, according to the given values. + * @param variables the variables that will be in the cube in their positive or negative form + * @param string a character array describing how the variables will appear in the result + * The length of string must be equal to the number of variables in the cube. + * For every ith char in string, if it is 0, the corresponding variable will appear in its negative form, + * if it is 1, it will appear in its positive form, and if it is 2, it will appear as "any", thus it will + * be skipped. + */ + static Bdd bddCube(const Bdd &variables, std::vector values); + + int operator==(const Bdd& other) const; + int operator!=(const Bdd& other) const; + Bdd operator=(const Bdd& right); + int operator<=(const Bdd& other) const; + int operator>=(const Bdd& other) const; + int operator<(const Bdd& other) const; + int operator>(const Bdd& other) const; + Bdd operator!() const; + Bdd operator~() const; + Bdd operator*(const Bdd& other) const; + Bdd operator*=(const Bdd& other); + Bdd operator&(const Bdd& other) const; + Bdd operator&=(const Bdd& other); + Bdd operator+(const Bdd& other) const; + Bdd operator+=(const Bdd& other); + Bdd operator|(const Bdd& other) const; + Bdd operator|=(const Bdd& other); + Bdd operator^(const Bdd& other) const; + Bdd operator^=(const Bdd& other); + Bdd operator-(const Bdd& other) const; + Bdd operator-=(const Bdd& other); + + /** + * @brief Returns non-zero if this Bdd is bddOne() or bddZero() + */ + int isConstant() const; + + /** + * @brief Returns non-zero if this Bdd is bddOne() or bddZero() + */ + int isTerminal() const; + + /** + * @brief Returns non-zero if this Bdd is bddOne() + */ + int isOne() const; + + /** + * @brief Returns non-zero if this Bdd is bddZero() + */ + int isZero() const; + + /** + * @brief Returns the top variable index of this Bdd (the variable in the root node) + */ + uint32_t TopVar() const; + + /** + * @brief Follows the high edge ("then") of the root node of this Bdd + */ + Bdd Then() const; + + /** + * @brief Follows the low edge ("else") of the root node of this Bdd + */ + Bdd Else() const; + + /** + * @brief Computes \exists cube: f \and g + */ + Bdd AndAbstract(const Bdd& g, const Bdd& cube) const; + + /** + * @brief Computes \exists cube: f + */ + Bdd ExistAbstract(const Bdd& cube) const; + + /** + * @brief Computes \forall cube: f + */ + Bdd UnivAbstract(const Bdd& cube) const; + + /** + * @brief Computes if f then g else h + */ + Bdd Ite(const Bdd& g, const Bdd& h) const; + + /** + * @brief Computes f \and g + */ + Bdd And(const Bdd& g) const; + + /** + * @brief Computes f \or g + */ + Bdd Or(const Bdd& g) const; + + /** + * @brief Computes \not (f \and g) + */ + Bdd Nand(const Bdd& g) const; + + /** + * @brief Computes \not (f \or g) + */ + Bdd Nor(const Bdd& g) const; + + /** + * @brief Computes f \xor g + */ + Bdd Xor(const Bdd& g) const; + + /** + * @brief Computes \not (f \xor g), i.e. f \equiv g + */ + Bdd Xnor(const Bdd& g) const; + + /** + * @brief Returns whether all elements in f are also in g + */ + int Leq(const Bdd& g) const; + + /** + * @brief Computes the reverse application of a transition relation to this set. + * @param relation the transition relation to apply + * @param cube the variables that are in the transition relation + * This function assumes that s,t are interleaved with s odd and t even. + * Other variables in the relation are ignored (by existential quantification) + * Set cube to "false" (illegal cube) to assume all encountered variables are in s,t + * + * Use this function to concatenate two relations --> --> + * or to take the 'previous' of a set --> S + */ + Bdd RelPrev(const Bdd& relation, const Bdd& cube) const; + + /** + * @brief Computes the application of a transition relation to this set. + * @param relation the transition relation to apply + * @param cube the variables that are in the transition relation + * This function assumes that s,t are interleaved with s odd and t even. + * Other variables in the relation are ignored (by existential quantification) + * Set cube to "false" (illegal cube) to assume all encountered variables are in s,t + * + * Use this function to take the 'next' of a set S --> + */ + Bdd RelNext(const Bdd& relation, const Bdd& cube) const; + + /** + * @brief Computes the transitive closure by traversing the BDD recursively. + * See Y. Matsunaga, P. C. McGeer, R. K. Brayton + * On Computing the Transitive Closre of a State Transition Relation + * 30th ACM Design Automation Conference, 1993. + */ + Bdd Closure() const; + + /** + * @brief Computes the constrain f @ c + */ + Bdd Constrain(const Bdd &c) const; + + /** + * @brief Computes the BDD restrict according to Coudert and Madre's algorithm (ICCAD90). + */ + Bdd Restrict(const Bdd &c) const; + + /** + * @brief Functional composition. Whenever a variable v in the map m is found in the BDD, + * it is substituted by the associated function. + * You can also use this function to implement variable reordering. + */ + Bdd Compose(const BddMap &m) const; + + /** + * @brief Substitute all variables in the array from by the corresponding variables in to. + */ + Bdd Permute(const std::vector& from, const std::vector& to) const; + + /** + * @brief Computes the support of a Bdd. + */ + Bdd Support() const; + + /** + * @brief Gets the BDD of this Bdd (for C functions) + */ + BDD GetBDD() const; + + /** + * @brief Writes .dot file of this Bdd. Not thread-safe! + */ + void PrintDot(FILE *out) const; + + /** + * @brief Gets a SHA2 hash that describes the structure of this Bdd. + * @param string a character array of at least 65 characters (includes zero-termination) + * This hash is 64 characters long and is independent of the memory locations of BDD nodes. + */ + void GetShaHash(char *string) const; + + std::string GetShaHash() const; + + /** + * @brief Computes the number of satisfying variable assignments, using variables in cube. + */ + double SatCount(const Bdd &variables) const; + + /** + * @brief Compute the number of satisfying variable assignments, using the given number of variables. + */ + double SatCount(const size_t nvars) const; + + /** + * @brief Gets one satisfying assignment according to the variables. + * @param variables The set of variables to be assigned, must include the support of the Bdd. + */ + void PickOneCube(const Bdd &variables, uint8_t *string) const; + + /** + * @brief Gets one satisfying assignment according to the variables. + * @param variables The set of variables to be assigned, must include the support of the Bdd. + * Returns an empty vector when either this Bdd equals bddZero() or the cube is empty. + */ + std::vector PickOneCube(const Bdd &variables) const; + + /** + * @brief Gets a cube that satisfies this Bdd. + */ + Bdd PickOneCube() const; + + /** + * @brief Faster version of: *this + Sylvan::bddCube(variables, values); + */ + Bdd UnionCube(const Bdd &variables, uint8_t *values) const; + + /** + * @brief Faster version of: *this + Sylvan::bddCube(variables, values); + */ + Bdd UnionCube(const Bdd &variables, std::vector values) const; + + /** + * @brief Generate a cube representing a set of variables + */ + static Bdd VectorCube(const std::vector variables); + + /** + * @brief Generate a cube representing a set of variables + * @param variables An sorted set of variable indices + */ + static Bdd VariablesCube(const std::vector variables); + + /** + * @brief Gets the number of nodes in this Bdd. Not thread-safe! + */ + size_t NodeCount() const; + +#include "sylvan_obj_bdd_storm.hpp" + + private: + BDD bdd; + }; - double getDoubleMax() const; - - double getDoubleMin() const; + 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); } + public: + BddMap() : bdd(sylvan_map_empty()) { sylvan_protect(&bdd); } + ~BddMap() { sylvan_unprotect(&bdd); } + + BddMap(uint32_t key_variable, const Bdd value); + + BddMap operator+(const Bdd& other) const; + BddMap operator+=(const Bdd& other); + BddMap operator-(const Bdd& other) const; + BddMap operator-=(const Bdd& other); + + /** + * @brief Adds a key-value pair to the map + */ + void put(uint32_t key, Bdd value); + + /** + * @brief Removes a key-value pair from the map + */ + void removeKey(uint32_t key); + + /** + * @brief Returns the number of key-value pairs in this map + */ + size_t size() const; + + /** + * @brief Returns non-zero when this map is empty + */ + int isEmpty() const; + }; - bool EqualNorm(const Mtbdd& other, double epsilon) const; - - bool EqualNormRel(const Mtbdd& other, double epsilon) const; + class MtbddMap; - Mtbdd Floor() const; - - Mtbdd Ceil() const; + class Mtbdd { + friend class Sylvan; + 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 Creates a Mtbdd leaf representing the uint64 value + */ + static Mtbdd uint64Terminal(uint64_t value); + + /** + * @brief Creates a Mtbdd leaf representing the floating-point value + */ + static Mtbdd doubleTerminal(double value); + + /** + * @brief Creates a Mtbdd leaf representing the fraction value / + * Internally, Sylvan uses 32-bit values and reports overflows to stderr. + */ + static Mtbdd fractionTerminal(uint64_t nominator, uint64_t denominator); + + /** + * @brief Creates a Mtbdd leaf of type holding value + * This is useful for custom Mtbdd types. + */ + static Mtbdd terminal(uint32_t type, uint64_t value); + + /** + * @brief Creates a Boolean Mtbdd representing jsut the variable index in its positive form + * The variable index must be 0<=index<=2^23 (Sylvan uses 24 bits internally) + */ + static Mtbdd mtbddVar(uint32_t variable); + + /** + * @brief Returns the Boolean Mtbdd representing "True" + */ + static Mtbdd mtbddOne(); + + /** + * @brief Returns the Boolean Mtbdd representing "False" + */ + static Mtbdd mtbddZero(); + + /** + * @brief Returns the Mtbdd representing a cube of variables, according to the given values. + * @param variables the variables that will be in the cube in their positive or negative form + * @param values a character array describing how the variables will appear in the result + * @param terminal the leaf of the cube + * The length of string must be equal to the number of variables in the cube. + * For every ith char in string, if it is 0, the corresponding variable will appear in its negative form, + * if it is 1, it will appear in its positive form, and if it is 2, it will appear as "any", thus it will + * be skipped. + */ + static Mtbdd mtbddCube(const Mtbdd &variables, unsigned char *values, const Mtbdd &terminal); + + /** + * @brief Returns the Mtbdd representing a cube of variables, according to the given values. + * @param variables the variables that will be in the cube in their positive or negative form + * @param values a character array describing how the variables will appear in the result + * @param terminal the leaf of the cube + * The length of string must be equal to the number of variables in the cube. + * For every ith char in string, if it is 0, the corresponding variable will appear in its negative form, + * if it is 1, it will appear in its positive form, and if it is 2, it will appear as "any", thus it will + * be skipped. + */ + static Mtbdd mtbddCube(const Mtbdd &variables, std::vector values, const Mtbdd &terminal); + + int operator==(const Mtbdd& other) const; + int operator!=(const Mtbdd& other) const; + Mtbdd operator=(const Mtbdd& right); + Mtbdd operator!() const; + Mtbdd operator~() const; + Mtbdd operator*(const Mtbdd& other) const; + Mtbdd operator*=(const Mtbdd& other); + Mtbdd operator+(const Mtbdd& other) const; + Mtbdd operator+=(const Mtbdd& other); + Mtbdd operator-(const Mtbdd& other) const; + Mtbdd operator-=(const Mtbdd& other); + + // not implemented (compared to Bdd): <=, >=, <, >, &, &=, |, |=, ^, ^= + + /** + * @brief Returns non-zero if this Mtbdd is a leaf + */ + int isTerminal() const; + + /** + * @brief Returns non-zero if this Mtbdd is a leaf + */ + int isLeaf() const; + + /** + * @brief Returns non-zero if this Mtbdd is mtbddOne() + */ + int isOne() const; + + /** + * @brief Returns non-zero if this Mtbdd is mtbddZero() + */ + int isZero() const; + + /** + * @brief Returns the top variable index of this Mtbdd (the variable in the root node) + */ + uint32_t TopVar() const; + + /** + * @brief Follows the high edge ("then") of the root node of this Mtbdd + */ + Mtbdd Then() const; + + /** + * @brief Follows the low edge ("else") of the root node of this Mtbdd + */ + Mtbdd Else() const; + + /** + * @brief Returns the negation of the MTBDD + * For Boolean, this means "not", for floating-point and fractions, this means "negative" + */ + Mtbdd Negate() const; + + /** + * @brief Applies the binary operation + */ + Mtbdd Apply(const Mtbdd &other, mtbdd_apply_op op) const; + + /** + * @brief Applies the unary operation with parameter + */ + Mtbdd UApply(mtbdd_uapply_op op, size_t param) const; + + /** + * @brief Computers the abstraction on variables using operator . + * See also: AbstractPlus, AbstractTimes, AbstractMin, AbstractMax + */ + Mtbdd Abstract(const Mtbdd &variables, mtbdd_abstract_op op) const; + + /** + * @brief Computes if f then g else h + * This Mtbdd must be a Boolean Mtbdd + */ + Mtbdd Ite(const Mtbdd &g, const Mtbdd &h) const; + + /** + * @brief Computes f + g + */ + Mtbdd Plus(const Mtbdd &other) const; + + /** + * @brief Computes f * g + */ + Mtbdd Times(const Mtbdd &other) const; + + /** + * @brief Computes min(f, g) + */ + Mtbdd Min(const Mtbdd &other) const; + + /** + * @brief Computes max(f, g) + */ + Mtbdd Max(const Mtbdd &other) const; + + /** + * @brief Computes abstraction by summation (existential quantification) + */ + Mtbdd AbstractPlus(const Mtbdd &variables) const; + + /** + * @brief Computes abstraction by multiplication (universal quantification) + */ + Mtbdd AbstractTimes(const Mtbdd &variables) const; + + /** + * @brief Computes abstraction by minimum + */ + Mtbdd AbstractMin(const Mtbdd &variables) const; + + /** + * @brief Computes abstraction by maximum + */ + Mtbdd AbstractMax(const Mtbdd &variables) const; + + /** + * @brief Computes abstraction by summation of f \times g + */ + Mtbdd AndExists(const Mtbdd &other, const Mtbdd &variables) const; + + /** + * @brief Convert floating-point/fraction Mtbdd to a Boolean Mtbdd, leaf >= value ? true : false + */ + Mtbdd MtbddThreshold(double value) const; + + /** + * @brief Convert floating-point/fraction Mtbdd to a Boolean Mtbdd, leaf > value ? true : false + */ + Mtbdd MtbddStrictThreshold(double value) const; + + /** + * @brief Convert floating-point/fraction Mtbdd to a Boolean Mtbdd, leaf >= value ? true : false + * Same as MtbddThreshold (Bdd = Boolean Mtbdd) + */ + Bdd BddThreshold(double value) const; + + /** + * @brief Convert floating-point/fraction Mtbdd to a Boolean Mtbdd, leaf > value ? true : false + * Same as MtbddStrictThreshold (Bdd = Boolean Mtbdd) + */ + Bdd BddStrictThreshold(double value) const; + + /** + * @brief Computes the support of a Mtbdd. + */ + Mtbdd Support() const; + + /** + * @brief Gets the MTBDD of this Mtbdd (for C functions) + */ + MTBDD GetMTBDD() const; + + /** + * @brief Functional composition. Whenever a variable v in the map m is found in the MTBDD, + * it is substituted by the associated function (which should be a Boolean MTBDD) + * You can also use this function to implement variable reordering. + */ + Mtbdd Compose(MtbddMap &m) const; + + /** + * @brief Substitute all variables in the array from by the corresponding variables in to. + */ + Mtbdd Permute(const std::vector& from, const std::vector& to) const; + + /** + * @brief Compute the number of satisfying variable assignments, using variables in cube. + */ + double SatCount(const Mtbdd &variables) const; + + /** + * @brief Compute the number of satisfying variable assignments, using the given number of variables. + */ + double SatCount(const size_t nvars) const; + + /** + * @brief Gets the number of nodes in this Bdd. Not thread-safe! + */ + size_t NodeCount() const; + +#include "sylvan_obj_mtbdd_storm.hpp" + + private: + MTBDD mtbdd; + }; - Mtbdd Pow(const Mtbdd& other) const; - - Mtbdd Mod(const Mtbdd& other) const; - - Mtbdd Logxy(const Mtbdd& other) const; + class MtbddMap + { + friend class Mtbdd; + MTBDD mtbdd; + MtbddMap(MTBDD from) : mtbdd(from) { mtbdd_protect(&mtbdd); } + MtbddMap(Mtbdd &from) : mtbdd(from.mtbdd) { mtbdd_protect(&mtbdd); } + public: + MtbddMap() : mtbdd(mtbdd_map_empty()) { mtbdd_protect(&mtbdd); } + ~MtbddMap() { mtbdd_unprotect(&mtbdd); } + + MtbddMap(uint32_t key_variable, Mtbdd value); + + MtbddMap operator+(const Mtbdd& other) const; + MtbddMap operator+=(const Mtbdd& other); + MtbddMap operator-(const Mtbdd& other) const; + MtbddMap operator-=(const Mtbdd& other); + + /** + * @brief Adds a key-value pair to the map + */ + void put(uint32_t key, Mtbdd value); + + /** + * @brief Removes a key-value pair from the map + */ + void removeKey(uint32_t key); + + /** + * @brief Returns the number of key-value pairs in this map + */ + size_t size(); + + /** + * @brief Returns non-zero when this map is empty + */ + int isEmpty(); + }; - size_t CountLeaves() const; + class Sylvan { + public: + /** + * @brief Initializes the Sylvan framework, call this only once in your program. + * @param initialTableSize The initial size of the nodes table. Must be a power of two. + * @param maxTableSize The maximum size of the nodes table. Must be a power of two. + * @param initialCacheSize The initial size of the operation cache. Must be a power of two. + * @param maxCacheSize The maximum size of the operation cache. Must be a power of two. + */ + static void initPackage(size_t initialTableSize, size_t maxTableSize, size_t initialCacheSize, size_t maxCacheSize); + + /** + * @brief Initializes the BDD module of the Sylvan framework. + * @param granularity determins operation cache behavior; for higher values (2+) it will use the operation cache less often. + * Values of 3-7 may result in better performance, since occasionally not using the operation cache is fine in practice. + * A granularity of 1 means that every BDD operation will be cached at every variable level. + */ + static void initBdd(int granularity); + + /** + * @brief Initializes the MTBDD module of the Sylvan framework. + */ + static void initMtbdd(); + + /** + * @brief Frees all memory in use by Sylvan. + * Warning: if you have any Bdd objects which are not bddZero() or bddOne() after this, your program may crash! + */ + static void quitPackage(); + }; - Mtbdd Permute(const std::vector& from, const std::vector& to) const; - - /** - * @brief Computes the support of a Mtbdd. - */ - Mtbdd Support() const; - - /** - * @brief Gets the MTBDD of this Mtbdd (for C functions) - */ - MTBDD GetMTBDD() const; - - /** - * @brief Functional composition. Whenever a variable v in the map m is found in the MTBDD, - * it is substituted by the associated function (which should be a Boolean MTBDD) - * You can also use this function to implement variable reordering. - */ - Mtbdd Compose(MtbddMap &m) const; - - /** - * @brief Compute the number of satisfying variable assignments, using variables in cube. - */ - double SatCount(size_t variableCount) const; - - /** - * @brief Compute the number of non-zero variable assignments, using variables in cube. - */ - double NonZeroCount(size_t variableCount) const; - - /** - * @brief Gets the number of nodes in this Bdd. Not thread-safe! - */ - size_t NodeCount() const; - -private: - MTBDD mtbdd; -}; - -class MtbddMap -{ - friend class Mtbdd; - MTBDD mtbdd; - MtbddMap(MTBDD from) : mtbdd(from) { mtbdd_protect(&mtbdd); } - MtbddMap(Mtbdd &from) : mtbdd(from.mtbdd) { mtbdd_protect(&mtbdd); } -public: - MtbddMap() : mtbdd(mtbdd_map_empty()) { mtbdd_protect(&mtbdd); } - ~MtbddMap() { mtbdd_unprotect(&mtbdd); } - - MtbddMap(uint32_t key_variable, Mtbdd value); - - MtbddMap operator+(const Mtbdd& other) const; - MtbddMap operator+=(const Mtbdd& other); - MtbddMap operator-(const Mtbdd& other) const; - MtbddMap operator-=(const Mtbdd& other); - - /** - * @brief Adds a key-value pair to the map - */ - void put(uint32_t key, Mtbdd value); - - /** - * @brief Removes a key-value pair from the map - */ - void removeKey(uint32_t key); - - /** - * @brief Returns the number of key-value pairs in this map - */ - size_t size(); - - /** - * @brief Returns non-zero when this map is empty - */ - int isEmpty(); -}; - -class Sylvan { -public: - /** - * @brief Initializes the Sylvan framework, call this only once in your program. - * @param initialTableSize The initial size of the nodes table. Must be a power of two. - * @param maxTableSize The maximum size of the nodes table. Must be a power of two. - * @param initialCacheSize The initial size of the operation cache. Must be a power of two. - * @param maxCacheSize The maximum size of the operation cache. Must be a power of two. - */ - static void initPackage(size_t initialTableSize, size_t maxTableSize, size_t initialCacheSize, size_t maxCacheSize); - - /** - * @brief Initializes the BDD module of the Sylvan framework. - * @param granularity determins operation cache behavior; for higher values (2+) it will use the operation cache less often. - * Values of 3-7 may result in better performance, since occasionally not using the operation cache is fine in practice. - * A granularity of 1 means that every BDD operation will be cached at every variable level. - */ - static void initBdd(int granularity); - - /** - * @brief Initializes the MTBDD module of the Sylvan framework. - */ - static void initMtbdd(); - - /** - * @brief Frees all memory in use by Sylvan. - * Warning: if you have any Bdd objects which are not bddZero() or bddOne() after this, your program may crash! - */ - static void quitPackage(); -}; - } #endif diff --git a/src/storage/dd/Add.cpp b/src/storage/dd/Add.cpp index 60a74f622..876ccc808 100644 --- a/src/storage/dd/Add.cpp +++ b/src/storage/dd/Add.cpp @@ -213,10 +213,10 @@ namespace storm { template Add Add::multiplyMatrix(Add const& otherMatrix, std::set const& summationMetaVariables) const { // Create the CUDD summation variables. - std::vector> summationDdVariables; + std::vector> summationDdVariables; for (auto const& metaVariable : summationMetaVariables) { for (auto const& ddVariable : this->getDdManager()->getMetaVariable(metaVariable).getDdVariables()) { - summationDdVariables.push_back(ddVariable.template toAdd()); + summationDdVariables.push_back(ddVariable); } } diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp index 2ede652f6..773845043 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.cpp +++ b/src/storage/dd/cudd/InternalCuddAdd.cpp @@ -178,11 +178,11 @@ namespace storm { } template - InternalAdd InternalAdd::multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const { + InternalAdd InternalAdd::multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const { // Create the CUDD summation variables. std::vector summationAdds; for (auto const& ddVariable : summationDdVariables) { - summationAdds.push_back(ddVariable.getCuddAdd()); + summationAdds.push_back(ddVariable.toAdd().getCuddAdd()); } return InternalAdd(ddManager, this->getCuddAdd().MatrixMultiply(otherMatrix.getCuddAdd(), summationAdds)); diff --git a/src/storage/dd/cudd/InternalCuddAdd.h b/src/storage/dd/cudd/InternalCuddAdd.h index 63fa308e7..63b176a0f 100644 --- a/src/storage/dd/cudd/InternalCuddAdd.h +++ b/src/storage/dd/cudd/InternalCuddAdd.h @@ -303,7 +303,7 @@ namespace storm { * @param summationDdVariables The DD variables (represented as ADDs) over which to sum. * @return An ADD representing the result of the matrix-matrix multiplication. */ - InternalAdd multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const; + InternalAdd multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const; /*! * Computes a BDD that represents the function in which all assignments with a function value strictly diff --git a/src/storage/dd/cudd/InternalCuddBdd.cpp b/src/storage/dd/cudd/InternalCuddBdd.cpp index 5017852d1..2c39523a5 100644 --- a/src/storage/dd/cudd/InternalCuddBdd.cpp +++ b/src/storage/dd/cudd/InternalCuddBdd.cpp @@ -111,6 +111,11 @@ namespace storm { } uint_fast64_t InternalBdd::getNonZeroCount(uint_fast64_t numberOfDdVariables) const { + // If the number of DD variables is zero, CUDD returns a number greater 0 for constant nodes different from + // zero, which is not the behaviour we expect. + if (numberOfDdVariables == 0) { + return 0; + } return static_cast(this->getCuddBdd().CountMinterm(static_cast(numberOfDdVariables))); } diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp index 9ebc66233..04ed4ae97 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -164,22 +164,23 @@ namespace storm { template InternalAdd InternalAdd::swapVariables(std::vector> const& from, std::vector> const& to) const { - std::vector fromBdd; - std::vector toBdd; + std::vector fromMtbdd; + std::vector toMtbdd; for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { - fromBdd.push_back(it1->getSylvanBdd()); - toBdd.push_back(it2->getSylvanBdd()); + fromMtbdd.push_back(it1->getSylvanBdd()); + toMtbdd.push_back(it2->getSylvanBdd()); } - return InternalAdd(ddManager, this->sylvanMtbdd.Permute(fromBdd, toBdd)); + return InternalAdd(ddManager, this->sylvanMtbdd.Permute(fromMtbdd, toMtbdd)); } template - InternalAdd InternalAdd::multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const { - sylvan::Mtbdd summationVariables = sylvan::Mtbdd::mtbddOne(); + InternalAdd InternalAdd::multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const { + InternalBdd summationVariables = ddManager->getBddOne(); for (auto const& ddVariable : summationDdVariables) { - summationVariables *= ddVariable.sylvanMtbdd; + summationVariables &= ddVariable; } - return InternalAdd(ddManager, this->sylvanMtbdd.AndExists(otherMatrix.sylvanMtbdd, summationVariables)); + + return InternalAdd(ddManager, this->sylvanMtbdd.AndExists(otherMatrix.sylvanMtbdd, summationVariables.getSylvanBdd())); } template @@ -323,6 +324,11 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Not yet implemented."); } + template + sylvan::Mtbdd InternalAdd::getSylvanMtbdd() const { + return sylvanMtbdd; + } + template class InternalAdd; template class InternalAdd; } diff --git a/src/storage/dd/sylvan/InternalSylvanAdd.h b/src/storage/dd/sylvan/InternalSylvanAdd.h index c1dbe5b44..1f1f12079 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.h +++ b/src/storage/dd/sylvan/InternalSylvanAdd.h @@ -303,7 +303,7 @@ namespace storm { * @param summationDdVariables The DD variables (represented as ADDs) over which to sum. * @return An ADD representing the result of the matrix-matrix multiplication. */ - InternalAdd multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const; + InternalAdd multiplyMatrix(InternalAdd const& otherMatrix, std::vector> const& summationDdVariables) const; /*! * Computes a BDD that represents the function in which all assignments with a function value strictly @@ -546,6 +546,8 @@ namespace storm { Odd createOdd(std::vector const& ddVariableIndices) const; private: + sylvan::Mtbdd getSylvanMtbdd() const; + InternalDdManager const* ddManager; sylvan::Mtbdd sylvanMtbdd; diff --git a/test/functional/storage/CuddDdTest.cpp b/test/functional/storage/CuddDdTest.cpp index 9bb57dc94..1c3132be1 100644 --- a/test/functional/storage/CuddDdTest.cpp +++ b/test/functional/storage/CuddDdTest.cpp @@ -198,7 +198,7 @@ TEST(CuddDd, AbstractionTest) { EXPECT_EQ(1ul, dd3Bdd.getNonZeroCount()); ASSERT_THROW(dd3Bdd = dd3Bdd.existsAbstract({x.second}), storm::exceptions::InvalidArgumentException); ASSERT_NO_THROW(dd3Bdd = dd3Bdd.existsAbstract({x.first})); - EXPECT_EQ(1ul, dd3Bdd.getNonZeroCount()); + EXPECT_EQ(0ul, dd3Bdd.getNonZeroCount()); EXPECT_EQ(1, dd3Bdd.template toAdd().getMax()); dd3 = dd1.equals(dd2).template toAdd(); diff --git a/test/functional/storage/SylvanDdTest.cpp b/test/functional/storage/SylvanDdTest.cpp index 442a9f1d4..ccb31c938 100644 --- a/test/functional/storage/SylvanDdTest.cpp +++ b/test/functional/storage/SylvanDdTest.cpp @@ -72,13 +72,10 @@ TEST(SylvanDd, EncodingTest) { EXPECT_EQ(5ul, encoding.getNodeCount()); EXPECT_EQ(1ul, encoding.getLeafCount()); - encoding.exportToDot("encoding.dot"); - storm::dd::Add add; ASSERT_NO_THROW(add = encoding.template toAdd()); // As an MTBDD, the 0-leaf is there, so the count is actually 2 and the node count is 6. - add.exportToDot("add.dot"); EXPECT_EQ(6ul, add.getNodeCount()); EXPECT_EQ(2ul, add.getLeafCount()); } @@ -191,97 +188,96 @@ TEST(SylvanDd, OperatorTest) { EXPECT_FALSE(dd1.equalModuloPrecision(dd2, 1e-6)); } -//TEST(SylvanDd, AbstractionTest) { -// std::shared_ptr> manager(new storm::dd::DdManager()); -// std::pair x = manager->addMetaVariable("x", 1, 9); -// storm::dd::Add dd1; -// storm::dd::Add dd2; -// storm::dd::Add dd3; -// -// dd1 = manager->template getIdentity(x.first); -// dd2 = manager->template getConstant(5); -// dd3 = dd1.equals(dd2); -// storm::dd::Bdd dd3Bdd = dd3.toBdd(); -// EXPECT_EQ(1ul, dd3Bdd.getNonZeroCount()); -// ASSERT_THROW(dd3Bdd = dd3Bdd.existsAbstract({x.second}), storm::exceptions::InvalidArgumentException); -// ASSERT_NO_THROW(dd3Bdd = dd3Bdd.existsAbstract({x.first})); -// EXPECT_EQ(1ul, dd3Bdd.getNonZeroCount()); -// EXPECT_EQ(1, dd3Bdd.template toAdd().getMax()); -// -// dd3 = dd1.equals(dd2); -// dd3 *= manager->template getConstant(3); -// EXPECT_EQ(1ul, dd3.getNonZeroCount()); -// ASSERT_THROW(dd3Bdd = dd3.toBdd().existsAbstract({x.second}), storm::exceptions::InvalidArgumentException); -// ASSERT_NO_THROW(dd3Bdd = dd3.toBdd().existsAbstract({x.first})); -// EXPECT_TRUE(dd3Bdd.isOne()); -// -// dd3 = dd1.equals(dd2); -// dd3 *= manager->template getConstant(3); -// ASSERT_THROW(dd3 = dd3.sumAbstract({x.second}), storm::exceptions::InvalidArgumentException); -// ASSERT_NO_THROW(dd3 = dd3.sumAbstract({x.first})); -// EXPECT_EQ(0ul, dd3.getNonZeroCount()); -// EXPECT_EQ(3, dd3.getMax()); -// -// dd3 = dd1.equals(dd2); -// dd3 *= manager->template getConstant(3); -// ASSERT_THROW(dd3 = dd3.minAbstract({x.second}), storm::exceptions::InvalidArgumentException); -// ASSERT_NO_THROW(dd3 = dd3.minAbstract({x.first})); -// EXPECT_EQ(0ul, dd3.getNonZeroCount()); -// EXPECT_EQ(0, dd3.getMax()); -// -// dd3 = dd1.equals(dd2); -// dd3 *= manager->template getConstant(3); -// ASSERT_THROW(dd3 = dd3.maxAbstract({x.second}), storm::exceptions::InvalidArgumentException); -// ASSERT_NO_THROW(dd3 = dd3.maxAbstract({x.first})); -// EXPECT_EQ(0ul, dd3.getNonZeroCount()); -// EXPECT_EQ(3, dd3.getMax()); -//} -// -//TEST(SylvanDd, SwapTest) { -// std::shared_ptr> manager(new storm::dd::DdManager()); -// -// std::pair x = manager->addMetaVariable("x", 1, 9); -// std::pair z = manager->addMetaVariable("z", 2, 8); -// storm::dd::Add dd1; -// storm::dd::Add dd2; -// -// dd1 = manager->template getIdentity(x.first); -// ASSERT_THROW(dd1 = dd1.swapVariables({std::make_pair(x.first, z.first)}), storm::exceptions::InvalidArgumentException); -// ASSERT_NO_THROW(dd1 = dd1.swapVariables({std::make_pair(x.first, x.second)})); -// EXPECT_TRUE(dd1 == manager->template getIdentity(x.second)); -//} -// -//TEST(SylvanDd, MultiplyMatrixTest) { -// std::shared_ptr> manager(new storm::dd::DdManager()); -// std::pair x = manager->addMetaVariable("x", 1, 9); -// -// storm::dd::Add dd1 = manager->template getIdentity(x.first).equals(manager->template getIdentity(x.second)); -// storm::dd::Add dd2 = manager->getRange(x.second).template toAdd(); -// storm::dd::Add dd3; -// dd1 *= manager->template getConstant(2); -// -// ASSERT_NO_THROW(dd3 = dd1.multiplyMatrix(dd2, {x.second})); -// ASSERT_NO_THROW(dd3 = dd3.swapVariables({std::make_pair(x.first, x.second)})); -// EXPECT_TRUE(dd3 == dd2 * manager->template getConstant(2)); -//} -// -//TEST(SylvanDd, GetSetValueTest) { -// std::shared_ptr> manager(new storm::dd::DdManager()); -// std::pair x = manager->addMetaVariable("x", 1, 9); -// -// storm::dd::Add dd1 = manager->template getAddOne(); -// ASSERT_NO_THROW(dd1.setValue(x.first, 4, 2)); -// EXPECT_EQ(2ul, dd1.getLeafCount()); -// -// std::map metaVariableToValueMap; -// metaVariableToValueMap.emplace(x.first, 1); -// EXPECT_EQ(1, dd1.getValue(metaVariableToValueMap)); -// -// metaVariableToValueMap.clear(); -// metaVariableToValueMap.emplace(x.first, 4); -// EXPECT_EQ(2, dd1.getValue(metaVariableToValueMap)); -//} -// +TEST(SylvanDd, AbstractionTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x = manager->addMetaVariable("x", 1, 9); + storm::dd::Add dd1; + storm::dd::Add dd2; + storm::dd::Add dd3; + storm::dd::Bdd bdd; + + dd1 = manager->template getIdentity(x.first); + dd2 = manager->template getConstant(5); + bdd = dd1.equals(dd2); + EXPECT_EQ(1ul, bdd.getNonZeroCount()); + ASSERT_THROW(bdd = bdd.existsAbstract({x.second}), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(bdd = bdd.existsAbstract({x.first})); + EXPECT_EQ(0ul, bdd.getNonZeroCount()); + EXPECT_EQ(1, bdd.template toAdd().getMax()); + + dd3 = dd1.equals(dd2).template toAdd(); + dd3 *= manager->template getConstant(3); + EXPECT_EQ(1ul, dd3.getNonZeroCount()); + ASSERT_THROW(bdd = dd3.toBdd().existsAbstract({x.second}), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(bdd = dd3.toBdd().existsAbstract({x.first})); + EXPECT_TRUE(bdd.isOne()); + + dd3 = dd1.equals(dd2).template toAdd(); + dd3 *= manager->template getConstant(3); + ASSERT_THROW(dd3 = dd3.sumAbstract({x.second}), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(dd3 = dd3.sumAbstract({x.first})); + EXPECT_EQ(0ul, dd3.getNonZeroCount()); + EXPECT_EQ(3, dd3.getMax()); + + dd3 = dd1.equals(dd2).template toAdd(); + dd3 *= manager->template getConstant(3); + ASSERT_THROW(dd3 = dd3.minAbstract({x.second}), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(dd3 = dd3.minAbstract({x.first})); + EXPECT_EQ(0ul, dd3.getNonZeroCount()); + EXPECT_EQ(0, dd3.getMax()); + + dd3 = dd1.equals(dd2).template toAdd(); + dd3 *= manager->template getConstant(3); + ASSERT_THROW(dd3 = dd3.maxAbstract({x.second}), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(dd3 = dd3.maxAbstract({x.first})); + EXPECT_EQ(0ul, dd3.getNonZeroCount()); + EXPECT_EQ(3, dd3.getMax()); +} + +TEST(SylvanDd, SwapTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + + std::pair x = manager->addMetaVariable("x", 1, 9); + std::pair z = manager->addMetaVariable("z", 2, 8); + storm::dd::Add dd1; + + dd1 = manager->template getIdentity(x.first); + ASSERT_THROW(dd1 = dd1.swapVariables({std::make_pair(x.first, z.first)}), storm::exceptions::InvalidArgumentException); + ASSERT_NO_THROW(dd1 = dd1.swapVariables({std::make_pair(x.first, x.second)})); + EXPECT_TRUE(dd1 == manager->template getIdentity(x.second)); +} + +TEST(SylvanDd, MultiplyMatrixTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x = manager->addMetaVariable("x", 1, 9); + + storm::dd::Add dd1 = manager->template getIdentity(x.first).equals(manager->template getIdentity(x.second)).template toAdd(); + storm::dd::Add dd2 = manager->getRange(x.second).template toAdd(); + storm::dd::Add dd3; + dd1 *= manager->template getConstant(2); + + ASSERT_NO_THROW(dd3 = dd1.multiplyMatrix(dd2, {x.second})); + ASSERT_NO_THROW(dd3 = dd3.swapVariables({std::make_pair(x.first, x.second)})); + EXPECT_TRUE(dd3 == dd2 * manager->template getConstant(2)); +} + +TEST(SylvanDd, GetSetValueTest) { + std::shared_ptr> manager(new storm::dd::DdManager()); + std::pair x = manager->addMetaVariable("x", 1, 9); + + storm::dd::Add dd1 = manager->template getAddOne(); + ASSERT_NO_THROW(dd1.setValue(x.first, 4, 2)); + EXPECT_EQ(2ul, dd1.getLeafCount()); + + std::map metaVariableToValueMap; + metaVariableToValueMap.emplace(x.first, 1); + EXPECT_EQ(1, dd1.getValue(metaVariableToValueMap)); + + metaVariableToValueMap.clear(); + metaVariableToValueMap.emplace(x.first, 4); + EXPECT_EQ(2, dd1.getValue(metaVariableToValueMap)); +} + //TEST(SylvanDd, ForwardIteratorTest) { // std::shared_ptr> manager(new storm::dd::DdManager()); // std::pair x = manager->addMetaVariable("x", 1, 9);