<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>