From 08599177d016812ec1f621ce4562cdd2910d1ec6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 13 Jul 2023 10:47:55 -0700 Subject: [PATCH] fix #6808 remove bv_eq_axioms as an external option to toggle. Diseqalities have to be enforced for extensionality. There are no internal code paths where the option is set to false. --- src/sat/smt/bv_solver.cpp | 8 +---- src/smt/params/smt_params_helper.pyg | 1 - src/smt/params/theory_bv_params.cpp | 2 -- src/smt/params/theory_bv_params.h | 1 - src/smt/theory_bv.cpp | 51 ++++++++++++---------------- 5 files changed, 23 insertions(+), 40 deletions(-) diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp index f76e5ab70..a3aa5f7b3 100644 --- a/src/sat/smt/bv_solver.cpp +++ b/src/sat/smt/bv_solver.cpp @@ -96,8 +96,6 @@ namespace bv { } void solver::add_fixed_eq(theory_var v1, theory_var v2) { - if (!get_config().m_bv_eq_axioms) - return; m_ackerman.used_eq_eh(v1, v2); } @@ -149,8 +147,6 @@ namespace bv { *\brief v[idx] = ~v'[idx], then v /= v' is a theory axiom. */ void solver::find_new_diseq_axioms(atom& a, theory_var v, unsigned idx) { - if (!get_config().m_bv_eq_axioms) - return; literal l = m_bits[v][idx]; l.neg(); for (auto vp : a) { @@ -271,7 +267,7 @@ namespace bv { ++num_undef; undef_idx = -static_cast(i + 1); } - if (num_undef > 1 && get_config().m_bv_eq_axioms) + if (num_undef > 1) return; } if (num_undef == 0) @@ -293,8 +289,6 @@ namespace bv { ++m_stats.m_num_ne2bit; s().assign(consequent, mk_ne2bit_justification(undef_idx, v1, v2, consequent, antecedent)); } - else if (!get_config().m_bv_eq_axioms) - ; else if (s().at_search_lvl()) { force_push(); assert_ackerman(v1, v2); diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 4b4a453c8..7bc9bc3fa 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -53,7 +53,6 @@ def_module_params(module_name='smt', ('bv.enable_int2bv', BOOL, True, 'enable support for int2bv and bv2int operators'), ('bv.watch_diseq', BOOL, False, 'use watch lists instead of eager axioms for bit-vectors'), ('bv.delay', BOOL, False, 'delay internalize expensive bit-vector operations'), - ('bv.eq_axioms', BOOL, True, 'enable redundant equality axioms for bit-vectors'), ('bv.size_reduce', BOOL, False, 'pre-processing; turn assertions that set the upper bits of a bit-vector to constants into a substitution that replaces the bit-vector with constant bits. Useful for minimizing circuits as many input bits to circuits are constant'), ('arith.random_initial_value', BOOL, False, 'use random initial values in the simplex-based procedure for linear arithmetic'), ('arith.solver', UINT, 6, 'arithmetic solver: 0 - no solver, 1 - bellman-ford based solver (diff. logic only), 2 - simplex based solver, 3 - floyd-warshall based solver (diff. logic only) and no theory combination 4 - utvpi, 5 - infinitary lra, 6 - lra solver'), diff --git a/src/smt/params/theory_bv_params.cpp b/src/smt/params/theory_bv_params.cpp index 09fa4513f..734a983fb 100644 --- a/src/smt/params/theory_bv_params.cpp +++ b/src/smt/params/theory_bv_params.cpp @@ -27,7 +27,6 @@ void theory_bv_params::updt_params(params_ref const & _p) { m_bv_reflect = p.bv_reflect(); m_bv_enable_int2bv2int = p.bv_enable_int2bv(); m_bv_delay = p.bv_delay(); - m_bv_eq_axioms = p.bv_eq_axioms(); m_bv_size_reduce = p.bv_size_reduce(); } @@ -38,7 +37,6 @@ void theory_bv_params::display(std::ostream & out) const { DISPLAY_PARAM(m_hi_div0); DISPLAY_PARAM(m_bv_reflect); DISPLAY_PARAM(m_bv_lazy_le); - DISPLAY_PARAM(m_bv_eq_axioms); DISPLAY_PARAM(m_bv_cc); DISPLAY_PARAM(m_bv_blast_max_size); DISPLAY_PARAM(m_bv_enable_int2bv2int); diff --git a/src/smt/params/theory_bv_params.h b/src/smt/params/theory_bv_params.h index e83b0b5db..523459f09 100644 --- a/src/smt/params/theory_bv_params.h +++ b/src/smt/params/theory_bv_params.h @@ -31,7 +31,6 @@ struct theory_bv_params { bool m_bv_reflect = true; bool m_bv_lazy_le = false; bool m_bv_cc = false; - bool m_bv_eq_axioms = true; unsigned m_bv_blast_max_size = INT_MAX; bool m_bv_enable_int2bv2int = true; bool m_bv_watch_diseq = false; diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index a44e1a1aa..55d3a1d62 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -429,12 +429,9 @@ namespace smt { }; void theory_bv::add_fixed_eq(theory_var v1, theory_var v2) { - if (!params().m_bv_eq_axioms) - return; - if (v1 > v2) { + if (v1 > v2) std::swap(v1, v2); - } unsigned act = m_eq_activity[hash_u_u(v1, v2) & 0xFF]++; if ((act & 0xFF) != 0xFF) { @@ -1163,8 +1160,6 @@ namespace smt { } void theory_bv::expand_diseq(theory_var v1, theory_var v2) { - if (!params().m_bv_eq_axioms) - return; SASSERT(get_bv_size(v1) == get_bv_size(v2)); if (v1 > v2) { @@ -1331,29 +1326,27 @@ namespace smt { } else { ctx.assign(consequent, mk_bit_eq_justification(v1, v2, consequent, antecedent)); - if (params().m_bv_eq_axioms) { - literal_vector lits; - lits.push_back(~consequent); - lits.push_back(antecedent); - literal eq = mk_eq(get_expr(v1), get_expr(v2), false); - lits.push_back(~eq); - // - // Issue #3035: - // merge_eh invokes assign_bit, which updates the propagation queue and includes the - // theory axiom for the propagated equality. When relevancy is non-zero, propagation may get - // lost on backtracking because the propagation queue is reset on conflicts. - // An alternative approach is to ensure the propagation queue is chronological with - // backtracking scopes (ie., it doesn't get reset, but shrunk to a previous level, and similar - // with a qhead indicator. - // - ctx.mark_as_relevant(lits[0]); - ctx.mark_as_relevant(lits[1]); - ctx.mark_as_relevant(lits[2]); - { - scoped_trace_stream _sts(*this, lits); - ctx.mk_th_axiom(get_id(), lits.size(), lits.data()); - } + literal_vector lits; + lits.push_back(~consequent); + lits.push_back(antecedent); + literal eq = mk_eq(get_expr(v1), get_expr(v2), false); + lits.push_back(~eq); + // + // Issue #3035: + // merge_eh invokes assign_bit, which updates the propagation queue and includes the + // theory axiom for the propagated equality. When relevancy is non-zero, propagation may get + // lost on backtracking because the propagation queue is reset on conflicts. + // An alternative approach is to ensure the propagation queue is chronological with + // backtracking scopes (ie., it doesn't get reset, but shrunk to a previous level, and similar + // with a qhead indicator. + // + ctx.mark_as_relevant(lits[0]); + ctx.mark_as_relevant(lits[1]); + ctx.mark_as_relevant(lits[2]); + { + scoped_trace_stream _sts(*this, lits); + ctx.mk_th_axiom(get_id(), lits.size(), lits.data()); } if (m_wpos[v2] == idx) @@ -1382,7 +1375,7 @@ namespace smt { } } } - + void theory_bv::relevant_eh(app * n) { TRACE("arith", tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_bounded_pp(n, m) << "\n";); TRACE("bv", tout << "relevant: #" << n->get_id() << " " << ctx.e_internalized(n) << ": " << mk_pp(n, m) << "\n";);