Documentation of the ADT #1013
Documentation of the ADT #1013
Conversation
Halbaroth
force-pushed
the
documentation-adt
branch
from
02a31ad to
0dddf61
Compare
There was a problem hiding this comment.
This is a PR that documents the ADT theory, but also includes code simplifications, which makes it hard to read as it requires many mental context switches. The code simplifications look correct, and more documentation is always good, however there are some points in the documentation that need clarification (questions inline).
I also think that it would be better to add a link to #1014 rather than copying the description of that bug in a comment.
src/lib/reasoners/adt_rel.ml
Outdated
| In this case, we deduce the constructor of the semantic value and | ||
| we add this equation to the pending queue using [deduce_is_constr]. | ||
|
|
||
| - When we add a guarded destructor for the first time, we add a new |
There was a problem hiding this comment.
Do you mean when the guard is activated (i.e. when we learn the tester)?
There was a problem hiding this comment.
It's the opposite situation. We know that the domain is a singleton, thus we call deduce_is_constr. This function propagate two literals to CC(X) through the queue pending_deds:
- an equation of the form
t = cons x_1 ... x_n - the literal
(_ cons t).
Thus in this situation we activate any guard on destructors of cons because the domain is a singleton. It makes sense as a singleton domain means that the only consistent way to produce a value for t is to use the constructor cons, so we can active the guard of any destructor of cons.
There was a problem hiding this comment.
This explanation corresponds to my understanding (although I think you meant ((_ is cons) t)), but I still don't understand what "when we add a guarded destructor for the first time" means. Can you clarify the second list item?
There was a problem hiding this comment.
If we have already assumed the tester of the associated constructor of the destructor d and we add d to the theory, we don't create a pending equation in selectors.
This PR documents and cleans a bit the ADT theory.
Halbaroth
force-pushed
the
documentation-adt
branch
from
0dddf61 to
0c0a464
Compare
src/lib/reasoners/adt_rel.ml
Outdated
| In this case, we deduce the constructor of the semantic value and | ||
| we add this equation to the pending queue using [deduce_is_constr]. | ||
|
|
||
| - When we add a guarded destructor for the first time, we add a new |
There was a problem hiding this comment.
This explanation corresponds to my understanding (although I think you meant ((_ is cons) t)), but I still don't understand what "when we add a guarded destructor for the first time" means. Can you clarify the second list item?
Halbaroth
force-pushed
the
documentation-adt
branch
from
0c0a464 to
535758d
Compare
This PR documents and cleans a bit the ADT theory.
Replace the PR #544 but this old PR contains more documentation on Shostak so I didn't close it yet.