OCamlPro
feat(shostak): Transparent abstracted constants
This patch introduces a new type of leaf in the Shostak module, called abstract leaves. Abstract leaves behave like constant terms, and are intended to replace the X.term_embed (E.fresh_name ty) pattern where possible.
An abstract leaf is created by calling X.abstract on an existing semantic value r. The abstract leaf X.abstract r is automatically defined to be equal to r when processed by the Uf and Ccx modules.
The benefits of abstract leaves over fresh term constants are twofold:
-
With fresh constants, when the same semantic value is abstracted multiple times, a new constant is created for each abstraction. Semantically, this is correct; however, this causes the introduction of unnecessary constants in the union-find that will just end up in the same equivalence class. With abstract leaves, abstracting the same semantic value multiple times always returns the same constant.
-
With fresh constants, an additional equation between the new constant and the original term to abstract must be kept and processed separately. Since abstract leaves embed their definition, the additional equations can be introduced automatically by the
UfandCcxmodules and do not need to be carried separately.
Abstract leaves are currently only used by the AC theory. In the future, it is intended to be used as a basis for implementing application of interpreted-but-not-solvable functions to semantic values (so that for instance we can denote bv2nat(r) where r is a semantic value). While it would be straightforward to adapt abstract leaves to be able to create terminal leaves for bv2nat(r) (without definitional equations), we want congruence closure and computation (so that bv2nat(x @ y) automatically becomes bv2nat(x) * 2^n + bv2nat(y)) to work for such leaves. This require additional adaptations to CC(X), and is expected to need abstract leaves to enforce an AC(X)-compatible ordering.
I expected this to have little to no impact but there seems to be some regressions on the internal dataset. I don't think we need it for 2.6.0 as the follow-up won't be complete by then, so I'm marking the PR as draft for now and will revisit in the next release cycle.
Sure — I think it will be mostly identical once it is posted again, but I want to make sure I understand the regressions better. If needed we will keep fresh_ac_name for AC abstractions and use the new mechanism for new abstractions.