<html><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; "><br><div><div>On Aug 26, 2008, at 11:44 PM, Zhongxing Xu wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite"><div dir="ltr"><br><div class="gmail_quote"><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"> Here are some comments!<br> <br> First, I have to be honest that I don't like the name "Assumer" for the actual interface. I think that using the word "Assume" is fine for the methods since that matches with the model-checking terminology (essentially, "Assume" represents a verb, or action, that we are taking with respect to modifying the state). I think the name of the Assumer class should reflect what it represents, which are constraints on the values of state. So I suggest *something* like the following (we can iterate on the precise name):<br> <br> Assumer -> ConstraintsManager<br> <br> This makes it much more clear that the ConstraintsManager manages 'constraints' within the state. We can iterate on the name, but "Assumer" I feel that isn't descriptive enough.<br> <br> I also think this patch is a little incomplete, since the code it introduces doesn't actually get hooked up to GRState. All of the Assume methods in GRStateManager should just forward over to the ConstraintManager object, e.g:<br> <br> class GRStateManager {<br> ...<br> const GRState* Assume(const GRState* St, NonLVal Cond, bool Assumption,<br> bool& isFeasible) {<br> return ConstraintsMgr.Assume(St, *this, Cond, Assumption, isFeasible);<br> }<br> <br> If you actually migrate this core logic over to BasicConstraintsManager (BasicAssumer in your patch), then you can actually run "make test" to see if your patch does the right thing.<br> <font color="#888888"></font></blockquote><div><br>New patch attached. <br></div></div><br></div> <span><constraintmanager.patch></span></blockquote></div><br><div>Looks great! Please apply.</div></body></html>