mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable
This commit is contained in:
commit
490e931f39
|
@ -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:
|
||||
|
|
|
@ -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";
|
||||
|
|
|
@ -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;
|
||||
|
|
Loading…
Reference in a new issue