fix #6127 again

this time adding inheritance to the recfun plugin so it properly contains the recursive definitions from the source.

RELEASE_NOTES

@@ -10,8 +10,8 @@ Version 4.9.next
     - native word level bit-vector solving.
   - introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
 
-Version 4.9
+Version 4.9.0
-===========
+=============
 - API for incremental parsing of assertions.
   A description of the feature is given by example here: https://github.com/Z3Prover/z3/commit/815518dc026e900392bf0d08ed859e5ec42d1e43
   It also allows incrementality at the level of adding assertions to the 
@@ -19,10 +19,21 @@ Version 4.9
 - Fold/map for sequences:
   https://microsoft.github.io/rise4fun/docs/guide/Sequences#map-and-fold
   At this point these functions are only exposed over the SMTLIB2 interface (and not programmatic API)
+  maxdiff/mindiff on arrays are more likely to be deprecated
 - User Propagator: 
   - Add functions and callbacks for external control over branching
   - A functioning dotnet API for the User Propagator 
     https://github.com/Z3Prover/z3/blob/master/src/api/dotnet/UserPropagator.cs
+- Java Script API
+  - higher level object wrappers are available thanks to Gibbons and Tomalka
+- Totalizers and RC2
+  - The MaxSAT engine now allows to run RC2 with totalizer encoding.
+    Totalizers are on by default as preliminary tests suggest this solves already 10% more problems on
+    standard benchmarks. The option rc2.totalizer (which by default is true) is used to control whether to use
+    totalizer encoding or built-in cardinality constraints.
+    The default engine is still maxres, so you have to set opt.maxsat_engine=rc2 to
+    enable the rc2 option at this point. The engines maxres-bin and rc2bin are experimental should not be used
+    (they are inferior to default options). 
 
 Version 4.8.17
 ==============

src/ast/recfun_decl_plugin.cpp

@@ -67,6 +67,30 @@ namespace recfun {
         m_decl = m.mk_func_decl(s, arity, domain, range, info);
     }
 
