From 9a681b1a37afaaceb4e3b70e94ec3c40f85a07d1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 9 Apr 2024 10:44:53 -0700 Subject: [PATCH] reorg sls Signed-off-by: Nikolaj Bjorner --- src/ast/bv_decl_plugin.h | 1 + src/ast/sls/bv_sls.cpp | 92 ++++++----------------- src/ast/sls/bv_sls.h | 2 - src/ast/sls/bv_sls_eval.cpp | 135 +++++++++++++++++++++++----------- src/ast/sls/bv_sls_eval.h | 14 ++++ src/ast/sls/bv_sls_fixed.cpp | 51 +++++++++++-- src/ast/sls/bv_sls_fixed.h | 1 + src/ast/sls/sls_valuation.cpp | 10 ++- src/ast/sls/sls_valuation.h | 4 + src/math/lp/nla_core.cpp | 22 ++++-- 10 files changed, 207 insertions(+), 125 deletions(-) diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index 137dc754f59..58445afda47 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -438,6 +438,7 @@ class bv_recognizers { MATCH_BINARY(is_bv_xor); MATCH_BINARY(is_bv_nand); MATCH_BINARY(is_bv_nor); + MATCH_BINARY(is_concat); MATCH_BINARY(is_bv_uremi); diff --git a/src/ast/sls/bv_sls.cpp b/src/ast/sls/bv_sls.cpp index f799d3cfee1..df741dac34b 100644 --- a/src/ast/sls/bv_sls.cpp +++ b/src/ast/sls/bv_sls.cpp @@ -56,18 +56,13 @@ namespace bv { } } for (auto* t : m_terms.terms()) { - if (t && !re_eval_is_correct(t)) + if (t && !m_eval.re_eval_is_correct(t)) m_repair_roots.insert(t->get_id()); } } void sls::init_repair_goal(app* t) { - if (m.is_bool(t)) - m_eval.set(t, m_eval.bval1(t)); - else if (bv.is_bv(t)) { - auto& v = m_eval.wval(t); - v.bits().copy_to(v.nw, v.eval); - } + m_eval.init_eval(t); } void sls::init_repair_candidates() { @@ -149,7 +144,7 @@ namespace bv { SASSERT(m_eval.bval0(e)); return { true, e }; } - if (!re_eval_is_correct(e)) { + if (!m_eval.re_eval_is_correct(e)) { init_repair_goal(e); return { true, e }; } @@ -162,7 +157,7 @@ namespace bv { lbool sls::search1() { // init and init_eval were invoked unsigned n = 0; - for (; n < m_config.m_max_repairs && m.inc(); ) { + for (; n < m_config.m_max_repairs && m.inc(); ++n) { auto [down, e] = next_to_repair(); if (!e) return l_true; @@ -170,10 +165,8 @@ namespace bv { IF_VERBOSE(20, trace_repair(down, e)); ++m_stats.m_moves; - if (down) { - try_repair_down(e); - ++n; - } + if (down) + try_repair_down(e); else try_repair_up(e); } @@ -219,12 +212,7 @@ namespace bv { void sls::try_repair_down(app* e) { unsigned n = e->get_num_args(); if (n == 0) { - if (m.is_bool(e)) { - m_eval.set(e, m_eval.bval1(e)); - } - else { - VERIFY(m_eval.wval(e).commit_eval()); - } + m_eval.commit_eval(e); IF_VERBOSE(3, verbose_stream() << "done\n"); for (auto p : m_terms.parents(e)) @@ -271,44 +259,24 @@ namespace bv { m_repair_roots.insert(e->get_id()); else if (!m_eval.repair_up(e)) { IF_VERBOSE(2, verbose_stream() << "repair-up "; trace_repair(true, e)); - init_repair(); + if (m_rand(10) != 0) { + m_eval.set_random(e); + + m_repair_roots.insert(e->get_id()); + } + else + init_repair(); } else { - if (!eval_is_correct(e)) { + if (!m_eval.eval_is_correct(e)) { verbose_stream() << "incorrect eval #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n"; } - SASSERT(eval_is_correct(e)); + SASSERT(m_eval.eval_is_correct(e)); for (auto p : m_terms.parents(e)) m_repair_up.insert(p->get_id()); } } - bool sls::eval_is_correct(app* e) { - if (!m_eval.can_eval1(e)) - return false; - if (m.is_bool(e)) - return m_eval.bval0(e) == m_eval.bval1(e); - if (bv.is_bv(e)) { - auto const& v = m_eval.wval(e); - return v.eval == v.bits(); - } - UNREACHABLE(); - return false; - } - - - bool sls::re_eval_is_correct(app* e) { - if (!m_eval.can_eval1(e)) - return false; - if (m.is_bool(e)) - return m_eval.bval0(e) == m_eval.bval1(e); - if (bv.is_bv(e)) { - auto const& v = m_eval.eval(e); - return v.eval == v.bits(); - } - UNREACHABLE(); - return false; - } model_ref sls::get_model() { if (m_engine_model) @@ -317,24 +285,17 @@ namespace bv { model_ref mdl = alloc(model, m); auto& terms = m_eval.sort_assertions(m_terms.assertions()); for (expr* e : terms) { - if (!re_eval_is_correct(to_app(e))) { + if (!m_eval.re_eval_is_correct(to_app(e))) { verbose_stream() << "missed evaluation #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n"; - if (bv.is_bv(e)) { - auto const& v = m_eval.wval(e); - verbose_stream() << v << "\n" << v.eval << "\n"; - } + m_eval.display_value(verbose_stream(), e) << "\n"; } if (!is_uninterp_const(e)) continue; auto f = to_app(e)->get_decl(); - if (m.is_bool(e)) - mdl->register_decl(f, m.mk_bool_val(m_eval.bval0(e))); - else if (bv.is_bv(e)) { - auto const& v = m_eval.wval(e); - rational n = v.get_value(); - mdl->register_decl(f, bv.mk_numeral(n, v.bw)); - } + auto v = m_eval.get_value(to_app(e)); + if (v) + mdl->register_decl(f, v); } terms.reset(); return mdl; @@ -350,10 +311,7 @@ namespace bv { out << "u "; if (m_repair_roots.contains(e->get_id())) out << "r "; - if (bv.is_bv(e)) - out << m_eval.wval(e); - else if (m.is_bool(e)) - out << (m_eval.bval0(e)?"T":"F"); + m_eval.display_value(out, e); out << "\n"; } terms.reset(); @@ -372,12 +330,10 @@ namespace bv { } std::ostream& sls::trace_repair(bool down, expr* e) { - verbose_stream() << (down ? "d #" : "u #") + verbose_stream() << (down ? "d #" : "u #") << e->get_id() << ": " << mk_bounded_pp(e, m, 1) << " "; - if (bv.is_bv(e)) verbose_stream() << m_eval.wval(e) << " " << (m_eval.is_fixed0(e) ? "fixed " : " "); - if (m.is_bool(e)) verbose_stream() << m_eval.bval0(e) << " "; - verbose_stream() << "\n"; + m_eval.display_value(verbose_stream(), e) << "\n"; return verbose_stream(); } diff --git a/src/ast/sls/bv_sls.h b/src/ast/sls/bv_sls.h index 01ccbc41f5d..fe31125a790 100644 --- a/src/ast/sls/bv_sls.h +++ b/src/ast/sls/bv_sls.h @@ -56,8 +56,6 @@ namespace bv { std::pair next_to_repair(); - bool eval_is_correct(app* e); - bool re_eval_is_correct(app* e); void init_repair_goal(app* e); void try_repair_down(app* e); void try_repair_up(app* e); diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp index b69cec867d0..486b3344565 100644 --- a/src/ast/sls/bv_sls_eval.cpp +++ b/src/ast/sls/bv_sls_eval.cpp @@ -914,15 +914,14 @@ namespace bv { bool sls_eval::try_repair_eq(bool is_true, bvval& a, bvval const& b) { if (is_true) { - if (m_rand() % 20 != 0) + if (m_rand(20) != 0) if (a.try_set(b.bits())) return true; - a.get_variant(m_tmp, m_rand); - return a.set_repair(random_bool(), m_tmp); + return a.set_random(m_rand); } else { - bool try_above = m_rand() % 2 == 0; + bool try_above = m_rand(2) == 0; if (try_above) { a.set_add(m_tmp, b.bits(), m_one); if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_tmp2, m_rand)) @@ -1018,17 +1017,16 @@ namespace bv { // If this fails, set a to a random value // bool sls_eval::try_repair_add(bvect const& e, bvval& a, bvval const& b) { - if (m_rand() % 20 != 0) { + if (m_rand(20) != 0) { a.set_sub(m_tmp, e, b.bits()); if (a.try_set(m_tmp)) return true; } - a.get_variant(m_tmp, m_rand); - return a.set_repair(random_bool(), m_tmp); + return a.set_random(m_rand); } bool sls_eval::try_repair_sub(bvect const& e, bvval& a, bvval & b, unsigned i) { - if (m_rand() % 20 != 0) { + if (m_rand(20) != 0) { if (i == 0) // e = a - b -> a := e + b a.set_add(m_tmp, e, b.bits()); @@ -1039,8 +1037,7 @@ namespace bv { return true; } // fall back to a random value - a.get_variant(m_tmp, m_rand); - return a.set_repair(random_bool(), m_tmp); + return a.set_random(m_rand); } /** @@ -1058,15 +1055,11 @@ namespace bv { return a.set_repair(random_bool(), m_tmp); } - if (b.is_zero()) { - a.get_variant(m_tmp, m_rand); - return a.set_repair(random_bool(), m_tmp); - } - - if (m_rand() % 20 == 0) { - a.get_variant(m_tmp, m_rand); - return a.set_repair(random_bool(), m_tmp); - } + if (b.is_zero()) + return a.set_random(m_rand); + + if (m_rand(20) == 0) + return a.set_random(m_rand); #if 0 verbose_stream() << "solve for " << e << "\n"; @@ -1096,7 +1089,7 @@ namespace bv { b.shift_right(y, parity_b); #if 0 for (unsigned i = parity_b; i < b.bw; ++i) - y.set(i, m_rand() % 2 == 0); + y.set(i, m_rand(2) == 0); #endif } @@ -1151,8 +1144,7 @@ namespace bv { if (a.set_repair(random_bool(), m_tmp)) return true; - a.get_variant(m_tmp, m_rand); - return a.set_repair(random_bool(), m_tmp); + return a.set_random(m_rand); } bool sls_eval::try_repair_bnot(bvect const& e, bvval& a) { @@ -1236,7 +1228,7 @@ namespace bv { bool sls_eval::try_repair_sle(bvval& a, bvect const& b, bvect const& p2) { bool r = false; if (b < p2) { - bool coin = m_rand() % 2 == 0; + bool coin = m_rand(2) == 0; if (coin) r = a.set_random_at_least(p2, m_tmp3, m_rand); if (!r) @@ -1268,7 +1260,7 @@ namespace bv { r = a.set_random_in_range(b, p2_1, m_tmp3, m_rand); else { // random b <= x or x < p2 - bool coin = m_rand() % 2 == 0; + bool coin = m_rand(2) == 0; if (coin) r = a.set_random_at_most(p2_1, m_tmp3, m_rand); if (!r) @@ -1657,12 +1649,9 @@ namespace bv { return a.set_repair(true, m_tmp3); } else { - if (a.is_one(e) && a.is_zero()) { - for (unsigned i = 0; i < a.nw; ++i) - m_tmp[i] = random_bits(); - a.clear_overflow_bits(m_tmp); - return b.set_repair(true, m_tmp); - } + if (a.is_one(e) && a.is_zero()) + return b.set_random(m_rand); + if (a.is_one(e)) { a.set(m_tmp, a.bits()); return b.set_repair(true, m_tmp); @@ -1858,8 +1847,7 @@ namespace bv { m_tmp.set(i, e.get(i)); b.clear_overflow_bits(m_tmp); r = b.try_set(m_tmp); - } - //verbose_stream() << e << " := " << a << " " << b << "\n"; + } return r; } @@ -1869,15 +1857,15 @@ namespace bv { // set a outside of [hi:lo] to random values with preference to 0 or 1 bits // bool sls_eval::try_repair_extract(bvect const& e, bvval& a, unsigned lo) { - if (m_rand() % m_config.m_prob_randomize_extract <= 100) { + if (m_rand(m_config.m_prob_randomize_extract) <= 100) { a.get_variant(m_tmp, m_rand); - if (0 == (m_rand() % 2)) { - auto bit = 0 == (m_rand() % 2); + if (0 == (m_rand(2))) { + auto bit = 0 == (m_rand(2)); if (!a.try_set_range(m_tmp, 0, lo, bit)) a.try_set_range(m_tmp, 0, lo, !bit); } - if (0 == (m_rand() % 2)) { - auto bit = 0 == (m_rand() % 2); + if (0 == (m_rand(2))) { + auto bit = 0 == (m_rand(2)); if (!a.try_set_range(m_tmp, lo + e.bw, a.bw, bit)) a.try_set_range(m_tmp, lo + e.bw, a.bw, !bit); } @@ -1888,10 +1876,7 @@ namespace bv { m_tmp.set(i + lo, e.get(i)); if (a.try_set(m_tmp)) return true; - a.get_variant(m_tmp, m_rand); - bool res = a.set_repair(random_bool(), m_tmp); - // verbose_stream() << "try set " << res << " " << m_tmp[0] << " " << a << "\n"; - return res; + return a.set_random(m_rand); } void sls_eval::set_div(bvect const& a, bvect const& b, unsigned bw, @@ -1945,6 +1930,66 @@ namespace bv { return *m_values[e->get_id()]; } + void sls_eval::init_eval(app* t) { + if (m.is_bool(t)) + set(t, bval1(t)); + else if (bv.is_bv(t)) { + auto& v = wval(t); + v.bits().copy_to(v.nw, v.eval); + } + } + + void sls_eval::commit_eval(app* e) { + if (m.is_bool(e)) { + set(e, bval1(e)); + } + else { + VERIFY(wval(e).commit_eval()); + } + } + + void sls_eval::set_random(app* e) { + if (bv.is_bv(e)) + eval(e).set_random(m_rand); + } + + bool sls_eval::eval_is_correct(app* e) { + if (!can_eval1(e)) + return false; + if (m.is_bool(e)) + return bval0(e) == bval1(e); + if (bv.is_bv(e)) { + auto const& v = wval(e); + return v.eval == v.bits(); + } + UNREACHABLE(); + return false; + } + + bool sls_eval::re_eval_is_correct(app* e) { + if (!can_eval1(e)) + return false; + if (m.is_bool(e)) + return bval0(e) ==bval1(e); + if (bv.is_bv(e)) { + auto const& v = eval(e); + return v.eval == v.bits(); + } + UNREACHABLE(); + return false; + } + + expr_ref sls_eval::get_value(app* e) { + if (m.is_bool(e)) + return expr_ref(m.mk_bool_val(bval0(e)), m); + else if (bv.is_bv(e)) { + auto const& v = wval(e); + rational n = v.get_value(); + return expr_ref(bv.mk_numeral(n, v.bw), m); + } + return expr_ref(m); + } + std::ostream& sls_eval::display(std::ostream& out, expr_ref_vector const& es) { auto& terms = sort_assertions(es); for (expr* e : terms) { @@ -1960,4 +2005,12 @@ namespace bv { terms.reset(); return out; } + + std::ostream& sls_eval::display_value(std::ostream& out, expr* e) { + if (bv.is_bv(e)) + return out << wval(e); + if (m.is_bool(e)) + return out << (bval0(e)?"T":"F"); + return out << "?"; + } } diff --git a/src/ast/sls/bv_sls_eval.h b/src/ast/sls/bv_sls_eval.h index ebd36048184..89cd3f4cf03 100644 --- a/src/ast/sls/bv_sls_eval.h +++ b/src/ast/sls/bv_sls_eval.h @@ -157,6 +157,18 @@ namespace bv { sls_valuation& eval(app* e) const; + void commit_eval(app* e); + + void init_eval(app* e); + + void set_random(app* e); + + bool eval_is_correct(app* e); + + bool re_eval_is_correct(app* e); + + expr_ref get_value(app* e); + /** * Override evaluaton. */ @@ -178,5 +190,7 @@ namespace bv { std::ostream& display(std::ostream& out, expr_ref_vector const& es); + + std::ostream& display_value(std::ostream& out, expr* e); }; } diff --git a/src/ast/sls/bv_sls_fixed.cpp b/src/ast/sls/bv_sls_fixed.cpp index 18518ed09bd..be587a8bda9 100644 --- a/src/ast/sls/bv_sls_fixed.cpp +++ b/src/ast/sls/bv_sls_fixed.cpp @@ -38,8 +38,8 @@ namespace bv { else ; } - ev.m_todo.reset(); init_ranges(es); + ev.m_todo.reset(); } @@ -49,6 +49,44 @@ namespace bv { if (is_app(e)) init_range(to_app(e), sign); } + + for (expr* e : ev.m_todo) + propagate_range_up(e); + } + + void sls_fixed::propagate_range_up(expr* e) { + expr* t, * s; + rational v; + if (bv.is_concat(e, t, s)) { + auto& val = wval(s); + if (val.lo() != val.hi() && (val.lo() < val.hi() || val.hi() == 0)) + // lo <= e + add_range(e, val.lo(), rational::zero(), false); + auto valt = wval(t); +#if 0 + if (val.lo() < val.hi()) + // e < (2^|s|) * hi + add_range(e, rational::zero(), val.hi() * rational::power_of_two(bv.get_bv_size(s)), false); +#endif + } + else if (bv.is_bv_add(e, s, t) && bv.is_numeral(s, v)) { + auto& val = wval(t); + if (val.lo() != val.hi()) + add_range(e, v + val.lo(), v + val.hi(), false); + } + else if (bv.is_bv_add(e, t, s) && bv.is_numeral(s, v)) { + auto& val = wval(t); + if (val.lo() != val.hi()) + add_range(e, v + val.lo(), v + val.hi(), false); + } + // x in [1, 4[ => -x in [-3, 0[ + // x in [lo, hi[ => -x in [-hi + 1, -lo + 1[ + else if (bv.is_bv_mul(e, s, t) && bv.is_numeral(s, v) && + v + 1 == rational::power_of_two(bv.get_bv_size(e))) { + auto& val = wval(t); + if (val.lo() != val.hi()) + add_range(e, -val.hi() + 1, - val.lo() + 1, false); + } } // s <=s t <=> s + K <= t + K, K = 2^{bw-1} @@ -117,6 +155,7 @@ namespace bv { val.tighten_range(); return true; } + return false; } @@ -138,9 +177,8 @@ namespace bv { init_eq(s, b, false); return true; } - if (!sign && bv.is_concat(t) && to_app(t)->get_num_args() == 2) { - auto x = to_app(t)->get_arg(0); - auto y = to_app(t)->get_arg(1); + expr* x, * y; + if (!sign && bv.is_concat(t, x, y)) { auto sz = bv.get_bv_size(y); auto k = rational::power_of_two(sz); init_eq(y, mod(a, k), false); @@ -206,9 +244,8 @@ namespace bv { if (sign) std::swap(lo, hi); v.add_range(lo, hi); - if (v.lo() == 0 && bv.is_concat(e) && to_app(e)->get_num_args() == 2) { - auto x = to_app(e)->get_arg(0); - auto y = to_app(e)->get_arg(1); + expr* x, * y; + if (v.lo() == 0 && bv.is_concat(e, x, y)) { auto sz = bv.get_bv_size(y); auto k = rational::power_of_two(sz); lo = v.lo(); diff --git a/src/ast/sls/bv_sls_fixed.h b/src/ast/sls/bv_sls_fixed.h index 73dd5a52c33..2e88484c55d 100644 --- a/src/ast/sls/bv_sls_fixed.h +++ b/src/ast/sls/bv_sls_fixed.h @@ -31,6 +31,7 @@ namespace bv { void init_ranges(expr_ref_vector const& es); bool init_range(app* e, bool sign); + void propagate_range_up(expr* e); bool init_range(expr* x, rational const& a, expr* y, rational const& b, bool sign); void get_offset(expr* e, expr*& x, rational& offset); bool init_eq(expr* e, rational const& v, bool sign); diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp index 1f3674e9329..68143e7b75a 100644 --- a/src/ast/sls/sls_valuation.cpp +++ b/src/ast/sls/sls_valuation.cpp @@ -153,6 +153,7 @@ namespace bv { m_lo.set_bw(bw); m_hi.set_bw(bw); m_bits.set_bw(bw); + m_tmp.set_bw(bw); fixed.set_bw(bw); eval.set_bw(bw); // have lo, hi bits, fixed point to memory allocated within this of size num_bytes each allocated @@ -440,6 +441,11 @@ namespace bv { clear_overflow_bits(dst); } + bool sls_valuation::set_random(random_gen& r) { + get_variant(m_tmp, r); + return set_repair(r(2) == 0, m_tmp); + } + void sls_valuation::repair_sign_bits(bvect& dst) const { if (m_signed_prefix == 0) return; @@ -489,7 +495,7 @@ namespace bv { } void sls_valuation::add_range(rational l, rational h) { - return; + //return; //verbose_stream() << *this << " " << l << " " << h << " --> \n"; l = mod(l, rational::power_of_two(bw)); @@ -622,7 +628,7 @@ namespace bv { inf_feasible(m_lo); - bvect hi1(nw); + bvect& hi1 = m_tmp; hi1.set_bw(bw); m_hi.copy_to(nw, hi1); sub1(hi1); diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h index 04efec24a5c..e4828302e0d 100644 --- a/src/ast/sls/sls_valuation.h +++ b/src/ast/sls/sls_valuation.h @@ -110,6 +110,7 @@ namespace bv { protected: bvect m_bits; bvect m_lo, m_hi; // range assignment to bit-vector, as wrap-around interval + bvect m_tmp; unsigned m_signed_prefix = 0; unsigned mask; @@ -123,6 +124,7 @@ namespace bv { bvect fixed; // bit assignment and don't care bit bvect eval; // current evaluation + sls_valuation(unsigned bw); void set_bw(unsigned bw); @@ -231,12 +233,14 @@ namespace bv { bool set_repair(bool try_down, bvect& dst); void set_random_above(bvect& dst, random_gen& r); void set_random_below(bvect& dst, random_gen& r); + bool set_random(random_gen& r); void round_down(bvect& dst, std::function const& is_feasible); void round_up(bvect& dst, std::function const& is_feasible); static digit_t random_bits(random_gen& r); void get_variant(bvect& dst, random_gen& r) const; + bool try_set(bvect const& src) { if (!can_set(src)) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 675bf502231..44f56efcd77 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1062,6 +1062,8 @@ new_lemma::~new_lemma() { if (current().is_conflict()) { c.m_conflicts++; } + IF_VERBOSE(4, verbose_stream() << name << "\n"); + IF_VERBOSE(4, verbose_stream() << *this << "\n"); TRACE("nla_solver", tout << name << " " << (++i) << "\n" << *this; ); } @@ -1519,6 +1521,12 @@ lbool core::check() { if (!m_lemmas.empty() || !m_literals.empty() || m_check_feasible) return l_false; } + + if (no_effect() && params().arith_nl_nra()) { + ret = m_nra.check(); + lp_settings().stats().m_nra_calls++; + } + if (no_effect() && should_run_bounded_nlsat()) ret = bounded_nlsat(); @@ -1530,12 +1538,16 @@ lbool core::check() { m_basics.basic_lemma(false); if (no_effect()) - m_divisions.check(); + m_divisions.check(); + - if (no_effect()) { - std::function check1 = [&]() { m_order.order_lemma(); }; - std::function check2 = [&]() { m_monotone.monotonicity_lemma(); }; - std::function check3 = [&]() { m_tangents.tangent_lemma(); }; + if (false && no_effect()) { + std::function check1 = [&]() { m_order.order_lemma(); + }; + std::function check2 = [&]() { m_monotone.monotonicity_lemma(); + }; + std::function check3 = [&]() { m_tangents.tangent_lemma(); + }; std::pair> checks[] = { { 6, check1 },