Add helper to detect length one string terms (#2654)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 19 Oct 2018 15:14:22 +0000 (08:14 -0700)
committerGitHub <noreply@github.com>
Fri, 19 Oct 2018 15:14:22 +0000 (08:14 -0700)
commitc116c6c1ec757fe51f2b874e750ad8281baea103
treecd5c1fc6deaff07d784705dae933a7abd01b546b
parent64dcc865f8aae4fd1591bfec9ee117b360e9f9b3
Add helper to detect length one string terms (#2654)

This commit introduces a helper function to detect string terms that
have exactly/at most length one. This is useful for a lot of rewrites
because strings of at most length one are guaranteed to not overlap
multiple components in a concatenation, which allows for more aggressive
rewriting.

This commit has been tested with --sygus-rr-synth-check for >1h on the
string term grammar.
src/theory/strings/theory_strings_rewriter.cpp
src/theory/strings/theory_strings_rewriter.h
test/unit/theory/theory_strings_rewriter_white.h