From 6ef2557e2a96657c85dee84397e4fdfa5027fe0d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 18 Nov 2018 09:34:33 -0800 Subject: [PATCH] investigate #1946 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 4 + src/tactic/bv/bit_blaster_model_converter.cpp | 6 +- src/util/params.cpp | 101 ++++++++---------- 3 files changed, 50 insertions(+), 61 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index f68b908e2..70dcb158e 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -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()) diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp index 5474700c3..be6ea8b7a 100644 --- a/src/tactic/bv/bit_blaster_model_converter.cpp +++ b/src/tactic/bv/bit_blaster_model_converter.cpp @@ -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::iterator it = bits.begin(); - obj_hashtable::iterator end = bits.end(); - for (; it != end; ++it) { - tout << (*it)->get_name() << " "; + for (func_decl* f : bits) { + tout << f->get_name() << " "; } tout << "\n";); diff --git a/src/util/params.cpp b/src/util/params.cpp index d7e05cb00..43f53514a 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -161,19 +161,15 @@ struct param_descrs::imp { void display(std::ostream & out, unsigned indent, bool smt2_style, bool include_descr) const { svector names; - dictionary::iterator it = m_info.begin(); - dictionary::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::iterator it2 = names.begin(); - svector::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(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::iterator it = other.m_imp->m_info.begin(); - dictionary::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::iterator it = m_entries.begin(); - svector::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::const_iterator it = m_entries.begin(); - svector::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 << " " <second.m_uint_value; + out << " " <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::const_iterator it = m_entries.begin(); - svector::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 << " " <second.m_uint_value; + out << " " <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::const_iterator it = m_entries.begin(); - svector::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); }