diff --git a/Cargo.lock b/Cargo.lock index 75db4fa038..54fb1e27d8 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -98,9 +98,9 @@ checksum = "86fdf8605db99b54d3cd748a44c6d04df638eb5dafb219b135d0149bd0db01f6" [[package]] name = "autocfg" -version = "1.3.0" +version = "1.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0c4b4d0bd25bd0b74681c0ad21497610ce1b7c91b1022cd21c80c6fbdd9476b0" +checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26" [[package]] name = "backtrace" @@ -132,7 +132,7 @@ dependencies = [ "bitflags", "cexpr", "clang-sys", - "itertools", + "itertools 0.13.0", "log", "prettyplease", "proc-macro2", @@ -140,7 +140,7 @@ dependencies = [ "regex", "rustc-hash", "shlex", - "syn 2.0.77", + "syn 2.0.79", ] [[package]] @@ -193,9 +193,9 @@ checksum = "428d9aa8fbc0670b7b8d6030a7fadd0f86151cae55e4dbbece15f3780a3dfaf3" [[package]] name = "cc" -version = "1.1.21" +version = "1.1.22" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "07b1695e2c7e8fc85310cde85aeaab7e3097f593c91d209d3f9df76c928100f0" +checksum = "9540e661f81799159abee814118cc139a2004b3a3aa3ea37724a1b66530b90e0" dependencies = [ "jobserver", "libc", @@ -280,7 +280,7 @@ dependencies = [ "heck", "proc-macro2", "quote", - "syn 2.0.77", + "syn 2.0.79", ] [[package]] @@ -305,7 +305,7 @@ dependencies = [ "derivative", "enum_compatability_macro", "im", - "itertools", + "itertools 0.13.0", "linkme", "log", "minion_rs", @@ -329,7 +329,7 @@ dependencies = [ "linkme", "proc-macro2", "quote", - "syn 2.0.77", + "syn 2.0.79", ] [[package]] @@ -383,7 +383,7 @@ dependencies = [ "proc-macro2", "quote", "strsim", - "syn 2.0.77", + "syn 2.0.79", ] [[package]] @@ -394,7 +394,7 @@ checksum = "d336a2a514f6ccccaa3e09b02d41d35330c07ddf03a62165fcec10bb561c7806" dependencies = [ "darling_core", "quote", - "syn 2.0.77", + "syn 2.0.79", ] [[package]] @@ -445,9 +445,9 @@ checksum = "60b1af1c220855b6ceac025d3f6ecdd2b7c4894bfe9cd9bda4fbb4bc7c0d4cf0" name = "enum_compatability_macro" version = "0.1.0" dependencies = [ - "itertools", + "itertools 0.13.0", "quote", - "syn 2.0.77", + "syn 2.0.79", ] [[package]] @@ -488,6 +488,13 @@ version = "1.0.7" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1" +[[package]] +name = "gen_reduce" +version = "0.1.0" +dependencies = [ + "uniplate", +] + [[package]] name = "getrandom" version = "0.2.15" @@ -607,6 +614,15 @@ version = "1.70.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7943c866cc5cd64cbc25b2e01621d07fa8eb2a1a23160ee81ce38704e97b8ecf" +[[package]] +name = "itertools" +version = "0.12.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ba291022dbbd398a455acf126c1e341954079855bc60dfdda641363bd6922569" +dependencies = [ + "either", +] + [[package]] name = "itertools" version = "0.13.0" @@ -711,7 +727,7 @@ checksum = "cb26336e6dc7cc76e7927d2c9e7e3bb376d7af65a6f56a0b16c47d18a9b1abc5" dependencies = [ "proc-macro2", "quote", - "syn 2.0.77", + "syn 2.0.79", ] [[package]] @@ -864,7 +880,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "479cf940fbbb3426c32c5d5176f62ad57549a0bb84773423ba8be9d089f5faba" dependencies = [ "proc-macro2", - "syn 2.0.77", + "syn 2.0.79", ] [[package]] @@ -910,7 +926,7 @@ checksum = "6ff7ff745a347b87471d859a377a9a404361e7efc2a971d73424a6d183c0fc77" dependencies = [ "proc-macro2", "quote", - "syn 2.0.77", + "syn 2.0.79", ] [[package]] @@ -1093,7 +1109,7 @@ dependencies = [ "proc-macro2", "quote", "serde_derive_internals", - "syn 2.0.77", + "syn 2.0.79", ] [[package]] @@ -1119,7 +1135,7 @@ checksum = "243902eda00fad750862fc144cea25caca5e20d615af0a81bee94ca738f1df1f" dependencies = [ "proc-macro2", "quote", - "syn 2.0.77", + "syn 2.0.79", ] [[package]] @@ -1130,7 +1146,7 @@ checksum = "18d26a20a969b9e3fdf2fc2d9f21eda6c40e2de84c9408bb5d3b05d499aae711" dependencies = [ "proc-macro2", "quote", - "syn 2.0.77", + "syn 2.0.79", ] [[package]] @@ -1181,7 +1197,7 @@ dependencies = [ "darling", "proc-macro2", "quote", - "syn 2.0.77", + "syn 2.0.79", ] [[package]] @@ -1241,7 +1257,7 @@ dependencies = [ "proc-macro2", "quote", "rustversion", - "syn 2.0.77", + "syn 2.0.79", ] [[package]] @@ -1335,9 +1351,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.77" +version = "2.0.79" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9f35bcdf61fd8e7be6caf75f429fdca8beb3ed76584befb503b1569faee373ed" +checksum = "89132cd0bf050864e1d38dc3bbc07a0eb8e7530af26344d3d2bbbef83499f590" dependencies = [ "proc-macro2", "quote", @@ -1374,7 +1390,7 @@ checksum = "08904e7672f5eb876eaaf87e0ce17857500934f4981c4a0ab2b4aa98baac7fc3" dependencies = [ "proc-macro2", "quote", - "syn 2.0.77", + "syn 2.0.79", ] [[package]] @@ -1446,9 +1462,9 @@ checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe" [[package]] name = "uniplate" -version = "0.1.1" +version = "0.1.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f1127ec835c86782a50431aca3c9028da4ded2ea6b1538e4023a64d09a1381a4" +checksum = "ac8053b2809b985835b37bf7ae1d7c48048e1b8f597acaac1ce37e7a27bd4b13" dependencies = [ "im", "proptest", @@ -1459,16 +1475,16 @@ dependencies = [ [[package]] name = "uniplate-derive" -version = "0.1.1" +version = "0.1.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b01981bd3fe2098383edf7b83bc76e760a87d96796c07f3da334f463f3477c11" +checksum = "cd60d7a363705f305acfb7d30b85ef9aad1744f09fa266e84f18408c12819f34" dependencies = [ - "itertools", + "itertools 0.12.1", "lazy_static", "log", "proc-macro2", "quote", - "syn 2.0.77", + "syn 2.0.79", ] [[package]] @@ -1525,7 +1541,7 @@ version = "6.3.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f25d498b63d1fdb376b4250f39ab3a5ee8d103957346abacd911e2d8b612c139" dependencies = [ - "itertools", + "itertools 0.13.0", "nom", ] @@ -1576,7 +1592,7 @@ dependencies = [ "once_cell", "proc-macro2", "quote", - "syn 2.0.77", + "syn 2.0.79", "wasm-bindgen-shared", ] @@ -1598,7 +1614,7 @@ checksum = "afc340c74d9005395cf9dd098506f7f44e38f2b4a21c6aaacf9a105ea5e1e836" dependencies = [ "proc-macro2", "quote", - "syn 2.0.77", + "syn 2.0.79", "wasm-bindgen-backend", "wasm-bindgen-shared", ] @@ -1727,5 +1743,5 @@ checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" dependencies = [ "proc-macro2", "quote", - "syn 2.0.77", + "syn 2.0.79", ] diff --git a/Cargo.toml b/Cargo.toml index 5df0533159..e4b405b613 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -16,6 +16,7 @@ members = [ "solvers/kissat", "solvers/minion", "solvers/chuffed", + "crates/gen_reduce", ] [workspace.lints.clippy] diff --git a/crates/gen_reduce/Cargo.toml b/crates/gen_reduce/Cargo.toml new file mode 100644 index 0000000000..7635a0d615 --- /dev/null +++ b/crates/gen_reduce/Cargo.toml @@ -0,0 +1,11 @@ +[package] +name = "gen_reduce" +version = "0.1.0" +edition = "2021" + +[dependencies] +uniplate = { version = "0.1.0" } + + +[lints] +workspace = true diff --git a/crates/gen_reduce/src/lib.rs b/crates/gen_reduce/src/lib.rs new file mode 100644 index 0000000000..3cc9d12648 --- /dev/null +++ b/crates/gen_reduce/src/lib.rs @@ -0,0 +1,257 @@ +use std::collections::VecDeque; +use uniplate::Uniplate; + +pub trait Rule +where + T: Uniplate, +{ + fn apply(&self, commands: &mut Commands, subtree: &T, meta: &M) -> Result; +} + +#[derive(Clone, Debug, PartialEq, Eq)] +pub enum Error { + /// The rule does not apply to the current node, but other rules might. + NotApplicable, + + /// The current node and its descendants up to a given depth should be ignored. + /// With a depth of `0`, only the current node is ignored. + /// + /// No rules are attempted on the ignored nodes. + Ignore(u32), + + /// The current node and all its descendants should be ignored. + /// Equivalent to `Ignore(Infinity)` + /// + /// No rules are attempted on the ignored nodes. + Prune, +} + +enum Command +where + T: Uniplate, +{ + Transform(fn(&T) -> T), + MutMeta(fn(&mut M)), +} + +/// A queue of commands to be applied after every successful rule application. +pub struct Commands +where + T: Uniplate, +{ + commands: VecDeque>, +} + +impl Commands +where + T: Uniplate, +{ + pub fn new() -> Self { + Self { + commands: VecDeque::new(), + } + } + + /// Apply the given transformation to the root node. + /// Commands are applied in order after the rule is applied. + pub fn transform(&mut self, f: fn(&T) -> T) { + self.commands.push_back(Command::Transform(f)); + } + + /// Update the associated metadata. + /// Commands are applied in order after the rule is applied. + pub fn mut_meta(&mut self, f: fn(&mut M)) { + self.commands.push_back(Command::MutMeta(f)); + } + + // Consumes and applies the commands currently in the queue. + fn apply(&mut self, mut tree: T, mut meta: M) -> (T, M) { + while let Some(cmd) = self.commands.pop_front() { + match cmd { + Command::Transform(f) => tree = f(&tree), + Command::MutMeta(f) => f(&mut meta), + } + } + (tree, meta) + } + + fn clear(&mut self) { + self.commands.clear(); + } +} + +// TODO: (Felix) how to allow rewrite selection? +// add a parameter F: `fn(Iterator<(R, T)>) -> Option`? Vec instead? + +// TODO: (Felix) dirty/clean optimisation: replace tree with a custom tree structure, +// which contains the original tree and adds metadata fields? + +/// Continuously apply rules to the tree until no more rules can be applied. +/// +/// The tree is traversed top-down, left-to-right. +/// At each node, rules are attempted in the order they are given. +/// If any rule returns a new subtree, that subtree replaces the existing one. +/// If no rules apply, the engine continues further down the tree. +/// +/// The command pattern is used to encapsulate side-effects caused by rules. +/// Commands are applied in order after the rule is successfully applied. +/// If a rule fails (returns an `Err`), all commands added by that rule are discarded. +pub fn reduce(rules: Vec, mut tree: T, mut meta: M) -> (T, M) +where + T: Uniplate, + R: Rule, +{ + let commands = &mut Commands::new(); + loop { + match reduce_iteration(commands, &rules, &tree, &meta, 0) { + Some(new_tree) => { + // Apply rule side-effects and set the current tree to the new one + (tree, meta) = commands.apply(new_tree, meta); + } + None => break, + } + } + (tree, meta) +} + +fn reduce_iteration( + commands: &mut Commands, + rules: &Vec, + subtree: &T, + meta: &M, + mut ignore_depth: u32, +) -> Option +where + T: Uniplate, + R: Rule, +{ + use Error::*; + + if ignore_depth == 0 { + // Try to apply rules to the current node + for rule in rules { + match rule.apply(commands, subtree, meta) { + Ok(new_tree) => return Some(new_tree), + Err(err) => { + commands.clear(); // Side effects are discarded + match err { + NotApplicable => continue, + Ignore(d) => { + ignore_depth = d + 1; // d == 0 -> ignore just this node + break; + } + Prune => return None, + } + } + } + } + } + + // Recursively apply rules to the children and return the updated subtree + let mut children = subtree.children(); + for i in 0..children.len() { + if let Some(new_child) = reduce_iteration( + commands, + rules, + &children[i], + meta, + if ignore_depth > 0 { + ignore_depth - 1 + } else { + 0 + }, + ) { + children[i] = new_child; + return Some(subtree.with_children(children)); + } + } + + None +} + +#[cfg(test)] +mod tests { + use super::*; + use uniplate::derive::Uniplate; + + #[derive(Debug, Clone, PartialEq, Eq, Uniplate)] + #[uniplate()] + enum Expr { + Add(Box, Box), + Mul(Box, Box), + Val(i32), + } + + enum ReductionRule { + AddZero, + MulOne, + Eval, + } + + impl Rule for ReductionRule { + fn apply(&self, _: &mut Commands, expr: &Expr, _: &()) -> Result { + use ReductionRule::*; + match self { + AddZero => match expr { + Expr::Add(a, b) if matches!(a.as_ref(), Expr::Val(0)) => Ok(*b.clone()), + Expr::Add(a, b) if matches!(b.as_ref(), Expr::Val(0)) => Ok(*a.clone()), + _ => Err(Error::NotApplicable), + }, + MulOne => match expr { + Expr::Mul(a, b) if matches!(a.as_ref(), Expr::Val(1)) => Ok(*b.clone()), + Expr::Mul(a, b) if matches!(b.as_ref(), Expr::Val(1)) => Ok(*a.clone()), + _ => Err(Error::NotApplicable), + }, + Eval => match expr { + Expr::Add(a, b) => match (a.as_ref(), b.as_ref()) { + (Expr::Val(x), Expr::Val(y)) => Ok(Expr::Val(x + y)), + _ => Err(Error::NotApplicable), + }, + Expr::Mul(a, b) => match (a.as_ref(), b.as_ref()) { + (Expr::Val(x), Expr::Val(y)) => Ok(Expr::Val(x * y)), + _ => Err(Error::NotApplicable), + }, + _ => Err(Error::NotApplicable), + }, + } + } + } + + #[test] + fn test_single_var() { + let expr = Expr::Val(42); + let (expr, _) = reduce(vec![ReductionRule::Eval], expr, ()); + assert_eq!(expr, Expr::Val(42)); + } + + #[test] + fn test_add_zero() { + let expr = Expr::Add(Box::new(Expr::Val(0)), Box::new(Expr::Val(42))); + let (expr, _) = reduce(vec![ReductionRule::AddZero], expr, ()); + assert_eq!(expr, Expr::Val(42)); + } + + #[test] + fn test_mul_one() { + let expr = Expr::Mul(Box::new(Expr::Val(1)), Box::new(Expr::Val(42))); + let (expr, _) = reduce(vec![ReductionRule::MulOne], expr, ()); + assert_eq!(expr, Expr::Val(42)); + } + + #[test] + fn test_eval() { + let expr = Expr::Add(Box::new(Expr::Val(1)), Box::new(Expr::Val(2))); + let (expr, _) = reduce(vec![ReductionRule::Eval], expr, ()); + assert_eq!(expr, Expr::Val(3)); + } + + #[test] + fn test_eval_nested() { + let expr = Expr::Mul( + Box::new(Expr::Add(Box::new(Expr::Val(1)), Box::new(Expr::Val(2)))), + Box::new(Expr::Val(3)), + ); + let (expr, _) = reduce(vec![ReductionRule::Eval], expr, ()); + assert_eq!(expr, Expr::Val(9)); + } +}