Add support for replace_re
#102
Conversation
| if(axiomatized_persist_terms.contains(e)) | ||
| return; |
There was a problem hiding this comment.
Why is this if check necessary? Why can it be run multiple times on the same e?
There was a problem hiding this comment.
Not completely sure, we have it also in other handle functions. I think z3 can send us the same term multiple times. It might be better to do it in relevant_eh() instead of in every handle function.
There was a problem hiding this comment.
Yes, there might be multiple occurrences of the syntactically same predicates/functions.
There was a problem hiding this comment.
That makes sense. Thanks for the explanation. Should we move these into the parent handler instead of copying them to every function, as suggested above?
There was a problem hiding this comment.
It is possible, but it is not that easy. Negated predicates are in the positive form in fact (sign is given by a Boolean flag). Maybe there are some other problems, not sure now. I would keep it as it is.
There was a problem hiding this comment.
OK. Let us just keep this as it is. I consider this conversation to be resolved.
|
On |
|
For the 2 instances with only |
Simple axiomization for
replace_re. Needs to run experiments.