fix #2650, use datatype constructor producing smallest possible tree whenever possible

NikolajBjorner · NikolajBjorner · commit 02e71c7d2362 · 2019-10-07T16:23:44.000-07:00
Signed-off-by: Nikolaj Bjorner &lt;nbjorner@microsoft.com&gt;
diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
@@ -1105,28 +1105,24 @@ namespace datatype {
     */
     func_decl * util::get_non_rec_constructor(sort * ty) {
         SASSERT(is_datatype(ty));
-        func_decl * r = nullptr;
-        if (m_datatype2nonrec_constructor.find(ty, r))
-            return r;
-        r = nullptr;
+        cnstr_depth cd;
+        if (m_datatype2nonrec_constructor.find(ty, cd))
+            return cd.first;
         ptr_vector<sort> forbidden_set;
         forbidden_set.push_back(ty);
         TRACE("util_bug", tout << "invoke get-non-rec: " << sort_ref(ty, m) << "\n";);
-        r = get_non_rec_constructor_core(ty, forbidden_set);
+        cd = get_non_rec_constructor_core(ty, forbidden_set);
         SASSERT(forbidden_set.back() == ty);
-        SASSERT(r);
-        m_asts.push_back(ty);
-        m_asts.push_back(r);
-        m_datatype2nonrec_constructor.insert(ty, r);
-        return r;
+        SASSERT(cd.first);
+        return cd.first;
     }
 
     /**
        \brief Return a constructor mk(T_1, ..., T_n) where
        each T_i is not a datatype or it is a datatype t not in forbidden_set,
        and get_non_rec_constructor_core(T_i, forbidden_set union { T_i })
     */
-    func_decl * util::get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set) {
+    util::cnstr_depth util::get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set) {
         // We must select a constructor c(T_1, ..., T_n):T such that
         //   1) T_i's are not recursive
         // If there is no such constructor, then we select one that 
@@ -1135,32 +1131,22 @@ namespace datatype {
         ptr_vector<func_decl> const& constructors = *get_datatype_constructors(ty);
         unsigned sz = constructors.size();
         array_util autil(m);
+        cnstr_depth result(nullptr, 0);
+        if (m_datatype2nonrec_constructor.find(ty, result))
+            return result;
         TRACE("util_bug", tout << "get-non-rec constructor: " << sort_ref(ty, m) << "\n";
               tout << "forbidden: ";
               for (sort* s : forbidden_set) tout << sort_ref(s, m) << " ";
               tout << "\n";
               tout << "constructors: " << sz << "\n";
               for (func_decl* f : constructors) tout << func_decl_ref(f, m) << "\n";
               );
-        // step 1)
-        unsigned start = ++m_start;
-        for (unsigned j = 0; j < sz; ++j) {        
-            func_decl * c = constructors[(j + start) % sz];
-            TRACE("util_bug", tout << "checking " << sort_ref(ty, m) << ": " << func_decl_ref(c, m) << "\n";);
-            unsigned num_args = c->get_arity();
-            unsigned i = 0;
-            for (; i < num_args && !is_datatype(autil.get_array_range_rec(c->get_domain(i))); i++);
-            if (i == num_args) {
-                TRACE("util_bug", tout << "found non-rec " << func_decl_ref(c, m) << "\n";);
-                return c;
-            }
-        }
-        // step 2)
-        for (unsigned j = 0; j < sz; ++j) {        
-            func_decl * c = constructors[(j + start) % sz];
-            TRACE("util_bug", tout << "non_rec_constructor c: " << j << " " << func_decl_ref(c, m) << "\n";);
+        unsigned min_depth = INT_MAX;
+        for (func_decl * c : constructors) {
+            TRACE("util_bug", tout << "non_rec_constructor c: " << func_decl_ref(c, m) << "\n";);
             unsigned num_args = c->get_arity();
             unsigned i = 0;
+            unsigned max_depth = 0;
             for (; i < num_args; i++) {
                 sort * T_i = autil.get_array_range_rec(c->get_domain(i));
                 TRACE("util_bug", tout << "c: " << i << " " << sort_ref(T_i, m) << "\n";);
@@ -1173,17 +1159,26 @@ namespace datatype {
                     break;
                 }
                 forbidden_set.push_back(T_i);
-                func_decl * nested_c = get_non_rec_constructor_core(T_i, forbidden_set);
+                cnstr_depth nested_c = get_non_rec_constructor_core(T_i, forbidden_set);
                 SASSERT(forbidden_set.back() == T_i);
                 forbidden_set.pop_back();
-                if (nested_c == nullptr)
+                if (nested_c.first == nullptr)
                     break;
-                TRACE("util_bug", tout << "nested_c: " << nested_c->get_name() << "\n";);
+                TRACE("util_bug", tout << "nested_c: " << nested_c.first->get_name() << "\n";);
+                max_depth = std::max(nested_c.second + 1, max_depth);
+            }
+            if (i == num_args && max_depth < min_depth) {
+                result.first = c;
+                result.second = max_depth;
+                min_depth = max_depth;
             }
-            if (i == num_args)
-                return c;
         }
-        return nullptr;
+        if (result.first) {
+            m_asts.push_back(result.first);
+            m_asts.push_back(ty);
+            m_datatype2nonrec_constructor.insert(ty, result);
+        }
+        return result;
     }
 
     unsigned util::get_constructor_idx(func_decl * f) const {
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
@@ -292,10 +292,10 @@ namespace datatype {
         ast_manager & m;
         family_id     m_family_id;
         mutable decl::plugin* m_plugin;
-
+        typedef std::pair<func_decl*, unsigned> cnstr_depth;
                 
         obj_map<sort, ptr_vector<func_decl> *>      m_datatype2constructors;
-        obj_map<sort, func_decl *>                  m_datatype2nonrec_constructor;
+        obj_map<sort, cnstr_depth>                  m_datatype2nonrec_constructor;
         obj_map<func_decl, ptr_vector<func_decl> *> m_constructor2accessors;
         obj_map<func_decl, func_decl *>             m_constructor2recognizer;
         obj_map<func_decl, func_decl *>             m_recognizer2constructor;
@@ -309,7 +309,7 @@ namespace datatype {
         unsigned                                    m_start;
         mutable ptr_vector<sort>                    m_fully_interp_trail;
         
-        func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set);
+        cnstr_depth get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set);
 
         friend class decl::plugin;
 
diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp
@@ -423,7 +423,7 @@ namespace nlsat {
             scoped_anum_vector & roots = m_tmp_values;
             roots.reset();
             m_am.isolate_roots(polynomial_ref(a->p(), m_pm), undef_var_assignment(m_assignment, a->x()), roots);
-            TRACE("nlsat",
+            TRACE("nlsat_evaluator",
                   m_solver.display(tout << (neg?"!":""), *a); tout << "\n";
                   if (roots.empty()) {
                       tout << "No roots\n";
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
@@ -826,6 +826,24 @@ namespace nlsat {
             }
             IF_VERBOSE(0, verbose_stream() << "check\n";);
             lbool r = checker.check();
+            if (r == l_true) {
+                for (bool_var b : tr) {
+                    literal lit(b, false);
+                    IF_VERBOSE(0, checker.display(verbose_stream(), lit) << " := " << checker.value(lit) << "\n");
+                    TRACE("nlsat", checker.display(tout, lit) << " := " << checker.value(lit) << "\n";);
+                }
+                for (clause* c : m_learned) {
+                    bool found = false;
+                    for (literal lit: *c) {
+                        literal tlit(tr[lit.var()], lit.sign());
+                        found |= checker.value(tlit) == l_true;
+                    }
+                    if (!found) {
+                        IF_VERBOSE(0, display(verbose_stream() << "violdated clause: ", *c) << "\n");
+                        TRACE("nlsat", display(tout << "violdated clause: ", *c) << "\n";);
+                    }
+                }
+            }
             VERIFY(r == l_false);
             for (bool_var b : tr) {
                 checker.dec_ref(b);
@@ -1738,7 +1756,7 @@ namespace nlsat {
                   tout << "new valid clause:\n";
                   display(tout, m_lazy_clause.size(), m_lazy_clause.c_ptr()) << "\n";);
 
-            if (m_check_lemmas && false) {
+            if (false && m_check_lemmas) {
                 check_lemma(m_lazy_clause.size(), m_lazy_clause.c_ptr(), true, nullptr);
             }
 
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
@@ -885,6 +885,7 @@ namespace smt {
                 unassigned_idx = idx;
             num_unassigned++;
         }
+        TRACE("datatype", tout << "propagate " << num_unassigned << " eqs: " << eqs.size() << "\n";);
         if (num_unassigned == 0) {
             // conflict
             SASSERT(!lits.empty());
@@ -938,13 +939,13 @@ namespace smt {
         enode * n             = get_enode(v);
         sort * s              = m.get_sort(n->get_owner());
         func_decl * non_rec_c = m_util.get_non_rec_constructor(s); 
-        TRACE("datatype_bug", tout << "non_rec_c: " << non_rec_c->get_name() << "\n";);
         unsigned non_rec_idx  = m_util.get_constructor_idx(non_rec_c);
         var_data * d          = m_var_data[v];
         SASSERT(d->m_constructor == nullptr);
         func_decl * r         = nullptr;
         m_stats.m_splits++;
 
+        TRACE("datatype_bug", tout << "non_rec_c: " << non_rec_c->get_name() << " #rec: " << d->m_recognizers.size() << "\n";);
 
         if (d->m_recognizers.empty()) {
             r = m_util.get_constructor_is(non_rec_c);
@@ -987,7 +988,7 @@ namespace smt {
                     return; // all recognizers are asserted to false... conflict will be detected...
             }
         }
-        SASSERT(r != 0);
+        SASSERT(r != nullptr);
         app * r_app     = m.mk_app(r, n->get_owner());
         TRACE("datatype", tout << "creating split: " << mk_pp(r_app, m) << "\n";);
         ctx.internalize(r_app, false);
