Split sequences rewriter (#4194)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 3 Apr 2020 14:43:12 +0000 (09:43 -0500)
committerGitHub <noreply@github.com>
Fri, 3 Apr 2020 14:43:12 +0000 (09:43 -0500)
commitd91b52085d7e3bbda65117c0cd88433aed383aff
tree5ed2055704066d28a3247a82030ed44bfeda4a57
parente24e6f3620996ee9e5010d30fefc51247cc55fdc
Split sequences rewriter (#4194)

This is in preparation for making the strings rewriter configurable for stats.

This moves all utility functions from SequencesRewriter to a proper place. This includes three new groupings of utility functions: those involving arithmetic entailments, those involving string entailments, those involving regular expression entailments. Here, "entailments" loosely means any question regarding a (set of) terms or formulas.

No major code changes. Added some missing documentation and lightly cleaned a few blocks of code in cpp.
21 files changed:
src/CMakeLists.txt
src/theory/strings/arith_entail.cpp [new file with mode: 0644]
src/theory/strings/arith_entail.h [new file with mode: 0644]
src/theory/strings/core_solver.cpp
src/theory/strings/regexp_elim.cpp
src/theory/strings/regexp_entail.cpp [new file with mode: 0644]
src/theory/strings/regexp_entail.h [new file with mode: 0644]
src/theory/strings/regexp_operation.cpp
src/theory/strings/regexp_operation.h
src/theory/strings/regexp_solver.cpp
src/theory/strings/sequences_rewriter.cpp
src/theory/strings/sequences_rewriter.h
src/theory/strings/skolem_cache.cpp
src/theory/strings/strings_entail.cpp [new file with mode: 0644]
src/theory/strings/strings_entail.h [new file with mode: 0644]
src/theory/strings/theory_strings_preprocess.cpp
src/theory/strings/theory_strings_utils.cpp
src/theory/strings/theory_strings_utils.h
src/theory/strings/word.cpp
src/theory/strings/word.h
test/unit/theory/sequences_rewriter_white.h