Make the implementation more robust

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<Trigger> = HashSet::new();
     let mut steps = 0;
 
@@ -138,24 +145,14 @@ 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)) {
+            if head_is_satisfied(instance, rule, &subst) {
                 continue;
             }
-            }
 
             // Mark this trigger as applied
             applied_triggers.insert(trigger);
@@ -208,22 +205,24 @@ fn find_body_matches(instance: &Instance, body: &[Atom]) -> Vec<Substitution> {
     results
 }
 
+fn head_is_satisfied(instance: &Instance, rule: &Rule, subst: &Substitution) -> bool {
+    let head = rule
+        .head
+        .iter()
+        .map(|atom| subst.apply_atom(atom))
+        .collect::<Vec<_>>();
+
+    !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<Atom> {
-    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<String, Term> = HashMap::new();
+    let mut existentials = rule.existential_variables().into_iter().collect::<Vec<_>>();
+    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<usize> {
+    match term {
+        Term::Null(id) => Some(*id),
+        _ => None,
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;

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::<HashMap<_, _>>();
-    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,16 +181,9 @@ fn chase_step(
                 continue;
             }
 
-            if rule.existential_variables().is_empty() {
-                let head_facts = rule
-                    .head
-                    .iter()
-                    .map(|atom| subst.apply_atom(atom))
-                    .collect::<Vec<_>>();
-                if head_facts.iter().all(|fact| instance.contains(fact)) {
+            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::<Vec<_>>();
+
+    !find_matches(instance, &head).is_empty()
+}
+
 fn apply_rule_head(rule: &Rule, subst: &Substitution, null_gen: &mut NullGenerator) -> Vec<Atom> {
     let mut extended_subst = subst.clone();
+    let mut existentials = rule.existential_variables().into_iter().collect::<Vec<_>>();
+    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<usize> {
+    match term {
+        Term::Null(id) => Some(*id),
+        _ => None,
+    }
+}
+
 fn render_derivation(
     atom: &Atom,
     state: &MaterializedState,

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 {

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));
+}