Adds support marking exprs as subsumed

src/ast/desugar.rs

@@ -25,12 +25,25 @@ fn desugar_rewrite(
     ruleset: Symbol,
     name: Symbol,
     rewrite: &Rewrite,
+    replace: bool,
     desugar: &mut Desugar,
 ) -> Vec<NCommand> {
     let var = Symbol::from("rewrite_var__");
     // 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
+    let mut head = vec![Action::Union(Expr::Var(var), rewrite.rhs.clone())];
+    if replace {
+        match &rewrite.lhs {
+            Expr::Call(f, args) => {
+                head.push(Action::Unextractable(*f, args.to_vec()));
+                head.push(Action::Subsume(*f, args.to_vec()));
+            }
+            _ => {
+                panic!("Unextractable rewrite must have a function call on the lhs");
+            }
+        }
+    }
     vec![NCommand::NormRule {
         ruleset,
         name,
@@ -40,7 +53,7 @@ fn desugar_rewrite(
                     .into_iter()
                     .chain(rewrite.conditions.clone())
                     .collect(),
-                head: vec![Action::Union(Expr::Var(var), rewrite.rhs.clone())],
+                head,
             },
             desugar,
         ),
@@ -58,15 +71,22 @@ fn desugar_birewrite(
         rhs: rewrite.lhs.clone(),
         conditions: rewrite.conditions.clone(),
     };
-    desugar_rewrite(ruleset, format!("{}=>", name).into(), rewrite, desugar)
-        .into_iter()
-        .chain(desugar_rewrite(
-            ruleset,
-            format!("{}<=", name).into(),
-            &rw2,
-            desugar,
-        ))
-        .collect()
+    desugar_rewrite(
+        ruleset,
+        format!("{}=>", name).into(),
+        rewrite,
+        false,
+        desugar,
+    )
+    .into_iter()
+    .chain(desugar_rewrite(
+        ruleset,
+        format!("{}<=", name).into(),
+        &rw2,
+        false,
+        desugar,
+    ))
+    .collect()
 }
 
 fn normalize_expr(
@@ -257,16 +277,48 @@ fn flatten_actions(actions: &Vec<Action>, desugar: &mut Desugar) -> Vec<NormActi
                 let added_variants = add_expr(variants.clone(), &mut res);
                 res.push(NormAction::Extract(added, added_variants));
             }
+            // TODO: Reduce duplication in these three cases
             Action::Delete(symbol, exprs) => {
-                let del = NormAction::Delete(NormExpr::Call(
-                    *symbol,
-                    exprs
-                        .clone()
-                        .into_iter()
-                        .map(|ex| add_expr(ex, &mut res))
-                        .collect(),
-                ));
-                res.push(del);
+                let unex = NormAction::ChangeRow(
+                    ChangeRow::Delete,
+                    NormExpr::Call(
+                        *symbol,
+                        exprs
+                            .clone()
+                            .into_iter()
+                            .map(|ex| add_expr(ex, &mut res))
+                            .collect(),
+                    ),
+                );
+                res.push(unex);
+            }
+            Action::Unextractable(symbol, exprs) => {
+                let unex = NormAction::ChangeRow(
+                    ChangeRow::Unextractable,
+                    NormExpr::Call(
+                        *symbol,
+                        exprs
+                            .clone()
+                            .into_iter()
+                            .map(|ex| add_expr(ex, &mut res))
+                            .collect(),
+                    ),
+                );
+                res.push(unex);
+            }
+            Action::Subsume(symbol, exprs) => {
+                let unex = NormAction::ChangeRow(
+                    ChangeRow::Subsume,
+                    NormExpr::Call(
+                        *symbol,
+                        exprs
+                            .clone()
+                            .into_iter()
+                            .map(|ex| add_expr(ex, &mut res))
+                            .collect(),
+                    ),
+                );
+                res.push(unex);
             }
             Action::Union(lhs, rhs) => {
                 let un = NormAction::Union(
@@ -550,9 +602,13 @@ 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, desugar)
-        }
+        Command::Rewrite(ruleset, rewrite, replace) => desugar_rewrite(
+            ruleset,
+            rewrite_name(&rewrite).into(),
+            &rewrite,
+            replace,
+            desugar,
+        ),
         Command::BiRewrite(ruleset, rewrite) => {
             desugar_birewrite(ruleset, rewrite_name(&rewrite).into(), &rewrite, desugar)
         }

src/ast/mod.rs

@@ -328,6 +328,8 @@ impl Display for NormSchedule {
     }
 }
 
+pub type Replace = bool;
+
 // TODO command before and after desugaring should be different
 /// A [`Command`] is the top-level construct in egglog.
 /// It includes defining rules, declaring functions,
