address accessor inconsistencies between - and from #1506

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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:

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):

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,
 

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 {

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););
-        }
+            IF_VERBOSE(11, model_pp(verbose_stream(), *m_proto_model););
-        else {
-
         }
     }
 

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<unsigned> sbuffer;
+            unsigned_vector sbuffer;
             bv_util bv(th.m);
             rational val;
             unsigned sz;
-
+            for (source_t src : m_source) {
-            for (unsigned i = 0; i < m_source.size(); ++i) {
+                switch (src) {
-                switch (m_source[i]) {
                 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) {
+            for (source_t src : m_source) {
-                switch (m_source[i]) {
+                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) {
+        for (expr* c : concats) {
-            expr* c = concats[i], *c1;
+            expr *c1;
             TRACE("seq", tout << mk_pp(c, m) << "\n";);
             if (m_util.str.is_unit(c, c1)) {
                 if (ctx.e_internalized(c1)) {