Before this PR, the ADT destructors worked as follow:
Destructor applictions from the user input were guarded: there are considered as aliens by the ADT theory;
If the domain of an ADT semantic values became a singleton or if the input contains a tester application on this value, the ADT destructor application on this semantic value became interpreted.
The reason of this contruction is because all the functions are total in the SMT-LIB standard, even the destructors. So a destructor is partially interpreted:
If v is an ADT value and d is a destructor of this ADT associated with the constructor c, then:
d v can be anything if the constructor of v isn't necessary c;
d v is the field of c associated with d if the only possible constructor for v is c.
This PR uses the new mechanism Rel_utils.Delayed to delay the computation of d v until we know that v is of the form (c ...).
Before this PR, the ADT destructors worked as follow:
The reason of this contruction is because all the functions are total in the SMT-LIB standard, even the destructors. So a destructor is partially interpreted:
If
vis an ADT value anddis a destructor of this ADT associated with the constructorc, then:d vcan be anything if the constructor ofvisn't necessaryc;d vis the field ofcassociated withdif the only possible constructor forvisc.This PR uses the new mechanism
Rel_utils.Delayedto delay the computation ofd vuntil we know thatvis of the form(c ...).This PR is rebased on #1078.