diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index f820b184b..3f5a0fcf1 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1059,6 +1059,7 @@ extern "C" { switch(_d->get_decl_kind()) { case OP_DT_CONSTRUCTOR: return Z3_OP_DT_CONSTRUCTOR; case OP_DT_RECOGNISER: return Z3_OP_DT_RECOGNISER; + case OP_DT_IS: return Z3_OP_DT_IS; case OP_DT_ACCESSOR: return Z3_OP_DT_ACCESSOR; case OP_DT_UPDATE_FIELD: return Z3_OP_DT_UPDATE_FIELD; default: diff --git a/src/api/python/z3/z3printer.py b/src/api/python/z3/z3printer.py index aef71be2f..3a6b7269e 100644 --- a/src/api/python/z3/z3printer.py +++ b/src/api/python/z3/z3printer.py @@ -485,7 +485,9 @@ class PP: raise StopPPException() def pp(self, f, indent): - if f.is_string(): + if isinstance(f, str): + sef.pp_string(f, indent) + elif f.is_string(): self.pp_string(f, indent) elif f.is_indent(): self.pp(f.child, min(indent + f.indent, self.max_indent)) @@ -846,10 +848,17 @@ class Formatter: else: return seq1('MultiPattern', [ self.pp_expr(arg, d+1, xs) for arg in a.children() ]) + def pp_is(self, a, d, xs): + f = a.params()[0] + return self.pp_fdecl(f, a, d, xs) + def pp_map(self, a, d, xs): + f = z3.get_map_func(a) + return self.pp_fdecl(f, a, d, xs) + + def pp_fdecl(self, f, a, d, xs): r = [] sz = 0 - f = z3.get_map_func(a) r.append(to_format(f.name())) for child in a.children(): r.append(self.pp_expr(child, d+1, xs)) @@ -909,6 +918,8 @@ class Formatter: return self.pp_unary_param(a, d, xs) elif k == Z3_OP_EXTRACT: return self.pp_extract(a, d, xs) + elif k == Z3_OP_DT_IS: + return self.pp_is(a, d, xs) elif k == Z3_OP_ARRAY_MAP: return self.pp_map(a, d, xs) elif k == Z3_OP_CONST_ARRAY: @@ -963,6 +974,14 @@ class Formatter: else: return to_format(self.pp_unknown()) + def pp_decl(self, f): + k = f.kind() + if k == Z3_OP_DT_IS or k == Z3_OP_ARRAY_MAP: + g = f.params()[0] + r = [ to_format(g.name()) ] + return seq1(self.pp_name(f), r) + return self.pp_name(f) + def pp_seq_core(self, f, a, d, xs): self.visited = self.visited + 1 if d > self.max_depth or self.visited > self.max_visited: @@ -1054,7 +1073,7 @@ class Formatter: elif z3.is_sort(a): return self.pp_sort(a) elif z3.is_func_decl(a): - return self.pp_name(a) + return self.pp_decl(a) elif isinstance(a, z3.Goal) or isinstance(a, z3.AstVector): return self.pp_seq(a, 0, []) elif isinstance(a, z3.Solver): diff --git a/src/api/z3_api.h b/src/api/z3_api.h index ea0c1615f..500533e91 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -876,6 +876,8 @@ typedef enum - Z3_OP_DT_RECOGNISER: datatype recognizer. + - Z3_OP_DT_IS: datatype recognizer. + - Z3_OP_DT_ACCESSOR: datatype accessor. - Z3_OP_DT_UPDATE_FIELD: datatype field update. @@ -1220,6 +1222,7 @@ typedef enum { // Datatypes Z3_OP_DT_CONSTRUCTOR=0x800, Z3_OP_DT_RECOGNISER, + Z3_OP_DT_IS, Z3_OP_DT_ACCESSOR, Z3_OP_DT_UPDATE_FIELD, diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 44752866c..722cb22b5 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -797,6 +797,7 @@ namespace datatype { if (m_constructor2recognizer.find(con, d)) return d; sort * datatype = con->get_range(); +#if 0 def const& dd = get_def(datatype); symbol r; for (constructor const* c : dd) { @@ -811,6 +812,14 @@ namespace datatype { m_asts.push_back(d); m_constructor2recognizer.insert(con, d); return d; +#else + parameter ps[1] = { parameter(con)}; + d = m.mk_func_decl(m_family_id, OP_DT_IS, 1, ps, 1, &datatype); + m_constructor2recognizer.insert(con, d); + m_asts.push_back(d); + m_asts.push_back(con); + return d; +#endif } func_decl * util::get_recognizer_constructor(func_decl * recognizer) const { diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index dd38776bc..cccc2e7fb 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4313,9 +4313,7 @@ namespace smt { if (m_fparams.m_model_compact) m_proto_model->compress(); TRACE("mbqi_bug", tout << "after cleanup:\n"; model_pp(tout, *m_proto_model);); - } - else { - + IF_VERBOSE(11, model_pp(verbose_stream(), *m_proto_model);); } } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 42056ce5c..12764fd9d 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -2731,13 +2731,12 @@ public: bool is_string = th.m_util.is_string(m_sort); expr_ref result(th.m); if (is_string) { - svector sbuffer; + unsigned_vector sbuffer; bv_util bv(th.m); rational val; unsigned sz; - - for (unsigned i = 0; i < m_source.size(); ++i) { - switch (m_source[i]) { + for (source_t src : m_source) { + switch (src) { case unit_source: { VERIFY(bv.is_numeral(values[j++], val, sz)); sbuffer.push_back(val.get_unsigned()); @@ -2767,12 +2766,13 @@ public: break; } } + // TRACE("seq", tout << src << " " << sbuffer << "\n";); } result = th.m_util.str.mk_string(zstring(sbuffer.size(), sbuffer.c_ptr())); } else { - for (unsigned i = 0; i < m_source.size(); ++i) { - switch (m_source[i]) { + for (source_t src : m_source) { + switch (src) { case unit_source: args.push_back(th.m_util.str.mk_unit(values[j++])); break; @@ -2814,8 +2814,8 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) { seq_value_proc* sv = alloc(seq_value_proc, *this, srt); TRACE("seq", tout << mk_pp(e, m) << "\n";); - for (unsigned i = 0; i < concats.size(); ++i) { - expr* c = concats[i], *c1; + for (expr* c : concats) { + expr *c1; TRACE("seq", tout << mk_pp(c, m) << "\n";); if (m_util.str.is_unit(c, c1)) { if (ctx.e_internalized(c1)) {