Ordered constraint accumulation

[Baltoli]

Transfer of: runtimeverification/pyk#1065

[ehildenb]

I think there are still some places where we could be comparing equality of CTerm without considering different constraint ordering. So I wolud drop the parameter, not sort them by default, and then test with Kontrol. If there are no problems, good to merge. Otherwise, maybe we need to implement explicit equality operator for CTerm directly.

So in short, I agree with @tothtamas28 to not provide the option to have the constraints out of order. Hopefully there are no problems, but if there are, then we need to implement equality over CTerm directly instead of using derived implementation.

[PetarMax]

Ok, I will proceed with that then. Since this could be quite fragile, perhaps we could just do a custom equality? Although, in truth, there are lots of sets in configurations that are just treated syntactically...

[ehildenb]

@PetarMax if you've tested this with Kontrol, feel free to merge. You'll probably need to track it's progress downstream, as it may change test output.

[PetarMax]

Thank you - yes, I will test with both KEVM and Kontrol before I merge.

[PetarMax]

Can confirm that all of the KEVM integration tests for the Build and Test KEVM proofs (test-prove-pyk, --use-booster, 150) job pass.

[PetarMax]

...but will have to wait to test with Kontrol since the transition to the new pyk approach seems non-trivial (the update PR for KEVM is failing).

[PetarMax]

I haven't observed any issues in the Kontrol test suite (other than the expected outputs needing to be updated, but that is expected since the order of constraints will be different).

[Baltoli]

@PetarMax please rebase against the develop branch and remove the Set version ... commits before you merge; when working on the new K repo your branches need to be based on develop rather than master.

This also applies to bringing the branch up to date; merge in develop rather than master when you git merge ... locally.