fixing issue #4651

[veanes]

Added rewrite rules to lift to_re from within ite-expressions.
Also disabled lift_ites_throttled that seems to cause performance issues (in this example 100x slowdown).
Updated also pp of regexes to indicate where a regex is not fixed.
The underlying issue of #4651 is fixed or at least does not show up with this example.

[NikolajBjorner]

this will create a perf regression for strings, where lifting ites is very useful.
So it could look at the type of the expression. If it is a seq, then lift, otherwise don't.
That can be accomplished inside lift_ites_throttled, not here.

[NikolajBjorner]

move { to after ), not on a new line as in C#

[NikolajBjorner]

this makes a "long distance" assumption about values.
Better to not make such assumptions deeply buried in code and have the routine more self-contained.
You can simply check for is_concat(s) regardless of whether it is a value, and you can check for unit, and empty as 3 separate cases. The is_value check only filters cases of concatenations of non-constants and constants, where the conventions in this routine are not uniform: in the default case you use (to_re ...), in the non-default case it doesn't use (to_re ..) around the expression.

So instead

if (is_empty(s))
    out << "();
else if is_unit(s))
      seq_unit(s, s);
else if (is_concat(s)) 
    for (expr* e : concats(s))
          concat_helper_sec(out, s);
else out << "(to_re " << pp(s) << ")";

[veanes]

I updated it similarly, but essentially I wanted to distinguish between 'A' vs uninterpreted const A, the latter is now printed as {A}
Another thing I wanted to distinguish is (in some cases) pp(to_re S) from pp(S), but in most cases the distiction is not needed or desired and just adds noise, so I did not do it in the end. e.g. pp(tore("ab") ++ tore("cd") ) and
pp(tore("ab" ++ "cd")) are printed the same way

[NikolajBjorner]

this is too low level, we have higher level checks, or add them if they don't already exist:

• u.is_re(f->get_range())
• u.is_seq(f->get_range())
• a.is_arith(m().get_sort(ite))

[veanes]

While the branch is named fix4651, it only partially addresses use of nonground regexes in the related issue. This is work in progress. But the PR does fix one crucial bug where state ids were off by one in lookup table, luckily this lookup table was not used in core algorithms (yet). Discovered this with the new feature I added to dgml generation that also generates a 'Value' field to each state that is the pretty printed regex corresponding to the state with the given label and is shown as tool-tip in VS when hovering over the node. I found it very useful for debugging. I added a callback method to the state_graph that asks for the string value of a state, so the state_graph is still not dependent and knows nothing of regexes, it can be sued for anu other graphs.