search

alcides / aeon

Aeon programming language
https://alcides.github.io/aeon/
8 stars 3 forks source link

Smt reversed constraint binders #25

Closed eduardo-imadeira closed 6 months ago

eduardo-imadeira commented 6 months ago

In the grammar_filter branch I needed to reverse the c.binders in the method translate inside the file verification/smt.py , to fix my smt_test.py but in this branch I dont need that modification. With that modification it raises the same error as the grammar_filter branch was raising without the modification

the test is a little bit different because the step of ensuring that the code is in anf is done differently in both branches

alcides commented 6 months ago

This is weird: The right order is to be reversed (the closest binder has priority, and shadows those var away). As in:

forall x:Int, forall x:Book x should be valid as x is Bool here. Reversing the order should not be a problem.

However, we may decide to make each new variable fresh, so there are no conflicts in Verification Conditions, and no order is even required.