diff --git a/src/chase/engine.rs b/src/chase/engine.rs index a168ab1..377dabd 100644 --- a/src/chase/engine.rs +++ b/src/chase/engine.rs @@ -1,6 +1,6 @@ //! Core chase algorithm implementation. -use std::collections::{HashMap, HashSet}; +use std::collections::HashSet; use super::atom::Atom; use super::instance::Instance; @@ -39,6 +39,12 @@ struct NullGenerator { } impl NullGenerator { + fn seeded_from(instance: &Instance, rules: &[Rule]) -> Self { + Self { + counter: next_null_id(instance, rules), + } + } + fn fresh(&mut self) -> Term { let id = self.counter; self.counter += 1; @@ -47,8 +53,8 @@ impl NullGenerator { } /// A trigger represents a rule application: (rule_index, frontier_variable_bindings). -/// We use this to track which rule applications have already been performed, -/// preventing infinite loops with existential variables. +/// We track fired frontier bindings so the same active trigger is not re-applied +/// before its newly derived facts are visible in the instance. #[derive(Debug, Clone, PartialEq, Eq, Hash)] struct Trigger { rule_index: usize, @@ -78,8 +84,9 @@ impl Trigger { /// The chase repeatedly applies rules to derive new facts until no more /// facts can be derived (fixpoint) or a limit is reached. /// -/// This implementation uses the "restricted chase" approach which tracks -/// applied triggers to ensure termination with existential rules. +/// This implementation uses a restricted chase style active-trigger check: +/// a rule fires only when its head is not already satisfied for the current +/// frontier-variable bindings. pub fn chase(instance: Instance, rules: &[Rule]) -> ChaseResult { chase_with_config(instance, rules, ChaseConfig::default()) } @@ -90,7 +97,7 @@ pub fn chase_with_config( rules: &[Rule], config: ChaseConfig, ) -> ChaseResult { - let mut null_gen = NullGenerator::default(); + let mut null_gen = NullGenerator::seeded_from(&instance, rules); let mut applied_triggers: HashSet = HashSet::new(); let mut steps = 0; @@ -138,23 +145,13 @@ fn chase_step( // Create a trigger to check if we've already applied this let trigger = Trigger::new(rule_idx, rule, &subst); - // Skip if already applied (prevents infinite loops with existentials) + // Skip if already applied in this materialization if applied_triggers.contains(&trigger) { continue; } - // For rules without existentials, check if head is already satisfied - if rule.existential_variables().is_empty() { - let head_facts: Vec<_> = rule - .head - .iter() - .map(|atom| subst.apply_atom(atom)) - .collect(); - - // Skip if all head facts already exist - if head_facts.iter().all(|f| instance.contains(f)) { - continue; - } + if head_is_satisfied(instance, rule, &subst) { + continue; } // Mark this trigger as applied @@ -208,22 +205,24 @@ fn find_body_matches(instance: &Instance, body: &[Atom]) -> Vec { results } +fn head_is_satisfied(instance: &Instance, rule: &Rule, subst: &Substitution) -> bool { + let head = rule + .head + .iter() + .map(|atom| subst.apply_atom(atom)) + .collect::>(); + + !find_body_matches(instance, &head).is_empty() +} + /// Apply a rule head with the given substitution, generating fresh nulls for existentials. fn apply_rule_head(rule: &Rule, subst: &Substitution, null_gen: &mut NullGenerator) -> Vec { - let existentials = rule.existential_variables(); - - // Create a mapping for existential variables to fresh nulls let mut extended_subst = subst.clone(); - let mut null_map: HashMap = HashMap::new(); + let mut existentials = rule.existential_variables().into_iter().collect::>(); + existentials.sort(); - for var in &existentials { - let null = null_gen.fresh(); - null_map.insert(var.clone(), null); - } - - // Add null mappings to substitution - for (var, null) in null_map { - extended_subst.bind(var, null); + for var in existentials { + extended_subst.bind(var, null_gen.fresh()); } // Generate head atoms @@ -233,6 +232,33 @@ fn apply_rule_head(rule: &Rule, subst: &Substitution, null_gen: &mut NullGenerat .collect() } +fn next_null_id(instance: &Instance, rules: &[Rule]) -> usize { + let instance_max = instance + .iter() + .flat_map(|atom| atom.terms.iter()) + .filter_map(term_null_id) + .max(); + let rule_max = rules + .iter() + .flat_map(|rule| rule.body.iter().chain(rule.head.iter())) + .flat_map(|atom| atom.terms.iter()) + .filter_map(term_null_id) + .max(); + + instance_max + .into_iter() + .chain(rule_max) + .max() + .map_or(0, |id| id.saturating_add(1)) +} + +fn term_null_id(term: &Term) -> Option { + match term { + Term::Null(id) => Some(*id), + _ => None, + } +} + #[cfg(test)] mod tests { use super::*; diff --git a/src/frontend/provenance.rs b/src/frontend/provenance.rs index 9bab970..6bb4618 100644 --- a/src/frontend/provenance.rs +++ b/src/frontend/provenance.rs @@ -29,6 +29,12 @@ struct NullGenerator { } impl NullGenerator { + fn seeded_from(instance: &Instance, rules: &[Rule]) -> Self { + Self { + counter: next_null_id(instance, rules), + } + } + fn fresh(&mut self) -> Term { let id = self.counter; self.counter += 1; @@ -70,7 +76,7 @@ pub fn materialize(base_instance: Instance, rules: &[Rule]) -> MaterializedState .cloned() .map(|fact| (fact, Derivation::Input)) .collect::>(); - let mut null_gen = NullGenerator::default(); + let mut null_gen = NullGenerator::seeded_from(&instance, rules); let mut applied_triggers = HashSet::new(); let mut steps = 0; @@ -175,15 +181,8 @@ fn chase_step( continue; } - if rule.existential_variables().is_empty() { - let head_facts = rule - .head - .iter() - .map(|atom| subst.apply_atom(atom)) - .collect::>(); - if head_facts.iter().all(|fact| instance.contains(fact)) { - continue; - } + if head_is_satisfied(instance, rule, &subst) { + continue; } applied_triggers.insert(trigger); @@ -213,10 +212,22 @@ fn chase_step( pending } +fn head_is_satisfied(instance: &Instance, rule: &Rule, subst: &Substitution) -> bool { + let head = rule + .head + .iter() + .map(|atom| subst.apply_atom(atom)) + .collect::>(); + + !find_matches(instance, &head).is_empty() +} + fn apply_rule_head(rule: &Rule, subst: &Substitution, null_gen: &mut NullGenerator) -> Vec { let mut extended_subst = subst.clone(); + let mut existentials = rule.existential_variables().into_iter().collect::>(); + existentials.sort(); - for variable in rule.existential_variables() { + for variable in existentials { extended_subst.bind(variable, null_gen.fresh()); } @@ -226,6 +237,33 @@ fn apply_rule_head(rule: &Rule, subst: &Substitution, null_gen: &mut NullGenerat .collect() } +fn next_null_id(instance: &Instance, rules: &[Rule]) -> usize { + let instance_max = instance + .iter() + .flat_map(|atom| atom.terms.iter()) + .filter_map(term_null_id) + .max(); + let rule_max = rules + .iter() + .flat_map(|rule| rule.body.iter().chain(rule.head.iter())) + .flat_map(|atom| atom.terms.iter()) + .filter_map(term_null_id) + .max(); + + instance_max + .into_iter() + .chain(rule_max) + .max() + .map_or(0, |id| id.saturating_add(1)) +} + +fn term_null_id(term: &Term) -> Option { + match term { + Term::Null(id) => Some(*id), + _ => None, + } +} + fn render_derivation( atom: &Atom, state: &MaterializedState, diff --git a/tests/property_tests.rs b/tests/property_tests.rs index 96ecd16..c10a62b 100644 --- a/tests/property_tests.rs +++ b/tests/property_tests.rs @@ -148,7 +148,7 @@ fn fixpoint_is_stable() { .then("Q", vec![Term::var("X")]) .build(); - let result1 = chase(instance, &[rule.clone()]); + let result1 = chase(instance, std::slice::from_ref(&rule)); prop_assert!(result1.terminated); let result2 = chase(result1.instance.clone(), &[rule]); @@ -426,7 +426,7 @@ fn substitution_preserves_arity() { runner .run(&strategy, |(pred, vars, replacement)| { - let atom = Atom::new(&pred, vars.iter().map(|v| Term::var(v)).collect()); + let atom = Atom::new(&pred, vars.iter().map(Term::var).collect()); let mut subst = Substitution::new(); for var in &vars { diff --git a/tests/regression_tests.rs b/tests/regression_tests.rs index 8b13789..b4aae27 100644 --- a/tests/regression_tests.rs +++ b/tests/regression_tests.rs @@ -1 +1,95 @@ +use chase_rs::chase::rule::RuleBuilder; +use chase_rs::frontend::Session; +use chase_rs::frontend::provenance::materialize; +use chase_rs::{Atom, Instance, Term, chase}; +#[test] +fn existential_trigger_stays_inactive_when_head_is_already_satisfied() { + let instance: Instance = vec![ + Atom::new("Person", vec![Term::constant("alice")]), + Atom::new( + "HasSSN", + vec![Term::constant("alice"), Term::constant("known")], + ), + ] + .into_iter() + .collect(); + + let rule = RuleBuilder::new() + .when("Person", vec![Term::var("X")]) + .then("HasSSN", vec![Term::var("X"), Term::var("Y")]) + .build(); + + let result = chase(instance, &[rule]); + + assert!(result.terminated); + assert_eq!(result.steps, 0); + assert_eq!(result.instance.facts_for_predicate("HasSSN").len(), 1); +} + +#[test] +fn fresh_nulls_skip_existing_input_null_ids() { + let instance: Instance = vec![ + Atom::new("Seed", vec![Term::null(0)]), + Atom::new("Person", vec![Term::constant("alice")]), + ] + .into_iter() + .collect(); + + let rule = RuleBuilder::new() + .when("Person", vec![Term::var("X")]) + .then("HasSSN", vec![Term::var("X"), Term::var("Y")]) + .build(); + + let result = chase(instance, &[rule]); + + assert!(result.terminated); + assert_eq!(result.instance.facts_for_predicate("HasSSN").len(), 1); + + let fact = result.instance.facts_for_predicate("HasSSN")[0]; + assert!(matches!(fact.terms[1], Term::Null(id) if id > 0)); +} + +#[test] +fn frontend_materialization_respects_existing_existential_witnesses() { + let mut session = Session::new(); + let output = session + .execute_script( + "fact Person(alice).\n\ + fact HasSSN(alice, known).\n\ + rule Person(?X) -> HasSSN(?X, ?Y).\n\ + run.\n\ + query HasSSN(alice, ?Y)?", + ) + .unwrap(); + + assert!(output.contains("1 row(s)")); + assert!(output.contains("?Y = known")); + assert!(!output.contains("⊥")); +} + +#[test] +fn frontend_materialization_starts_after_existing_null_ids() { + let instance: Instance = vec![ + Atom::new("Seed", vec![Term::null(7)]), + Atom::new("Employee", vec![Term::constant("alice")]), + ] + .into_iter() + .collect(); + + let rule = RuleBuilder::new() + .when("Employee", vec![Term::var("X")]) + .then("WorksIn", vec![Term::var("X"), Term::var("Dept")]) + .build(); + + let state = materialize(instance, &[rule]); + + assert!(state.result.terminated); + assert_eq!( + state.result.instance.facts_for_predicate("WorksIn").len(), + 1 + ); + + let fact = state.result.instance.facts_for_predicate("WorksIn")[0]; + assert!(matches!(fact.terms[1], Term::Null(id) if id > 7)); +}