diff --git a/resources/3rdparty/sylvan/src/sylvan_bdd.h b/resources/3rdparty/sylvan/src/sylvan_bdd.h index 78c8f5772..6208fe1c3 100644 --- a/resources/3rdparty/sylvan/src/sylvan_bdd.h +++ b/resources/3rdparty/sylvan/src/sylvan_bdd.h @@ -119,7 +119,7 @@ TASK_DECL_4(BDD, sylvan_and_exists, BDD, BDD, BDDSET, BDDVAR); /** * Compute R(s,t) = \exists x: A(s,x) \and B(x,t) * or R(s) = \exists x: A(s,x) \and B(x) - * Assumes s,t are interleaved with s odd and t even. + * Assumes s,t are interleaved with s even and t odd (s+1). * Parameter vars is the cube of all s and/or t variables. * Other variables in A are "ignored" (existential quantification) * Other variables in B are kept @@ -134,7 +134,7 @@ TASK_DECL_4(BDD, sylvan_relprev, BDD, BDD, BDDSET, BDDVAR); /** * Compute R(s) = \exists x: A(x) \and B(x,s) * with support(result) = s, support(A) = s, support(B) = s+t - * Assumes s,t are interleaved with s odd and t even. + * Assumes s,t are interleaved with s even and t odd (s+1). * Parameter vars is the cube of all s and/or t variables. * Other variables in A are kept * Other variables in B are "ignored" (existential quantification) @@ -152,7 +152,7 @@ TASK_DECL_4(BDD, sylvan_relnext, BDD, BDD, BDDSET, BDDVAR); * 30th ACM Design Automation Conference, 1993. * * The input BDD must be a transition relation that only has levels of s,t - * with s,t interleaved with s odd and t even, i.e. + * with s,t interleaved with s even and t odd, i.e. * s level 0,2,4 matches with t level 1,3,5 and so forth. */ TASK_DECL_2(BDD, sylvan_closure, BDD, BDDVAR); diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c index d7cf736f8..742dcffa9 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c @@ -14,7 +14,7 @@ * limitations under the License. */ -#include "sylvan_config.h" +#include #include #include @@ -25,11 +25,11 @@ #include #include -#include "refs.h" -#include "sha2.h" -#include "sylvan.h" -#include "sylvan_common.h" -#include "sylvan_mtbdd_int.h" +#include +#include +#include +#include +#include /* Primitives */ int @@ -2326,6 +2326,111 @@ TASK_IMPL_2(double, mtbdd_satcount, MTBDD, dd, size_t, nvars) return hack.d; } +static MTBDD +mtbdd_enum_next_leaf(MTBDD dd, MTBDD variables, MTBDD prev) +{ + // dd is a leaf + + if (variables == mtbdd_true) { + // if prev is not false, then it equals dd and we should return false (seen before) + if (prev != mtbdd_false) return mtbdd_false; + else return dd; + } else { + // get next variable from + uint32_t v = mtbdd_getvar(variables); + variables = mtbdd_gethigh(variables); + + // if prev is not false, get plow and phigh (one of these leads to "false") + MTBDD plow, phigh; + if (prev != mtbdd_false) { + mtbddnode_t pn = GETNODE(prev); + assert(!mtbdd_isleaf(prev) && mtbddnode_getvariable(pn) == v); + plow = node_getlow(prev, pn); + phigh = node_gethigh(prev, pn); + assert(plow == mtbdd_false || phigh == mtbdd_false); + } else { + plow = phigh = mtbdd_false; + } + + MTBDD sub; + + // first maybe follow low + if (phigh == mtbdd_false) { + sub = mtbdd_enum_next_leaf(dd, variables, plow); + if (sub != mtbdd_false) return mtbdd_makenode(v, sub, mtbdd_false); + } + + // if not low, try following high + sub = mtbdd_enum_next_leaf(dd, variables, phigh); + if (sub != mtbdd_false) return mtbdd_makenode(v, mtbdd_false, sub); + + // we've tried low and high, return false + return mtbdd_false; + } +} + +MTBDD +mtbdd_enum_next(MTBDD dd, MTBDD variables, MTBDD prev, mtbdd_enum_filter_cb filter_cb) +{ + if (dd == mtbdd_false) { + // the leaf dd is skipped + return mtbdd_false; + } else if (mtbdd_isleaf(dd)) { + // a leaf for which the filter returns 0 is skipped + if (filter_cb != NULL && filter_cb(dd) == 0) return mtbdd_false; + // ok, we have a leaf that is not skipped, go for it! + return mtbdd_enum_next_leaf(dd, variables, prev); + } else { + // if variables == true, then dd must be a leaf. But then this line is unreachable. + assert(variables != mtbdd_true); + + // get next variable from + uint32_t v = mtbdd_getvar(variables); + variables = mtbdd_gethigh(variables); + + // if prev is not false, get plow and phigh (one of these leads to "false") + MTBDD plow, phigh; + if (prev != mtbdd_false) { + mtbddnode_t pn = GETNODE(prev); + assert(!mtbdd_isleaf(prev) && mtbddnode_getvariable(pn) == v); + plow = node_getlow(prev, pn); + phigh = node_gethigh(prev, pn); + assert(plow == mtbdd_false || phigh == mtbdd_false); + } else { + plow = phigh = mtbdd_false; + } + + // get cofactors ddlow and ddhigh + MTBDD ddlow, ddhigh; + if (!mtbdd_isleaf(dd)) { + mtbddnode_t n = GETNODE(dd); + if (mtbddnode_getvariable(n) == v) { + ddlow = node_getlow(dd, n); + ddhigh = node_gethigh(dd, n); + } else { + ddlow = ddhigh = dd; + } + } else { + ddlow = ddhigh = dd; + } + + MTBDD sub; + + // first maybe follow low + if (phigh == mtbdd_false) { + sub = mtbdd_enum_next(ddlow, variables, plow, filter_cb); + if (sub != mtbdd_false) return mtbdd_makenode(v, sub, mtbdd_false); + } + + // if not low, try following high + sub = mtbdd_enum_next(ddhigh, variables, phigh, filter_cb); + if (sub != mtbdd_false) return mtbdd_makenode(v, mtbdd_false, sub); + + // we've tried low and high, return false + return mtbdd_false; + } +} + /** * Helper function for recursive unmarking */ @@ -2583,3 +2688,4 @@ mtbdd_map_removeall(MTBDDMAP map, MTBDD variables) } #include "sylvan_storm_custom.c" + diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h index a6c6ebf62..b22ff3f67 100644 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.h +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.h @@ -223,7 +223,7 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_plus, MTBDD, MTBDD, int); */ TASK_DECL_2(MTBDD, mtbdd_op_times, MTBDD*, MTBDD*); TASK_DECL_3(MTBDD, mtbdd_abstract_op_times, MTBDD, MTBDD, int); - + /** * Binary operation Minimum (for MTBDDs of same type) * Only for MTBDDs where either all leaves are Boolean, or Integer, or Double. @@ -241,7 +241,7 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_min, MTBDD, MTBDD, int); */ TASK_DECL_2(MTBDD, mtbdd_op_max, MTBDD*, MTBDD*); TASK_DECL_3(MTBDD, mtbdd_abstract_op_max, MTBDD, MTBDD, int); - + /** * Compute a + b */ @@ -250,13 +250,13 @@ TASK_DECL_3(MTBDD, mtbdd_abstract_op_max, MTBDD, MTBDD, int); /** * Compute a - b */ -//#define mtbdd_minus(a, b) mtbdd_plus(a, mtbdd_negate(b)) +//#define mtbdd_minus(a, b) mtbdd_plus(a, mtbdd_negate(minus)) /** * Compute a * b */ #define mtbdd_times(a, b) mtbdd_apply(a, b, TASK(mtbdd_op_times)) - + /** * Compute min(a, b) */ @@ -310,7 +310,7 @@ TASK_DECL_2(MTBDD, mtbdd_op_threshold_double, MTBDD, size_t) * Monad that converts double to a Boolean MTBDD, translate terminals > value to 1 and to 0 otherwise; */ TASK_DECL_2(MTBDD, mtbdd_op_strict_threshold_double, MTBDD, size_t) - + /** * Convert double to a Boolean MTBDD, translate terminals >= value to 1 and to 0 otherwise; */ @@ -322,7 +322,7 @@ TASK_DECL_2(MTBDD, mtbdd_threshold_double, MTBDD, double); */ TASK_DECL_2(MTBDD, mtbdd_strict_threshold_double, MTBDD, double); #define mtbdd_strict_threshold_double(dd, value) CALL(mtbdd_strict_threshold_double, dd, value) - + /** * For two Double MTBDDs, calculate whether they are equal module some value epsilon * i.e. abs(a-b)<3 @@ -331,7 +331,7 @@ TASK_DECL_3(MTBDD, mtbdd_equal_norm_d, MTBDD, MTBDD, double); #define mtbdd_equal_norm_d(a, b, epsilon) CALL(mtbdd_equal_norm_d, a, b, epsilon) /** - * For two Double MTBDDs, calculate whether they are relatively equal module some value epsilon + * For two Double MTBDDs, calculate whether they are equal modulo some value epsilon * i.e. abs((a-b)/a) < e */ TASK_DECL_3(MTBDD, mtbdd_equal_norm_rel_d, MTBDD, MTBDD, double); @@ -391,6 +391,23 @@ TASK_DECL_1(MTBDD, mtbdd_minimum, MTBDD); TASK_DECL_1(MTBDD, mtbdd_maximum, MTBDD); #define mtbdd_maximum(dd) CALL(mtbdd_maximum, dd) +/** + * Enumeration. Get the next cube+terminal encoded by the MTBDD. + * The cube follows a variable assignment to each variable in the cube and + * ends with the terminal that the MTBDD assigns to that assignment. + * Terminal "false" is always skipped. + * + * Usage: + * MTBDD cube = mtbdd_enum_next(dd, variables, mtbdd_false, NULL); + * while (cube != mtbdd_false) { + * .... + * cube = mtbdd_enum_next(dd, variables, cube, NULL); + * } + * The callback is an optional function that returns 0 when the given terminal node should be skipped. + */ +typedef int (*mtbdd_enum_filter_cb)(MTBDD); +MTBDD mtbdd_enum_next(MTBDD dd, MTBDD variables, MTBDD prev, mtbdd_enum_filter_cb filter_cb); + /** * Write a DOT representation of a MTBDD * The callback function is required for custom terminals. diff --git a/resources/3rdparty/sylvan/src/sylvan_obj.hpp b/resources/3rdparty/sylvan/src/sylvan_obj.hpp index 94053afc7..e63cd0706 100644 --- a/resources/3rdparty/sylvan/src/sylvan_obj.hpp +++ b/resources/3rdparty/sylvan/src/sylvan_obj.hpp @@ -196,7 +196,7 @@ public: * @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. + * This function assumes that s,t are interleaved with s even and t odd (s+1). * 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 * @@ -209,7 +209,7 @@ public: * @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. + * This function assumes that s,t are interleaved with s even and t odd (s+1). * 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 * @@ -773,9 +773,9 @@ public: * @brief Gets the number of nodes in this Bdd. Not thread-safe! */ size_t NodeCount() const; - -#include "sylvan_obj_mtbdd_storm.hpp" +#include "sylvan_obj_mtbdd_storm.hpp" + private: MTBDD mtbdd; };