Explore crepe #3440
Explore crepe #3440
Conversation
| for v in env.single_occurrence_variables().cloned(), | ||
| AlgebraicConstraint(e), | ||
| ContainsVariable(e, v2), | ||
| (v == v2); |
There was a problem hiding this comment.
Could this be simplified by replacing ContainsVariable(e, v2), (v == v2)
with just ContainsVariable(e, v)?
There was a problem hiding this comment.
it somehow does not work when you do this, I think it's related to the "for".
| HasProductSummand(e, x2, v2_), | ||
| (x2 != v1_), | ||
| (x1 != v2_), | ||
| AffineExpression(v2_, coeff2, v2, offset2), |
There was a problem hiding this comment.
Why does this rule only check the coefficients of v1_ and v2_, but not the
coefficients of x1 and x2? Since x1 and x2 are expressions, they could
also contain affine parts. Is the idea that this rule will be applied
iteratively to catch those cases?why here only consider the coefficients of v1_ and v2_, but not the coefficients of x1, x2, they are expressions and can have coefficients, or is this intend to do it iteratively?
There was a problem hiding this comment.
Yes, it is applied iteratively, I don't see a way how to do an arbitrary number of variables with such rules (all items predicates need to be Copy)
|
|
||
| // Algebraic constraints: | ||
| cmp_result_0 * (cmp_result_0 - 1) = 0 | ||
| (1 - cmp_result_0) * a__0_0 = 0 |
There was a problem hiding this comment.
Why does it not remove these?
| (1 - cmp_result_2) * (a__0_2 - b__0_2) = 0 | ||
| (1 - cmp_result_2) * (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1) = 0 | ||
| ((opcode_loadb_flag0_1 - 1) * shifted_read_data__1_1 + opcode_loadb_flag0_0 * shifted_read_data__0_0 + (1 - opcode_loadb_flag0_0) * shifted_read_data__1_0 - opcode_loadb_flag0_1 * shifted_read_data__0_1) * diff_inv_marker__0_2 + (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1) * diff_inv_marker__1_2 + (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1) * diff_inv_marker__2_2 + (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1) * diff_inv_marker__3_2 - cmp_result_2 = 0 | ||
| free_var_103 * ((a__0_2 - b__0_2) * (a__0_2 - b__0_2) + (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1) * (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1) + (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1) * (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1) + (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1) * (255 * data_most_sig_bit_0 - 255 * data_most_sig_bit_1)) - cmp_result_2 = 0 |
There was a problem hiding this comment.
Since this rule increases the degree, we should maybe only run it after inlining.
| // Here, we have e = coeff1 * v1 * x1 + coeff2 * v2 * x2 + ... | ||
| RangeConstraintOnExpression(x1, rc1), | ||
| RangeConstraintOnExpression(x2, rc2), | ||
| let Some(replacement) = (|| { |
There was a problem hiding this comment.
This code should be simplified
|
After we get a basic version of this merged (that potentially already replaces some functionality in the solver), a next goal would be to reduce the number of variables before constructing the solver, to reduce its runtime. All flags are boolean, so they must all be zero. I think the general case here could be something like If the RC of an affine expression is not the default and its lower bound matches the constant, then all components have to be "minimal". |
No description provided.