Update cvc5 to 1.0.8

[CyanoKobalamyne]

Fixes #328.

[yoni206]

Hi @CyanoKobalamyne , Thanks for doing this, it looks great!
I would be happy to review, but first, could you make CI to pass?
There seems to be a problem with the macos build.

Also, in case this indeed solves #328 , can you mention this in the PR description? This way the issue will be closed automatically.

[CyanoKobalamyne]

I think I fixed that particular error, but now there seem to be other ones that I don't quite understand. Why do the jobs get canceled? Is there some sort of timeout or memory limit?

[barrettcw]

Weird - I don't know why they are getting cancelled. Something in the configuration?

[CyanoKobalamyne]

Ah, it looks like, by default, if one job fails, all others get cancelled: https://docs.github.com/en/actions/using-jobs/using-a-matrix-for-your-jobs#handling-failures

[yoni206]

Right, but once you push a fix to your branch, all jobs should restart running.

…

On Friday, October 6, 2023, Áron Ricardo Perez-Lopez < ***@***.***> wrote: Ah, it looks like, by default, if one job fails, all others get cancelled: https://docs.github.com/en/actions/using-jobs/using-a- matrix-for-your-jobs#handling-failures — Reply to this email directly, view it on GitHub <#332 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ADAKGRB3QBXYCCSUOF4M3ELX554UBAVCNFSM6AAAAAA5TLF6U2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONBZHE2DCMBWHE> . You are receiving this because you commented.Message ID: ***@***.***>

[CyanoKobalamyne]

Weird, the one failing test, cvc5-printing_test, passes locally on my machine.

[yoni206]

Do you have the same configuration as the test? https://github.com/stanford-centaur/smt-switch/actions/runs/6437096065/job/17481656787?pr=332#step:9:1 Also -- I see that it fails on ubuntu (and then the macOS one does not run as a consequence). If the configuration is the same and you still can't reproduce, perhaps you can try running it on ubuntu? And specifically regarding the printing solver test: it relies on the location of the cvc5 binary: https://github.com/stanford-centaur/smt-switch/blob/f2d7d3d6dfccc0b4d6b604563acd34629bac884d/tests/cvc5/cvc5-printing.cpp#L68 Maybe this has changed in this PR?

…

On Sat, Oct 7, 2023 at 2:11 AM Áron Ricardo Perez-Lopez < ***@***.***> wrote: Weird, the one failing test, cvc5-printing_test passes locally on my machine. — Reply to this email directly, view it on GitHub <#332 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ADAKGRDDHUPACJBH7EMPOTDX6CF2VAVCNFSM6AAAAAA5TLF6U2VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONJRGQ4DSNJZGM> . You are receiving this because you were assigned.Message ID: ***@***.***>

[yoni206]

Another possibly useful pointer:
https://github.com/stanford-centaur/smt-switch/tree/master/ci-scripts

These are scripts that are used in CI.

[CyanoKobalamyne]

I reran all the steps of the CI script in an Ubuntu 22.04 container, and they all passed... I'll try to rerun the checks here, to see if this was some sort of transient issue.

[CyanoKobalamyne]

Sorry, it turns out that I was using the wrong commit. I have successfully reproduced the issue on Ubuntu 22.04.

[CyanoKobalamyne]

The mystery about the error not appearing on my machine is solved: I was compiling smt-switch with assertions disabled.

The failure in the test is an assertion on the expected output (called from test1):

smt-switch/tests/cvc5/cvc5-printing.cpp

Line 78 in f2d7d3d

assert(result == expected_result);

The string given here as the expected output is in fact not the output from cvc5 1.0.8 for the same input. The second line, which is the output for s->get_unsat_assumptions(usc), is (ind1), while the test expects it to be (). I'm currently trying to investigate what changed between 1.0.0 and 1.0.8.

[yoni206]

The mystery about the error not appearing on my machine is solved: I was compiling smt-switch with assertions disabled.

Do you mean with debug disabled? I don't see assertions here.

The failure in the test is an assertion on the expected output (called from test1):

smt-switch/tests/cvc5/cvc5-printing.cpp

Line 78 in f2d7d3d

assert(result == expected_result);

The string given here as the expected output is in fact not the output from cvc5 1.0.8 for the same input. The second line, which is the output for s->get_unsat_assumptions(usc), is (ind1), while the test expects it to be (). I'm currently trying to investigate what changed between 1.0.0 and 1.0.8.

I think it is perfectly reasonable that one version of cvc5 gives one unsat core while another gives another unsat core, since unsat cores are not unique.

So I think a good solution would be just to fix the test to expect (ind1). A more robust solution would be to check that the output from the solver is a space-separated list wrapped with parentheses, instead of expecting a specific solution that can change between versions. But I don't think that's a priority.

[CyanoKobalamyne]

It seems that the change causing the different output was introduced in cvc5/cvc5@7b8fb6675. After that commit, the arithmetic static learner gets disabled when unsat cores are enabled, and unsat cores are implicitly enabled by the :produce-unsat-assumptions flag set in this test (necessary for (get-unsat-assumptions) to work).

The end result is technically correct, because the list of assumptions is not required to be minimal by the SMT-LIB standard, but since ind1 is an assertion itself, it seems unnecessary to list it as an assumption needed to prove unsat.

Is this something we would file a bug against cvc5 for? The output after the change is not incorrect, but I would certainly consider this a regression.

(As an aside, I think that the way this test is currently written is brittle, and doesn't really just test our code, but is sensitive to changes in cvc5 too. Although it did enable us to discover this regression.)

[CyanoKobalamyne]

So I think a good solution would be just to fix the test to expect (ind1). A more robust solution would be to check that the output from the solver is a space-separated list wrapped with parentheses, instead of expecting a specific solution that can change between versions. But I don't think that's a priority.

Sorry, I only saw your reply after I had already written mine, but this is essentially what I was trying to say in the last paragraph.

I think it is perfectly reasonable that one version of cvc5 gives one unsat core while another gives another unsat core, since unsat cores are not unique.

Okay, so does this mean that we shouldn't bother the cvc5 folks with asking them to "fix" this?

[yoni206]

Thanks for the fix! I see the regressions now pass and I'll review it.
As for cvc5, I agree that this is a regression in the sense that this unsat core is bigger than the previous one, but i am not sure if it is really considered a bug...

[yoni206]

Looks great, and thanks a lot for doing this.
BTW, just wondering: Why did the include paths changed from api/cpp/... to cvc5/...?

[barrettcw]

I forgot the reason but we had a discussion with Aina and Mathias and decided this was a better organization of the header files.