Mine Experiment with Running Rules

core-relations/src/table/mod.rs

@@ -401,6 +401,10 @@ impl Table for SortedWritesTable {
     fn as_any(&self) -> &dyn Any {
         self
     }
+
+    fn as_any_mut(&mut self) -> &mut dyn Any {
+        self
+    }
     fn clear(&mut self) {
         self.pending_state.clear();
         if self.data.data.len() == 0 {
@@ -620,6 +624,12 @@ impl Table for SortedWritesTable {
     }
 }
 
+impl SortedWritesTable {
+    pub fn set_merge(&mut self, merge: Box<MergeFn>) {
+        self.merge = merge.into();
+    }
+}
+
 impl SortedWritesTable {
     /// Create a new [`SortedWritesTable`] with the given number of keys,
     /// columns, and an optional sort column.

core-relations/src/table_spec.rs

@@ -27,7 +27,7 @@ use crate::{
     offsets::{RowId, Subset, SubsetRef},
     pool::{with_pool_set, PoolSet, Pooled},
     row_buffer::{RowBuffer, TaggedRowBuffer},
-    QueryEntry, TableId, Variable,
+    DisplacedTable, DisplacedTableWithProvenance, QueryEntry, TableId, Variable,
 };
 
 define_id!(pub ColumnId, u32, "a particular column in a table");
@@ -183,6 +183,9 @@ pub trait Table: Any + Send + Sync {
     /// `self`.
     fn as_any(&self) -> &dyn Any;
 
+    /// A mutable variant of [`Table::as_any`] for downcasting.
+    fn as_any_mut(&mut self) -> &mut dyn Any;
+
     /// The schema of the table.
     ///
     /// These are immutable properties of the table; callers can assume they
@@ -542,8 +545,17 @@ impl<'de> Deserialize<'de> for WrappedTable {
         D: serde::Deserializer<'de>,
     {
         let inner: Box<dyn Table> = Deserialize::deserialize(deserializer)?;
-
-        let wrapper = wrapper::<SortedWritesTable>(); // todo: different kind of wrapper?
+        let wrapper = if inner.as_any().is::<SortedWritesTable>() {
+            wrapper::<SortedWritesTable>()
+        } else if inner.as_any().is::<DisplacedTable>() {
+            wrapper::<DisplacedTable>()
+        } else if inner.as_any().is::<DisplacedTableWithProvenance>() {
+            wrapper::<DisplacedTableWithProvenance>()
+        } else {
+            return Err(serde::de::Error::custom(
+                "unknown table type for WrappedTable",
+            ));
+        };
 
         Ok(WrappedTable { inner, wrapper })
     }
@@ -564,6 +576,10 @@ impl WrappedTable {
         }
     }
 
+    pub fn as_any_mut(&mut self) -> &mut dyn Any {
+        self.inner.as_any_mut()
+    }
+
     pub(crate) fn as_ref(&self) -> WrappedTableRef<'_> {
         WrappedTableRef {
             inner: &*self.inner,

core-relations/src/uf/mod.rs

@@ -279,6 +279,10 @@ impl Table for DisplacedTable {
     fn as_any(&self) -> &dyn Any {
         self
     }
+
+    fn as_any_mut(&mut self) -> &mut dyn Any {
+        self
+    }
     fn spec(&self) -> TableSpec {
         let mut uncacheable_columns = DenseIdMap::default();
         // The second column of this table is determined dynamically by the union-find.
@@ -882,6 +886,10 @@ impl Table for DisplacedTableWithProvenance {
     fn as_any(&self) -> &dyn Any {
         self
     }
+
+    fn as_any_mut(&mut self) -> &mut dyn Any {
+        self
+    }
     fn clear(&mut self) {
         self.base.clear()
     }

egglog-bridge/src/lib.rs

@@ -768,6 +768,7 @@ impl EGraph {
             incremental_rebuild_rules: Default::default(),
             nonincremental_rebuild_rule: RuleId::new(!0),
             default_val: default,
+            merge: merge.clone(),
             can_subsume,
             name,
         });
@@ -1135,6 +1136,43 @@ impl EGraph {
         updated
     }
 
+    pub fn restore_deserialized_runtime(&mut self) {
+        let funcs = self
+            .funcs
+            .iter()
+            .map(|(func, info)| {
+                (
+                    func,
+                    info.table,
+                    info.schema.clone(),
+                    info.can_subsume,
+                    info.name.clone(),
+                    info.merge.clone(),
+                )
+            })
+            .collect::<Vec<_>>();
+        for (func, table_id, schema, can_subsume, name, merge) in funcs {
+            let schema_math = SchemaMath {
+                tracing: self.tracing,
+                subsume: can_subsume,
+                func_cols: schema.len(),
+            };
+            let merge_fn = merge.to_callback(schema_math, &name, self);
+            let table = self
+                .db
+                .get_table_mut(table_id)
+                .as_any_mut()
+                .downcast_mut::<SortedWritesTable>()
+                .expect("function tables must use SortedWritesTable");
+            table.set_merge(merge_fn);
+            let incremental_rebuild_rules = self.incremental_rebuild_rules(func, &schema);
+            let nonincremental_rebuild_rule = self.nonincremental_rebuild(func, &schema);
+            let info = &mut self.funcs[func];
+            info.incremental_rebuild_rules = incremental_rebuild_rules;
+            info.nonincremental_rebuild_rule = nonincremental_rebuild_rule;
+        }
+    }
+
     pub fn set_report_level(&mut self, level: ReportLevel) {
         self.report_level = level;
     }
@@ -1163,6 +1201,7 @@ struct FunctionInfo {
     incremental_rebuild_rules: Vec<RuleId>,
     nonincremental_rebuild_rule: RuleId,
     default_val: DefaultVal,
+    merge: MergeFn,
     can_subsume: bool,
     name: Arc<str>,
 }
@@ -1185,6 +1224,7 @@ pub enum DefaultVal {
 }
 
 /// How to resolve FD conflicts for a table.
+#[derive(Clone, Serialize, Deserialize)]
 pub enum MergeFn {
     /// Panic if the old and new values don't match.
     AssertEq,

infra/nightly-resources/web/chart.js

@@ -197,7 +197,7 @@ function initializeCharts() {
             },
           },
           y: {
-            stacked: false,
+            stacked: true,
             title: {
               display: true,
               text: "Time (ms)",

infra/nightly-resources/web/data.js

@@ -59,6 +59,7 @@ function initializeGlobalData() {
   GLOBAL_DATA.extractChart = null;
   GLOBAL_DATA.differenceChart = null;
   GLOBAL_DATA.minedChart = null;
+  GLOBAL_DATA.mineData = {};
 
   return fetch("data/data.json")
     .then((response) => response.json())
@@ -86,22 +87,11 @@ function processRawData(blob) {
     if (!GLOBAL_DATA.data[suite]) {
       return;
     }
-    // Aggregate commands across all timelines
     const times = {
       benchmark,
-      ...Object.fromEntries(CMDS.map((cmd) => [cmd, []])),
-      other: [],
+      ...aggregateTimelinesByCommand(timelines),
     };
 
-    timelines.forEach(({ events, sexps }) => {
-      events.forEach((time_micros, idx) => {
-        const cmd = getCmd(sexps[idx]);
-
-        // Group times by command type
-        times[getCmdType(cmd)].push(time_micros / 1000); // we measure microseconds, but for charts, it's nicer to show in ms
-      });
-    });
-
     GLOBAL_DATA.data[suite][runMode][benchmark] = times;
   });
 }

infra/nightly-resources/web/mined.html

@@ -29,7 +29,21 @@ <h2>POACH vs Vanilla Egglog</h2>
     <div style="max-height: 800px;">
       <canvas class="content" id="mined-chart"></canvas>
     </div>
+
+    <h3>Extraction Cost Summary (easteregg)</h3>
+    <table id="mine-summary-table">
+      <thead>
+        <tr>
+          <th>benchmark name</th>
+          <th># extracts</th>
+          <th>avg initial cost</th>
+          <th>avg final cost</th>
+          <th>avg cost difference</th>
+        </tr>
+      </thead>
+      <tbody id="mine-summary-body"></tbody>
+    </table>
   </div>
 </body>
 
-</html>
+</html>

infra/nightly-resources/web/mined.js

@@ -1,45 +1,137 @@
 function initialize() {
-  initializeGlobalData().then(initializeCharts).then(plotMine);
+  Promise.all([initializeGlobalData(), loadMineData()])
+    .then(initializeCharts)
+    .then(() => {
+      plotMine();
+      renderMineSummaryTable();
+    });
 }
 
-function plotMine() {
-  const mega_mined = GLOBAL_DATA.data.easteregg["mine-mega"];
-  const indiv_mined = GLOBAL_DATA.data.easteregg["mine-indiv"];
-  const baseline = GLOBAL_DATA.data.easteregg.timeline;
+function loadMineData() {
+  return fetch("data/mine-data.json")
+    .then((response) => response.json())
+    .then((data) => {
+      GLOBAL_DATA.mineData = data;
+    })
+    .catch((error) => {
+      console.error("Failed to load mine-data.json", error);
+      GLOBAL_DATA.mineData = {};
+    });
+}
 
+function plotMine() {
   if (GLOBAL_DATA.minedChart === null) {
     return;
   }
 
-  const benchmarks = Object.keys(baseline);
-
-  const data = {};
-
-  benchmarks.forEach((b) => {
-    data[b] = {};
-
-    data[b].baseline = benchmarkTotalTime(baseline[b]);
-    data[b].mega_mined = benchmarkTotalTime(mega_mined[b]);
-    data[b].indiv_mined = benchmarkTotalTime(indiv_mined[b]);
-  });
+  const benchmarks = Object.keys(GLOBAL_DATA.mineData).sort();
+  const byBenchmark = Object.fromEntries(
+    benchmarks.map((b) => {
+      const baseline = aggregateTimelinesByCommand(
+        GLOBAL_DATA.mineData[b].baseline_timeline,
+      );
+      const mega = aggregateTimelinesByCommand(
+        GLOBAL_DATA.mineData[b].mine_mega_timeline,
+      );
+      const indiv = aggregateTimelinesByCommand(
+        GLOBAL_DATA.mineData[b].mine_indiv_timeline,
+      );
+      return [
+        b,
+        {
+          baseline: {
+            run: aggregate(baseline.run, "total"),
+            extract: aggregate(baseline.extract, "total"),
+          },
+          mega: {
+            run: aggregate(mega.run, "total"),
+            extract: aggregate(mega.extract, "total"),
+          },
+          indiv: {
+            run: aggregate(indiv.run, "total"),
+            extract: aggregate(indiv.extract, "total"),
+          },
+        },
+      ];
+    }),
+  );
 
   GLOBAL_DATA.minedChart.data = {
     labels: benchmarks,
     datasets: [
       {
-        label: "baseline",
-        data: Object.values(data).map((d) => d.baseline),
+        label: "baseline: run",
+        stack: "baseline",
+        backgroundColor: "#1e3a8a",
+        data: benchmarks.map((b) => byBenchmark[b].baseline.run),
+      },
+      {
+        label: "baseline: extract",
+        stack: "baseline",
+        backgroundColor: "#60a5fa",
+        data: benchmarks.map((b) => byBenchmark[b].baseline.extract),
+      },
+      {
+        label: "mined (mega): run",
+        stack: "mega",
+        backgroundColor: "#b91c1c",
+        data: benchmarks.map((b) => byBenchmark[b].mega.run),
+      },
+      {
+        label: "mined (mega): extract",
+        stack: "mega",
+        backgroundColor: "#f472b6",
+        data: benchmarks.map((b) => byBenchmark[b].mega.extract),
       },
       {
-        label: "mined (mega)",
-        data: Object.values(data).map((d) => d.mega_mined),
+        label: "mined (indiv): run",
+        stack: "indiv",
+        backgroundColor: "#166534",
+        data: benchmarks.map((b) => byBenchmark[b].indiv.run),
       },
       {
-        label: "mined (indiv)",
-        data: Object.values(data).map((d) => d.indiv_mined),
+        label: "mined (indiv): extract",
+        stack: "indiv",
+        backgroundColor: "#86efac",
+        data: benchmarks.map((b) => byBenchmark[b].indiv.extract),
       },
     ],
   };
 
   GLOBAL_DATA.minedChart.update();
 }
+
+function renderMineSummaryTable() {
+  const tableBody = document.getElementById("mine-summary-body");
+  if (!tableBody) {
+    return;
+  }
+
+  const rows = Object.entries(GLOBAL_DATA.mineData)
+    .sort(([a], [b]) => a.localeCompare(b))
+    .map(([benchmarkName, data]) => {
+      const entries = data.mine_mega_extracts || [];
+      const extractCount = entries.length;
+      const initialTotal = entries.reduce(
+        (sum, entry) => sum + entry.initial_cost,
+        0,
+      );
+      const finalTotal = entries.reduce(
+        (sum, entry) => sum + entry.final_cost,
+        0,
+      );
+      const avgInitialCost =
+        extractCount === 0 ? 0 : initialTotal / extractCount;
+      const avgFinalCost = extractCount === 0 ? 0 : finalTotal / extractCount;
+      return `
+        <tr>
+          <td>${benchmarkName}</td>
+          <td>${extractCount}</td>
+          <td>${avgInitialCost}</td>
+          <td>${avgFinalCost}</td>
+        </tr>
+      `;
+    });
+
+  tableBody.innerHTML = rows.join("\n");
+}