From 17280846f8978ee8d4ef43882193f2b4bb0551fb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 21 Jan 2022 01:40:31 +0100 Subject: [PATCH] added comments to explain #5781 --- src/smt/seq_eq_solver.cpp | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp index a54ebdac9..8eb3e0c98 100644 --- a/src/smt/seq_eq_solver.cpp +++ b/src/smt/seq_eq_solver.cpp @@ -375,6 +375,15 @@ bool theory_seq::split_lengths(dependency* dep, SASSERT(X != Y); // |b| < |X| <= |b| + |Y| => x = bY1, Y = Y1Y2 + // at this point |b| = lenB - |Y| which is less than |X| + // given how bs is constructed: + // bs is constructed as a vector of strings with length >= |X| + // but when the last element it removed the length is < |X| + // We also have |X| <= |b| + |Y|, also by how bs is constructed. + // Therefore the antecedent is true in the current model. + // It could be the antecendet is not justified, so we create + // literals to justify the antecedent and ensure they are relevant. + // If the literals are relevant and assigned they should be true. expr_ref lenXE = mk_len(X); expr_ref lenYE = mk_len(Y); expr_ref lenb = mk_len(b); @@ -383,7 +392,9 @@ bool theory_seq::split_lengths(dependency* dep, literal_vector lits; lits.push_back(lit1); lits.push_back(lit2); - + + SASSERT(!ctx.is_relevant(lit1) || ctx.get_assignment(lit1) == l_true); + SASSERT(!ctx.is_relevant(lit2) || ctx.get_assignment(lit2) == l_true); if (ctx.get_assignment(lit1) != l_true || ctx.get_assignment(lit2) != l_true) { ctx.mark_as_relevant(lit1);