Smart Printing

[viper-admin]

Created by bitbucket user nilsbecker_ on 2019-02-27 20:10
Last updated on 2019-02-27 20:22

It is not uncommon that the bodies of quantifiers contain a number of implications which z3 rewrites into a big or clause. Oftentimes a user is only interested in one of the disjucts. At least when looking at paths or generalizations the tool should be able to tell which disjuncts are interesting based on which terms are used to trigger the next instantiation in the path (these terms are highlighted in yellow and blue). It may, therefore, be useful to be able to set a different printing depth for "interesting" terms than for other ones. This would especially be useful to reduce clutter when exploring deep term structures. The resulting representation may then look similar to:

#!

or(..., ..., >...<, >...<, ...,
    f(g(T+1, h(...))),
    >...<, >...<, >...<)

It may also be worth considering applying a similar technique to additional triggers of a quantifier that were not used to produce this instantiation.

[viper-admin]

Bitbucket user nilsbecker_ on 2019-02-27 20:22:

• changed kind from enhancement to proposal