fix unsoundness in explanation handling for nested datatypes and sequences

src/ast/seq_decl_plugin.cpp

@@ -971,6 +971,22 @@ bool seq_util::str::is_len_sub(expr const* s, expr*& l, expr*& u, rational& k) c
         return false;
 }
 
+bool seq_util::str::is_concat_of_units(expr* s) const {
+    ptr_vector<expr> todo;
+    todo.push_back(s);
+    while (!todo.empty()) {
+        expr* e = todo.back();
+        todo.pop_back();
+        if (is_empty(e) || is_unit(e))
+            continue;
+        if (is_concat(e))
+            todo.append(to_app(e)->get_num_args(), to_app(e)->get_args());
+        else
+            return false;
+    }
+    return true;
+}
+
 bool seq_util::str::is_unit_string(expr const* s, expr_ref& c) const {
     zstring z;
     expr* ch = nullptr;

src/ast/seq_decl_plugin.h

@@ -375,6 +375,7 @@ public:
         bool is_to_code(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_TO_CODE); }
 
         bool is_len_sub(expr const* n, expr*& l, expr*& u, rational& k) const;
+        bool is_concat_of_units(expr* n) const;
 
         /*
         tests if s is a single character string(c) or a unit (c)

src/smt/theory_datatype.cpp

@@ -25,6 +25,7 @@ Revision History:
 #include "smt/theory_datatype.h"
 #include "smt/theory_array.h"
 #include "smt/smt_model_generator.h"
+#include <iostream>
 
 namespace smt {
     
@@ -519,9 +520,8 @@ namespace smt {
 
     void theory_datatype::explain_is_child(enode* parent, enode* child) {
         enode * parentc = oc_get_cstor(parent);        
-        if (parent != parentc) {
+        if (parent != parentc) 
             m_used_eqs.push_back(enode_pair(parent, parentc));
-        }
 
         // collect equalities on all children that may have been used.
         bool found = false;
@@ -546,11 +546,13 @@ namespace smt {
             }
             sort* se = nullptr;
             if (m_sutil.is_seq(s, se) && m_util.is_datatype(se)) {
-                for (enode* aarg : get_seq_args(arg)) {
+                enode* sibling;
+                for (enode* aarg : get_seq_args(arg, sibling)) {
                     if (aarg->get_root() == child->get_root()) {
-                        if (aarg != child) {
+                        if (aarg != child) 
                             m_used_eqs.push_back(enode_pair(aarg, child));
-                        }
+                        if (sibling != arg)
+                            m_used_eqs.push_back(enode_pair(arg, sibling));
                         found = true;
                     }
                 }
@@ -582,9 +584,11 @@ namespace smt {
 
         TRACE("datatype",
               tout << "occurs_check\n";
-              for (enode_pair const& p : m_used_eqs) {
+              for (enode_pair const& p : m_used_eqs) 
                   tout << enode_eq_pp(p, ctx);
-              });
+              for (auto const& [a,b] : m_used_eqs)
+                  tout << mk_pp(a->get_expr(), m) << " = " << mk_pp(b->get_expr(), m) << "\n";
+              );
     }
 
     // start exploring subgraph below `app`
@@ -596,9 +600,9 @@ namespace smt {
         }
         v = m_find.find(v);
         var_data * d = m_var_data[v];
-        if (!d->m_constructor) {
+
+        if (!d->m_constructor) 
             return false;
-        }
         enode * parent = d->m_constructor;
         oc_mark_on_stack(parent);
         auto process_arg = [&](enode* aarg) {
@@ -616,9 +620,8 @@ namespace smt {
         };
         
         for (enode * arg : enode::args(parent)) {
-            if (oc_cycle_free(arg)) {
+            if (oc_cycle_free(arg)) 
                 continue;
-            }
             if (oc_on_stack(arg)) {
                 // arg was explored before app, and is still on the stack: cycle
                 occurs_check_explain(parent, arg);
@@ -632,9 +635,11 @@ namespace smt {
                 oc_push_stack(arg);
             }
             else if (m_sutil.is_seq(s, se) && m_util.is_datatype(se)) {
-                for (enode* sarg : get_seq_args(arg))
+                enode* sibling;
-                    if (process_arg(sarg))
+                for (enode* sarg : get_seq_args(arg, sibling)) {
+                    if (process_arg(sarg)) 
                         return true;
+                }
             }
             else if (m_autil.is_array(s) && m_util.is_datatype(get_array_range(s))) {
                 for (enode* aarg : get_array_args(arg)) 
@@ -645,7 +650,7 @@ namespace smt {
         return false;
     }
 
-    ptr_vector<enode> const& theory_datatype::get_seq_args(enode* n) {
+    ptr_vector<enode> const& theory_datatype::get_seq_args(enode* n, enode*& sibling) {
         m_args.reset();
         m_todo.reset();
         auto add_todo = [&](enode* n) {
@@ -654,9 +659,14 @@ namespace smt {
                 m_todo.push_back(n);
             }
         };
-            
+        
-        for (enode* sib : *n)
+        for (enode* sib : *n) {
-            add_todo(sib);
+            if (m_sutil.str.is_concat_of_units(sib->get_expr())) {
+                add_todo(sib);
+                sibling = sib;
+                break;
+            }
+        }
             
         for (unsigned i = 0; i < m_todo.size(); ++i) {
             enode* n = m_todo[i];
@@ -691,7 +701,7 @@ namespace smt {
        a3 = cons(v3, a1)
     */
     bool theory_datatype::occurs_check(enode * n) {
-        TRACE("datatype", tout << "occurs check: " << enode_pp(n, ctx) << "\n";);
+        TRACE("datatype_verbose", tout << "occurs check: " << enode_pp(n, ctx) << "\n";);
         m_stats.m_occurs_check++;
 
         bool res = false;
@@ -706,7 +716,7 @@ namespace smt {
             if (oc_cycle_free(app))
                 continue;
 
-            TRACE("datatype", tout << "occurs check loop: " << enode_pp(app, ctx) << (op==ENTER?" enter":" exit")<< "\n";);
+            TRACE("datatype_verbose", tout << "occurs check loop: " << enode_pp(app, ctx) << (op==ENTER?" enter":" exit")<< "\n";);
 
             switch (op) {
             case ENTER:
@@ -830,15 +840,14 @@ namespace smt {
         SASSERT(d->m_constructor);
         func_decl * c_decl = d->m_constructor->get_decl();
         datatype_value_proc * result = alloc(datatype_value_proc, c_decl);
-        for (enode* arg : enode::args(d->m_constructor)) {
+        for (enode* arg : enode::args(d->m_constructor)) 
             result->add_dependency(arg);
-        }
         TRACE("datatype", 
               tout << pp(n, m) << "\n";
               tout << "depends on\n";
-              for (enode* arg : enode::args(d->m_constructor)) {
+              for (enode* arg : enode::args(d->m_constructor)) 
                   tout << " " << pp(arg, m) << "\n";
-              });
+              );
         return result;
     }
 
@@ -965,12 +974,11 @@ namespace smt {
             SASSERT(!lits.empty());
             region & reg = ctx.get_region();
             TRACE("datatype_conflict", tout << mk_ismt2_pp(recognizer->get_expr(), m) << "\n";
-                  for (literal l : lits) {
+                  for (literal l : lits) 
                       ctx.display_detailed_literal(tout, l) << "\n";
-                  }
+                  for (auto const& p : eqs) 
-                  for (auto const& p : eqs) {
                       tout << enode_eq_pp(p, ctx);
-                  });
+                  );
             ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), reg, lits.size(), lits.data(), eqs.size(), eqs.data())));
         }
         else if (num_unassigned == 1) {
@@ -1052,9 +1060,8 @@ namespace smt {
                         ctx.mark_as_relevant(curr);
                         return;
                     }
-                    else if (ctx.get_assignment(curr) != l_false) {
+                    else if (ctx.get_assignment(curr) != l_false) 
                         return;
-                    }
                 }
                 if (r == nullptr)
                     return; // all recognizers are asserted to false... conflict will be detected...

src/smt/theory_datatype.h

@@ -94,7 +94,7 @@ namespace smt {
         void oc_push_stack(enode * n);
         ptr_vector<enode> m_args, m_todo;
         ptr_vector<enode> const& get_array_args(enode* n);
-        ptr_vector<enode> const& get_seq_args(enode* n);
+        ptr_vector<enode> const& get_seq_args(enode* n, enode*& sibling);
 
         // class for managing state of final_check
         class final_check_st {