
<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Mar 26, 2018, at 2:05 PM, Réka Nikolett Kovács <<a href="mailto:rekanikolett@gmail.com" class="">rekanikolett@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">Hi,<div class=""><br class=""></div><div class="">Thanks again for the comments and explanations. I hope I've incorporated all of your advice, except for this one.</div><div class=""><br class=""></div><div class="">George: I've been thinking about what you wrote ("<span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline" class="">unifying a place where the constraints are dropped, and adding a flag guarding that"</span>) </div><div class="">and I have to admit that I'm not sure I understand that precisely.</div><div class=""><br class=""></div><div class="">Constraints dropped before being added to the environment should mean that SValBuilder gave up while trying to construct a specific</div><div class="">symbolic expression from them (returned an UnknownVal), if I understand correctly. Now, the logic responsible for this seems pretty</div><div class="">much scattered around, so I thought maybe by unifying you mean creating a function like the constraint managers' canReasonAbout()?</div></div></div></blockquote><div><br class=""></div><div>Yes.</div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class="">Supposing that building more complex expressions (if such will be added) might be expensive, something like that could come handy in</div><div class="">controlling the level of detail. Did you mean something like that?</div></div></div></blockquote><div><br class=""></div>Yes, precisely, the logic is currently all over the place, so we don’t even know whether we get any performance benefit from dropping the constraints.</div><div>Having logic in one place behind the flag would at least let us perform an evaluation and to see whether the optimization is worth it.</div><div><br class=""></div><div>I would say it’s a fairly important stretch goal, due to the fact that as we have seen, very many useful constraints are getting dropped.</div><div><br class=""><blockquote type="cite" class=""><div class=""><div dir="ltr" class=""><div class=""><br class=""></div><div class="">Thanks,</div><div class="">Réka</div><div class=""><br class=""></div><div class=""><br class=""><div class="gmail_extra"><br class=""><div class="gmail_quote">2018-03-25 22:26 GMT+02:00 George Karpenkov <span dir="ltr" class=""><<a href="mailto:ekarpenkov@apple.com" target="_blank" class="">ekarpenkov@apple.com</a>></span>:<br class=""><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div style="word-wrap:break-word;line-break:after-white-space" class="">Hi Réka,<div class=""><br class=""></div><div class="">Great! I think it would be beneficial to add an example where the “complex” constraint is dropped before even being added to the environment,</div><div class="">and add a stretch goal of fixing those (e.g. by unifying a place where the constraints are dropped, and adding a flag guarding that).</div><span class="m_2379769367196519423HOEnZb"><font color="#888888" class=""><div class=""><br class=""></div></font></span><div class=""><span class="m_2379769367196519423HOEnZb"><font color="#888888" class="">George</font></span><div class=""><div class="m_2379769367196519423h5"><br class=""><div class=""><br class=""><blockquote type="cite" class=""><div class="">On Mar 24, 2018, at 1:52 PM, Réka Nikolett Kovács <<a href="mailto:rekanikolett@gmail.com" target="_blank" class="">rekanikolett@gmail.com</a>> wrote:</div><br class="m_2379769367196519423m_3387306277682206925Apple-interchange-newline"><div class=""><div dir="ltr" class=""><div class="">Hi,</div><div class=""><br class=""></div><div class="">I'd like to add my own version of a Z3 integration proposal draft:</div><div class=""><br class=""></div><a href="https://docs.google.com/document/d/1Qpw_rQ8-JFJJtqyJz8YBqui-FNcBgJJvpLBvPcCzHV4/edit?usp=sharing" target="_blank" class="">https://docs.google.com/docume<wbr class="">nt/d/1Qpw_rQ8-JFJJtqyJz8YBqui-<wbr class="">FNcBgJJvpLBvPcCzHV4/edit?usp=s<wbr class="">haring</a><br class=""><div class=""><br class=""></div><div class="">Any feedback would be much appreciated.</div><div class=""><br class=""></div><div class="">Thanks,</div><div class="">Réka</div></div>

</div></blockquote></div><br class=""></div></div></div></div></blockquote></div><br class=""></div></div></div>

</div></blockquote></div><br class=""></body></html>