Open bclement-ocp opened 1 month ago
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.
Do you want my review? I was reviewing it yesterday.
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.
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 valuer
. The abstract leafX.abstract r
is automatically defined to be equal tor
when processed by theUf
andCcx
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
Uf
andCcx
modules 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)
wherer
is a semantic value). While it would be straightforward to adapt abstract leaves to be able to create terminal leaves forbv2nat(r)
(without definitional equations), we want congruence closure and computation (so thatbv2nat(x @ y)
automatically becomesbv2nat(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.