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

unsound equality propagation #5676

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-12-08 09:02:05 -08:00
parent a5bd115235
commit e45ae32685
2 changed files with 23 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/seq_axioms.cpp
View file

@ -1034,7 +1034,7 @@ namespace seq {
* Assume that r has the property that if r accepts string p * Assume that r has the property that if r accepts string p
* then r does *not* accept any suffix of p. It is conceptually easy to * then r does *not* accept any suffix of p. It is conceptually easy to
* convert a deterministic automaton for a regex to a suffix blocking acceptor * convert a deterministic automaton for a regex to a suffix blocking acceptor
* by redirecting removing outgoing edges from accepting states and redirecting them * by removing outgoing edges from accepting states and redirecting them
* to a sink. Alternative, introduce a different string membership predicate that is * to a sink. Alternative, introduce a different string membership predicate that is
* prefix sensitive. * prefix sensitive.
* *

31
src/math/lp/lp_bound_propagator.h
View file

@ -116,30 +116,43 @@ class lp_bound_propagator {
map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_val2fixed_row; map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_val2fixed_row;
bool is_fixed_row(unsigned r, unsigned & x) {
x = UINT_MAX;
const auto & row = lp().get_row(r);
for (unsigned k = 0; k < row.size(); k++) {
const auto& c = row[k];
if (column_is_fixed(c.var()))
continue;
if (x != UINT_MAX)
return false;
x = c.var();
}
return x != UINT_MAX;
}
void try_add_equation_with_internal_fixed_tables(unsigned r1, vertex const* v) { void try_add_equation_with_internal_fixed_tables(unsigned r1) {
SASSERT(m_fixed_vertex); SASSERT(m_fixed_vertex);
if (v != m_root) unsigned v1, v2;
if (!is_fixed_row(r1, v1))
return; return;
unsigned v1 = v->column();
unsigned r2 = UINT_MAX; unsigned r2 = UINT_MAX;
if (!m_val2fixed_row.find(val(v1), r2) || r2 >= lp().row_count()) { if (!m_val2fixed_row.find(val(v1), r2) || r2 >= lp().row_count()) {
m_val2fixed_row.insert(val(v1), r1); m_val2fixed_row.insert(val(v1), r1);
return; return;
} }
unsigned v2, v3; if (!is_fixed_row(r2, v2) || val(v1) != val(v2) || is_int(v1) != is_int(v2)) {
int polarity;
if (!is_tree_offset_row(r2, v2, v3, polarity) || !not_set(v3) ||
is_int(v1) != is_int(v2) || val(v1) != val(v2)) {
m_val2fixed_row.insert(val(v1), r1); m_val2fixed_row.insert(val(v1), r1);
return; return;
} }
if (v1 == v2) if (v1 == v2)
return; return;
TRACE("eq", tout << v1 << " = " << v2 << "\n");
explanation ex; explanation ex;
explain_fixed_in_row(r1, ex); explain_fixed_in_row(r1, ex);
explain_fixed_in_row(r2, ex); explain_fixed_in_row(r2, ex);
TRACE("eq", print_row(tout, r1); print_row(tout, r2); tout << v1 << " == " << v2 << " = " << val(v1) << "\n");
add_eq_on_columns(ex, v1, v2, true); add_eq_on_columns(ex, v1, v2, true);
} }
@ -148,7 +161,7 @@ class lp_bound_propagator {
unsigned v_j = v->column(); unsigned v_j = v->column();
unsigned j = null_lpvar; unsigned j = null_lpvar;
if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j)) { if (!lp().find_in_fixed_tables(val(v_j), is_int(v_j), j)) {
try_add_equation_with_internal_fixed_tables(row_index, v); try_add_equation_with_internal_fixed_tables(row_index);
return; return;
} }