mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 05:11:21 +00:00
Code Activity

Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2014-10-08 21:03:01 +01:00
commit ca83f47be6
3 changed files with 64 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/tactic/tactical.cpp
View file

@ -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);
}

61
src/util/params.cpp
View file

@ -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());
}
}
}
@ -351,7 +360,7 @@ public:
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();
@ -427,6 +471,13 @@ void params_ref::display(std::ostream & out) const {
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));
}

1
src/util/params.h
View file

@ -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;