mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

fix #6808

Browse source 
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.
This commit is contained in:
Nikolaj Bjorner 2023-07-13 10:47:55 -07:00
parent d0d434e4f1
commit 08599177d0
5 changed files with 23 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/sat/smt/bv_solver.cpp
View file

@ -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<int>(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);

1
src/smt/params/smt_params_helper.pyg
View file

@ -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'),

2
src/smt/params/theory_bv_params.cpp
View file

@ -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);

1
src/smt/params/theory_bv_params.h
View file

@ -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;

51
src/smt/theory_bv.cpp
View file

@ -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";);