projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c69b57e) | patch
Implement model construction for the array extension of sequences (#7815)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 17 Dec 2021 14:27:26 +0000 (08:27 -0600)
committerGitHub <noreply@github.com>
Fri, 17 Dec 2021 14:27:26 +0000 (14:27 +0000)
commit0adba8bf8e9769da251bee670fb9b8dde4012927
tree4ab4885c86f3057f8bac0c63b24143f3460b74f3tree
parentc69b57edf5ed63b5d6ad65e5ab7936a6e830099acommit | diff
Implement model construction for the array extension of sequences (#7815)

The array solver is still not usable, the only remaining changes from seqArray are to connect the array solver to the strings theory solver via the strategy + the regressions.
src/theory/strings/core_solver.cpp diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/strings/theory_strings.h diff | blob | history
src/theory/theory_model.cpp diff | blob | history
src/theory/theory_model_builder.cpp diff | blob | history