#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.
Z3Prover · Sep 6, 2021 · 72f6271 · 72f6271
1 parent 3764eb1
commit 72f6271
Show file tree

Hide file tree

Showing 13 changed files with 70 additions and 38 deletions.
diff --git a/src/ast/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp
@@ -80,6 +80,9 @@ class ll_printer {
                 display_child_ref(n);
             }
             break;
+        case AST_FUNC_DECL:
+            m_out << to_func_decl(n)->get_name();
+            break;
         default:
             display_child_ref(n);
         }

diff --git a/src/ast/rewriter/array_rewriter.cpp b/src/ast/rewriter/array_rewriter.cpp
@@ -247,7 +247,6 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
         // select(as-array[f], I) --> f(I)
         func_decl * f = m_util.get_as_array_func_decl(to_app(args[0]));
         result = m().mk_app(f, num_args - 1, args + 1);
-        TRACE("array", tout << mk_pp(args[0], m()) << " " << result << "\n";);
         return BR_REWRITE1;
     }
 

diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
@@ -192,12 +192,16 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
     switch (t->get_kind()) {
     case AST_APP:
         if (to_app(t)->get_num_args() == 0) {
-            if (process_const<ProofGen>(to_app(t))) 
-                return true; 
-            TRACE("rewriter", tout << "process const: " << mk_bounded_pp(t, m()) << " -> " << mk_bounded_pp(m_r,m()) << "\n";);
-	        set_new_child_flag(t, m_r);
-	        result_stack().push_back(m_r);
-	        return true;
+            if (process_const<ProofGen>(to_app(t)))
+                return true;
+            TRACE("rewriter_const", tout << "process const: " << mk_bounded_pp(t, m()) << " -> " << mk_bounded_pp(m_r, m()) << "\n";);
+            rewriter_tpl rw(m(), false, m_cfg);
+            expr_ref result(m());
+            rw(m_r, result, m_pr);
+            m_r = result;
+            set_new_child_flag(t, m_r);
+            result_stack().push_back(m_r);
+            return true;
         }
         if (max_depth != RW_UNBOUNDED_DEPTH)
             max_depth--;

diff --git a/src/math/lp/core_solver_pretty_printer.h b/src/math/lp/core_solver_pretty_printer.h
@@ -118,10 +118,6 @@ class core_solver_pretty_printer {
 
     void print_basis_heading();
 
-    void print_bottom_line() {
-        m_out << "----------------------" << std::endl;
-    }
-
     void print_cost();
 
     void print_given_row(vector<string> & row, vector<string> & signs, X rst);

diff --git a/src/math/lp/core_solver_pretty_printer_def.h b/src/math/lp/core_solver_pretty_printer_def.h
@@ -345,12 +345,6 @@ template <typename T, typename X> void core_solver_pretty_printer<T, X>::print()
     for (unsigned i = 0; i < nrows(); i++) {
         print_row(i);
     }
-    print_bottom_line();
-    print_cost();
-    print_x();
-    print_basis_heading();
-    print_lows();
-    print_upps();
     print_exact_norms();
     if (!m_core_solver.m_column_norms.empty())
         print_approx_norms();

diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
@@ -18,6 +18,7 @@ Revision History:
 --*/
 #include "ast/ast_pp.h"
 #include "ast/ast_util.h"
+#include "ast/for_each_expr.h"
 #include "ast/recfun_decl_plugin.h"
 #include "ast/rewriter/rewriter_types.h"
 #include "ast/rewriter/bool_rewriter.h"
@@ -278,6 +279,9 @@ struct evaluator_cfg : public default_rewriter_cfg {
         }
         expr_ref tmp(m);
         func_interp* fi = m_model.get_func_interp(g);
+        if (fi && !fi->get_else()) {
+            fi->set_else(m_model.get_some_value(g->get_range()));
+        }
         if (fi && (tmp = fi->get_array_interp(g))) {
             model_evaluator ev(m_model, m_params);
             ev.set_model_completion(false);
@@ -287,6 +291,10 @@ struct evaluator_cfg : public default_rewriter_cfg {
             TRACE("model_evaluator", tout << mk_pp(g, m) << " " << result << "\n";);
             return true;
         }
+
+        TRACE("model_evaluator",
+            tout << "could not get array interpretation " << mk_pp(g, m) << " " << fi << "\n";
+            tout << m_model << "\n";);                    
 
         return false;
     }
@@ -403,15 +411,16 @@ struct evaluator_cfg : public default_rewriter_cfg {
     }
 
     br_status mk_array_eq(expr* a, expr* b, expr_ref& result) {
-        TRACE("model_evaluator", tout << "mk_array_eq " << m_array_equalities << " " 
-              << mk_pp(a, m) << " " << mk_pp(b, m) << "\n";);
+
         if (a == b) {
             result = m.mk_true();
             return BR_DONE;
         }
         if (!m_array_equalities) {
             return m_ar_rw.mk_eq_core(a, b, result);
         }
+        TRACE("model_evaluator", tout << "mk_array_eq " << m_array_equalities << " "
+            << mk_pp(a, m) << " " << mk_pp(b, m) << "\n";);
 
         vector<expr_ref_vector> stores1, stores2;
         bool args_are_unique1, args_are_unique2;

diff --git a/src/sat/smt/arith_diagnostics.cpp b/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; 
     }

diff --git a/src/sat/smt/arith_solver.cpp b/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";

diff --git a/src/sat/smt/array_axioms.cpp b/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;
     }
 

diff --git a/src/sat/smt/array_model.cpp b/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;
     }

diff --git a/src/sat/smt/array_solver.h b/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          

diff --git a/src/sat/smt/euf_internalize.cpp b/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())

diff --git a/src/sat/smt/euf_model.cpp b/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";
+		      );
 
             }
         }