From 6902a3c8f82a37069d8c6b9bbfa41a4cf879be7a Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 8 Sep 2020 18:47:42 +0200 Subject: [PATCH] Revert "Fixed dot output of BDDs in sylvan." This reverts commit 6dcfd281867d5c360352ab2be98c420d4cdb9c0d. --- resources/3rdparty/sylvan/src/sylvan_mtbdd.c | 57 ++++++++------------ 1 file changed, 23 insertions(+), 34 deletions(-) diff --git a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c index 2397c9932..964b538be 100755 --- a/resources/3rdparty/sylvan/src/sylvan_mtbdd.c +++ b/resources/3rdparty/sylvan/src/sylvan_mtbdd.c @@ -3044,39 +3044,30 @@ mtbdd_leaf_to_str(MTBDD leaf, char *buf, size_t buflen) */ static void -mtbdd_fprintdot_rec(FILE *out, MTBDD mtbdd, int *mtbdd_true_marked, int *mtbdd_false_marked) +mtbdd_fprintdot_rec(FILE *out, MTBDD mtbdd) { - if (mtbdd == mtbdd_true) { - if (*mtbdd_true_marked) return; - *mtbdd_true_marked = 1; - fprintf(out, "%" PRIu64 " [shape=box, style=filled, label=\"T\"];\n", mtbdd); - } else if (mtbdd == mtbdd_false) { - if (*mtbdd_false_marked) return; - *mtbdd_false_marked = 1; - fprintf(out, "%" PRIu64 " [shape=box, style=filled, label=\"F\"];\n", mtbdd); + mtbddnode_t n = MTBDD_GETNODE(mtbdd); // also works for mtbdd_false + if (mtbddnode_getmark(n)) return; + mtbddnode_setmark(n, 1); + + if (mtbdd == mtbdd_true || mtbdd == mtbdd_false) { + fprintf(out, "0 [shape=box, style=filled, label=\"F\"];\n"); + } else if (mtbddnode_isleaf(n)) { + fprintf(out, "%" PRIu64 " [shape=box, style=filled, label=\"", MTBDD_STRIPMARK(mtbdd)); + mtbdd_fprint_leaf(out, mtbdd); + fprintf(out, "\"];\n"); } else { - mtbddnode_t n = MTBDD_GETNODE(mtbdd); // also works for mtbdd_false - if (mtbddnode_getmark(n)) return; - mtbddnode_setmark(n, 1); - if (mtbddnode_isleaf(n)) { - fprintf(out, "%" PRIu64 " [shape=box, style=filled, label=\"", MTBDD_STRIPMARK(mtbdd)); - mtbdd_fprint_leaf(out, mtbdd); - fprintf(out, "\"];\n"); - } else { - fprintf(out, "%" PRIu64 " [label=\"%" PRIu32 "\"];\n", - MTBDD_STRIPMARK(mtbdd), mtbddnode_getvariable(n)); - - mtbdd_fprintdot_rec(out, mtbddnode_getlow(n), mtbdd_true_marked, mtbdd_false_marked); - mtbdd_fprintdot_rec(out, mtbddnode_gethigh(n), mtbdd_true_marked, mtbdd_false_marked); - - fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=dashed];\n", - MTBDD_STRIPMARK(mtbdd), - (mtbddnode_getlow(n) == mtbdd_true || mtbddnode_getlow(n) == mtbdd_false) ? mtbddnode_getlow(n) : MTBDD_STRIPMARK(mtbddnode_getlow(n))); - fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=solid dir=both arrowtail=%s];\n", - MTBDD_STRIPMARK(mtbdd), - (mtbddnode_gethigh(n) == mtbdd_true || mtbddnode_gethigh(n) == mtbdd_false) ? mtbddnode_gethigh(n) : MTBDD_STRIPMARK(mtbddnode_gethigh(n)), - mtbddnode_getcomp(n) ? "dot" : "none"); - } + fprintf(out, "%" PRIu64 " [label=\"%" PRIu32 "\"];\n", + MTBDD_STRIPMARK(mtbdd), mtbddnode_getvariable(n)); + + mtbdd_fprintdot_rec(out, mtbddnode_getlow(n)); + mtbdd_fprintdot_rec(out, mtbddnode_gethigh(n)); + + fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=dashed];\n", + MTBDD_STRIPMARK(mtbdd), mtbddnode_getlow(n)); + fprintf(out, "%" PRIu64 " -> %" PRIu64 " [style=solid dir=both arrowtail=%s];\n", + MTBDD_STRIPMARK(mtbdd), MTBDD_STRIPMARK(mtbddnode_gethigh(n)), + mtbddnode_getcomp(n) ? "dot" : "none"); } } @@ -3091,9 +3082,7 @@ mtbdd_fprintdot(FILE *out, MTBDD mtbdd) fprintf(out, "root -> %" PRIu64 " [style=solid dir=both arrowtail=%s];\n", MTBDD_STRIPMARK(mtbdd), MTBDD_HASMARK(mtbdd) ? "dot" : "none"); - int mtbdd_true_marked = 0; - int mtbdd_false_marked = 0; - mtbdd_fprintdot_rec(out, mtbdd, &mtbdd_true_marked, &mtbdd_false_marked); + mtbdd_fprintdot_rec(out, mtbdd); mtbdd_unmark_rec(mtbdd); fprintf(out, "}\n");