Create iprover_smtcomp.sh #96
Conversation
To run iProver please use cd bin iprover_smtcomp.sh <problem> "cd bin" is needed as paths in scripts are relative to bin.
|
Hi Konstantin, please run make check and then commit and push again. Our CI is a bit nitpicky about trailing whitespaces and with make check this should be fixed automatically. The CI should then also run some tests automatically, so you can see whether your solver will run on our execution platform. |
|
Hi Martin, Thanks
|
|
PS I don't have any logic specific command lines. Just: cd bin for the specified logics in the json file. |
|
You are missing some imports. The quickest solution would be that you try to commit and push it again and then we will see if the CI that has all the imports still detects any errors. |
|
Now it looks much better. I just now noticed that your submission ending is .sh but should be .json |
|
And parallel and cloud tracks must be in a separate submission. |
|
OK, thanks!
K.
…On Thu, 13 Jun 2024 at 16:02, mbromber ***@***.***> wrote:
And parallel and cloud tracks must be in a separate submission.
—
Reply to this email directly, view it on GitHub
<#96 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AIVYHTOUCEH2JRNVKRAD5ODZHGYBLAVCNFSM6AAAAABJIJC55SVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCNRVHEZTQOJQGE>
.
You are receiving this because you authored the thread.Message ID:
***@***.***>
|
|
Your submission file is no longer tracked by git. You need to do a "git add" if you renamed it without "git mv" |
|
The CI has found the next bug in your submission. should be And if you add something in the field divison, then you are automatically registered to all logics in that division! So maybe you want to remove that field? |
Summary of modified submissionsiProver v3.9
|
|
Next issue is that the link does not point to an archive. It should be https://zenodo.org/records/11636244/files/iprover_v3.9_smt_comp_2024.zip |
|
Thanks Martin,
How can I correctly specify the command line:
cd bin; iprover_smtcomp.sh <problem>
Konstantin
…On Thu, 13 Jun 2024 at 16:29, mbromber ***@***.***> wrote:
Next issue is that the link does not point to an archive. It should be
https://zenodo.org/records/11636244/files/iprover_v3.9_smt_comp_2024.zip
—
Reply to this email directly, view it on GitHub
<#96 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AIVYHTLKCEOCZRCLCHSED33ZHG3FHAVCNFSM6AAAAABJIJC55SVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCNRWGAYTAMRYGY>
.
You are receiving this because you authored the thread.Message ID:
***@***.***>
|
|
As far as I know, you can't. The first argument of command is supposed to be a script or binary in your folder and is not even executed from your base folder directly. You will need to query in your script(s) the current directory path. |
|
So the command should be "bin/iprover_smtcomp.sh" and you need to modify your scripts so you can run the script from anywhere. |
|
OK, I'll try to adapt the head script and see if this helps.
Thanks
…On Thu, 13 Jun 2024 at 16:48, mbromber ***@***.***> wrote:
So the command should be "bin/iprover_smtcomp.sh" and you need to modify
your scripts so you can run the script from anywhere.
—
Reply to this email directly, view it on GitHub
<#96 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AIVYHTIO3ZWTSMVYDROIBOTZHG5OVAVCNFSM6AAAAABJIJC55SVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCNRWGA3DIMZQHA>
.
You are receiving this because you authored the thread.Message ID:
***@***.***>
|
|
Hi Martin,
Is it possible to see the log output ?
I think submitted set up would run on StarExec....
['unpack/2f5c6f5aae51d6c6e23e345ad8a15b1e3d6a0d2832776e55b05fb397847c9d31/bin/iprover_smtcomp.sh',
'trivial_bench/files/LRA/LRA.unsat.smt2']
Error expected unsat result obtained unknown
....
Thanks
Konstantin
On Thu, 13 Jun 2024 at 16:50, Konstantin Korovin ***@***.***>
wrote:
… OK, I'll try to adapt the head script and see if this helps.
Thanks
On Thu, 13 Jun 2024 at 16:48, mbromber ***@***.***> wrote:
> So the command should be "bin/iprover_smtcomp.sh" and you need to modify
> your scripts so you can run the script from anywhere.
>
> —
> Reply to this email directly, view it on GitHub
> <#96 (comment)>,
> or unsubscribe
> <https://github.com/notifications/unsubscribe-auth/AIVYHTIO3ZWTSMVYDROIBOTZHG5OVAVCNFSM6AAAAABJIJC55SVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCNRWGA3DIMZQHA>
> .
> You are receiving this because you authored the thread.Message ID:
> ***@***.***>
>
|
|
Hi Martin,
I noticed that behaviour on the smt-comp server and our local server is
different. In particular,
./iprover_smtcomp.sh UF.sat.smt2
is solved locally but not solved on smtcomp. I also added dbg output and
can see iProver scripts run differently on smt-comp server compared
locally.
After some investigation I see that smt-comp has old python3 version 3.10.12
We rely on python 3.11.
Although we are using cx_Freeze to get an executable from python scripts
and packagies
I suspect 3.10.12 is still too old.
Any chance upgrading python ?
I tried to run the submitted version on a "fresh" Ubuntu laptop and it
runs as expected.
Note that currently upload is a dbg version to investigate this issue.
Thanks,
Konstantin
…On Thu, 13 Jun 2024 at 22:04, mbromber ***@***.***> wrote:
"Error: Process completed with exit code 1." should be because you
returned unknown on some of the benchmarks. But I think only on benchmarks
where you expected this. So don't worry about it.
—
Reply to this email directly, view it on GitHub
<#96 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AIVYHTKKBVRXCRR72LEDUS3ZHICM5AVCNFSM6AAAAABJIJC55SVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCNRWG44TENJYHE>
.
You are receiving this because you authored the thread.Message ID:
***@***.***>
|
|
@konstantin-korovin We have executed the latest version of iProver on a randomly chosen subset of 20 single-query benchmarks from each logic where it participates. The benchmarks are also scrambled by the competition scrambler (with seed 1). You can find the results here: https://www.fi.muni.cz/~xjonas/smtcomp/iprover.table.html#/table Quick explanation:
Please check whether there are some discrepancies, such as missing/extra logics, unexpected aborts or unknowns, and similar. |
I don't think we can update it. But we have a meeting in 15 minutes and we will discuss whether this is possible there. |
|
Hi Konstantin, it is not in our power to change the python version that is used on the cluster nodes. But you could add and use a virtual environment in your archive. There you can pick any python version you want independent of what we have installed. See https://docs.python.org/3/library/venv.html and https://stackoverflow.com/questions/1534210/use-different-python-version-with-virtualenv |
|
Hi Martin,
Thanks for the links I'll try to make this work.
Regards,
Konstantin
…On Fri, 14 Jun 2024 at 09:37, mbromber ***@***.***> wrote:
Hi Konstantin, it is not in our power to change the python version that is
used on the cluster nodes. But you could add and use a virtual environment
in your archive. There you can pick any python version you want independent
of what we have installed. See https://docs.python.org/3/library/venv.html
and
https://stackoverflow.com/questions/1534210/use-different-python-version-with-virtualenv
—
Reply to this email directly, view it on GitHub
<#96 (comment)>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AIVYHTOQSQG6XHUW4HNCQYTZHKTU7AVCNFSM6AAAAABJIJC55SVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDCNRXGUZTSMZZGY>
.
You are receiving this because you were mentioned.Message ID:
***@***.***>
|
To run iProver please use
cd bin
iprover_smtcomp.sh
"cd bin" is needed as paths in scripts are relative to bin.