projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 80b14c0) | patch
Solver state for theory of strings (#3181)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 16 Oct 2019 23:44:17 +0000 (18:44 -0500)
committerAndres Noetzli <andres.noetzli@gmail.com>
Wed, 16 Oct 2019 23:44:17 +0000 (16:44 -0700)
commit207245fef36ccad1281fefe9d3f3403cd4f6d15b
treeaa364b8701f01cb9e30afb8b85c615fae0ee6f40tree
parent80b14c0965678fb91467de287b00a9a1d8a39be5commit | diff
Solver state for theory of strings (#3181)

This refactors the theory of strings to use a solver state object, which manages state information regarding assertions.

It also deletes some unused/undefined functions in theory_strings.h.

There are no major changes to the behavior of the code or its documentation in this PR.

This is work towards #1881.
src/CMakeLists.txt diff | blob | history
src/theory/strings/inference_manager.cpp diff | blob | history
src/theory/strings/inference_manager.h diff | blob | history
src/theory/strings/regexp_solver.cpp diff | blob | history
src/theory/strings/regexp_solver.h diff | blob | history
src/theory/strings/solver_state.cpp [new file with mode: 0644] blob
src/theory/strings/solver_state.h [new file with mode: 0644] blob
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/strings/theory_strings.h diff | blob | history
src/theory/strings/theory_strings_utils.cpp diff | blob | history
src/theory/strings/theory_strings_utils.h diff | blob | history