mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
investigate #1946
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
fb1287155e
commit
6ef2557e2a
|
@ -6164,6 +6164,10 @@ class ModelRef(Z3PPObject):
|
|||
def __deepcopy__(self):
|
||||
return self.translate(self.ctx)
|
||||
|
||||
def Model(ctx = None):
|
||||
ctx = _get_ctx(ctx)
|
||||
return ModelRef(Z3_mk_model(ctx.ref()), ctx)
|
||||
|
||||
def is_as_array(n):
|
||||
"""Return true if n is a Z3 expression of the form (_ as-array f)."""
|
||||
return isinstance(n, ExprRef) and Z3_is_as_array(n.ctx.ref(), n.as_ast())
|
||||
|
|
|
@ -72,10 +72,8 @@ struct bit_blaster_model_converter : public model_converter {
|
|||
}
|
||||
TRACE("blaster_mc",
|
||||
tout << "bits that should not be included in the model:\n";
|
||||
obj_hashtable<func_decl>::iterator it = bits.begin();
|
||||
obj_hashtable<func_decl>::iterator end = bits.end();
|
||||
for (; it != end; ++it) {
|
||||
tout << (*it)->get_name() << " ";
|
||||
for (func_decl* f : bits) {
|
||||
tout << f->get_name() << " ";
|
||||
}
|
||||
tout << "\n";);
|
||||
|
||||
|
|
|
@ -161,19 +161,15 @@ struct param_descrs::imp {
|
|||
|
||||
void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const {
|
||||
svector<symbol> names;
|
||||
dictionary<info>::iterator it = m_info.begin();
|
||||
dictionary<info>::iterator end = m_info.end();
|
||||
for (; it != end; ++it) {
|
||||
names.push_back(it->m_key);
|
||||
for (auto const& kv : m_info) {
|
||||
names.push_back(kv.m_key);
|
||||
}
|
||||
std::sort(names.begin(), names.end(), lt());
|
||||
svector<symbol>::iterator it2 = names.begin();
|
||||
svector<symbol>::iterator end2 = names.end();
|
||||
for (; it2 != end2; ++it2) {
|
||||
for (symbol const& name : names) {
|
||||
for (unsigned i = 0; i < indent; i++) out << " ";
|
||||
if (smt2_style)
|
||||
out << ':';
|
||||
char const * s = it2->bare_str();
|
||||
char const * s = name.bare_str();
|
||||
unsigned n = static_cast<unsigned>(strlen(s));
|
||||
for (unsigned i = 0; i < n; i++) {
|
||||
if (smt2_style && s[i] == '_')
|
||||
|
@ -186,7 +182,7 @@ struct param_descrs::imp {
|
|||
out << s[i];
|
||||
}
|
||||
info d;
|
||||
m_info.find(*it2, d);
|
||||
m_info.find(name, d);
|
||||
SASSERT(d.m_descr);
|
||||
out << " (" << d.m_kind << ")";
|
||||
if (include_descr)
|
||||
|
@ -198,10 +194,8 @@ struct param_descrs::imp {
|
|||
}
|
||||
|
||||
void copy(param_descrs & other) {
|
||||
dictionary<info>::iterator it = other.m_imp->m_info.begin();
|
||||
dictionary<info>::iterator end = other.m_imp->m_info.end();
|
||||
for (; it != end; ++it) {
|
||||
insert(it->m_key, it->m_value.m_kind, it->m_value.m_descr, it->m_value.m_default, it->m_value.m_module);
|
||||
for (auto const& kv : other.m_imp->m_info) {
|
||||
insert(kv.m_key, kv.m_value.m_kind, kv.m_value.m_descr, kv.m_value.m_default, kv.m_value.m_module);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -346,24 +340,22 @@ public:
|
|||
void reset(symbol const & k);
|
||||
void reset(char const * k);
|
||||
|
||||
void validate(param_descrs const & p) {
|
||||
svector<params::entry>::iterator it = m_entries.begin();
|
||||
svector<params::entry>::iterator end = m_entries.end();
|
||||
void validate(param_descrs const & p) {
|
||||
symbol suffix, prefix;
|
||||
for (; it != end; ++it) {
|
||||
param_kind expected = p.get_kind_in_module(it->first);
|
||||
for (params::entry& e : m_entries) {
|
||||
param_kind expected = p.get_kind_in_module(e.first);
|
||||
if (expected == CPK_INVALID) {
|
||||
std::stringstream strm;
|
||||
strm << "unknown parameter '" << it->first.str() << "'\n";
|
||||
strm << "unknown parameter '" << e.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 &&
|
||||
!(it->second.m_kind == CPK_UINT && expected == CPK_NUMERAL)) {
|
||||
if (e.second.m_kind != expected &&
|
||||
!(e.second.m_kind == CPK_UINT && expected == CPK_NUMERAL)) {
|
||||
std::stringstream strm;
|
||||
strm << "Parameter " << it->first.str() << " was given argument of type ";
|
||||
strm << it->second.m_kind << ", expected " << expected;
|
||||
strm << "Parameter " << e.first.str() << " was given argument of type ";
|
||||
strm << e.second.m_kind << ", expected " << expected;
|
||||
throw default_exception(strm.str());
|
||||
}
|
||||
}
|
||||
|
@ -405,28 +397,26 @@ public:
|
|||
|
||||
void display(std::ostream & out) const {
|
||||
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;
|
||||
switch (it->second.m_kind) {
|
||||
for (params::entry const& e : m_entries) {
|
||||
out << " " << e.first;
|
||||
switch (e.second.m_kind) {
|
||||
case CPK_BOOL:
|
||||
out << " " << (it->second.m_bool_value?"true":"false");
|
||||
out << " " << (e.second.m_bool_value?"true":"false");
|
||||
break;
|
||||
case CPK_UINT:
|
||||
out << " " <<it->second.m_uint_value;
|
||||
out << " " <<e.second.m_uint_value;
|
||||
break;
|
||||
case CPK_DOUBLE:
|
||||
out << " " << it->second.m_double_value;
|
||||
out << " " << e.second.m_double_value;
|
||||
break;
|
||||
case CPK_NUMERAL:
|
||||
out << " " << *(it->second.m_rat_value);
|
||||
out << " " << *(e.second.m_rat_value);
|
||||
break;
|
||||
case CPK_SYMBOL:
|
||||
out << " " << symbol::mk_symbol_from_c_ptr(it->second.m_sym_value);
|
||||
out << " " << symbol::mk_symbol_from_c_ptr(e.second.m_sym_value);
|
||||
break;
|
||||
case CPK_STRING:
|
||||
out << " " << it->second.m_str_value;
|
||||
out << " " << e.second.m_str_value;
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
|
@ -437,31 +427,29 @@ public:
|
|||
}
|
||||
|
||||
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;
|
||||
for (params::entry const& e : m_entries) {
|
||||
if (!descrs.contains(e.first)) continue;
|
||||
out << "(set-option :";
|
||||
out << module << ".";
|
||||
out << it->first;
|
||||
switch (it->second.m_kind) {
|
||||
out << e.first;
|
||||
switch (e.second.m_kind) {
|
||||
case CPK_BOOL:
|
||||
out << " " << (it->second.m_bool_value?"true":"false");
|
||||
out << " " << (e.second.m_bool_value?"true":"false");
|
||||
break;
|
||||
case CPK_UINT:
|
||||
out << " " <<it->second.m_uint_value;
|
||||
out << " " <<e.second.m_uint_value;
|
||||
break;
|
||||
case CPK_DOUBLE:
|
||||
out << " " << it->second.m_double_value;
|
||||
out << " " << e.second.m_double_value;
|
||||
break;
|
||||
case CPK_NUMERAL:
|
||||
out << " " << *(it->second.m_rat_value);
|
||||
out << " " << *(e.second.m_rat_value);
|
||||
break;
|
||||
case CPK_SYMBOL:
|
||||
out << " " << symbol::mk_symbol_from_c_ptr(it->second.m_sym_value);
|
||||
out << " " << symbol::mk_symbol_from_c_ptr(e.second.m_sym_value);
|
||||
break;
|
||||
case CPK_STRING:
|
||||
out << " " << it->second.m_str_value;
|
||||
out << " " << e.second.m_str_value;
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
|
@ -472,29 +460,27 @@ public:
|
|||
}
|
||||
|
||||
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();
|
||||
for (; it != end; ++it) {
|
||||
if (it->first != k)
|
||||
for (params::entry const& e : m_entries) {
|
||||
if (e.first != k)
|
||||
continue;
|
||||
switch (it->second.m_kind) {
|
||||
switch (e.second.m_kind) {
|
||||
case CPK_BOOL:
|
||||
out << (it->second.m_bool_value?"true":"false");
|
||||
out << (e.second.m_bool_value?"true":"false");
|
||||
return;
|
||||
case CPK_UINT:
|
||||
out << it->second.m_uint_value;
|
||||
out << e.second.m_uint_value;
|
||||
return;
|
||||
case CPK_DOUBLE:
|
||||
out << it->second.m_double_value;
|
||||
out << e.second.m_double_value;
|
||||
return;
|
||||
case CPK_NUMERAL:
|
||||
out << *(it->second.m_rat_value);
|
||||
out << *(e.second.m_rat_value);
|
||||
return;
|
||||
case CPK_SYMBOL:
|
||||
out << symbol::mk_symbol_from_c_ptr(it->second.m_sym_value);
|
||||
out << symbol::mk_symbol_from_c_ptr(e.second.m_sym_value);
|
||||
return;
|
||||
case CPK_STRING:
|
||||
out << it->second.m_str_value;
|
||||
out << e.second.m_str_value;
|
||||
return;
|
||||
default:
|
||||
out << "internal";
|
||||
|
@ -786,6 +772,7 @@ void params::del_values() {
|
|||
return false; \
|
||||
}
|
||||
|
||||
|
||||
bool params::contains(symbol const & k) const {
|
||||
CONTAINS(k);
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue