Skip to content

Commit 45b70b2

Browse files
committed
Tweak edge costs
This reduces the number of vertices explored during graph solving. typing_1.ml: 143,845 to 135,298 vertices (6% reduction) slow_1.rs: 1,011,157 to 967,941 vertices (4% reduction) Instruction count changes are negligible (typing_1.ml is marginally worse, slow_1.rs is slightly improved), but wall time is down proportionately to vertex count.
1 parent 440aa71 commit 45b70b2

1 file changed

Lines changed: 22 additions & 5 deletions

File tree

src/diff/graph.rs

Lines changed: 22 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -331,10 +331,13 @@ impl Edge {
331331
// TODO: Perhaps prefer matching longer strings? It's
332332
// probably easier to read.
333333

334-
// The cost for unchanged nodes can be as low as 1,
335-
// but we penalise nodes that have a different depth
334+
// We always want non-zero costs, or things get hard
335+
// to reason about.
336+
let base_cost = 1;
337+
338+
// We penalise nodes that have a different depth
336339
// difference, capped at 40.
337-
let base = min(40, depth_difference + 1);
340+
let depth_cost = min(40, depth_difference);
338341

339342
// If the node is only punctuation, increase the
340343
// cost. It's better to have unchanged variable names
@@ -349,10 +352,24 @@ impl Edge {
349352
// If we have replacements either side of a node
350353
// (e.g. see comma_and_comment_1.js), then that's
351354
// potentially a cost difference of 200.
352-
base + if probably_punctuation { 200 } else { 0 }
355+
let punctuation_cost = if probably_punctuation { 200 } else { 0 };
356+
357+
base_cost + depth_cost + punctuation_cost
353358
}
354359
// Matching an outer delimiter is good.
355-
EnterUnchangedDelimiter { depth_difference } => 100 + min(40, depth_difference),
360+
EnterUnchangedDelimiter { depth_difference } => {
361+
// This cost must be less than the novel edges, but
362+
// greater than UnchangedNode.
363+
//
364+
// The shortest route often has a bunch of
365+
// EnterUnchangedDelimiter, so preferring a cost
366+
// closer to UnchangedNode means we explore slightly
367+
// fewer nodes.
368+
let base_cost = 10;
369+
370+
let depth_cost = min(40, depth_difference);
371+
base_cost + depth_cost
372+
}
356373

357374
// Otherwise, we've added/removed a node.
358375
NovelAtomLHS {} | NovelAtomRHS {} => 300,

0 commit comments

Comments
 (0)