diff --git a/src/ast/rewriter/seq_monadic.cpp b/src/ast/rewriter/seq_monadic.cpp index 4f9f1993b1..95e4626949 100644 --- a/src/ast/rewriter/seq_monadic.cpp +++ b/src/ast/rewriter/seq_monadic.cpp @@ -29,19 +29,6 @@ TODOs: Model construction would assign values to the elements. - make unsat core tracking less naive by tracking dependencies at a finer grain. - add selective tracing TRACE(seq, ..). -- revisit DFS to select next membership constraint to explore base on the current state. - In the current state include current set of variable intersection membership constraints. - The next membership constraint to explore is preferrably for a variable that was just - explored and we can check the variable intersection membership constraints if the new - expansion is feasible. Constant characters are consumed at the same time to also prune - the choice. -- separate out "live-state" and enumerator over reachable live states: - - make it share live states between callers. - - make it expose an iterator instead of using vectors of live states to allow on-demand expansion of live states. - - make use of DFS exploration of derivatives to extract live states without visiting all states up front. - - use it in seq_regex legacy mode that also has this notion. - - Author: @@ -72,24 +59,29 @@ namespace { } } - char const* bail_name(unsigned i) { - static char const* const names[] = { - "unsupported", - "state-cap", - "dnf-cap", - "budget", - "resource", - "nullability", - "guard" - }; - return i < std::size(names) ? names[i] : "unknown"; - } - char const* result_name(lbool r) { return r == l_true ? "sat" : r == l_false ? "unsat" : "unknown"; } } +#define SEQ_MONADIC_BAIL_PREFIX "seq monadic bail " + +char const* seq_monadic::bail_stat_name(bail_reason reason) { + switch (reason) { + case bail_reason::unsupported: return SEQ_MONADIC_BAIL_PREFIX "unsupported"; + case bail_reason::state_cap: return SEQ_MONADIC_BAIL_PREFIX "state cap"; + case bail_reason::budget: return SEQ_MONADIC_BAIL_PREFIX "budget"; + case bail_reason::resource: return SEQ_MONADIC_BAIL_PREFIX "resource"; + case bail_reason::nullability: return SEQ_MONADIC_BAIL_PREFIX "nullability"; + case bail_reason::guard: return SEQ_MONADIC_BAIL_PREFIX "guard"; + default: return SEQ_MONADIC_BAIL_PREFIX "unknown"; + } +} + +char const* seq_monadic::bail_name(bail_reason reason) { + return bail_stat_name(reason) + (sizeof(SEQ_MONADIC_BAIL_PREFIX) - 1); +} + expr_ref seq_monadic::der_elem(expr* r, expr* elem) { expr* cached = nullptr; @@ -509,6 +501,8 @@ unsigned seq_monadic::var_index(expr* v) { m_var_idx.insert(v, vi); m_vars.push_back(v); m_groups.push_back(svector()); + m_num_occ.push_back(0); + m_head_cnt.push_back(0); return vi; } @@ -520,13 +514,15 @@ void seq_monadic::reset_search() { m_vars.reset(); m_var_idx.reset(); m_groups.reset(); - m_last_occ.reset(); + m_num_occ.reset(); m_group_cache.clear(); m_der_cache.reset(); m_nullable_cache.reset(); m_undef_vars = 0; m_cursors.reset(); m_last_var = UINT_MAX; + m_head_cnt.reset(); + m_head_stack.reset(); m_live_states.reset(); } @@ -550,17 +546,12 @@ bool seq_monadic::prepare(membership_vec const& memberships) { m_atoms.push_back(atoms); m_pin.push_back(regex); } - // A variable's component group is complete once the search passes the variable's - // last occurrence; positions are compared in search order, i.e. lexicographically - // on (membership index, atom index). for (unsigned mi = 0; mi < m_atoms.size(); ++mi) { vector const& atoms = m_atoms[mi]; - for (unsigned i = 0; i < atoms.size(); ++i) { - if (!atoms[i].is_var) + for (atom const& a : atoms) { + if (!a.is_var) continue; - expr* v = atoms[i].var.get(); - var_index(v); - m_last_occ.insert(v, (static_cast(mi) << 32) | i); + ++m_num_occ[var_index(a.var.get())]; } } return true; @@ -614,6 +605,23 @@ lbool seq_monadic::leaf() { return l_true; } +bool seq_monadic::inc_budget() { + if (m_giveup) + return false; // unwind the whole search, don't keep branching + if (m_budget == 0) { + m_stats.inc_bail(bail_reason::budget); + m_giveup = true; + return false; + } + if (!m.inc()) { + m_stats.inc_bail(bail_reason::resource); + m_giveup = true; + return false; + } + --m_budget; + return true; +} + lbool seq_monadic::dfs_membership(unsigned mi) { if (mi == m_atoms.size()) return leaf(); @@ -621,19 +629,8 @@ lbool seq_monadic::dfs_membership(unsigned mi) { } lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) { - if (m_giveup) - return l_undef; // unwind the whole search, don't keep branching - if (m_budget == 0) { - m_stats.inc_bail(bail_reason::budget); - m_giveup = true; + if (!inc_budget()) return l_undef; - } - if (!m.inc()) { - m_stats.inc_bail(bail_reason::resource); - m_giveup = true; - return l_undef; - } - --m_budget; vector const& atoms = m_atoms[mi]; if (i == atoms.size()) { // the rest of this membership is epsilon lbool nb = nullable(R); @@ -649,7 +646,6 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) { expr_ref d = der_elem(R, a.elem.get()); if (re().is_empty(d)) return l_false; - m_pin.push_back(d); return dfs_atoms(mi, i + 1, d); } @@ -657,9 +653,6 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) { // the derivative automaton from R to some live state q, which splits the search. bool last_atom = (i + 1 == atoms.size()); unsigned vi = var_index(a.var.get()); - uint64_t pos = (static_cast(mi) << 32) | i; - uint64_t last = 0; - bool finalize = m_last_occ.find(a.var.get(), last) && last == pos; // Explores one split target; the caller stops at the first l_true. auto explore = [&](expr* target) -> lbool { @@ -670,7 +663,7 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) { lbool ne = l_true; if (re().is_empty(R)) ne = l_false; - else if (finalize || m_groups[vi].size() > 1) + else if (group_complete(vi) || m_groups[vi].size() > 1) ne = group_nonempty(vi); lbool r; if (ne == l_false) @@ -731,179 +724,116 @@ lbool seq_monadic::dfs_atoms(unsigned mi, unsigned i, expr* R) { // - the per-variable component groups (m_groups) == variable intersection constraints, // - the last expanded variable (m_last_var) == locality hint for the next choice. // Every non-complete cursor has a variable head (leading constants are eagerly consumed by -// advance_cursor / initial_normalize). The state is complete when every cursor is -// complete, and accepting when additionally every variable group is non-empty. +// consume_constants). The state is complete when every cursor is complete, and accepting +// when additionally every variable group is non-empty. + +lbool seq_monadic::consume_constants(cursor& c, unsigned mi) { + vector const& atoms = m_atoms[mi]; + while (c.i < atoms.size() && !atoms[c.i].is_var) { + expr_ref d = der_elem(c.R, atoms[c.i].elem.get()); + if (re().is_empty(d)) + return l_false; // dead: this continuation is empty + c.R = d; + c.i += 1; + } + c.complete = (c.i == atoms.size()); + if (!c.complete) + return l_true; // stopped on a variable head + lbool nb = nullable(c.R); // the remaining tail is epsilon + if (nb == l_false) + return l_false; + if (nb == l_undef) { + m_stats.inc_bail(bail_reason::nullability); + return l_undef; // tail nullability undecidable + } + return l_true; +} lbool seq_monadic::advance_cursor(cursor& c, unsigned mi, expr* target) { - vector const& atoms = m_atoms[mi]; // Step past the head variable. target == null encodes "the variable is the last atom", // i.e. a plain membership component: nothing follows, the cursor is complete. if (!target) { - c.i = atoms.size(); + c.i = m_atoms[mi].size(); c.complete = true; return l_true; } c.i += 1; c.R = target; - // Eagerly consume the constant atoms following the variable (mirrors dfs_atoms walking - // a run of constants via der_elem), so that the cursor again exposes a variable head. - while (c.i < atoms.size() && !atoms[c.i].is_var) { - expr_ref d = der_elem(c.R, atoms[c.i].elem.get()); - if (re().is_empty(d)) - return l_false; // dead: this continuation is empty - m_pin.push_back(d); - c.R = d; - c.i += 1; - } - if (c.i == atoms.size()) { // the remaining tail is epsilon - c.complete = true; - lbool nb = nullable(c.R); - if (nb == l_false) - return l_false; - if (nb == l_undef) { - m_stats.inc_bail(bail_reason::nullability); - return l_undef; // tail nullability undecidable - } - return l_true; - } - c.complete = false; // stopped on a variable head - return l_true; -} - -lbool seq_monadic::initial_normalize() { - for (unsigned mi = 0; mi < m_cursors.size(); ++mi) { - cursor& c = m_cursors[mi]; - vector const& atoms = m_atoms[mi]; - while (c.i < atoms.size() && !atoms[c.i].is_var) { - expr_ref d = der_elem(c.R, atoms[c.i].elem.get()); - if (re().is_empty(d)) - return l_false; // this membership is already empty - m_pin.push_back(d); - c.R = d; - c.i += 1; - } - // prepare() guarantees every membership has a variable, so c.i now points at a - // variable head (c.complete stays false). A membership of only constants would - // have been rejected by prepare(). - c.complete = (c.i == atoms.size()); - if (c.complete) { - // Defensive: no variable head (shouldn't happen); require the tail nullable. - lbool nb = nullable(c.R); - if (nb == l_false) - return l_false; - if (nb == l_undef) - ++m_undef_vars; - } - } - return l_true; -} - -lbool seq_monadic::accept_state() { - if (m_undef_vars > 0) - return l_undef; // some group / tail nullability gave up - if (!m_config.m_model) - return l_true; // groups already shown non-empty - m_model.reset(); - for (unsigned vi = 0; vi < m_groups.size(); ++vi) { - if (m_groups[vi].empty()) - continue; - expr_ref w(m); - lbool ne = product_nonempty(m_groups[vi], &w); - if (ne != l_true) { - m_model.reset(); - return ne; - } - m_pin.push_back(w); - m_model.insert(m_vars[vi], w.get()); - } - return l_true; + return consume_constants(c, mi); } lbool seq_monadic::search() { - if (m_giveup) + if (!inc_budget()) return l_undef; - if (m_budget == 0) { - m_stats.inc_bail(bail_reason::budget); - m_giveup = true; - return l_undef; - } - if (!m.inc()) { - m_stats.inc_bail(bail_reason::resource); - m_giveup = true; - return l_undef; - } - --m_budget; - // Gather the head variables of the active cursors and how often each occurs as a head. unsigned best_vi = UINT_MAX, best_cnt = 0; - obj_map head_cnt; for (unsigned mi = 0; mi < m_cursors.size(); ++mi) { cursor const& c = m_cursors[mi]; if (c.complete) continue; - expr* v = m_atoms[mi][c.i].var.get(); - unsigned cnt = 0; - head_cnt.find(v, cnt); - head_cnt.insert(v, ++cnt); - unsigned vi = m_var_idx[v]; + unsigned vi = m_var_idx[m_atoms[mi][c.i].var.get()]; + unsigned cnt = ++m_head_cnt[vi]; // Prefer the most frequent head variable; break ties toward the smallest index so // the choice is deterministic. m_last_var (locality) is applied afterwards. - if (cnt > best_cnt || (cnt == best_cnt && (best_vi == UINT_MAX || vi < best_vi))) { + if (cnt > best_cnt || (cnt == best_cnt && vi < best_vi)) { best_cnt = cnt; best_vi = vi; } } - if (best_vi == UINT_MAX) - return accept_state(); // every cursor complete // Locality: if the last expanded variable is still an active head, expand it next -- // its freshly chosen continuation can be checked against the intersection immediately. unsigned vi = best_vi; - if (m_last_var != UINT_MAX && m_last_var < m_vars.size()) { - unsigned lc = 0; - if (head_cnt.find(m_vars[m_last_var], lc) && lc > 0) - vi = m_last_var; - } + if (best_vi != UINT_MAX && m_last_var != UINT_MAX && m_head_cnt[m_last_var] > 0) + vi = m_last_var; // All cursors whose current head is variable vi are expanded together at this step. - svector S; - expr* vv = m_vars[vi]; + unsigned s_offset = m_head_stack.size(), s_size = 0; for (unsigned mi = 0; mi < m_cursors.size(); ++mi) { cursor const& c = m_cursors[mi]; - if (!c.complete && m_atoms[mi][c.i].var.get() == vv) - S.push_back(mi); + if (c.complete) + continue; + unsigned hv = m_var_idx[m_atoms[mi][c.i].var.get()]; + m_head_cnt[hv] = 0; + if (hv == vi) { + m_head_stack.push_back(mi); + ++s_size; + } } - return choose_cont(vi, S, 0); + if (best_vi == UINT_MAX) + return leaf(); // every cursor complete + + lbool r = choose_cont(vi, s_offset, s_size, 0); + m_head_stack.shrink(s_offset); + return r; } -lbool seq_monadic::choose_cont(unsigned vi, svector const& S, unsigned k) { - if (m_giveup) +lbool seq_monadic::choose_cont(unsigned vi, unsigned s_offset, unsigned s_size, unsigned k) { + if (!inc_budget()) return l_undef; - if (k == S.size()) { + if (k == s_size) { unsigned saved = m_last_var; m_last_var = vi; lbool r = search(); m_last_var = saved; return r; } - unsigned mi = S[k]; + unsigned mi = m_head_stack[s_offset + k]; cursor& c = m_cursors[mi]; vector const& atoms = m_atoms[mi]; expr* R = c.R; - uint64_t pos = (static_cast(mi) << 32) | c.i; - uint64_t last = 0; - bool finalize = m_last_occ.find(atoms[c.i].var.get(), last) && last == pos; + expr* v = atoms[c.i].var.get(); bool last_atom = (c.i + 1 == atoms.size()); - auto explore = [&](expr* target) { - m_groups[vi].push_back(component{ atoms[c.i].var.get(), R, target }); + auto explore = [&](expr* target) -> lbool { + m_groups[vi].push_back(component{ v, R, target }); // Intersect immediately: prune as soon as vi's accumulated components are empty. - // The test is forced once the group is complete (past vi's last occurrence) so the - // accepting state does not need to re-verify; running it earlier (size > 1) prunes. + // The test is forced once the group is complete so the accepting state does not + // need to re-verify; running it earlier (size > 1) prunes. lbool ne; if (re().is_empty(R)) ne = l_false; - else if (finalize || m_groups[vi].size() > 1) + else if (group_complete(vi) || m_groups[vi].size() > 1) ne = group_nonempty(vi); else ne = l_true; @@ -920,7 +850,7 @@ lbool seq_monadic::choose_cont(unsigned vi, svector const& S, unsigned } unsigned undef_here = (ne == l_undef ? 1u : 0u) + (adv == l_undef ? 1u : 0u); m_undef_vars += undef_here; - lbool r = choose_cont(vi, S, k + 1); + lbool r = choose_cont(vi, s_offset, s_size, k + 1); m_undef_vars -= undef_here; c = saved; m_groups[vi].pop_back(); @@ -968,14 +898,18 @@ lbool seq_monadic::decide(membership_vec const& memberships) { r = l_undef; else if (!memberships.empty()) { if (m_config.m_state_search) { - // Build one cursor per membership at its regex start; initial_normalize consumes - // leading constants so every active cursor exposes a variable head. + // Build one cursor per membership at its regex start; consuming the leading + // constants leaves every active cursor on a variable head. m_cursors.reset(); - for (unsigned mi = 0; mi < m_atoms.size(); ++mi) - m_cursors.push_back(cursor{ 0, m_regexes.get(mi), false }); m_last_var = UINT_MAX; - lbool norm = initial_normalize(); - r = (norm == l_false) ? l_false : search(); + for (unsigned mi = 0; mi < m_atoms.size() && r != l_false; ++mi) { + m_cursors.push_back(cursor{ 0, m_regexes.get(mi), false }); + r = consume_constants(m_cursors.back(), mi); + if (r == l_undef) + ++m_undef_vars; + } + if (r != l_false) + r = search(); } else r = dfs_membership(0); @@ -1110,6 +1044,7 @@ std::ostream& seq_monadic::display(std::ostream& out) const { << " :mode " << mode_name(m_config.m_mode) << "\n" << " :generate-model " << (m_config.m_model ? "true" : "false") << "\n" << " :minimize-core " << (m_config.m_min_core ? "true" : "false") << "\n" + << " :state-search " << (m_config.m_state_search ? "true" : "false") << "\n" << " :last-result " << result_name(m_last_result) << "\n" << " :budget " << m_budget << "\n" << " :giveup " << (m_giveup ? "true" : "false") << "\n" @@ -1167,6 +1102,9 @@ std::ostream& seq_monadic::display(std::ostream& out) const { out << " "; display_expr(var); } + out << " )\n :variable-occurrences ("; + for (unsigned n : m_num_occ) + out << " " << n; out << " )\n :parsed-memberships ("; for (unsigned mi = 0; mi < m_atoms.size(); ++mi) { out << "\n [" << mi << "] :regex "; @@ -1211,25 +1149,14 @@ std::ostream& seq_monadic::display(std::ostream& out) const { << " :pinned-expressions " << m_pin.size() << ")\n"; out << " :statistics\n" - << " (:cofactor-calls " << m_stats.m_cofactor_calls << "\n" - << " :states " << m_stats.m_states; + << " (:cofactor-calls " << m_stats.m_cofactor_calls; for (unsigned i = 0; i < static_cast(bail_reason::num_reasons); ++i) - out << "\n :bail-" << bail_name(i) << " " << m_stats.m_bails[i]; + out << "\n :bail-" << bail_name(static_cast(i)) << " " << m_stats.m_bails[i]; return out << "))\n"; } void seq_monadic::collect_statistics(::statistics& st) const { - static char const* const bail_names[] = { - "seq monadic bail unsupported", - "seq monadic bail state cap", - "seq monadic bail dnf cap", - "seq monadic bail budget", - "seq monadic bail resource", - "seq monadic bail nullability", - "seq monadic bail guard" - }; st.update("seq monadic cofactor calls", m_stats.m_cofactor_calls); - st.update("seq monadic states", m_stats.m_states); for (unsigned i = 0; i < static_cast(bail_reason::num_reasons); ++i) - st.update(bail_names[i], m_stats.m_bails[i]); + st.update(bail_stat_name(static_cast(i)), m_stats.m_bails[i]); } diff --git a/src/ast/rewriter/seq_monadic.h b/src/ast/rewriter/seq_monadic.h index d66cefca44..28c2f3be92 100644 --- a/src/ast/rewriter/seq_monadic.h +++ b/src/ast/rewriter/seq_monadic.h @@ -91,11 +91,13 @@ class seq_monadic { config(seq::transition_mode mode) : m_mode(mode) {} }; - enum class bail_reason { unsupported, state_cap, dnf_cap, budget, resource, nullability, guard, num_reasons }; + enum class bail_reason { unsupported, state_cap, budget, resource, nullability, guard, num_reasons }; + + static char const* bail_stat_name(bail_reason reason); + static char const* bail_name(bail_reason reason); struct statistics { unsigned m_cofactor_calls = 0; - unsigned m_states = 0; unsigned m_bails[static_cast(bail_reason::num_reasons)] = {}; void inc_bail(bail_reason reason) { @@ -167,7 +169,7 @@ class seq_monadic { ptr_vector m_vars; // variables occurring in the memberships obj_map m_var_idx; // variable -> index into m_vars / m_groups vector> m_groups; // components accumulated on the current branch - obj_map m_last_occ; // variable -> last (membership, atom) position + svector m_num_occ; unsigned m_undef_vars = 0; // depth of groups whose emptiness test gave up // memo for the per-variable emptiness test, keyed by the sorted, deduplicated // (state, target) signature of the variable's component group @@ -197,6 +199,8 @@ class seq_monadic { struct cursor { unsigned i; expr* R; bool complete; }; svector m_cursors; // one cursor per membership (parallel to m_atoms) unsigned m_last_var = UINT_MAX; // index (in m_vars) of the last expanded variable + unsigned_vector m_head_cnt; + unsigned_vector m_head_stack; // Brzozowski derivative of regex `r` by the concrete element `elem`. Memoized on // (r, elem): the search revisits the same constant step on many branches. @@ -223,11 +227,13 @@ class seq_monadic { // Drop all search state accumulated by the previous decide()/solve(). void reset_search(); - // Parse every membership into atoms, register its variables and record each - // variable's last occurrence. Sets m_seq_sort/m_elem_sort. False on an + // Parse every membership into atoms, register its variables and count each + // variable's occurrences. Sets m_seq_sort/m_elem_sort. False on an // unsupported shape. bool prepare(membership_vec const& memberships); + bool group_complete(unsigned vi) const { return m_groups[vi].size() == m_num_occ[vi]; } + // Index of `v` in m_vars / m_groups, registering it on first sight. unsigned var_index(expr* v); @@ -240,9 +246,7 @@ class seq_monadic { lbool dfs_atoms(unsigned mi, unsigned i, expr* R); // ---- state-based search driver ---------------------------------------------------- - // Consume the leading constant atoms of every cursor so that each non-complete cursor - // has a variable head. l_false if some membership is already empty (unsat). - lbool initial_normalize(); + bool inc_budget(); // One search step: pick the next variable to expand (preferring the last-expanded // variable, else the one occurring most often as a head atom of the active cursors), @@ -250,12 +254,15 @@ class seq_monadic { // l_undef (gave up on a sub-branch). lbool search(); - // Expand variable `vi`, which is the head of the cursors in `S`. Assign a continuation - // (a reach target q, or the epsilon/membership encoding for a last atom) to each cursor - // in turn (k indexes S), pushing the component on m_groups[vi] and pruning as soon as - // the accumulated intersection for vi is empty. When every cursor in S is assigned, - // recurse into search(). - lbool choose_cont(unsigned vi, svector const& S, unsigned k); + // Expand variable `vi`, which is the head of the cursors in + // m_head_stack[s_offset .. s_offset + s_size). Assign a continuation (a reach target + // q, or the epsilon/membership encoding for a last atom) to each cursor in turn (k + // indexes the set), pushing the component on m_groups[vi] and pruning as soon as the + // accumulated intersection for vi is empty. When every cursor is assigned, recurse + // into search(). + lbool choose_cont(unsigned vi, unsigned s_offset, unsigned s_size, unsigned k); + + lbool consume_constants(cursor& c, unsigned mi); // Advance cursor `mi` past its head variable to continuation `target` (null = the // variable is a last atom, i.e. a plain membership component), then eagerly consume @@ -263,10 +270,6 @@ class seq_monadic { // l_undef = feasible but the tail nullability is unknown, l_true = feasible. lbool advance_cursor(cursor& c, unsigned mi, expr* target); - // Every cursor is complete: the state is accepting iff every variable intersection is - // non-empty. Extracts witnesses into m_model when model generation is enabled. - lbool accept_state(); - // Emptiness of the components accumulated for variable `vi` on the current branch, // memoized on their signature. Duplicated components are collapsed before the // product search (they constrain the variable identically). @@ -327,6 +330,9 @@ public: // returns the dependencies of all asserted memberships (no deletion-based shrinking). void set_min_core(bool b) { m_config.m_min_core = b; } + void set_state_search(bool b) { m_config.m_state_search = b; } + bool state_search() const { return m_config.m_state_search; } + void set_is_var(std::function const &is_var) { m_is_var = is_var; } diff --git a/src/test/seq_monadic.cpp b/src/test/seq_monadic.cpp index 65867ac4ad..4082854045 100644 --- a/src/test/seq_monadic.cpp +++ b/src/test/seq_monadic.cpp @@ -29,6 +29,7 @@ Author: #include #include #include +#include namespace { @@ -126,9 +127,28 @@ class seq_monadic_test { << mode_name() << " cofactor construction\n"; } + lbool run_both_drivers(char const* name, std::function const& query) { + bool saved = m_mon.state_search(); + m_mon.set_state_search(true); + lbool a = query(); + m_mon.set_state_search(false); + lbool b = query(); + m_mon.set_state_search(saved); + if (a != b && a != l_undef && b != l_undef) { + ++m_fail; + std::cout << " FAIL " << name << " drivers contradict: state=" << s(a) + << " positional=" << s(b) << "\n"; + } + else if (a != b) { + std::cout << " NOTE " << name << " state=" << s(a) + << " positional=" << s(b) << " (one gave up)\n"; + } + return a; + } + void check(char const* name, expr* term, expr* R, lbool expected) { m_mon.set_gen_model(false); // this check does not use the model - lbool got = m_mon.solve(term, R); + lbool got = run_both_drivers(name, [&]() { return m_mon.solve(term, R); }); bool ok = (got == expected); if (!ok) ++m_fail; std::cout << (ok ? " OK " : " FAIL ") << name @@ -148,7 +168,7 @@ class seq_monadic_test { m_trail.push_scope(); add_extra(term, R, ve); m_mon.set_gen_model(false); // this check does not use the model - lbool got = m_mon.check(); + lbool got = run_both_drivers(name, [&]() { return m_mon.check(); }); m_trail.pop_scope(1); bool ok = (got == expected); if (!ok) ++m_fail;