@@ -541,7 +543,13 @@ pub enum Command {
     ///          :when ((= a (Num 0)))
     /// ```
     ///
-    Rewrite(Symbol, Rewrite),
+    /// To make the left hand side unextractable and unmatchable (subsumsed) use the `:replace ` clause
+    ///
+    /// ```text
+    /// (rewrite (Mul a 2) (bitshift-left a 1) :replace)
+    /// ```
+    ///
+    Rewrite(Symbol, Rewrite, Replace),
     /// Similar to [`Command::Rewrite`], but
     /// generates two rules, one for each direction.
     ///
@@ -679,8 +687,10 @@ impl ToSexp for Command {
     fn to_sexp(&self) -> Sexp {
         match self {
             Command::SetOption { name, value } => list!("set-option", name, value),
-            Command::Rewrite(name, rewrite) => rewrite.to_sexp(*name, false),
-            Command::BiRewrite(name, rewrite) => rewrite.to_sexp(*name, true),
+            Command::Rewrite(name, rewrite, unextractable) => {
+                rewrite.to_sexp(*name, false, *unextractable)
+            }
+            Command::BiRewrite(name, rewrite) => rewrite.to_sexp(*name, true, false),
             Command::Datatype { name, variants } => list!("datatype", name, ++ variants),
             Command::Declare { name, sort } => list!("declare", name, sort),
             Command::Action(a) => a.to_sexp(),
@@ -1080,6 +1090,12 @@ pub enum Action {
     /// Be wary! Only delete entries that are subsumed in some way or
     /// guaranteed to be not useful.
     Delete(Symbol, Vec<Expr>),
+    /// Set an entry to be `unextractable`
+    /// so that it cannot be extracted.
+    /// Note that this cannot be an expr but has to be a symbol and args, because we need to refer to a specific row
+    Unextractable(Symbol, Vec<Expr>),
+    /// `subsume` an an entry so that it cannot be queries for during rules or rewrites.
+    Subsume(Symbol, Vec<Expr>),
     /// `union` two datatypes, making them equal
     /// in the implicit, global equality relation
     /// of egglog.
@@ -1107,14 +1123,31 @@ pub enum Action {
     // If(Expr, Action, Action),
 }
 
+#[derive(Clone, Debug, Copy, PartialEq, Eq, Hash)]
+pub enum ChangeRow {
+    Delete,
+    Subsume,
+    Unextractable,
+}
+
+impl ChangeRow {
+    pub fn to_action(&self, op: Symbol, args: Vec<Expr>) -> Action {
+        match self {
+            ChangeRow::Delete => Action::Delete(op, args),
+            ChangeRow::Subsume => Action::Subsume(op, args),
+            ChangeRow::Unextractable => Action::Unextractable(op, args),
+        }
+    }
+}
+
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub enum NormAction {
     Let(Symbol, NormExpr),
     LetVar(Symbol, Symbol),
     LetLit(Symbol, Literal),
     Extract(Symbol, Symbol),
     Set(NormExpr, Symbol),
-    Delete(NormExpr),
+    ChangeRow(ChangeRow, NormExpr),
     Union(Symbol, Symbol),
     Panic(String),
 }
@@ -1133,8 +1166,8 @@ impl NormAction {
             NormAction::Extract(symbol, variants) => {
                 Action::Extract(Expr::Var(*symbol), Expr::Var(*variants))
             }
-            NormAction::Delete(NormExpr::Call(symbol, args)) => {
-                Action::Delete(*symbol, args.iter().map(|s| Expr::Var(*s)).collect())
+            NormAction::ChangeRow(change, NormExpr::Call(symbol, args)) => {
+                change.to_action(*symbol, args.iter().map(|s| Expr::Var(*s)).collect())
             }
             NormAction::Union(lhs, rhs) => Action::Union(Expr::Var(*lhs), Expr::Var(*rhs)),
             NormAction::Panic(msg) => Action::Panic(msg.clone()),
@@ -1148,7 +1181,7 @@ impl NormAction {
             NormAction::LetLit(symbol, lit) => NormAction::LetLit(*symbol, lit.clone()),
             NormAction::Set(expr, other) => NormAction::Set(f(expr), *other),
             NormAction::Extract(var, variants) => NormAction::Extract(*var, *variants),
-            NormAction::Delete(expr) => NormAction::Delete(f(expr)),
+            NormAction::ChangeRow(change, expr) => NormAction::ChangeRow(*change, f(expr)),
             NormAction::Union(lhs, rhs) => NormAction::Union(*lhs, *rhs),
             NormAction::Panic(msg) => NormAction::Panic(msg.clone()),
         }
@@ -1170,7 +1203,9 @@ impl NormAction {
             NormAction::Extract(var, variants) => {
                 NormAction::Extract(fvar(*var, false), fvar(*variants, false))
             }
-            NormAction::Delete(expr) => NormAction::Delete(expr.map_def_use(fvar, false)),
+            NormAction::ChangeRow(change, expr) => {
+                NormAction::ChangeRow(*change, expr.map_def_use(fvar, false))
+            }
             NormAction::Union(lhs, rhs) => NormAction::Union(fvar(*lhs, false), fvar(*rhs, false)),
             NormAction::Panic(msg) => NormAction::Panic(msg.clone()),
         }
@@ -1184,6 +1219,8 @@ impl ToSexp for Action {
             Action::Set(lhs, args, rhs) => list!("set", list!(lhs, ++ args), rhs),
             Action::Union(lhs, rhs) => list!("union", lhs, rhs),
             Action::Delete(lhs, args) => list!("delete", list!(lhs, ++ args)),
+            Action::Unextractable(lhs, args) => list!("unextractable", list!(lhs, ++ args)),
+            Action::Subsume(lhs, args) => list!("subsume", list!(lhs, ++ args)),
             Action::Extract(expr, variants) => list!("extract", expr, variants),
             Action::Panic(msg) => list!("panic", format!("\"{}\"", msg.clone())),
             Action::Expr(e) => e.to_sexp(),
@@ -1200,6 +1237,10 @@ impl Action {
                 Action::Set(*lhs, args.iter().map(f).collect(), right)
             }
             Action::Delete(lhs, args) => Action::Delete(*lhs, args.iter().map(f).collect()),
+            Action::Unextractable(lhs, args) => {
+                Action::Unextractable(*lhs, args.iter().map(f).collect())
+            }
+            Action::Subsume(lhs, args) => Action::Subsume(*lhs, args.iter().map(f).collect()),
             Action::Union(lhs, rhs) => Action::Union(f(lhs), f(rhs)),
             Action::Extract(expr, variants) => Action::Extract(f(expr), f(variants)),
             Action::Panic(msg) => Action::Panic(msg.clone()),
@@ -1218,6 +1259,12 @@ impl Action {
             Action::Delete(lhs, args) => {
                 Action::Delete(*lhs, args.iter().map(|e| e.subst(canon)).collect())
             }
+            Action::Unextractable(lhs, args) => {
+                Action::Unextractable(*lhs, args.iter().map(|e| e.subst(canon)).collect())
+            }
+            Action::Subsume(lhs, args) => {
+                Action::Subsume(*lhs, args.iter().map(|e| e.subst(canon)).collect())
+            }
             Action::Union(lhs, rhs) => Action::Union(lhs.subst(canon), rhs.subst(canon)),
             Action::Extract(expr, variants) => {
                 Action::Extract(expr.subst(canon), variants.subst(canon))
@@ -1399,7 +1446,7 @@ impl NormRule {
                         _ => panic!("Expected call in set"),
                     }
                 }
-                NormAction::Delete(expr) => {
+                NormAction::ChangeRow(change, expr) => {
                     let new_expr = expr.to_expr();
                     new_expr.map(&mut |subexpr| {
                         if let Expr::Var(v) = subexpr {
@@ -1409,11 +1456,12 @@ impl NormRule {
                     });
                     match new_expr.subst(subst) {
                         Expr::Call(op, children) => {
-                            head.push(Action::Delete(op, children));
+                            head.push(change.to_action(op, children));
                         }
-                        _ => panic!("Expected call in delete"),
+                        _ => panic!("Expected call"),
                     }
                 }
+
                 NormAction::Union(lhs, rhs) => {
                     let new_lhs = subst.get(lhs).unwrap_or(&Expr::Var(*lhs)).clone();
                     let new_rhs = subst.get(rhs).unwrap_or(&Expr::Var(*rhs)).clone();
@@ -1559,7 +1607,7 @@ pub struct Rewrite {
 
 impl Rewrite {
     /// 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, unextractable: bool) -> Sexp {
         let mut res = vec![
             Sexp::Symbol(if is_bidirectional {
                 "birewrite".into()
@@ -1569,6 +1617,9 @@ impl Rewrite {
             self.lhs.to_sexp(),
             self.rhs.to_sexp(),
         ];
+        if unextractable {
+            res.insert(1, Sexp::Symbol(":unextractable".into()));
+        }
 
         if !self.conditions.is_empty() {
             res.push(Sexp::Symbol(":when".into()));
@@ -1587,6 +1638,6 @@ impl Rewrite {
 
 impl Display for Rewrite {
     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

@@ -23,14 +23,14 @@ pub Program: Vec<Command> = { (Command)* => <> }
 
 LParen: () = {
     "(" => (),
-    "[" => (), 
+    "[" => (),
 };
 RParen: () = {
     ")" => (),
     "]" => (),
 };
 
-List<T>: Vec<T> = { 
+List<T>: Vec<T> = {
     LParen <T*> RParen => <>,
 }
 
@@ -60,9 +60,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, body }},
     LParen "rewrite" <lhs:Expr> <rhs:Expr>
+        <replace:(":replace")?>
         <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() }, replace.is_some()),
     LParen "birewrite" <lhs:Expr> <rhs:Expr>
         <conditions:(":when" <List<Fact>>)?>
         <ruleset:(":ruleset" <Ident>)?>
@@ -71,7 +72,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) },
@@ -93,7 +94,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,6 +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 "unextractable" LParen <f: Ident> <args:Expr*> RParen RParen => Action::Unextractable ( f, args),
+    LParen "subsume" LParen <f: Ident> <args:Expr*> RParen RParen => Action::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))),