+    def* def::copy(util& dst, ast_translation& tr) {
+        SASSERT(&dst.m() == &tr.to());
+        sort_ref_vector domain(tr.to());
+        sort_ref range(tr(m_range.get()), tr.to());
+        for (auto* s : m_domain)
+            domain.push_back(tr(s));
+        family_id fid = dst.get_family_id();
+        bool is_generated = m_decl->get_parameter(0).get_int() != 0;
+        def* r = alloc(def, tr.to(), fid, m_name, domain.size(), domain.data(), range, is_generated);
+        r->m_rhs = tr(m_rhs.get());
+        for (auto* v : m_vars)
+            r->m_vars.push_back(tr(v));
+        for (auto const& c1 : m_cases) {
+            r->m_cases.push_back(case_def(tr.to()));
+            auto& c2 = r->m_cases.back();
+            c2.m_pred = tr(c1.m_pred.get());
+            c2.m_guards = tr(c1.m_guards);
+            c2.m_rhs = tr(c1.m_rhs.get());
+            c2.m_def = r;
+            c2.m_immediate = c1.m_immediate;
+        }
+        return r;
+    }
+
     bool def::contains_def(util& u, expr * e) {
         struct def_find_p : public i_expr_pred {
             util& u;
@@ -415,6 +439,19 @@ namespace recfun {
             return promise_def(&u(), d);
         }
 
+        void plugin::inherit(decl_plugin* other, ast_translation& tr) {
+            for (auto [k, v] : static_cast<plugin*>(other)->m_defs) {
+                func_decl_ref f(tr(k), tr.to());
+                if (m_defs.contains(f))
+                    continue;
+                def* d = v->copy(u(), tr);
+                m_defs.insert(f, d);
+                for (case_def & c : d->get_cases())
+                    m_case_defs.insert(c.get_decl(), &c);
+                    
+            }
+        }
+
         promise_def plugin::ensure_def(symbol const& name, unsigned n, sort *const * params, sort * range, bool is_generated) {
             def* d = u().decl_fun(name, n, params, range, is_generated);
             erase_def(d->get_decl());

src/ast/recfun_decl_plugin.h

@@ -21,6 +21,7 @@ Revision History:
 
 #include "ast/ast.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_translation.h"
 #include "util/obj_hashtable.h"
 
 namespace recfun {
@@ -62,6 +63,12 @@ namespace recfun {
         def *               m_def; //<! definition this is a part of
         bool                m_immediate; //<! does `rhs` contain no defined_fun/case_pred?
 
+        case_def(ast_manager& m):
+            m_pred(m),
+            m_guards(m),
+            m_rhs(m)
+        {}
+        
         case_def(ast_manager & m,
                  family_id fid,
                  def * d,
@@ -132,6 +139,8 @@ namespace recfun {
         bool is_fun_macro() const { return m_cases.size() == 1; }
         bool is_fun_defined() const { return !is_fun_macro(); }
 
+        def* copy(util& dst, ast_translation& tr);
+
     };
     
     // definition to be complete (missing RHS)
@@ -205,6 +214,8 @@ namespace recfun {
 
             expr_ref redirect_ite(replace& subst, unsigned n, var * const* vars, expr * e);
 
+            void inherit(decl_plugin* other, ast_translation& tr) override;
+
         };
     }
 

src/sat/smt/dt_solver.cpp

@@ -506,7 +506,7 @@ namespace dt {
         return m_nodes;
     }
 
-    ptr_vector<euf::enode> const& solver::get_seq_args(enode* n) {
+    ptr_vector<euf::enode> const& solver::get_seq_args(enode* n, enode*& sibling) {
         m_nodes.reset();
         m_todo.reset();
         auto add_todo = [&](enode* n) {
@@ -516,8 +516,14 @@ namespace dt {
             }
         };
 
-        for (enode* sib : euf::enode_class(n))
+        for (enode* sib : euf::enode_class(n)) {
+            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];
@@ -551,10 +557,10 @@ namespace dt {
 
         // collect equalities on all children that may have been used.
         bool found = false;
-        auto add = [&](enode* arg) {
+        auto add = [&](enode* seq_arg) {
-            if (arg->get_root() == child->get_root()) {
+            if (seq_arg->get_root() == child->get_root()) {
-                if (arg != child)
+                if (seq_arg != child)
-                    m_used_eqs.push_back(enode_pair(arg, child));
+                    m_used_eqs.push_back(enode_pair(seq_arg, child));
                 found = true;
             }
         };
@@ -564,11 +570,14 @@ namespace dt {
             if (m_autil.is_array(s) && dt.is_datatype(get_array_range(s)))
                 for (enode* aarg : get_array_args(arg))
                     add(aarg);
-        }
             sort* se;
-        if (m_sutil.is_seq(child->get_sort(), se) && dt.is_datatype(se)) {
+            if (m_sutil.is_seq(arg->get_sort(), se) && dt.is_datatype(se)) {
-            for (enode* aarg : get_seq_args(child))
+                enode* sibling = nullptr;
-                add(aarg);
+                for (enode* seq_arg : get_seq_args(arg, sibling))
+                    add(seq_arg);
+                if (sibling && sibling != arg)
+                    m_used_eqs.push_back(enode_pair(arg, sibling));                
+            }
         }
         
         VERIFY(found);
@@ -636,12 +645,13 @@ namespace dt {
             // explore `arg` (with parent)
             expr* earg = arg->get_expr();
             sort* s = earg->get_sort(), *se;
+            enode* sibling;
             if (dt.is_datatype(s)) {
                 m_parent.insert(arg->get_root(), parent);
                 oc_push_stack(arg);
             }
             else if (m_sutil.is_seq(s, se) && dt.is_datatype(se)) {
-                for (enode* sarg : get_seq_args(arg))
+                for (enode* sarg : get_seq_args(arg, sibling))
                     if (process_arg(sarg))
                         return true;
             }

src/sat/smt/dt_solver.h

@@ -112,7 +112,7 @@ namespace dt {
         void oc_push_stack(enode * n);
         ptr_vector<enode> m_nodes, 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);
 
         void pop_core(unsigned n) override;