projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ce3a462) | patch
Connecting the core array solver in strings (#7800)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 14 Dec 2021 19:35:09 +0000 (13:35 -0600)
committerGitHub <noreply@github.com>
Tue, 14 Dec 2021 19:35:09 +0000 (19:35 +0000)
commiteffb0d47ba5bfaebae17dcd06153489dccd90eff
treeca323ec7815ba2f285355e8289eae33b3f892276tree
parentce3a462918ac62c10b14d6a23be7e57db0ee984ecommit | diff
Connecting the core array solver in strings (#7800)

This PR takes most of the remaining changes from the seqArray branch apart from the extension to model construction.

Notably it connects the core array solver to the array solver in strings.
src/expr/skolem_manager.cpp diff | blob | history
src/expr/skolem_manager.h diff | blob | history
src/smt/proof_post_processor.cpp diff | blob | history
src/theory/strings/array_core_solver.cpp diff | blob | history
src/theory/strings/array_core_solver.h diff | blob | history
src/theory/strings/array_solver.cpp diff | blob | history
src/theory/strings/array_solver.h diff | blob | history
src/theory/strings/rewrites.cpp diff | blob | history
src/theory/strings/rewrites.h diff | blob | history
src/theory/strings/sequences_rewriter.cpp diff | blob | history