Get rid of Z3 string theory in the String wrapper

[dtim]

Description

Currently many string operations are modeled using Z3 string theory. There are several major drawbacks of this approach:

• SAT checks may take too long, and the solver behavior is flaky;
• many string operations are not supported, so corresponding String methods have to be implemented with executeConcretely;
• it is impossible to replace Z3 with another SMT solver.

We should get rid of Z3-based implementation of the String wrapper.

Methods that don't rely upon it will keep working. Methods that require Z3 string theory should be rewritten. Experiments show that the only group of methods that require Z3 string theory, are toString() conversions for Byte, Short, Integer, and Double, that should be replaced with the straightforward Java implementation.

Expected behavior

Symbolic analysis of strings should work as before, but no string-related Z3 expression should be generated.

Environment

This change does not depend on any specific environment.

Potential alternatives

As we want to have the opportunity to replace Z3 with another SMT solver, there is no alternative to removing Z3-specific parts from String wrapper implementation.

Context

String wrapper should be completely rewritten to enable effective symbolic operations on strings.

TODO: create a separate proposal and a design document.