projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a86b617) | patch
[Sequences/Array Solver] Minor refactoring (#7843)
authorAndres Noetzli <andres.noetzli@gmail.com>
Mon, 20 Dec 2021 14:41:06 +0000 (06:41 -0800)
committerGitHub <noreply@github.com>
Mon, 20 Dec 2021 14:41:06 +0000 (14:41 +0000)
commit4120c564c2ac0d6b80a1764f1d191c8993897bc7
treeb4536691b9d727a8b9ac03ec013d038f57cd5ba2tree
parenta86b6177a0311d5de8ab1439890db84b290a66bdcommit | diff
[Sequences/Array Solver] Minor refactoring (#7843)

This commit performs a minor refactoring of our array core solver. It
adds more comments and avoids sending the
STRINGS_ARRAY_NTH_TERM_FROM_UPDATE lemma more than once in a given
user context.
src/theory/strings/array_core_solver.cpp diff | blob | history
src/theory/strings/array_core_solver.h diff | blob | history