Open YehorBoiar opened 1 week ago
@niklasdewally @ozgurakgun Since we are changing Model.constraints
to a Vec<Expression>
, should we assume it will always contain only one expression, or is it acceptable to have multiple expressions in constraints?
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
}
@niklasdewally @ozgurakgun Since we are changing
Model.constraints
to aVec<Expression>
, should we assume it will always contain only one expression, or is it acceptable to have multiple expressions in constraints?
We currently have a top level And
containing many expressions, the top level vector would just replace this.
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.
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 conjure_oxide/tests/integration/basic/div/01/input.essence
is the debugging section here useful: https://code.visualstudio.com/docs/languages/rust
assuming you are using vs code.
RUST_LOG=
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...
is the debugging section here useful: https://code.visualstudio.com/docs/languages/rust
assuming you are using vs code.
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
@ozgurakgun I don't understand how apply() function should be written.
Here is what I understand: Our model is still a conjunction of rules. Previously, we represented this conjunction as a single Expression, and the apply() function rewrote the entire tree into a new_expression plus new_top (if it existed) after applying reductions.
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: I iterate through the vector of constraints and try to reduce each constraint separately. I don’t check if new_top is empty; I always add it to the constraint vector. After that, I replace the current model with the reduced model obtained from rewrite_iteration.
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... Run this test through cargo run and stick the logs on pastebin/gist and I'll be happy to take a look
I've took a quick look, and it seems that we have a stray FactorE
in the final model that hasn't been ran through boolean_literal_to_wliteral for whatever reason
@YehorBoiar - did you see my comment above? you didn't respond to that.
@niklasdewally Do you have any clues why it could happen?
@niklasdewally Do you have any clues why it could happen?
I'm not too familiar with this PR or the rewriter in general unfortunately.
I just thought of a possible approach - in rewrite_model
, why don't we just turn the top level vector into an And
before passing it to the engine? I know development on rewriting a vector of expressions instead is already pretty far ahead, so just a thought.
This would minimise the conflicts between our rewrite engine and the new model structure (like the new boolean bug Ty mentioned to me), while still keeping the better representation of a vector.
I just thought of a possible approach - in
rewrite_model
, why don't we just turn the top level vector into anAnd
before passing it to the engine? I know development on rewriting a vector of expressions instead is already pretty far ahead, so just a thought.This would minimise the conflicts between our rewrite engine and the new model structure (like the new boolean bug Ty mentioned to me), while still keeping the better representation of a vector.
I don't have an opinion either way, but I would like to point out that that bool bug was just bad code on my part and nothing to do with this pr
most importantly I think you want to update this branch to main and see how far you get. is it still broken? if so, what happens?
conjure-oxide seems to work fine when running cargo run
on models. However ACCEPT=true cargo test
gives me bunch of poison errors that point to this line of code
206 let expected_rule_trace = read_rule_trace(path, essence_base, "expected")?;
207 let generated_rule_trace = read_rule_trace(path, essence_base, "generated")?;
208
209 assert_eq!(expected_rule_trace, generated_rule_trace);
This is a problem that I addressed in issue #476. We don't rewrite the generated_rule_trace into expected_rule_trace on ACCEPT=true. I'm doing it manually for now, but I know that @Soph1514 and @a-nosnitram are working on it
conjure-oxide seems to work fine when running
cargo run
on models. HoweverACCEPT=true cargo test
gives me bunch of poison errors that point to this line of code206 let expected_rule_trace = read_rule_trace(path, essence_base, "expected")?; 207 let generated_rule_trace = read_rule_trace(path, essence_base, "generated")?; 208 209 assert_eq!(expected_rule_trace, generated_rule_trace);
This is a problem that I addressed in issue #476. We don't rewrite the generated_rule_trace into expected_rule_trace on ACCEPT=true. I'm doing it manually for now, but I know that @Soph1514 and @a-nosnitram are working on it
I have just finished implementing it. Waiting on @a-nosnitram to add me her repository since I do not have access to her branch connected to pr #478
Yesterday me and @lixitrixi resolved one bug. The bug was that when we were running cargo test, one tests was panicking and poisoning all following tests. The fix was to just do .unwrap_or_else(|e| e.into_inner())
instead of doing just unwrap()
.
Tests still don't pass though. Sometimes our rule engine doesn't apply rules that it supposed to apply. For example in basic/div/04 it doesn't apply the very last rule that main is applying
Here are last 3 rules that we get to apply on main
2024-11-23T13:32:50.032579Z INFO conjure_core::rule_engine::rewrite: Rule applicable: distribute_not_over_and ([("Base", 8400)]), to expression: Not(And([(c != 0)])), resulting in: Not((c != 0)), new_top: And([])
at crates/conjure_core/src/rule_engine/rewrite.rs:374
2024-11-23T13:32:50.829650Z WARN conjure_core::rule_engine::rewrite: Multiple rules of different priorities are applicable to expression Not(Metadata { clean: false, etype: None }, Neq(Metadata { clean: false, etype: None }, Atomic(Metadata { clean: false, etype: None }, Reference(UserName("c"))), Atomic(Metadata { clean: false, etype: None }, Literal(Int(0)))))
resulting in expression: Eq(Metadata { clean: false, etype: None }, Atomic(Metadata { clean: false, etype: None }, Reference(UserName("c"))), Atomic(Metadata { clean: false, etype: None }, Literal(Int(0))))
Rules[Rule { name: "negated_neq_to_eq", application: 0x55dfe8303c40, rule_sets: [("Base", 8800)] }, Rule { name: "not_constraint_to_reify", application: 0x55dfe830c810, rule_sets: [("Minion", 4090)] }]
at crates/conjure_core/src/rule_engine/rewrite.rs:432
2024-11-23T13:32:50.833835Z INFO conjure_core::rule_engine::rewrite: Rule applicable: negated_neq_to_eq ([("Base", 8800)]), to expression: Not((c != 0)), resulting in: (c = 0), new_top: And([])
at crates/conjure_core/src/rule_engine/rewrite.rs:374
2024-11-23T13:32:52.065701Z WARN conjure_core::rules::constant: Unimplemented constant eval, expr: __0 =aux SafeDiv(b, c)
at crates/conjure_core/src/rules/constant.rs:90
2024-11-23T13:32:52.155994Z INFO conjure_core::rule_engine::rewrite: Rule applicable: introduce_diveq ([("Minion", 4200)]), to expression: __0 =aux SafeDiv(b, c), resulting in: DivEq(b, c, __0), new_top: And([])
at crates/conjure_core/src/rule_engine/rewrite.rs:374
Here are last 2 rules that we get to apply on exp_to_vector branch
2024-11-23T13:33:40.069080Z INFO conjure_core::rule_engine::rewrite: Rule applicable: distribute_not_over_and ([("Base", 8400)]), to expression: Not(And([(c != 0)])), resulting in: Not((c != 0)), new_top_string: []
at crates/conjure_core/src/rule_engine/rewrite.rs:377
2024-11-23T13:33:40.644623Z WARN conjure_core::rule_engine::rewrite: Multiple rules of different priorities are applicable to expression Not(Metadata { clean: false, etype: None }, Neq(Metadata { clean: false, etype: None }, Atomic(Metadata { clean: false, etype: None }, Reference(UserName("c"))), Atomic(Metadata { clean: false, etype: None }, Literal(Int(0)))))
resulting in expression: Eq(Metadata { clean: false, etype: None }, Atomic(Metadata { clean: false, etype: None }, Reference(UserName("c"))), Atomic(Metadata { clean: false, etype: None }, Literal(Int(0))))
Rules[Rule { name: "negated_neq_to_eq", application: 0x55a6f2b490c0, rule_sets: [("Base", 8800)] }, Rule { name: "not_constraint_to_reify", application: 0x55a6f2b51850, rule_sets: [("Minion", 4090)] }]
at crates/conjure_core/src/rule_engine/rewrite.rs:435
2024-11-23T13:33:40.649778Z INFO conjure_core::rule_engine::rewrite: Rule applicable: negated_neq_to_eq ([("Base", 8800)]), to expression: Not((c != 0)), resulting in: (c = 0), new_top_string: []
at crates/conjure_core/src/rule_engine/rewrite.rs:377
Building model...
Error: model invalid: expected a constant, but got `SafeDiv(Metadata { clean: false, etype: None }, Atomic(Metadata { clean: false, etype: None }, Reference(UserName("b"))), Atomic(Metadata { clean: false, etype: None }, Reference(UserName("c"))))`
I need to check if it even tries to apply something to our SafeDiv, but I forgot how we did during our last meeting. Can you remind me? @TAswan @ozgurakgun
This PR: Detailed Report
lines......: 24.7% (1475 of 5976 lines)
functions..: 28.1% (180 of 640 functions)
branches...: no data found
Main: Detailed Report
lines......: 79.7% (5074 of 6363 lines)
functions..: 62.8% (446 of 710 functions)
branches...: no data found
Lines coverage changed by -55.00% and covered lines changed by -3599
Functions coverage changed by -34.70% and covered lines changed by -266
Branches... coverage: No comparison data available
This PR is created to address the issue #421.