Fixed which closure elimination transformers had scope as a precondition

WatForm / fortress

Fortress: Finite Model Finder for Many-Sorted First-Order Logic

MIT License

5 stars 0 forks source link

Fixed which closure elimination transformers had scope as a precondition #113

Closed otzzila closed 3 months ago

otzzila commented 3 months ago

Fixes WatForm/fortress#109

Removed precondition incorrectly checking for a scope on closing sort in Eijck transformer
Added sort-exists precondition to iterative and squaring transformers
Added tests to ensure transformers behave correctly in regards to this issue

nancyday commented 3 months ago

Looks good, but for

Added sort-exists precondition to iterative and squaring transformers I'm thinking that we should guard any non-essential tests with a flag to say if we are in some sort of "correctness testing" mode rather than "performance testing" I will make another issue for adding this flag.

otzzila commented 3 months ago

Looks good, but for

* Added sort-exists precondition to iterative and squaring transformers
  I'm thinking that we should guard any non-essential tests with a flag to say if we are in some sort of "correctness testing" mode rather than "performance testing"
  I will make another issue for adding this flag.

We can tag tests, then use certain sbt flags to use or exclude tags.

nancyday commented 3 months ago

Do you mean in the Tests - because I'm talking about with the main program?