Fix `Nth-Update` rule, add `Update-Bound` rule (#7968)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 20 Jan 2022 23:03:02 +0000 (15:03 -0800)
committerGitHub <noreply@github.com>
Thu, 20 Jan 2022 23:03:02 +0000 (23:03 +0000)
commita22355748973e5e567e9543a7f036a23d616bbbd
treede111de0b815513c128a8d34c3d36e285a927d0d
parent66d8d5a6755170e91bb272b2a7dbf78e53b2eb9e
Fix `Nth-Update` rule, add `Update-Bound` rule (#7968)

This commit updates the inferences in the sequences array solver to more
closely resemble the current rules in the paper. Concretely, it adds an
implementation of the `Update-Bound` rule and it fixes the `Nth-Update`
rule to take into account all three branches in the conclusion of the
rule.

Co-authored-by: Yoni Zohar <yoni206@gmail.com>
src/theory/inference_id.cpp
src/theory/inference_id.h
src/theory/strings/array_core_solver.cpp
test/regress/CMakeLists.txt
test/regress/regress0/seq/array/update-word-eq.smt2
test/regress/regress0/seq/err1.smt2 [new file with mode: 0644]
test/regress/regress0/seq/nth-oob.smt2 [new file with mode: 0644]
test/regress/regress0/seq/nth-update.smt2 [new file with mode: 0644]
test/regress/regress0/seq/update-eq.smt2 [new file with mode: 0644]