search

runtimeverification / k

K Framework Tools 7.0
BSD 3-Clause "New" or "Revised" License
430 stars 141 forks source link

Revise symbolic set simplification rules and tests #3026

Open jberthold opened 1 year ago

jberthold commented 1 year ago

After fixing two set matching bugs in the Haskell backend, the set simplification rules in domains.md should be revised, and possible some more rules added. Some tests in regression-new/set-symbolic-tests were failing before, and more cases should be added if more powerful simplification rules can be added.

ehildenb commented 1 year ago

This directory: https://github.com/runtimeverification/k/tree/master/k-distribution/tests/regression-new/set-symbolic-tests/failing

Contains all the failing tests, and we should see if some of them are passing now, and if so enable them on CI.

This directory as well: https://github.com/runtimeverification/k/tree/master/k-distribution/tests/regression-new/set-symbolic-tests/unsimplified