mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

fix #4414

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-05-20 14:28:41 -07:00
parent f2d3160181
commit 1729232254
3 changed files with 9 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/seq_unicode.cpp
View file

@ -71,7 +71,7 @@ namespace smt {
} }
// != on characters // != on characters
void seq_unicode::new_diseq_eh(theory_var v1, theory_var v2) { void seq_unicode::new_diseq_eh(theory_var v1, theory_var v2) {
adapt_eq(v1, v2); adapt_eq(v1, v2);
} }
@ -134,6 +134,7 @@ namespace smt {
} }
void seq_unicode::propagate() { void seq_unicode::propagate() {
return;
ctx().push_trail(value_trail<smt::context, unsigned>(m_qhead)); ctx().push_trail(value_trail<smt::context, unsigned>(m_qhead));
for (; m_qhead < m_asserted_edges.size() && !ctx().inconsistent(); ++m_qhead) { for (; m_qhead < m_asserted_edges.size() && !ctx().inconsistent(); ++m_qhead) {
propagate(m_asserted_edges[m_qhead]); propagate(m_asserted_edges[m_qhead]);
@ -141,6 +142,7 @@ namespace smt {
} }
void seq_unicode::propagate(edge_id edge) { void seq_unicode::propagate(edge_id edge) {
return;
if (dl.enable_edge(edge)) if (dl.enable_edge(edge))
return; return;
dl.traverse_neg_cycle2(false, m_nc_functor); dl.traverse_neg_cycle2(false, m_nc_functor);

2
src/smt/seq_unicode.h
View file

@ -70,12 +70,12 @@ namespace smt {
var_value_hash m_var_value_hash; var_value_hash m_var_value_hash;
var_value_eq m_var_value_eq; var_value_eq m_var_value_eq;
var_value_table m_var_value_table; var_value_table m_var_value_table;
std::function<void(literal, literal, literal)> m_add_axiom;
context& ctx() const { return th.get_context(); } context& ctx() const { return th.get_context(); }
void propagate(edge_id edge); void propagate(edge_id edge);
std::function<void(literal, literal, literal)> m_add_axiom;
void add_axiom(literal a, literal b = null_literal, literal c = null_literal) { void add_axiom(literal a, literal b = null_literal, literal c = null_literal) {
m_add_axiom(a, b, c); m_add_axiom(a, b, c);
} }

10
src/smt/theory_seq.cpp
View file

@ -377,7 +377,7 @@ final_check_status theory_seq::final_check_eh() {
TRACEFIN("zero_length"); TRACEFIN("zero_length");
return FC_CONTINUE; return FC_CONTINUE;
} }
if (!m_unicode.final_check()) { if (false && !m_unicode.final_check()) {
return FC_CONTINUE; return FC_CONTINUE;
} }
if (get_fparams().m_split_w_len && len_based_split()) { if (get_fparams().m_split_w_len && len_based_split()) {
@ -2510,7 +2510,7 @@ void theory_seq::add_dependency(dependency*& dep, enode* a, enode* b) {
void theory_seq::propagate() { void theory_seq::propagate() {
m_unicode.propagate(); // m_unicode.propagate();
while (m_axioms_head < m_axioms.size() && !ctx.inconsistent()) { while (m_axioms_head < m_axioms.size() && !ctx.inconsistent()) {
expr_ref e(m); expr_ref e(m);
e = m_axioms[m_axioms_head].get(); e = m_axioms[m_axioms_head].get();
@ -3072,7 +3072,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
else if (m_util.str.is_nth_i(e) || m_util.str.is_nth_u(e)) { else if (m_util.str.is_nth_i(e) || m_util.str.is_nth_u(e)) {
// no-op // no-op
} }
else if (m_util.is_char_le(e, e1, e2)) { else if (false && m_util.is_char_le(e, e1, e2)) {
theory_var v1 = get_th_var(ctx.get_enode(e1)); theory_var v1 = get_th_var(ctx.get_enode(e1));
theory_var v2 = get_th_var(ctx.get_enode(e2)); theory_var v2 = get_th_var(ctx.get_enode(e2));
if (is_true) if (is_true)
@ -3093,7 +3093,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) {
void theory_seq::new_eq_eh(theory_var v1, theory_var v2) { void theory_seq::new_eq_eh(theory_var v1, theory_var v2) {
enode* n1 = get_enode(v1); enode* n1 = get_enode(v1);
enode* n2 = get_enode(v2); enode* n2 = get_enode(v2);
if (m_util.is_char(n1->get_owner())) { if (false && m_util.is_char(n1->get_owner())) {
m_unicode.new_eq_eh(v1, v2); m_unicode.new_eq_eh(v1, v2);
return; return;
} }
@ -3188,7 +3188,7 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) {
throw default_exception("convert regular expressions into automata"); throw default_exception("convert regular expressions into automata");
} }
} }
if (m_util.is_char(n1->get_owner())) { if (false && m_util.is_char(n1->get_owner())) {
m_unicode.new_diseq_eh(v1, v2); m_unicode.new_diseq_eh(v1, v2);
return; return;
} }