Skip to content

Commit

Permalink
fix bug for no variable queries
Browse files Browse the repository at this point in the history
  • Loading branch information
oflatt committed Feb 15, 2024
1 parent 76cb253 commit ad8a06b
Show file tree
Hide file tree
Showing 4 changed files with 73 additions and 18 deletions.
64 changes: 46 additions & 18 deletions src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -470,6 +470,17 @@ impl Default for EGraph {
#[error("Not found: {0}")]
pub struct NotFoundError(Expr);

/// For each rule, we produce a `SearchResult`
/// storing data about that rule's matches.
/// When a rule has no variables, it may still match- in this case
/// the `matched` field is used.
struct SearchResult {
name: Symbol,
all_matches: Vec<Value>,
did_match: bool,
rule_search_time: Duration,
}

impl EGraph {
/// Use the rust backend implimentation of eqsat,
/// including a rust implementation of the union-find
Expand Down Expand Up @@ -936,13 +947,15 @@ impl EGraph {
let search_start = Instant::now();
let mut searched = vec![];
for (name, rule) in copy_rules.iter() {
let mut all_values = vec![];
let mut all_matches = vec![];
if rule.banned_until <= iteration {
let mut fuel = safe_shl(match_limit, rule.times_banned);
let rule_search_start = Instant::now();
let mut did_match = false;
self.run_query(&rule.query, rule.todo_timestamp, |values| {
did_match = true;
assert_eq!(values.len(), rule.query.vars.len());
all_values.extend_from_slice(values);
all_matches.extend_from_slice(values);
if fuel > 0 {
fuel -= 1;
Ok(())
Expand All @@ -954,9 +967,14 @@ impl EGraph {
log::trace!(
"Searched for {name} in {:.3}s ({} results)",
rule_search_time.as_secs_f64(),
all_values.len()
all_matches.len()
);
searched.push((name, all_values, rule_search_time));
searched.push(SearchResult {
name: *name,
all_matches,
rule_search_time,
did_match,
});
}
}

Expand All @@ -968,22 +986,28 @@ impl EGraph {
.or_insert(Duration::default()) += search_elapsed;

let apply_start = Instant::now();
for (name, all_values, search_time) in searched {
let rule = rules.get_mut(name).unwrap();
for search_result in searched {
let SearchResult {
name,
all_matches,
rule_search_time,
did_match,
} = search_result;
let rule = rules.get_mut(&name).unwrap();
// add to the rule's search time
*report
.search_time_per_rule
.entry(*name)
.or_insert(Duration::default()) += search_time;
.entry(name)
.or_insert(Duration::default()) += rule_search_time;
let num_vars = rule.query.vars.len();

// make sure the query requires matches
if num_vars != 0 {
*report.num_matches_per_rule.entry(*name).or_insert(0) +=
all_values.len() / num_vars;
*report.num_matches_per_rule.entry(name).or_insert(0) +=
all_matches.len() / num_vars;

// backoff logic
let len = all_values.len() / num_vars;
let len = all_matches.len() / num_vars;
let threshold = safe_shl(match_limit, rule.times_banned);
if len > threshold {
let ban_length = safe_shl(ban_length, rule.times_banned);
Expand All @@ -999,14 +1023,18 @@ impl EGraph {
let rule_apply_start = Instant::now();

let stack = &mut vec![];
// run one iteration when n == 0

// when there are no variables, a query can still fail to match
// here we handle that case
if num_vars == 0 {
rule.matches += 1;
stack.clear();
self.run_actions(stack, &[], &rule.program, true)
.unwrap_or_else(|e| panic!("error while running actions for {name}: {e}"));
if did_match {
rule.matches += 1;
stack.clear();
self.run_actions(stack, &[], &rule.program, true)
.unwrap_or_else(|e| panic!("error while running actions for {name}: {e}"));
}
} else {
for values in all_values.chunks(num_vars) {
for values in all_matches.chunks(num_vars) {
rule.matches += 1;
stack.clear();
self.run_actions(stack, values, &rule.program, true)
Expand All @@ -1017,7 +1045,7 @@ impl EGraph {
// add to the rule's apply time
*report
.apply_time_per_rule
.entry(*name)
.entry(name)
.or_insert(Duration::default()) += rule_apply_start.elapsed();
}
self.rulesets.insert(ruleset, rules);
Expand Down
9 changes: 9 additions & 0 deletions tests/repro-empty-query.egg
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
(function foo () i64 :merge (min old new))

(rule () ((set (foo) 4)))

(set (foo) 10)

(run 3)

(check (= (foo) 4))
9 changes: 9 additions & 0 deletions tests/repro-equal-constant.egg
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
(function foo () i64 :merge (min old new))

(rule ((= (foo) 5)) ((set (foo) 4)))

(set (foo) 10)

(run 3)

(check (!= (foo) 4))
9 changes: 9 additions & 0 deletions tests/repro-equal-constant2.egg
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
(function foo () i64 :merge (min old new))

(rule ((= (foo) 10)) ((set (foo) 4)))

(set (foo) 10)

(run 3)

(check (= (foo) 4))

0 comments on commit ad8a06b

Please sign in to comment.