diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-29 10:39:50 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-29 15:39:50 +0000 |
| commit | a6e09da79c31d9f7cf783f17072239a44e538162 (patch) | |
| tree | 577121352f4ed2a27bfb6297c50055c5ccfca9d2 /src/CMakeLists.txt | |
| parent | c9b3f13981ce88bc081e49213b15da6999f4aea5 (diff) | |
Add the strings array solver (#7232)
This adds the arrays subsolver utility. It does not yet connect it down to the core array solver, or up to TheoryStrings.
It adds implementation of its lemma schemas for processing nth/update over concat.
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 13ab74d4b..6c03db7e7 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1051,6 +1051,8 @@ libcvc5_add_sources( theory/smt_engine_subsolver.h theory/sort_inference.cpp theory/sort_inference.h + theory/strings/array_solver.cpp + theory/strings/array_solver.h theory/strings/arith_entail.cpp theory/strings/arith_entail.h theory/strings/base_solver.cpp |