WIP Syntactic simplifications #4022
Conversation
geo2a
force-pushed
the
4579-syntactic-simplifications
branch
6 times, most recently
from
76fa380 to
bebd5c0
Compare
Refactor `applyRule` and `applyEquation` to check `requires`/`ensures` in separate functions. This will make reviewing #4022 easier.
geo2a
force-pushed
the
4579-syntactic-simplifications
branch
from
bebd5c0 to
c4a7dec
Compare
Fix unit tests
Run test-syntactic-simplification Fix test
geo2a
force-pushed
the
4579-syntactic-simplifications
branch
from
322432f to
908ddf6
Compare
| [] -> | ||
| unless (null restRequires') $ | ||
| -- no more @syntacticRequires@, but unresolved conditions remain: abort | ||
| throwRemainingRequires currentSubst restRequires' |
There was a problem hiding this comment.
why do we throw here?? i would expect at the base case to simply check the regular requires clauses...
There was a problem hiding this comment.
As I understand, the simplifications marked as syntactic must be only applied "syntactically", which means their side condition must not go to Z3. If we do not stop here, we will proceed to trying to discharge a syntactic simplification as a regular one, and, as far as I understand, we do not want that. We want them either to succeed fast or to fail fast. @PetarMax do you agree?
There was a problem hiding this comment.
Regarding the code: we never want to transfer control to checkRequiresSemantically from checkRequiresSyntactically.
There was a problem hiding this comment.
So the semantics of the syntactic(1) attribute is:
- the
simplificationis syntactic, Z3 is never called - the clause 1 is the driver clause which learns its variables from the known truth, and the the substitution for these learned variables is applied to all other clauses
I.e. the whole simplification is syntactic, not a clause of a simplification
There was a problem hiding this comment.
So, for me, the clauses marked as syntactic should be checked syntactically, the other ones should be checked semantically. A simplification can have both syntactic and semantic clauses.
This still does mean, I think, that checkRequiresSyntactically should not call checkRequiresSemantically.
There was a problem hiding this comment.
But also, all syntactics should be handled first, I think.
|
Thanks @PetarMax, we'll modify the code to do that then. |
…g variables that only appear in the requires clause with syntactic
Fixes #3861