Proof optimization- consolidate proof and view/UF tables

egglog-bridge/src/rule.rs

@@ -115,6 +115,9 @@ pub(crate) struct Query {
     /// If set, execute a single rule (rather than O(atoms.len()) rules) during
     /// seminaive, with the given atom as the focus.
     sole_focus: Option<usize>,
+    /// Atoms to skip when generating seminaive variants.
+    /// Variants focused on these atoms will not be generated.
+    skip_seminaive: Vec<usize>,
     seminaive: bool,
     plan_strategy: PlanStrategy,
 }
@@ -143,6 +146,7 @@ impl EGraph {
                 rule_id,
                 seminaive,
                 sole_focus: None,
+                skip_seminaive: Vec::new(),
                 vars: Default::default(),
                 atoms: Default::default(),
                 add_rule: Default::default(),
@@ -284,10 +288,16 @@ impl RuleBuilder<'_> {
         res
     }
 
-    pub(crate) fn set_focus(&mut self, focus: usize) {
+    pub fn set_focus(&mut self, focus: usize) {
         self.query.sole_focus = Some(focus);
     }
 
+    /// Mark an atom to be skipped during seminaive variant generation.
+    /// Variants focused on skipped atoms will not be generated.
+    pub fn skip_seminaive_atom(&mut self, atom: usize) {
+        self.query.skip_seminaive.push(atom);
+    }
+
     /// Bind a new variable of the given type in the query.
     pub fn new_var(&mut self, ty: ColumnTy) -> Variable {
         let res = self.query.vars.next_id();
@@ -784,10 +794,20 @@ impl Query {
         let mut constraints: Vec<(core_relations::AtomId, Constraint)> =
             Vec::with_capacity(self.atoms.len());
         'outer: for focus_atom in 0..self.atoms.len() {
+            if self.skip_seminaive.contains(&focus_atom) {
+                continue;
+            }
             for (i, (_, _, schema_info)) in self.atoms.iter().enumerate() {
                 let ts_col = ColumnId::from_usize(schema_info.ts_col());
                 match i.cmp(&focus_atom) {
                     Ordering::Less => {
+                        // Skip the "must be old" constraint for atoms we're
+                        // skipping seminaive on — they never drive new
+                        // matches, so constraining them to old would
+                        // incorrectly filter out valid matches.
+                        if self.skip_seminaive.contains(&i) {
+                            continue;
+                        }
                         if mid_ts == Timestamp::new(0) {
                             continue 'outer;
                         }

src/ast/desugar.rs

@@ -18,10 +18,22 @@ pub(crate) fn desugar_command(
             merge,
             hidden,
             let_binding,
+            term_constructor,
+            unextractable,
         } => {
             let mut fdecl = FunctionDecl::function(span, name, schema, merge);
             fdecl.internal_hidden = hidden;
             fdecl.internal_let = let_binding;
+            fdecl.term_constructor = term_constructor;
+            // Functions with term_constructor are view tables that should be
+            // extractable unless explicitly marked unextractable
+            if fdecl.term_constructor.is_some() {
+                fdecl.unextractable = unextractable;
+            } else if unextractable {
+                fdecl.unextractable = true;
+            }
+            // For regular functions without term_constructor, keep the default
+            // unextractable=true from FunctionDecl::function()
             vec![NCommand::Function(fdecl)]
         }
         Command::Constructor {

src/ast/mod.rs

@@ -142,6 +142,8 @@ where
                     merge: f.merge.clone(),
                     hidden: f.internal_hidden,
                     let_binding: f.internal_let,
+                    term_constructor: f.term_constructor.clone(),
+                    unextractable: f.unextractable,
                 },
             },
             GenericNCommand::AddRuleset(span, name) => {
@@ -636,8 +638,8 @@ where
         /// Internal-let constructors are let bindings, excluded from print-size output.
         /// Used for global let bindings that are converted to constructors.
         let_binding: bool,
-        /// For view tables in proof encoding: the constructor to use for building
-        /// terms from the first n-1 children during extraction.
+        /// Internal-only metadata for proof-encoding view tables.
+        /// Parsed user syntax only supports `:term-constructor` on `function`.
         term_constructor: Option<String>,
     },
 
@@ -699,6 +701,8 @@ where
         merge: Option<GenericExpr<Head, Leaf>>,
         hidden: bool,
         let_binding: bool,
+        term_constructor: Option<String>,
+        unextractable: bool,
     },
 
     /// Using the `ruleset` command, defines a new
@@ -976,19 +980,27 @@ where
                 merge,
                 hidden,
                 let_binding,
+                term_constructor,
+                unextractable,
             } => {
                 write!(f, "(function {name} {schema}")?;
                 if let Some(merge) = &merge {
                     write!(f, " :merge {merge}")?;
                 } else {
                     write!(f, " :no-merge")?;
                 }
+                if *unextractable {
+                    write!(f, " :unextractable")?;
+                }
                 if *hidden {
                     write!(f, " :internal-hidden")?;
                 }
                 if *let_binding {
                     write!(f, " :internal-let")?;
                 }
+                if let Some(tc) = term_constructor {
+                    write!(f, " :term-constructor {tc}")?;
+                }
                 write!(f, ")")
             }
             GenericCommand::Constructor {
@@ -1679,6 +1691,8 @@ where
                 merge,
                 hidden,
                 let_binding,
+                term_constructor,
+                unextractable,
             } => GenericCommand::Function {
                 span,
                 name: fun(name),
@@ -1689,6 +1703,8 @@ where
                 merge,
                 hidden,
                 let_binding,
+                term_constructor: term_constructor.map(&mut *fun),
+                unextractable,
             },
             GenericCommand::AddRuleset(span, name) => GenericCommand::AddRuleset(span, fun(name)),
             GenericCommand::UnstableCombinedRuleset(span, name, others) => {
@@ -1766,13 +1782,17 @@ where
                 merge,
                 hidden,
                 let_binding,
+                term_constructor,
+                unextractable,
             } => GenericCommand::Function {
                 span,
                 name,
                 schema,
                 merge: merge.map(|e| e.visit_exprs(f)),
                 hidden,
                 let_binding,
+                term_constructor,
+                unextractable,
             },
             GenericCommand::Rule { rule } => GenericCommand::Rule {
                 rule: rule.visit_exprs(f),
@@ -1899,13 +1919,17 @@ where
                 merge,
                 hidden,
                 let_binding,
+                term_constructor,
+                unextractable,
             } => GenericCommand::Function {
                 span,
                 name,
                 schema,
                 merge: merge.map(|expr| expr.map_symbols(head, leaf)),
                 hidden,
                 let_binding,
+                term_constructor,
+                unextractable,
             },
             GenericCommand::AddRuleset(span, name) => GenericCommand::AddRuleset(span, name),
             GenericCommand::UnstableCombinedRuleset(span, name, others) => {

src/ast/parse.rs

@@ -339,6 +339,8 @@ impl Parser {
                     let mut merge = None;
                     let mut hidden = false;
                     let mut let_binding = false;
+                    let mut term_constructor = None;
+                    let mut unextractable = false;
                     for (key, val) in self.parse_options(rest)? {
                         match (key, val) {
                             (":no-merge", []) => {
@@ -361,6 +363,10 @@ impl Parser {
                             }
                             (":internal-hidden", []) => hidden = true,
                             (":internal-let", []) => let_binding = true,
+                            (":unextractable", []) => unextractable = true,
+                            (":term-constructor", [tc]) => {
+                                term_constructor = Some(tc.expect_atom("term constructor name")?)
+                            }
                             _ => return error!(span, "could not parse function options"),
                         }
                     }
@@ -379,6 +385,8 @@ impl Parser {
                         merge,
                         hidden,
                         let_binding,
+                        term_constructor,
+                        unextractable,
                         span,
                     }]
                 }
@@ -400,17 +408,12 @@ impl Parser {
                         let mut unextractable = false;
                         let mut hidden = false;
                         let mut let_binding = false;
-                        let mut term_constructor = None;
                         for (key, val) in self.parse_options(rest)? {
                             match (key, val) {
                                 (":unextractable", []) => unextractable = true,
                                 (":internal-hidden", []) => hidden = true,
                                 (":internal-let", []) => let_binding = true,
                                 (":cost", [c]) => cost = Some(c.expect_uint("cost")?),
-                                (":term-constructor", [tc]) => {
-                                    term_constructor =
-                                        Some(tc.expect_atom("term constructor name")?)
-                                }
                                 _ => return error!(span, "could not parse constructor options"),
                             }
                         }
@@ -423,15 +426,14 @@ impl Parser {
                             unextractable,
                             hidden,
                             let_binding,
-                            term_constructor,
+                            term_constructor: None,
                         }]
                     }
                     _ => {
                         let a = "(constructor <name> (<input sort>*) <output sort>)";
                         let b = "(constructor <name> (<input sort>*) <output sort> :cost <cost>)";
                         let c = "(constructor <name> (<input sort>*) <output sort> :unextractable)";
-                        let d = "(constructor <name> (<input sort>*) <output sort> :term-constructor <constructor name>)";
-                        return error!(span, "usages:\n{a}\n{b}\n{c}\n{d}");
+                        return error!(span, "usages:\n{a}\n{b}\n{c}");
                     }
                 }
             }

src/extract.rs

@@ -222,11 +222,12 @@ impl<C: Cost + Ord + Eq + Clone + Debug> Extractor<C> {
                 options.skip_view_tables && func.1.decl.term_constructor.is_some();
             let hidden = func.1.decl.internal_hidden && options.respect_hidden;
 
-            // only extract constructors, skip view tables when requested for proof extraction, and respect unextractable/hidden flag
+            // only extract constructors (and functions with term_constructor), skip view tables when requested for proof extraction, and respect unextractable/hidden flag
             if !unextractable
                 && !should_skip_view
                 && !hidden
-                && func.1.decl.subtype == FunctionSubtype::Constructor
+                && (func.1.decl.subtype == FunctionSubtype::Constructor
+                    || func.1.decl.term_constructor.is_some())
             {
                 let func_name = func.0.clone();
                 // For view tables (with term_constructor in proof mode), the e-class is the last input column

src/lib.rs

@@ -368,6 +368,7 @@ impl Default for EGraph {
         eg.type_info.add_presort::<VecSort>(span!()).unwrap();
         eg.type_info.add_presort::<FunctionSort>(span!()).unwrap();
         eg.type_info.add_presort::<MultiSetSort>(span!()).unwrap();
+        eg.type_info.add_presort::<PairSort>(span!()).unwrap();
 
         // Add != with a validator that computes inequality result
         let neq_validator = |termdag: &mut TermDag, args: &[TermId]| -> Option<TermId> {
@@ -707,7 +708,8 @@ impl EGraph {
 
         let can_subsume = match decl.subtype {
             FunctionSubtype::Constructor => true,
-            FunctionSubtype::Custom => false,
+            // View tables (functions with term_constructor) need subsumption support
+            FunctionSubtype::Custom => decl.term_constructor.is_some(),
         };
 
         use egglog_bridge::{DefaultVal, MergeFn};

src/prelude.rs

@@ -702,6 +702,8 @@ pub fn add_function(
         merge,
         hidden: false,
         let_binding: false,
+        term_constructor: None,
+        unextractable: false,
     }])
 }