From 0f4f32c5d020e4d63fa84a64f3136f6ad84aefb2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 20 Jan 2023 13:04:50 -0800 Subject: [PATCH] apply relevancy filtering on unsupported ops, fix term construction bug in bv2fpa_converter fix #6548 --- src/ast/fpa/bv2fpa_converter.cpp | 4 ++-- src/smt/theory_arith.h | 3 +-- src/smt/theory_arith_aux.h | 3 +-- src/smt/theory_arith_core.h | 26 +++++++++++--------------- src/smt/theory_lra.cpp | 9 ++++++++- 5 files changed, 23 insertions(+), 22 deletions(-) diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index 597ab9ca6..00e9d71c3 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -324,8 +324,8 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * expr_ref else_value(m.mk_app(to_bv_i, dom.size(), dom.data()), m); result->set_else(else_value); } - else if (m_fpa_util.is_to_real(f)) { - expr_ref_vector dom(m); + else if (m_fpa_util.is_to_real(f)) { + SASSERT(dom.size() == 1); func_decl_ref to_real_i(m.mk_func_decl(fid, OP_FPA_TO_REAL_I, 0, nullptr, dom.size(), dom.data()), m); expr_ref else_value(m.mk_app(to_real_i, dom.size(), dom.data()), m); result->set_else(else_value); diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h index 07709666b..34a76d955 100644 --- a/src/smt/theory_arith.h +++ b/src/smt/theory_arith.h @@ -436,9 +436,8 @@ namespace smt { theory_arith_params & m_params; arith_util m_util; arith_eq_solver m_arith_eq_solver; - bool m_found_unsupported_op; - bool m_found_underspecified_op; ptr_vector m_underspecified_ops; + ptr_vector m_unsupported_ops; arith_eq_adapter m_arith_eq_adapter; vector m_rows; svector m_dead_rows; diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index d5eca0bc4..470ea5f7b 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -2169,9 +2169,8 @@ namespace smt { */ template bool theory_arith::is_shared(theory_var v) const { - if (!m_found_underspecified_op) { + if (m_underspecified_ops.empty()) return false; - } enode * n = get_enode(v); enode * r = n->get_root(); enode_vector::const_iterator it = r->begin_parents(); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 2d18a3496..3a5c86207 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -29,22 +29,16 @@ namespace smt { template void theory_arith::found_unsupported_op(app * n) { - if (!m_found_unsupported_op) { - TRACE("arith", tout << "found non supported expression:\n" << mk_pp(n, m) << "\n";); - ctx.push_trail(value_trail(m_found_unsupported_op)); - m_found_unsupported_op = true; - } + CTRACE("arith", m_unsupported_ops.empty(), tout << "found non supported expression:\n" << mk_pp(n, m) << "\n";); + m_unsupported_ops.push_back(n); + ctx.push_trail(push_back_vector>(m_unsupported_ops)); } template void theory_arith::found_underspecified_op(app * n) { + CTRACE("arith", m_underspecified_ops.empty(), tout << "found underspecified expression:\n" << mk_pp(n, m) << "\n";); m_underspecified_ops.push_back(n); ctx.push_trail(push_back_vector>(m_underspecified_ops)); - if (!m_found_underspecified_op) { - TRACE("arith", tout << "found underspecified expression:\n" << mk_pp(n, m) << "\n";); - ctx.push_trail(value_trail(m_found_underspecified_op)); - m_found_underspecified_op = true; - } expr* e = nullptr; if (m_util.is_div(n)) { @@ -1532,9 +1526,13 @@ namespace smt { } } while (m_final_check_idx != old_idx); - if (result == FC_DONE && m_found_unsupported_op) { - TRACE("arith", tout << "Found unsupported operation\n";); - result = FC_GIVEUP; + if (result == FC_DONE) { + for (app* n : m_unsupported_ops) { + if (!ctx.is_relevant(n)) + continue; + TRACE("arith", tout << "Found unsupported operation " << mk_pp(n, m) << "\n"); + result = FC_GIVEUP; + } } return result; } @@ -1733,8 +1731,6 @@ namespace smt { m_params(ctx.get_fparams()), m_util(m), m_arith_eq_solver(m), - m_found_unsupported_op(false), - m_found_underspecified_op(false), m_arith_eq_adapter(*this, m_util), m_asserted_qhead(0), m_row_vars_top(0), diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 1309724d2..0507f7564 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -454,6 +454,11 @@ class theory_lra::imp { st.to_ensure_var().push_back(n1); st.to_ensure_var().push_back(n2); } + else if (a.is_power(n, n1, n2)) { + found_unsupported(n); + st.to_ensure_var().push_back(n1); + st.to_ensure_var().push_back(n2); + } else if (!a.is_div0(n)) { found_unsupported(n); } @@ -543,7 +548,7 @@ class theory_lra::imp { } enode * mk_enode(app * n) { - TRACE("arith", tout << expr_ref(n, m) << " internalized: " << ctx().e_internalized(n) << "\n";); + TRACE("arith", tout << mk_bounded_pp(n, m) << " internalized: " << ctx().e_internalized(n) << "\n";); if (reflect(n)) for (expr* arg : *n) if (!ctx().e_internalized(arg)) @@ -1600,6 +1605,8 @@ public: return FC_CONTINUE; } for (expr* e : m_not_handled) { + if (!ctx().is_relevant(e)) + continue; (void) e; // just in case TRACE() is a no-op TRACE("arith", tout << "unhandled operator " << mk_pp(e, m) << "\n";); st = FC_GIVEUP;