From c2b8f25cf922b3c5cb5c708aa393e1391461d8cf Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 23 May 2018 15:03:44 -0700 Subject: [PATCH] Switch to using solver instead of smt::kernel all around --- src/muz/spacer/spacer_context.cpp | 61 ++++++++---- src/muz/spacer/spacer_iuc_solver.h | 6 +- src/muz/spacer/spacer_manager.h | 8 +- src/muz/spacer/spacer_prop_solver.cpp | 18 ++-- src/muz/spacer/spacer_prop_solver.h | 29 +++--- src/muz/spacer/spacer_smt_context_manager.cpp | 23 +++-- src/muz/spacer/spacer_smt_context_manager.h | 7 +- src/muz/spacer/spacer_virtual_solver.cpp | 96 +++++++------------ src/muz/spacer/spacer_virtual_solver.h | 36 ++++--- 9 files changed, 146 insertions(+), 138 deletions(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index f29f73b3a..b1ab0082a 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -2289,33 +2289,56 @@ void context::reset_lemma_generalizers() // initialize global SMT parameters shared by all solvers void context::init_global_smt_params() { m.toggle_proof_mode(PGM_ENABLED); - smt_params &fparams = m_pm.fparams (); + params_ref p; if (!m_params.spacer_eq_prop ()) { - fparams.m_arith_bound_prop = BP_NONE; - fparams.m_arith_auto_config_simplex = true; - fparams.m_arith_propagate_eqs = false; - fparams.m_arith_eager_eq_axioms = false; + // arith_propagation_mode + p.set_uint("arith.propagation_mode", 0); + // fparams.m_arith_bound_prop = BP_NONE; + // NOT AVAILABLE + // fparams.m_arith_auto_config_simplex = true; + // arith_propagate_eqs + // fparams.m_arith_propagate_eqs = false; + p.set_bool("arith.propagate_eqs", false); + // NOT AVAILABLE + // fparams.m_arith_eager_eq_axioms = false; } - fparams.m_random_seed = m_params.spacer_random_seed (); + // fparams.m_random_seed = m_params.spacer_random_seed (); + p.set_uint("random_seed", m_params.spacer_random_seed()); - fparams.m_dump_benchmarks = m_params.spacer_vs_dump_benchmarks(); - fparams.m_dump_min_time = m_params.spacer_vs_dump_min_time(); - fparams.m_dump_recheck = m_params.spacer_vs_recheck(); + // fparams.m_dump_benchmarks = m_params.spacer_vs_dump_benchmarks(); + // fparams.m_dump_min_time = m_params.spacer_vs_dump_min_time(); + // fparams.m_dump_recheck = m_params.spacer_vs_recheck(); - fparams.m_mbqi = m_params.spacer_mbqi(); + // mbqi + // fparams.m_mbqi = m_params.spacer_mbqi(); + p.set_bool("mbqi", m_params.spacer_mbqi()); if (!m_params.spacer_ground_cti()) { - fparams.m_pi_use_database = true; // you don't need this - fparams.m_phase_selection = PS_CACHING_CONSERVATIVE2; - fparams.m_restart_strategy = RS_GEOMETRIC; - fparams.m_restart_factor = 1.5; - fparams.m_eliminate_bounds = true; - fparams.m_qi_quick_checker = MC_UNSAT; // - fparams.m_qi_eager_threshold = 10; - fparams.m_qi_lazy_threshold = 20; - fparams.m_ng_lift_ite = LI_FULL; // ? probably useless + // fparams.m_pi_use_database = true; // you don't need this + // phase_selection + // fparams.m_phase_selection = PS_CACHING_CONSERVATIVE2; + p.set_uint("phase_selection", 4); + // restart_strategy + // fparams.m_restart_strategy = RS_GEOMETRIC; + p.set_uint("restart_strategy", 0); + // restart factor + // fparams.m_restart_factor = 1.5; + p.set_double("restart_factor", 1.5); + // probably not needed in our use case + // fparams.m_eliminate_bounds = true; + // NONE + // fparams.m_qi_quick_checker = MC_UNSAT; // + // qi_eager_threshold + // fparams.m_qi_eager_threshold = 10; + p.set_double("qi.eager_threshold", 10.0); + // qi_lazy_threshold + // fparams.m_qi_lazy_threshold = 20; + p.set_double("qi.lazy_threshold", 20.0); + // useless + // fparams.m_ng_lift_ite = LI_FULL; } + m_pm.updt_params(p); } void context::init_lemma_generalizers() { diff --git a/src/muz/spacer/spacer_iuc_solver.h b/src/muz/spacer/spacer_iuc_solver.h index 568124629..8bb0a8605 100644 --- a/src/muz/spacer/spacer_iuc_solver.h +++ b/src/muz/spacer/spacer_iuc_solver.h @@ -106,7 +106,11 @@ public: /* solver interface */ solver* translate(ast_manager &m, params_ref const &p) override { return m_solver.translate(m, p);} - void updt_params(params_ref const &p) override { m_solver.updt_params(p);} + void updt_params(params_ref const &p) override {m_solver.updt_params(p);} + void reset_params(params_ref const &p) override {m_solver.reset_params(p);} + const params_ref &get_params() const override {return m_solver.get_params();} + void push_params() override {m_solver.push_params();} + void pop_params() override {m_solver.pop_params();} void collect_param_descrs(param_descrs &r) override { m_solver.collect_param_descrs(r);} void set_produce_models(bool f) override { m_solver.set_produce_models(f);} void assert_expr_core(expr *t) override { m_solver.assert_expr(t);} diff --git a/src/muz/spacer/spacer_manager.h b/src/muz/spacer/spacer_manager.h index 58b5aca07..471090c30 100644 --- a/src/muz/spacer/spacer_manager.h +++ b/src/muz/spacer/spacer_manager.h @@ -155,11 +155,13 @@ public: // three different solvers with three different sets of parameters // different solvers are used for different types of queries in spacer solver* mk_fresh() {return m_contexts.mk_fresh();} - smt_params& fparams() { return m_contexts.fparams(); } + void updt_params(const params_ref &p) {m_contexts.updt_params(p);} + solver* mk_fresh2() {return m_contexts2.mk_fresh();} - smt_params &fparams2() { return m_contexts2.fparams(); } + void updt_params2(const params_ref &p) {m_contexts2.updt_params(p);} + solver* mk_fresh3() {return m_contexts3.mk_fresh();} - smt_params &fparams3() {return m_contexts3.fparams();} + void updt_params3(const params_ref &p) {m_contexts3.updt_params(p);} diff --git a/src/muz/spacer/spacer_prop_solver.cpp b/src/muz/spacer/spacer_prop_solver.cpp index 1dd4515a7..a4ea79a25 100644 --- a/src/muz/spacer/spacer_prop_solver.cpp +++ b/src/muz/spacer/spacer_prop_solver.cpp @@ -56,10 +56,7 @@ prop_solver::prop_solver(spacer::manager& pm, { m_solvers[0] = pm.mk_fresh(); - m_fparams[0] = &pm.fparams(); - m_solvers[1] = pm.mk_fresh2(); - m_fparams[1] = &pm.fparams2(); m_contexts[0] = alloc(spacer::iuc_solver, *(m_solvers[0]), p.spacer_iuc(), @@ -293,8 +290,12 @@ lbool prop_solver::internal_check_assumptions( { // XXX Turn model generation if m_model != 0 SASSERT(m_ctx); - SASSERT(m_ctx_fparams); - flet _model(m_ctx_fparams->m_model, m_model != nullptr); + + params_ref p; + if (m_model != nullptr) { + p.set_bool("produce_models", true); + m_ctx->updt_params(p); + } if (m_in_level) { assert_level_atoms(m_current_level); } lbool result = maxsmt(hard_atoms, soft_atoms); @@ -333,6 +334,12 @@ lbool prop_solver::internal_check_assumptions( // manually undo proxies because maxsmt() call above manually adds proxies m_ctx->undo_proxies(*m_core); } + + if (m_model != nullptr) { + p.set_bool("produce_models", false); + m_ctx->updt_params(p); + } + return result; } @@ -350,7 +357,6 @@ lbool prop_solver::check_assumptions(const expr_ref_vector & _hard, flatten_and(hard); m_ctx = m_contexts [solver_id == 0 ? 0 : 0 /* 1 */].get(); - m_ctx_fparams = m_fparams [solver_id == 0 ? 0 : 0 /* 1 */]; // can be disabled if use_push_bg == true // solver::scoped_push _s_(*m_ctx); diff --git a/src/muz/spacer/spacer_prop_solver.h b/src/muz/spacer/spacer_prop_solver.h index d10ebcfcd..27b2fd51d 100644 --- a/src/muz/spacer/spacer_prop_solver.h +++ b/src/muz/spacer/spacer_prop_solver.h @@ -42,11 +42,9 @@ class prop_solver { private: ast_manager& m; symbol m_name; - smt_params* m_fparams[2]; solver* m_solvers[2]; scoped_ptr m_contexts[2]; iuc_solver * m_ctx; - smt_params * m_ctx_fparams; decl_vector m_level_preds; app_ref_vector m_pos_level_atoms; // atoms used to identify level app_ref_vector m_neg_level_atoms; // @@ -138,25 +136,20 @@ public: }; class scoped_weakness { - - smt_params &m_params; - bool m_arith_ignore_int; - bool m_array_weak; public: - scoped_weakness(prop_solver &ps, unsigned solver_id, unsigned weakness) : - m_params(*ps.m_fparams[solver_id == 0 ? 0 : 0 /*1*/]) { - // save current values - m_arith_ignore_int = m_params.m_arith_ignore_int; - m_array_weak = m_params.m_array_weak; + solver *sol; + scoped_weakness(prop_solver &ps, unsigned solver_id, unsigned weakness) + : sol(nullptr) { + sol = ps.m_solvers[solver_id == 0 ? 0 : 0 /* 1 */]; + if (!sol) return; + sol->push_params(); - // set values based on weakness score - m_params.m_arith_ignore_int = weakness < 1; - m_params.m_array_weak = weakness < 2; - } - ~scoped_weakness() { - m_params.m_arith_ignore_int = m_arith_ignore_int; - m_params.m_array_weak = m_array_weak; + params_ref p; + p.set_bool("arith.ignore_int", weakness < 1); + p.set_bool("array.weak", weakness < 2); + sol->updt_params(p); } + ~scoped_weakness() {if (sol) {sol->pop_params();}} }; }; } diff --git a/src/muz/spacer/spacer_smt_context_manager.cpp b/src/muz/spacer/spacer_smt_context_manager.cpp index e26381afd..78f01b6e5 100644 --- a/src/muz/spacer/spacer_smt_context_manager.cpp +++ b/src/muz/spacer/spacer_smt_context_manager.cpp @@ -24,19 +24,17 @@ Revision History: #include "smt/smt_context.h" #include "smt/params/smt_params.h" +#include "smt/smt_solver.h" #include "muz/spacer/spacer_util.h" #include "muz/spacer/spacer_smt_context_manager.h" namespace spacer { - - - smt_context_manager::smt_context_manager(ast_manager &m, unsigned max_num_contexts, const params_ref &p) : - m_fparams(p), m(m), + m_params(p), m_max_num_contexts(max_num_contexts), m_num_contexts(0) { m_stats.reset();} @@ -45,6 +43,13 @@ smt_context_manager::~smt_context_manager() { std::for_each(m_solvers.begin(), m_solvers.end(), delete_proc()); + m_solvers.reset(); + m_base_solvers.reset(); +} + +void smt_context_manager::updt_params(params_ref const &p) { + m_params.append(p); + for (auto *s : m_base_solvers) {s->updt_params(m_params);} } virtual_solver* smt_context_manager::mk_fresh() @@ -53,10 +58,14 @@ virtual_solver* smt_context_manager::mk_fresh() virtual_solver_factory *solver_factory = nullptr; if (m_max_num_contexts == 0 || m_solvers.size() < m_max_num_contexts) { - m_solvers.push_back(alloc(spacer::virtual_solver_factory, m, m_fparams)); + m_base_solvers.push_back(mk_smt_solver(m, m_params, symbol::null)); + m_solvers.push_back(alloc(spacer::virtual_solver_factory, + *m_base_solvers.back())); solver_factory = m_solvers.back(); - } else - { solver_factory = m_solvers[(m_num_contexts - 1) % m_max_num_contexts]; } + } + else { + solver_factory = m_solvers[(m_num_contexts - 1) % m_max_num_contexts]; + } return solver_factory->mk_solver(); } diff --git a/src/muz/spacer/spacer_smt_context_manager.h b/src/muz/spacer/spacer_smt_context_manager.h index 0df9bc77b..a62aba6cd 100644 --- a/src/muz/spacer/spacer_smt_context_manager.h +++ b/src/muz/spacer/spacer_smt_context_manager.h @@ -37,9 +37,10 @@ class smt_context_manager { void reset() { memset(this, 0, sizeof(*this)); } }; - smt_params m_fparams; ast_manager& m; + params_ref m_params; unsigned m_max_num_contexts; + sref_vector m_base_solvers; ptr_vector m_solvers; unsigned m_num_contexts; @@ -58,8 +59,8 @@ public: void collect_statistics(statistics& st) const; void reset_statistics(); - void updt_params(params_ref const &p) { m_fparams.updt_params(p); } - smt_params& fparams() {return m_fparams;} + void updt_params(params_ref const &p); + }; diff --git a/src/muz/spacer/spacer_virtual_solver.cpp b/src/muz/spacer/spacer_virtual_solver.cpp index 873f94160..a1a1a7eec 100644 --- a/src/muz/spacer/spacer_virtual_solver.cpp +++ b/src/muz/spacer/spacer_virtual_solver.cpp @@ -7,7 +7,7 @@ Module Name: Abstract: - multi-solver view of a single smt::kernel + multi-solver view of a single solver Author: @@ -28,13 +28,14 @@ Notes: #include "ast/scoped_proof.h" +#include "smt/smt_kernel.h" + namespace spacer { -virtual_solver::virtual_solver(virtual_solver_factory &factory, - smt::kernel &context, app* pred) : - solver_na2as(context.m()), +virtual_solver::virtual_solver(virtual_solver_factory &factory, app* pred) : + solver_na2as(factory.get_manager()), m_factory(factory), - m(context.m()), - m_context(context), + m(factory.get_manager()), + m_context(factory.get_base_solver()), m_pred(pred, m), m_virtual(!m.is_true(pred)), m_assertions(m), @@ -42,7 +43,7 @@ virtual_solver::virtual_solver(virtual_solver_factory &factory, m_flat(m), m_pushed(false), m_in_delay_scope(false), - m_dump_benchmarks(factory.fparams().m_dump_benchmarks), + m_dump_benchmarks(false /*factory.fparams().m_dump_benchmarks*/), m_dump_counter(0), m_proof(m) { @@ -114,7 +115,7 @@ lbool virtual_solver::check_sat_core(unsigned num_assumptions, out << "(exit)\n"; out.close(); } - lbool res = m_context.check(num_assumptions, assumptions); + lbool res = m_context.check_sat(num_assumptions, assumptions); sw.stop(); if (res == l_true) { m_factory.m_check_sat_watch.add(sw); @@ -125,8 +126,8 @@ lbool virtual_solver::check_sat_core(unsigned num_assumptions, } set_status(res); - if (m_dump_benchmarks && - sw.get_seconds() >= m_factory.fparams().m_dump_min_time) { + if (false /*m_dump_benchmarks && + sw.get_seconds() >= m_factory.fparams().m_dump_min_time*/) { std::stringstream file_name; file_name << "virt_solver"; if (m_virtual) { file_name << "_" << m_pred->get_decl()->get_name(); } @@ -151,13 +152,13 @@ lbool virtual_solver::check_sat_core(unsigned num_assumptions, st.display_smt2(out); - if (m_factory.fparams().m_dump_recheck) { + if (false /* m_factory.fparams().m_dump_recheck */) { scoped_no_proof _no_proof_(m); smt_params p; stopwatch sw2; smt::kernel kernel(m, p); - for (unsigned i = 0, sz = m_context.size(); i < sz; ++i) - { kernel.assert_expr(m_context.get_formula(i)); } + for (unsigned i = 0, sz = m_context.get_num_assertions(); i < sz; ++i) + { kernel.assert_expr(m_context.get_assertion(i)); } sw2.start(); kernel.check(num_assumptions, assumptions); sw2.stop(); @@ -208,10 +209,12 @@ void virtual_solver::pop_core(unsigned n) { void virtual_solver::get_unsat_core(ptr_vector &r) { - for (unsigned i = 0, sz = m_context.get_unsat_core_size(); i < sz; ++i) { - expr *core = m_context.get_unsat_core_expr(i); - if (is_aux_predicate(core)) { continue; } - r.push_back(core); + ptr_vector core; + m_context.get_unsat_core(core); + + for (unsigned i = 0, sz = core.size(); i < sz; ++i) { + if (is_aux_predicate(core.get(i))) { continue; } + r.push_back(core.get(i)); } } @@ -244,40 +247,25 @@ void virtual_solver::internalize_assertions() m_context.assert_expr(f); } } -void virtual_solver::refresh() -{ - SASSERT(!m_pushed); - m_head = 0; -} - -void virtual_solver::reset() -{ - SASSERT(!m_pushed); - m_head = 0; - m_assertions.reset(); - m_factory.refresh(); -} void virtual_solver::get_labels(svector &r) -{ - r.reset(); - buffer tmp; - m_context.get_relevant_labels(nullptr, tmp); - r.append(tmp.size(), tmp.c_ptr()); -} +{m_context.get_labels(r);} solver* virtual_solver::translate(ast_manager& m, params_ref const& p) { UNREACHABLE(); return nullptr; } -void virtual_solver::updt_params(params_ref const &p) { m_factory.updt_params(p); } -void virtual_solver::collect_param_descrs(param_descrs &r) { m_factory.collect_param_descrs(r); } -void virtual_solver::set_produce_models(bool f) { m_factory.set_produce_models(f); } -smt_params &virtual_solver::fparams() {return m_factory.fparams();} +void virtual_solver::updt_params(params_ref const &p) {m_context.updt_params(p);} +void virtual_solver::reset_params(params_ref const &p) {m_context.reset_params(p);} +const params_ref &virtual_solver::get_params() const {return m_context.get_params();} +void virtual_solver::push_params(){m_context.push_params();} +void virtual_solver::pop_params(){m_context.pop_params();} +void virtual_solver::collect_param_descrs(param_descrs &r) { m_context.collect_param_descrs(r); } +void virtual_solver::set_produce_models(bool f) { m_context.set_produce_models(f); } void virtual_solver::to_smt2_benchmark(std::ostream &out, - smt::kernel &context, + solver &context, unsigned num_assumptions, expr * const * assumptions, char const * name, @@ -288,11 +276,8 @@ void virtual_solver::to_smt2_benchmark(std::ostream &out, ast_pp_util pp(m); expr_ref_vector asserts(m); - - for (unsigned i = 0, sz = context.size(); i < sz; ++i) { - asserts.push_back(context.get_formula(i)); - pp.collect(asserts.back()); - } + context.get_assertions(asserts); + pp.collect(asserts); pp.collect(num_assumptions, assumptions); pp.display_decls(out); pp.display_asserts(out, asserts); @@ -303,11 +288,8 @@ void virtual_solver::to_smt2_benchmark(std::ostream &out, } -virtual_solver_factory::virtual_solver_factory(ast_manager &mgr, smt_params &fparams) : - m_fparams(fparams), m(mgr), m_context(m, m_fparams) -{ - m_stats.reset(); -} +virtual_solver_factory::virtual_solver_factory(solver &base) : + m(base.get_manager()), m_context(base) {m_stats.reset();} virtual_solver* virtual_solver_factory::mk_solver() { @@ -316,7 +298,7 @@ virtual_solver* virtual_solver_factory::mk_solver() app_ref pred(m); pred = m.mk_const(symbol(name.str().c_str()), m.mk_bool_sort()); SASSERT(m_context.get_scope_level() == 0); - m_solvers.push_back(alloc(virtual_solver, *this, m_context, pred)); + m_solvers.push_back(alloc(virtual_solver, *this, pred)); return m_solvers.back(); } @@ -333,7 +315,6 @@ void virtual_solver_factory::collect_statistics(statistics &st) const } void virtual_solver_factory::reset_statistics() { - m_context.reset_statistics(); m_stats.reset(); m_check_sat_watch.reset(); m_check_undef_watch.reset(); @@ -341,17 +322,10 @@ void virtual_solver_factory::reset_statistics() m_proof_watch.reset(); } -void virtual_solver_factory::refresh() -{ - m_context.reset(); - for (unsigned i = 0, e = m_solvers.size(); i < e; ++i) - { m_solvers [i]->refresh(); } -} - virtual_solver_factory::~virtual_solver_factory() { for (unsigned i = 0, e = m_solvers.size(); i < e; ++i) - { dealloc(m_solvers [i]); } + { dealloc(m_solvers[i]); } } diff --git a/src/muz/spacer/spacer_virtual_solver.h b/src/muz/spacer/spacer_virtual_solver.h index 162f56178..e5db5e396 100644 --- a/src/muz/spacer/spacer_virtual_solver.h +++ b/src/muz/spacer/spacer_virtual_solver.h @@ -7,7 +7,7 @@ Module Name: Abstract: - multi-solver view of a single smt::kernel + multi-solver view of a single solver Author: @@ -21,7 +21,6 @@ Notes: #include"ast/ast.h" #include"util/params.h" #include"solver/solver_na2as.h" -#include"smt/smt_kernel.h" #include"smt/params/smt_params.h" #include"util/stopwatch.h" namespace spacer { @@ -33,7 +32,7 @@ class virtual_solver : public solver_na2as { private: virtual_solver_factory &m_factory; ast_manager &m; - smt::kernel &m_context; + solver &m_context; app_ref m_pred; bool m_virtual; @@ -49,12 +48,12 @@ private: proof_ref m_proof; - virtual_solver(virtual_solver_factory &factory, smt::kernel &context, app* pred); + virtual_solver(virtual_solver_factory &factory, app* pred); bool is_aux_predicate(expr *p); void internalize_assertions(); void to_smt2_benchmark(std::ostream &out, - smt::kernel &context, + solver &context, unsigned num_assumptions, expr * const * assumptions, char const * name = "benchmarks", @@ -62,8 +61,6 @@ private: char const * status = "unknown", char const * attributes = ""); - void refresh(); - public: ~virtual_solver() override; unsigned get_num_assumptions() const override @@ -84,21 +81,24 @@ public: void get_model_core(model_ref &m) override {m_context.get_model(m);} proof* get_proof() override; std::string reason_unknown() const override - {return m_context.last_failure_as_string();} + {return m_context.reason_unknown();} void set_reason_unknown(char const *msg) override {m_context.set_reason_unknown(msg);} ast_manager& get_manager() const override {return m;} void get_labels(svector &r) override; void set_produce_models(bool f) override; smt_params &fparams(); - void reset(); expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); } void set_progress_callback(progress_callback *callback) override {UNREACHABLE();} solver *translate(ast_manager &m, params_ref const &p) override; void updt_params(params_ref const &p) override; + void reset_params(params_ref const& p) override; + params_ref const& get_params() const override; void collect_param_descrs(param_descrs &r) override; + void push_params() override; + void pop_params() override; protected: @@ -107,13 +107,12 @@ protected: void pop_core(unsigned n) override; }; -/// multi-solver abstraction on top of a single smt::kernel +/// multi-solver abstraction on top of a single solver class virtual_solver_factory { friend class virtual_solver; private: - smt_params &m_fparams; ast_manager &m; - smt::kernel m_context; + solver &m_context; /// solvers managed by this factory ptr_vector m_solvers; @@ -132,20 +131,17 @@ private: stopwatch m_proof_watch; - void refresh(); - - smt_params &fparams() { return m_fparams; } + solver &get_base_solver() {return m_context;} + ast_manager &get_manager() {return m;} public: - virtual_solver_factory(ast_manager &mgr, smt_params &fparams); + virtual_solver_factory(solver &base); virtual ~virtual_solver_factory(); virtual_solver* mk_solver(); void collect_statistics(statistics &st) const; void reset_statistics(); - void updt_params(params_ref const &p) { m_fparams.updt_params(p); } - void collect_param_descrs(param_descrs &r) { /* empty */ } - void set_produce_models(bool f) { m_fparams.m_model = f; } - bool get_produce_models() { return m_fparams.m_model; } + void updt_params(params_ref const &p) {m_context.updt_params(p);} + void collect_param_descrs(param_descrs &r) {m_context.collect_param_descrs(r);} }; }