Overhaul Predicate simplifier: In simplifier

[ana-pantilie]

Part of #2570

---

Review checklist

The author performs the actions on the checklist. The reviewer evaluates the work and checks the boxes as they are completed.

• Summary. Write a summary of the changes. Explain what you did to fix the issue, and why you did it. Present the changes in a logical order. Instead of writing a summary in the pull request, you may push a clean Git history.
• Documentation. Write documentation for new functions. Update documentation for functions that changed, or complete documentation where it is missing.
• Tests. Write unit tests for every change. Write the unit tests that were missing before the changes. Include any examples from the reported issue as integration tests.
• Clean up. The changes are already clean. Clean up anything near the changes that you noticed while working. This does not mean only spatially near the changes, but logically near: any code that interacts with the changes!

[github-actions]

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-add0.sh	-0.007271	0
test/regression-evm/test-sum-to-n.sh	-0.005525	-0.000000
test/regression-evm/test-branching-no-invalid.sh	-0.008075	0
test/regression-evm/test-straight-line-no-invalid.sh	-0.009536	0
test/regression-evm/test-branching-invalid.sh	-0.007915	-0.000000
test/regression-evm/test-pop1.sh	-0.009389	0
test/regression-evm/test-straight-line.sh	-0.009347	-0.000000
test/regression-evm/test-sumTo10.sh	-0.001949	0.000113
test/regression-wasm/test-locals.sh	-0.022376	0.000231
test/regression-wasm/test-simple-arithmetic.sh	-0.020869	0.000220
test/regression-wasm/test-wrc20.sh	-0.001039	-0.001998
test/regression-wasm/test-loops.sh	-0.013176	0.000158
test/regression-wasm/test-memory.sh	-0.017170	0.000026

[andreiburdusa]

This is not directly related to your PR, but do you think we should update the In documentation so it doesn't refer to Semantics of K anymore?

[ana-pantilie]

This is not directly related to your PR, but do you think we should update the In documentation so it doesn't refer to Semantics of K anymore?

Hmm, I think all the Syntax modules do that. Do you want to open an issue for this?

[github-actions]

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-add0.sh	-0.007254	0
test/regression-evm/test-sum-to-n.sh	-0.005525	0
test/regression-evm/test-branching-no-invalid.sh	-0.008075	0
test/regression-evm/test-straight-line-no-invalid.sh	-0.009537	0
test/regression-evm/test-branching-invalid.sh	-0.007945	0.000038
test/regression-evm/test-pop1.sh	-0.009389	0
test/regression-evm/test-straight-line.sh	-0.009347	0
test/regression-evm/test-sumTo10.sh	-0.001949	0.002649
test/regression-wasm/test-locals.sh	-0.022376	0.000231
test/regression-wasm/test-simple-arithmetic.sh	-0.020869	0.000218
test/regression-wasm/test-wrc20.sh	-0.001056	0.000585
test/regression-wasm/test-loops.sh	-0.013180	0.000161
test/regression-wasm/test-memory.sh	-0.017175	0.000026

[github-actions]

name	diff_allocated_bytes	diff_max_live_bytes
test/regression-evm/test-add0.sh	-0.007251	0
test/regression-evm/test-sum-to-n.sh	-0.005565	0.000000
test/regression-evm/test-branching-no-invalid.sh	-0.008080	0
test/regression-evm/test-straight-line-no-invalid.sh	-0.009536	0
test/regression-evm/test-branching-invalid.sh	-0.007958	0
test/regression-evm/test-pop1.sh	-0.009389	0
test/regression-evm/test-straight-line.sh	-0.009347	0
test/regression-evm/test-sumTo10.sh	-0.001949	0.000114
test/regression-wasm/test-locals.sh	-0.022376	0.000231
test/regression-wasm/test-simple-arithmetic.sh	-0.020892	0.000219
test/regression-wasm/test-wrc20.sh	-0.001059	0.002545
test/regression-wasm/test-loops.sh	-0.013247	0.000161
test/regression-wasm/test-memory.sh	-0.017204	0.000026