Adds support marking exprs as subsumed

src/actions.rs

@@ -40,14 +40,15 @@ impl<'a> ActionCompiler<'a> {
                 self.do_atom_term(e);
                 self.instructions.push(Instruction::Set(func.name));
             }
-            GenericCoreAction::Delete(f, args) => {
+            GenericCoreAction::Change(change, f, args) => {
                 let ResolvedCall::Func(func) = f else {
-                    panic!("Cannot delete primitive- should have been caught by typechecking!!!")
+                    panic!("Cannot change primitive- should have been caught by typechecking!!!")
                 };
                 for arg in args {
                     self.do_atom_term(arg);
                 }
-                self.instructions.push(Instruction::DeleteRow(func.name));
+                self.instructions
+                    .push(Instruction::Change(*change, func.name));
             }
             GenericCoreAction::Union(arg1, arg2) => {
                 self.do_atom_term(arg1);
@@ -132,9 +133,9 @@ enum Instruction {
     /// Pop primitive arguments off the stack, calls the primitive,
     /// and push the result onto the stack.
     CallPrimitive(Primitive, usize),
-    /// Pop function arguments off the stack and delete the corresponding row
-    /// from the function.
-    DeleteRow(Symbol),
+    /// Pop function arguments off the stack and either deletes or subsumes the corresponding row
+    /// in the function.
+    Change(Change, Symbol),
     /// Pop the value to be set and the function arguments off the stack.
     /// Set the function at the given arguments to the new value.
     Set(Symbol),
@@ -417,11 +418,21 @@ impl EGraph {
                     Literal::Bool(b) => stack.push(Value::from(*b)),
                     Literal::Unit => stack.push(Value::unit()),
                 },
-                Instruction::DeleteRow(f) => {
+                Instruction::Change(change, f) => {
                     let function = self.functions.get_mut(f).unwrap();
                     let new_len = stack.len() - function.schema.input.len();
                     let args = &stack[new_len..];
-                    function.remove(args, self.timestamp);
+                    match change {
+                        Change::Delete => {
+                            function.remove(args, self.timestamp);
+                        }
+                        Change::Subsume => {
+                            if function.decl.merge.is_some() {
+                                return Err(Error::SubsumeMergeError(*f));
+                            }
+                            function.subsume(args);
+                        }
+                    }
                     stack.truncate(new_len);
                 }
             }

src/ast/desugar.rs

@@ -21,8 +21,25 @@ fn desugar_datatype(name: Symbol, variants: Vec<Variant>) -> Vec<NCommand> {
         .collect()
 }
 
-fn desugar_rewrite(ruleset: Symbol, name: Symbol, rewrite: &Rewrite) -> Vec<NCommand> {
+fn desugar_rewrite(
+    ruleset: Symbol,
+    name: Symbol,
+    rewrite: &Rewrite,
+    subsume: bool,
+) -> Vec<NCommand> {
     let var = Symbol::from("rewrite_var__");
+    let mut head = Actions::singleton(Action::Union((), Expr::Var((), var), rewrite.rhs.clone()));
+    if subsume {
+        match &rewrite.lhs {
+            Expr::Call(_, f, args) => {
+                head.0
+                    .push(Action::Change((), Change::Subsume, *f, args.to_vec()));
+            }
+            _ => {
+                panic!("Subsumed rewrite must have a function call on the lhs");
+            }
+        }
+    }
     // make two rules- one to insert the rhs, and one to union
     // this way, the union rule can only be fired once,
     // which helps proofs not add too much info
@@ -34,7 +51,7 @@ fn desugar_rewrite(ruleset: Symbol, name: Symbol, rewrite: &Rewrite) -> Vec<NCom
                 .into_iter()
                 .chain(rewrite.conditions.clone())
                 .collect(),
-            head: Actions::singleton(Action::Union((), Expr::Var((), var), rewrite.rhs.clone())),
+            head,
         },
     }]
 }
@@ -45,9 +62,14 @@ fn desugar_birewrite(ruleset: Symbol, name: Symbol, rewrite: &Rewrite) -> Vec<NC
         rhs: rewrite.lhs.clone(),
         conditions: rewrite.conditions.clone(),
     };
