diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.cpp b/resources/3rdparty/sylvan/src/sylvan_obj.cpp index 7cf5960fb..143061704 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.cpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.cpp @@ -172,24 +172,24 @@ Bdd::operator-=(const Bdd& other) } Bdd -Bdd::AndAbstract(const Bdd &g, const Bdd &cube) const +Bdd::AndAbstract(const Bdd &g, const BddSet &cube) const { LACE_ME; - return sylvan_and_exists(bdd, g.bdd, cube.bdd); + return sylvan_and_exists(bdd, g.bdd, cube.set.bdd); } Bdd -Bdd::ExistAbstract(const Bdd &cube) const +Bdd::ExistAbstract(const BddSet &cube) const { LACE_ME; - return sylvan_exists(bdd, cube.bdd); + return sylvan_exists(bdd, cube.set.bdd); } Bdd -Bdd::UnivAbstract(const Bdd &cube) const +Bdd::UnivAbstract(const BddSet &cube) const { LACE_ME; - return sylvan_forall(bdd, cube.bdd); + return sylvan_forall(bdd, cube.set.bdd); } Bdd @@ -251,17 +251,17 @@ Bdd::Leq(const Bdd &g) const } Bdd -Bdd::RelPrev(const Bdd& relation, const Bdd& cube) const +Bdd::RelPrev(const Bdd& relation, const BddSet& cube) const { LACE_ME; - return sylvan_relprev(relation.bdd, bdd, cube.bdd); + return sylvan_relprev(relation.bdd, bdd, cube.set.bdd); } Bdd -Bdd::RelNext(const Bdd &relation, const Bdd &cube) const +Bdd::RelNext(const Bdd &relation, const BddSet &cube) const { LACE_ME; - return sylvan_relnext(bdd, relation.bdd, cube.bdd); + return sylvan_relnext(bdd, relation.bdd, cube.set.bdd); } Bdd @@ -293,16 +293,16 @@ Bdd::Compose(const BddMap &m) const } Bdd -Bdd::Permute(const std::vector& from, const std::vector& to) const +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]); + map.put(from[i], Bdd::bddVar(to[i])); } - + return sylvan_compose(bdd, map.bdd); } @@ -340,13 +340,12 @@ Bdd::GetShaHash() const } double -Bdd::SatCount(const Bdd &variables) const +Bdd::SatCount(const BddSet &variables) const { LACE_ME; - return sylvan_satcount(bdd, variables.bdd); + return sylvan_satcount(bdd, variables.set.bdd); } - double Bdd::SatCount(size_t nvars) const { @@ -356,22 +355,22 @@ Bdd::SatCount(size_t nvars) const } void -Bdd::PickOneCube(const Bdd &variables, uint8_t *values) const +Bdd::PickOneCube(const BddSet &variables, uint8_t *values) const { LACE_ME; - sylvan_sat_one(bdd, variables.bdd, values); + sylvan_sat_one(bdd, variables.set.bdd, values); } std::vector -Bdd::PickOneCube(const Bdd &variables) const +Bdd::PickOneCube(const BddSet &variables) const { std::vector result = std::vector(); - + BDD bdd = this->bdd; - BDD vars = variables.bdd; - + BDD vars = variables.set.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) { @@ -394,7 +393,7 @@ Bdd::PickOneCube(const Bdd &variables) const } } } - + return result; } @@ -406,18 +405,18 @@ Bdd::PickOneCube() const } Bdd -Bdd::UnionCube(const Bdd &variables, uint8_t *values) const +Bdd::UnionCube(const BddSet &variables, uint8_t *values) const { LACE_ME; - return sylvan_union_cube(bdd, variables.bdd, values); + return sylvan_union_cube(bdd, variables.set.bdd, values); } Bdd -Bdd::UnionCube(const Bdd &variables, std::vector values) const +Bdd::UnionCube(const BddSet &variables, std::vector values) const { LACE_ME; uint8_t *data = values.data(); - return sylvan_union_cube(bdd, variables.bdd, data); + return sylvan_union_cube(bdd, variables.set.bdd, data); } /** @@ -472,18 +471,18 @@ Bdd::bddVar(uint32_t index) } Bdd -Bdd::bddCube(const Bdd &variables, uint8_t *values) +Bdd::bddCube(const BddSet &variables, uint8_t *values) { LACE_ME; - return sylvan_cube(variables.bdd, values); + return sylvan_cube(variables.set.bdd, values); } Bdd -Bdd::bddCube(const Bdd &variables, std::vector values) +Bdd::bddCube(const BddSet &variables, std::vector values) { LACE_ME; uint8_t *data = values.data(); - return sylvan_cube(variables.bdd, data); + return sylvan_cube(variables.set.bdd, data); } int @@ -636,18 +635,18 @@ Mtbdd::mtbddZero() } Mtbdd -Mtbdd::mtbddCube(const Mtbdd &variables, uint8_t *values, const Mtbdd &terminal) +Mtbdd::mtbddCube(const BddSet &variables, uint8_t *values, const Mtbdd &terminal) { LACE_ME; - return mtbdd_cube(variables.mtbdd, values, terminal.mtbdd); + return mtbdd_cube(variables.set.bdd, values, terminal.mtbdd); } Mtbdd -Mtbdd::mtbddCube(const Mtbdd &variables, std::vector values, const Mtbdd &terminal) +Mtbdd::mtbddCube(const BddSet &variables, std::vector values, const Mtbdd &terminal) { LACE_ME; uint8_t *data = values.data(); - return mtbdd_cube(variables.mtbdd, data, terminal.mtbdd); + return mtbdd_cube(variables.set.bdd, data, terminal.mtbdd); } int @@ -713,10 +712,10 @@ Mtbdd::UApply(mtbdd_uapply_op op, size_t param) const } Mtbdd -Mtbdd::Abstract(const Mtbdd &variables, mtbdd_abstract_op op) const +Mtbdd::Abstract(const BddSet &variables, mtbdd_abstract_op op) const { LACE_ME; - return mtbdd_abstract(mtbdd, variables.mtbdd, op); + return mtbdd_abstract(mtbdd, variables.set.bdd, op); } Mtbdd @@ -755,38 +754,38 @@ Mtbdd::Max(const Mtbdd &other) const } Mtbdd -Mtbdd::AbstractPlus(const Mtbdd &variables) const +Mtbdd::AbstractPlus(const BddSet &variables) const { LACE_ME; - return mtbdd_abstract_plus(mtbdd, variables.mtbdd); + return mtbdd_abstract_plus(mtbdd, variables.set.bdd); } Mtbdd -Mtbdd::AbstractTimes(const Mtbdd &variables) const +Mtbdd::AbstractTimes(const BddSet &variables) const { LACE_ME; - return mtbdd_abstract_times(mtbdd, variables.mtbdd); + return mtbdd_abstract_times(mtbdd, variables.set.bdd); } Mtbdd -Mtbdd::AbstractMin(const Mtbdd &variables) const +Mtbdd::AbstractMin(const BddSet &variables) const { LACE_ME; - return mtbdd_abstract_min(mtbdd, variables.mtbdd); + return mtbdd_abstract_min(mtbdd, variables.set.bdd); } Mtbdd -Mtbdd::AbstractMax(const Mtbdd &variables) const +Mtbdd::AbstractMax(const BddSet &variables) const { LACE_ME; - return mtbdd_abstract_max(mtbdd, variables.mtbdd); + return mtbdd_abstract_max(mtbdd, variables.set.bdd); } Mtbdd -Mtbdd::AndExists(const Mtbdd &other, const Mtbdd &variables) const +Mtbdd::AndExists(const Mtbdd &other, const BddSet &variables) const { LACE_ME; - return mtbdd_and_exists(mtbdd, other.mtbdd, variables.mtbdd); + return mtbdd_and_exists(mtbdd, other.mtbdd, variables.set.bdd); } int @@ -914,16 +913,16 @@ Mtbdd::Compose(MtbddMap &m) const } 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 */ MtbddMap map; for (int i=from.size()-1; i>=0; i--) { - map.put(from[i].TopVar(), to[i]); + map.put(from[i], Bdd::bddVar(to[i])); } - + return mtbdd_compose(mtbdd, map.mtbdd); } @@ -935,9 +934,9 @@ Mtbdd::SatCount(size_t nvars) const } double -Mtbdd::SatCount(const Mtbdd &variables) const +Mtbdd::SatCount(const BddSet &variables) const { - return SatCount(sylvan_set_count(variables.mtbdd)); + return SatCount(sylvan_set_count(variables.set.bdd)); } size_t diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.hpp b/resources/3rdparty/sylvan/src/sylvan_obj.hpp index 46670ae73..94053afc7 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.hpp @@ -24,681 +24,831 @@ #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(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; - + +class BddSet; +class BddMap; +class Mtbdd; + +class Bdd { + friend class Sylvan; + friend class BddSet; + 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 BddSet &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 BddSet &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 BddSet& cube) const; + + /** + * @brief Computes \exists cube: f + */ + Bdd ExistAbstract(const BddSet& cube) const; + + /** + * @brief Computes \forall cube: f + */ + Bdd UnivAbstract(const BddSet& 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 BddSet& 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 BddSet& 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 BddSet &cube) 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 BddSet &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 BddSet &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 BddSet &variables, uint8_t *values) const; + + /** + * @brief Faster version of: *this + Sylvan::bddCube(variables, values); + */ + Bdd UnionCube(const BddSet &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; - }; - - 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 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; - +private: + BDD bdd; +}; + +class BddSet +{ + friend class Bdd; + friend class Mtbdd; + Bdd set; + +public: + /** + * @brief Create a new empty set. + */ + BddSet() : set(Bdd::bddOne()) {} + + /** + * @brief Wrap the BDD cube in a set. + */ + BddSet(const Bdd &other) : set(other) {} + + /** + * @brief Create a copy of the set . + */ + BddSet(const BddSet &other) : set(other.set) {} + + /** + * @brief Add the variable to this set. + */ + void add(uint32_t variable) { + set *= Bdd::bddVar(variable); + } + + /** + * @brief Add all variables in the set to this set. + */ + void add(BddSet &other) { + set *= other.set; + } + + /** + * @brief Remove the variable from this set. + */ + 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) { + set = set.ExistAbstract(other.set); + } + + /** + * @brief Retrieve the head of the set. (The first variable.) + */ + 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 { + Bdd then = set.Then(); + return BddSet(then); + } + + /** + * @brief Return true if this set is empty, or false otherwise. + */ + bool isEmpty() const { + return set.isOne(); + } + + /** + * @brief Return true if this set contains the variable , or false otherwise. + */ + bool contains(uint32_t variable) const { + if (isEmpty()) return false; + else if (TopVar() == variable) return true; + else return Next().contains(variable); + } + + /** + * @brief Return the number of variables in this set. + */ + size_t size() const { + if (isEmpty()) return 0; + else return 1 + Next().size(); + } + + /** + * @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) { + BddSet set; + for (size_t i = 0; i < length; i++) { + set.add(arr[length-i-1]); + } + } + + /** + * @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) { + BddSet set; + for (int i=variables.size()-1; i>=0; i--) { + set.set *= variables[i]; + } + return set; + } + + /** + * @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) { + BddSet set; + for (int i=variables.size()-1; i>=0; i--) { + set.add(variables[i]); + } + return set; + } + + /** + * @brief Write all variables in this set to . + * @param arr An array of at least size this.size(). + */ + void toArray(BDDVAR *arr) const { + if (!isEmpty()) { + *arr = TopVar(); + Next().toArray(arr+1); + } + } + + /** + * @brief Return the vector of all variables in this set. + */ + std::vector toVector() const { + std::vector result; + Bdd x = set; + while (!x.isOne()) { + result.push_back(x.TopVar()); + x = x.Then(); + } + return result; + } +}; + +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 BddSet &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 BddSet &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 BddSet &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 BddSet &variables) const; + + /** + * @brief Computes abstraction by multiplication (universal quantification) + */ + Mtbdd AbstractTimes(const BddSet &variables) const; + + /** + * @brief Computes abstraction by minimum + */ + Mtbdd AbstractMin(const BddSet &variables) const; + + /** + * @brief Computes abstraction by maximum + */ + Mtbdd AbstractMax(const BddSet &variables) const; + + /** + * @brief Computes abstraction by summation of f \times g + */ + Mtbdd AndExists(const Mtbdd &other, const BddSet &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 BddSet &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; - }; - - 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(); - }; +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/sylvan/InternalSylvanAdd.cpp b/src/storage/dd/sylvan/InternalSylvanAdd.cpp index 04ed4ae97..da1064dd5 100644 --- a/src/storage/dd/sylvan/InternalSylvanAdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanAdd.cpp @@ -140,17 +140,17 @@ namespace storm { template InternalAdd InternalAdd::sumAbstract(InternalBdd const& cube) const { - return InternalAdd(ddManager, this->sylvanMtbdd.AbstractPlus(static_cast(cube.sylvanBdd.GetBDD()))); + return InternalAdd(ddManager, this->sylvanMtbdd.AbstractPlus(cube.sylvanBdd)); } template InternalAdd InternalAdd::minAbstract(InternalBdd const& cube) const { - return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMin(static_cast(cube.sylvanBdd.GetBDD()))); + return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMin(cube.sylvanBdd)); } template InternalAdd InternalAdd::maxAbstract(InternalBdd const& cube) const { - return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMax(static_cast(cube.sylvanBdd.GetBDD()))); + return InternalAdd(ddManager, this->sylvanMtbdd.AbstractMax(cube.sylvanBdd)); } template @@ -164,13 +164,15 @@ namespace storm { template InternalAdd InternalAdd::swapVariables(std::vector> const& from, std::vector> const& to) const { - std::vector fromMtbdd; - std::vector toMtbdd; + std::vector fromIndices; + std::vector toIndices; + uint_fast64_t var = 0; for (auto it1 = from.begin(), ite1 = from.end(), it2 = to.begin(); it1 != ite1; ++it1, ++it2) { - fromMtbdd.push_back(it1->getSylvanBdd()); - toMtbdd.push_back(it2->getSylvanBdd()); + fromIndices.push_back(it1->getIndex()); + toIndices.push_back(it2->getIndex()); + ++var; } - return InternalAdd(ddManager, this->sylvanMtbdd.Permute(fromMtbdd, toMtbdd)); + return InternalAdd(ddManager, this->sylvanMtbdd.Permute(fromIndices, toIndices)); } template diff --git a/src/storage/dd/sylvan/InternalSylvanBdd.cpp b/src/storage/dd/sylvan/InternalSylvanBdd.cpp index 12e1d32aa..6f4cc610c 100644 --- a/src/storage/dd/sylvan/InternalSylvanBdd.cpp +++ b/src/storage/dd/sylvan/InternalSylvanBdd.cpp @@ -91,13 +91,13 @@ namespace storm { } InternalBdd InternalBdd::swapVariables(std::vector> const& from, std::vector> const& to) const { - std::vector fromBdd; - std::vector toBdd; + std::vector fromIndices; + std::vector toIndices; 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()); + fromIndices.push_back(it1->getIndex()); + toIndices.push_back(it2->getIndex()); } - return InternalBdd(ddManager, this->sylvanBdd.Permute(fromBdd, toBdd)); + return InternalBdd(ddManager, this->sylvanBdd.Permute(fromIndices, toIndices)); } InternalBdd InternalBdd::getSupport() const { @@ -131,7 +131,7 @@ namespace storm { } uint_fast64_t InternalBdd::getIndex() const { - return static_cast(this->sylvanBdd.GetBDD()); + return static_cast(this->sylvanBdd.TopVar()); } void InternalBdd::exportToDot(std::string const& filename, std::vector const& ddVariableNamesAsStrings) const {