Changing Model.constraints, and Reduction.new_top to be a Vec<Expression> #435
Conversation
|
@niklasdewally @ozgurakgun Since we are changing I'm asking this because in rewrite_iteration expression is not a Vec<>, and I'm not sure how to handle that. fn rewrite_iteration<'a>(
expression: &'a Vec<Expression>,
model: &'a Model,
rules: &'a Vec<&'a Rule<'a>>,
apply_optimizations: bool,
stats: &mut RewriterStats,
) -> Option<Reduction> {
if apply_optimizations && expression.is_clean() { // should we use expression.first in here???
// Skip processing this expression if it's clean
return None;
}
// Mark the expression as clean - will be marked dirty if any rule is applied
let mut expression = expression.clone();
let rule_results = apply_all_rules(&expression, model, rules, stats); // should we try to iterate through the Vector, or expression.first would be just fine?
if let Some(new) = choose_rewrite(&rule_results, &expression) {
// If a rule is applied, mark the expression as dirty
return Some(new);
}
let mut sub = expression.children();
for i in 0..sub.len() {
if let Some(red) = rewrite_iteration(&sub[i], model, rules, apply_optimizations, stats) {
sub[i] = red.new_expression;
let res = expression.with_children(sub.clone());
return Some(Reduction::new(res, red.new_top, red.symbols));
}
}
// If all children are clean, mark this expression as clean
if apply_optimizations {
assert!(expression.children().iter().all(|c| c.is_clean()));
expression.set_clean(true);
return Some(Reduction::pure(expression));
}
None
} |
We currently have a top level |
|
Agreed. So the vector can, and often will, contain multiple expressions in it. |
|
to me it looks like rewrite_iteration should operate on expressions, not vectors. we aren't rewriting vectors of expressions at a time after all? |
|
Good point. |
YehorBoiar
force-pushed
the
exp_to_vector
branch
from
db6441b
to
cec2eab
Compare
|
I run into the same problem I had last time. For some reason on some models it's getting in an infinite loop, but I don't know exactly where and why. I'm planning to run it in a debug mode, but I don't know how. @niklasdewally Can you tell me how to do that?I want to run |
| &mut stats, | ||
| ) { | ||
| step.apply(&mut new_model); // Apply side-effects (e.g. symbol table updates) | ||
| let constraints = new_model.constraints.clone(); |
There was a problem hiding this comment.
fine for now, but just to note that in gen_reduce (or whatever it's called) this for loop shouldn't be necessary. it's a container containing expressions, the top level container can be a vector of expressions or just an expression, it shouldn't matter via uniplate/biplate. fyi @lixitrixi @niklasdewally @YehorBoiar
There was a problem hiding this comment.
So, we can just use model.constraints.transform instead?
There was a problem hiding this comment.
It would be a <_ as Biplate<Expr>>::descend_bi(constraints,fn) i think.
If you only want to operate on your immediate children, use descend not transform.
There was a problem hiding this comment.
I have a mutable iterator in the roadmap which also work nicely here, but for now descend_bi is the better option.
|
is the debugging section here useful: https://code.visualstudio.com/docs/languages/rust assuming you are using vs code. |
|
RUST_LOG= cargo run -- --verbose INFO is the default log level, if thats all you need, no need to set rustlog, just use --verbose. INFO logs will give you "rule was applied", which might be enough, otherwise use TRACE. I would try info first as trace is very chatty... |
If not, the default binaries created by cargo build, stored in target/debug, have debug symbols for rust-gdb. |
|
I cancelled the CI runs manually and added time limits to CI jobs in #437 |
YehorBoiar
force-pushed
the
exp_to_vector
branch
2 times, most recently
from
ef509c5
to
e897aff
Compare
YehorBoiar
force-pushed
the
exp_to_vector
branch
from
e897aff
to
fdd8dc4
Compare
Code and Documentation Coverage ReportDocumentation CoverageClick to view documentation coverage for this PRClick to view documentation coverage for mainCode Coverage SummaryThis PR: Detailed Report Main: Detailed Report Coverage Main & PR Coverage ChangeLines coverage changed by -7.60% and covered lines changed by -612
Functions coverage changed by -8.10% and covered lines changed by -84
Branches... coverage: No comparison data available |
|
@ozgurakgun I don't understand how apply() function should be written. Here is what I understand: Although we changed the constraint field in our model construct, it’s still a conjunction. However, this change affects how we apply rules to it. Here is what my approach was: My approach doesn't work, and I can't figure out why. |
|
@YehorBoiar curious that it just seems to be the test tests_integration_eprime_minion_bool_literals_to_wlit_1 that failed... |
|
I've took a quick look, and it seems that we have a stray |
|
@YehorBoiar - did you see my comment above? you didn't respond to that. |
|
@niklasdewally Do you have any clues why it could happen? |
I'm not too familiar with this PR or the rewriter in general unfortunately. |
| // Apply side-effects (e.g. symbol table updates | ||
| pub fn apply(self, model: &mut Model) { | ||
| // Apply side-effects (e.g. symbol table updates) | ||
| pub fn apply(self, model: &mut Model, constraint_idx: usize) { |
There was a problem hiding this comment.
passing the constraint id into apply looks suspicious to me. why do you need to do this?
There was a problem hiding this comment.
We needed this to target reductions to a specific constraint instead of applying them to the whole model like before. But I just realized how this could go wrong. For instance, if we add a constraint to the start of the model, we would not attempt to apply reductions to it, leaving one dirty node that never gets processed.
I’ll try applying reductions to the entire vector of constraints each time we attempt to reduce the model. If my assumption is correct, this should work!
There was a problem hiding this comment.
I tried naively implement it through the while loop
let mut changed = true;
while changed {
changed = false; // Reset change tracker
// Iterate over all constraints
for i in 0..new_model.constraints.len() {
while let Some(step) = rewrite_iteration(
&new_model.constraints[i],
&new_model,
&rules,
apply_optimizations,
&mut stats,
) {
step.apply(&mut new_model, i); // Apply reduction
changed = true; // Track that a change occurred
}
}
} but it didn't work either.
Addressing your suspicion, I could try to pass a direct reference to a constraint in apply() function, but I don't see how it would be different from what I am doing right now.
There was a problem hiding this comment.
For instance, if we add a constraint to the start of the model, we would not attempt to apply reductions to it, leaving one dirty node that never gets processed.
Shouldn't it rewrite until the entire model is clean?
There was a problem hiding this comment.
On further reflection I think this is a stop gap, working constraint by constraint, but we should make it work like this before designing the ultimate version. I'll try this afternoon to see what's breaking.
There was a problem hiding this comment.
@niklasdewally Yes, it should, and I was thinking that it doesn't so I tried to fix it. Apparently, it wasn't the problem
There was a problem hiding this comment.
@ozgurakgun Okay, thank you for help!
There was a problem hiding this comment.
sorry I am failing to find time to look into this, but it's on the list. feel free to keep trying :)
updating the branch to track main is probably a good idea.
This PR is created to address the issue #421.