#5532

bugs in:
- rewriting of 0-ary expressions was incomplete
- sharing annotations when a node has two theories attached it is shared
- sharing of const of an array

Remove unreadable part of pretty printer for lp solver.

src/sat/smt/arith_diagnostics.cpp

@@ -57,7 +57,11 @@ namespace arith {
                 if (ctx.is_shared(var2enode(v))) 
                     out << ", shared";
             }
-            out << " := " << mk_bounded_pp(var2expr(v), m) << "\n";
+            expr* e = var2expr(v);
+            out << " := ";
+            if (e)
+                out << "#" << e->get_id() << ": ";
+            out << mk_bounded_pp(var2expr(v), m) << "\n";
         }
         return out; 
     }

src/sat/smt/arith_solver.cpp

@@ -584,13 +584,23 @@ namespace arith {
 
             TRACE("arith",
                 ptr_vector<expr> nodes;
+                expr_mark marks;
                 nodes.push_back(n->get_expr());
                 for (unsigned i = 0; i < nodes.size(); ++i) {
                     expr* r = nodes[i];
+                    if (marks.is_marked(r))
+                        continue;
+                    marks.mark(r);
                     if (is_app(r))
                         for (expr* arg : *to_app(r))
                             nodes.push_back(arg);
-                    tout << r->get_id() << ": " << mk_bounded_pp(r, m, 1) << " := " << mdl(r) << "\n";
+                    expr_ref rval(m);                    
+                    expr_ref mval = mdl(r);
+                    if (ctx.get_egraph().find(r))
+                        rval = mdl(ctx.get_egraph().find(r)->get_root()->get_expr());
+                    tout << r->get_id() << ": " << mk_bounded_pp(r, m, 1) << " := " << mval;
+                    if (rval != mval) tout << " " << rval;
+                    tout << "\n";
                 });
             TRACE("arith",
                 tout << eval << " " << value << " " << ctx.bpp(n) << "\n";

src/sat/smt/array_axioms.cpp

@@ -570,10 +570,12 @@ namespace array {
                 expr* e2 = var2expr(v2);
                 if (e1->get_sort() != e2->get_sort())
                     continue;
-                if (must_have_different_model_values(v1, v2))
+                if (must_have_different_model_values(v1, v2)) {
                     continue;
-                if (ctx.get_egraph().are_diseq(var2enode(v1), var2enode(v2)))
-                    continue;              
+                }
+                if (ctx.get_egraph().are_diseq(var2enode(v1), var2enode(v2))) {
+                    continue;
+                }
                 sat::literal lit = eq_internalize(e1, e2);
                 if (s().value(lit) == l_undef) 
                     prop = true;
@@ -594,7 +596,7 @@ namespace array {
             if (r->is_marked1()) 
                 continue;            
             // arrays used as indices in other arrays have to be treated as shared issue #3532, #3529            
-            if (ctx.is_shared(r) || is_select_arg(r)) 
+            if (ctx.is_shared(r) || is_shared_arg(r)) 
                 roots.push_back(r->get_th_var(get_id()));
             
             r->mark1();
@@ -605,13 +607,18 @@ namespace array {
             n->unmark1();
     }
 
-    bool solver::is_select_arg(euf::enode* r) {
+    bool solver::is_shared_arg(euf::enode* r) {
         SASSERT(r->is_root());
-        for (euf::enode* n : euf::enode_parents(r)) 
-            if (a.is_select(n->get_expr())) 
-                for (unsigned i = 1; i < n->num_args(); ++i) 
-                    if (r == n->get_arg(i)->get_root()) 
+        for (euf::enode* n : euf::enode_parents(r)) {
+            expr* e = n->get_expr();
+            if (a.is_select(e))
+                for (unsigned i = 1; i < n->num_args(); ++i)
+                    if (r == n->get_arg(i)->get_root())
                         return true;
+            if (a.is_const(e))
+                return true;
+        }
+            
         return false;
     }
 

src/sat/smt/array_model.cpp

@@ -111,6 +111,7 @@ namespace array {
             }
         }
         
+        TRACE("array", tout << "array-as-function " << ctx.bpp(n) << " := " << mk_pp(f, m) << "\n" << "default " << mk_pp(fi->get_else(), m) << "\n";);
         parameter p(f);
         values.set(n->get_expr_id(), m.mk_app(get_id(), OP_AS_ARRAY, 1, &p));
     }
@@ -215,8 +216,8 @@ namespace array {
     }
 
     void solver::set_default(theory_var v, euf::enode* n) {
-        TRACE("array", tout << "set default: " << v << " " << ctx.bpp(n) << "\n";);
         v = mg_find(v);
+        CTRACE("array", !m_defaults[v], tout << "set default: " << v << " " << ctx.bpp(n) << "\n";);
         if (!m_defaults[v]) 
             m_defaults[v] = n;
     }

src/sat/smt/array_solver.h

@@ -190,7 +190,7 @@ namespace array {
         std::pair<app*, func_decl*> mk_epsilon(sort* s);
         void collect_shared_vars(sbuffer<theory_var>& roots);
         bool add_interface_equalities();
-        bool is_select_arg(euf::enode* r);
+        bool is_shared_arg(euf::enode* r);
         bool is_array(euf::enode* n) const { return a.is_array(n->get_expr()); }
 
         // solving          

src/sat/smt/euf_internalize.cpp

@@ -335,12 +335,14 @@ namespace euf {
 
         // the variable is shared if the equivalence class of n
         // contains a parent application.
-
+        
         family_id th_id = m.get_basic_family_id();
         for (auto p : euf::enode_th_vars(n)) {
-            if (m.get_basic_family_id() != p.get_id()) {
-                th_id = p.get_id();
-                break;
+            family_id id = p.get_id();
+            if (m.get_basic_family_id() != id) {
+                if (th_id != m.get_basic_family_id())
+                    return true;
+                th_id = id;               
             }
         }
         if (m.is_bool(n->get_expr()) && th_id != m.get_basic_family_id())

src/sat/smt/euf_model.cpp

@@ -228,9 +228,12 @@ namespace euf {
                 SASSERT(args.size() == arity);
                 if (!fi->get_entry(args.data()))
                     fi->insert_new_entry(args.data(), v);
-                TRACE("euf", tout << f->get_name() << "\n";
+                TRACE("euf", tout << bpp(n) << " " << f->get_name() << "\n";
                       for (expr* arg : args) tout << mk_pp(arg, m) << " ";
-                      tout << "\n -> " << mk_pp(v, m) << "\n";);
+                      tout << "\n -> " << mk_pp(v, m) << "\n";
+		      for (euf::enode* arg : euf::enode_args(n)) tout << bpp(arg) << " ";
+		      tout << "\n";
+		      );
 
             }
         }