-    desugar_rewrite(ruleset, format!("{}=>", name).into(), rewrite)
+    desugar_rewrite(ruleset, format!("{}=>", name).into(), rewrite, false)
         .into_iter()
-        .chain(desugar_rewrite(ruleset, format!("{}<=", name).into(), &rw2))
+        .chain(desugar_rewrite(
+            ruleset,
+            format!("{}<=", name).into(),
+            &rw2,
+            false,
+        ))
         .collect()
 }
 
@@ -215,8 +237,8 @@ pub(crate) fn desugar_command(
         } => desugar.desugar_function(&FunctionDecl::relation(constructor, inputs)),
         Command::Declare { name, sort } => desugar.declare(name, sort),
         Command::Datatype { name, variants } => desugar_datatype(name, variants),
-        Command::Rewrite(ruleset, rewrite) => {
-            desugar_rewrite(ruleset, rewrite_name(&rewrite).into(), &rewrite)
+        Command::Rewrite(ruleset, rewrite, subsume) => {
+            desugar_rewrite(ruleset, rewrite_name(&rewrite).into(), &rewrite, subsume)
         }
         Command::BiRewrite(ruleset, rewrite) => {
             desugar_birewrite(ruleset, rewrite_name(&rewrite).into(), &rewrite)

src/ast/mod.rs

@@ -218,6 +218,8 @@ impl<Head: Display, Leaf: Display, Ann> Display for GenericSchedule<Head, Leaf,
 
 pub type Command = GenericCommand<Symbol, Symbol>;
 
+pub type Subsume = bool;
+
 /// A [`Command`] is the top-level construct in egglog.
 /// It includes defining rules, declaring functions,
 /// adding to tables, and running rules (via a [`Schedule`]).
@@ -430,7 +432,20 @@ pub enum GenericCommand<Head, Leaf> {
     ///          :when ((= a (Num 0)))
     /// ```
     ///
-    Rewrite(Symbol, GenericRewrite<Head, Leaf, ()>),
+    /// Add the `:subsume` flag to cause the left hand side to be subsumed after matching, which means it can
+    /// no longer be matched in a rule, but can still be checked against (See [`Change`] for more details.)
+    ///
+    /// ```text
+    /// (rewrite (Mul a 2) (bitshift-left a 1) :subsume)
+    /// ```
+    ///
+    /// Desugars to:
+    /// ```text
+    /// (rule ((= lhs (Mul a 2)))
+    ///       ((union lhs (bitshift-left a 1))
+    ///        (subsume (Mul a 2))))
+    /// ```
+    Rewrite(Symbol, GenericRewrite<Head, Leaf, ()>, Subsume),
     /// Similar to [`Command::Rewrite`], but
     /// generates two rules, one for each direction.
     ///
@@ -568,8 +583,10 @@ impl<Head: Display + ToSexp, Leaf: Display + ToSexp> ToSexp for GenericCommand<H
     fn to_sexp(&self) -> Sexp {
         match self {
             GenericCommand::SetOption { name, value } => list!("set-option", name, value),
-            GenericCommand::Rewrite(name, rewrite) => rewrite.to_sexp(*name, false),
-            GenericCommand::BiRewrite(name, rewrite) => rewrite.to_sexp(*name, true),
+            GenericCommand::Rewrite(name, rewrite, subsume) => {
+                rewrite.to_sexp(*name, false, *subsume)
+            }
+            GenericCommand::BiRewrite(name, rewrite) => rewrite.to_sexp(*name, true, false),
             GenericCommand::Datatype { name, variants } => list!("datatype", name, ++ variants),
             GenericCommand::Declare { name, sort } => list!("declare", name, sort),
             GenericCommand::Action(a) => a.to_sexp(),
@@ -942,6 +959,17 @@ where
     }
 }
 
+/// Change a function entry.
+#[derive(Clone, Debug, Copy, PartialEq, Eq, Hash)]
+pub enum Change {
+    /// `delete` this entry from a function.
+    /// Be wary! Only delete entries that are guaranteed to be not useful.
+    Delete,
+    /// `subsume` this entry so that it cannot be queried or extracted, but still can be checked.
+    /// Note that this is currently forbidden for functions with custom merges.
+    Subsume,
+}
+
 pub type Action = GenericAction<Symbol, Symbol, ()>;
 pub(crate) type MappedAction = GenericAction<(Symbol, Symbol), Symbol, ()>;
 pub(crate) type ResolvedAction = GenericAction<ResolvedCall, ResolvedVar, ()>;
@@ -961,10 +989,8 @@ pub enum GenericAction<Head, Leaf, Ann> {
         Vec<GenericExpr<Head, Leaf, Ann>>,
         GenericExpr<Head, Leaf, Ann>,
     ),
-    /// `delete` an entry from a function.
-    /// Be wary! Only delete entries that are subsumed in some way or
-    /// guaranteed to be not useful.
-    Delete(Ann, Head, Vec<GenericExpr<Head, Leaf, Ann>>),
+    /// Delete or subsume (mark as hidden from future rewrites and unextractable) an entry from a function.
+    Change(Ann, Change, Head, Vec<GenericExpr<Head, Leaf, Ann>>),
     /// `union` two datatypes, making them equal
     /// in the implicit, global equality relation
     /// of egglog.
@@ -1034,7 +1060,15 @@ impl<Head: Display + ToSexp, Leaf: Display + ToSexp, Ann> ToSexp
             GenericAction::Let(_ann, lhs, rhs) => list!("let", lhs, rhs),
             GenericAction::Set(_ann, lhs, args, rhs) => list!("set", list!(lhs, ++ args), rhs),
             GenericAction::Union(_ann, lhs, rhs) => list!("union", lhs, rhs),
-            GenericAction::Delete(_ann, lhs, args) => list!("delete", list!(lhs, ++ args)),
+            GenericAction::Change(_ann, change, lhs, args) => {
+                list!(
+                    match change {
+                        Change::Delete => "delete",
+                        Change::Subsume => "subsume",
+                    },
+                    list!(lhs, ++ args)
+                )
+            }
             GenericAction::Extract(_ann, expr, variants) => list!("extract", expr, variants),
             GenericAction::Panic(_ann, msg) => list!("panic", format!("\"{}\"", msg.clone())),
             GenericAction::Expr(_ann, e) => e.to_sexp(),
@@ -1065,9 +1099,12 @@ where
                     right,
                 )
             }
-            GenericAction::Delete(ann, lhs, args) => {
-                GenericAction::Delete(ann.clone(), lhs.clone(), args.iter().map(f).collect())
-            }
+            GenericAction::Change(ann, change, lhs, args) => GenericAction::Change(
+                ann.clone(),
+                *change,
+                lhs.clone(),
+                args.iter().map(f).collect(),
+            ),
             GenericAction::Union(ann, lhs, rhs) => {
                 GenericAction::Union(ann.clone(), f(lhs), f(rhs))
             }
@@ -1103,12 +1140,12 @@ where
                 let rhs = rhs.subst_leaf(&mut fvar_expr!());
                 GenericAction::Set(ann.clone(), lhs.clone(), args, rhs)
             }
