From 83a7d1a658088157e2281d7ad2a55d204ce2eb01 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 30 Aug 2014 11:46:29 -0700 Subject: [PATCH] adding options to maxres for experiments, include option to pretty print module parameters in smt2 style Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 185 +++++++++++++++++++++++-------------- src/opt/maxsmt.cpp | 36 ++++++++ src/opt/maxsmt.h | 15 +++ src/opt/opt_context.cpp | 5 + src/opt/opt_params.pyg | 9 +- src/opt/wmax.cpp | 54 +---------- src/opt/wmax.h | 3 +- src/sat/sat_mus.cpp | 4 + src/sat/sat_mus.h | 3 + src/sat/sat_solver.cpp | 2 + src/smt/theory_wmaxsat.cpp | 4 + src/smt/theory_wmaxsat.h | 9 +- src/util/params.cpp | 50 +++++++++- src/util/params.h | 1 + 14 files changed, 249 insertions(+), 131 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index 0124cf6c1..d4fef002d 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -62,6 +62,7 @@ Notes: #include "inc_sat_solver.h" #include "opt_context.h" #include "pb_decl_plugin.h" +#include "opt_params.hpp" using namespace opt; @@ -85,9 +86,14 @@ private: expr_ref_vector m_trail; strategy_t m_st; rational m_max_upper; - bool m_hill_climb; - bool m_all_cores; - bool m_add_upper_bound_block; + bool m_hill_climb; // prefer large weight soft clauses for cores + bool m_add_upper_bound_block; // restrict upper bound with constraint + unsigned m_max_num_cores; // max number of cores per round. + unsigned m_max_core_size; // max core size per round. + bool m_maximize_assignment; // maximize assignment to find MCS + unsigned m_max_correction_set_size;// maximal set of correction set that is tolerated. + bool m_wmax; // Block upper bound using wmax + // this option is disabled if SAT core is used. typedef ptr_vector exprs; @@ -102,8 +108,11 @@ public: m_trail(m), m_st(st), m_hill_climb(true), - m_all_cores(false), - m_add_upper_bound_block(false) + m_add_upper_bound_block(false), + m_max_num_cores(UINT_MAX), + m_max_core_size(3), + m_maximize_assignment(false), + m_max_correction_set_size(3) { } @@ -201,14 +210,11 @@ public: return l_true; case l_true: SASSERT(cores.empty() || mcs.empty()); - for (unsigned i = 0; is_sat == l_true && i < cores.size(); ++i) { - is_sat = process_unsat(cores[i]); + for (unsigned i = 0; i < cores.size(); ++i) { + process_unsat(cores[i]); } - if (is_sat == l_true && cores.empty()) { - is_sat = process_sat(mcs); - } - if (is_sat != l_true) { - return is_sat; + if (cores.empty()) { + process_sat(mcs); } break; } @@ -233,8 +239,8 @@ public: mcs.reset(); s().get_model(mdl); update_assignment(mdl.get()); - is_sat = get_mss(cores, mss, mcs); - + is_sat = get_mss(mdl.get(), cores, mss, mcs); + switch (is_sat) { case l_undef: return l_undef; @@ -242,11 +248,8 @@ public: m_lower = m_upper; return l_true; case l_true: { - is_sat = process_sat(mcs); - if (is_sat != l_true) { - return is_sat; - } - update_mss_model(); + process_sat(mcs); + get_mss_model(); break; } } @@ -281,12 +284,15 @@ public: What are the corner cases: - suppose that cost of cores adds up to current upper bound. -> it means that each core is a unit (?) + + TBD: + - Block upper bound using wmax or pb constraint, or in case of + unweighted constraints using incremental tricks. + - Throttle when correction set gets added based on its size. + Suppose correction set is huge. Do we really need it? */ lbool mus_mss2_solver() { - // m_all_cores = true; - // m_add_upper_bound_block = true; - bool maximize_assignment = false; init(); init_local(); sls(); @@ -321,42 +327,46 @@ public: SASSERT((is_sat == l_true) == !cores.empty()); if (cores.empty()) { break; - } + } // - // There is a best model, - // retrieve it from the previous - // core calls. + // There is a best model, retrieve + // it from the previous core calls. // - update_mus_model(); + model_ref mdl; + get_mus_model(mdl); + // // Extend the current model to a (maximal) // assignment extracting the ss and cs. // ss - satisfying subset // cs - correction set (complement of ss). // - if (maximize_assignment) { + if (m_maximize_assignment && mdl.get()) { exprs ss, cs; - // TBD: current model has to evaluate all auxiliary predicates. - is_sat = get_mss(cores, ss, cs); + is_sat = get_mss(mdl.get(), cores, ss, cs); if (is_sat != l_true) return is_sat; - update_mss_model(); + get_mss_model(); } // // block the hard constraints corresponding to the cores. // block the soft constraints corresponding to the cs // obtained from the current best model. // - // TBD: model must be updated with definitions for the - // fresh variables. - // - is_sat = process_unsat(cores); - if (is_sat != l_true) return is_sat; + + // + // TBD: throttle blocking on correction sets if they are too big. + // likewise, if the cores are too big, don't block the cores. + // + + process_unsat(cores); exprs cs; get_current_correction_set(cs); - is_sat = process_sat(cs); - if (is_sat != l_true) return is_sat; + unsigned max_core = max_core_size(cores); + if (cs.size() <= std::max(max_core, m_max_correction_set_size)) { + process_sat(cs); + } } m_lower = m_upper; @@ -404,8 +414,15 @@ public: if (is_sat != l_true) { break; } + if (core.empty()) { + cores.reset(); + return l_false; + } cores.push_back(core); - if (!m_all_cores && core.size() >= 3) { + if (core.size() >= m_max_core_size) { + break; + } + if (cores.size() >= m_max_num_cores) { break; } remove_soft(core, asms); @@ -442,7 +459,6 @@ public: } void get_current_correction_set(exprs& cs) { - TRACE("opt", display_vec(tout << "old correction set: ", cs.size(), cs.c_ptr());); cs.reset(); for (unsigned i = 0; i < m_asms.size(); ++i) { if (!is_true(m_asms[i].get())) { @@ -482,13 +498,12 @@ public: return index; } - lbool process_sat(exprs const& corr_set) { + void process_sat(exprs const& corr_set) { expr_ref fml(m), tmp(m); TRACE("opt", display_vec(tout << "corr_set: ", corr_set.size(), corr_set.c_ptr());); remove_core(corr_set); rational w = split_core(corr_set); cs_max_resolve(corr_set, w); - return l_true; } lbool process_unsat() { @@ -501,19 +516,26 @@ public: return l_false; } else { - return process_unsat(cores); + process_unsat(cores); + return l_true; } } - lbool process_unsat(vector& cores) { - lbool is_sat = l_true; - for (unsigned i = 0; is_sat == l_true && i < cores.size(); ++i) { - is_sat = process_unsat(cores[i]); + unsigned max_core_size(vector const& cores) { + unsigned result = 0; + for (unsigned i = 0; i < cores.size(); ++i) { + result = std::max(cores[i].size(), result); + } + return result; + } + + void process_unsat(vector const& cores) { + for (unsigned i = 0; i < cores.size(); ++i) { + process_unsat(cores[i]); } - return is_sat; } - lbool process_unsat(exprs const& core) { + void process_unsat(exprs const& core) { expr_ref fml(m); remove_core(core); SASSERT(!core.empty()); @@ -524,31 +546,35 @@ public: s().assert_expr(fml); m_lower += w; IF_VERBOSE(1, verbose_stream() << "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";); - return l_true; } - void update_mus_model() { - if (!m_c.sat_enabled()) { - model_ref mdl; - rational w = m_mus.get_best_model(mdl); - if (mdl.get() && w < m_upper) { - update_assignment(mdl.get()); - } + void get_mus_model(model_ref& mdl) { + rational w(0); + if (m_c.sat_enabled()) { + // SAT solver core extracts some model + // during unsat core computation. + s().get_model(mdl); + } + else { + w = m_mus.get_best_model(mdl); + } + if (mdl.get() && w < m_upper) { + update_assignment(mdl.get()); } } - void update_mss_model() { + void get_mss_model() { model_ref mdl; m_mss.get_model(mdl); // last model is best way to reduce search space. update_assignment(mdl.get()); } - lbool get_mss(vector const& cores, exprs& literals, exprs& mcs) { + lbool get_mss(model* mdl, vector const& cores, exprs& literals, exprs& mcs) { literals.reset(); mcs.reset(); literals.append(m_asms.size(), m_asms.c_ptr()); set_mus(false); - lbool is_sat = m_mss(m_model.get(), cores, literals, mcs); + lbool is_sat = m_mss(mdl, cores, literals, mcs); set_mus(true); return is_sat; } @@ -735,7 +761,7 @@ public: if (is_sat != l_true) { return is_sat; } - update_mss_model(); + get_mss_model(); if (!cores.empty() && mcs.size() > cores.back().size()) { mcs.reset(); } @@ -804,16 +830,19 @@ public: IF_VERBOSE(1, verbose_stream() << "(opt.maxres [" << m_lower << ":" << m_upper << "])\n";); - if (m_add_upper_bound_block) { - pb_util u(m); - expr_ref_vector nsoft(m); - expr_ref fml(m); - for (unsigned i = 0; i < m_soft.size(); ++i) { - nsoft.push_back(m.mk_not(m_soft[i].get())); - } - fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper); - s().assert_expr(fml); - } + add_upper_bound_block(); + } + + void add_upper_bound_block() { + if (!m_add_upper_bound_block) return; + pb_util u(m); + expr_ref_vector nsoft(m); + expr_ref fml(m); + for (unsigned i = 0; i < m_soft.size(); ++i) { + nsoft.push_back(m.mk_not(m_soft[i].get())); + } + fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper); + s().assert_expr(fml); } bool is_true(expr* e) { @@ -845,6 +874,19 @@ public: m_mus.set_cancel(f); } + virtual void updt_params(params_ref& p) { + maxsmt_solver_base::updt_params(p); + opt_params _p(p); + + m_hill_climb = _p.maxres_hill_climb(); + m_add_upper_bound_block = _p.maxres_add_upper_bound_block(); + m_max_num_cores = _p.maxres_max_num_cores(); + m_max_core_size = _p.maxres_max_core_size(); + m_maximize_assignment = _p.maxres_maximize_assignment(); + m_max_correction_set_size = _p.maxres_max_correction_set_size(); + m_wmax = _p.maxres_wmax(); + } + void init_local() { m_upper.reset(); m_lower.reset(); @@ -853,6 +895,7 @@ public: add_soft(m_soft[i].get(), m_weights[i]); } m_max_upper = m_upper; + add_upper_bound_block(); } void verify_assignment() { diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp index 8c9148e17..73931a3cd 100644 --- a/src/opt/maxsmt.cpp +++ b/src/opt/maxsmt.cpp @@ -30,6 +30,7 @@ Notes: #include "ast_pp.h" #include "uint_set.h" #include "opt_context.h" +#include "theory_wmaxsat.h" namespace opt { @@ -108,6 +109,40 @@ namespace opt { return result; } + smt::theory_wmaxsat* maxsmt_solver_base::get_wmax_theory() const { + smt::theory_id th_id = m.get_family_id("weighted_maxsat"); + smt::theory* th = m_c.smt_context().get_theory(th_id); + if (th) { + return dynamic_cast(th); + } + else { + return 0; + } + } + + smt::theory_wmaxsat* maxsmt_solver_base::ensure_wmax_theory() { + smt::theory_wmaxsat* wth = get_wmax_theory(); + if (wth) { + wth->reset_local(); + } + else { + wth = alloc(smt::theory_wmaxsat, m, m_c.fm()); + m_c.smt_context().register_plugin(wth); + } + return wth; + } + + maxsmt_solver_base::scoped_ensure_theory::scoped_ensure_theory(maxsmt_solver_base& s) { + m_wth = s.ensure_wmax_theory(); + } + maxsmt_solver_base::scoped_ensure_theory::~scoped_ensure_theory() { + //m_wth->reset(); + } + smt::theory_wmaxsat& maxsmt_solver_base::scoped_ensure_theory::operator()() { return *m_wth; } + + + + maxsmt::maxsmt(context& c): m_s(c.get_solver()), m(c.get_manager()), m_c(c), m_cancel(false), m_soft_constraints(m), m_answer(m) {} @@ -160,6 +195,7 @@ namespace opt { } if (m_msolver) { + m_msolver->updt_params(m_params); is_sat = (*m_msolver)(); if (is_sat != l_false) { m_msolver->get_model(m_model); diff --git a/src/opt/maxsmt.h b/src/opt/maxsmt.h index 47b903e17..2b868408a 100644 --- a/src/opt/maxsmt.h +++ b/src/opt/maxsmt.h @@ -24,6 +24,9 @@ Notes: #include"solver.h" #include"filter_model_converter.h" #include"statistics.h" +#include"smt_context.h" +#include"smt_theory.h" +#include"theory_wmaxsat.h" namespace opt { @@ -82,6 +85,18 @@ namespace opt { expr* mk_not(expr* e); void set_mus(bool f); app* mk_fresh_bool(char const* name); + + class smt::theory_wmaxsat* get_wmax_theory() const; + smt::theory_wmaxsat* ensure_wmax_theory(); + class scoped_ensure_theory { + smt::theory_wmaxsat* m_wth; + public: + scoped_ensure_theory(maxsmt_solver_base& s); + ~scoped_ensure_theory(); + smt::theory_wmaxsat& operator()(); + }; + + protected: void enable_sls(expr_ref_vector const& soft, weights_t& ws); void set_enable_sls(bool f); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 59b0ee566..39316b772 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1157,6 +1157,11 @@ namespace opt { break; } } + + param_descrs descrs; + collect_param_descrs(descrs); + m_params.display_smt2(out, "opt", descrs); + out << "(check-sat)\n"; return out.str(); } diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg index 86c3fba11..fd291336c 100644 --- a/src/opt/opt_params.pyg +++ b/src/opt/opt_params.pyg @@ -10,7 +10,14 @@ def_module_params('opt', ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'), ('enable_sat', BOOL, False, 'enable the new SAT core for propositional constraints'), ('elim_01', BOOL, True, 'eliminate 01 variables'), - ('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)') + ('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'), + ('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'), + ('maxres.add_upper_bound_block', BOOL, False, 'restict upper bound with constraint'), + ('maxres.max_num_cores', UINT, UINT_MAX, 'maximal number of cores per round'), + ('maxres.max_core_size', UINT, 3, 'break batch of generated cores if size reaches this number'), + ('maxres.maximize_assignment', BOOL, False, 'find an MSS/MCS to improve current assignment'), + ('maxres.max_correction_set_size', UINT, 3, 'allow generating correction set constraints up to maximal size'), + ('maxres.wmax', BOOL, False, 'use weighted theory solver to constrain upper bounds') )) diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index 24f381dbd..bb6451c41 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -26,59 +26,15 @@ Notes: #include "opt_context.h" namespace opt { - class maxsmt_solver_wbase : public maxsmt_solver_base { - smt::context& ctx; - public: - maxsmt_solver_wbase(context& c, - vector const& ws, expr_ref_vector const& soft): - maxsmt_solver_base(c, ws, soft), ctx(c.smt_context()) {} - ~maxsmt_solver_wbase() {} - - class scoped_ensure_theory { - smt::theory_wmaxsat* m_wth; - public: - scoped_ensure_theory(maxsmt_solver_wbase& s) { - m_wth = s.ensure_theory(); - } - ~scoped_ensure_theory() { - m_wth->reset(); - } - smt::theory_wmaxsat& operator()() { return *m_wth; } - }; - - smt::theory_wmaxsat* ensure_theory() { - smt::theory_wmaxsat* wth = get_theory(); - if (wth) { - wth->reset(); - } - else { - wth = alloc(smt::theory_wmaxsat, m, m_c.fm()); - ctx.register_plugin(wth); - } - return wth; - } - smt::theory_wmaxsat* get_theory() const { - smt::theory_id th_id = m.get_family_id("weighted_maxsat"); - smt::theory* th = ctx.get_theory(th_id); - if (th) { - return dynamic_cast(th); - } - else { - return 0; - } - } - }; - // ---------------------------------------------------------- // weighted max-sat using a custom theory solver for max-sat. // NB. it is quite similar to pseudo-Boolean propagation. - class wmax : public maxsmt_solver_wbase { + class wmax : public maxsmt_solver_base { public: - wmax(context& c, - vector const& ws, expr_ref_vector const& soft): - maxsmt_solver_wbase(c, ws, soft) {} + wmax(context& c, weights_t& ws, expr_ref_vector const& soft): + maxsmt_solver_base(c, ws, soft) {} virtual ~wmax() {} lbool operator()() { @@ -90,7 +46,6 @@ namespace opt { for (unsigned i = 0; i < m_soft.size(); ++i) { wth().assert_weighted(m_soft[i].get(), m_weights[i]); } - solver::scoped_push _s2(s()); while (l_true == is_sat) { is_sat = s().check_sat(0,0); if (m_cancel) { @@ -122,8 +77,7 @@ namespace opt { } }; - maxsmt_solver_base* mk_wmax(context& c, - vector const& ws, expr_ref_vector const& soft) { + maxsmt_solver_base* mk_wmax(context& c, weights_t& ws, expr_ref_vector const& soft) { return alloc(wmax, c, ws, soft); } diff --git a/src/opt/wmax.h b/src/opt/wmax.h index 77be62f92..bb1be1b4e 100644 --- a/src/opt/wmax.h +++ b/src/opt/wmax.h @@ -23,8 +23,7 @@ Notes: #include "maxsmt.h" namespace opt { - maxsmt_solver_base* mk_wmax(context& c, - vector const& ws, expr_ref_vector const& soft); + maxsmt_solver_base* mk_wmax(context& c, weights_t & ws, expr_ref_vector const& soft); } #endif diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp index b6c7390e5..fd4cf0338 100644 --- a/src/sat/sat_mus.cpp +++ b/src/sat/sat_mus.cpp @@ -31,6 +31,7 @@ namespace sat { void mus::reset() { m_core.reset(); m_mus.reset(); + m_model.reset(); } void mus::set_core() { @@ -88,6 +89,9 @@ namespace sat { if (!core.empty()) { // mr(); // TBD: measure } + if (m_model.empty()) { + m_model.append(s.m_model); + } break; } case l_false: diff --git a/src/sat/sat_mus.h b/src/sat/sat_mus.h index 2f5879a0e..b68f4ee5c 100644 --- a/src/sat/sat_mus.h +++ b/src/sat/sat_mus.h @@ -24,6 +24,8 @@ namespace sat { literal_vector m_core; literal_vector m_mus; bool m_is_active; + model m_model; // model obtained during minimal unsat core + solver& s; public: @@ -31,6 +33,7 @@ namespace sat { ~mus(); lbool operator()(); bool is_active() const { return m_is_active; } + model const& get_model() const { return m_model; } private: lbool mus2(); void mr(); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 3d854522b..ad7f4ea02 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1736,6 +1736,8 @@ namespace sat { // initial experiment suggests it has no effect. m_mus(); // ignore return value on cancelation. + m_model.reset(); + m_model.append(m_mus.get_model()); } } diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp index e6f410442..17ec4ff0a 100644 --- a/src/smt/theory_wmaxsat.cpp +++ b/src/smt/theory_wmaxsat.cpp @@ -164,6 +164,10 @@ final_check_status theory_wmaxsat::final_check_eh() { void theory_wmaxsat::reset_eh() { theory::reset_eh(); + reset_local(); +} + +void theory_wmaxsat::reset_local() { m_vars.reset(); m_fmls.reset(); m_rweights.reset(); diff --git a/src/smt/theory_wmaxsat.h b/src/smt/theory_wmaxsat.h index feac6c04e..1ddb388ca 100644 --- a/src/smt/theory_wmaxsat.h +++ b/src/smt/theory_wmaxsat.h @@ -17,6 +17,9 @@ Notes: --*/ +#ifndef _THEORY_WMAXSAT_H_ +#define _THEORY_WMAXSAT_H_ + #include "smt_theory.h" #include "smt_clause.h" #include "filter_model_converter.h" @@ -84,9 +87,7 @@ namespace smt { virtual bool build_models() const { return false; } - void reset() { - reset_eh(); - } + void reset_local(); virtual void reset_eh(); virtual theory * mk_fresh(context * new_ctx) { return 0; } virtual bool internalize_atom(app * atom, bool gate_ctx) { return false; } @@ -123,3 +124,5 @@ namespace smt { }; }; + +#endif diff --git a/src/util/params.cpp b/src/util/params.cpp index 4aff0de92..7d517fb10 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -347,11 +347,11 @@ public: out << "(params"; svector::const_iterator it = m_entries.begin(); svector::const_iterator end = m_entries.end(); - for (; it != end; ++it) { - out << " " << it->first; + for (; it != end; ++it) { + out << " " << it->first; switch (it->second.m_kind) { case CPK_BOOL: - out << " " << it->second.m_bool_value; + out << " " << (it->second.m_bool_value?"true":"false"); break; case CPK_UINT: out << " " <second.m_uint_value; @@ -376,6 +376,41 @@ public: out << ")"; } + void display_smt2(std::ostream & out, char const* module, param_descrs& descrs) const { + svector::const_iterator it = m_entries.begin(); + svector::const_iterator end = m_entries.end(); + for (; it != end; ++it) { + if (!descrs.contains(it->first)) continue; + out << "(set-option :"; + out << module << "."; + out << it->first; + switch (it->second.m_kind) { + case CPK_BOOL: + out << " " << (it->second.m_bool_value?"true":"false"); + break; + case CPK_UINT: + out << " " <second.m_uint_value; + break; + case CPK_DOUBLE: + out << " " << it->second.m_double_value; + break; + case CPK_NUMERAL: + out << " " << *(it->second.m_rat_value); + break; + case CPK_SYMBOL: + out << " " << symbol::mk_symbol_from_c_ptr(it->second.m_sym_value); + break; + case CPK_STRING: + out << " " << it->second.m_str_value; + break; + default: + UNREACHABLE(); + break; + } + out << ")\n"; + } + } + void display(std::ostream & out, symbol const & k) const { svector::const_iterator it = m_entries.begin(); svector::const_iterator end = m_entries.end(); @@ -423,10 +458,17 @@ params_ref::params_ref(params_ref const & p): void params_ref::display(std::ostream & out) const { if (m_params) m_params->display(out); - else + else out << "(params)"; } +void params_ref::display_smt2(std::ostream& out, char const* module, param_descrs& descrs) const { + if (m_params) + m_params->display_smt2(out, module, descrs); + +} + + void params_ref::display(std::ostream & out, char const * k) const { display(out, symbol(k)); } diff --git a/src/util/params.h b/src/util/params.h index 15be825b0..06be486bb 100644 --- a/src/util/params.h +++ b/src/util/params.h @@ -90,6 +90,7 @@ public: void set_sym(char const * k, symbol const & v); void display(std::ostream & out) const; + void display_smt2(std::ostream& out, char const* module, param_descrs& module_desc) const; void validate(param_descrs const & p) const;