Improved bit constraint detection #1461
Conversation
aminlatifi
commented
Jun 23, 2024
aminlatifi
commented
- Ref Improve bit constraint detection #711
Added documentation
| @@ -268,8 +266,67 @@ fn propagate_constraints<T: FieldElement>( | |||
| (known_constraints, remove) | |||
| } | |||
|
|
|||
| /// Get simple expression roots for a given expression. | |||
There was a problem hiding this comment.
Please tell me if the following is correct:
Tries to return the set of roots of a given expression in one variable.
If Some(vec![r1, r2, ... ,rn]) is returned, then the expression is equivalent to (x - r1)*(x - r2) * ... * (x - rn).
Please also change this function to return a tuple of the variable an the vector of roots. Or do you think this return type is better suited in some way?
There was a problem hiding this comment.
Oh, the above is actually not true, it should be equivalent to a nonzero multiple of the product.
There was a problem hiding this comment.
If Some(vec![r1, r2, ... ,rn]) is returned, then the expression is equivalent to (x - r1)*(x - r2) * ... * (x - rn).
This one is correct. If I understood correctly, you need to support (x-r1)(x-r2)...(y-r'1)(y-r'2)*...
and return [(x, [r1,r2,...]),(y,[r'1, r'2,...])]
There was a problem hiding this comment.
No, we cannot support that, for the pattern to match, there can only even be one variable.
| .and_then(|l| l.solve().ok())?; | ||
|
|
||
| match root.constraints[..] { | ||
| [] => Some(vec![]), |
There was a problem hiding this comment.
I think in this case, the expression evaluates to zero and this is a very important specila case: While the numbers returned are all roots in that case, the list is not complete (all numbers are roots).
There was a problem hiding this comment.
So you mean we must return None and don't make any constraint?
| assert!(known_constraints | ||
| .insert(p, RangeConstraint::from_max_bit(0)) | ||
| .is_none()); | ||
| if let Some((p, constraint)) = is_binary_constraint(identity.expression_for_poly_id()) { |
There was a problem hiding this comment.
Now to use the root-finding function in the most general case (that includes the binary one), you should do the following:
Set the constraint to from_range(min, max) and set remove to true if all values from min to max occur in the list.
There was a problem hiding this comment.
I didn't get the it well, can you give more details? You mean I don't use from_mask and use from_range instead? and don't try to make a binary mask which covers all numbers?
chriseth
changed the title
| pub fn get_roots<T: FieldElement>( | ||
| /// Get simple expression roots for a given expression. | ||
| /// | ||
| /// This function recursively evaluates an algebraic expression and attempts |
There was a problem hiding this comment.
This function is very complex, so its description has to be water-tight. It has to define what a root is and so on. I think a wording in the from of "if X is returned, it means the expression is equivalent to ..." would be helpful since it leaves little room for misunderstanding. Also, I don't think we need to explain how the function works, just what it returns.
