mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
add parameter validation to tactic parameters
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
4ea3ed7e27
commit
335f9a9be1
|
@ -1229,6 +1229,9 @@ class using_params_tactical : public unary_tactical {
|
|||
params_ref m_params;
|
||||
public:
|
||||
using_params_tactical(tactic * t, params_ref const & p):unary_tactical(t), m_params(p) {
|
||||
param_descrs r;
|
||||
collect_param_descrs(r);
|
||||
p.validate(r);
|
||||
t->updt_params(p);
|
||||
}
|
||||
|
||||
|
@ -1276,7 +1279,7 @@ public:
|
|||
model_converter_ref & mc,
|
||||
proof_converter_ref & pc,
|
||||
expr_dependency_ref & core) {
|
||||
if (m_p->operator()(*(in.get())).is_true())
|
||||
if (m_p->operator()(*(in.get())).is_true())
|
||||
m_t1->operator()(in, result, mc, pc, core);
|
||||
else
|
||||
m_t2->operator()(in, result, mc, pc, core);
|
||||
|
|
|
@ -302,10 +302,19 @@ public:
|
|||
svector<params::entry>::const_iterator end = m_entries.end();
|
||||
for (; it != end; ++it) {
|
||||
param_kind expected = p.get_kind(it->first);
|
||||
if (expected == CPK_INVALID)
|
||||
throw default_exception("unknown parameter '%s'", it->first.str().c_str());
|
||||
if (it->second.m_kind != expected)
|
||||
throw default_exception("parameter kind mismatch '%s'", it->first.str().c_str());
|
||||
if (expected == CPK_INVALID) {
|
||||
std::stringstream strm;
|
||||
strm << "unknown parameter '" << it->first.str() << "'\n";
|
||||
strm << "Legal parameters are:\n";
|
||||
p.display(strm, 2, false, false);
|
||||
throw default_exception(strm.str());
|
||||
}
|
||||
if (it->second.m_kind != expected) {
|
||||
std::stringstream strm;
|
||||
strm << "Parameter " << it->first.str() << " was given argument of type ";
|
||||
strm << it->second.m_kind << ", expected " << expected;
|
||||
throw default_exception(strm.str());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -347,11 +356,11 @@ public:
|
|||
out << "(params";
|
||||
svector<params::entry>::const_iterator it = m_entries.begin();
|
||||
svector<params::entry>::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 << " " <<it->second.m_uint_value;
|
||||
|
@ -376,6 +385,41 @@ public:
|
|||
out << ")";
|
||||
}
|
||||
|
||||
void display_smt2(std::ostream & out, char const* module, param_descrs& descrs) const {
|
||||
svector<params::entry>::const_iterator it = m_entries.begin();
|
||||
svector<params::entry>::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 << " " <<it->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<params::entry>::const_iterator it = m_entries.begin();
|
||||
svector<params::entry>::const_iterator end = m_entries.end();
|
||||
|
@ -423,10 +467,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));
|
||||
}
|
||||
|
|
|
@ -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;
|
||||
|
||||
|
|
Loading…
Reference in a new issue