update to newest version of sylvan

Former-commit-id: c727c9c57a

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);

resources/3rdparty/sylvan/src/sylvan_mtbdd.c

@@ -14,7 +14,7 @@
  * limitations under the License.
  */
 
-#include "sylvan_config.h"
+#include <sylvan_config.h>
 
 #include <assert.h>
 #include <inttypes.h>
@@ -25,11 +25,11 @@
 #include <stdlib.h>
 #include <string.h>
 
-#include "refs.h"
-#include "sha2.h"
-#include "sylvan.h"
-#include "sylvan_common.h"
-#include "sylvan_mtbdd_int.h"
+#include <refs.h>
+#include <sha2.h>
+#include <sylvan.h>
+#include <sylvan_common.h>
+#include <sylvan_mtbdd_int.h>
 
 /* 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 <variables>
+        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 <variables>
+        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"
+

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.

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;
 };