mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

apply relevancy filtering on unsupported ops, fix term construction bug in bv2fpa_converter fix #6548

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-01-20 13:04:50 -08:00
parent 37652e7e17
commit 0f4f32c5d0
5 changed files with 23 additions and 22 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/fpa/bv2fpa_converter.cpp
View file

@ -325,7 +325,7 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
result->set_else(else_value); result->set_else(else_value);
} }
else if (m_fpa_util.is_to_real(f)) { else if (m_fpa_util.is_to_real(f)) {
expr_ref_vector dom(m); 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); 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); expr_ref else_value(m.mk_app(to_real_i, dom.size(), dom.data()), m);
result->set_else(else_value); result->set_else(else_value);

3
src/smt/theory_arith.h
View file

@ -436,9 +436,8 @@ namespace smt {
theory_arith_params & m_params; theory_arith_params & m_params;
arith_util m_util; arith_util m_util;
arith_eq_solver m_arith_eq_solver; arith_eq_solver m_arith_eq_solver;
bool m_found_unsupported_op;
bool m_found_underspecified_op;
ptr_vector<app> m_underspecified_ops; ptr_vector<app> m_underspecified_ops;
ptr_vector<app> m_unsupported_ops;
arith_eq_adapter m_arith_eq_adapter; arith_eq_adapter m_arith_eq_adapter;
vector<row> m_rows; vector<row> m_rows;
svector<unsigned> m_dead_rows; svector<unsigned> m_dead_rows;

3
src/smt/theory_arith_aux.h
View file

@ -2169,9 +2169,8 @@ namespace smt {
*/ */
template<typename Ext> template<typename Ext>
bool theory_arith<Ext>::is_shared(theory_var v) const { bool theory_arith<Ext>::is_shared(theory_var v) const {
if (!m_found_underspecified_op) { if (m_underspecified_ops.empty())
return false; return false;
}
enode * n = get_enode(v); enode * n = get_enode(v);
enode * r = n->get_root(); enode * r = n->get_root();
enode_vector::const_iterator it = r->begin_parents(); enode_vector::const_iterator it = r->begin_parents();

26
src/smt/theory_arith_core.h
View file

@ -29,22 +29,16 @@ namespace smt {
template<typename Ext> template<typename Ext>
void theory_arith<Ext>::found_unsupported_op(app * n) { void theory_arith<Ext>::found_unsupported_op(app * n) {
if (!m_found_unsupported_op) { CTRACE("arith", m_unsupported_ops.empty(), tout << "found non supported expression:\n" << mk_pp(n, m) << "\n";);
TRACE("arith", tout << "found non supported expression:\n" << mk_pp(n, m) << "\n";); m_unsupported_ops.push_back(n);
ctx.push_trail(value_trail<bool>(m_found_unsupported_op)); ctx.push_trail(push_back_vector<ptr_vector<app>>(m_unsupported_ops));
m_found_unsupported_op = true;
}
} }
template<typename Ext> template<typename Ext>
void theory_arith<Ext>::found_underspecified_op(app * n) { void theory_arith<Ext>::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); m_underspecified_ops.push_back(n);
ctx.push_trail(push_back_vector<ptr_vector<app>>(m_underspecified_ops)); ctx.push_trail(push_back_vector<ptr_vector<app>>(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<bool>(m_found_underspecified_op));
m_found_underspecified_op = true;
}
expr* e = nullptr; expr* e = nullptr;
if (m_util.is_div(n)) { if (m_util.is_div(n)) {
@ -1532,9 +1526,13 @@ namespace smt {
} }
} }
while (m_final_check_idx != old_idx); while (m_final_check_idx != old_idx);
if (result == FC_DONE && m_found_unsupported_op) { if (result == FC_DONE) {
TRACE("arith", tout << "Found unsupported operation\n";); for (app* n : m_unsupported_ops) {
result = FC_GIVEUP; if (!ctx.is_relevant(n))
continue;
TRACE("arith", tout << "Found unsupported operation " << mk_pp(n, m) << "\n");
result = FC_GIVEUP;
}
} }
return result; return result;
} }
@ -1733,8 +1731,6 @@ namespace smt {
m_params(ctx.get_fparams()), m_params(ctx.get_fparams()),
m_util(m), m_util(m),
m_arith_eq_solver(m), m_arith_eq_solver(m),
m_found_unsupported_op(false),
m_found_underspecified_op(false),
m_arith_eq_adapter(*this, m_util), m_arith_eq_adapter(*this, m_util),
m_asserted_qhead(0), m_asserted_qhead(0),
m_row_vars_top(0), m_row_vars_top(0),

9
src/smt/theory_lra.cpp
View file

@ -454,6 +454,11 @@ class theory_lra::imp {
st.to_ensure_var().push_back(n1); st.to_ensure_var().push_back(n1);
st.to_ensure_var().push_back(n2); 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)) { else if (!a.is_div0(n)) {
found_unsupported(n); found_unsupported(n);
} }
@ -543,7 +548,7 @@ class theory_lra::imp {
} }
enode * mk_enode(app * n) { 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)) if (reflect(n))
for (expr* arg : *n) for (expr* arg : *n)
if (!ctx().e_internalized(arg)) if (!ctx().e_internalized(arg))
@ -1600,6 +1605,8 @@ public:
return FC_CONTINUE; return FC_CONTINUE;
} }
for (expr* e : m_not_handled) { for (expr* e : m_not_handled) {
if (!ctx().is_relevant(e))
continue;
(void) e; // just in case TRACE() is a no-op (void) e; // just in case TRACE() is a no-op
TRACE("arith", tout << "unhandled operator " << mk_pp(e, m) << "\n";); TRACE("arith", tout << "unhandled operator " << mk_pp(e, m) << "\n";);
st = FC_GIVEUP; st = FC_GIVEUP;