zulip log viewer

New AVATAR issue

Petar Vukmirovic
2020-04-22 16:53:16 (GMT)
I might be wrong here, but I think that unit clauses (unit before splitting) should not be asserted with component equal to their own label
Petar Vukmirovic
2020-04-22 16:56:24 (GMT)
Right now, in Zip, unit clauses $s \approx t$ are represented as $s \approx t \leftarrow [s \approx t]$
Petar Vukmirovic
2020-04-22 16:56:54 (GMT)
(if Avatar is turned on, of course)
Petar Vukmirovic
2020-04-22 16:57:27 (GMT)
This might be the biggest reason why turning on AVATAR results in performance loss, IMO
Petar Vukmirovic
2020-04-22 16:57:38 (GMT)
@Simon Cruanes , whay do you think?
Simon Cruanes
2020-04-22 16:58:34 (GMT)
It should definitely not be the case in the current implementation.
$s \simeq t$ is just itself unless it comes from an avatar case split.
Simon Cruanes
2020-04-22 16:58:48 (GMT)
if not, that's a big bug (and one that didn't use to be there)
Petar Vukmirovic
2020-04-22 17:24:56 (GMT)
OK. I made a mistake... I misread one symbol on the clause level and thought that equtions are the same, but they were not
Petar Vukmirovic
2020-04-22 17:24:57 (GMT)
sorry
Simon Cruanes
2020-04-22 17:25:21 (GMT)
no worries :)