Allow String in TermCompiler

[serras]

No description provided.

[serras]

@jhoenicke I found that without this change there's no way to use a logical formula containing a constant string, not even the simplest (= x "hello").

[jhoenicke]

I think this is unsound without any String reasoning. E.g., with this change, SMTInterpol will also say that (and (= x "hello") (= x "good bye")) is satisfiable.

[serras]

I'm happy to devote some time to have this working; is there any place I could look at to bring strings to SMTInterpol?

[jhoenicke]

Writing a string solver can be quite an involved task. The whole theory is undecidable, so the first step would be to pick a decidable fragment and an algorithm for this fragment. Here is a survey on techniques of string solving: https://arxiv.org/pdf/2002.02376.pdf

If you want to work on a solver, I can help you to integrate it in SMTInterpol.