Expose extraction support helpers

Author: saulshanabrook

src/lib.rs

@@ -359,6 +359,16 @@ impl Function {
         self.decl.internal_hidden
     }
 
+    /// Whether this table is a constructor or relation table.
+    pub fn is_constructor(&self) -> bool {
+        self.decl.subtype == FunctionSubtype::Constructor
+    }
+
+    /// Whether this constructor is excluded from ordinary extraction.
+    pub fn is_unextractable(&self) -> bool {
+        self.decl.unextractable
+    }
+
     /// The term-constructor name associated with this function table, if
     /// any. Set on view tables created by the term/proof encoding to refer
     /// back to the user-visible constructor name.
@@ -2242,6 +2252,30 @@ impl EGraph {
         self.functions.get(name)
     }
 
+    /// Find the canonical representative of an eq-sort value.
+    ///
+    /// If `sort` does not have an internal union-find table, or if `value` is
+    /// not currently mapped in that table, this returns `value` unchanged.
+    pub fn canonical_value(&self, sort: &ArcSort, value: Value) -> Value {
+        let Some(uf_name) = self.proof_state.uf_parent.get(sort.name()) else {
+            return value;
+        };
+        let Some(uf_func) = self.functions.get(uf_name) else {
+            return value;
+        };
+
+        let mut canonical = value;
+        self.backend
+            .for_each(uf_func.backend_id, |row: egglog_bridge::ScanEntry| {
+                // The internal UF table stores `(child, parent)` and is kept at
+                // one hop to the canonical representative.
+                if row.vals[0] == value {
+                    canonical = row.vals[1];
+                }
+            });
+        canonical
+    }
+
     /// Returns `true` if a user-defined command with the given name is
     /// registered in this e-graph.
     pub fn has_command(&self, name: &str) -> bool {