[FEATURE] Rewrite \E x \in a..b: p to \E x \in Int: a <= x /\ x <= b /\ p

[Kukovec]

ExprOptimizer already translates x \in a..b to a <= x <= b, and while there's no good way to handle the set a..b for non-constant a,b explicitly, quantification should be one of the cases where we can introduce optimizations.

We should also consider translating \A x \in a..b: p to \A x \in Int: (a <= x /\ x <= b) => p (though at the moment, \A x \in Int: ... might be a bad idea).

Related: #446

[Kukovec]

@konnov thoughts?

[Kukovec]

Also, from what I can tell, this would not throw in cases like #425

[konnov]

Also mentioned in #481

[konnov]

It is a very good idea and we should do it. It is not just an optimization. It may enable support of a..b for the case when a and b are not constants. As we discussed during the stand up, I think we should do that in two steps:

1. Translate expressions over unbounded sets of integers into the unbound forms:

• Translate \E x \in Int: P and \A x \in Int: P into \E x: P and \A x: P.
• Translate \E x \in Nat: P and \A x \in Nat: P into \E x: x >= 0 /\ P and \A x: x >= 0 => P
• Translate \E x \in a..b: P and \A x \in a..b: P into \E x: a <= x /\ x <= b /\ P and \A x: (a <= x /\ x <= b) => P

2. Add a special rule for the unbound forms \E x: P and \A x: P. By having the types, we can figure the type of x. The only complication here is that Z3SolverContext immediately pushes assertions on assertGroundExpression. We have to introduce a stack of quantified contexts, similar to database transactions. Whenever \E x: P or \A x: P is met, it would call solver.introQuantifier(...). All calls to assertGroundExpressions should be buffered, if the quantifier stack is non-empty. Once the rewriting rule is done with P, it calls solver.commitQuantifier(...) and this pushes the buffered expressions either to the solver context, or to the higher level context (if quantifiers are nested).

[konnov]

Also related is #844

[konnov]

This one is also related #480. All these issues call for a general approach.

[konnov]

Hey Jure @Kukovec! Is this issue closed via #1431?

[Kukovec]

No. While that PR implements the rewriting itself, it does not

• Change PreproPass to actually use it, or
• Implement a translation rule for unbounded quantifiers.