mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 02:15:19 +00:00
Code Activity

make module parameter validation and adjustment more flexible: you can use both module qualifiers and unqualified parameters from the API at local scope

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-08 16:27:40 -07:00
parent 8cf21dc242
commit f0c63e56f3
3 changed files with 57 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
scripts/mk_util.py
View file

@ -1801,7 +1801,7 @@ def def_module_params(module_name, export, params, class_name=None, description=
out.write(' {}\n')
out.write(' static void collect_param_descrs(param_descrs & d) {\n')
for param in params:
out.write(' d.insert("%s", %s, "%s", "%s");\n' % (param[0], TYPE2CPK[param[1]], param[3], pyg_default(param)))
out.write(' d.insert("%s", %s, "%s", "%s","%s");\n' % (param[0], TYPE2CPK[param[1]], param[3], pyg_default(param), module_name))
out.write(' }\n')
if export:
out.write(' /*\n')

66
src/util/params.cpp
View file

@ -51,31 +51,34 @@ struct param_descrs::imp {
param_kind m_kind;
char const * m_descr;
char const * m_default;
char const * m_module;
info(param_kind k, char const * descr, char const * def):
info(param_kind k, char const * descr, char const * def, char const* module):
m_kind(k),
m_descr(descr),
m_default(def) {
m_default(def),
m_module(module) {
}
info():
m_kind(CPK_INVALID),
m_descr(0),
m_default(0) {
m_default(0),
m_module(0) {
}
};
dictionary<info> m_info;
svector<symbol> m_names;
void insert(symbol const & name, param_kind k, char const * descr, char const * def) {
void insert(symbol const & name, param_kind k, char const * descr, char const * def, char const* module) {
SASSERT(!name.is_numerical());
info i;
if (m_info.find(name, i)) {
SASSERT(i.m_kind == k);
return;
}
m_info.insert(name, info(k, descr, def));
m_info.insert(name, info(k, descr, def, module));
m_names.push_back(name);
}
@ -94,6 +97,13 @@ struct param_descrs::imp {
return CPK_INVALID;
}
char const* get_module(symbol const& name) const {
info i;
if (m_info.find(name, i))
return i.m_module;
return 0;
}
char const * get_descr(symbol const & name) const {
info i;
if (m_info.find(name, i))
@ -162,7 +172,7 @@ struct param_descrs::imp {
dictionary<info>::iterator it = other.m_imp->m_info.begin();
dictionary<info>::iterator end = other.m_imp->m_info.end();
for (; it != end; ++it) {
insert(it->m_key, it->m_value.m_kind, it->m_value.m_descr, it->m_value.m_default);
insert(it->m_key, it->m_value.m_kind, it->m_value.m_descr, it->m_value.m_default, it->m_value.m_module);
}
}
@ -180,12 +190,12 @@ void param_descrs::copy(param_descrs & other) {
m_imp->copy(other);
}
void param_descrs::insert(symbol const & name, param_kind k, char const * descr, char const * def) {
m_imp->insert(name, k, descr, def);
void param_descrs::insert(symbol const & name, param_kind k, char const * descr, char const * def, char const* module) {
m_imp->insert(name, k, descr, def, module);
}
void param_descrs::insert(char const * name, param_kind k, char const * descr, char const * def) {
insert(symbol(name), k, descr, def);
void param_descrs::insert(char const * name, param_kind k, char const * descr, char const * def, char const* module) {
insert(symbol(name), k, descr, def, module);
}
bool param_descrs::contains(char const * name) const {
@ -236,6 +246,10 @@ symbol param_descrs::get_param_name(unsigned i) const {
return m_imp->get_param_name(i);
}
char const* param_descrs::get_module(symbol const& name) const {
return m_imp->get_module(name);
}
void param_descrs::display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const {
return m_imp->display(out, indent, smt2_style, include_descr);
}
@ -297,11 +311,35 @@ public:
void reset(symbol const & k);
void reset(char const * k);
void validate(param_descrs const & p) const {
svector<params::entry>::const_iterator it = m_entries.begin();
svector<params::entry>::const_iterator end = m_entries.end();
bool split_name(symbol const& name, symbol & prefix, symbol & suffix) {
if (name.is_numerical()) return false;
char const* str = name.bare_str();
char const* period = strchr(str,'.');
if (!period) return false;
svector<char> prefix_((unsigned)(period-str), str);
prefix_.push_back(0);
prefix = symbol(prefix_.c_ptr());
suffix = symbol(period + 1);
return true;
}
void validate(param_descrs const & p) {
svector<params::entry>::iterator it = m_entries.begin();
svector<params::entry>::iterator end = m_entries.end();
symbol suffix, prefix;
for (; it != end; ++it) {
param_kind expected = p.get_kind(it->first);
if (expected == CPK_INVALID && split_name(it->first, prefix, suffix)) {
expected = p.get_kind(suffix);
if (expected != CPK_INVALID) {
if (symbol(p.get_module(suffix)) == prefix) {
it->first = suffix;
}
else {
expected = CPK_INVALID;
}
}
}
if (expected == CPK_INVALID) {
std::stringstream strm;
strm << "unknown parameter '" << it->first.str() << "'\n";
@ -490,7 +528,7 @@ void params_ref::display(std::ostream & out, symbol const & k) const {
out << "default";
}
void params_ref::validate(param_descrs const & p) const {
void params_ref::validate(param_descrs const & p) {
if (m_params)
m_params->validate(p);
}

7
src/util/params.h
View file

@ -92,7 +92,7 @@ public:
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;
void validate(param_descrs const & p);
/*
\brief Display the value of the given parameter.
@ -115,8 +115,8 @@ public:
param_descrs();
~param_descrs();
void copy(param_descrs & other);
void insert(char const * name, param_kind k, char const * descr, char const * def = 0);
void insert(symbol const & name, param_kind k, char const * descr, char const * def = 0);
void insert(char const * name, param_kind k, char const * descr, char const * def = 0, char const* module = 0);
void insert(symbol const & name, param_kind k, char const * descr, char const * def = 0, char const* module = 0);
bool contains(char const * name) const;
bool contains(symbol const & name) const;
void erase(char const * name);
@ -130,6 +130,7 @@ public:
void display(std::ostream & out, unsigned indent = 0, bool smt2_style=false, bool include_descr=true) const;
unsigned size() const;
symbol get_param_name(unsigned idx) const;
char const * get_module(symbol const& name) const;
};
void insert_max_memory(param_descrs & r);