From 7149521f4899b6d5dcaba5fb9aa8af9c6215dd51 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 13 Sep 2023 11:31:49 +0200 Subject: [PATCH] relabel_bse: rework to simplify more patterns Rework the way we compute and use cut-points to catch more patterns we can rewrite. Also Use BDDs to check if a Boolean sub-expression is false or true. Fixes issue #540. * spot/tl/relabel.hh: Update documentation * spot/tl/relabel.cc (relabel_bse): Rework. * tests/core/ltlfilt.test: Add more test cases. * tests/python/_mealy.ipynb: Update. * NEWS: Mention the change. --- NEWS | 5 + spot/tl/relabel.cc | 214 +++++++++++++++++++++----------------- spot/tl/relabel.hh | 8 +- tests/core/ltlfilt.test | 125 +++++++++++++++++++++- tests/python/_mealy.ipynb | 112 ++++++++++---------- 5 files changed, 305 insertions(+), 159 deletions(-) diff --git a/NEWS b/NEWS index d2c5ce5cb..8f147ad35 100644 --- a/NEWS +++ b/NEWS @@ -33,6 +33,11 @@ New in spot 2.11.6.dev (not yet released) - spot::bdd_to_cnf_formula() is a new variant of spot::bdd_to_formula() that converts a BDD into a CNF instead of a DNF. + - spot::relabel_bse() has been improved to better deal with more + cases. For instance '(a & b & c) U (!c & d & e)' is now + correctly reduced as '(p0 & p1) U (!p1 & p2)', and + '((a & !b) | (a->b)) U c' now becomes '1 U c'. (Issue #540.) + - spot::relabel_overlapping_bse() is a new function that will replace boolean subformulas by fresh atomic propositions even if those subformulas share atomic propositions. diff --git a/spot/tl/relabel.cc b/spot/tl/relabel.cc index f57c0c919..7fe94842c 100644 --- a/spot/tl/relabel.cc +++ b/spot/tl/relabel.cc @@ -19,6 +19,7 @@ #include "config.h" #include +#include #include #include #include @@ -82,7 +83,7 @@ namespace spot // if subexp == false, matches APs // if subexp == true, matches boolean subexps - template + template class relabeler { public: @@ -90,6 +91,7 @@ namespace spot map newname; ap_generator* gen; relabeling_map* oldnames; + tl_simplifier tl; relabeler(ap_generator* gen, relabeling_map* m) : gen(gen), oldnames(m) @@ -115,6 +117,16 @@ namespace spot if (!r.second) return r.first->second; + if constexpr (use_bdd) + if (!old.is(op::ap)) + { + bdd b = tl.as_bdd(old); + if (b == bddtrue) + return r.first->second = formula::tt(); + if (b == bddfalse) + return r.first->second = formula::ff(); + } + formula res = gen->next(); r.first->second = res; if (oldnames) @@ -269,7 +281,7 @@ namespace spot // Furthermore, because we are already representing LTL formulas // with sharing of identical sub-expressions we can easily rename // a subexpression (such as c&d above) only once. However this - // scheme has two problems: + // scheme (done by relabel_overlapping_bse()) has two problems: // // A. It will not detect inter-dependent Boolean subexpressions. // For instance it will mistakenly relabel "(a & b) U (a & !b)" @@ -278,53 +290,40 @@ namespace spot // B. Because of our n-ary operators, it will fail to // notice that (a & b) is a sub-expression of (a & b & c). // - // The way we compute the subexpressions that can be relabeled is - // by transforming the formula syntax tree into an undirected - // graph, and computing the cut points of this graph. The cut - // points (or articulation points) are the nodes whose removal - // would split the graph in two components. To ensure that a - // Boolean operator is only considered as a cut point if it would - // separate all of its children from the rest of the graph, we - // connect all the children of Boolean operators. + // The way we compute the subexpressions that can be relabeled is by + // transforming the formula syntax tree into an undirected graph, + // and computing the cut-points of this graph. The cut-points (or + // articulation points) are the nodes whose removal would split the + // graph in two components; in our case, we extend this definition to + // also consider the leaves as cut-points. // - // For instance (a & b) U (c & d) has two (Boolean) cut points - // corresponding to the two AND operators: + // For instance ((a|b)&c&d)U(!d&e&f) is represented by + // the following graph, were cut-points are marked with *. // - // (a&b)U(c&d) - // ╱ ╲ - // a&b c&d - // ╱ ╲ ╱ ╲ - // a─────b c─────d + // ((a|b)&c&d)U(!d&e&f) + // ╱ ╲ + // ((a|b)&c&d)* (!d&e&f)* + // ╱ │ ╲ ╱ │ ╲ + // a|b* │ ╲ ! │ ╲ + // ╱ ╲ │ ╲ ╱ │ ╲ + // a* b* c* d e* f* // - // (The root node is also a cut point, but we only consider Boolean - // cut points for relabeling.) + // The relabeling of a formula is done in 3 passes: + // 1. Convert the formula's syntax tree into an undirected graph. + // 2. Compute the (Boolean) cut points of that graph, using the + // Hopcroft-Tarjan algorithm (see below for a reference). + // 3. Recursively scan the formula's tree until we reach + // a (Boolean) cut-point. If all the children of this node + // are cut-points, rename the node with a fresh label. + // If it's a n-ary operator, group all children that are + // and cut-points relabel them as a whole. // - // On the other hand, (a & b) U (b & !c) has only one Boolean - // cut-point which corresponds to the NOT operator: - // - // (a&b)U(b&!c) - // ╱ ╲ - // a&b b&!c - // ╱ ╲ ╱ ╲ - // a─────b────!c - // │ - // c - // - // Note that if the children of a&b and b&c were not connected, - // a&b and b&c would be considered as cut points because they - // separate "a" or "!c" from the rest of the graph. - // - // The relabeling of a formula is therefore done in 3 passes: - // 1. convert the formula's syntax tree into an undirected graph, - // adding links between children of Boolean operators - // 2. compute the (Boolean) cut points of that graph, using the - // Hopcroft-Tarjan algorithm (see below for a reference) - // 3. recursively scan the formula's tree until we reach - // either a (Boolean) cut point or an atomic proposition, and - // replace that node by a fresh atomic proposition. - // - // In the example above (a&b)U(b&!c), the last recursion - // stops on a, b, and !c, producing (p0&p1)U(p1&p2). + // On the above example, when processing the cut-point + // ((a|b)&c&d) we group its children that are cut-points + // (a|b)&c and rename this group as p0. Then d gets + // his own name p1, and when processing (!d&e&f) we group + // e&f because they are both cut-points, are rename them p1. + // The result is (p0 & p1) U (!p1 & p2). // // Problem #B above (handling of n-ary expression) need some // additional tricks. Consider (a&b&c&d) U X(c&d), and assume @@ -343,24 +342,19 @@ namespace spot // Convert the formula's syntax tree into an undirected graph // labeled by subformulas. - class formula_to_fgraph + class formula_to_fgraph final { public: fgraph& g; std::stack s; sub_formula_count_t& subcount; - formula_to_fgraph(fgraph& g, sub_formula_count_t& subcount): - g(g), subcount(subcount) - { - } + formula_to_fgraph(fgraph& g, sub_formula_count_t& subcount) + : g(g), subcount(subcount) + { + } - ~formula_to_fgraph() - { - } - - void - visit(formula f) + void visit(formula f) { { // Connect to parent @@ -411,27 +405,6 @@ namespace spot } for (; i < sz; ++i) visit(f[i]); - if (sz > 1 && f.is_boolean()) - { - // For Boolean nodes, connect all children in a - // loop. This way the node can only be a cut point - // if it separates all children from the reset of - // the graph (not only one). - formula pred = f[0]; - for (i = 1; i < sz; ++i) - { - formula next = f[i]; - // Note that we add an edge in both directions, - // as the cut point algorithm really need undirected - // graphs. (We used to do only one direction, and - // that turned out to be a bug.) - g[pred].emplace_back(next); - g[next].emplace_back(pred); - pred = next; - } - g[pred].emplace_back(f[0]); - g[f[0]].emplace_back(pred); - } done: s.pop(); } @@ -465,11 +438,12 @@ namespace spot // the ACM, 16 (6), June 1973. // // It differs from the original algorithm by returning only the - // Boolean cutpoints, and not dealing with the initial state + // Boolean cut-points, not dealing with the initial state // properly (our initial state will always be considered as a // cut-point, but since we only return Boolean cut-points it's // OK: if the top-most formula is Boolean we want to replace it - // as a whole). + // as a whole), and considering the atomic propositions that + // are leaves as cutpoints too. void cut_points(const fgraph& g, fset& c, formula start) { stack_t s; @@ -530,7 +504,14 @@ namespace spot data_entry& dgrand_parent = data[grand_parent]; if (dparent.low >= dgrand_parent.num // cut-point && grand_parent.is_boolean()) - c.insert(grand_parent); + { + c.insert(grand_parent); + // Also consider atomic propositions as + // cut-points if they are leaves. + if (parent.is(op::ap) + && g.find(parent)->second.size() == 1) + c.insert(parent); + } if (dparent.low < dgrand_parent.low) dgrand_parent.low = dparent.low; } @@ -539,7 +520,7 @@ namespace spot } - class bse_relabeler final: public relabeler + class bse_relabeler final: public relabeler { public: const fset& c; @@ -553,12 +534,45 @@ namespace spot using relabeler::visit; - formula - visit(formula f) + formula visit(formula f) { - if (f.is(op::ap) || (c.find(f) != c.end())) + if (f.is(op::ap)) return rename(f); + // This is Boolean cut-point? + // We can only relabel it if all its children are cut-points. + if (c.find(f) != c.end()) + { + unsigned fsz = f.size(); + assert(fsz > 0); // A cut point has children + if (fsz == 1 + || (fsz == 2 + && ((c.find(f[0]) != c.end()) + == (c.find(f[1]) != c.end())))) + return rename(f); + if (fsz > 2) + { + // cp[0] will contains non cut-points + // cp[1] will contain cut-points or atomic propositions + std::vector cp[2]; + cp[0].reserve(fsz); + cp[1].reserve(fsz); + for (unsigned i = 0; i < fsz; ++i) + { + formula cf = f[i]; + cp[c.find(cf) != c.end()].push_back(cf); + } + if (cp[0].empty() + || cp[1].empty()) + // all children are cut-points or non-cut-points + return rename(f); + formula cp1group = rename(formula::multop(f.kind(), cp[1])); + formula cp0group = visit(formula::multop(f.kind(), cp[0])); + return formula::multop(f.kind(), {cp1group, cp0group}); + } + } + + // Not a cut-point, recurse unsigned sz = f.size(); if (sz <= 2) return f.map([this](formula f) @@ -566,24 +580,24 @@ namespace spot return visit(f); }); - unsigned i = 0; - std::vector res; if (f.is_boolean() && sz > 2) - { - // If we have a Boolean formula with more than two - // children, like (a & b & c & d) where some children - // (assume {a,b}) are used only once, but some other - // (assume {c,d}) are used multiple time in the formula, - // then split that into ((a & b) & (c & d)) to give - // (a & b) a chance to be relabeled as a whole. - auto pair = split_used_once(f, subcount); - if (pair.second) - return formula::multop(f.kind(), { visit(pair.first), - visit(pair.second) }); - } + // If we have a Boolean formula with more than two + // children, like (a & b & c & d) where some children + // (assume {a,b}) are used only once, but some other + // (assume {c,d}) are used multiple time in the formula, + // then split that into ((a & b) & (c & d)) to give + // (a & b) a chance to be relabeled as a whole. + if (auto pair = split_used_once(f, subcount); pair.second) + { + formula left = visit(pair.first); + formula right = visit(pair.second); + return formula::multop(f.kind(), { left, right }); + } /// If we have a formula like (a & b & Xc), consider /// it as ((a & b) & Xc) in the graph to isolate the /// Boolean operands as a single node. + unsigned i = 0; + std::vector res; formula b = f.boolean_operands(&i); if (b && b != f) { @@ -630,6 +644,10 @@ namespace spot fset c; cut_points(g, c, f); + // std::cerr << "cut-points\n"; + // for (formula cp: c) + // std::cerr << " - " << cp << '\n'; + // Relabel the formula recursively, stopping // at cut-points or atomic propositions. ap_generator* gen = nullptr; diff --git a/spot/tl/relabel.hh b/spot/tl/relabel.hh index 59efdf94b..5d076f10c 100644 --- a/spot/tl/relabel.hh +++ b/spot/tl/relabel.hh @@ -53,13 +53,13 @@ namespace spot /// proposition for each maximal Boolean subexpression encountered, /// even if they overlap (i.e., share common atomic /// propositions). For instance `(a & b & c) U (c & d & e)` will be - /// simply be relabeled as `p0 U p1`. This kind of renaming to not - /// preserves the + /// simply be relabeled as `p0 U p1`. This kind of renaming does not + /// preserve the satisfiability of the input formula. /// /// The relabel_bse() version will make sure that the replaced /// subexpressions do not share atomic propositions. For instance - /// `(a & b & c) U (c & d & e)` will be simply be relabeled as - /// `(p0 & p1) U (p1 & p2)`, were `p1` replaces `c` and the rest + /// `(a & b & c) U (!c & d & e)` will be simply be relabeled as + /// `(p0 & p1) U (!p1 & p2)`, were `p1` replaces `c` and the rest /// is obvious. /// /// @{ diff --git a/tests/core/ltlfilt.test b/tests/core/ltlfilt.test index 192a60fef..f28ee445d 100755 --- a/tests/core/ltlfilt.test +++ b/tests/core/ltlfilt.test @@ -363,6 +363,14 @@ b & GF(a | c) & !GF!(a | c) F(a <-> b) -> (c xor d) (a & b & c) U (c & d & e) (a & b & c) U !(a & b & c) +(a & b & c) U (!c & d & e) +((a | b) & c & d) U (!d & e & f) +((a | b) & d) U (!d & e & f) +(a & !a) | (b & !b) | (c & !c) +((a & !a) | (b & !b) | (c & !c)) U d +((a & !a) | (b & !b) | (c & e)) U d +((a & !b) | (!a & b)) U c +((a & !b) | (a->b)) U c EOF cat >exp <out @@ -405,6 +419,22 @@ p0 || []p1 #define p1 (b) #define p2 (c) (p0 && p1 && p2) U (!p0 || !p1 || !p2) +#define p0 (a && b) +#define p1 (c) +#define p2 (d && e) +(p0 && p1) U (!p1 && p2) +#define p0 (d) +#define p1 (a || b) +#define p2 (e && f) +(p0 && p1) U (!p0 && p2) +false +#define p0 (d) +p0 +#define p0 ((a && !a) || (b && !b) || (c && e)) +#define p1 (d) +p0 U p1 +#define p0 (c) +true U p0 EOF run 0 ltlfilt -s -u --nnf --relabel-bool=pnn --define in >out @@ -455,6 +485,48 @@ p0 && []<>(p1 || p2) && ![]<>!(p1 || p2) #define p1 (b) #define p2 (c) (p0 && p1 && p2) U !(p0 && p1 && p2) +#define p0 (a) +#define p1 (b) +#define p2 (c) +#define p3 (d) +#define p4 (e) +(p0 && p1 && p2) U (!p2 && p3 && p4) +#define p0 (c) +#define p1 (d) +#define p2 (a) +#define p3 (b) +#define p4 (e) +#define p5 (f) +(p0 && p1 && (p2 || p3)) U (!p1 && p4 && p5) +#define p0 (d) +#define p1 (a) +#define p2 (b) +#define p3 (e) +#define p4 (f) +(p0 && (p1 || p2)) U (!p0 && p3 && p4) +#define p0 (a) +#define p1 (b) +#define p2 (c) +(p0 && !p0) || (p1 && !p1) || (p2 && !p2) +#define p0 (a) +#define p1 (b) +#define p2 (c) +#define p3 (d) +((p0 && !p0) || (p1 && !p1) || (p2 && !p2)) U p3 +#define p0 (a) +#define p1 (b) +#define p2 (c) +#define p3 (e) +#define p4 (d) +((p2 && p3) || (p0 && !p0) || (p1 && !p1)) U p4 +#define p0 (a) +#define p1 (b) +#define p2 (c) +((p0 && !p1) || (!p0 && p1)) U p2 +#define p0 (a) +#define p1 (b) +#define p2 (c) +((p0 && !p1) || (p0 -> p1)) U p2 EOF run 0 ltlfilt -s -u --relabel=pnn --define in >out @@ -486,12 +558,13 @@ Fp0 -> p1 p0 U p1 #define p0 (a & b & c) p0 U !p0 +#define p0 ((a & !a) | (b & !b) | (c & !c)) +p0 EOF run 0 ltlfilt -u --relabel-over=pnn --define in >out diff exp out - toolong='((p2=0) * (p3=1))' # work around the 80-col check cat >exp <exp <out diff exp out @@ -550,6 +665,14 @@ b & GF(a | c) & !GF!(a | c)@ F(a <-> b) -> (c xor d)@ (a & b & c) U (c & d & e)@ (a & b & c) U !(a & b & c)@ +(a & b & c) U (!c & d & e)@ +(c & d & (a | b)) U (!d & e & f)@ +(d & (a | b)) U (!d & e & f)@ +(a & !a) | (b & !b) | (c & !c)@ +((a & !a) | (b & !b) | (c & !c)) U d@ +((a & !a) | (b & !b) | (c & e)) U d@ +((a & !b) | (!a & b)) U c@ +((a -> b) | (a & !b)) U c@ EOF diff exp out diff --git a/tests/python/_mealy.ipynb b/tests/python/_mealy.ipynb index ebeeaacb7..20ea5fd4e 100644 --- a/tests/python/_mealy.ipynb +++ b/tests/python/_mealy.ipynb @@ -129,7 +129,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f86481a2690> >" + " *' at 0x7f8877796550> >" ] }, "execution_count": 4, @@ -209,7 +209,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f85f45cbb70> >" + " *' at 0x7f8877796820> >" ] }, "execution_count": 6, @@ -283,7 +283,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f85f45cbb70> >" + " *' at 0x7f8877796820> >" ] }, "execution_count": 8, @@ -387,7 +387,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f861bfc8ae0> >" + " *' at 0x7f8877797b40> >" ] }, "execution_count": 9, @@ -532,7 +532,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f85f45efde0> >" + " *' at 0x7f88777970f0> >" ] }, "execution_count": 10, @@ -600,15 +600,15 @@ " \n", " 0\n", " presat\n", - " 3868.95\n", - " 3.282e-06\n", - " 1.4388e-05\n", - " 0.000129765\n", - " 1.3759e-05\n", - " 9.499e-06\n", - " 8.73e-06\n", - " 9.01e-06\n", - " 6.6209e-05\n", + " 7.7176e-05\n", + " 2.863e-06\n", + " 1.6553e-05\n", + " 0.000186061\n", + " 7.753e-06\n", + " 1.0616e-05\n", + " 1.1804e-05\n", + " 8.101e-06\n", + " 6.7328e-05\n", " ...\n", " NaN\n", " NaN\n", @@ -634,7 +634,7 @@ " NaN\n", " NaN\n", " ...\n", - " 0.000743251\n", + " 0.000496302\n", " 2\n", " 0\n", " 7\n", @@ -652,16 +652,16 @@ ], "text/plain": [ " task premin_time reorg_time partsol_time player_incomp_time incomp_time \\\n", - "0 presat 3868.95 3.282e-06 1.4388e-05 0.000129765 1.3759e-05 \n", + "0 presat 7.7176e-05 2.863e-06 1.6553e-05 0.000186061 7.753e-06 \n", "1 sat NaN NaN NaN NaN NaN \n", "\n", " split_all_let_time split_min_let_time split_cstr_time prob_init_build_time \\\n", - "0 9.499e-06 8.73e-06 9.01e-06 6.6209e-05 \n", + "0 1.0616e-05 1.1804e-05 8.101e-06 6.7328e-05 \n", "1 NaN NaN NaN NaN \n", "\n", " ... total_time n_classes n_refinement n_lit n_clauses n_iteration \\\n", "0 ... NaN NaN NaN NaN NaN NaN \n", - "1 ... 0.000743251 2 0 7 12 0 \n", + "1 ... 0.000496302 2 0 7 12 0 \n", "\n", " n_letters_part n_bisim_let n_min_states done \n", "0 3 2 NaN NaN \n", @@ -758,7 +758,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f861bfc8630> >" + " *' at 0x7f8877796eb0> >" ] }, "execution_count": 11, @@ -855,13 +855,13 @@ "1\n", "/\n", "\n", - "(!o0 & o1) | (o0 & !o1)\n", + "(o0 & !o1) | (!o0 & o1)\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f861bf9fb40> >" + " *' at 0x7f8877797120> >" ] }, "execution_count": 12, @@ -994,13 +994,13 @@ "5->2\n", "\n", "\n", - "(!o0 & o1) | (o0 & !o1)\n", + "(o0 & !o1) | (!o0 & o1)\n", "\n", "\n", "\n" ], "text/plain": [ - " *' at 0x7f861bf9f210> >" + " *' at 0x7f8877797990> >" ] }, "execution_count": 13, @@ -1067,15 +1067,15 @@ " \n", " 0\n", " presat\n", - " 3869.08\n", - " 3.213e-06\n", - " 9.079e-06\n", - " 9.5752e-05\n", - " 5.168e-06\n", - " 5.727e-06\n", - " 7.543e-06\n", - " 1.5784e-05\n", - " 4.0507e-05\n", + " 3.282e-06\n", + " 3.702e-06\n", + " 1.4248e-05\n", + " 0.000109094\n", + " 6.705e-06\n", + " 9.219e-06\n", + " 8.52e-06\n", + " 1.0407e-05\n", + " 3.2896e-05\n", " ...\n", " NaN\n", " NaN\n", @@ -1149,7 +1149,7 @@ " NaN\n", " NaN\n", " ...\n", - " 0.000399073\n", + " 0.00041242\n", " 2\n", " 0\n", " 17\n", @@ -1167,22 +1167,22 @@ ], "text/plain": [ " task premin_time reorg_time partsol_time player_incomp_time \\\n", - "0 presat 3869.08 3.213e-06 9.079e-06 9.5752e-05 \n", + "0 presat 3.282e-06 3.702e-06 1.4248e-05 0.000109094 \n", "1 sat NaN NaN NaN NaN \n", "2 refinement NaN NaN NaN NaN \n", "3 sat NaN NaN NaN NaN \n", "\n", " incomp_time split_all_let_time split_min_let_time split_cstr_time \\\n", - "0 5.168e-06 5.727e-06 7.543e-06 1.5784e-05 \n", + "0 6.705e-06 9.219e-06 8.52e-06 1.0407e-05 \n", "1 NaN NaN NaN NaN \n", "2 NaN NaN NaN NaN \n", "3 NaN NaN NaN NaN \n", "\n", - " prob_init_build_time ... total_time n_classes n_refinement n_lit \\\n", - "0 4.0507e-05 ... NaN NaN NaN NaN \n", - "1 NaN ... NaN 1 0 3 \n", - "2 NaN ... NaN 1 1 10 \n", - "3 NaN ... 0.000399073 2 0 17 \n", + " prob_init_build_time ... total_time n_classes n_refinement n_lit \\\n", + "0 3.2896e-05 ... NaN NaN NaN NaN \n", + "1 NaN ... NaN 1 0 3 \n", + "2 NaN ... NaN 1 1 10 \n", + "3 NaN ... 0.00041242 2 0 17 \n", "\n", " n_clauses n_iteration n_letters_part n_bisim_let n_min_states done \n", "0 NaN NaN 1 1 NaN NaN \n", @@ -1286,7 +1286,7 @@ "\n" ], "text/plain": [ - " *' at 0x7f861bfcdc00> >" + " *' at 0x7f8877797cc0> >" ] }, "execution_count": 14, @@ -1365,15 +1365,15 @@ " \n", " 0\n", " presat\n", - " 3869.14\n", - " 2.863e-06\n", - " 9.08e-06\n", - " 6.0622e-05\n", - " 4.679e-06\n", - " 5.308e-06\n", - " 8.59e-06\n", - " 7.962e-06\n", - " 4.0159e-05\n", + " 1.956e-06\n", + " 2.445e-06\n", + " 8.171e-06\n", + " 5.0007e-05\n", + " 4.819e-06\n", + " 6.077e-06\n", + " 5.797e-06\n", + " 4.33e-06\n", + " 2.242e-05\n", " ...\n", " NaN\n", " NaN\n", @@ -1447,7 +1447,7 @@ " NaN\n", " NaN\n", " ...\n", - " 0.000416464\n", + " 0.000252132\n", " 2\n", " 0\n", " 17\n", @@ -1465,22 +1465,22 @@ ], "text/plain": [ " task premin_time reorg_time partsol_time player_incomp_time \\\n", - "0 presat 3869.14 2.863e-06 9.08e-06 6.0622e-05 \n", + "0 presat 1.956e-06 2.445e-06 8.171e-06 5.0007e-05 \n", "1 sat NaN NaN NaN NaN \n", "2 refinement NaN NaN NaN NaN \n", "3 sat NaN NaN NaN NaN \n", "\n", " incomp_time split_all_let_time split_min_let_time split_cstr_time \\\n", - "0 4.679e-06 5.308e-06 8.59e-06 7.962e-06 \n", + "0 4.819e-06 6.077e-06 5.797e-06 4.33e-06 \n", "1 NaN NaN NaN NaN \n", "2 NaN NaN NaN NaN \n", "3 NaN NaN NaN NaN \n", "\n", " prob_init_build_time ... total_time n_classes n_refinement n_lit \\\n", - "0 4.0159e-05 ... NaN NaN NaN NaN \n", + "0 2.242e-05 ... NaN NaN NaN NaN \n", "1 NaN ... NaN 1 0 3 \n", "2 NaN ... NaN 1 1 10 \n", - "3 NaN ... 0.000416464 2 0 17 \n", + "3 NaN ... 0.000252132 2 0 17 \n", "\n", " n_clauses n_iteration n_letters_part n_bisim_let n_min_states done \n", "0 NaN NaN 1 1 NaN NaN \n", @@ -1705,7 +1705,7 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.8.10" + "version": "3.11.5" }, "vscode": { "interpreter": {