Simplify numerical expressions in SMT-LIB printers

[Halbaroth]

The modifications done in PR #970 are to risky for what we need.
This commit simplify (0 - x) to (- x)expressions printed in the SMT-LIB
format only.

[bclement-ocp]

Some high-level comments:

I don't think it is a good idea to do these transformations directly in the printer, because it can be confusing when using debug outputs — the printer should show the actual structure of the expressions. It would be better to have a separate simplify function and to call simplify before printing where we want to print a simplified expression.

I am also a bit surprised that we need all of these simplifications at the Expr level. I understand that this is for model generation, but I would expect most of these to happen while we still have semantic values (the arith theory normalization should already do all of these simplifications), prior to converting back into expressions (which I think is the direction you are going with). Can you share some insight as to why these can't be done in the "semantic value" world where these simplifications should already be available?

[Halbaroth]

Honestly, I don't think it will be a big issue. I prefer keeping a simple printing function.

[bclement-ocp]

What I am thinking is for instance we can now have duplicate entries in the UF table for (f x) where one is actually (f x) and the other is (f (+ x 0)) which I would personally find confusing while debugging and might end up losing time to. For instance the recent bugs that we had with the BV theory not adding certain terms to the UF could have been harder to debug, because it could have looked like the term was in the UF when in fact it was not (bv2nat creates terms of the form x + 0). Another issue is that currently, (+x (+ 0 0)) is still printed (+ x 0). Might not be a big deal, I just want us to be aware of these things.

Can you please answer my second question? This is a case where I don't understand why we need to do this, so it renders my approval meaningless (for instance, printing (+ x (+ 0 0)) as (+ x 0) might be an issue or not, I don't know without more context of where this code will be used). We can hop on a call if you want, I assume it has to do with some subtleties of model generation.

[Halbaroth]

I don't think this will happen in semantic values but some values produced by the optimization don't require to produce semantic values at all.

[bclement-ocp]

I don't think this will happen in semantic values but some values produced by the optimization don't require to produce semantic values at all.

Not sure I understand that; the values produced by the optimization procedure are always constants and need to be semantic values at least to be included in case splits, no?

[Halbaroth]

Actually we produce two values during the optimization of case-split:

1. the first value is used in the literal of the case-split.
2. the second value is used in the objective model. Most of the time, they are equal but if you try to optimize a strict inequality or your problem is unbounded, the value for the objective model will be different.

In #921, I changed the way we manipulate these values. Now there is three cases:

• the problem is unbounded. We write an infinite objective value in the model and we produce a constant expression in the current interval of the objective function. Then we use the semantic value of this expression in the literal of the case split.
• the problem is bounded and we get a maximum. We create a constant expression and its semantic value. The constant expression is used in the objective model and the semantic value in the case split. In this case, the two values agree but their types are different.
• the problem is bounded and we get a strict bound. We create a constant expression as in the case of the unbounded problem but we keep the strict bound returned by Ocplib-simplex. The strict bound is an expression and we don't produce its semantic value as we don't plan to feed the SAT solver with a literal using this value.

Basically, semantic values should be used internally and expressions are the input and output type of the solver.

[bclement-ocp]

So after reading through #921 I still don't understand — the values we create seem to all come from ocplib-simplex optimization passed to mk_const_term and hence should be either Sy.Int or Sy.Real, which should print correctly already. Am I missing something?

[Halbaroth]

We have also the optimized expression by the user but still the printer will display 0-x instead of -x for literals x.

[bclement-ocp]

After discussion in the dev meeting: we agreed on printing (- 0 x) as (- x) only, but not the other simplifications.

[bclement-ocp]

Trusting that the large chunk of changes is just copy/paste (although probably no longer necessary)

[Halbaroth]

Uhm I don't understand why you accept this PR? I just change it only commit in order to perform only the transformation (0 - x) to (- x) as we said during the last dev meeting.

[bclement-ocp]

Uhm I don't understand why you accept this PR? I just change it only commit in order to perform only the transformation (0 - x) to (- x) as we said during the last dev meeting.

Because the changes that we agreed upon were made :) I was still marked as "review requested" and so accepted after you pushed those changes (even though GitHub's UI is messed up and doesn't show that).

[bclement-ocp]

Approving again since GitHub insists.