fix(AC): Also abstract non-AC arguments of AC symbols #974
Conversation
Alt-Ergo uses an abstraction mechanism for the arguments of AC symbols to ensure termination of the induced rewrite ordering without resorting to a recursive path ordering. This is described in section 6 of [this paper][1], except that the implementation doesn't do exactly what is described there -- in particular, it only abstracts nested AC symbols, which is an issue when an argument is not an AC symbol but a semantic value that contains another AC symbol. This patch changes the `abstract2` function in `ac.ml`, where this abstraction mechanism is implemented, to also introduce abstracted constants for non-constant terms. Fixes OCamlPro#964 [1]: https://arxiv.org/abs/1207.3262
bclement-ocp
force-pushed
the
bclement-ocp/issue-964
branch
from
b75802e to
b52ac0f
Compare
|
Damn, -11 on AE-Format, looks like this is too aggressive :(
Following discussion at the dev meeting yesterday: this is not actually what happens in the paper, as noticed by @Halbaroth |
This patch implements a variation of the abstraction mechanism described in the AC(X) paper. This should hopefully ensure that we can't create substitution cycles due to improper term ordering. Note that the issue is related to comparing distinct AC symbols: when the AC symbols are identical, the AC theory uses a multiset ordering on its argument, which prevent substitution cycles. But when the AC symbols are different, only the symbols are compared, not the arguments, and so we must rely on the abstraction mechanism to prevent cycles. This is a do-over of OCamlPro#974 that should be closer in spirit to the implementation of the paper and without the associated regressions. Fixes OCamlPro#964
|
Did you try to implement naively the paper? I mean you explain to us that your patch abstracts some interpreted symbols to avoid a bunch of new abstract variables. Did you try the naive way? Is it terrible? |
I think it would be problematic (strictly speaking, the paper requires introducing one variable for every AC and uninterpreted symbol appearing in a semantic value, so there would never |
This patch implements a variation of the abstraction mechanism described in the AC(X) paper. This should hopefully ensure that we can't create substitution cycles due to improper term ordering. Note that the issue is related to comparing distinct AC symbols: when the AC symbols are identical, the AC theory uses a multiset ordering on its argument, which prevent substitution cycles. But when the AC symbols are different, only the symbols are compared, not the arguments, and so we must rely on the abstraction mechanism to prevent cycles. This is a do-over of OCamlPro#974 that should be closer in spirit to the implementation of the paper and without the associated regressions. Fixes OCamlPro#964
This patch implements a variation of the abstraction mechanism described in the AC(X) paper. This should hopefully ensure that we can't create substitution cycles due to improper term ordering. Note that the issue is related to comparing distinct AC symbols: when the AC symbols are identical, the AC theory uses a multiset ordering on its argument, which prevent substitution cycles. But when the AC symbols are different, only the symbols are compared, not the arguments, and so we must rely on the abstraction mechanism to prevent cycles. This is a do-over of OCamlPro#974 that should be closer in spirit to the implementation of the paper and without the associated regressions. Fixes OCamlPro#964
This patch implements a variation of the abstraction mechanism described in the AC(X) paper. This should hopefully ensure that we can't create substitution cycles due to improper term ordering. Note that the issue is related to comparing distinct AC symbols: when the AC symbols are identical, the AC theory uses a multiset ordering on its argument, which prevent substitution cycles. But when the AC symbols are different, only the symbols are compared, not the arguments, and so we must rely on the abstraction mechanism to prevent cycles. This is a do-over of OCamlPro#974 that should be closer in spirit to the implementation of the paper and without the associated regressions. Fixes OCamlPro#964
This patch implements a variation of the abstraction mechanism described in the AC(X) paper. This should hopefully ensure that we can't create substitution cycles due to improper term ordering. Note that the issue is related to comparing distinct AC symbols: when the AC symbols are identical, the AC theory uses a multiset ordering on its argument, which prevent substitution cycles. But when the AC symbols are different, only the symbols are compared, not the arguments, and so we must rely on the abstraction mechanism to prevent cycles. This is a do-over of #974 that should be closer in spirit to the implementation of the paper and without the associated regressions. Fixes #964
Alt-Ergo uses an abstraction mechanism for the arguments of AC symbols to ensure termination of the induced rewrite ordering without resorting to a recursive path ordering.
This is described in section 6 of this paper, except that the implementation doesn't do exactly what is described there -- in particular, it only abstracts nested AC symbols, which is an issue when an argument is not an AC symbol but a semantic value that contains another AC symbol.
This patch changes the
abstract2function inac.ml, where this abstraction mechanism is implemented, to also introduce abstracted constants for non-constant terms.Fixes #964
Note: while this is ready for review, I want to run benches prior to actually merging — this changes the way reasoning proceeds in the presence of AC symbols, which can have an impact on any NLA problems (see also #500).