Filter full results to only keep differing results

sneeuwballen / benchpress

Testing and benchmarking tool for logic-related programs.

BSD 2-Clause "Simplified" License

26 stars 8 forks source link

Filter full results to only keep differing results #43

Open Gbury opened 4 years ago

Gbury commented 4 years ago

On a view such as https://benchpress.cedeela.fr/show_table/res-20200515T222015-2eed2c42-3d64-4611-956f-341d3b2d54ab.sqlite/?offset=0 , it would be useful to be able to list only the results that differ between provers (and this list would be linked to by the numbers in the comparison table of https://benchpress.cedeela.fr/show/res-20200515T222015-2eed2c42-3d64-4611-956f-341d3b2d54ab.sqlite , like is done for each provers' individual results)

iguerNL commented 4 years ago

You can even go one step further and imagine showing:

differing results: sat / unsat vs unknown / timeout / memout
conflicting results: sat (or unsat) vs unsat (or sat)

with a prioritization of showing conflicting results, as it implies a potential soundness bug in the tool(s).

c-cube commented 4 years ago

note that when viewing a file, you already should get a list of errors (per prover), and summary tables with comparisons between provers, including conflicting instances. Then you can click on these to get to these conflicting files.

But in general, yes, the UI could use more cross linking and filtering :)

iguerNL commented 4 years ago

Ah yes, didn't notice it. Guillaume just showed me the tool.

c-cube commented 2 years ago

does this suffice, actually: https://benchpress.cedeela.fr/show_table/res-20200515T222015-2eed2c42-3d64-4611-956f-341d3b2d54ab.sqlite/?pb=&res=different ?