From ca7d066c4e591c42b704c97eb27a06da5ad5b763 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 10 Oct 2019 19:20:02 -0700 Subject: [PATCH] fix #2624 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/arith_rewriter.cpp | 22 +++++++++++ src/ast/static_features.cpp | 61 +++++++++++++++-------------- src/ast/static_features.h | 6 +-- src/smt/params/smt_params.cpp | 2 - src/smt/params/smt_params.h | 4 -- src/smt/smt_context.cpp | 39 +++++------------- 6 files changed, 66 insertions(+), 68 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 53f7c85cd..56af9a00d 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -483,6 +483,28 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin return BR_REWRITE_FULL; } } + expr* c = nullptr, *t = nullptr, *e = nullptr; + if (m().is_ite(arg1, c, t, e) && is_numeral(t, a1) && is_numeral(arg2, a2)) { + switch (kind) { + case LE: result = a1 <= a2 ? m().mk_or(c, m_util.mk_le(e, arg2)) : m().mk_and(m().mk_not(c), m_util.mk_le(e, arg2)); return BR_REWRITE2; + case GE: result = a1 >= a1 ? m().mk_or(c, m_util.mk_ge(e, arg2)) : m().mk_and(m().mk_not(c), m_util.mk_ge(e, arg2)); return BR_REWRITE2; + case EQ: result = a1 == a2 ? m().mk_or(c, m().mk_eq(e, arg2)) : m().mk_and(m().mk_not(c), m_util.mk_eq(e, arg2)); return BR_REWRITE2; + } + } + if (m().is_ite(arg1, c, t, e) && is_numeral(e, a1) && is_numeral(arg2, a2)) { + switch (kind) { + case LE: result = a1 <= a2 ? m().mk_or(m().mk_not(c), m_util.mk_le(t, arg2)) : m().mk_and(c, m_util.mk_le(t, arg2)); return BR_REWRITE2; + case GE: result = a1 >= a1 ? m().mk_or(m().mk_not(c), m_util.mk_ge(t, arg2)) : m().mk_and(c, m_util.mk_ge(t, arg2)); return BR_REWRITE2; + case EQ: result = a1 == a2 ? m().mk_or(m().mk_not(c), m().mk_eq(t, arg2)) : m().mk_and(c, m_util.mk_eq(t, arg2)); return BR_REWRITE2; + } + } + if (m().is_ite(arg1, c, t, e) && arg1->get_ref_count() == 1) { + switch (kind) { + case LE: result = m().mk_ite(c, m_util.mk_le(t, arg2), m_util.mk_le(e, arg2)); return BR_REWRITE2; + case GE: result = m().mk_ite(c, m_util.mk_ge(t, arg2), m_util.mk_ge(e, arg2)); return BR_REWRITE2; + case EQ: result = m().mk_ite(c, m().mk_eq(t, arg2), m().mk_eq(e, arg2)); return BR_REWRITE2; + } + } if ((m_arith_lhs || m_arith_ineq_lhs) && is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) { a2.neg(); new_arg2 = m_util.mk_numeral(a2, m_util.is_int(new_arg1)); diff --git a/src/ast/static_features.cpp b/src/ast/static_features.cpp index c16557a50..f216022f2 100644 --- a/src/ast/static_features.cpp +++ b/src/ast/static_features.cpp @@ -20,7 +20,7 @@ Revision History: #include "ast/ast_pp.h" static_features::static_features(ast_manager & m): - m_manager(m), + m(m), m_autil(m), m_bvutil(m), m_arrayutil(m), @@ -123,31 +123,32 @@ bool static_features::is_diff_term(expr const * e, rational & r) const { } if (is_numeral(e, r)) return true; - return m_autil.is_add(e) && to_app(e)->get_num_args() == 2 && is_numeral(to_app(e)->get_arg(0), r) && !is_arith_expr(to_app(e)->get_arg(1)); + expr* a1 = nullptr, *a2 = nullptr; + return m_autil.is_add(e, a1, a2) && is_numeral(a1, r) && !is_arith_expr(a2) && !m.is_ite(a2); } bool static_features::is_diff_atom(expr const * e) const { if (!is_bool(e)) return false; - if (!m_manager.is_eq(e) && !is_arith_expr(e)) + if (!m.is_eq(e) && !is_arith_expr(e)) return false; SASSERT(to_app(e)->get_num_args() == 2); expr * lhs = to_app(e)->get_arg(0); expr * rhs = to_app(e)->get_arg(1); - if (!is_arith_expr(lhs) && !is_arith_expr(rhs)) + if (!is_arith_expr(lhs) && !is_arith_expr(rhs) && !m.is_ite(lhs) && !m.is_ite(rhs)) return true; if (!is_numeral(rhs)) return false; // lhs can be 'x' or '(+ x (* -1 y))' or '(+ (* -1 x) y)' - if (!is_arith_expr(lhs)) + if (!is_arith_expr(lhs) && !m.is_ite(lhs)) return true; expr* arg1, *arg2; if (!m_autil.is_add(lhs, arg1, arg2)) return false; expr* m1, *m2; - if (!is_arith_expr(arg1) && m_autil.is_mul(arg2, m1, m2) && is_minus_one(m1) && !is_arith_expr(m2)) + if (!is_arith_expr(arg1) && m_autil.is_mul(arg2, m1, m2) && is_minus_one(m1) && !is_arith_expr(m2) && !m.is_ite(m2)) return true; - if (!is_arith_expr(arg2) && m_autil.is_mul(arg1, m1, m2) && is_minus_one(m1) && !is_arith_expr(m2)) + if (!is_arith_expr(arg2) && m_autil.is_mul(arg1, m1, m2) && is_minus_one(m1) && !is_arith_expr(m2) && !m.is_ite(m2)) return true; return false; @@ -159,7 +160,7 @@ bool static_features::is_gate(expr const * e) const { case OP_ITE: case OP_AND: case OP_OR: case OP_XOR: case OP_IMPLIES: return true; case OP_EQ: - return m_manager.is_bool(e); + return m.is_bool(e); } } return false; @@ -170,12 +171,12 @@ void static_features::update_core(expr * e) { // even if a benchmark does not contain any theory interpreted function decls, we still have to install // the theory if the benchmark contains constants or function applications of an interpreted sort. - sort * s = m_manager.get_sort(e); - if (!m_manager.is_uninterp(s)) + sort * s = m.get_sort(e); + if (!m.is_uninterp(s)) mark_theory(s->get_family_id()); bool _is_gate = is_gate(e); - bool _is_eq = m_manager.is_eq(e); + bool _is_eq = m.is_eq(e); if (_is_gate) { m_cnf = false; m_num_nested_formulas++; @@ -191,12 +192,12 @@ void static_features::update_core(expr * e) { acc_num(arg); // Must check whether arg is diff logic or not. // Otherwise, problem can be incorrectly tagged as diff logic. - sort * arg_s = m_manager.get_sort(arg); + sort * arg_s = m.get_sort(arg); family_id fid_arg = arg_s->get_family_id(); if (fid_arg == m_afid) { m_num_arith_terms++; rational k; - TRACE("diff_term", tout << "diff_term: " << is_diff_term(arg, k) << "\n" << mk_pp(arg, m_manager) << "\n";); + TRACE("diff_term", tout << "diff_term: " << is_diff_term(arg, k) << "\n" << mk_pp(arg, m) << "\n";); if (is_diff_term(arg, k)) { m_num_diff_terms++; acc_num(k); @@ -238,7 +239,7 @@ void static_features::update_core(expr * e) { bool _is_le_ge = m_autil.is_le(e) || m_autil.is_ge(e); if (_is_le_ge) { m_num_arith_ineqs++; - TRACE("diff_atom", tout << "diff_atom: " << is_diff_atom(e) << "\n" << mk_pp(e, m_manager) << "\n";); + TRACE("diff_atom", tout << "diff_atom: " << is_diff_atom(e) << "\n" << mk_pp(e, m) << "\n";); if (is_diff_atom(e)) m_num_diff_ineqs++; if (!is_arith_expr(to_app(e)->get_arg(0))) @@ -255,14 +256,14 @@ void static_features::update_core(expr * e) { if (is_numeral(to_app(e)->get_arg(1))) { acc_num(to_app(e)->get_arg(1)); m_num_arith_eqs++; - TRACE("diff_atom", tout << "diff_atom: " << is_diff_atom(e) << "\n" << mk_pp(e, m_manager) << "\n";); + TRACE("diff_atom", tout << "diff_atom: " << is_diff_atom(e) << "\n" << mk_pp(e, m) << "\n";); if (is_diff_atom(e)) m_num_diff_eqs++; if (!is_arith_expr(to_app(e)->get_arg(0))) m_num_simple_eqs++; } - sort * s = m_manager.get_sort(to_app(e)->get_arg(0)); - if (!m_manager.is_uninterp(s)) { + sort * s = m.get_sort(to_app(e)->get_arg(0)); + if (!m.is_uninterp(s)) { family_id fid = s->get_family_id(); if (fid != null_family_id && fid != m_bfid) inc_theory_eqs(fid); @@ -300,7 +301,7 @@ void static_features::update_core(expr * e) { m_num_interpreted_constants++; } if (fid == m_afid) { - // std::cout << mk_pp(e, m_manager) << "\n"; + // std::cout << mk_pp(e, m) << "\n"; switch (to_app(e)->get_decl_kind()) { case OP_MUL: if (!is_numeral(to_app(e)->get_arg(0)) || to_app(e)->get_num_args() > 2) { @@ -320,8 +321,8 @@ void static_features::update_core(expr * e) { m_num_uninterpreted_exprs++; if (to_app(e)->get_num_args() == 0) { m_num_uninterpreted_constants++; - sort * s = m_manager.get_sort(e); - if (!m_manager.is_uninterp(s)) { + sort * s = m.get_sort(e); + if (!m.is_uninterp(s)) { family_id fid = s->get_family_id(); if (fid != null_family_id && fid != m_bfid) inc_theory_constants(fid); @@ -329,7 +330,7 @@ void static_features::update_core(expr * e) { } } if (m_arrayutil.is_array(e)) { - TRACE("sf_array", tout << mk_ismt2_pp(e, m_manager) << "\n";); + TRACE("sf_array", tout << mk_ismt2_pp(e, m) << "\n";); sort * ty = to_app(e)->get_decl()->get_range(); mark_theory(ty->get_family_id()); unsigned n = ty->get_num_parameters(); @@ -347,8 +348,8 @@ void static_features::update_core(expr * e) { } if (!_is_eq && !_is_gate) { for (expr * arg : *to_app(e)) { - sort * arg_s = m_manager.get_sort(arg); - if (!m_manager.is_uninterp(arg_s)) { + sort * arg_s = m.get_sort(arg); + if (!m.is_uninterp(arg_s)) { family_id fid_arg = arg_s->get_family_id(); if (fid_arg != fid && fid_arg != null_family_id) { m_num_aliens++; @@ -357,7 +358,7 @@ void static_features::update_core(expr * e) { SASSERT(!_is_le_ge); m_num_arith_terms++; rational k; - TRACE("diff_term", tout << "diff_term: " << is_diff_term(arg, k) << "\n" << mk_pp(arg, m_manager) << "\n";); + TRACE("diff_term", tout << "diff_term: " << is_diff_term(arg, k) << "\n" << mk_pp(arg, m) << "\n";); if (is_diff_term(arg, k)) { m_num_diff_terms++; acc_num(k); @@ -385,7 +386,7 @@ void static_features::update_core(sort * s) { } void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite_ctx, unsigned stack_depth) { - TRACE("static_features", tout << "processing\n" << mk_pp(e, m_manager) << "\n";); + TRACE("static_features", tout << "processing\n" << mk_pp(e, m) << "\n";); if (is_var(e)) return; if (is_marked(e)) { @@ -413,7 +414,7 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite if (is_basic_expr(e)) { switch (to_app(e)->get_decl_kind()) { case OP_ITE: - form_ctx_new = m_manager.is_bool(e); + form_ctx_new = m.is_bool(e); ite_ctx_new = true; break; case OP_AND: @@ -435,7 +436,7 @@ void static_features::process(expr * e, bool form_ctx, bool or_and_ctx, bool ite unsigned num_args = to_app(e)->get_num_args(); for (unsigned i = 0; i < num_args; i++) { expr * arg = to_app(e)->get_arg(i); - if (m_manager.is_not(arg)) + if (m.is_not(arg)) arg = to_app(arg)->get_arg(0); process(arg, form_ctx_new, or_and_ctx_new, ite_ctx_new, stack_depth+1); depth = std::max(depth, get_depth(arg)); @@ -490,7 +491,7 @@ void static_features::process_root(expr * e) { return; } m_num_roots++; - if (m_manager.is_or(e)) { + if (m.is_or(e)) { mark(e); m_num_clauses++; m_num_bool_exprs++; @@ -503,7 +504,7 @@ void static_features::process_root(expr * e) { unsigned or_and_depth = 0; for (unsigned i = 0; i < num_args; i++) { expr * arg = to_app(e)->get_arg(i); - if (m_manager.is_not(arg)) + if (m.is_not(arg)) arg = to_app(arg)->get_arg(0); process(arg, true, true, false, 0); depth = std::max(depth, get_depth(arg)); @@ -547,7 +548,7 @@ bool static_features::internal_family(symbol const & f_name) const { void static_features::display_family_data(std::ostream & out, char const * prefix, unsigned_vector const & data) const { for (unsigned fid = 0; fid < data.size(); fid++) { - symbol const & n = m_manager.get_family_name(fid); + symbol const & n = m.get_family_name(fid); if (!internal_family(n)) out << prefix << "_" << n << " " << data[fid] << "\n"; } diff --git a/src/ast/static_features.h b/src/ast/static_features.h index 047c429b7..f7a59ca00 100644 --- a/src/ast/static_features.h +++ b/src/ast/static_features.h @@ -29,7 +29,7 @@ Revision History: #include "util/map.h" struct static_features { - ast_manager & m_manager; + ast_manager & m; arith_util m_autil; bv_util m_bvutil; array_util m_arrayutil; @@ -120,7 +120,7 @@ struct static_features { bool is_marked(ast * e) const { return m_already_visited.is_marked(e); } void mark(ast * e) { m_already_visited.mark(e, true); } - bool is_bool(expr const * e) const { return m_manager.is_bool(e); } + bool is_bool(expr const * e) const { return m.is_bool(e); } bool is_basic_expr(expr const * e) const { return is_app(e) && to_app(e)->get_family_id() == m_bfid; } bool is_arith_expr(expr const * e) const { return is_app(e) && to_app(e)->get_family_id() == m_afid; } bool is_numeral(expr const * e) const { return m_autil.is_numeral(e); } @@ -130,7 +130,7 @@ struct static_features { bool is_diff_atom(expr const * e) const; bool is_gate(expr const * e) const; void mark_theory(family_id fid) { - if (fid != null_family_id && !m_manager.is_builtin_family_id(fid) && !m_theories.get(fid, false)) { + if (fid != null_family_id && !m.is_builtin_family_id(fid) && !m_theories.get(fid, false)) { m_theories.setx(fid, true, false); m_num_theories++; } diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index c38b9fbb2..89147165c 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -142,7 +142,6 @@ void smt_params::display(std::ostream & out) const { DISPLAY_PARAM(m_profile_res_sub); DISPLAY_PARAM(m_display_bool_var2expr); DISPLAY_PARAM(m_display_ll_bool_var2expr); - DISPLAY_PARAM(m_abort_after_preproc); DISPLAY_PARAM(m_model); DISPLAY_PARAM(m_model_compact); @@ -151,7 +150,6 @@ void smt_params::display(std::ostream & out) const { DISPLAY_PARAM(m_progress_sampling_freq); - DISPLAY_PARAM(m_display_installed_theories); DISPLAY_PARAM(m_core_validate); DISPLAY_PARAM(m_preprocess); diff --git a/src/smt/params/smt_params.h b/src/smt/params/smt_params.h index 9462ebb0c..45f287f4f 100644 --- a/src/smt/params/smt_params.h +++ b/src/smt/params/smt_params.h @@ -181,7 +181,6 @@ struct smt_params : public preprocessor_params, bool m_profile_res_sub; bool m_display_bool_var2expr; bool m_display_ll_bool_var2expr; - bool m_abort_after_preproc; // ----------------------------------- // @@ -205,7 +204,6 @@ struct smt_params : public preprocessor_params, // Debugging goodies // // ----------------------------------- - bool m_display_installed_theories; bool m_core_validate; // ----------------------------------- @@ -292,13 +290,11 @@ struct smt_params : public preprocessor_params, m_profile_res_sub(false), m_display_bool_var2expr(false), m_display_ll_bool_var2expr(false), - m_abort_after_preproc(false), m_model(true), m_model_compact(false), m_model_on_timeout(false), m_model_on_final_check(false), m_progress_sampling_freq(0), - m_display_installed_theories(false), m_core_validate(false), m_preprocess(true), // temporary hack for disabling all preprocessing.. m_user_theory_preprocess_axioms(false), diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index da63437f3..de90df979 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1091,10 +1091,9 @@ namespace smt { tout << mk_ll_pp(r2->get_owner(), m_manager) << "\n"; ); -#ifdef Z3DEBUG - push_trail(push_back_trail(m_diseq_vector)); - m_diseq_vector.push_back(enode_pair(n1, n2)); -#endif + DEBUG_CODE( + push_trail(push_back_trail(m_diseq_vector)); + m_diseq_vector.push_back(enode_pair(n1, n2));); if (r1 == r2) { TRACE("add_diseq_inconsistent", tout << "add_diseq #" << n1->get_owner_id() << " #" << n2->get_owner_id() << " inconsistency, scope_lvl: " << m_scope_lvl << "\n";); @@ -1299,7 +1298,7 @@ namespace smt { enode * tmp = m_tmp_enode.set(f, num_args, args); enode * r = m_cg_table.find(tmp); #ifdef Z3DEBUG - if (r != 0) { + if (r != nullptr) { SASSERT(r->get_owner()->get_decl() == f); SASSERT(r->get_num_args() == num_args); if (r->is_commutative()) { @@ -1592,9 +1591,7 @@ namespace smt { } } TRACE("propagate_relevancy", tout << "marking as relevant:\n" << mk_bounded_pp(n, m_manager) << " " << m_scope_lvl << "\n";); -#ifndef SMTCOMP m_case_split_queue->relevant_eh(n); -#endif if (is_app(n)) { if (e_internalized(n)) { @@ -1662,10 +1659,9 @@ namespace smt { theory * th = get_theory(curr.m_th_id); SASSERT(th); th->new_eq_eh(curr.m_lhs, curr.m_rhs); -#ifdef Z3DEBUG - push_trail(push_back_trail(m_propagated_th_eqs)); - m_propagated_th_eqs.push_back(curr); -#endif + DEBUG_CODE( + push_trail(push_back_trail(m_propagated_th_eqs)); + m_propagated_th_eqs.push_back(curr);); } m_th_eq_propagation_queue.reset(); } @@ -1676,10 +1672,9 @@ namespace smt { theory * th = get_theory(curr.m_th_id); SASSERT(th); th->new_diseq_eh(curr.m_lhs, curr.m_rhs); -#ifdef Z3DEBUG - push_trail(push_back_trail(m_propagated_th_diseqs)); - m_propagated_th_diseqs.push_back(curr); -#endif + DEBUG_CODE( + push_trail(push_back_trail(m_propagated_th_diseqs)); + m_propagated_th_diseqs.push_back(curr);); } m_th_diseq_propagation_queue.reset(); } @@ -3407,15 +3402,6 @@ namespace smt { return; m_setup(get_config_mode(use_static_features)); setup_components(); -#ifndef _EXTERNAL_RELEASE - if (m_fparams.m_display_installed_theories) { - std::cout << "(theories"; - for (theory* th : m_theory_set) { - std::cout << " " << th->get_name(); - } - std::cout << ")" << std::endl; - } -#endif } void context::setup_components() { @@ -3542,11 +3528,6 @@ namespace smt { lbool context::search() { -#ifndef _EXTERNAL_RELEASE - if (m_fparams.m_abort_after_preproc) { - exit(1); - } -#endif if (m_asserted_formulas.inconsistent()) return l_false; if (inconsistent()) {