-            GenericAction::Delete(ann, lhs, args) => {
+            GenericAction::Change(ann, change, lhs, args) => {
                 let args = args
                     .iter()
                     .map(|e| e.subst_leaf(&mut fvar_expr!()))
                     .collect();
-                GenericAction::Delete(ann.clone(), lhs.clone(), args)
+                GenericAction::Change(ann.clone(), *change, lhs.clone(), args)
             }
             GenericAction::Union(ann, lhs, rhs) => {
                 let lhs = lhs.subst_leaf(&mut fvar_expr!());
@@ -1227,7 +1264,7 @@ pub struct GenericRewrite<Head, Leaf, Ann> {
 
 impl<Head: Display, Leaf: Display, Ann> GenericRewrite<Head, Leaf, Ann> {
     /// Converts the rewrite into an s-expression.
-    pub fn to_sexp(&self, ruleset: Symbol, is_bidirectional: bool) -> Sexp {
+    pub fn to_sexp(&self, ruleset: Symbol, is_bidirectional: bool, subsume: bool) -> Sexp {
         let mut res = vec![
             Sexp::Symbol(if is_bidirectional {
                 "birewrite".into()
@@ -1237,6 +1274,9 @@ impl<Head: Display, Leaf: Display, Ann> GenericRewrite<Head, Leaf, Ann> {
             self.lhs.to_sexp(),
             self.rhs.to_sexp(),
         ];
+        if subsume {
+            res.push(Sexp::Symbol(":subsume".into()));
+        }
 
         if !self.conditions.is_empty() {
             res.push(Sexp::Symbol(":when".into()));
@@ -1255,7 +1295,7 @@ impl<Head: Display, Leaf: Display, Ann> GenericRewrite<Head, Leaf, Ann> {
 
 impl<Head: Display, Leaf: Display, Ann> Display for GenericRewrite<Head, Leaf, Ann> {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        write!(f, "{}", self.to_sexp("".into(), false))
+        write!(f, "{}", self.to_sexp("".into(), false, false))
     }
 }
 

src/ast/parse.lalrpop

@@ -24,14 +24,14 @@ pub Program: Vec<Command> = { (Command)* => <> }
 
 LParen: () = {
     "(" => (),
-    "[" => (), 
+    "[" => (),
 };
 RParen: () = {
     ")" => (),
     "]" => (),
 };
 
-List<T>: Vec<T> = { 
+List<T>: Vec<T> = {
     LParen <T*> RParen => <>,
 }
 
@@ -61,9 +61,10 @@ Command: Command = {
     LParen "ruleset" <name:Ident> RParen => Command::AddRuleset(name),
     LParen "rule" <body:List<Fact>> <head:List<Action>> <ruleset:(":ruleset" <Ident>)?> <name:(":name" <String>)?> RParen => Command::Rule{ruleset: ruleset.unwrap_or("".into()), name: name.unwrap_or("".to_string()).into(), rule: Rule { head: Actions::new(head), body }},
     LParen "rewrite" <lhs:Expr> <rhs:Expr>
+        <subsume:(":subsume")?>
         <conditions:(":when" <List<Fact>>)?>
         <ruleset:(":ruleset" <Ident>)?>
-    RParen => Command::Rewrite(ruleset.unwrap_or("".into()), Rewrite { lhs, rhs, conditions: conditions.unwrap_or_default() }),
+    RParen => Command::Rewrite(ruleset.unwrap_or("".into()), Rewrite { lhs, rhs, conditions: conditions.unwrap_or_default() }, subsume.is_some()),
     LParen "birewrite" <lhs:Expr> <rhs:Expr>
         <conditions:(":when" <List<Fact>>)?>
         <ruleset:(":ruleset" <Ident>)?>
@@ -72,7 +73,7 @@ Command: Command = {
     <NonLetAction> => Command::Action(<>),
     LParen "run" <limit:UNum>  <until:(":until" <(Fact)*>)?> RParen => Command::RunSchedule(Schedule::Repeat(limit, Box::new(Schedule::Run(RunConfig { ruleset : "".into(), until })))),
     LParen "run" <ruleset: Ident> <limit:UNum> <until:(":until" <(Fact)*>)?> RParen => Command::RunSchedule(Schedule::Repeat(limit, Box::new(Schedule::Run(RunConfig { ruleset, until })))),
-    LParen "simplify"  <schedule:Schedule> <expr:Expr> RParen 
+    LParen "simplify"  <schedule:Schedule> <expr:Expr> RParen
         => Command::Simplify { expr, schedule },
     LParen "calc" LParen <idents:IdentSort*> RParen <exprs:Expr+> RParen => Command::Calc(idents, exprs),
     LParen "query-extract" <variants:(":variants" <UNum>)?> <expr:Expr> RParen => Command::QueryExtract { expr, variants: variants.unwrap_or(0) },
@@ -94,7 +95,7 @@ Schedule: Schedule = {
     LParen "saturate" <Schedule*> RParen => Schedule::Saturate(Box::new(Schedule::Sequence(<>))),
     LParen "seq" <Schedule*> RParen => Schedule::Sequence(<>),
     LParen "repeat" <limit:UNum> <scheds:Schedule*> RParen => Schedule::Repeat(limit, Box::new(Schedule::Sequence(scheds))),
-    LParen "run" <until:(":until" <(Fact)*>)?> RParen => 
+    LParen "run" <until:(":until" <(Fact)*>)?> RParen =>
     Schedule::Run(RunConfig { ruleset: "".into(), until }),
     LParen "run" <ruleset: Ident> <until:(":until" <(Fact)*>)?> RParen => Schedule::Run(RunConfig { ruleset, until }),
     <ident:Ident> => Schedule::Run(RunConfig { ruleset: ident, until: None }),
@@ -107,7 +108,8 @@ Cost: Option<usize> = {
 
 NonLetAction: Action = {
     LParen "set" LParen <f: Ident> <args:Expr*> RParen <v:Expr> RParen => Action::Set ( (), f, args, v ),
-    LParen "delete" LParen <f: Ident> <args:Expr*> RParen RParen => Action::Delete ( (), f, args),
+    LParen "delete" LParen <f: Ident> <args:Expr*> RParen RParen => Action::Change ( (), Change::Delete, f, args),
+    LParen "subsume" LParen <f: Ident> <args:Expr*> RParen RParen => Action::Change ( (), Change::Subsume, f, args),
     LParen "union" <e1:Expr> <e2:Expr> RParen => Action::Union((), <>),
     LParen "panic" <msg:String> RParen => Action::Panic((), msg),
     LParen "extract" <expr:Expr> RParen => Action::Extract((), expr, Expr::Lit((), Literal::Int(0))),

src/constraint.rs

@@ -321,7 +321,7 @@ impl Assignment<AtomTerm, ArcSort> {
                 Ok(ResolvedAction::Set((), resolved_call, children, rhs))
             }
             // Note mapped_var for delete is a dummy variable that does not mean anything
-            GenericAction::Delete((), (head, _mapped_var), children) => {
+            GenericAction::Change((), change, (head, _mapped_var), children) => {
                 let children: Vec<_> = children
                     .iter()
                     .map(|child| self.annotate_expr(child, typeinfo))
@@ -333,7 +333,12 @@ impl Assignment<AtomTerm, ArcSort> {
                 let resolved_call =
                     ResolvedCall::from_resolution_func_types(head, &types, typeinfo)
                         .ok_or_else(|| TypeError::UnboundFunction(*head))?;
-                Ok(ResolvedAction::Delete((), resolved_call, children.clone()))
+                Ok(ResolvedAction::Change(
+                    (),
+                    *change,
+                    resolved_call,
+                    children.clone(),
+                ))
             }
             GenericAction::Union((), lhs, rhs) => Ok(ResolvedAction::Union(
                 (),
@@ -477,7 +482,7 @@ impl CoreAction {
                     .chain(get_atom_application_constraints(head, &args, typeinfo)?)
                     .collect())
             }
-            CoreAction::Delete(head, args) => {
+            CoreAction::Change(_change, head, args) => {
                 let mut args = args.clone();
                 // Add a dummy last output argument
                 let var = symbol_gen.fresh(&Symbol::from(format!("constraint${head}")));