Introduce best content heuristic for strings (#4382)
authorAndres Noetzli <andres.noetzli@gmail.com>
Thu, 23 Apr 2020 12:58:00 +0000 (05:58 -0700)
committerGitHub <noreply@github.com>
Thu, 23 Apr 2020 12:58:00 +0000 (07:58 -0500)
commit1cacd328b60713e21af6836c65007ebe3bfffa81
tree93cd02a820e60949ba1e9ef2e12286ee7600288f
parent855143cfa1e4cf38f67ff99eba5d59e5a2786120
Introduce best content heuristic for strings (#4382)

* Introduce best content heuristic for strings

This commit introduces a "best content heuristic" to perform
context-dependent simplifications. The high-level idea is that for each
equivalence class for strings, we compute a representation that is a
string concatentation of constants and other string terms. For this
representation, we try to get as many letters in the string constants as
we can (i.e. the best approximation of the content). This "best content"
representation is then used by `EXTF_EVAL` to perform simplifications.

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
src/theory/strings/base_solver.cpp
src/theory/strings/base_solver.h
src/theory/strings/extf_solver.cpp