mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 19:35:50 +00:00
Code Activity

enable modular parameters from the parser

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-09 10:18:46 -07:00
parent f0c63e56f3
commit bcd2d935a9
3 changed files with 36 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/cmd_context/tactic_cmds.cpp
View file

@ -500,7 +500,7 @@ static tactic * mk_using_params(cmd_context & ctx, sexpr * n) {
symbol param_name = symbol(norm_param_name(c->get_symbol()).c_str());
c = n->get_child(i);
i++;
switch (descrs.get_kind(param_name)) {
switch (descrs.get_kind_in_module(param_name)) {
case CPK_INVALID:
throw cmd_exception("invalid using-params combinator, unknown parameter ", param_name, c->get_line(), c->get_pos());
case CPK_BOOL:

57
src/util/params.cpp
View file

@ -97,6 +97,35 @@ struct param_descrs::imp {
return CPK_INVALID;
}
bool split_name(symbol const& name, symbol & prefix, symbol & suffix) const {
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;
}
param_kind get_kind_in_module(symbol & name) const {
param_kind k = get_kind(name);
symbol prefix, suffix;
if (k == CPK_INVALID && split_name(name, prefix, suffix)) {
k = get_kind(suffix);
if (k != CPK_INVALID) {
if (symbol(get_module(suffix)) == prefix) {
name = suffix;
}
else {
k = CPK_INVALID;
}
}
}
return k;
}
char const* get_module(symbol const& name) const {
info i;
if (m_info.find(name, i))
@ -230,6 +259,10 @@ void param_descrs::erase(char const * name) {
erase(symbol(name));
}
param_kind param_descrs::get_kind_in_module(symbol & name) const {
return m_imp->get_kind_in_module(name);
}
param_kind param_descrs::get_kind(symbol const & name) const {
return m_imp->get_kind(name);
}
@ -311,35 +344,13 @@ public:
void reset(symbol const & k);
void reset(char const * k);
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;
}
}
}
param_kind expected = p.get_kind_in_module(it->first);
if (expected == CPK_INVALID) {
std::stringstream strm;
strm << "unknown parameter '" << it->first.str() << "'\n";

1
src/util/params.h
View file

@ -123,6 +123,7 @@ public:
void erase(symbol const & name);
param_kind get_kind(char const * name) const;
param_kind get_kind(symbol const & name) const;
param_kind get_kind_in_module(symbol & name) const;
char const * get_descr(char const * name) const;
char const * get_descr(symbol const & name) const;
char const * get_default(char const * name) const;