alt-ergo
alt-ergo copied to clipboard
Preserve mapping between old and new representatives with AC symbols
In CC(X), the leaves are always terms that were present in the original problem: we do not introduce new uninterpreted terms.
In AC(X), this is no longer true: we might introduce new AC leaves dynamically that are not themselves term representatives (i.e. they don't have an entry in the repr
map) through "deep" rewriting into the AC leaf.
When we have a class representative rr
for a semantic value r
, and a new class representative nrr
is found, the relations see an equality (with Subst
origin) r = nrr
. Normally, since rr
is a term representative, we have rr --> rr
as a mapping, and so the relation will see rr = nrr
and can use this to update its internal state.
With these "dynamic" representative, when they later get override by a new representative, the relations will not see an rr = nrr
equality, which makes its internal state get out of sync and can cause bugs.
This patch makes it so that, when we encounter one of these "dynamic" representatives, we artificially add the rr = nrr
equality (by adding rr --> nrr
as a pivot, which will in turn cause the equality to show up).
Since this case should only be possible with AC rewriting, the rr = nrr
equality is only added in up_uf_rs
, i.e. if there are AC rewrite rules.
Fixes #474
(Note that I did not add the original test case from #474 as a test — this is because since #731, we simplify if true then ruqv0 else ur_3
into ruqv0
which causes Alt-Ergo to not terminate with the CDCL solver)