From 4392c03b57bb9c46afb055b1b25e73563dc8f813 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 30 Jul 2020 22:10:33 -0700 Subject: [PATCH] better behavior on disequality and branch selection Signed-off-by: Nikolaj Bjorner --- src/smt/theory_seq.cpp | 7 ++++++- src/smt/theory_seq.h | 3 ++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 19a338f5bad..c6fa3c6b9b4 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -3101,7 +3101,12 @@ void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { } dependency* dep = m_dm.mk_leaf(assumption(~lit)); - m_nqs.push_back(ne(e1, e2, dep)); + expr_ref len1(m_util.str.mk_length(e1), m); + expr_ref len2(m_util.str.mk_length(e2), m); + m_rewrite(len1); + m_rewrite(len2); + literal eqlen = mk_eq(len1, len2, false); + m_nqs.push_back(ne(e1, e2, eqlen, dep)); if (ctx.get_assignment(lit) != l_undef) { solve_nqs(m_nqs.size() - 1); } diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index f0e5e06f2ca..1c62ee0e8d2 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -178,11 +178,12 @@ namespace smt { literal_vector m_lits; dependency* m_dep; public: - ne(expr_ref const& l, expr_ref const& r, dependency* dep): + ne(expr_ref const& l, expr_ref const& r, literal eqlen, dependency* dep): m_l(l), m_r(r), m_dep(dep) { expr_ref_vector ls(l.get_manager()); ls.push_back(l); expr_ref_vector rs(r.get_manager()); rs.push_back(r); m_eqs.push_back(std::make_pair(ls, rs)); + m_lits.push_back(eqlen); } ne(expr_ref const& _l, expr_ref const& _r, vector const& eqs, literal_vector const& lits, dependency* dep):