From 4527a99f64dde0ca650e285e91a6b173de30a2f8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 8 Nov 2019 11:05:49 +0100
Subject: [PATCH] fix #2675
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/theory_seq.cpp | 63 ++++++++++++++++++++++++++++++++++++++++--
src/smt/theory_seq.h | 3 ++
2 files changed, 63 insertions(+), 3 deletions(-)
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 2dfdb16c1..68aea6cdd 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -405,6 +405,11 @@ final_check_status theory_seq::final_check_eh() {
TRACEFIN("extensionality");
return FC_CONTINUE;
}
+ if (branch_nqs()) {
+ ++m_stats.m_branch_nqs;
+ TRACEFIN("branch_ne");
+ return FC_CONTINUE;
+ }
if (is_solved()) {
//scoped_enable_trace _se;
TRACEFIN("is_solved");
@@ -3177,6 +3182,56 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) {
}
+bool theory_seq::branch_nqs() {
+ context & ctx = get_context();
+ if (m_nqs.empty()) {
+ return false;
+ }
+ ne n = m_nqs[0];
+ branch_nq(n);
+ if (m_nqs.size() > 1) {
+ ne n2 = m_nqs[m_nqs.size() - 1];
+ m_nqs.set(0, n2);
+ }
+ m_nqs.pop_back();
+ return true;
+}
+
+void theory_seq::branch_nq(ne const& n) {
+ context& ctx = get_context();
+ literal_vector lits;
+ enode_pair_vector eqs;
+ VERIFY(linearize(n.dep(), eqs, lits));
+ for (literal & l : lits) {
+ l.neg();
+ }
+ for (enode_pair const& p : eqs) {
+ lits.push_back(mk_eq(p.first->get_owner(), p.second->get_owner(), false));
+ }
+ literal eq_len = mk_eq(mk_len(n.l()), mk_len(n.r()), false);
+ literal len_gt = mk_literal(m_autil.mk_ge(mk_len(n.l()), m_autil.mk_int(1)));
+ expr_ref h1(m), t1(m), h2(m), t2(m);
+ mk_decompose(n.l(), h1, t1);
+ mk_decompose(n.r(), h2, t2);
+ ctx.mark_as_relevant(eq_len);
+ ctx.mark_as_relevant(len_gt);
+ lits.push_back(~eq_len);
+
+ // Deps => |l| != |r| or |l| > 0
+ lits.push_back(len_gt);
+ literal_vector lits1(lits);
+ lits.pop_back();
+
+ // Deps => |l| != |r| or h1 != h2 or t1 != t2
+ lits.push_back(~mk_eq(h1, h2, false));
+ lits.push_back(~mk_eq(t1, t2, false));
+ literal_vector lits2(lits);
+ lits.pop_back();
+
+ ctx.mk_th_axiom(get_id(), lits1.size(), lits1.c_ptr());
+ ctx.mk_th_axiom(get_id(), lits2.size(), lits2.c_ptr());
+}
+
bool theory_seq::solve_nqs(unsigned i) {
context & ctx = get_context();
for (; !ctx.inconsistent() && i < m_nqs.size(); ++i) {
@@ -3347,8 +3402,9 @@ bool theory_seq::solve_ne(unsigned idx) {
}
else {
m_nqs.push_back(ne(n.l(), n.r(), new_ls, new_rs, new_lits, new_deps));
+ TRACE("seq", display_disequation(tout << "updated: ", m_nqs[m_nqs.size()-1]););
}
- }
+ }
return updated;
}
@@ -3997,10 +4053,10 @@ std::ostream& theory_seq::display_deps(std::ostream& out, literal_vector const&
else {
expr* e = ctx.bool_var2expr(l.var());
if (l.sign()) {
- out << "(not " << mk_bounded_pp(e, m) << ")";
+ out << " (not " << mk_bounded_pp(e, m) << ")";
}
else {
- out << mk_bounded_pp(e, m);
+ out << " " << mk_bounded_pp(e, m);
}
}
out << "\n";
@@ -4023,6 +4079,7 @@ void theory_seq::collect_statistics(::statistics & st) const {
st.update("seq branch", m_stats.m_branch_variable);
st.update("seq solve !=", m_stats.m_solve_nqs);
st.update("seq solve =", m_stats.m_solve_eqs);
+ st.update("seq branch !=", m_stats.m_branch_nqs);
st.update("seq add axiom", m_stats.m_add_axiom);
st.update("seq extensionality", m_stats.m_extensionality);
st.update("seq fixed length", m_stats.m_fixed_length);
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 2a2abd8f6..1cdc33694 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -332,6 +332,7 @@ namespace smt {
unsigned m_propagate_automata;
unsigned m_check_length_coherence;
unsigned m_branch_variable;
+ unsigned m_branch_nqs;
unsigned m_solve_nqs;
unsigned m_solve_eqs;
unsigned m_add_axiom;
@@ -512,6 +513,8 @@ namespace smt {
bool solve_nqs(unsigned i);
bool solve_ne(unsigned i);
bool solve_nc(unsigned i);
+ bool branch_nqs();
+ void branch_nq(ne const& n);
struct cell {
cell* m_parent;