<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="">Also please don’t forget to submit the PDF of the final proposal *using the GSoC website*!<br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Mar 26, 2018, at 2:12 PM, George Karpenkov via cfe-dev <<a href="mailto:cfe-dev@lists.llvm.org" class="">cfe-dev@lists.llvm.org</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class="Apple-interchange-newline"><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 class="" 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); float: none; display: inline;">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 class=""><br class=""></div><div class="">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 class=""><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 style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">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 style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><br class=""></div><div style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class="">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 style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><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 class="Apple-converted-space"> </span><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: 0px 0px 0px 0.8ex; border-left-width: 1px; border-left-style: solid; border-left-color: rgb(204, 204, 204); padding-left: 1ex;"><div class="" style="word-wrap: break-word; line-break: after-white-space;">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="" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;"><span style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">_______________________________________________</span><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><span style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; float: none; display: inline !important;" class="">cfe-dev mailing list</span><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><a href="mailto:cfe-dev@lists.llvm.org" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;" class="">cfe-dev@lists.llvm.org</a><br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><a href="http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;" class="">http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev</a></div></blockquote></div><br class=""></body></html>