Handling of Rewrite Steps

[viper-admin]

Created by bitbucket user nilsbecker_ on 2019-02-27 19:51 Last updated on 2019-09-30 15:50

For simple loops as shown in the attached file where we have some term f(x) and add 1 to x each time around the loop the integer arithmetic solver (or any other solver in different examples) may rewrite some terms. In the attached example we bind x to a then a+1 then a+2 etc. In order to correctly generalize these terms we would need to have a+1+1 as the third term.

Note that we end up with something looking very similar to what we would want the generalization to be due to the generalization going wrong in just the right way: we first anti-unify the terms shown above to obtain T then essentially ignore the first term (a) for the results since it was not produced by any instantiation in the loop. Anti-unifying a+1, a+2, etc. then gives us a+Int() (it is even possible to obtain T+Int() in other examples), however, the identifier of the Int constant is prefixed with a "g" indicating that the constant changes in each iteration of the loop.

---

Attachments:

• z3.log.zip
• simple-loop.smt2

[viper-admin]

Bitbucket user nilsbecker_ on 2019-02-27 19:52:

• edited the description

[viper-admin]

Bitbucket user nilsbecker_ commented on 2019-09-30 15:45

Updated log file to one generated with a newer version of z3

[viper-admin]

Bitbucket user nilsbecker_ on 2019-09-30 15:45:

• changed attachment from (none) to z3.log.zip

[viper-admin]

Bitbucket user nilsbecker_ commented on 2019-09-30 15:50

Since we introduced handling of term rewritings done by z3 this mostly works now:

We get f(+(1, T)) in the generalized yield term. However, we do not seem to generate the correct bindings to start the next iteration. We still get T' = +(Int(), a()) there.