mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

added comments to explain #5781

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-21 01:40:31 +01:00
parent b1ff4bc24a
commit 17280846f8
1 changed files with 12 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/smt/seq_eq_solver.cpp
View file

@ -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);