TRS / SRS categories done, C and LP running
Dear all, the TRS and SRS categories are done! I just started the categories C and Logic Programming. https://termcomp.verify.rwth-aachen.de/Y2024/ Best Florian
Hi Florian,
the TRS and SRS categories are done!
Nice, and thank you very much. That was smooth sailing? At least it appears like this, from the outside. Also, it was just in time for a quick coffee table presentation for my colleagues. SRS-Relative: AProVE was not using _Fixed? SRS-Rel-Cert: matchbox has some UNSUPPORTED (I know what is happening/missing, had no time to fix it https://git.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/issues/500) and some REJECT (I don't ... https://git.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/issues/526) - Johannes.
Hi there, also thanks from my side to Florian for running the competition.
and some REJECT (I don't ... https://git.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/issues/526)
Here is what I see in the proof of Waldmann_23/size-10-alpha-2-num-58.ari there is the following rule (among others) b1 (b1 (b1 (b1 (b0 (a0 (x)))))) -> b1 (b1 (b0 (x))) this is labeled according to CeTA (when instantiating x by 0) b13(b13(b13(b12(b00(a00(x)))))) -> b13(b12(b00(x))) using the following interpretation that is given in certificate [a0(x1)] = 4*x1 + 0 (mod 4) = 0 [a1(x1)] = 4*x1 + 1 (mod 4) = 1 [b0(x1)] = 4*x1 + 2 (mod 4) = 2 [b1(x1)] = 4*x1 + 3 (mod 4) = 3 When calculating this by hand it looks correct to me, though there might be some misunderstanding in the labeling function: when working with carrier {0,..,3}, so everything is "mod 4", there is no point in adding 4*x1 in the interpretations. Perhaps this is the problem??? Nevertheless, Matchbox produces the following labeled rule (when instantiating x by 0) b10(b10(b10(b11(b03(a00(x)))))) -> b10(b11(b00(x))) which seems to have used a different interpretation. Therefore, CeTA complains at this step. Best, René
Hey Johannes, "AProVE was not using _Fixed?" Yes, we sadly didn't have the time to optimize our new DPs for relative SRSs as they were mainly invented for relative TRSs, but we still wanted to show that they can be used for SRSs as well. We still need to implement Matrix interpretations for them, etc. The "_Fixed" version is simply the strategy from last year. This is also the reason why our certified version is better than the version without certificates. Next time, we plan on having a more refined strategy for relative SRSs again! Best, Jan-Christoph
Hi Jan-Christoph, Johannes, I'm sorry that TRS_Relative was a demo. I haven't had time to look into NaTT's bug... Best, Akihisa On 2024/07/04 16:27, Jan-Christoph Kassing wrote:
Hey Johannes,
"AProVE was not using _Fixed?" Yes, we sadly didn't have the time to optimize our new DPs for relative SRSs as they were mainly invented for relative TRSs, but we still wanted to show that they can be used for SRSs as well. We still need to implement Matrix interpretations for them, etc.
The "_Fixed" version is simply the strategy from last year. This is also the reason why our certified version is better than the version without certificates.
Next time, we plan on having a more refined strategy for relative SRSs again!
Best, Jan-Christoph _______________________________________________ Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
Dear Florian, sorry to be late to notice. Last years VBS of TRS_Relative is completely polluted by the NaTT bug. Can you replace https://github.com/TermCOMP/starexec-master/blob/master/Y2023/TRS_Relative.V... by .../Y2022/... ? Best, Akihisa On 2024/07/18 10:55, YAMADA, Akihisa wrote:
Hi Jan-Christoph, Johannes,
I'm sorry that TRS_Relative was a demo. I haven't had time to look into NaTT's bug...
Best, Akihisa
On 2024/07/04 16:27, Jan-Christoph Kassing wrote:
Hey Johannes,
"AProVE was not using _Fixed?" Yes, we sadly didn't have the time to optimize our new DPs for relative SRSs as they were mainly invented for relative TRSs, but we still wanted to show that they can be used for SRSs as well. We still need to implement Matrix interpretations for them, etc.
The "_Fixed" version is simply the strategy from last year. This is also the reason why our certified version is better than the version without certificates.
Next time, we plan on having a more refined strategy for relative SRSs again!
Best, Jan-Christoph _______________________________________________ Termtools mailing list -- termtools@lists.rwth-aachen.de To unsubscribe send an email to termtools-leave@lists.rwth-aachen.de
participants (5)
-
Florian Frohn -
Jan-Christoph Kassing -
Johannes Waldmann -
Thiemann, René -
YAMADA, Akihisa