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

add more information to error messages

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-15 21:33:29 -07:00
parent 630a3d6ea8
commit 9d75babcda
4 changed files with 31 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/api/api_config_params.cpp
View file

@ -37,9 +37,7 @@ extern "C" {
catch (z3_exception & ex) { catch (z3_exception & ex) {
// The error handler is only available for contexts // The error handler is only available for contexts
// Just throw a warning. // Just throw a warning.
std::ostringstream buffer; warning_msg(ex.msg());
buffer << "Error setting " << param_id << ", " << ex.msg();
warning_msg(buffer.str().c_str());
} }
} }
@ -64,9 +62,7 @@ extern "C" {
catch (z3_exception & ex) { catch (z3_exception & ex) {
// The error handler is only available for contexts // The error handler is only available for contexts
// Just throw a warning. // Just throw a warning.
std::ostringstream buffer; warning_msg(ex.msg());
buffer << "Error setting " << param_id << ": " << ex.msg();
warning_msg(buffer.str().c_str());
return Z3_FALSE; return Z3_FALSE;
} }
} }
@ -92,9 +88,7 @@ extern "C" {
catch (z3_exception & ex) { catch (z3_exception & ex) {
// The error handler is only available for contexts // The error handler is only available for contexts
// Just throw a warning. // Just throw a warning.
std::ostringstream buffer; warning_msg(ex.msg());
buffer << "Error setting " << param_id << ": " << ex.msg();
warning_msg(buffer.str().c_str());
} }
} }

8
src/cmd_context/context_params.cpp
View file

@ -86,7 +86,13 @@ void context_params::set(char const * param, char const * value) {
set_bool(m_smtlib2_compliant, param, value); set_bool(m_smtlib2_compliant, param, value);
} }
else { else {
throw default_exception("unknown parameter '%s'", p.c_str()); param_descrs d;
collect_param_descrs(d);
std::stringstream strm;
strm << "unknown parameter '" << p << "'\n";
strm << "Legal parameters are:\n";
d.display(strm, 2, false, false);
throw default_exception(strm.str());
} }
} }

6
src/smt/theory_arith_core.h
View file

@ -3225,11 +3225,13 @@ namespace smt {
case QUASI_BASE: case QUASI_BASE:
SASSERT(m_columns[v].size() == 1); SASSERT(m_columns[v].size() == 1);
del_row(get_var_row(v)); del_row(get_var_row(v));
TRACE("arith_make_feasible", tout << "del row v" << v << "\n";);
break; break;
case BASE: case BASE:
SASSERT(lazy_pivoting_lvl() != 0 || m_columns[v].size() == 1); SASSERT(lazy_pivoting_lvl() != 0 || m_columns[v].size() == 1);
if (lazy_pivoting_lvl() > 0) if (lazy_pivoting_lvl() > 0)
eliminate<false>(v, false); eliminate<false>(v, false);
TRACE("arith_make_feasible", tout << "del row v" << v << "\n";);
del_row(get_var_row(v)); del_row(get_var_row(v));
break; break;
case NON_BASE: { case NON_BASE: {
@ -3241,6 +3243,10 @@ namespace smt {
pivot<false>(r.get_base_var(), v, r[entry->m_row_idx].m_coeff, false); pivot<false>(r.get_base_var(), v, r[entry->m_row_idx].m_coeff, false);
SASSERT(is_base(v)); SASSERT(is_base(v));
del_row(get_var_row(v)); del_row(get_var_row(v));
TRACE("arith_make_feasible", tout << "del row v" << v << "\n";);
}
else {
TRACE("arith_make_feasible", tout << "no row v" << v << "\n";);
} }
break; break;
} } } }

21
src/util/gparams.cpp
View file

@ -201,7 +201,7 @@ public:
} }
} }
void throw_unknown_parameter(symbol const & param_name, symbol const & mod_name) { void throw_unknown_parameter(symbol const & param_name, param_descrs const& d, symbol const & mod_name) {
if (mod_name == symbol::null) { if (mod_name == symbol::null) {
char const * new_name = get_new_param_name(param_name); char const * new_name = get_new_param_name(param_name);
if (new_name) { if (new_name) {
@ -213,11 +213,20 @@ public:
param_name.bare_str()); param_name.bare_str());
} }
else { else {
throw exception("unknown parameter '%s'", param_name.bare_str()); std::stringstream strm;
strm << "unknown parameter '" << param_name << "'\n";
strm << "Legal parameters are:\n";
d.display(strm, 2, false, false);
throw default_exception(strm.str());
} }
} }
else { else {
throw exception("unknown parameter '%s' at module '%s'", param_name.bare_str(), mod_name.bare_str()); std::stringstream strm;
strm << "unknown parameter '" << param_name << "' ";
strm << "at module '" << mod_name << "'\n";
strm << "Legal parameters are:\n";
d.display(strm, 2, false, false);
throw default_exception(strm.str());
} }
} }
@ -225,7 +234,7 @@ public:
param_kind k = d.get_kind(param_name); param_kind k = d.get_kind(param_name);
params_ref & ps = get_params(mod_name); params_ref & ps = get_params(mod_name);
if (k == CPK_INVALID) { if (k == CPK_INVALID) {
throw_unknown_parameter(param_name, mod_name); throw_unknown_parameter(param_name, d, mod_name);
} }
else if (k == CPK_UINT) { else if (k == CPK_UINT) {
long val = strtol(value, 0, 10); long val = strtol(value, 0, 10);
@ -312,7 +321,7 @@ public:
std::string get_default(param_descrs const & d, symbol const & p, symbol const & m) { std::string get_default(param_descrs const & d, symbol const & p, symbol const & m) {
if (!d.contains(p)) { if (!d.contains(p)) {
throw_unknown_parameter(p, m); throw_unknown_parameter(p, d, m);
} }
char const * r = d.get_default(p); char const * r = d.get_default(p);
if (r == 0) if (r == 0)
@ -478,7 +487,7 @@ public:
throw exception("unknown module '%s'", m.bare_str()); throw exception("unknown module '%s'", m.bare_str());
} }
if (!d->contains(p)) if (!d->contains(p))
throw_unknown_parameter(p, m); throw_unknown_parameter(p, *d, m);
out << " name: " << p << "\n"; out << " name: " << p << "\n";
if (m != symbol::null) { if (m != symbol::null) {
out << " module: " << m << "\n"; out << " module: " << m << "\n";