2020-07-05 10:13:44 (GMT)
This is not strictly IJCAR (but SMT), but I think this is still the nearest stream to pick.
Do you have any idea how your encoding behaves for classical E-matching e.g. for trigger based instantiation?
2020-07-05 10:15:26 (GMT)
I don't, but maybe @Haniel Barbosa, @Daniel El Ouraoui or @Pascal Fontaine has an answer for you?
2020-07-05 10:26:8 (GMT)
Not yet, we only implemented the encoding for conflicting-instantiation. Implement it for Triggers is on the task list.
2020-07-05 10:29:37 (GMT)
Thanks for the great talk, I like the approach! What I wanted to ask before was that it looks like it could be extended to lambdas (where you need to come up with a member of that congruence class yourself then). Is this something you're trying?
2020-07-05 10:31:43 (GMT)
We are not yet seriously looking into how to extend to handling lambdas. What you are proposing would be one way, but a very costly one because then we can't rule out classes where there is no known solution. We'll see if we can find something better or not. ^^
2020-07-05 10:34:32 (GMT)
Yeah... I'm just thinking about if part of the complexity is not inherent to (full) HO unification
2020-07-05 10:42:8 (GMT)
@Daniel El Ouraoui I wondered about the impact regarding the encoding because it's a special case